0 | module Core.Env
  1 |
  2 | import Core.TT
  3 | import Data.List
  4 |
  5 | import Libraries.Data.List.SizeOf
  6 |
  7 | import Libraries.Data.VarSet
  8 |
  9 | import Libraries.Data.SnocList.SizeOf
 10 |
 11 | %default total
 12 |
 13 | -- Environment containing types and values of local variables
 14 | public export
 15 | data Env : (tm : Scoped) -> Scope -> Type where
 16 |      Nil : Env tm Scope.empty
 17 |      (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 18 |
 19 | %name Env rho
 20 |
 21 | public export
 22 | empty : Env tm Scope.empty
 23 | empty = []
 24 |
 25 | export
 26 | extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 27 | extend x = (::) {x}
 28 |
 29 | export
 30 | (++) : {ns : _} -> Env Term ns -> Env Term vars -> Env Term (ns ++ vars)
 31 | (++) (b :: bs) e = extend _ (map embed b) (bs ++ e)
 32 | (++) [] e = e
 33 |
 34 | export
 35 | length : Env tm xs -> Nat
 36 | length [] = 0
 37 | length (_ :: xs) = S (length xs)
 38 |
 39 | export
 40 | lengthNoLet : Env tm xs -> Nat
 41 | lengthNoLet [] = 0
 42 | lengthNoLet (Let _ _ _ _ :: xs) = lengthNoLet xs
 43 | lengthNoLet (_ :: xs) = S (lengthNoLet xs)
 44 |
 45 | export
 46 | lengthExplicitPi : Env tm xs -> Nat
 47 | lengthExplicitPi [] = 0
 48 | lengthExplicitPi (Pi _ _ Explicit _ :: rho) = S (lengthExplicitPi rho)
 49 | lengthExplicitPi (_ :: rho) = lengthExplicitPi rho
 50 |
 51 | export
 52 | namesNoLet : {xs : _} -> Env tm xs -> List Name
 53 | namesNoLet [] = []
 54 | namesNoLet (Let _ _ _ _ :: xs) = namesNoLet xs
 55 | namesNoLet {xs = x :: _} (_ :: env) = x :: namesNoLet env
 56 |
 57 | export
 58 | eraseLinear : Env tm vs -> Env tm vs
 59 | eraseLinear [] = Env.empty
 60 | eraseLinear (b :: bs)
 61 |     = if isLinear (multiplicity b)
 62 |          then setMultiplicity b erased :: eraseLinear bs
 63 |          else b :: eraseLinear bs
 64 |
 65 | export
 66 | getErased : {0 vs : _} -> Env tm vs -> List (Var vs)
 67 | getErased env = go env [<] where
 68 |
 69 |   go : Env tm vars -> SizeOf seen -> List (Var (seen <>> vars))
 70 |   go [] p = []
 71 |   go (b :: bs) p
 72 |     = if isErased (multiplicity b)
 73 |          then mkVarChiply p :: go bs (p :< _)
 74 |          else go bs (p :< _)
 75 |
 76 | public export
 77 | data IsDefined : Name -> Scope -> Type where
 78 |   MkIsDefined : {idx : Nat} -> RigCount -> (0 p : IsVar n idx vars) ->
 79 |                 IsDefined n vars
 80 |
 81 | export
 82 | defined : {vars : _} ->
 83 |           (n : Name) -> Env Term vars ->
 84 |           Maybe (IsDefined n vars)
 85 | defined n [] = Nothing
 86 | defined {vars = x :: xs} n (b :: env)
 87 |     = case nameEq n x of
 88 |            Nothing => do MkIsDefined rig prf <- defined n env
 89 |                          pure (MkIsDefined rig (Later prf))
 90 |            Just Refl => Just (MkIsDefined (multiplicity b) First)
 91 |
 92 | -- Bind additional pattern variables in an LHS, when checking an LHS in an
 93 | -- outer environment
 94 | export
 95 | bindEnv : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
 96 | bindEnv loc [] tm = tm
 97 | bindEnv loc (b :: env) tm
 98 |     = bindEnv loc env (Bind loc _ (PVar (binderLoc b)
 99 |                                         (multiplicity b)
100 |                                         Explicit
101 |                                         (binderType b)) tm)
102 |
103 | revOnto : (xs, vs : List a) -> reverseOnto xs vs = reverse vs ++ xs
104 | revOnto xs [] = Refl
105 | revOnto xs (v :: vs)
106 |     = rewrite revOnto (v :: xs) vs in
107 |         rewrite appendAssociative (reverse vs) [v] xs in
108 |           rewrite revOnto [v] vs in Refl
109 |
110 |
111 | -- Weaken by all the names at once at the end, to save multiple traversals
112 | -- in big environments
113 | -- Also reversing the names at the end saves significant time over concatenating
114 | -- when environments get fairly big.
115 | getBinderUnder : Weaken tm =>
116 |                  {vars : _} -> {idx : Nat} ->
117 |                  (ns : Scope) ->
118 |                  (0 p : IsVar x idx vars) -> Env tm vars ->
119 |                  Binder (tm (reverseOnto vars ns))
120 | getBinderUnder {idx = Z} {vars = v :: vs} ns First (b :: env)
121 |     = rewrite revOnto vs (v :: ns) in map (weakenNs (reverse (mkSizeOf (v :: ns)))) b
122 | getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)
123 |     = getBinderUnder (v :: ns) lp env
124 |
125 | export
126 | getBinder : Weaken tm =>
127 |             {vars : _} -> {idx : Nat} ->
128 |             (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm vars)
129 | getBinder el env = getBinderUnder Scope.empty el env
130 |
131 | -- For getBinderLoc, we are not reusing getBinder because there is no need to
132 | -- needlessly weaken stuff;
133 | export
134 | getBinderLoc : {vars : _} -> {idx : Nat} -> (0 p : IsVar x idx vars) -> Env tm vars -> FC
135 | getBinderLoc {idx = Z}   First     (b :: _)   = binderLoc b
136 | getBinderLoc {idx = S k} (Later p) (_ :: env) = getBinderLoc p env
137 |
138 | -- Make a type which abstracts over an environment
139 | -- Don't include 'let' bindings, since they have a concrete value and
140 | -- shouldn't be generalised
141 | export
142 | abstractEnvType : {vars : _} ->
143 |                   FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
144 | abstractEnvType fc [] tm = tm
145 | abstractEnvType fc (Let fc' c val ty :: env) tm
146 |     = abstractEnvType fc env (Bind fc _ (Let fc' c val ty) tm)
147 | abstractEnvType fc (Pi fc' c e ty :: env) tm
148 |     = abstractEnvType fc env (Bind fc _ (Pi fc' c e ty) tm)
149 | abstractEnvType fc (b :: env) tm
150 |     = let bnd = Pi (binderLoc b) (multiplicity b) Explicit (binderType b)
151 |        in abstractEnvType fc env (Bind fc _ bnd tm)
152 |
153 | -- As above, for the corresponding term
154 | export
155 | abstractEnv : {vars : _} ->
156 |               FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
157 | abstractEnv fc [] tm = tm
158 | abstractEnv fc (Let fc' c val ty :: env) tm
159 |     = abstractEnv fc env (Bind fc _ (Let fc' c val ty) tm)
160 | abstractEnv fc (b :: env) tm
161 |     = let bnd = Lam (binderLoc b) (multiplicity b) Explicit (binderType b)
162 |       in abstractEnv fc env (Bind fc _ bnd tm)
163 |
164 | -- As above, but abstract over all binders including lets
165 | export
166 | abstractFullEnvType : {vars : _} ->
167 |                       FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
168 | abstractFullEnvType fc [] tm = tm
169 | abstractFullEnvType fc (Pi fc' c e ty :: env) tm
170 |     = abstractFullEnvType fc env (Bind fc _ (Pi fc' c e ty) tm)
171 | abstractFullEnvType fc (b :: env) tm
172 |     = let bnd = Pi fc (multiplicity b) Explicit (binderType b)
173 |       in abstractFullEnvType fc env (Bind fc _ bnd tm)
174 |
175 | export
176 | mkExplicit : Env Term vs -> Env Term vs
177 | mkExplicit [] = Env.empty
178 | mkExplicit (Pi fc c _ ty :: env) = Pi fc c Explicit ty :: mkExplicit env
179 | mkExplicit (b :: env) = b :: mkExplicit env
180 |
181 | export
182 | letToLam : Env Term vars -> Env Term vars
183 | letToLam [] = []
184 | letToLam (Let fc c val ty :: env) = Lam fc c Explicit ty :: letToLam env
185 | letToLam (b :: env) = b :: letToLam env
186 |
187 | mutual
188 |   findUsed : {vars : _} ->
189 |              Env Term vars -> VarSet vars -> Term vars -> VarSet vars
190 |   findUsed env used (Local fc r idx p)
191 |       = let v := MkVar p in
192 |         if v `elem` used
193 |            then used
194 |            else assert_total (findUsedInBinder env (VarSet.insert v used)
195 |                                                (getBinder p env))
196 |   findUsed env used (Meta _ _ _ args)
197 |       = findUsedArgs env used args
198 |     where
199 |       findUsedArgs : Env Term vars -> VarSet vars -> List (Term vars) -> VarSet vars
200 |       findUsedArgs env u [] = u
201 |       findUsedArgs env u (a :: as)
202 |           = findUsedArgs env (findUsed env u a) as
203 |   findUsed env used (Bind fc x b tm)
204 |       = assert_total $
205 |           VarSet.dropFirst (findUsed (b :: env)
206 |                           (weaken {tm = VarSet} (findUsedInBinder env used b))
207 |                           tm)
208 |   findUsed env used (App fc fn arg)
209 |       = findUsed env (findUsed env used fn) arg
210 |   findUsed env used (As fc s a p)
211 |       = findUsed env (findUsed env used a) p
212 |   findUsed env used (TDelayed fc r tm)
213 |       = findUsed env used tm
214 |   findUsed env used (TDelay fc r ty tm)
215 |       = findUsed env (findUsed env used ty) tm
216 |   findUsed env used (TForce fc r tm)
217 |       = findUsed env used tm
218 |   findUsed env used (Erased fc (Dotted tm))
219 |       = findUsed env used tm
220 |   findUsed env used _ = used
221 |
222 |   findUsedInBinder : {vars : _} ->
223 |                      Env Term vars -> VarSet vars ->
224 |                      Binder (Term vars) -> VarSet vars
225 |   findUsedInBinder env used (Let _ _ val ty)
226 |     = findUsed env (findUsed env used val) ty
227 |   findUsedInBinder env used (PLet _ _ val ty)
228 |     = findUsed env (findUsed env used val) ty
229 |   findUsedInBinder env used b = findUsed env used (binderType b)
230 |
231 | export
232 | findUsedLocs : {vars : _} ->
233 |                Env Term vars -> Term vars -> VarSet vars
234 | findUsedLocs env tm = findUsed env VarSet.empty tm
235 |
236 | mkShrinkSub : {n : _} ->
237 |               (vars : _) -> VarSet (n :: vars) ->
238 |               (newvars ** Thin newvars (n :: vars))
239 | mkShrinkSub [] els
240 |     = if first `VarSet.elem` els
241 |          then (_ ** Keep Refl)
242 |          else (_ ** Drop Refl)
243 | mkShrinkSub (x :: xs) els
244 |     = let (_ ** subRest) = mkShrinkSub xs (VarSet.dropFirst els) in
245 |       if first `VarSet.elem` els
246 |         then (_ ** Keep subRest)
247 |         else (_ ** Drop subRest)
248 |
249 | mkShrink : {vars : _} ->
250 |            VarSet vars ->
251 |            (newvars ** Thin newvars vars)
252 | mkShrink {vars = []} xs = (_ ** Refl)
253 | mkShrink {vars = v :: vs} xs = mkShrinkSub _ xs
254 |
255 | -- Find the smallest subset of the environment which is needed to type check
256 | -- the given term
257 | export
258 | findSubEnv : {vars : _} ->
259 |              Env Term vars -> Term vars ->
260 |              (vars' : Scope ** Thin vars' vars)
261 | findSubEnv env tm = mkShrink (findUsedLocs env tm)
262 |
263 | export
264 | shrinkEnv : Env Term vars -> Thin newvars vars -> Maybe (Env Term newvars)
265 | shrinkEnv env Refl = Just env
266 | shrinkEnv (b :: env) (Drop p) = shrinkEnv env p
267 | shrinkEnv (b :: env) (Keep p)
268 |     = do env' <- shrinkEnv env p
269 |          b' <- assert_total (shrinkBinder b p)
270 |          pure (b' :: env')
271 |
272 | export
273 | mkEnvOnto : FC -> (xs : List Name) -> Env Term ys -> Env Term (xs ++ ys)
274 | mkEnvOnto fc [] vs = vs
275 | mkEnvOnto fc (n :: ns) vs
276 |    = PVar fc top Explicit (Erased fc Placeholder)
277 |    :: mkEnvOnto fc ns vs
278 |
279 | -- Make a dummy environment, if we genuinely don't care about the values
280 | -- and types of the contents.
281 | -- We use this when building and comparing case trees.
282 | export
283 | mkEnv : FC -> (vs : Scope) -> Env Term vs
284 | mkEnv fc [] = []
285 | mkEnv fc (n :: ns) = PVar fc top Explicit (Erased fc Placeholder) :: mkEnv fc ns
286 |
287 | -- Update an environment so that all names are guaranteed unique. In the
288 | -- case of a clash, the most recently bound is left unchanged.
289 | --
290 | -- TODO replace list of `used` names with a proper set
291 | export
292 | uniqifyEnv : {vars : _} ->
293 |              Env Term vars ->
294 |              (vars' ** (Env Term vars', CompatibleVars vars vars'))
295 | uniqifyEnv env = uenv [] env
296 |   where
297 |     next : Name -> Name
298 |     next (MN n i) = MN n (i + 1)
299 |     next (UN n) = MN (displayUserName n) 0
300 |     next (NS ns n) = NS ns (next n)
301 |     next n = MN (show n) 0
302 |
303 |     uniqueLocal : List Name -> Name -> Name
304 |     uniqueLocal vs n
305 |        = if n `elem` vs
306 |                  -- we'll find a new name eventualy since the list of names
307 |                  -- is empty, and next generates something new. But next has
308 |                  -- to be correct... an exercise for someone: this could
309 |                  -- probebly be done without an assertion by making a stream of
310 |                  -- possible names...
311 |             then assert_total (uniqueLocal vs (next n))
312 |             else n
313 |
314 |     uenv : {vars : _} ->
315 |            List Name -> Env Term vars ->
316 |            (vars' ** (Env Term vars', CompatibleVars vars vars'))
317 |     uenv used [] = ([] ** ([], Pre))
318 |     uenv used {vars = v :: vs} (b :: bs)
319 |         = if v `elem` used
320 |              then let v' = uniqueLocal used v
321 |                       (vs' ** (env', compat)) = uenv (v' :: used) bs
322 |                       b' = map (compatNs compat) b in
323 |                   (v' :: vs' ** (b' :: env', Ext compat))
324 |              else let (vs' ** (env', compat)) = uenv (v :: used) bs
325 |                       b' = map (compatNs compat) b in
326 |                   (v :: vs' ** (b' :: env', Ext compat))
327 |
328 | export
329 | allVars : {0 vars : _} -> Env Term vars -> List (Var vars)
330 | allVars env = go env [<] where
331 |
332 |   go :  {0 vars : _} -> Env Term vars ->
333 |         {0 seen : SnocList Name} -> SizeOf seen ->
334 |         List (Var (seen <>> vars))
335 |   go [] _ = []
336 |   go (v :: vs) p = mkVarChiply p :: go vs (p :< _)
337 |
338 |
339 | export
340 | allVarsNoLet : {0 vars : _} -> Env Term vars -> List (Var vars)
341 | allVarsNoLet env = go env [<] where
342 |
343 |   go :  {0 vars : _} -> Env Term vars ->
344 |         {0 seen : SnocList Name} -> SizeOf seen ->
345 |         List (Var (seen <>> vars))
346 |   go [] _ = []
347 |   go (Let _ _ _ _ :: vs) p = go vs (p :< _)
348 |   go (v :: vs) p = mkVarChiply p :: go vs (p :< _)
349 |
350 | export
351 | close : FC -> String -> Env Term vars -> Term vars -> ClosedTerm
352 | close fc nm env tm
353 |   = let (s, env) = mkSubstEnv 0 env in
354 |     substs s env (rewrite appendNilRightNeutral vars in tm)
355 |
356 |   where
357 |     mkSubstEnv : Int -> Env Term vs -> (SizeOf vs, SubstEnv vs Scope.empty)
358 |     mkSubstEnv i [] = (zero, Subst.empty)
359 |     mkSubstEnv i (v :: vs)
360 |        = let (s, env) = mkSubstEnv (i + 1) vs in
361 |          (suc s, Ref fc Bound (MN nm i) :: env)
362 |