@@ -99,6 +99,7 @@ data Err = Msg String
9999 -- unification succeed
100100 | InfiniteUnify Name Term [(Name, Type)]
101101 | CantConvert Term Term [(Name, Type)]
102+ | CantSolveGoal Term [(Name, Type)]
102103 | UnifyScope Name Name Term [(Name, Type)]
103104 | CantInferType String
104105 | NonFunctionType Term Term
@@ -156,6 +157,7 @@ score (CantUnify _ _ _ m _ s) = s + score m
156157score (CantResolve _) = 20
157158score (NoSuchVariable _) = 1000
158159score (ProofSearchFail _) = 10000
160+score (CantSolveGoal _ _) = 10000
159161score (InternalMsg _) = -1
160162score _ = 0
161163
@@ -164,6 +166,7 @@ instance Show Err where
164166 show (InternalMsg s) = "Internal error: " ++ show s
165167 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "
166168 ++ show e ++ " in " ++ show sc ++ " " ++ show i
169+ show (CantSolveGoal g _) = "CantSolve " ++ show g
167170 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
168171 show (ProviderError msg) = "Type provider error: " ++ msg
169172 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
@@ -334,6 +337,8 @@ emptyContext = Map.empty
334337mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
335338mapCtxt = fmap . fmap
336339
340+-- |Return True if the argument 'Name' should be interpreted as the name of a
341+-- typeclass.
337342tcname (UN xs) | T.null xs = False
338343 | otherwise = T.head xs == '@'
339344tcname (NS n _) = tcname n
@@ -503,11 +508,18 @@ deriving instance Binary Raw
503508deriving instance NFData Raw
504509!-}
505510
506−-- | All binding forms are represented in a unform fashion.
511+-- The type parameter `b` will normally be something like `TT Name` or just
512+-- `Raw`. We do not make a type-level distinction between TT terms that happen
513+-- to be TT types and TT terms that are not TT types.
514+-- | All binding forms are represented in a uniform fashion. This type only represents
515+-- the types of bindings (and their values, if any); the attached identifiers are part
516+-- of the 'Bind' constructor for the 'TT' type.
507517data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
508518 | Pi { binderTy :: !b }
519+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
509520 | Let { binderTy :: !b,
510521 binderVal :: b {-^ value for bound variable-}}
522+ -- ^ A binding that occurs in a @let@ expression
511523 | NLet { binderTy :: !b,
512524 binderVal :: b }
513525 | Hole { binderTy :: !b}
@@ -516,6 +528,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
516528 | Guess { binderTy :: !b,
517529 binderVal :: b }
518530 | PVar { binderTy :: !b }
531+ -- ^ A pattern variable
519532 | PVTy { binderTy :: !b }
520533 deriving (Show, Eq, Ord, Functor)
521534{-!
@@ -594,8 +607,8 @@ type UCs = (Int, [UConstraint])
594607
595608data NameType = Bound
596609 | Ref
597− | DCon Int Int -- ^ Data constructor; Ints are tag and arity
598− | TCon Int Int -- ^ Type constructor; Ints are tag and arity
610+ | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor
611+ | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
599612 deriving (Show, Ord)
600613{-!
601614deriving instance Binary NameType
@@ -615,8 +628,12 @@ instance Eq NameType where
615628 TCon _ a == TCon _ b = (a == b) -- ignore tag
616629 _ == _ = False
617630
618−-- | Terms in the core language
619−data TT n = P NameType n (TT n) -- ^ named references
631+-- | Terms in the core language. The type parameter is the type of
632+-- identifiers used for bindings and explicit named references;
633+-- usually we use @TT 'Name'@.
634+data TT n = P NameType n (TT n) -- ^ named references with type
635+ -- (P for "Parameter", motivated by McKinna and Pollack's
636+ -- Pure Type Systems Formalized)
620637 | V !Int -- ^ a resolved de Bruijn-indexed variable
621638 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
622639 | App !(TT n) (TT n) -- ^ function, function type, arg
@@ -640,10 +657,14 @@ instance TermSize a => TermSize [a] where
640657 termsize n (x : xs) = termsize n x + termsize n xs
641658
642659instance TermSize (TT Name) where
643− termsize n (P _ x _)
644− | x == n = 1000000 -- recursive => really big
660+ termsize n (P _ n' _)
661+ | n' == n = 1000000 -- recursive => really big
645662 | otherwise = 1
646663 termsize n (V _) = 1
664+ -- for `Bind` terms, we can erroneously declare a term
665+ -- "recursive => really big" if the name of the bound
666+ -- variable is the same as the name we're using
667+ -- So generate a different name in that case.
647668 termsize n (Bind n' (Let t v) sc)
648669 = let rn = if n == n' then sMN 0 "noname" else n in
649670 termsize rn v + termsize rn sc
@@ -709,6 +730,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
709730 instancesB _ = 0
710731vinstances i t = 0
711732
733+-- | Replace the outermost (index 0) de Bruijn variable with the given term
712734instantiate :: TT n -> TT n -> TT n
713735instantiate e = subst 0 where
714736 subst i (V x) | i == x = e
@@ -717,6 +739,9 @@ instantiate e = subst 0 where
717739 subst i (Proj x idx) = Proj (subst i x) idx
718740 subst i t = t
719741
742+-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
743+-- remaining in the term, so that there are no more references to the variable
744+-- that has been substituted.
720745substV :: TT n -> TT n -> TT n
721746substV x tm = dropV 0 (instantiate x tm) where
722747 dropV i (V x) | x > i = V (x - 1)
@@ -726,6 +751,8 @@ substV x tm = dropV 0 (instantiate x tm) where
726751 dropV i (Proj x idx) = Proj (dropV i x) idx
727752 dropV i t = t
728753
754+-- | Replace all non-free de Bruijn references in the given term with references
755+-- to the name of their binding.
729756explicitNames :: TT n -> TT n
730757explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
731758 Bind x b'
@@ -735,6 +762,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
735762explicitNames (Proj x idx) = Proj (explicitNames x) idx
736763explicitNames t = t
737764
765+-- | Replace references to the given 'Name'-like id with references to
766+-- de Bruijn index 0.
738767pToV :: Eq n => n -> TT n -> TT n
739768pToV n = pToV' n 0
740769pToV' n i (P _ x _) | n == x = V i
@@ -764,6 +793,9 @@ pToVs ns tm = pToVs' ns tm 0 where
764793 pToVs' [] tm i = tm
765794 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
766795
796+-- | Replace de Bruijn indices in the given term with explicit references to
797+-- the names of the bindings they refer to. It is an error if the given term
798+-- contains free de Bruijn indices.
767799vToP :: TT n -> TT n
768800vToP = vToP' [] where
769801 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -773,6 +805,8 @@ vToP = vToP' [] where
773805 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
774806 vToP' env t = t
775807
808+-- | Replace every non-free reference to the name of a binding in
809+-- the given term with a de Bruijn index.
776810finalise :: Eq n => TT n -> TT n
777811finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
778812finalise (App f a) = App (finalise f) (finalise a)
@@ -787,7 +821,12 @@ pEraseType (App f a) = App (pEraseType f) (pEraseType a)
787821pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
788822pEraseType t = t
789823
790−subst :: Eq n => n -> TT n -> TT n -> TT n
824+-- | As 'instantiate', but in addition to replacing @'V' 0@,
825+-- replace references to the given 'Name'-like id.
826+subst :: Eq n => n {-^ The id to replace -} ->
827+ TT n {-^ The replacement term -} ->
828+ TT n {-^ The term to replace in -} ->
829+ TT n
791830subst n v tm = instantiate v (pToV n tm)
792831
793832-- If there are no Vs in the term (i.e. in proof state)
@@ -800,19 +839,25 @@ psubst n v tm = s' tm where
800839 s' (Proj t idx) = Proj (s' t) idx
801840 s' t = t
802841
842+-- | As 'subst', but takes a list of (name, substitution) pairs instead
843+-- of a single name and substitution
803844substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
804845substNames [] t = t
805846substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
806847
807−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
848+-- | Replaces all terms equal (in the sense of @(==)@) to
849+-- the old term with the new term.
850+substTerm :: Eq n => TT n {-^ Old term -} ->
851+ TT n {-^ New term -} ->
852+ TT n {-^ template term -}
853+ -> TT n
808854substTerm old new = st where
809855 st t | t == old = new
810856 st (App f a) = App (st f) (st a)
811857 st (Bind x b sc) = Bind x (fmap st b) (st sc)
812858 st t = t
813859
814−-- Returns true if V 0 and bound name n do not occur in the term
815−
860+-- | Returns true if V 0 and bound name n do not occur in the term
816861noOccurrence :: Eq n => n -> TT n -> Bool
817862noOccurrence n t = no' 0 t
818863 where
@@ -847,6 +892,8 @@ unApply t = ua [] t where
847892 ua args (App f a) = ua (a:args) f
848893 ua args t = (t, args)
849894
895+-- | Returns a term representing the application of the first argument
896+-- (a function) to every element of the second argument.
850897mkApp :: TT n -> [TT n] -> TT n
851898mkApp f [] = f
852899mkApp f (a:as) = mkApp (App f a) as
@@ -859,6 +906,10 @@ unList tm = case unApply tm of
859906 return $ x:rest
860907 (f, args) -> Nothing
861908
909+-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
910+-- the types of named references and replacing all de Bruijn indices
911+-- with the corresponding name. It is an error if there are free de
912+-- Bruijn indices.
862913forget :: TT Name -> Raw
863914forget tm = fe [] tm
864915 where
@@ -873,13 +924,21 @@ forget tm = fe [] tm
873924 fe env (TType i) = RType
874925 fe env Erased = RConstant Forgot
875926
927+-- | Introduce a 'Bind' into the given term for each element of the
928+-- given list of (name, binder) pairs.
876929bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
877−bindAll [] t =t
930+bindAll [] t = t
878931bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
879932
933+-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
934+-- The first argument is a function to map @TT@ terms to @Binder@s.
935+-- This function might often be something like 'Lam', which directly
936+-- constructs a @Binder@ from a @TT@ term.
880937bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
881938bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
882939
940+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
941+-- variables in the given term, together with their types.
883942getArgTys :: TT n -> [(n, TT n)]
884943getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
885944getArgTys _ = []
@@ -927,7 +986,7 @@ type Type = Term
927986
928987type Env = EnvTT Name
929988
930−-- an environment with de Bruijn indices 'normalised' so that they all refer to
989+-- | an environment with de Bruijn indices 'normalised' so that they all refer to
931990-- this environment
932991
933992newtype WkEnvTT n = Wk (EnvTT n)
@@ -965,6 +1024,7 @@ instance Show Const where
9651024 show PtrType = "Ptr"
9661025 show VoidType = "Void"
9671026
1027+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
9681028showEnv env t = showEnv' env t False
9691029showEnvDbg env t = showEnv' env t True
9701030
@@ -1002,6 +1062,7 @@ prettyEnv env t = prettyEnv' env t False
10021062 prettySe p env Erased debug = text "[_]"
10031063 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
10041064
1065+ -- Render a `Binder` and its name
10051066 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
10061067 prettySb env n (Hole t) = prettyB env "?defer" "." n t
10071068 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -1010,9 +1071,14 @@ prettyEnv env t = prettyEnv' env t False
10101071 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
10111072 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
10121073
1074+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1075+ -- declaration
1076+ -- e.g. "λx : Int =>" for the Lam case
10131077 prettyB env op sc n t debug =
10141078 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
10151079
1080+ -- Like `prettyB`, but handle the bindings that have values in addition
1081+ -- to names and types
10161082 prettyBv env op sc n t v debug =
10171083 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
10181084 prettySe 10 env v debug <> text sc
@@ -1085,9 +1151,12 @@ weakenEnv env = wk (length env - 1) env
10851151 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
10861152 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
10871153
1154+-- | Weaken every term in the environment by the given amount
10881155weakenTmEnv :: Int -> EnvTT n -> EnvTT n
10891156weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
10901157
1158+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1159+-- them in a canonical order
10911160orderPats :: Term -> Term
10921161orderPats tm = op [] tm
10931162 where