@@ -99,40 +99,45 @@ data ErrorReportPart = TextPart String
9999
100100-- | Idris errors. Used as exceptions in the compiler, but reported to users
101101-- if they reach the top level.
102−data Err = Msg String
102+data Err' t
103+ = Msg String
103104 | InternalMsg String
104− | CantUnify Bool Term Term Err [(Name, Type)] Int
105+ | CantUnify Bool t t (Err' t) [(Name, t)] Int
105106 -- Int is 'score' - how much we did unify
106107 -- Bool indicates recoverability, True indicates more info may make
107108 -- unification succeed
108− | InfiniteUnify Name Term [(Name, Type)]
109− | CantConvert Term Term [(Name, Type)]
110− | UnifyScope Name Name Term [(Name, Type)]
109+ | InfiniteUnify Name t [(Name, t)]
110+ | CantConvert t t [(Name, t)]
111+ | CantSolveGoal t [(Name, t)]
112+ | UnifyScope Name Name t [(Name, t)]
111113 | CantInferType String
112− | NonFunctionType Term Term
113− | NotEquality Term Term
114+ | NonFunctionType t t
115+ | NotEquality t t
114116 | TooManyArguments Name
115− | CantIntroduce Term
117+ | CantIntroduce t
116118 | NoSuchVariable Name
117119 | NoTypeDecl Name
118− | NotInjective Term Term Term
119− | CantResolve Term
120+ | NotInjective t t t
121+ | CantResolve t
120122 | CantResolveAlts [String]
121− | IncompleteTerm Term
123+ | IncompleteTerm t
122124 | UniverseError
123125 | ProgramLineComment
124126 | Inaccessible Name
125127 | NonCollapsiblePostulate Name
126128 | AlreadyDefined Name
127− | ProofSearchFail Err
128− | NoRewriting Term
129− | At FC Err
130− | Elaborating String Name Err
129+ | ProofSearchFail (Err' t)
130+ | NoRewriting t
131+ | At FC (Err' t)
132+ | Elaborating String Name (Err' t)
131133 | ProviderError String
132− | LoadingFailed String Err
133− | ReflectionError [[ErrorReportPart]] Err
134− | ReflectionFailed String Err
135− deriving Eq
134+ | LoadingFailed String (Err' t)
135+ | ReflectionError [[ErrorReportPart]] (Err' t)
136+ | ReflectionFailed String (Err' t)
137+ deriving (Eq, Functor)
138+
139+type Err = Err' Term
140+
136141{-!
137142deriving instance NFData Err
138143!-}
@@ -164,6 +169,7 @@ score (CantUnify _ _ _ m _ s) = s + score m
164169score (CantResolve _) = 20
165170score (NoSuchVariable _) = 1000
166171score (ProofSearchFail _) = 10000
172+score (CantSolveGoal _ _) = 10000
167173score (InternalMsg _) = -1
168174score _ = 0
169175
@@ -172,6 +178,7 @@ instance Show Err where
172178 show (InternalMsg s) = "Internal error: " ++ show s
173179 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "
174180 ++ show e ++ " in " ++ show sc ++ " " ++ show i
181+ show (CantSolveGoal g _) = "CantSolve " ++ show g
175182 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
176183 show (ProviderError msg) = "Type provider error: " ++ msg
177184 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
@@ -346,6 +353,8 @@ emptyContext = Map.empty
346353mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
347354mapCtxt = fmap . fmap
348355
356+-- |Return True if the argument 'Name' should be interpreted as the name of a
357+-- typeclass.
349358tcname (UN xs) | T.null xs = False
350359 | otherwise = T.head xs == '@'
351360tcname (NS n _) = tcname n
@@ -515,11 +524,18 @@ deriving instance Binary Raw
515524deriving instance NFData Raw
516525!-}
517526
518−-- | All binding forms are represented in a unform fashion.
527+-- The type parameter `b` will normally be something like `TT Name` or just
528+-- `Raw`. We do not make a type-level distinction between TT terms that happen
529+-- to be TT types and TT terms that are not TT types.
530+-- | All binding forms are represented in a uniform fashion. This type only represents
531+-- the types of bindings (and their values, if any); the attached identifiers are part
532+-- of the 'Bind' constructor for the 'TT' type.
519533data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
520534 | Pi { binderTy :: !b }
535+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
521536 | Let { binderTy :: !b,
522537 binderVal :: b {-^ value for bound variable-}}
538+ -- ^ A binding that occurs in a @let@ expression
523539 | NLet { binderTy :: !b,
524540 binderVal :: b }
525541 | Hole { binderTy :: !b}
@@ -528,6 +544,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
528544 | Guess { binderTy :: !b,
529545 binderVal :: b }
530546 | PVar { binderTy :: !b }
547+ -- ^ A pattern variable
531548 | PVTy { binderTy :: !b }
532549 deriving (Show, Eq, Ord, Functor)
533550{-!
@@ -606,8 +623,8 @@ type UCs = (Int, [UConstraint])
606623
607624data NameType = Bound
608625 | Ref
609− | DCon Int Int -- ^ Data constructor; Ints are tag and arity
610− | TCon Int Int -- ^ Type constructor; Ints are tag and arity
626+ | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor
627+ | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
611628 deriving (Show, Ord)
612629{-!
613630deriving instance Binary NameType
@@ -627,8 +644,12 @@ instance Eq NameType where
627644 TCon _ a == TCon _ b = (a == b) -- ignore tag
628645 _ == _ = False
629646
630−-- | Terms in the core language
631−data TT n = P NameType n (TT n) -- ^ named references
647+-- | Terms in the core language. The type parameter is the type of
648+-- identifiers used for bindings and explicit named references;
649+-- usually we use @TT 'Name'@.
650+data TT n = P NameType n (TT n) -- ^ named references with type
651+ -- (P for "Parameter", motivated by McKinna and Pollack's
652+ -- Pure Type Systems Formalized)
632653 | V !Int -- ^ a resolved de Bruijn-indexed variable
633654 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
634655 | App !(TT n) (TT n) -- ^ function, function type, arg
@@ -652,10 +673,14 @@ instance TermSize a => TermSize [a] where
652673 termsize n (x : xs) = termsize n x + termsize n xs
653674
654675instance TermSize (TT Name) where
655− termsize n (P _ x _)
656− | x == n = 1000000 -- recursive => really big
676+ termsize n (P _ n' _)
677+ | n' == n = 1000000 -- recursive => really big
657678 | otherwise = 1
658679 termsize n (V _) = 1
680+ -- for `Bind` terms, we can erroneously declare a term
681+ -- "recursive => really big" if the name of the bound
682+ -- variable is the same as the name we're using
683+ -- So generate a different name in that case.
659684 termsize n (Bind n' (Let t v) sc)
660685 = let rn = if n == n' then sMN 0 "noname" else n in
661686 termsize rn v + termsize rn sc
@@ -721,6 +746,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
721746 instancesB _ = 0
722747vinstances i t = 0
723748
749+-- | Replace the outermost (index 0) de Bruijn variable with the given term
724750instantiate :: TT n -> TT n -> TT n
725751instantiate e = subst 0 where
726752 subst i (V x) | i == x = e
@@ -729,6 +755,9 @@ instantiate e = subst 0 where
729755 subst i (Proj x idx) = Proj (subst i x) idx
730756 subst i t = t
731757
758+-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
759+-- remaining in the term, so that there are no more references to the variable
760+-- that has been substituted.
732761substV :: TT n -> TT n -> TT n
733762substV x tm = dropV 0 (instantiate x tm) where
734763 dropV i (V x) | x > i = V (x - 1)
@@ -738,6 +767,8 @@ substV x tm = dropV 0 (instantiate x tm) where
738767 dropV i (Proj x idx) = Proj (dropV i x) idx
739768 dropV i t = t
740769
770+-- | Replace all non-free de Bruijn references in the given term with references
771+-- to the name of their binding.
741772explicitNames :: TT n -> TT n
742773explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
743774 Bind x b'
@@ -747,6 +778,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
747778explicitNames (Proj x idx) = Proj (explicitNames x) idx
748779explicitNames t = t
749780
781+-- | Replace references to the given 'Name'-like id with references to
782+-- de Bruijn index 0.
750783pToV :: Eq n => n -> TT n -> TT n
751784pToV n = pToV' n 0
752785pToV' n i (P _ x _) | n == x = V i
@@ -776,6 +809,9 @@ pToVs ns tm = pToVs' ns tm 0 where
776809 pToVs' [] tm i = tm
777810 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
778811
812+-- | Replace de Bruijn indices in the given term with explicit references to
813+-- the names of the bindings they refer to. It is an error if the given term
814+-- contains free de Bruijn indices.
779815vToP :: TT n -> TT n
780816vToP = vToP' [] where
781817 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -785,6 +821,8 @@ vToP = vToP' [] where
785821 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
786822 vToP' env t = t
787823
824+-- | Replace every non-free reference to the name of a binding in
825+-- the given term with a de Bruijn index.
788826finalise :: Eq n => TT n -> TT n
789827finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
790828finalise (App f a) = App (finalise f) (finalise a)
@@ -799,7 +837,12 @@ pEraseType (App f a) = App (pEraseType f) (pEraseType a)
799837pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
800838pEraseType t = t
801839
802−subst :: Eq n => n -> TT n -> TT n -> TT n
840+-- | As 'instantiate', but in addition to replacing @'V' 0@,
841+-- replace references to the given 'Name'-like id.
842+subst :: Eq n => n {-^ The id to replace -} ->
843+ TT n {-^ The replacement term -} ->
844+ TT n {-^ The term to replace in -} ->
845+ TT n
803846subst n v tm = instantiate v (pToV n tm)
804847
805848-- If there are no Vs in the term (i.e. in proof state)
@@ -812,19 +855,25 @@ psubst n v tm = s' tm where
812855 s' (Proj t idx) = Proj (s' t) idx
813856 s' t = t
814857
858+-- | As 'subst', but takes a list of (name, substitution) pairs instead
859+-- of a single name and substitution
815860substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
816861substNames [] t = t
817862substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
818863
819−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
864+-- | Replaces all terms equal (in the sense of @(==)@) to
865+-- the old term with the new term.
866+substTerm :: Eq n => TT n {-^ Old term -} ->
867+ TT n {-^ New term -} ->
868+ TT n {-^ template term -}
869+ -> TT n
820870substTerm old new = st where
821871 st t | t == old = new
822872 st (App f a) = App (st f) (st a)
823873 st (Bind x b sc) = Bind x (fmap st b) (st sc)
824874 st t = t
825875
826−-- Returns true if V 0 and bound name n do not occur in the term
827−
876+-- | Returns true if V 0 and bound name n do not occur in the term
828877noOccurrence :: Eq n => n -> TT n -> Bool
829878noOccurrence n t = no' 0 t
830879 where
@@ -859,6 +908,8 @@ unApply t = ua [] t where
859908 ua args (App f a) = ua (a:args) f
860909 ua args t = (t, args)
861910
911+-- | Returns a term representing the application of the first argument
912+-- (a function) to every element of the second argument.
862913mkApp :: TT n -> [TT n] -> TT n
863914mkApp f [] = f
864915mkApp f (a:as) = mkApp (App f a) as
@@ -871,6 +922,10 @@ unList tm = case unApply tm of
871922 return $ x:rest
872923 (f, args) -> Nothing
873924
925+-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
926+-- the types of named references and replacing all de Bruijn indices
927+-- with the corresponding name. It is an error if there are free de
928+-- Bruijn indices.
874929forget :: TT Name -> Raw
875930forget tm = fe [] tm
876931 where
@@ -885,13 +940,21 @@ forget tm = fe [] tm
885940 fe env (TType i) = RType
886941 fe env Erased = RConstant Forgot
887942
943+-- | Introduce a 'Bind' into the given term for each element of the
944+-- given list of (name, binder) pairs.
888945bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
889−bindAll [] t =t
946+bindAll [] t = t
890947bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
891948
949+-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
950+-- The first argument is a function to map @TT@ terms to @Binder@s.
951+-- This function might often be something like 'Lam', which directly
952+-- constructs a @Binder@ from a @TT@ term.
892953bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
893954bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
894955
956+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
957+-- variables in the given term, together with their types.
895958getArgTys :: TT n -> [(n, TT n)]
896959getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
897960getArgTys _ = []
@@ -939,7 +1002,7 @@ type Type = Term
9391002
9401003type Env = EnvTT Name
9411004
942−-- an environment with de Bruijn indices 'normalised' so that they all refer to
1005+-- | an environment with de Bruijn indices 'normalised' so that they all refer to
9431006-- this environment
9441007
9451008newtype WkEnvTT n = Wk (EnvTT n)
@@ -977,6 +1040,7 @@ instance Show Const where
9771040 show PtrType = "Ptr"
9781041 show VoidType = "Void"
9791042
1043+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
9801044showEnv env t = showEnv' env t False
9811045showEnvDbg env t = showEnv' env t True
9821046
@@ -1014,6 +1078,7 @@ prettyEnv env t = prettyEnv' env t False
10141078 prettySe p env Erased debug = text "[_]"
10151079 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
10161080
1081+ -- Render a `Binder` and its name
10171082 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
10181083 prettySb env n (Hole t) = prettyB env "?defer" "." n t
10191084 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -1022,9 +1087,14 @@ prettyEnv env t = prettyEnv' env t False
10221087 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
10231088 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
10241089
1090+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1091+ -- declaration
1092+ -- e.g. "λx : Int =>" for the Lam case
10251093 prettyB env op sc n t debug =
10261094 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
10271095
1096+ -- Like `prettyB`, but handle the bindings that have values in addition
1097+ -- to names and types
10281098 prettyBv env op sc n t v debug =
10291099 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
10301100 prettySe 10 env v debug <> text sc
@@ -1097,9 +1167,12 @@ weakenEnv env = wk (length env - 1) env
10971167 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
10981168 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
10991169
1170+-- | Weaken every term in the environment by the given amount
11001171weakenTmEnv :: Int -> EnvTT n -> EnvTT n
11011172weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
11021173
1174+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1175+-- them in a canonical order
11031176orderPats :: Term -> Term
11041177orderPats tm = op [] tm
11051178 where