@@ -469,11 +469,15 @@ deriving instance NFData Raw
469-- The type parameter `b` will normally be something like `TT Name` or just
469-- The type parameter `b` will normally be something like `TT Name` or just
470-- `Raw`. We do not make a type-level distinction between TT terms that happen
470-- `Raw`. We do not make a type-level distinction between TT terms that happen
471-- to be TT types and TT terms that are not TT types.
471-- to be TT types and TT terms that are not TT types.
472−-- | All binding forms are represented in a uniform fashion.
472+-- | All binding forms are represented in a uniform fashion. This type only represents
473+-- the types of bindings (and their values, if any); the attached identifiers are part
474+-- of the 'Bind' constructor for the 'TT' type.
473data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
475data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
474 | Pi { binderTy :: b }
476 | Pi { binderTy :: b }
477+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
475 | Let { binderTy :: b,
478 | Let { binderTy :: b,
476 binderVal :: b {-^ value for bound variable-}}
479 binderVal :: b {-^ value for bound variable-}}
480+ -- ^ A binding that occurs in a @let@ expression
477 | NLet { binderTy :: b,
481 | NLet { binderTy :: b,
478 binderVal :: b }
482 binderVal :: b }
479 | Hole { binderTy :: b}
483 | Hole { binderTy :: b}
@@ -771,19 +775,25 @@ subst :: Eq n => n {-^ The id to replace -} ->
772subst n v tm = instantiate v (pToV n tm)
776subst n v tm = instantiate v (pToV n tm)
778+-- | As 'subst', but takes a list of (name, substitution) pairs instead
779+-- of a single name and substitution
774substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
780substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
775substNames [] t = t
781substNames [] t = t
776substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
782substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
784+-- | Replaces all terms equal (in the sense of @(==)@) to
785+-- the old term with the new term.
778−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
786+substTerm :: Eq n => TT n {-^ Old term -} ->
787+ TT n {-^ New term -} ->
788+ TT n {-^ template term -}
779substTerm old new = st where
790substTerm old new = st where
780 st t | t == old = new
791 st t | t == old = new
781 st (App f a) = App (st f) (st a)
792 st (App f a) = App (st f) (st a)
782 st (Bind x b sc) = Bind x (fmap st b) (st sc)
793 st (Bind x b sc) = Bind x (fmap st b) (st sc)
785−-- Returns true if V 0 and bound name n do not occur in the term
796+-- | Returns true if V 0 and bound name n do not occur in the term
787noOccurrence :: Eq n => n -> TT n -> Bool
797noOccurrence :: Eq n => n -> TT n -> Bool
788noOccurrence n t = no' 0 t
798noOccurrence n t = no' 0 t
@@ -818,10 +828,16 @@ unApply t = ua [] t where
818 ua args (App f a) = ua (a:args) f
828 ua args (App f a) = ua (a:args) f
819 ua args t = (t, args)
829 ua args t = (t, args)
831+-- | Returns a term representing the application of the first argument
832+-- (a function) to every element of the second argument.
821mkApp :: TT n -> [TT n] -> TT n
833mkApp :: TT n -> [TT n] -> TT n
822mkApp f [] = f
834mkApp f [] = f
823mkApp f (a:as) = mkApp (App f a) as
835mkApp f (a:as) = mkApp (App f a) as
837+-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
838+-- the types of named references and replacing all de Bruijn indices
839+-- with the corresponding name. It is an error if there are free de
825forget :: TT Name -> Raw
841forget :: TT Name -> Raw
826forget tm = fe [] tm
842forget tm = fe [] tm
@@ -835,13 +851,21 @@ forget tm = fe [] tm
835 fe env (TType i) = RType
851 fe env (TType i) = RType
836 fe env Erased = RConstant Forgot
852 fe env Erased = RConstant Forgot
854+-- | Introduce a 'Bind' into the given term for each element of the
855+-- given list of (name, binder) pairs.
838bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
856bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
839−bindAll [] t =t
857+bindAll [] t = t
840bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
858bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
860+-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
861+-- The first argument is a function to map @TT@ terms to @Binder@s.
862+-- This function might often be something like 'Lam', which directly
863+-- constructs a @Binder@ from a @TT@ term.
842bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
864bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
843bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
865bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
867+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
868+-- variables in the given term, together with their types.
845getArgTys :: TT n -> [(n, TT n)]
869getArgTys :: TT n -> [(n, TT n)]
846getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
870getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
847getArgTys _ = []
871getArgTys _ = []
@@ -889,7 +913,7 @@ type Type = Term
890type Env = EnvTT Name
914type Env = EnvTT Name
892−-- an environment with de Bruijn indices 'normalised' so that they all refer to
916+-- | an environment with de Bruijn indices 'normalised' so that they all refer to
893-- this environment
917-- this environment
895newtype WkEnvTT n = Wk (EnvTT n)
919newtype WkEnvTT n = Wk (EnvTT n)
@@ -927,6 +951,7 @@ instance Show Const where
927 show PtrType = "Ptr"
951 show PtrType = "Ptr"
928 show VoidType = "Void"
952 show VoidType = "Void"
954+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
930showEnv env t = showEnv' env t False
955showEnv env t = showEnv' env t False
931showEnvDbg env t = showEnv' env t True
956showEnvDbg env t = showEnv' env t True
@@ -964,6 +989,7 @@ prettyEnv env t = prettyEnv' env t False
964 prettySe p env Erased debug = text "[_]"
989 prettySe p env Erased debug = text "[_]"
965 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
990 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
992+ -- Render a `Binder` and its name
967 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
993 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
968 prettySb env n (Hole t) = prettyB env "?defer" "." n t
994 prettySb env n (Hole t) = prettyB env "?defer" "." n t
969 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
995 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -972,9 +998,14 @@ prettyEnv env t = prettyEnv' env t False
972 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
998 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
973 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
999 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1001+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1003+ -- e.g. "λx : Int =>" for the Lam case
975 prettyB env op sc n t debug =
1004 prettyB env op sc n t debug =
976 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1005 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1007+ -- Like `prettyB`, but handle the bindings that have values in addition
1008+ -- to names and types
978 prettyBv env op sc n t v debug =
1009 prettyBv env op sc n t v debug =
979 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1010 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
980 prettySe 10 env v debug <> text sc
1011 prettySe 10 env v debug <> text sc
@@ -1047,6 +1078,7 @@ weakenEnv env = wk (length env - 1) env
1047 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1078 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1048 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1079 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1081+-- | Weaken every term in the environment by the given amount
1050weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1082weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1051weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1083weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))