@@ -99,6 +99,7 @@ data Err = Msg String
99 -- unification succeed
99 -- unification succeed
100 | InfiniteUnify Name Term [(Name, Type)]
100 | InfiniteUnify Name Term [(Name, Type)]
101 | CantConvert Term Term [(Name, Type)]
101 | CantConvert Term Term [(Name, Type)]
102+ | CantSolveGoal Term [(Name, Type)]
102 | UnifyScope Name Name Term [(Name, Type)]
103 | UnifyScope Name Name Term [(Name, Type)]
103 | CantInferType String
104 | CantInferType String
104 | NonFunctionType Term Term
105 | NonFunctionType Term Term
@@ -156,6 +157,7 @@ score (CantUnify _ _ _ m _ s) = s + score m
156score (CantResolve _) = 20
157score (CantResolve _) = 20
157score (NoSuchVariable _) = 1000
158score (NoSuchVariable _) = 1000
158score (ProofSearchFail _) = 10000
159score (ProofSearchFail _) = 10000
160+score (CantSolveGoal _ _) = 10000
159score (InternalMsg _) = -1
161score (InternalMsg _) = -1
160score _ = 0
162score _ = 0
@@ -164,6 +166,7 @@ instance Show Err where
164 show (InternalMsg s) = "Internal error: " ++ show s
166 show (InternalMsg s) = "Internal error: " ++ show s
165 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "
167 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "
166 ++ show e ++ " in " ++ show sc ++ " " ++ show i
168 ++ show e ++ " in " ++ show sc ++ " " ++ show i
169+ show (CantSolveGoal g _) = "CantSolve " ++ show g
167 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
170 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
168 show (ProviderError msg) = "Type provider error: " ++ msg
171 show (ProviderError msg) = "Type provider error: " ++ msg
169 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
172 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
@@ -334,6 +337,8 @@ emptyContext = Map.empty
334mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
337mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
335mapCtxt = fmap . fmap
338mapCtxt = fmap . fmap
340+-- |Return True if the argument 'Name' should be interpreted as the name of a
337tcname (UN xs) | T.null xs = False
342tcname (UN xs) | T.null xs = False
338 | otherwise = T.head xs == '@'
343 | otherwise = T.head xs == '@'
339tcname (NS n _) = tcname n
344tcname (NS n _) = tcname n
@@ -503,11 +508,18 @@ deriving instance Binary Raw
503deriving instance NFData Raw
508deriving instance NFData Raw
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.
506−-- | All binding forms are represented in a unform fashion.
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.
507data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
517data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
508 | Pi { binderTy :: !b }
518 | Pi { binderTy :: !b }
519+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
509 | Let { binderTy :: !b,
520 | Let { binderTy :: !b,
510 binderVal :: b {-^ value for bound variable-}}
521 binderVal :: b {-^ value for bound variable-}}
522+ -- ^ A binding that occurs in a @let@ expression
511 | NLet { binderTy :: !b,
523 | NLet { binderTy :: !b,
512 binderVal :: b }
524 binderVal :: b }
513 | Hole { binderTy :: !b}
525 | Hole { binderTy :: !b}
@@ -516,6 +528,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
516 | Guess { binderTy :: !b,
528 | Guess { binderTy :: !b,
517 binderVal :: b }
529 binderVal :: b }
518 | PVar { binderTy :: !b }
530 | PVar { binderTy :: !b }
531+ -- ^ A pattern variable
519 | PVTy { binderTy :: !b }
532 | PVTy { binderTy :: !b }
520 deriving (Show, Eq, Ord, Functor)
533 deriving (Show, Eq, Ord, Functor)
@@ -594,8 +607,8 @@ type UCs = (Int, [UConstraint])
595data NameType = Bound
608data NameType = Bound
597− | DCon Int Int -- ^ Data constructor; Ints are tag and arity
610+ | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor
598− | TCon Int Int -- ^ Type constructor; Ints are tag and arity
611+ | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
599 deriving (Show, Ord)
612 deriving (Show, Ord)
601deriving instance Binary NameType
614deriving instance Binary NameType
@@ -615,8 +628,12 @@ instance Eq NameType where
615 TCon _ a == TCon _ b = (a == b) -- ignore tag
628 TCon _ a == TCon _ b = (a == b) -- ignore tag
616 _ == _ = False
629 _ == _ = False
618−-- | Terms in the core language
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'@.
619−data TT n = P NameType n (TT n) -- ^ named references
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)
620 | V !Int -- ^ a resolved de Bruijn-indexed variable
637 | V !Int -- ^ a resolved de Bruijn-indexed variable
621 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
638 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
622 | App !(TT n) (TT n) -- ^ function, function type, arg
639 | App !(TT n) (TT n) -- ^ function, function type, arg
@@ -640,10 +657,14 @@ instance TermSize a => TermSize [a] where
640 termsize n (x : xs) = termsize n x + termsize n xs
657 termsize n (x : xs) = termsize n x + termsize n xs
642instance TermSize (TT Name) where
659instance TermSize (TT Name) where
643− termsize n (P _ x _)
660+ termsize n (P _ n' _)
644− | x == n = 1000000 -- recursive => really big
661+ | n' == n = 1000000 -- recursive => really big
645 | otherwise = 1
662 | otherwise = 1
646 termsize n (V _) = 1
663 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.
647 termsize n (Bind n' (Let t v) sc)
668 termsize n (Bind n' (Let t v) sc)
648 = let rn = if n == n' then sMN 0 "noname" else n in
669 = let rn = if n == n' then sMN 0 "noname" else n in
649 termsize rn v + termsize rn sc
670 termsize rn v + termsize rn sc
@@ -709,6 +730,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
709 instancesB _ = 0
730 instancesB _ = 0
710vinstances i t = 0
731vinstances i t = 0
733+-- | Replace the outermost (index 0) de Bruijn variable with the given term
712instantiate :: TT n -> TT n -> TT n
734instantiate :: TT n -> TT n -> TT n
713instantiate e = subst 0 where
735instantiate e = subst 0 where
714 subst i (V x) | i == x = e
736 subst i (V x) | i == x = e
@@ -717,6 +739,9 @@ instantiate e = subst 0 where
717 subst i (Proj x idx) = Proj (subst i x) idx
739 subst i (Proj x idx) = Proj (subst i x) idx
718 subst i t = t
740 subst i t = t
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.
720substV :: TT n -> TT n -> TT n
745substV :: TT n -> TT n -> TT n
721substV x tm = dropV 0 (instantiate x tm) where
746substV x tm = dropV 0 (instantiate x tm) where
722 dropV i (V x) | x > i = V (x - 1)
747 dropV i (V x) | x > i = V (x - 1)
@@ -726,6 +751,8 @@ substV x tm = dropV 0 (instantiate x tm) where
726 dropV i (Proj x idx) = Proj (dropV i x) idx
751 dropV i (Proj x idx) = Proj (dropV i x) idx
727 dropV i t = t
752 dropV i t = t
754+-- | Replace all non-free de Bruijn references in the given term with references
755+-- to the name of their binding.
729explicitNames :: TT n -> TT n
756explicitNames :: TT n -> TT n
730explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
757explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
731 Bind x b'
758 Bind x b'
@@ -735,6 +762,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
735explicitNames (Proj x idx) = Proj (explicitNames x) idx
762explicitNames (Proj x idx) = Proj (explicitNames x) idx
736explicitNames t = t
763explicitNames t = t
765+-- | Replace references to the given 'Name'-like id with references to
766+-- de Bruijn index 0.
738pToV :: Eq n => n -> TT n -> TT n
767pToV :: Eq n => n -> TT n -> TT n
739pToV n = pToV' n 0
768pToV n = pToV' n 0
740pToV' n i (P _ x _) | n == x = V i
769pToV' n i (P _ x _) | n == x = V i
@@ -764,6 +793,9 @@ pToVs ns tm = pToVs' ns tm 0 where
764 pToVs' [] tm i = tm
793 pToVs' [] tm i = tm
765 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
794 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
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.
767vToP :: TT n -> TT n
799vToP :: TT n -> TT n
768vToP = vToP' [] where
800vToP = vToP' [] where
769 vToP' env (V i) = let (n, b) = (env !! i) in
801 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -773,6 +805,8 @@ vToP = vToP' [] where
773 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
805 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
774 vToP' env t = t
806 vToP' env t = t
808+-- | Replace every non-free reference to the name of a binding in
809+-- the given term with a de Bruijn index.
776finalise :: Eq n => TT n -> TT n
810finalise :: Eq n => TT n -> TT n
777finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
811finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
778finalise (App f a) = App (finalise f) (finalise a)
812finalise (App f a) = App (finalise f) (finalise a)
@@ -787,7 +821,12 @@ pEraseType (App f a) = App (pEraseType f) (pEraseType a)
787pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
821pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
788pEraseType t = t
822pEraseType t = t
824+-- | As 'instantiate', but in addition to replacing @'V' 0@,
825+-- replace references to the given 'Name'-like id.
790−subst :: Eq n => n -> TT n -> TT n -> TT n
826+subst :: Eq n => n {-^ The id to replace -} ->
827+ TT n {-^ The replacement term -} ->
828+ TT n {-^ The term to replace in -} ->
791subst n v tm = instantiate v (pToV n tm)
830subst n v tm = instantiate v (pToV n tm)
793-- If there are no Vs in the term (i.e. in proof state)
832-- If there are no Vs in the term (i.e. in proof state)
@@ -800,19 +839,25 @@ psubst n v tm = s' tm where
800 s' (Proj t idx) = Proj (s' t) idx
839 s' (Proj t idx) = Proj (s' t) idx
842+-- | As 'subst', but takes a list of (name, substitution) pairs instead
843+-- of a single name and substitution
803substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
844substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
804substNames [] t = t
845substNames [] t = t
805substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
846substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
848+-- | Replaces all terms equal (in the sense of @(==)@) to
849+-- the old term with the new term.
807−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
850+substTerm :: Eq n => TT n {-^ Old term -} ->
851+ TT n {-^ New term -} ->
852+ TT n {-^ template term -}
808substTerm old new = st where
854substTerm old new = st where
809 st t | t == old = new
855 st t | t == old = new
810 st (App f a) = App (st f) (st a)
856 st (App f a) = App (st f) (st a)
811 st (Bind x b sc) = Bind x (fmap st b) (st sc)
857 st (Bind x b sc) = Bind x (fmap st b) (st sc)
814−-- Returns true if V 0 and bound name n do not occur in the term
860+-- | Returns true if V 0 and bound name n do not occur in the term
816noOccurrence :: Eq n => n -> TT n -> Bool
861noOccurrence :: Eq n => n -> TT n -> Bool
817noOccurrence n t = no' 0 t
862noOccurrence n t = no' 0 t
@@ -847,6 +892,8 @@ unApply t = ua [] t where
847 ua args (App f a) = ua (a:args) f
892 ua args (App f a) = ua (a:args) f
848 ua args t = (t, args)
893 ua args t = (t, args)
895+-- | Returns a term representing the application of the first argument
896+-- (a function) to every element of the second argument.
850mkApp :: TT n -> [TT n] -> TT n
897mkApp :: TT n -> [TT n] -> TT n
851mkApp f [] = f
898mkApp f [] = f
852mkApp f (a:as) = mkApp (App f a) as
899mkApp f (a:as) = mkApp (App f a) as
@@ -859,6 +906,10 @@ unList tm = case unApply tm of
859 return $ x:rest
906 return $ x:rest
860 (f, args) -> Nothing
907 (f, args) -> Nothing
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
862forget :: TT Name -> Raw
913forget :: TT Name -> Raw
863forget tm = fe [] tm
914forget tm = fe [] tm
@@ -873,13 +924,21 @@ forget tm = fe [] tm
873 fe env (TType i) = RType
924 fe env (TType i) = RType
874 fe env Erased = RConstant Forgot
925 fe env Erased = RConstant Forgot
927+-- | Introduce a 'Bind' into the given term for each element of the
928+-- given list of (name, binder) pairs.
876bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
929bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
877−bindAll [] t =t
930+bindAll [] t = t
878bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
931bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
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.
880bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
937bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
881bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
938bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
940+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
941+-- variables in the given term, together with their types.
883getArgTys :: TT n -> [(n, TT n)]
942getArgTys :: TT n -> [(n, TT n)]
884getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
943getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
885getArgTys _ = []
944getArgTys _ = []
@@ -927,7 +986,7 @@ type Type = Term
928type Env = EnvTT Name
987type Env = EnvTT Name
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
931-- this environment
990-- this environment
933newtype WkEnvTT n = Wk (EnvTT n)
992newtype WkEnvTT n = Wk (EnvTT n)
@@ -965,6 +1024,7 @@ instance Show Const where
965 show PtrType = "Ptr"
1024 show PtrType = "Ptr"
966 show VoidType = "Void"
1025 show VoidType = "Void"
1027+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
968showEnv env t = showEnv' env t False
1028showEnv env t = showEnv' env t False
969showEnvDbg env t = showEnv' env t True
1029showEnvDbg env t = showEnv' env t True
@@ -1002,6 +1062,7 @@ prettyEnv env t = prettyEnv' env t False
1002 prettySe p env Erased debug = text "[_]"
1062 prettySe p env Erased debug = text "[_]"
1003 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1063 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1065+ -- Render a `Binder` and its name
1005 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1066 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1006 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1067 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1007 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
1068 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -1010,9 +1071,14 @@ prettyEnv env t = prettyEnv' env t False
1010 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1071 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1011 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1072 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1074+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1076+ -- e.g. "λx : Int =>" for the Lam case
1013 prettyB env op sc n t debug =
1077 prettyB env op sc n t debug =
1014 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1078 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1080+ -- Like `prettyB`, but handle the bindings that have values in addition
1081+ -- to names and types
1016 prettyBv env op sc n t v debug =
1082 prettyBv env op sc n t v debug =
1017 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1083 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1018 prettySe 10 env v debug <> text sc
1084 prettySe 10 env v debug <> text sc
@@ -1085,9 +1151,12 @@ weakenEnv env = wk (length env - 1) env
1085 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1151 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1086 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1152 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1154+-- | Weaken every term in the environment by the given amount
1088weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1155weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1089weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1156weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1158+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1159+-- them in a canonical order
1091orderPats :: Term -> Term
1160orderPats :: Term -> Term
1092orderPats tm = op [] tm
1161orderPats tm = op [] tm