quox/lib/Quox/Syntax/Subst.idr

163 lines
4.3 KiB
Idris
Raw Normal View History

2021-07-20 16:05:19 -04:00
module Quox.Syntax.Subst
2021-09-09 17:53:00 -04:00
import public Quox.Syntax.Shift
2021-07-20 16:05:19 -04:00
import Quox.Syntax.Var
import Quox.Name
2023-01-22 21:22:50 -05:00
import Data.Nat
2021-07-20 16:05:19 -04:00
import Data.List
2023-03-26 10:09:47 -04:00
import Data.SnocVect
import Derive.Prelude
2021-07-20 16:05:19 -04:00
%default total
%language ElabReflection
2021-07-20 16:05:19 -04:00
public export
data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
Shift : Shift from to -> Subst env from to
(:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
%name Subst th, ph, ps
infixr 7 !:::
||| in case the automatic laziness insertion gets confused
public export
(!:::) : env to -> Subst env from to -> Subst env (S from) to
t !::: ts = t ::: ts
2021-07-20 16:05:19 -04:00
private
Repr : (Nat -> Type) -> Nat -> Type
Repr f to = (List (f to), Nat)
private
repr : Subst f from to -> Repr f to
repr (Shift by) = ([], by.nat)
repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
export Eq (f to) => Eq (Subst f from to) where (==) = (==) `on` repr
export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
export Show (f to) => Show (Subst f from to) where show = show . repr
2021-07-20 16:05:19 -04:00
infixl 8 //
public export
interface FromVar term => CanSubstSelf term where
(//) : term from -> Lazy (Subst term from to) -> term to
2021-07-20 16:05:19 -04:00
public export
2023-05-01 21:06:25 -04:00
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
getLoc (Shift by) i loc = fromVarLoc (shift by i) loc
getLoc (t ::: th) VZ _ = t
getLoc (t ::: th) (VS i) loc = getLoc th i loc
2021-07-20 16:05:19 -04:00
public export
CanSubstSelf Var where
2021-09-03 11:10:50 -04:00
i // Shift by = shift by i
2021-07-20 16:05:19 -04:00
VZ // (t ::: th) = t
VS i // (t ::: th) = i // th
public export %inline
shift : (by : Nat) -> Subst env from (by + from)
shift by = Shift $ fromNat by
public export %inline
shift0 : (by : Nat) -> Subst env 0 by
shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by
2021-07-20 16:05:19 -04:00
public export
(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
2021-09-25 14:13:51 -04:00
Shift by . Shift bz = Shift $ by . bz
2021-07-20 16:05:19 -04:00
Shift SZ . ph = ph
Shift (SS by) . (t ::: th) = Shift by . th
(t ::: th) . ph = (t // ph) ::: (th . ph)
public export %inline
id : Subst f n n
id = shift 0
public export
traverse : Applicative m =>
(f to -> m (g to)) -> Subst f from to -> m (Subst g from to)
traverse f (Shift by) = pure $ Shift by
traverse f (t ::: th) = [|f t !::: traverse f th|]
-- not in terms of traverse because this map can maintain laziness better
2021-07-20 16:05:19 -04:00
public export
map : (f to -> g to) -> Subst f from to -> Subst g from to
map f (Shift by) = Shift by
map f (t ::: th) = f t ::: map f th
public export %inline
push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
2021-07-20 16:05:19 -04:00
push th = fromVar VZ ::: (th . shift 1)
2023-01-22 21:22:50 -05:00
-- [fixme] a better way to do this?
public export
pushN : CanSubstSelf f => (s : Nat) ->
2023-01-22 21:22:50 -05:00
Subst f from to -> Subst f (s + from) (s + to)
pushN 0 th = th
pushN (S s) th =
rewrite plusSuccRightSucc s from in
rewrite plusSuccRightSucc s to in
pushN s $ fromVar VZ ::: (th . shift 1)
2021-09-09 17:56:10 -04:00
public export
drop1 : Subst f (S from) to -> Subst f from to
drop1 (Shift by) = Shift $ ssDown by
2021-09-09 17:56:10 -04:00
drop1 (t ::: th) = th
2021-07-20 16:05:19 -04:00
2023-01-26 13:54:46 -05:00
public export
2023-03-26 10:09:47 -04:00
fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
fromSnocVect [<] = id
fromSnocVect (xs :< x) = x ::: fromSnocVect xs
2023-01-26 13:54:46 -05:00
2022-02-26 19:46:44 -05:00
public export %inline
one : f n -> Subst f (S n) n
2023-03-26 10:09:47 -04:00
one x = fromSnocVect [< x]
2022-02-26 19:46:44 -05:00
2023-05-01 21:06:25 -04:00
||| whether two substitutions with the same codomain have the same shape
||| (the same number of terms and the same shift at the end). if so, they
||| also have the same domain
export
2023-05-01 21:06:25 -04:00
cmpShape : Subst env from1 to -> Subst env from2 to ->
Either Ordering (from1 = from2)
cmpShape (Shift by) (Shift bz) = cmpLen by bz
cmpShape (Shift _) (_ ::: _) = Left LT
cmpShape (_ ::: _) (Shift _) = Left GT
2023-07-13 15:28:39 -04:00
cmpShape (_ ::: th) (_ ::: ph) = map (\x => cong S x) $ cmpShape th ph
public export
record WithSubst tm env n where
constructor Sub
term : tm from
subst : Lazy (Subst env from n)
export
2023-05-01 21:06:25 -04:00
(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubst tm env n) where
Sub t1 s1 == Sub t2 s2 =
2023-05-01 21:06:25 -04:00
case cmpShape s1 s2 of
Left _ => False
Right Refl => t1 == t2 && s1 == s2
export
(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubst tm env n) where
Sub t1 s1 `compare` Sub t2 s2 =
case cmpShape s1 s2 of
Left o => o
Right Refl => compare (t1, s1) (t2, s2)
export %hint
2023-05-01 21:06:25 -04:00
ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
Show (WithSubst tm env n)
ShowWithSubst = deriveShow