quox/src/Quox/Syntax/Subst.idr

125 lines
3.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
import Quox.Pretty
import Data.List
%default total
infixr 5 :::
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
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
infixl 8 //
public export
interface FromVar env => CanSubst env term where
2021-09-09 17:54:18 -04:00
(//) : term from -> Lazy (Subst env from to) -> term to
2021-07-20 16:05:19 -04:00
public export
2021-09-03 10:34:57 -04:00
CanSubst1 : (Nat -> Type) -> Type
2021-07-20 16:05:19 -04:00
CanSubst1 f = CanSubst f f
infixl 8 !!
public export
(!!) : FromVar term => Subst term from to -> Var from -> term to
(Shift by) !! i = fromVar $ shift by i
(t ::: th) !! VZ = t
(t ::: th) !! (VS i) = th !! i
public export
CanSubst Var 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
infixl 9 .
public export
(.) : CanSubst1 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
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 : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
push th = 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 $ drop1 by
drop1 (t ::: th) = th
2021-07-20 16:05:19 -04:00
2021-11-21 08:59:41 -05:00
||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
2021-07-20 16:05:19 -04:00
||| with the following arguments:
|||
||| * `th : Subst f from to`
2021-11-21 08:59:41 -05:00
||| * `pr : f to -> m (Doc HL)` prints a single element
2021-07-20 16:05:19 -04:00
||| * `names : List Name` is a list of known bound var names
||| * `bnd : HL` is the highlight to use for bound variables being subsituted
||| * `op, cl : Doc HL` are the opening and closing brackets
export
prettySubstM : Pretty.HasEnv m =>
(pr : f to -> m (Doc HL)) ->
(names : List Name) -> (bnd : HL) -> (op, cl : Doc HL) ->
Subst f from to -> m (Doc HL)
2021-07-20 16:05:19 -04:00
prettySubstM pr names bnd op cl th =
encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$>
withPrec Outer (go 0 th)
where
go1 : Nat -> f to -> m (Doc HL)
2021-07-20 16:05:19 -04:00
go1 i t = pure $ hang 2 $ sep
[hsep [!(prettyVar' bnd bnd names i),
hl Delim !(ifUnicode "" ":=")],
!(pr t)]
go : forall from. Nat -> Subst f from to -> m (List (Doc HL))
2021-07-20 16:05:19 -04:00
go _ (Shift SZ) = pure []
go _ (Shift by) = [|pure (prettyShift bnd by)|]
go i (t ::: th) = [|go1 i t :: go (S i) th|]
||| prints with [square brackets] and the `TVar` highlight for variables
export
PrettyHL (f to) => PrettyHL (Subst f from to) where
2021-09-03 10:31:53 -04:00
prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th