@@ -469,11 +469,15 @@ deriving instance NFData Raw
469469-- The type parameter `b` will normally be something like `TT Name` or just
470470-- `Raw`. We do not make a type-level distinction between TT terms that happen
471471-- 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.
473475data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
474476 | Pi { binderTy :: b }
477+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
475478 | Let { binderTy :: b,
476479 binderVal :: b {-^ value for bound variable-}}
480+ -- ^ A binding that occurs in a @let@ expression
477481 | NLet { binderTy :: b,
478482 binderVal :: b }
479483 | Hole { binderTy :: b}
@@ -771,19 +775,25 @@ subst :: Eq n => n {-^ The id to replace -} ->
771775 TT n
772776subst n v tm = instantiate v (pToV n tm)
773777
778+-- | As 'subst', but takes a list of (name, substitution) pairs instead
779+-- of a single name and substitution
774780substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
775781substNames [] t = t
776782substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
777783
778−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
784+-- | Replaces all terms equal (in the sense of @(==)@) to
785+-- the old term with the new term.
786+substTerm :: Eq n => TT n {-^ Old term -} ->
787+ TT n {-^ New term -} ->
788+ TT n {-^ template term -}
789+ -> TT n
779790substTerm old new = st where
780791 st t | t == old = new
781792 st (App f a) = App (st f) (st a)
782793 st (Bind x b sc) = Bind x (fmap st b) (st sc)
783794 st t = t
784795
785−-- Returns true if V 0 and bound name n do not occur in the term
786−
796+-- | Returns true if V 0 and bound name n do not occur in the term
787797noOccurrence :: Eq n => n -> TT n -> Bool
788798noOccurrence n t = no' 0 t
789799 where
@@ -818,10 +828,16 @@ unApply t = ua [] t where
818828 ua args (App f a) = ua (a:args) f
819829 ua args t = (t, args)
820830
831+-- | Returns a term representing the application of the first argument
832+-- (a function) to every element of the second argument.
821833mkApp :: TT n -> [TT n] -> TT n
822834mkApp f [] = f
823835mkApp f (a:as) = mkApp (App f a) as
824836
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
840+-- Bruijn indices.
825841forget :: TT Name -> Raw
826842forget tm = fe [] tm
827843 where
@@ -835,13 +851,21 @@ forget tm = fe [] tm
835851 fe env (TType i) = RType
836852 fe env Erased = RConstant Forgot
837853
854+-- | Introduce a 'Bind' into the given term for each element of the
855+-- given list of (name, binder) pairs.
838856bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
839−bindAll [] t =t
857+bindAll [] t = t
840858bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
841859
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.
842864bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
843865bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
844866
867+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
868+-- variables in the given term, together with their types.
845869getArgTys :: TT n -> [(n, TT n)]
846870getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
847871getArgTys _ = []
@@ -889,7 +913,7 @@ type Type = Term
889913
890914type Env = EnvTT Name
891915
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
893917-- this environment
894918
895919newtype WkEnvTT n = Wk (EnvTT n)
@@ -927,6 +951,7 @@ instance Show Const where
927951 show PtrType = "Ptr"
928952 show VoidType = "Void"
929953
954+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
930955showEnv env t = showEnv' env t False
931956showEnvDbg env t = showEnv' env t True
932957
@@ -964,6 +989,7 @@ prettyEnv env t = prettyEnv' env t False
964989 prettySe p env Erased debug = text "[_]"
965990 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
966991
992+ -- Render a `Binder` and its name
967993 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
968994 prettySb env n (Hole t) = prettyB env "?defer" "." n t
969995 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -972,9 +998,14 @@ prettyEnv env t = prettyEnv' env t False
972998 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
973999 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
9741000
1001+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1002+ -- declaration
1003+ -- e.g. "λx : Int =>" for the Lam case
9751004 prettyB env op sc n t debug =
9761005 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
9771006
1007+ -- Like `prettyB`, but handle the bindings that have values in addition
1008+ -- to names and types
9781009 prettyBv env op sc n t v debug =
9791010 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
9801011 prettySe 10 env v debug <> text sc
@@ -1047,6 +1078,7 @@ weakenEnv env = wk (length env - 1) env
10471078 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
10481079 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
10491080
1081+-- | Weaken every term in the environment by the given amount
10501082weakenTmEnv :: Int -> EnvTT n -> EnvTT n
10511083weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
10521084