@@ -336,6 +336,8 @@ emptyContext = Map.empty
336336mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
337337mapCtxt = fmap . fmap
338338
339+-- |Return True if the argument 'Name' should be interpreted as the name of a
340+-- typeclass.
339341tcname (UN xs) | T.null xs = False
340342 | otherwise = T.head xs == '@'
341343tcname (NS n _) = tcname n
@@ -505,11 +507,18 @@ deriving instance Binary Raw
505507deriving instance NFData Raw
506508!-}
507509
508−-- | All binding forms are represented in a unform fashion.
510+-- The type parameter `b` will normally be something like `TT Name` or just
511+-- `Raw`. We do not make a type-level distinction between TT terms that happen
512+-- to be TT types and TT terms that are not TT types.
513+-- | All binding forms are represented in a uniform fashion. This type only represents
514+-- the types of bindings (and their values, if any); the attached identifiers are part
515+-- of the 'Bind' constructor for the 'TT' type.
509516data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
510517 | Pi { binderTy :: !b }
518+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
511519 | Let { binderTy :: !b,
512520 binderVal :: b {-^ value for bound variable-}}
521+ -- ^ A binding that occurs in a @let@ expression
513522 | NLet { binderTy :: !b,
514523 binderVal :: b }
515524 | Hole { binderTy :: !b}
@@ -518,6 +527,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
518527 | Guess { binderTy :: !b,
519528 binderVal :: b }
520529 | PVar { binderTy :: !b }
530+ -- ^ A pattern variable
521531 | PVTy { binderTy :: !b }
522532 deriving (Show, Eq, Ord, Functor)
523533{-!
@@ -596,8 +606,8 @@ type UCs = (Int, [UConstraint])
596606
597607data NameType = Bound
598608 | Ref
599− | DCon Int Int -- ^ Data constructor; Ints are tag and arity
600− | TCon Int Int -- ^ Type constructor; Ints are tag and arity
609+ | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor
610+ | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
601611 deriving (Show, Ord)
602612{-!
603613deriving instance Binary NameType
@@ -617,8 +627,12 @@ instance Eq NameType where
617627 TCon _ a == TCon _ b = (a == b) -- ignore tag
618628 _ == _ = False
619629
620−-- | Terms in the core language
621−data TT n = P NameType n (TT n) -- ^ named references
630+-- | Terms in the core language. The type parameter is the type of
631+-- identifiers used for bindings and explicit named references;
632+-- usually we use @TT 'Name'@.
633+data TT n = P NameType n (TT n) -- ^ named references with type
634+ -- (P for "Parameter", motivated by McKinna and Pollack's
635+ -- Pure Type Systems Formalized)
622636 | V !Int -- ^ a resolved de Bruijn-indexed variable
623637 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
624638 | App !(TT n) (TT n) -- ^ function, function type, arg
@@ -642,10 +656,14 @@ instance TermSize a => TermSize [a] where
642656 termsize n (x : xs) = termsize n x + termsize n xs
643657
644658instance TermSize (TT Name) where
645− termsize n (P _ x _)
646− | x == n = 1000000 -- recursive => really big
659+ termsize n (P _ n' _)
660+ | n' == n = 1000000 -- recursive => really big
647661 | otherwise = 1
648662 termsize n (V _) = 1
663+ -- for `Bind` terms, we can erroneously declare a term
664+ -- "recursive => really big" if the name of the bound
665+ -- variable is the same as the name we're using
666+ -- So generate a different name in that case.
649667 termsize n (Bind n' (Let t v) sc)
650668 = let rn = if n == n' then sMN 0 "noname" else n in
651669 termsize rn v + termsize rn sc
@@ -711,6 +729,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
711729 instancesB _ = 0
712730vinstances i t = 0
713731
732+-- | Replace the outermost (index 0) de Bruijn variable with the given term
714733instantiate :: TT n -> TT n -> TT n
715734instantiate e = subst 0 where
716735 subst i (V x) | i == x = e
@@ -719,6 +738,9 @@ instantiate e = subst 0 where
719738 subst i (Proj x idx) = Proj (subst i x) idx
720739 subst i t = t
721740
741+-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
742+-- remaining in the term, so that there are no more references to the variable
743+-- that has been substituted.
722744substV :: TT n -> TT n -> TT n
723745substV x tm = dropV 0 (instantiate x tm) where
724746 dropV i (V x) | x > i = V (x - 1)
@@ -728,6 +750,8 @@ substV x tm = dropV 0 (instantiate x tm) where
728750 dropV i (Proj x idx) = Proj (dropV i x) idx
729751 dropV i t = t
730752
753+-- | Replace all non-free de Bruijn references in the given term with references
754+-- to the name of their binding.
731755explicitNames :: TT n -> TT n
732756explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
733757 Bind x b'
@@ -737,6 +761,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
737761explicitNames (Proj x idx) = Proj (explicitNames x) idx
738762explicitNames t = t
739763
764+-- | Replace references to the given 'Name'-like id with references to
765+-- de Bruijn index 0.
740766pToV :: Eq n => n -> TT n -> TT n
741767pToV n = pToV' n 0
742768pToV' n i (P _ x _) | n == x = V i
@@ -766,6 +792,9 @@ pToVs ns tm = pToVs' ns tm 0 where
766792 pToVs' [] tm i = tm
767793 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
768794
795+-- | Replace de Bruijn indices in the given term with explicit references to
796+-- the names of the bindings they refer to. It is an error if the given term
797+-- contains free de Bruijn indices.
769798vToP :: TT n -> TT n
770799vToP = vToP' [] where
771800 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -775,6 +804,8 @@ vToP = vToP' [] where
775804 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
776805 vToP' env t = t
777806
807+-- | Replace every non-free reference to the name of a binding in
808+-- the given term with a de Bruijn index.
778809finalise :: Eq n => TT n -> TT n
779810finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
780811finalise (App f a) = App (finalise f) (finalise a)
@@ -789,7 +820,12 @@ pEraseType (App f a) = App (pEraseType f) (pEraseType a)
789820pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
790821pEraseType t = t
791822
792−subst :: Eq n => n -> TT n -> TT n -> TT n
823+-- | As 'instantiate', but in addition to replacing @'V' 0@,
824+-- replace references to the given 'Name'-like id.
825+subst :: Eq n => n {-^ The id to replace -} ->
826+ TT n {-^ The replacement term -} ->
827+ TT n {-^ The term to replace in -} ->
828+ TT n
793829subst n v tm = instantiate v (pToV n tm)
794830
795831-- If there are no Vs in the term (i.e. in proof state)
@@ -802,19 +838,25 @@ psubst n v tm = s' tm where
802838 s' (Proj t idx) = Proj (s' t) idx
803839 s' t = t
804840
841+-- | As 'subst', but takes a list of (name, substitution) pairs instead
842+-- of a single name and substitution
805843substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
806844substNames [] t = t
807845substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
808846
809−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
847+-- | Replaces all terms equal (in the sense of @(==)@) to
848+-- the old term with the new term.
849+substTerm :: Eq n => TT n {-^ Old term -} ->
850+ TT n {-^ New term -} ->
851+ TT n {-^ template term -}
852+ -> TT n
810853substTerm old new = st where
811854 st t | t == old = new
812855 st (App f a) = App (st f) (st a)
813856 st (Bind x b sc) = Bind x (fmap st b) (st sc)
814857 st t = t
815858
816−-- Returns true if V 0 and bound name n do not occur in the term
817−
859+-- | Returns true if V 0 and bound name n do not occur in the term
818860noOccurrence :: Eq n => n -> TT n -> Bool
819861noOccurrence n t = no' 0 t
820862 where
@@ -849,6 +891,8 @@ unApply t = ua [] t where
849891 ua args (App f a) = ua (a:args) f
850892 ua args t = (t, args)
851893
894+-- | Returns a term representing the application of the first argument
895+-- (a function) to every element of the second argument.
852896mkApp :: TT n -> [TT n] -> TT n
853897mkApp f [] = f
854898mkApp f (a:as) = mkApp (App f a) as
@@ -861,6 +905,10 @@ unList tm = case unApply tm of
861905 return $ x:rest
862906 (f, args) -> Nothing
863907
908+-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
909+-- the types of named references and replacing all de Bruijn indices
910+-- with the corresponding name. It is an error if there are free de
911+-- Bruijn indices.
864912forget :: TT Name -> Raw
865913forget tm = fe [] tm
866914 where
@@ -875,13 +923,21 @@ forget tm = fe [] tm
875923 fe env (TType i) = RType
876924 fe env Erased = RConstant Forgot
877925
926+-- | Introduce a 'Bind' into the given term for each element of the
927+-- given list of (name, binder) pairs.
878928bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
879−bindAll [] t =t
929+bindAll [] t = t
880930bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
881931
932+-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
933+-- The first argument is a function to map @TT@ terms to @Binder@s.
934+-- This function might often be something like 'Lam', which directly
935+-- constructs a @Binder@ from a @TT@ term.
882936bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
883937bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
884938
939+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
940+-- variables in the given term, together with their types.
885941getArgTys :: TT n -> [(n, TT n)]
886942getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
887943getArgTys _ = []
@@ -929,7 +985,7 @@ type Type = Term
929985
930986type Env = EnvTT Name
931987
932−-- an environment with de Bruijn indices 'normalised' so that they all refer to
988+-- | an environment with de Bruijn indices 'normalised' so that they all refer to
933989-- this environment
934990
935991newtype WkEnvTT n = Wk (EnvTT n)
@@ -967,6 +1023,7 @@ instance Show Const where
9671023 show PtrType = "Ptr"
9681024 show VoidType = "Void"
9691025
1026+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
9701027showEnv env t = showEnv' env t False
9711028showEnvDbg env t = showEnv' env t True
9721029
@@ -1004,6 +1061,7 @@ prettyEnv env t = prettyEnv' env t False
10041061 prettySe p env Erased debug = text "[_]"
10051062 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
10061063
1064+ -- Render a `Binder` and its name
10071065 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
10081066 prettySb env n (Hole t) = prettyB env "?defer" "." n t
10091067 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -1012,9 +1070,14 @@ prettyEnv env t = prettyEnv' env t False
10121070 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
10131071 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
10141072
1073+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1074+ -- declaration
1075+ -- e.g. "λx : Int =>" for the Lam case
10151076 prettyB env op sc n t debug =
10161077 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
10171078
1079+ -- Like `prettyB`, but handle the bindings that have values in addition
1080+ -- to names and types
10181081 prettyBv env op sc n t v debug =
10191082 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
10201083 prettySe 10 env v debug <> text sc
@@ -1087,9 +1150,12 @@ weakenEnv env = wk (length env - 1) env
10871150 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
10881151 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
10891152
1153+-- | Weaken every term in the environment by the given amount
10901154weakenTmEnv :: Int -> EnvTT n -> EnvTT n
10911155weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
10921156
1157+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1158+-- them in a canonical order
10931159orderPats :: Term -> Term
10941160orderPats tm = op [] tm
10951161 where