@@ -336,6 +336,8 @@ emptyContext = Map.empty
336mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
336mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
337mapCtxt = fmap . fmap
337mapCtxt = fmap . fmap
339+-- |Return True if the argument 'Name' should be interpreted as the name of a
339tcname (UN xs) | T.null xs = False
341tcname (UN xs) | T.null xs = False
340 | otherwise = T.head xs == '@'
342 | otherwise = T.head xs == '@'
341tcname (NS n _) = tcname n
343tcname (NS n _) = tcname n
@@ -505,11 +507,18 @@ deriving instance Binary Raw
505deriving instance NFData Raw
507deriving instance NFData Raw
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.
508−-- | All binding forms are represented in a unform fashion.
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.
509data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
516data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
510 | Pi { binderTy :: !b }
517 | Pi { binderTy :: !b }
518+ {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
511 | Let { binderTy :: !b,
519 | Let { binderTy :: !b,
512 binderVal :: b {-^ value for bound variable-}}
520 binderVal :: b {-^ value for bound variable-}}
521+ -- ^ A binding that occurs in a @let@ expression
513 | NLet { binderTy :: !b,
522 | NLet { binderTy :: !b,
514 binderVal :: b }
523 binderVal :: b }
515 | Hole { binderTy :: !b}
524 | Hole { binderTy :: !b}
@@ -518,6 +527,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
518 | Guess { binderTy :: !b,
527 | Guess { binderTy :: !b,
519 binderVal :: b }
528 binderVal :: b }
520 | PVar { binderTy :: !b }
529 | PVar { binderTy :: !b }
530+ -- ^ A pattern variable
521 | PVTy { binderTy :: !b }
531 | PVTy { binderTy :: !b }
522 deriving (Show, Eq, Ord, Functor)
532 deriving (Show, Eq, Ord, Functor)
@@ -596,8 +606,8 @@ type UCs = (Int, [UConstraint])
597data NameType = Bound
607data NameType = Bound
599− | DCon Int Int -- ^ Data constructor; Ints are tag and arity
609+ | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor
600− | TCon Int Int -- ^ Type constructor; Ints are tag and arity
610+ | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
601 deriving (Show, Ord)
611 deriving (Show, Ord)
603deriving instance Binary NameType
613deriving instance Binary NameType
@@ -617,8 +627,12 @@ instance Eq NameType where
617 TCon _ a == TCon _ b = (a == b) -- ignore tag
627 TCon _ a == TCon _ b = (a == b) -- ignore tag
618 _ == _ = False
628 _ == _ = False
620−-- | Terms in the core language
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'@.
621−data TT n = P NameType n (TT n) -- ^ named references
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)
622 | V !Int -- ^ a resolved de Bruijn-indexed variable
636 | V !Int -- ^ a resolved de Bruijn-indexed variable
623 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
637 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
624 | App !(TT n) (TT n) -- ^ function, function type, arg
638 | App !(TT n) (TT n) -- ^ function, function type, arg
@@ -642,10 +656,14 @@ instance TermSize a => TermSize [a] where
642 termsize n (x : xs) = termsize n x + termsize n xs
656 termsize n (x : xs) = termsize n x + termsize n xs
644instance TermSize (TT Name) where
658instance TermSize (TT Name) where
645− termsize n (P _ x _)
659+ termsize n (P _ n' _)
646− | x == n = 1000000 -- recursive => really big
660+ | n' == n = 1000000 -- recursive => really big
647 | otherwise = 1
661 | otherwise = 1
648 termsize n (V _) = 1
662 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.
649 termsize n (Bind n' (Let t v) sc)
667 termsize n (Bind n' (Let t v) sc)
650 = let rn = if n == n' then sMN 0 "noname" else n in
668 = let rn = if n == n' then sMN 0 "noname" else n in
651 termsize rn v + termsize rn sc
669 termsize rn v + termsize rn sc
@@ -711,6 +729,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
711 instancesB _ = 0
729 instancesB _ = 0
712vinstances i t = 0
730vinstances i t = 0
732+-- | Replace the outermost (index 0) de Bruijn variable with the given term
714instantiate :: TT n -> TT n -> TT n
733instantiate :: TT n -> TT n -> TT n
715instantiate e = subst 0 where
734instantiate e = subst 0 where
716 subst i (V x) | i == x = e
735 subst i (V x) | i == x = e
@@ -719,6 +738,9 @@ instantiate e = subst 0 where
719 subst i (Proj x idx) = Proj (subst i x) idx
738 subst i (Proj x idx) = Proj (subst i x) idx
720 subst i t = t
739 subst i t = t
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.
722substV :: TT n -> TT n -> TT n
744substV :: TT n -> TT n -> TT n
723substV x tm = dropV 0 (instantiate x tm) where
745substV x tm = dropV 0 (instantiate x tm) where
724 dropV i (V x) | x > i = V (x - 1)
746 dropV i (V x) | x > i = V (x - 1)
@@ -728,6 +750,8 @@ substV x tm = dropV 0 (instantiate x tm) where
728 dropV i (Proj x idx) = Proj (dropV i x) idx
750 dropV i (Proj x idx) = Proj (dropV i x) idx
729 dropV i t = t
751 dropV i t = t
753+-- | Replace all non-free de Bruijn references in the given term with references
754+-- to the name of their binding.
731explicitNames :: TT n -> TT n
755explicitNames :: TT n -> TT n
732explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
756explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
733 Bind x b'
757 Bind x b'
@@ -737,6 +761,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
737explicitNames (Proj x idx) = Proj (explicitNames x) idx
761explicitNames (Proj x idx) = Proj (explicitNames x) idx
738explicitNames t = t
762explicitNames t = t
764+-- | Replace references to the given 'Name'-like id with references to
765+-- de Bruijn index 0.
740pToV :: Eq n => n -> TT n -> TT n
766pToV :: Eq n => n -> TT n -> TT n
741pToV n = pToV' n 0
767pToV n = pToV' n 0
742pToV' n i (P _ x _) | n == x = V i
768pToV' n i (P _ x _) | n == x = V i
@@ -766,6 +792,9 @@ pToVs ns tm = pToVs' ns tm 0 where
766 pToVs' [] tm i = tm
792 pToVs' [] tm i = tm
767 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
793 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
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.
769vToP :: TT n -> TT n
798vToP :: TT n -> TT n
770vToP = vToP' [] where
799vToP = vToP' [] where
771 vToP' env (V i) = let (n, b) = (env !! i) in
800 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -775,6 +804,8 @@ vToP = vToP' [] where
775 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
804 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
776 vToP' env t = t
805 vToP' env t = t
807+-- | Replace every non-free reference to the name of a binding in
808+-- the given term with a de Bruijn index.
778finalise :: Eq n => TT n -> TT n
809finalise :: Eq n => TT n -> TT n
779finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
810finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
780finalise (App f a) = App (finalise f) (finalise a)
811finalise (App f a) = App (finalise f) (finalise a)
@@ -789,7 +820,12 @@ pEraseType (App f a) = App (pEraseType f) (pEraseType a)
789pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
820pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
790pEraseType t = t
821pEraseType t = t
823+-- | As 'instantiate', but in addition to replacing @'V' 0@,
824+-- replace references to the given 'Name'-like id.
792−subst :: Eq n => n -> TT n -> TT n -> TT n
825+subst :: Eq n => n {-^ The id to replace -} ->
826+ TT n {-^ The replacement term -} ->
827+ TT n {-^ The term to replace in -} ->
793subst n v tm = instantiate v (pToV n tm)
829subst n v tm = instantiate v (pToV n tm)
795-- If there are no Vs in the term (i.e. in proof state)
831-- If there are no Vs in the term (i.e. in proof state)
@@ -802,19 +838,25 @@ psubst n v tm = s' tm where
802 s' (Proj t idx) = Proj (s' t) idx
838 s' (Proj t idx) = Proj (s' t) idx
841+-- | As 'subst', but takes a list of (name, substitution) pairs instead
842+-- of a single name and substitution
805substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
843substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
806substNames [] t = t
844substNames [] t = t
807substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
845substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
847+-- | Replaces all terms equal (in the sense of @(==)@) to
848+-- the old term with the new term.
809−substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
849+substTerm :: Eq n => TT n {-^ Old term -} ->
850+ TT n {-^ New term -} ->
851+ TT n {-^ template term -}
810substTerm old new = st where
853substTerm old new = st where
811 st t | t == old = new
854 st t | t == old = new
812 st (App f a) = App (st f) (st a)
855 st (App f a) = App (st f) (st a)
813 st (Bind x b sc) = Bind x (fmap st b) (st sc)
856 st (Bind x b sc) = Bind x (fmap st b) (st sc)
816−-- Returns true if V 0 and bound name n do not occur in the term
859+-- | Returns true if V 0 and bound name n do not occur in the term
818noOccurrence :: Eq n => n -> TT n -> Bool
860noOccurrence :: Eq n => n -> TT n -> Bool
819noOccurrence n t = no' 0 t
861noOccurrence n t = no' 0 t
@@ -849,6 +891,8 @@ unApply t = ua [] t where
849 ua args (App f a) = ua (a:args) f
891 ua args (App f a) = ua (a:args) f
850 ua args t = (t, args)
892 ua args t = (t, args)
894+-- | Returns a term representing the application of the first argument
895+-- (a function) to every element of the second argument.
852mkApp :: TT n -> [TT n] -> TT n
896mkApp :: TT n -> [TT n] -> TT n
853mkApp f [] = f
897mkApp f [] = f
854mkApp f (a:as) = mkApp (App f a) as
898mkApp f (a:as) = mkApp (App f a) as
@@ -861,6 +905,10 @@ unList tm = case unApply tm of
861 return $ x:rest
905 return $ x:rest
862 (f, args) -> Nothing
906 (f, args) -> Nothing
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
864forget :: TT Name -> Raw
912forget :: TT Name -> Raw
865forget tm = fe [] tm
913forget tm = fe [] tm
@@ -875,13 +923,21 @@ forget tm = fe [] tm
875 fe env (TType i) = RType
923 fe env (TType i) = RType
876 fe env Erased = RConstant Forgot
924 fe env Erased = RConstant Forgot
926+-- | Introduce a 'Bind' into the given term for each element of the
927+-- given list of (name, binder) pairs.
878bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
928bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
879−bindAll [] t =t
929+bindAll [] t = t
880bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
930bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
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.
882bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
936bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
883bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
937bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
939+-- | Return a list of pairs of the names of the outermost 'Pi'-bound
940+-- variables in the given term, together with their types.
885getArgTys :: TT n -> [(n, TT n)]
941getArgTys :: TT n -> [(n, TT n)]
886getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
942getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc
887getArgTys _ = []
943getArgTys _ = []
@@ -929,7 +985,7 @@ type Type = Term
930type Env = EnvTT Name
986type Env = EnvTT Name
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
933-- this environment
989-- this environment
935newtype WkEnvTT n = Wk (EnvTT n)
991newtype WkEnvTT n = Wk (EnvTT n)
@@ -967,6 +1023,7 @@ instance Show Const where
967 show PtrType = "Ptr"
1023 show PtrType = "Ptr"
968 show VoidType = "Void"
1024 show VoidType = "Void"
1026+showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
970showEnv env t = showEnv' env t False
1027showEnv env t = showEnv' env t False
971showEnvDbg env t = showEnv' env t True
1028showEnvDbg env t = showEnv' env t True
@@ -1004,6 +1061,7 @@ prettyEnv env t = prettyEnv' env t False
1004 prettySe p env Erased debug = text "[_]"
1061 prettySe p env Erased debug = text "[_]"
1005 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1062 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1064+ -- Render a `Binder` and its name
1007 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1065 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1008 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1066 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1009 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
1067 prettySb env n (Pi t) = prettyB env "(" ") ->" n t
@@ -1012,9 +1070,14 @@ prettyEnv env t = prettyEnv' env t False
1012 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1070 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1013 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1071 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1073+ -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1075+ -- e.g. "λx : Int =>" for the Lam case
1015 prettyB env op sc n t debug =
1076 prettyB env op sc n t debug =
1016 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1077 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1079+ -- Like `prettyB`, but handle the bindings that have values in addition
1080+ -- to names and types
1018 prettyBv env op sc n t v debug =
1081 prettyBv env op sc n t v debug =
1019 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1082 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1020 prettySe 10 env v debug <> text sc
1083 prettySe 10 env v debug <> text sc
@@ -1087,9 +1150,12 @@ weakenEnv env = wk (length env - 1) env
1087 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1150 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1088 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1151 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1153+-- | Weaken every term in the environment by the given amount
1090weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1154weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1091weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1155weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1157+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1158+-- them in a canonical order
1093orderPats :: Term -> Term
1159orderPats :: Term -> Term
1094orderPats tm = op [] tm
1160orderPats tm = op [] tm