module Core.Env import Core.TT -- Environment containing types and values of local variablespublic exportdata Env : (tm : List Name -> Type) -> List Name -> Type where     Nil : Env tm []     (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars) exportextend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)extend x = (::) {x} exportlength : Env tm xs -> Natlength [] = 0length (_ :: xs) = S (length xs) exportlengthNoLet : Env tm xs -> NatlengthNoLet [] = 0lengthNoLet (Let _ _ _ :: xs) = lengthNoLet xslengthNoLet (_ :: xs) = S (lengthNoLet xs) exportnamesNoLet : {xs : _} -> Env tm xs -> List NamenamesNoLet [] = []namesNoLet (Let _ _ _ :: xs) = namesNoLet xsnamesNoLet {xs = x :: _} (_ :: env) = x :: namesNoLet env public exportdata IsDefined : Name -> List Name -> Type where  MkIsDefined : {idx : Nat} -> RigCount -> .(IsVar n idx vars) ->                IsDefined n vars exportdefined : {vars : _} ->          (n : Name) -> Env Term vars ->          Maybe (IsDefined n vars)defined n [] = Nothingdefined {vars = x :: xs} n (b :: env)    = case nameEq n x of           Nothing => do MkIsDefined rig prf <- defined n env                         pure (MkIsDefined rig (Later prf))           Just Refl => Just (MkIsDefined (multiplicity b) First) exportbindEnv : FC -> Env Term vars -> (tm : Term vars) -> ClosedTermbindEnv loc [] tm = tmbindEnv loc (b :: env) tm    = bindEnv loc env (Bind loc _ b tm) revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xsrevOnto xs [] = ReflrevOnto xs (v :: vs)    = rewrite revOnto (v :: xs) vs in        rewrite appendAssociative (reverse vs) [v] xs in				  rewrite revOnto [v] vs in Refl revNs : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)revNs [] ns = rewrite appendNilRightNeutral (reverse ns) in ReflrevNs (v :: vs) ns    = rewrite revOnto [v] vs in        rewrite revOnto [v] (vs ++ ns) in          rewrite sym (revNs vs ns) in            rewrite appendAssociative (reverse ns) (reverse vs) [v] in              Refl -- Weaken by all the names at once at the end, to save multiple traversals-- in big environments-- Also reversing the names at the end saves significant time over concatenating-- when environments get fairly big.getBinderUnder : Weaken tm =>                 {idx : Nat} ->                 (ns : List Name) ->                 .(IsVar x idx vars) -> Env tm vars ->                 Binder (tm (reverseOnto vars ns))getBinderUnder {idx = Z} {vars = v :: vs} ns First (b :: env)    = rewrite revOnto vs (v :: ns) in map (weakenNs (reverse (v :: ns))) bgetBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)    = getBinderUnder (v :: ns) lp env exportgetBinder : Weaken tm =>            {idx : Nat} ->            .(IsVar x idx vars) -> Env tm vars -> Binder (tm vars)getBinder el env = getBinderUnder [] el env -- Make a type which abstracts over an environment-- Don't include 'let' bindings, since they have a concrete value and-- shouldn't be generalisedexportabstractEnvType : FC -> Env Term vars -> (tm : Term vars) -> ClosedTermabstractEnvType fc [] tm = tmabstractEnvType fc (Let c val ty :: env) tm    = abstractEnvType fc env (Bind fc _ (Let c val ty) tm)abstractEnvType fc (Pi c e ty :: env) tm    = abstractEnvType fc env (Bind fc _ (Pi c e ty) tm)abstractEnvType fc (b :: env) tm    = abstractEnvType fc env (Bind fc _						(Pi (multiplicity b) Explicit (binderType b)) tm) -- As above, for the corresponding termexportabstractEnv : FC -> Env Term vars -> (tm : Term vars) -> ClosedTermabstractEnv fc [] tm = tmabstractEnv fc (Let c val ty :: env) tm    = abstractEnv fc env (Bind fc _ (Let c val ty) tm)abstractEnv fc (b :: env) tm    = abstractEnv fc env (Bind fc _						(Lam (multiplicity b) Explicit (binderType b)) tm) -- As above, but abstract over all binders including letsexportabstractFullEnvType : FC -> Env Term vars -> (tm : Term vars) -> ClosedTermabstractFullEnvType fc [] tm = tmabstractFullEnvType fc (b :: env) tm    = abstractFullEnvType fc env (Bind fc _						(Pi (multiplicity b) Explicit (binderType b)) tm) exportletToLam : Env Term vars -> Env Term varsletToLam [] = []letToLam (Let c val ty :: env) = Lam c Explicit ty :: letToLam envletToLam (b :: env) = b :: letToLam env mutual	-- Quicker, if less safe, to store variables as a Nat, for quick comparison  findUsed : Env Term vars -> List Nat -> Term vars -> List Nat  findUsed env used (Local fc r idx p)      = if elemBy eqNat idx used           then used           else assert_total (findUsedInBinder env (idx :: used)                                               (getBinder p env))    where      eqNat : Nat -> Nat -> Bool      eqNat i j = toIntegerNat i == toIntegerNat j  findUsed env used (Meta _ _ _ args)      = findUsedArgs env used args    where      findUsedArgs : Env Term vars -> List Nat -> List (Term vars) -> List Nat      findUsedArgs env u [] = u      findUsedArgs env u (a :: as)          = findUsedArgs env (findUsed env u a) as  findUsed env used (Bind fc x b tm)      = assert_total $          dropS (findUsed (b :: env)                          (map S (findUsedInBinder env used b))                          tm)    where      dropS : List Nat -> List Nat      dropS [] = []      dropS (Z :: xs) = dropS xs      dropS (S p :: xs) = p :: dropS xs  findUsed env used (App fc fn arg)      = findUsed env (findUsed env used fn) arg  findUsed env used (As fc s a p)      = findUsed env (findUsed env used a) p  findUsed env used (TDelayed fc r tm)      = findUsed env used tm  findUsed env used (TDelay fc r ty tm)      = findUsed env (findUsed env used ty) tm  findUsed env used (TForce fc r tm)      = findUsed env used tm  findUsed env used _ = used   findUsedInBinder : Env Term vars -> List Nat ->										 Binder (Term vars) -> List Nat  findUsedInBinder env used (Let _ val ty)    = findUsed env (findUsed env used val) ty  findUsedInBinder env used (PLet _ val ty)    = findUsed env (findUsed env used val) ty  findUsedInBinder env used b = findUsed env used (binderType b) toVar : (vars : List Name) -> Nat -> Maybe (Var vars)toVar (v :: vs) Z = Just (MkVar First)toVar (v :: vs) (S k)   = do MkVar prf <- toVar vs k        Just (MkVar (Later prf))toVar _ _ = Nothing exportfindUsedLocs : Env Term vars -> Term vars -> List (Var vars)findUsedLocs env tm    = mapMaybe (toVar _) (findUsed env [] tm) isUsed : Nat -> List (Var vars) -> BoolisUsed n [] = FalseisUsed n (v :: vs) = n == varIdx v || isUsed n vs mkShrinkSub : (vars : _) -> List (Var (n :: vars)) ->              (newvars ** SubVars newvars (n :: vars))mkShrinkSub [] els    = if isUsed 0 els         then (_ ** KeepCons SubRefl)         else (_ ** DropCons SubRefl)mkShrinkSub (x :: xs) els    = let (_ ** subRest) = mkShrinkSub xs (dropFirst els) in					if isUsed 0 els				     then (_ ** KeepCons subRest)				     else (_ ** DropCons subRest) mkShrink : List (Var vars) ->           (newvars ** SubVars newvars vars)mkShrink {vars = []} xs = (_ ** SubRefl)mkShrink {vars = v :: vs} xs = mkShrinkSub _ xs -- Find the smallest subset of the environment which is needed to type check-- the given termexportfindSubEnv : Env Term vars -> Term vars ->						 (vars' : List Name ** SubVars vars' vars)findSubEnv env tm = mkShrink (findUsedLocs env tm) exportshrinkEnv : Env Term vars -> SubVars newvars vars -> Maybe (Env Term newvars)shrinkEnv env SubRefl = Just envshrinkEnv (b :: env) (DropCons p) = shrinkEnv env pshrinkEnv (b :: env) (KeepCons p)    = do env' <- shrinkEnv env p         b' <- shrinkBinder b p         pure (b' :: env')