
  0 | module Core.TT.Subst
  1 | 
  2 | import Core.Name.Scoped
  3 | import Core.TT.Var
  4 | 
  5 | import Libraries.Data.List.SizeOf
  6 | 
  7 | %default total
  8 | 
  9 | -- TODO replace by pointwise lifting: `Subst tm ds vars = All (\_. tm vars) ds`
 10 | public export
 11 | data Subst : Scoped -> Scope -> Scoped where
 12 |   Nil : Subst tm Scope.empty vars
 13 |   (::) : tm vars -> Subst tm ds vars -> Subst tm (d :: ds) vars
 14 | 
 15 | public export
 16 | empty : Subst tm Scope.empty vars
 17 | empty = []
 18 | 
 19 | 
 20 | namespace Var
 21 | 
 22 |   export
 23 |   index : Subst tm ds vars -> Var ds -> tm vars
 24 |   index [] (MkVar p) impossible
 25 |   index (t :: _) (MkVar First) = t
 26 |   index (_ :: ts) (MkVar (Later p)) = index ts (MkVar p)
 27 | 
 28 | -- TODO revisit order of `dropped` and `Subst`
 29 | export
 30 | findDrop :
 31 |   (Var vars -> tm vars) ->
 32 |   SizeOf dropped ->
 33 |   Var (dropped ++ vars) ->
 34 |   Subst tm dropped vars ->
 35 |   tm vars
 36 | findDrop k s var sub = case locateVar s var of
 37 |   Left var => index sub var
 38 |   Right var => k var
 39 | 
 40 | export
 41 | find : Weaken tm =>
 42 |        (forall vars. Var vars -> tm vars) ->
 43 |        SizeOf outer -> SizeOf dropped ->
 44 |        Var (outer ++ (dropped ++ vars)) ->
 45 |        Subst tm dropped vars ->
 46 |        tm (outer ++ vars)
 47 | find k outer dropped var sub = case locateVar outer var of
 48 |   Left var => k (embed var)
 49 |   Right var => weakenNs outer (findDrop k dropped var sub)
 50 | 
 51 | -- TODO rename `outer`
 52 | public export
 53 | 0 Substitutable : Scoped -> Scoped -> Type
 54 | Substitutable val tm
 55 |   = {0 outer, dropped, vars : Scope} ->
 56 |     SizeOf outer ->
 57 |     SizeOf dropped ->
 58 |     Subst val dropped vars ->
 59 |     tm (outer ++ (dropped ++ vars)) ->
 60 |     tm (outer ++ vars)
 61 |