@@ -1,5 +1,5 @@
11{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}
2−
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33{-| TT is the core language of Idris. The language has:
44
55 * Full dependent types
@@ -366,6 +366,7 @@ data SpecialName = WhereN Int Name Name
366366 | CaseN Name
367367 | ElimN Name
368368 | InstanceCtorN Name
369+ | MetaN Name Name
369370 deriving (Eq, Ord, Data, Typeable)
370371{-!
371372deriving instance Binary SpecialName
@@ -390,6 +391,9 @@ instance Pretty Name OutputAnnotation where
390391 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
391392 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
392393 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
394+ pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $
395+ text $ "##symbol" ++ show i ++ "##"
396+ pretty NErased = annotate (AnnName NErased Nothing Nothing Nothing) $ text "_"
393397
394398instance Pretty [Name] OutputAnnotation where
395399 pretty = encloseSep empty empty comma . map pretty
@@ -400,6 +404,7 @@ instance Show Name where
400404 show (MN _ u) | u == txt "underscore" = "_"
401405 show (MN i s) = "{" ++ str s ++ show i ++ "}"
402406 show (SN s) = show s
407+ show (SymRef i) = "##symbol" ++ show i ++ "##"
403408 show NErased = "_"
404409
405410instance Show SpecialName where
@@ -411,6 +416,7 @@ instance Show SpecialName where
411416 show (CaseN n) = "case block in " ++ show n
412417 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
413418 show (InstanceCtorN n) = "constructor of " ++ show n
419+ show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"
414420
415421-- Show a name in a way decorated for code generation, not human reading
416422showCG :: Name -> String
@@ -427,6 +433,8 @@ showCG (SN s) = showCG' s
427433 showCG' (CaseN c) = showCG c ++ "_case"
428434 showCG' (ElimN sn) = showCG sn ++ "_elim"
429435 showCG' (InstanceCtorN n) = showCG n ++ "_ictor"
436+ showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta
437+showCG (SymRef i) = error "can't do codegen for a symbol reference"
430438showCG NErased = "_"
431439
432440
@@ -861,6 +869,9 @@ instance TermSize (TT Name) where
861869 termsize n (Proj t i) = termsize n t
862870 termsize n _ = 1
863871
872+instance Sized Universe where
873+ size u = 1
874+
864875instance Sized a => Sized (TT a) where
865876 size (P name n trm) = 1 + size name + size n + size trm
866877 size (V v) = 1
@@ -869,6 +880,9 @@ instance Sized a => Sized (TT a) where
869880 size (Constant c) = size c
870881 size Erased = 1
871882 size (TType u) = 1 + size u
883+ size (Proj a _) = 1 + size a
884+ size Impossible = 1
885+ size (UType u) = 1 + size u
872886
873887instance Pretty a o => Pretty (TT a) o where
874888 pretty _ = text "test"
@@ -952,7 +966,7 @@ instantiate e = subst 0 where
952966-- that has been substituted.
953967substV :: TT n -> TT n -> TT n
954968substV x tm = dropV 0 (instantiate x tm) where
955− subst i (P nt x ty) = P nt x (subst i ty)
969+ dropV i (P nt x ty) = P nt x (dropV i ty)
956970 dropV i (V x) | x > i = V (x - 1)
957971 | otherwise = V x
958972 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
@@ -1186,23 +1200,25 @@ forgetEnv env tm = case safeForgetEnv env tm of
11861200safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
11871201safeForgetEnv env (P _ n _) = Just $ Var n
11881202safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
1189− | otherwise = Nothing
1190−safeForgetEnv env (Bind n b sc)
1203+ | otherwise = Nothing
1204+safeForgetEnv env (Bind n b sc)
11911205 = do let n' = uniqueName n env
11921206 b' <- safeForgetEnvB env b
11931207 sc' <- safeForgetEnv (n':env) sc
11941208 Just $ RBind n' b' sc'
1195− where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
1209+ where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
11961210 (safeForgetEnv env v)
1197− safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)
1211+ safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)
11981212 (safeForgetEnv env v)
11991213 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1200− Just $ fmap (\_ -> ty') b
1214+ Just $ fmap (\_ -> ty') b
12011215safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
12021216safeForgetEnv env (Constant c) = Just $ RConstant c
12031217safeForgetEnv env (TType i) = Just RType
12041218safeForgetEnv env (UType u) = Just $ RUType u
12051219safeForgetEnv env Erased = Just $ RConstant Forgot
1220+safeForgetEnv env (Proj tm i) = error "Don't know how to forget a projection"
1221+safeForgetEnv env Impossible = error "Don't know how to forget Impossible"
12061222
12071223-- | Introduce a 'Bind' into the given term for each element of the
12081224-- given list of (name, binder) pairs.
@@ -1255,6 +1271,7 @@ uniqueBinders ns = ubSet (fromList ns) where
12551271 ubSet ns t = t
12561272
12571273
1274+nextName :: Name -> Name
12581275nextName (NS x s) = NS (nextName x) s
12591276nextName (MN i n) = MN (i+1) n
12601277nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
@@ -1274,6 +1291,9 @@ nextName (SN x) = SN (nextName' x)
12741291 nextName' (ElimN n) = ElimN (nextName n)
12751292 nextName' (MethodN n) = MethodN (nextName n)
12761293 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)
1294+ nextName' (MetaN parent meta) = MetaN parent (nextName meta)
1295+nextName NErased = NErased
1296+nextName (SymRef i) = error "Can't generate a name from a symbol reference"
12771297
12781298type Term = TT Name
12791299type Type = Term
@@ -1313,11 +1333,13 @@ instance Show Const where
13131333 show WorldType = "prim__WorldType"
13141334 show StrType = "String"
13151335 show VoidType = "Void"
1336+ show Forgot = "Forgot"
13161337
13171338showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
13181339showEnv env t = showEnv' env t False
13191340showEnvDbg env t = showEnv' env t True
13201341
1342+prettyEnv :: Env -> Term -> Doc OutputAnnotation
13211343prettyEnv env t = prettyEnv' env t False
13221344 where
13231345 prettyEnv' env t dbg = prettySe 10 env t dbg
@@ -1351,14 +1373,18 @@ prettyEnv env t = prettyEnv' env t False
13511373 prettySe p env (Constant c) debug = pretty c
13521374 prettySe p env Erased debug = text "[_]"
13531375 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1376+ prettySe p env Impossible debug = text "Impossible"
1377+ prettySe p env (UType u) debug = text (show u)
13541378
13551379 -- Render a `Binder` and its name
13561380 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
13571381 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1382+ prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t
13581383 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
13591384 prettySb env n (PVar t) = prettyB env "pat" "." n t
13601385 prettySb env n (PVTy t) = prettyB env "pty" "." n t
13611386 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1387+ prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v
13621388 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
13631389
13641390 -- Use `op` and `sc` to delimit `n` (a binding name) and its type
@@ -1404,6 +1430,7 @@ showEnv' env t dbg = se 10 env t where
14041430 sb env n (PVar t) = showb env "pat " ". " n t
14051431 sb env n (PVTy t) = showb env "pty " ". " n t
14061432 sb env n (Let t v) = showbv env "let " " in " n t v
1433+ sb env n (NLet t v) = showbv env "nlet " " in " n t v
14071434 sb env n (Guess t v) = showbv env "?? " " in " n t v
14081435
14091436 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc