0 | module Core.Context.Context

  2 | import        Core.Case.CaseTree

  3 | import        Core.CompileExpr

  4 | import        Core.Env

  5 | import public Core.Name

  6 | import public Core.Options.Log

  7 | import public Core.TT

  8 | import public Core.WithData

 10 | import public Algebra.SizeChange

 12 | import Data.IOArray

 13 | import Data.IORef

 14 | import Data.List1

 15 | import Data.String

 17 | import Libraries.Data.IntMap

 18 | import Libraries.Data.NameMap

 19 | import Libraries.Data.NatSet

 20 | import Libraries.Data.UserNameMap

 21 | import Libraries.Data.WithDefault

 22 | import Libraries.Data.SparseMatrix

 23 | import Libraries.Utils.Binary

 24 | import Libraries.Utils.Scheme

 26 | %hide LabelledValue.label

 27 | %hide KeyVal.label

 29 | public export

 30 | data Ref : (l : label) -> Type -> Type where

 31 |      [search l]

 32 |      MkRef : IORef a -> Ref x a

 34 | public export

 35 | data HoleInfo

 36 |         = NotHole

 37 |         | SolvedHole Nat

 39 | public export

 40 | record PMDefInfo where

 41 |   constructor MkPMDefInfo

 42 |   holeInfo : HoleInfo -- data if it comes from a solved hole

 43 |   alwaysReduce : Bool -- always reduce, even when quoting etc

 44 |                  -- typically for inlinable metavariable solutions

 45 |   externalDecl : Bool -- declared in another module, which may affect how it

 46 |                       -- is compiled

 47 | %name PMDefInfo pminfo

 50 | defaultPI : PMDefInfo

 51 | defaultPI = MkPMDefInfo NotHole False False

 53 | public export

 54 | record TypeFlags where

 55 |   constructor MkTypeFlags

 56 |   uniqueAuto : Bool  -- should 'auto' implicits check for uniqueness

 57 |   external : Bool -- defined externally (e.g. in a C or Scheme library)

 60 | defaultFlags : TypeFlags

 61 | defaultFlags = MkTypeFlags False False

 63 | public export

 64 | record HoleFlags where

 65 |   constructor MkHoleFlags

 66 |   implbind : Bool -- stands for an implicitly bound name

 67 |   precisetype : Bool -- don't generalise multiplicities when instantiating

 70 | holeInit : Bool -> HoleFlags

 71 | holeInit b = MkHoleFlags b False

 73 | public export

 74 | data Def : Type where

 75 |     None : Def -- Not yet defined

 76 |     PMDef : (pminfo : PMDefInfo) ->

 77 |             (args : Scope) ->

 78 |             (treeCT : CaseTree args) ->

 79 |             (treeRT : CaseTree args) ->

 80 |             (pats : List (vs : Scope ** (Env Term vs, Term vs, Term vs))) ->

 81 |                 -- original checked patterns (LHS/RHS) with the names in

 82 |                 -- the environment. Used for display purposes, for helping

 83 |                 -- find size changes in termination checking, and for

 84 |                 -- generating specialised definitions (so needs to be the

 85 |                 -- full, non-erased, term)

 86 |             Def -- Ordinary function definition

 87 |     ExternDef : (arity : Nat) -> Def

 88 |     ForeignDef : (arity : Nat) ->

 89 |                  List String -> -- supported calling conventions,

 90 |                                 -- e.g "C:printf,libc,stdlib.h", "scheme:display", ...

 91 |                  Def

 92 |     Builtin : {arity : Nat} -> PrimFn arity -> Def

 93 |     DCon : (tag : Int) -> (arity : Nat) ->

 94 |            (newtypeArg : Maybe (Bool, Nat)) ->

 95 |                -- if only constructor, and only one argument is non-Rig0,

 96 |                -- flag it here. The Nat is the unerased argument position.

 97 |                -- The Bool is 'True' if there is no %World token in the

 98 |                -- structure, which means it is safe to completely erase

 99 |                -- when pattern matching (otherwise we still have to ensure

100 |                -- that the value is inspected, to make sure external effects

101 |                -- happen)

102 |            Def -- data constructor

103 |     TCon : (arity : Nat) ->

104 |            (parampos : NatSet) -> -- parameters

105 |            (detpos : NatSet) -> -- determining arguments

106 |            (flags : TypeFlags) -> -- should 'auto' implicits check

107 |            (mutwith : List Name) -> -- TODO morally `Set Name`

108 |            (datacons : Maybe (List Name)) ->

109 |            (detagabbleBy : Maybe NatSet) ->

110 |                     -- argument positions which can be used for

111 |                     -- detagging, if it's possible (to check if it's

112 |                     -- safe to erase)

113 |            Def

114 |     Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point

115 |                               -- (mostly to help display)

116 |            HoleFlags ->

117 |            Def

118 |     BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def

119 |     -- Constraints are integer references into the current map of

120 |     -- constraints in the UnifyState (see Core.UnifyState)

121 |     Guess : (guess : ClosedTerm) ->

122 |             (envbind : Nat) -> -- Number of things in the environment when

123 |                                -- we guessed the term

124 |             (constraints : List Int) -> Def

125 |     ImpBind : Def -- global name temporarily standing for an implicitly bound name

126 |     -- a name standing for a universe level in a Type

127 |     UniverseLevel : Integer -> Def

128 |     -- A delayed elaboration. The elaborators themselves are stored in the

129 |     -- unification state

130 |     Delayed : Def

133 | defNameType : Def -> Maybe NameType

134 | defNameType None = Nothing

135 | defNameType (PMDef {}) = Just Func

136 | defNameType (ExternDef {}) = Just Func

137 | defNameType (ForeignDef {}) = Just Func

138 | defNameType (Builtin {}) = Just Func

139 | defNameType (DCon tag ar _) = Just (DataCon tag ar)

140 | defNameType (TCon ar _ _ _ _ _ _) = Just (TyCon ar)

141 | defNameType (Hole {}) = Just Func

142 | defNameType (BySearch {}) = Nothing

143 | defNameType (Guess {}) = Nothing

144 | defNameType ImpBind = Just Bound

145 | defNameType (UniverseLevel {}) = Nothing

146 | defNameType Delayed = Nothing

150 | Show Def where

151 |   show None = "undefined"

152 |   show (PMDef _ args ct rt pats)

153 |       = unlines [ show args ++ ";"

154 |                 , "Compile time tree: " ++ show ct

155 |                 , "Run time tree: " ++ show rt

156 |                 ]

157 |   show (DCon t a nt)

158 |       = "DataCon " ++ show t ++ " " ++ show a

159 |            ++ maybe "" (\n => " (newtype by " ++ show n ++ ")") nt

160 |   show (TCon a ps ds u ms cons det)

161 |       = "TyCon " ++ show a ++ " params: " ++ show ps ++

162 |         " constructors: " ++ show cons ++

163 |         " mutual with: " ++ show ms ++

164 |         " detaggable by: " ++ show det

165 |   show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"

166 |   show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++

167 |                            " " ++ show cs ++">"

168 |   show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"

169 |   show (Hole _ p) = "Hole" ++ if implbind p then " [impl]" else ""

170 |   show (BySearch c depth def) = "Search in " ++ show def

171 |   show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs

172 |   show (UniverseLevel i) = "Universe level #" ++ show i

173 |   show ImpBind = "Bound name"

174 |   show Delayed = "Delayed"

176 | public export

177 | Constructor' : Type -> Type

178 | Constructor' = AddFC . WithName . WithArity

180 | public export

181 | Constructor : Type

182 | Constructor = Constructor' ClosedTerm

184 | public export

185 | data DataDef : Type where

186 |      MkData : (tycon : Constructor) -> (datacons : List Constructor) ->

187 |               DataDef

189 | public export

190 | data Clause : Type where

191 |      MkClause : {vars : _} ->

192 |                 (env : Env Term vars) ->

193 |                 (lhs : Term vars) -> (rhs : Term vars) -> Clause

194 | %name Clause cl

198 | Show Clause where

199 |   show (MkClause {vars} env lhs rhs)

200 |       = show vars ++ ": " ++ show lhs ++ " = " ++ show rhs

202 | public export

203 | data DefFlag

204 |     = Inline

205 |     | NoInline

206 |     | ||| A definition has been marked as deprecated

207 |       Deprecate

208 |     | Invertible -- assume safe to cancel arguments in unification

209 |     | Overloadable -- allow ad-hoc overloads

210 |     | TCInline -- always inline before totality checking

211 |          -- (in practice, this means it's reduced in 'normaliseHoles')

212 |          -- This means the function gets inlined when calculating the size

213 |          -- change graph, but otherwise not. It's only safe if the function

214 |          -- being inlined is terminating no matter what, and is really a bit

215 |          -- of a hack to make sure interface dictionaries are properly inlined

216 |          -- (otherwise they look potentially non terminating) so use with

217 |          -- care!

218 |     | SetTotal TotalReq

219 |     | BlockedHint -- a hint, but blocked for the moment (so don't use)

220 |     | Macro

221 |     | PartialEval (List (Name, Nat)) -- Partially evaluate on completing defintion.

222 |          -- This means the definition is standing for a specialisation so we

223 |          -- should evaluate the RHS, with reduction limits on the given names,

224 |          -- and ensure the name has made progress in doing so (i.e. has reduced

225 |          -- at least once)

226 |     | AllGuarded -- safe to treat as a constructor for the purposes of

227 |          -- productivity checking. All clauses are guarded by constructors,

228 |          -- and there are no other function applications

229 |     | ConType ConInfo

230 |          -- Is it a special type of constructor, e.g. a nil or cons shaped

231 |          -- thing, that can be compiled specially?

232 |     | Identity Nat

233 |          -- Is it the identity function at runtime?

234 |          -- The nat represents which argument the function evaluates to

235 | %name DefFlag dflag

238 | Eq DefFlag where

239 |     (==) Inline Inline = True

240 |     (==) NoInline NoInline = True

241 |     (==) Deprecate Deprecate = True

242 |     (==) Invertible Invertible = True

243 |     (==) Overloadable Overloadable = True

244 |     (==) TCInline TCInline = True

245 |     (==) (SetTotal x) (SetTotal y) = x == y

246 |     (==) BlockedHint BlockedHint = True

247 |     (==) Macro Macro = True

248 |     (==) (PartialEval x) (PartialEval y) = x == y

249 |     (==) AllGuarded AllGuarded = True

250 |     (==) (ConType x) (ConType y) = x == y

251 |     (==) (Identity x) (Identity y) = x == y

252 |     (==) _ _ = False

255 | Show DefFlag where

256 |   show Inline = "inline"

257 |   show NoInline = "noinline"

258 |   show Deprecate = "deprecate"

259 |   show Invertible = "invertible"

260 |   show Overloadable = "overloadable"

261 |   show TCInline = "tcinline"

262 |   show (SetTotal x) = show x

263 |   show BlockedHint = "blockedhint"

264 |   show Macro = "macro"

265 |   show (PartialEval _) = "partialeval"

266 |   show AllGuarded = "allguarded"

267 |   show (ConType ci) = "contype " ++ show ci

268 |   show (Identity x) = "identity " ++ show x

270 | public export

271 | record SCCall where

272 |      constructor MkSCCall

273 |      fnCall : Name -- Function called

274 |      fnArgs : Matrix SizeChange

275 |         -- relationship to arguments of calling function; argument position

276 |         -- (in the calling function), and how its size changed in the call.

277 |         -- 'Nothing' if it's not related to any of the calling function's

278 |         -- arguments

279 |      fnLoc : FC

282 | Show SCCall where

283 |   show c = show (fnCall c) ++ ": " ++ show (fnArgs c)

286 | Eq SCCall where

287 |   x == y = fnCall x == fnCall y && fnArgs x == fnArgs y

289 | public export

290 | data SchemeMode

291 |         = EvalAll -- evaluate everything

292 |         | BlockExport -- compile 'export' names in other modules as blocked

295 | Eq SchemeMode where

296 |    EvalAll == EvalAll = True

297 |    BlockExport == BlockExport = True

298 |    _ == _ = False

300 | public export

301 | record GlobalDef where

302 |   constructor MkGlobalDef

303 |   location : FC

304 |   fullname : Name -- original unresolved name

305 |   type : ClosedTerm

306 |   eraseArgs : NatSet -- which argument positions to erase at runtime

307 |   safeErase : NatSet -- which argument positions are safe to assume

308 |                        -- erasable without 'dotting', because their types

309 |                        -- are collapsible relative to non-erased arguments

310 |   specArgs : NatSet -- arguments to specialise by

311 |   inferrable : NatSet -- arguments which can be inferred from elsewhere in the type

312 |   multiplicity : RigCount

313 |   localVars : Scope -- environment name is defined in

314 |   visibility : WithDefault Visibility Private

315 |   totality : Totality

316 |   isEscapeHatch : Bool

317 |   flags : List DefFlag

318 |   refersToM : Maybe (NameMap Bool)

319 |   refersToRuntimeM : Maybe (NameMap Bool)

320 |   invertible : Bool -- for an ordinary definition, is it invertible in unification

321 |   noCycles : Bool -- for metavariables, whether they can be cyclic (this

322 |                   -- would only be allowed when using a metavariable as a

323 |                   -- placeholder for a yet to be elaborated arguments, but

324 |                   -- not for implicits because that'd indicate failing the

325 |                   -- occurs check)

326 |   linearChecked : Bool -- Flag whether we've already checked its linearity

327 |   definition : Def

328 |   compexpr : Maybe CDef

329 |   namedcompexpr : Maybe NamedDef

330 |   sizeChange : List SCCall

331 |   schemeExpr : Maybe (SchemeMode, SchemeObj Write)

334 | getDefNameType : GlobalDef -> NameType

335 | getDefNameType = fromMaybe Func . defNameType . definition

338 | gDefKindedName : GlobalDef -> KindedName

339 | gDefKindedName def

340 |   = let nm = fullname def in

341 |     MkKindedName (defNameType $ definition def) nm nm

344 | refersTo : GlobalDef -> NameMap Bool

345 | refersTo def = maybe empty id (refersToM def)

348 | refersToRuntime : GlobalDef -> NameMap Bool

349 | refersToRuntime def = maybe empty id (refersToRuntimeM def)

352 | findSetTotal : List DefFlag -> Maybe TotalReq

353 | findSetTotal [] = Nothing

354 | findSetTotal (SetTotal t :: _) = Just t

355 | findSetTotal (_ :: xs) = findSetTotal xs

359 | data Arr : Type where

363 | public export

364 | data ContextEntry : Type where

365 |      Coded : Namespace -> -- namespace for decoding into, with restoreNS

366 |              Binary -> ContextEntry

367 |      Decoded : GlobalDef -> ContextEntry

369 | public export

370 | data PossibleName : Type where

371 |      Direct : Name -> Int -> PossibleName -- full name and resolved name id

372 |      Alias : Name -> -- aliased name (from "import as")

373 |              Name -> Int -> -- real full name and resolved name, as above

374 |              PossibleName

376 | public export

377 | data UConstraint : Type where

378 |      ULE : Name -> Name -> UConstraint

379 |      ULT : Name -> Name -> UConstraint

382 | Eq UConstraint where

383 |   ULE x y == ULE x' y' = x == x' && y == y'

384 |   ULT x y == ULT x' y' = x == x' && y == y'

385 |   _ == _ = False

388 | Ord UConstraint where

389 |   compare (ULE {}) (ULT {}) = LT

390 |   compare (ULT {}) (ULE {}) = GT

391 |   compare (ULE x y) (ULE x' y')

392 |       = case compare x x' of

393 |              EQ => compare y y'

394 |              t => t

395 |   compare (ULT x y) (ULT x' y')

396 |       = case compare x x' of

397 |              EQ => compare y y'

398 |              t => t

403 | public export

404 | record Context where

405 |     constructor MkContext

406 |     firstEntry : Int -- First entry in the current source file

407 |     nextEntry : Int

408 |     -- Map from full name to its position in the context

409 |     resolvedAs : NameMap Int

410 |     -- Map from usernames to all the possible names in all namespaces

411 |     possibles : UserNameMap (List PossibleName)

412 |     -- Reference to the actual content, indexed by Int

413 |     content : Ref Arr (IOArray ContextEntry)

414 |     -- Branching depth, in a backtracking elaborator. 0 is top level; at lower

415 |     -- levels we need to stage updates rather than add directly to the

416 |     -- 'content' store

417 |     branchDepth : Nat

418 |     -- Things which we're going to add, if this branch succeeds

419 |     staging : IntMap ContextEntry

421 |     -- Namespaces which are visible (i.e. have been imported)

422 |     -- This only matters during evaluation and type checking, to control

423 |     -- access in a program - in all other cases, we'll assume everything is

424 |     -- visible

425 |     visibleNS : List Namespace

426 |     allPublic : Bool -- treat everything as public. This is intended

427 |                      -- for checking partially evaluated definitions

428 |                      -- or for use outside of the main compilation

429 |                      -- process (e.g. when implementing interactive

430 |                      -- features such as case splitting).

431 |     inlineOnly : Bool -- only return things with the 'alwaysReduce' flag

432 |     hidden : NameMap () -- Never return these

433 |     uconstraints : List UConstraint

435 | %name Context gam