git.iko.soy/Idris-dev
on master help sign in
Reflection for SN, plus an SN for meta-stuff
3592edbDavid Raymond Christiansen
libs/prelude/Language/Reflection.idr+71−25
compare with master
unifiedsplit
@@ -11,18 +11,35 @@ import Prelude.Traversable
11
11
12%access public
12%access public
13
13
14+mutual
14−data TTName =
15+ data TTName =
15− ||| A user-provided name
16+ ||| A user-provided name
16− UN String |
17+ UN String |
17− ||| A name in some namespace.
18+ ||| A name in some namespace.
18− |||
19+ |||
19− ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])` represents the name `A.B.foo`
20+ ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])`
21+ ||| represents the name `A.B.foo`
20− NS TTName (List String) |
22+ NS TTName (List String) |
21− ||| Machine-chosen names
23+ ||| Machine-chosen names
22− MN Int String |
24+ MN Int String |
25+ ||| Special names, to make conflicts impossible and language features
26+ ||| predictable
27+ SN SpecialName |
23− ||| Name of something which is never used in scope
28+ ||| Name of something which is never used in scope
24− NErased
29+ NErased
25−%name TTName n, n'
30+ %name TTName n, n'
31+
32+ data SpecialName = WhereN Int TTName TTName
33+ | WithN Int TTName
34+ | InstanceN TTName (List String)
35+ | ParentN TTName String
36+ | MethodN TTName
37+ | CaseN TTName
38+ | ElimN TTName
39+ | InstanceCtorN TTName
40+ | MetaN TTName TTName
41+
42+
26
43
27implicit
44implicit
28userSuppliedName : String -> TTName
45userSuppliedName : String -> TTName
@@ -390,19 +407,48 @@ instance Quotable a Raw => Quotable (List a) Raw where
390 quote [] = `(List.Nil {a=~(quotedTy {a})})
407 quote [] = `(List.Nil {a=~(quotedTy {a})})
391 quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
408 quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
392
409
410+mutual
393−instance Quotable TTName TT where
411+ instance Quotable TTName TT where
394− quotedTy = `(TTName)
412+ quotedTy = `(TTName)
395− quote (UN x) = `(UN ~(quote x))
413+ quote (UN x) = `(UN ~(quote x))
396− quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
414+ quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
397− quote (MN x y) = `(MN ~(quote x) ~(quote y))
415+ quote (MN x y) = `(MN ~(quote x) ~(quote y))
416+ quote (SN sn) = `(SN ~(assert_total $ quote sn))
398− quote NErased = `(NErased)
417+ quote NErased = `(NErased)
399−
418+
400−instance Quotable TTName Raw where
419+ instance Quotable SpecialName TT where
401− quotedTy = `(TTName)
420+ quotedTy = `(SpecialName)
402− quote (UN x) = `(UN ~(quote {t=Raw} x))
421+ quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2))
403− quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))
422+ quote (WithN i n) = `(WithN ~(quote i) ~(quote n))
404− quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))
423+ quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))
405− quote NErased = `(NErased)
424+ quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))
425+ quote (MethodN n) = `(MethodN ~(quote n))
426+ quote (CaseN n) = `(CaseN ~(quote n))
427+ quote (ElimN n) = `(ElimN ~(quote n))
428+ quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))
429+ quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))
430+
431+mutual
432+ instance Quotable TTName Raw where
433+ quotedTy = `(TTName)
434+ quote (UN x) = `(UN ~(quote {t=Raw} x))
435+ quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))
436+ quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))
437+ quote (SN sn) = `(SN ~(assert_total $ quote sn))
438+ quote NErased = `(NErased)
439+
440+ instance Quotable SpecialName Raw where
441+ quotedTy = `(SpecialName)
442+ quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2))
443+ quote (WithN i n) = `(WithN ~(quote i) ~(quote n))
444+ quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))
445+ quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))
446+ quote (MethodN n) = `(MethodN ~(quote n))
447+ quote (CaseN n) = `(CaseN ~(quote n))
448+ quote (ElimN n) = `(ElimN ~(quote n))
449+ quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))
450+ quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))
451+
406
452
407instance Quotable NativeTy TT where
453instance Quotable NativeTy TT where
408 quotedTy = `(NativeTy)
454 quotedTy = `(NativeTy)
src/Idris/Core/Binary.hs+6
@@ -292,6 +292,9 @@ instance Binary SpecialName where
292 WithN x1 x2 -> do putWord8 7
292 WithN x1 x2 -> do putWord8 7
293 put x1
293 put x1
294 put x2
294 put x2
295+ MetaN x1 x2 -> do putWord8 8
296+ put x1
297+ put x2
295 get
298 get
296 = do i <- getWord8
299 = do i <- getWord8
297 case i of
300 case i of
@@ -316,6 +319,9 @@ instance Binary SpecialName where
316 7 -> do x1 <- get
319 7 -> do x1 <- get
317 x2 <- get
320 x2 <- get
318 return (WithN x1 x2)
321 return (WithN x1 x2)
322+ 8 -> do x1 <- get
323+ x2 <- get
324+ return (MetaN x1 x2)
319 _ -> error "Corrupted binary data for SpecialName"
325 _ -> error "Corrupted binary data for SpecialName"
320
326
321
327
src/Idris/Core/DeepSeq.hs+1
@@ -25,6 +25,7 @@ instance NFData SpecialName where
25 rnf (CaseN x1) = rnf x1 `seq` ()
25 rnf (CaseN x1) = rnf x1 `seq` ()
26 rnf (ElimN x1) = rnf x1 `seq` ()
26 rnf (ElimN x1) = rnf x1 `seq` ()
27 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
27 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
28+ rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
28
29
29instance NFData Universe where
30instance NFData Universe where
30 rnf NullType = ()
31 rnf NullType = ()
src/Idris/Core/TT.hs+34−7
@@ -1,5 +1,5 @@
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}
2−
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3{-| TT is the core language of Idris. The language has:
3{-| TT is the core language of Idris. The language has:
4
4
5 * Full dependent types
5 * Full dependent types
@@ -366,6 +366,7 @@ data SpecialName = WhereN Int Name Name
366 | CaseN Name
366 | CaseN Name
367 | ElimN Name
367 | ElimN Name
368 | InstanceCtorN Name
368 | InstanceCtorN Name
369+ | MetaN Name Name
369 deriving (Eq, Ord, Data, Typeable)
370 deriving (Eq, Ord, Data, Typeable)
370{-!
371{-!
371deriving instance Binary SpecialName
372deriving instance Binary SpecialName
@@ -390,6 +391,9 @@ instance Pretty Name OutputAnnotation where
390 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
391 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
391 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
392 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
392 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
393 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 "_"
393
397
394instance Pretty [Name] OutputAnnotation where
398instance Pretty [Name] OutputAnnotation where
395 pretty = encloseSep empty empty comma . map pretty
399 pretty = encloseSep empty empty comma . map pretty
@@ -400,6 +404,7 @@ instance Show Name where
400 show (MN _ u) | u == txt "underscore" = "_"
404 show (MN _ u) | u == txt "underscore" = "_"
401 show (MN i s) = "{" ++ str s ++ show i ++ "}"
405 show (MN i s) = "{" ++ str s ++ show i ++ "}"
402 show (SN s) = show s
406 show (SN s) = show s
407+ show (SymRef i) = "##symbol" ++ show i ++ "##"
403 show NErased = "_"
408 show NErased = "_"
404
409
405instance Show SpecialName where
410instance Show SpecialName where
@@ -411,6 +416,7 @@ instance Show SpecialName where
411 show (CaseN n) = "case block in " ++ show n
416 show (CaseN n) = "case block in " ++ show n
412 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
417 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
413 show (InstanceCtorN n) = "constructor of " ++ show n
418 show (InstanceCtorN n) = "constructor of " ++ show n
419+ show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"
414
420
415-- Show a name in a way decorated for code generation, not human reading
421-- Show a name in a way decorated for code generation, not human reading
416showCG :: Name -> String
422showCG :: Name -> String
@@ -427,6 +433,8 @@ showCG (SN s) = showCG' s
427 showCG' (CaseN c) = showCG c ++ "_case"
433 showCG' (CaseN c) = showCG c ++ "_case"
428 showCG' (ElimN sn) = showCG sn ++ "_elim"
434 showCG' (ElimN sn) = showCG sn ++ "_elim"
429 showCG' (InstanceCtorN n) = showCG n ++ "_ictor"
435 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"
430showCG NErased = "_"
438showCG NErased = "_"
431
439
432
440
@@ -861,6 +869,9 @@ instance TermSize (TT Name) where
861 termsize n (Proj t i) = termsize n t
869 termsize n (Proj t i) = termsize n t
862 termsize n _ = 1
870 termsize n _ = 1
863
871
872+instance Sized Universe where
873+ size u = 1
874+
864instance Sized a => Sized (TT a) where
875instance Sized a => Sized (TT a) where
865 size (P name n trm) = 1 + size name + size n + size trm
876 size (P name n trm) = 1 + size name + size n + size trm
866 size (V v) = 1
877 size (V v) = 1
@@ -869,6 +880,9 @@ instance Sized a => Sized (TT a) where
869 size (Constant c) = size c
880 size (Constant c) = size c
870 size Erased = 1
881 size Erased = 1
871 size (TType u) = 1 + size u
882 size (TType u) = 1 + size u
883+ size (Proj a _) = 1 + size a
884+ size Impossible = 1
885+ size (UType u) = 1 + size u
872
886
873instance Pretty a o => Pretty (TT a) o where
887instance Pretty a o => Pretty (TT a) o where
874 pretty _ = text "test"
888 pretty _ = text "test"
@@ -952,7 +966,7 @@ instantiate e = subst 0 where
952-- that has been substituted.
966-- that has been substituted.
953substV :: TT n -> TT n -> TT n
967substV :: TT n -> TT n -> TT n
954substV x tm = dropV 0 (instantiate x tm) where
968substV 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)
956 dropV i (V x) | x > i = V (x - 1)
970 dropV i (V x) | x > i = V (x - 1)
957 | otherwise = V x
971 | otherwise = V x
958 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
972 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
1186safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
1200safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
1187safeForgetEnv env (P _ n _) = Just $ Var n
1201safeForgetEnv env (P _ n _) = Just $ Var n
1188safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
1202safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
1189− | otherwise = Nothing
1203+ | otherwise = Nothing
1190−safeForgetEnv env (Bind n b sc)
1204+safeForgetEnv env (Bind n b sc)
1191 = do let n' = uniqueName n env
1205 = do let n' = uniqueName n env
1192 b' <- safeForgetEnvB env b
1206 b' <- safeForgetEnvB env b
1193 sc' <- safeForgetEnv (n':env) sc
1207 sc' <- safeForgetEnv (n':env) sc
1194 Just $ RBind n' b' sc'
1208 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)
1196 (safeForgetEnv env v)
1210 (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)
1198 (safeForgetEnv env v)
1212 (safeForgetEnv env v)
1199 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1213 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1200− Just $ fmap (\_ -> ty') b
1214+ Just $ fmap (\_ -> ty') b
1201safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1215safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1202safeForgetEnv env (Constant c) = Just $ RConstant c
1216safeForgetEnv env (Constant c) = Just $ RConstant c
1203safeForgetEnv env (TType i) = Just RType
1217safeForgetEnv env (TType i) = Just RType
1204safeForgetEnv env (UType u) = Just $ RUType u
1218safeForgetEnv env (UType u) = Just $ RUType u
1205safeForgetEnv env Erased = Just $ RConstant Forgot
1219safeForgetEnv 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"
1206
1222
1207-- | Introduce a 'Bind' into the given term for each element of the
1223-- | Introduce a 'Bind' into the given term for each element of the
1208-- given list of (name, binder) pairs.
1224-- given list of (name, binder) pairs.
@@ -1255,6 +1271,7 @@ uniqueBinders ns = ubSet (fromList ns) where
1255 ubSet ns t = t
1271 ubSet ns t = t
1256
1272
1257
1273
1274+nextName :: Name -> Name
1258nextName (NS x s) = NS (nextName x) s
1275nextName (NS x s) = NS (nextName x) s
1259nextName (MN i n) = MN (i+1) n
1276nextName (MN i n) = MN (i+1) n
1260nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
1277nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
@@ -1274,6 +1291,9 @@ nextName (SN x) = SN (nextName' x)
1274 nextName' (ElimN n) = ElimN (nextName n)
1291 nextName' (ElimN n) = ElimN (nextName n)
1275 nextName' (MethodN n) = MethodN (nextName n)
1292 nextName' (MethodN n) = MethodN (nextName n)
1276 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)
1293 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"
1277
1297
1278type Term = TT Name
1298type Term = TT Name
1279type Type = Term
1299type Type = Term
@@ -1313,11 +1333,13 @@ instance Show Const where
1313 show WorldType = "prim__WorldType"
1333 show WorldType = "prim__WorldType"
1314 show StrType = "String"
1334 show StrType = "String"
1315 show VoidType = "Void"
1335 show VoidType = "Void"
1336+ show Forgot = "Forgot"
1316
1337
1317showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
1338showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
1318showEnv env t = showEnv' env t False
1339showEnv env t = showEnv' env t False
1319showEnvDbg env t = showEnv' env t True
1340showEnvDbg env t = showEnv' env t True
1320
1341
1342+prettyEnv :: Env -> Term -> Doc OutputAnnotation
1321prettyEnv env t = prettyEnv' env t False
1343prettyEnv env t = prettyEnv' env t False
1322 where
1344 where
1323 prettyEnv' env t dbg = prettySe 10 env t dbg
1345 prettyEnv' env t dbg = prettySe 10 env t dbg
@@ -1351,14 +1373,18 @@ prettyEnv env t = prettyEnv' env t False
1351 prettySe p env (Constant c) debug = pretty c
1373 prettySe p env (Constant c) debug = pretty c
1352 prettySe p env Erased debug = text "[_]"
1374 prettySe p env Erased debug = text "[_]"
1353 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1375 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)
1354
1378
1355 -- Render a `Binder` and its name
1379 -- Render a `Binder` and its name
1356 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1380 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1357 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1381 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1382+ prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t
1358 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
1383 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
1359 prettySb env n (PVar t) = prettyB env "pat" "." n t
1384 prettySb env n (PVar t) = prettyB env "pat" "." n t
1360 prettySb env n (PVTy t) = prettyB env "pty" "." n t
1385 prettySb env n (PVTy t) = prettyB env "pty" "." n t
1361 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1386 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
1362 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1388 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1363
1389
1364 -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1390 -- 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
1404 sb env n (PVar t) = showb env "pat " ". " n t
1430 sb env n (PVar t) = showb env "pat " ". " n t
1405 sb env n (PVTy t) = showb env "pty " ". " n t
1431 sb env n (PVTy t) = showb env "pty " ". " n t
1406 sb env n (Let t v) = showbv env "let " " in " n t v
1432 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
1407 sb env n (Guess t v) = showbv env "?? " " in " n t v
1434 sb env n (Guess t v) = showbv env "?? " " in " n t v
1408
1435
1409 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
1436 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
src/Idris/Reflection.hs+58
@@ -5,6 +5,7 @@ quoters and unquoters along with some supporting datatypes.
5{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
5{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
6module Idris.Reflection where
6module Idris.Reflection where
7
7
8+import Control.Applicative ((<$>), (<*>), pure)
8import Control.Monad (liftM, liftM2)
9import Control.Monad (liftM, liftM2)
9import Data.Maybe (catMaybes)
10import Data.Maybe (catMaybes)
10import Data.List ((\\))
11import Data.List ((\\))
@@ -193,6 +194,39 @@ reifyTTNameApp t [n, ns]
193 return $ sNS n' ns'
194 return $ sNS n' ns'
194reifyTTNameApp t [Constant (I i), Constant (Str n)]
195reifyTTNameApp t [Constant (I i), Constant (Str n)]
195 | t == reflm "MN" = return $ sMN i n
196 | t == reflm "MN" = return $ sMN i n
197+reifyTTNameApp t [sn]
198+ | t == reflm "SN"
199+ , (P _ f _, args) <- unApply sn = SN <$> reifySN f args
200+ where reifySN :: Name -> [Term] -> ElabD SpecialName
201+ reifySN t [Constant (I i), n1, n2]
202+ | t == reflm "WhereN" = WhereN i <$> reifyTTName n1 <*> reifyTTName n2
203+ reifySN t [Constant (I i), n]
204+ | t == reflm "WithN" = WithN i <$> reifyTTName n
205+ reifySN t [n, ss]
206+ | t == reflm "InstanceN" =
207+ case unList ss of
208+ Nothing -> fail "Can't reify InstanceN strings"
209+ Just ss' -> InstanceN <$> reifyTTName n <*>
210+ pure [T.pack s | Constant (Str s) <- ss']
211+ reifySN t [n, Constant (Str s)]
212+ | t == reflm "ParentN" =
213+ ParentN <$> reifyTTName n <*> pure (T.pack s)
214+ reifySN t [n]
215+ | t == reflm "MethodN" =
216+ MethodN <$> reifyTTName n
217+ reifySN t [n]
218+ | t == reflm "CaseN" =
219+ CaseN <$> reifyTTName n
220+ reifySN t [n]
221+ | t == reflm "ElimN" =
222+ ElimN <$> reifyTTName n
223+ reifySN t [n]
224+ | t == reflm "InstanceCtorN" =
225+ InstanceCtorN <$> reifyTTName n
226+ reifySN t [n1, n2]
227+ | t == reflm "MetaN" =
228+ MetaN <$> reifyTTName n1 <*> reifyTTName n2
229+ reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
196reifyTTNameApp t []
230reifyTTNameApp t []
197 | t == reflm "NErased" = return NErased
231 | t == reflm "NErased" = return NErased
198reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
232reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
@@ -600,6 +634,30 @@ reflectName (MN i n)
600reflectName (NErased) = Var (reflm "NErased")
634reflectName (NErased) = Var (reflm "NErased")
601reflectName n = Var (reflm "NErased") -- special name, not yet implemented
635reflectName n = Var (reflm "NErased") -- special name, not yet implemented
602
636
637+reflectSpecialName :: SpecialName -> Raw
638+reflectSpecialName (WhereN i n1 n2) =
639+ reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
640+reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
641+ , reflectName n
642+ ]
643+reflectSpecialName (InstanceN inst ss) =
644+ reflCall "InstanceN" [ reflectName inst
645+ , mkList (RConstant StrType) $
646+ map (RConstant . Str . T.unpack) ss
647+ ]
648+reflectSpecialName (ParentN n s) =
649+ reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
650+reflectSpecialName (MethodN n) =
651+ reflCall "MethodN" [reflectName n]
652+reflectSpecialName (CaseN n) =
653+ reflCall "CaseN" [reflectName n]
654+reflectSpecialName (ElimN n) =
655+ reflCall "ElimN" [reflectName n]
656+reflectSpecialName (InstanceCtorN n) =
657+ reflCall "InstanceCtorN" [reflectName n]
658+reflectSpecialName (MetaN parent meta) =
659+ reflCall "MetaN" [reflectName parent, reflectName meta]
660+
603-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
661-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
604-- MNs corresponding to will care about the string but not the number. All
662-- MNs corresponding to will care about the string but not the number. All
605-- others become _.
663-- others become _.