0 | module TTImp.ProcessData

  2 | import Core.CompileExpr

  3 | import Core.Context.Data

  4 | import Core.Env

  5 | import Core.Hash

  6 | import Core.Metadata

  7 | import Core.UnifyState

  8 | import Core.Value

 10 | import Idris.REPL.Opts

 11 | import Idris.Syntax

 13 | import TTImp.BindImplicits

 14 | import TTImp.Elab.Check

 15 | import TTImp.Elab.Utils

 16 | import TTImp.Elab

 17 | import TTImp.TTImp

 19 | import Data.DPair

 20 | import Libraries.Data.NameMap

 21 | import Libraries.Data.NatSet

 22 | import Libraries.Data.WithDefault

 24 | %default covering

 26 | processDataOpt : {auto c : Ref Ctxt Defs} ->

 27 |                  FC -> Name -> DataOpt -> Core ()

 28 | processDataOpt fc n NoHints

 29 |     = pure ()

 30 | processDataOpt fc ndef (SearchBy dets)

 31 |     = setDetermining fc ndef dets

 32 | processDataOpt fc ndef UniqueSearch

 33 |     = setUniqueSearch fc ndef True

 34 | processDataOpt fc ndef External

 35 |     = setExternal fc ndef True

 36 | processDataOpt fc ndef NoNewtype

 37 |     = pure ()

 39 | checkRetType : {auto c : Ref Ctxt Defs} ->

 40 |                Env Term vars -> NF vars ->

 41 |                (NF vars -> Core ()) -> Core ()

 42 | checkRetType env (NBind fc x (Pi _ _ _ ty) sc) chk

 43 |     = do defs <- get Ctxt

 44 |          checkRetType env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder))) chk

 45 | checkRetType env nf chk = chk nf

 47 | checkIsType : {auto c : Ref Ctxt Defs} ->

 48 |               FC -> Name -> Env Term vars -> NF vars -> Core ()

 49 | checkIsType loc n env nf

 50 |     = checkRetType env nf $

 51 |          \case

 52 |            NType {} => pure ()

 53 |            _ => throw $ BadTypeConType loc n

 55 | checkFamily : {auto c : Ref Ctxt Defs} ->

 56 |               FC -> Name -> Name -> Env Term vars -> NF vars -> Core ()

 57 | checkFamily loc cn tn env nf

 58 |     = checkRetType env nf $

 59 |          \case

 60 |            NType {} => throw $ BadDataConType loc cn tn

 61 |            NTCon _ n' _ _ =>

 62 |                  if tn == n'

 63 |                     then pure ()

 64 |                     else throw $ BadDataConType loc cn tn

 65 |            _ => throw $ BadDataConType loc cn tn

 67 | updateNS : Name -> Name -> RawImp -> RawImp

 68 | updateNS orig ns (IPi fc c p n ty sc) = IPi fc c p n ty (updateNS orig ns sc)

 69 | updateNS orig ns tm = updateNSApp tm

 70 |   where

 71 |     updateNSApp : RawImp -> RawImp

 72 |     updateNSApp (IVar fc n) -- data type type, must be defined in this namespace

 73 |         = if n == orig

 74 |              then IVar fc ns

 75 |              else IVar fc n

 76 |     updateNSApp (IApp fc f arg) = IApp fc (updateNSApp f) arg

 77 |     updateNSApp (IAutoApp fc f arg) = IAutoApp fc (updateNSApp f) arg

 78 |     updateNSApp (INamedApp fc f n arg) = INamedApp fc (updateNSApp f) n arg

 79 |     updateNSApp t = t

 81 | checkCon : {vars : _} ->

 82 |            {auto c : Ref Ctxt Defs} ->

 83 |            {auto m : Ref MD Metadata} ->

 84 |            {auto u : Ref UST UState} ->

 85 |            {auto s : Ref Syn SyntaxInfo} ->

 86 |            {auto o : Ref ROpts REPLOpts} ->

 87 |            List ElabOpt -> NestedNames vars ->

 88 |            Env Term vars -> Visibility -> (orig : Name) -> (resolved : Name) ->

 89 |            ImpTy -> Core Constructor

 90 | checkCon {vars} opts nest env vis tn_in tn ty_raw

 91 |     = do let cn_in = ty_raw.tyName

 92 |          let fc = ty_raw.fc

 93 |          cn <- inCurrentNS cn_in.val

 94 |          let ty_raw = updateNS tn_in tn ty_raw.val

 95 |          log "declare.data.constructor" 5 $ "Checking constructor type " ++ show cn ++ " : " ++ show ty_raw

 96 |          log "declare.data.constructor" 10 $ "Updated " ++ show (tn_in, tn)

 98 |          defs <- get Ctxt

 99 |          -- Check 'cn' is undefined

100 |          Nothing <- lookupCtxtExact cn (gamma defs)

101 |              | Just gdef => throw (AlreadyDefined fc cn)

102 |          u <- uniVar fc

103 |          ty <-

104 |              wrapErrorC opts (InCon cn_in) $

105 |                    checkTerm !(resolveName cn) InType opts nest env

106 |                               (IBindHere fc (PI erased) ty_raw)

107 |                               (gType fc u)

109 |          -- Check 'ty' returns something in the right family

110 |          checkFamily fc cn tn env !(nf defs env ty)

111 |          let fullty = abstractEnvType fc env ty

112 |          logTermNF "declare.data.constructor" 5 ("Constructor " ++ show cn) Env.empty fullty

114 |          traverse_ addToSave (keys (getMetas ty))

115 |          addToSave cn

116 |          log "declare.data.constructor" 10 $ "Saving from " ++ show cn ++ ": " ++ show (keys (getMetas ty))

118 |          case vis of

119 |               Public => do addHashWithNames cn

120 |                            addHashWithNames fullty

121 |                            log "module.hash" 15 "Adding hash for data constructor: \{show cn}"

122 |               _ => pure ()

123 |          pure (Mk [fc, NoFC cn, !(getArity defs Env.empty fullty)] fullty)

126 | getIndexPats : {auto c : Ref Ctxt Defs} ->

127 |                ClosedTerm -> Core (List ClosedNF)

128 | getIndexPats tm

129 |     = do defs <- get Ctxt

130 |          tmnf <- nf defs Env.empty tm

131 |          ret <- getRetType defs tmnf

132 |          getPats defs ret

133 |   where

134 |     getRetType : Defs -> ClosedNF -> Core ClosedNF

135 |     getRetType defs (NBind fc _ (Pi {}) sc)

136 |         = do sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))

137 |              getRetType defs sc'

138 |     getRetType defs t = pure t

140 |     getPats : Defs -> ClosedNF -> Core (List ClosedNF)

141 |     getPats defs (NTCon fc _ _ args)

142 |         = do args' <- traverse (evalClosure defs . snd) args

143 |              pure (toList args')

144 |     getPats defs _ = pure [] -- Can't happen if we defined the type successfully!

146 | getDetags : {auto c : Ref Ctxt Defs} ->

147 |             FC -> List ClosedTerm -> Core (Maybe NatSet)

148 | getDetags fc [] = pure (Just NatSet.empty) -- empty type, trivially detaggable

149 | getDetags fc [t] = pure (Just NatSet.empty) -- one constructor, trivially detaggable

150 | getDetags fc tys

151 |    = do ps <- traverse getIndexPats tys

152 |         ds <- getDisjointPos 0 (transpose ps)

153 |         pure $ ds <$ guard (not (isEmpty ds))

154 |   where

155 |     mutual

156 |       disjointArgs : List ClosedNF -> List ClosedNF -> Core Bool

157 |       disjointArgs [] _ = pure False

158 |       disjointArgs _ [] = pure False

159 |       disjointArgs (a :: args) (a' :: args')

160 |           = if !(disjoint a a')

161 |                then pure True

162 |                else disjointArgs args args'

164 |       disjoint : ClosedNF -> ClosedNF -> Core Bool

165 |       disjoint (NDCon _ _ t _ args) (NDCon _ _ t' _ args')

166 |           = if t /= t'

167 |                then pure True

168 |                else do defs <- get Ctxt

169 |                        argsnf <- traverse (evalClosure defs . snd) args

170 |                        args'nf <- traverse (evalClosure defs . snd) args'

171 |                        disjointArgs argsnf args'nf

172 |       disjoint (NTCon _ n _ args) (NTCon _ n' _ args')

173 |           = if n /= n'

174 |                then pure True

175 |                else do defs <- get Ctxt

176 |                        argsnf <- traverse (evalClosure defs . snd) args

177 |                        args'nf <- traverse (evalClosure defs . snd) args'

178 |                        disjointArgs argsnf args'nf

179 |       disjoint (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c')

180 |       disjoint _ _ = pure False

182 |     allDisjointWith : ClosedNF -> List ClosedNF -> Core Bool

183 |     allDisjointWith val [] = pure True

184 |     allDisjointWith (NErased {}) _ = pure False

185 |     allDisjointWith val (nf :: nfs)

186 |         = do ok <- disjoint val nf

187 |              if ok then allDisjointWith val nfs

188 |                    else pure False

190 |     allDisjoint : List ClosedNF -> Core Bool

191 |     allDisjoint [] = pure True

192 |     allDisjoint (NErased _ _ :: _) = pure False

193 |     allDisjoint (nf :: nfs)

194 |         = do ok <- allDisjoint nfs

195 |              if ok then allDisjointWith nf nfs

196 |                    else pure False

198 |     -- Which argument positions have completely disjoint contructors

199 |     getDisjointPos : Nat -> List (List ClosedNF) -> Core NatSet

200 |     getDisjointPos i [] = pure NatSet.empty

201 |     getDisjointPos i (args :: argss)

202 |         = do rest <- getDisjointPos (1 + i) argss

203 |              if !(allDisjoint args)

204 |                 then pure (NatSet.insert i rest)

205 |                 else pure rest

208 | getRelevantArg : {auto c : Ref Ctxt Defs} ->

209 |                  Defs -> Nat -> Maybe Nat -> Bool -> ClosedNF ->

210 |                  Core (Maybe (Bool, Nat))

211 | getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)

212 |     = branchZero (getRelevantArg defs (1 + i) rel world

213 |                               !(sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))))

214 |                  (case !(evalClosure defs val) of

215 |                        -- %World is never inspected, so might as well be deleted from data types,

216 |                        -- although it needs care when compiling to ensure that the function that

217 |                        -- returns the IO/%World type isn't erased

218 |                        (NPrimVal _ $ PrT WorldType) =>

219 |                            getRelevantArg defs (1 + i) rel False

220 |                                !(sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder)))

221 |                        _ =>

222 |                        -- if we haven't found a relevant argument yet, make

223 |                        -- a note of this one and keep going. Otherwise, we

224 |                        -- have more than one, so give up.

225 |                            maybe (do sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))

226 |                                      getRelevantArg defs (1 + i) (Just i) False sc')

227 |                                  (const (pure Nothing))

228 |                                  rel)

229 |                  rig

230 | getRelevantArg defs i rel world tm

231 |     = pure ((world,) <$> rel)

236 | findNewtype : {auto c : Ref Ctxt Defs} ->

237 |               List Constructor -> Core ()

238 | findNewtype [con]

239 |     = do defs <- get Ctxt

240 |          Just arg <- getRelevantArg defs 0 Nothing True !(nf defs Env.empty con.val)

241 |               | Nothing => pure ()

242 |          updateDef con.name.val $

243 |                \case

244 |                  DCon t a _ => Just $ DCon t a $ Just arg

245 |                  _ => Nothing

246 | findNewtype _ = pure ()

248 | hasArgs : Nat -> Term vs -> Bool

249 | hasArgs (S k) (Bind _ _ (Pi _ c _ _) sc)

250 |     = if isErased c

251 |          then hasArgs (S k) sc

252 |          else hasArgs k sc

253 | hasArgs (S k) _ = False

254 | hasArgs Z (Bind _ _ (Pi _ c _ _) sc)

255 |     = if isErased c

256 |          then hasArgs Z sc

257 |          else False

258 | hasArgs Z _ = True

261 | firstArg : Term vs -> Maybe (Exists Term)

262 | firstArg (Bind _ _ (Pi _ c _ val) sc)

263 |     = if isErased c

264 |          then firstArg sc

265 |          else Just $ Evidence _ val

266 | firstArg tm = Nothing

268 | typeCon : Term vs -> Maybe Name

269 | typeCon (Ref _ (TyCon _) n) = Just n

270 | typeCon (App _ fn _) = typeCon fn

271 | typeCon _ = Nothing

273 | shaped : {auto c : Ref Ctxt Defs} ->

274 |          (forall vs . Term vs -> Bool) ->

275 |          List Constructor -> Core (Maybe Name)

276 | shaped as [] = pure Nothing

277 | shaped as (c :: cs)

278 |     = do defs <- get Ctxt

279 |          if as !(normalise defs Env.empty c.val)

280 |             then pure (Just c.name.val)

281 |             else shaped as cs

290 | calcListy : {auto c : Ref Ctxt Defs} ->

291 |             FC -> List Constructor -> Core Bool

292 | calcListy fc cs@[_]

293 |     = do Just cons <- shaped (hasArgs 2) cs

294 |               | Nothing => pure False

295 |          setFlag fc cons (ConType CONS)

296 |          pure True

297 | calcListy fc cs@[_, _]

298 |     = do Just nil <- shaped (hasArgs 0) cs

299 |               | Nothing => pure False

300 |          Just cons <- shaped (hasArgs 2) cs

301 |               | Nothing => pure False

302 |          setFlag fc nil (ConType NIL)

303 |          setFlag fc cons (ConType CONS)

304 |          pure True

305 | calcListy _ _ = pure False

309 | calcMaybe : {auto c : Ref Ctxt Defs} ->

310 |             FC -> List Constructor -> Core Bool

311 | calcMaybe fc cs@[_, _]

312 |     = do Just nothing <- shaped (hasArgs 0) cs

313 |               | Nothing => pure False

314 |          Just just <- shaped (hasArgs 1) cs

315 |               | Nothing => pure False

316 |          setFlag fc nothing (ConType NOTHING)

317 |          setFlag fc just (ConType JUST)

318 |          pure True

319 | calcMaybe _ _ = pure False

321 | calcEnum : {auto c : Ref Ctxt Defs} ->

322 |            FC -> List Constructor -> Core Bool

323 | calcEnum fc cs

324 |     = if !(allM isNullary cs)

325 |          then do traverse_ (\c => setFlag fc c (ConType (ENUM $ length cs))) (map (.name.val) cs)

326 |                  pure True

327 |          else pure False

328 |   where

329 |     isNullary : Constructor -> Core Bool

330 |     isNullary c

331 |         = do defs <- get Ctxt

332 |              pure $ hasArgs 0 !(normalise defs Env.empty c.val)

334 | calcRecord : {auto c : Ref Ctxt Defs} ->

335 |              FC -> List Constructor -> Core Bool

336 | calcRecord fc [c]

337 |     = do setFlag fc c.name.val (ConType RECORD)

338 |          pure True

339 | calcRecord _ _ = pure False

344 | calcNaty : {auto c : Ref Ctxt Defs} ->

345 |            FC -> Name -> List Constructor -> Core Bool

346 | calcNaty fc tyCon cs@[_, _]

347 |     = do Just zero <- shaped (hasArgs 0) cs

348 |               | Nothing => pure False

349 |          Just succ <- shaped (hasArgs 1) cs

350 |               | Nothing => pure False

351 |          let Just succCon = find (\con => con.name.val == succ) cs

352 |               | Nothing => pure False

353 |          let Just (Evidence _ succArgTy) = firstArg succCon.val

354 |               | Nothing => pure False

355 |          let Just succArgCon = typeCon succArgTy

356 |               | Nothing => pure False

357 |          if succArgCon == tyCon

358 |             then do setFlag fc zero (ConType ZERO)

359 |                     setFlag fc succ (ConType SUCC)

360 |                     pure True

361 |             else pure False

362 | calcNaty _ _ _ = pure False

365 | calcUnity : {auto c : Ref Ctxt Defs} ->

366 |             FC -> Name -> List Constructor -> Core Bool

367 | calcUnity fc tyCon cs@[_]

368 |     = do Just mkUnit <- shaped (hasArgs 0) cs

369 |               | Nothing => pure False

370 |          setFlag fc mkUnit (ConType UNIT)

371 |          pure True

372 | calcUnity _ _ _ = pure False

374 | calcConInfo : {auto c : Ref Ctxt Defs} ->

375 |               FC -> Name -> List Constructor -> Core ()

376 | calcConInfo fc type cons

377 |    = do False <- calcNaty fc type cons

378 |            | True => pure ()

379 |         False <- calcUnity fc type cons

380 |            | True => pure ()

381 |         False <- calcListy fc cons

382 |            | True => pure ()

383 |         False <- calcMaybe fc cons

384 |            | True => pure ()

385 |         False <- calcEnum fc cons

386 |            | True => pure ()

387 |         False <- calcRecord fc cons

388 |            | True => pure ()

389 |         pure ()

390 |      -- ... maybe more to come? The Bool just says when to stop looking

393 | processData : {vars : _} ->

394 |               {auto c : Ref Ctxt Defs} ->

395 |               {auto m : Ref MD Metadata} ->

396 |               {auto u : Ref UST UState} ->

397 |               {auto s : Ref Syn SyntaxInfo} ->

398 |               {auto o : Ref ROpts REPLOpts} ->

399 |               List ElabOpt -> NestedNames vars ->

400 |               Env Term vars -> FC ->

401 |               WithDefault Visibility Private -> Maybe TotalReq ->

402 |               ImpData -> Core ()

403 | processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)

404 |     = do n <- inCurrentNS n_in

405 |          ty_raw <- bindTypeNames fc [] (toList vars) ty_raw

407 |          defs <- get Ctxt

408 |          -- Check 'n' is undefined

409 |          Nothing <- lookupCtxtExact n (gamma defs)

410 |              | Just gdef => throw (AlreadyDefined fc n)

412 |          u <- uniVar fc

413 |          (ty, _) <-

414 |              wrapErrorC eopts (InCon $ MkFCVal dfc n) $

415 |                     elabTerm !(resolveName n) InType eopts nest env

416 |                               (IBindHere fc (PI erased) ty_raw)

417 |                               (Just (gType dfc u))

418 |          let fullty = abstractEnvType dfc env ty

419 |          logTermNF "declare.data" 5 ("data " ++ show n) Env.empty fullty

421 |          checkIsType fc n env !(nf defs env ty)

422 |          arity <- getArity defs Env.empty fullty

424 |          -- Add the type constructor as a placeholder

425 |          tidx <- addDef n (newDef fc n top vars fullty def_vis

426 |                           (TCon arity NatSet.empty NatSet.empty defaultFlags [] Nothing Nothing))

427 |          addMutData (Resolved tidx)

428 |          defs <- get Ctxt

429 |          traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)

431 |          traverse_ addToSave (keys (getMetas ty))

432 |          addToSave n

433 |          log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))

435 |          case collapseDefault def_vis of

436 |               Private => pure ()

437 |               _ => do addHashWithNames n

438 |                       addHashWithNames fullty

439 |                       log "module.hash" 15 "Adding hash for data declaration with name \{show n}"

441 |          whenJust mbtot $ \ tot => do

442 |              log "declare.data" 5 $ "setting totality flag for data declaration with name \{show n}"

443 |              setFlag fc n (SetTotal tot)

445 | processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw)

446 |     = do n <- inCurrentNS n_in

448 |          log "declare.data" 1 $ "Processing " ++ show n

449 |          defs <- get Ctxt

451 |          mmetasfullty <- flip traverseOpt mty_raw $ \ ty_raw => do

452 |            ty_raw <- bindTypeNames fc [] (toList vars) ty_raw

454 |            u <- uniVar fc

455 |            (ty, _) <-

456 |                wrapErrorC eopts (InCon $ MkFCVal fc n) $

457 |                       elabTerm !(resolveName n) InType eopts nest env

458 |                                 (IBindHere fc (PI erased) ty_raw)

459 |                                 (Just (gType dfc u))

460 |            checkIsType fc n env !(nf defs env ty)

462 |            pure (keys (getMetas ty), abstractEnvType dfc env ty)

464 |          let metas = maybe empty fst mmetasfullty

465 |          let mfullty = map snd mmetasfullty

467 |          -- If n exists, check it's the same type as we have here, is

468 |          -- a type constructor, and has either the same visibility and totality

469 |          -- or we don't define them.

470 |          -- When looking up, note the data types which were undefined at the

471 |          -- point of declaration.

472 |          ndefm <- lookupCtxtExact n (gamma defs)

473 |          (mw, vis, tot, fullty) <- the (Core (List Name, Visibility, Maybe TotalReq, ClosedTerm)) $ case ndefm of

474 |                   Nothing => case mfullty of

475 |                     Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}")

476 |                     Just fullty => pure ([], collapseDefault def_vis, mbtot, fullty)

477 |                   Just ndef => do

478 |                     vis <- the (Core Visibility) $ case collapseDefaults ndef.visibility def_vis of

479 |                       Right finalVis => pure finalVis

480 |                       Left (oldVis, newVis) => do

481 |                         -- TODO : In a later release, at least after 0.7.0, replace this with an error.

482 |                         recordWarning (IncompatibleVisibility fc oldVis newVis n)

483 |                         pure (max oldVis newVis)

485 |                     let declTot = findSetTotal $ ndef.flags

486 |                     tot <- case (mbtot, declTot) of

487 |                       (Just oldTot, Just newTot) => do

488 |                         when (oldTot /= newTot) $ throw $ GenericMsgSol fc

489 |                           "Data \{show n_in} has been forward-declared with totality `\{show oldTot}`, cannot change to `\{show newTot}`"

490 |                           "Possible solutions"

491 |                           [ "Use the same totality modifiers"

492 |                           , "Remove the totality modifier from the declaration"

493 |                           , "Remove the totality modifier from the definition"

494 |                           ]

495 |                         pure mbtot

496 |                       _ => pure $ mbtot <|> declTot

498 |                     case definition ndef of

499 |                       TCon _ _ _ flags mw Nothing _ => case mfullty of

500 |                         Nothing => pure (mw, vis, tot, type ndef)

501 |                         Just fullty =>

502 |                             do ok <- convert defs Env.empty fullty (type ndef)

503 |                                if ok then pure (mw, vis, tot, fullty)

504 |                                      else do logTermNF "declare.data" 1 "Previous" Env.empty (type ndef)

505 |                                              logTermNF "declare.data" 1 "Now" Env.empty fullty

506 |                                              throw (CantConvert fc (gamma defs) Env.empty (type ndef) fullty)

507 |                       _ => throw (AlreadyDefined fc n)

509 |          logTermNF "declare.data" 5 ("data " ++ show n) Env.empty fullty

511 |          arity <- getArity defs Env.empty fullty

513 |          -- Add the type constructor as a placeholder while checking

514 |          -- data constructors

515 |          tidx <- addDef n (newDef fc n linear vars fullty (specified vis)

516 |                           (TCon arity NatSet.empty NatSet.empty defaultFlags [] Nothing Nothing))

517 |          case vis of

518 |               Private => pure ()

519 |               _ => do addHashWithNames n

520 |                       addHashWithNames fullty

521 |                       log "module.hash" 15 "Adding hash for data declaration with name \{show n}"

523 |          -- Constructors are private if the data type as a whole is

524 |          -- export

525 |          let cvis = if vis == Export then Private else vis

526 |          cons <- traverse (checkCon eopts nest env cvis n_in (Resolved tidx)) cons_raw

528 |          let ddef = MkData (Mk [dfc, NoFC n, arity] fullty) cons

529 |          ignore $ addData vars vis tidx ddef

531 |          -- Flag data type as a newtype, if possible (See `findNewtype` for criteria).

532 |          -- Skip optimisation if the data type has specified `noNewtype` in its

533 |          -- options list.

534 |          when (not (NoNewtype `elem` opts)) $

535 |               findNewtype cons

537 |          -- Type is defined mutually with every data type undefined at the

538 |          -- point it was declared, and every data type undefined right now

539 |          defs <- get Ctxt

540 |          let mutWith = nub (mw ++ mutData defs)

541 |          log "declare.data" 3 $ show n ++ " defined in a mutual block with " ++ show mw

542 |          setMutWith fc (Resolved tidx) mw

544 |          traverse_ (processDataOpt fc (Resolved tidx)) opts

545 |          dropMutData (Resolved tidx)

547 |          detags <- getDetags fc (map val cons)

548 |          setDetags fc (Resolved tidx) detags

550 |          traverse_ addToSave metas

551 |          addToSave n

552 |          log "declare.data" 10 $

553 |            "Saving from " ++ show n ++ ": " ++ show metas

555 |          let connames = map (.name.val) cons

556 |          unless (NoHints `elem` opts) $

557 |               traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames

559 |          calcConInfo fc (Resolved tidx) cons

560 |          traverse_ updateErasable (Resolved tidx :: connames)

562 |          -- #1404

563 |          whenJust tot $ \ tot => do

564 |              log "declare.data" 5 $ "setting totality flag for \{show n} and its constructors"

565 |              for_ (n :: map (.name.val) cons) $ \ n => setFlag fc n (SetTotal tot)