
  0 | module Core.TT.Term.Subst
  1 | 
  2 | import Core.Name.Scoped
  3 | 
  4 | import Core.TT.Binder
  5 | import Core.TT.Subst
  6 | import Core.TT.Term
  7 | import Core.TT.Var
  8 | 
  9 | import Libraries.Data.List.SizeOf
 10 | 
 11 | %default total
 12 | 
 13 | public export
 14 | SubstEnv : Scope -> Scoped
 15 | SubstEnv = Subst Term
 16 | 
 17 | substTerm : Substitutable Term Term
 18 | substTerms : Substitutable Term (List . Term)
 19 | substBinder : Substitutable Term (Binder . Term)
 20 | 
 21 | substTerm outer dropped env (Local fc r _ prf)
 22 |     = find (\ (MkVar p) => Local fc r _ p) outer dropped (MkVar prf) env
 23 | substTerm outer dropped env (Ref fc x name) = Ref fc x name
 24 | substTerm outer dropped env (Meta fc n i xs)
 25 |     = Meta fc n i (substTerms outer dropped env xs)
 26 | substTerm outer dropped env (Bind fc x b scope)
 27 |     = Bind fc x (substBinder outer dropped env b)
 28 |                 (substTerm (suc outer) dropped env scope)
 29 | substTerm outer dropped env (App fc fn arg)
 30 |     = App fc (substTerm outer dropped env fn) (substTerm outer dropped env arg)
 31 | substTerm outer dropped env (As fc s as pat)
 32 |     = As fc s (substTerm outer dropped env as) (substTerm outer dropped env pat)
 33 | substTerm outer dropped env (TDelayed fc x y) = TDelayed fc x (substTerm outer dropped env y)
 34 | substTerm outer dropped env (TDelay fc x t y)
 35 |     = TDelay fc x (substTerm outer dropped env t) (substTerm outer dropped env y)
 36 | substTerm outer dropped env (TForce fc r x) = TForce fc r (substTerm outer dropped env x)
 37 | substTerm outer dropped env (PrimVal fc c) = PrimVal fc c
 38 | substTerm outer dropped env (Erased fc Impossible) = Erased fc Impossible
 39 | substTerm outer dropped env (Erased fc Placeholder) = Erased fc Placeholder
 40 | substTerm outer dropped env (Erased fc (Dotted t)) = Erased fc (Dotted (substTerm outer dropped env t))
 41 | substTerm outer dropped env (TType fc u) = TType fc u
 42 | 
 43 | substTerms outer dropped env xs
 44 |   = assert_total $ map (substTerm outer dropped env) xs
 45 | 
 46 | substBinder outer dropped env b
 47 |   = assert_total $ map (substTerm outer dropped env) b
 48 | 
 49 | export
 50 | substs : SizeOf dropped -> SubstEnv dropped vars -> Term (dropped ++ vars) -> Term vars
 51 | substs dropped env tm = substTerm zero dropped env tm
 52 | 
 53 | export
 54 | subst : Term vars -> Term (Scope.bind vars x) -> Term vars
 55 | subst val tm = substs (suc zero) [val] tm
 56 |