git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2149 from david-christiansen/wip/tactical
1dfbb72David Christiansen
libs/prelude/Language/Reflection/Elab.idrnew file+149
compare with master
unifiedsplit
@@ -0,0 +1,149 @@
1+module Language.Reflection.Elab
2+
3+import Builtins
4+import Prelude.Applicative
5+import Prelude.Functor
6+import Prelude.List
7+import Prelude.Maybe
8+import Prelude.Monad
9+import Language.Reflection
10+
11+data Arg : Type where
12+ Explicit : TTName -> Raw -> Arg
13+ Implicit : TTName -> Raw -> Arg
14+ Constraint : TTName -> Raw -> Arg
15+
16+data TyDecl : Type where
17+ Declare : TTName -> List Arg -> Raw -> TyDecl
18+
19+data FunClause : Type where
20+ MkFunClause : (lhs, rhs : Raw) -> FunClause
21+ MkImpossibleClause : (lhs : Raw) -> FunClause
22+
23+data FunDefn : Type where
24+ DefineFun : TTName -> List FunClause -> FunDefn
25+
26+abstract
27+data Elab : Type -> Type where
28+ -- obligatory control stuff
29+ prim__PureElab : a -> Elab a
30+ prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
31+
32+ prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
33+ prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
34+
35+ prim__Env : Elab (List (TTName, Binder TT))
36+ prim__Goal : Elab (TTName, TT)
37+ prim__Holes : Elab (List TTName)
38+ prim__Guess : Elab (Maybe TT)
39+
40+ prim__SourceLocation : Elab SourceLocation
41+
42+ prim__Forget : TT -> Elab Raw
43+
44+ prim__Gensym : String -> Elab TTName
45+
46+ prim__Solve : Elab ()
47+ prim__Fill : Raw -> Elab ()
48+ prim__Focus : TTName -> Elab ()
49+ prim__Unfocus : TTName -> Elab ()
50+ prim__Attack : Elab ()
51+
52+ prim__Rewrite : Raw -> Elab ()
53+
54+ prim__Claim : TTName -> Raw -> Elab ()
55+ prim__Intro : Maybe TTName -> Elab ()
56+
57+ prim__DeclareType : TyDecl -> Elab ()
58+ prim__DefineFunction : FunDefn -> Elab ()
59+
60+ prim__Debug : {a : Type} -> Maybe String -> Elab a
61+
62+
63+-------------
64+-- Public API
65+-------------
66+%access public
67+
68+instance Functor Elab where
69+ map f t = prim__BindElab t (\x => prim__PureElab (f x))
70+
71+instance Applicative Elab where
72+ pure x = prim__PureElab x
73+ f <*> x = prim__BindElab f $ \g =>
74+ prim__BindElab x $ \y =>
75+ prim__PureElab $ g y
76+
77+instance Alternative Elab where
78+ empty = prim__Fail [TextPart "empty"]
79+ x <|> y = prim__Try x y
80+
81+instance Monad Elab where
82+ x >>= f = prim__BindElab x f
83+
84+fail : List ErrorReportPart -> Elab a
85+fail err = prim__Fail err
86+
87+getEnv : Elab (List (TTName, Binder TT))
88+getEnv = prim__Env
89+
90+getGoal : Elab (TTName, TT)
91+getGoal = prim__Goal
92+
93+getHoles : Elab (List TTName)
94+getHoles = prim__Holes
95+
96+getGuess : Elab (Maybe TT)
97+getGuess = prim__Guess
98+
99+forgetTypes : TT -> Elab Raw
100+forgetTypes tt = prim__Forget tt
101+
102+gensym : (hint : String) -> Elab TTName
103+gensym hint = prim__Gensym hint
104+
105+solve : Elab ()
106+solve = prim__Solve
107+
108+fill : Raw -> Elab ()
109+fill tm = prim__Fill tm
110+
111+focus : (hole : TTName) -> Elab ()
112+focus hole = prim__Focus hole
113+
114+unfocus : TTName -> Elab ()
115+unfocus hole = prim__Unfocus hole
116+
117+attack : Elab ()
118+attack = prim__Attack
119+
120+claim : TTName -> Raw -> Elab ()
121+claim n ty = prim__Claim n ty
122+
123+intro : Maybe TTName -> Elab ()
124+intro n = prim__Intro n
125+
126+||| Find out the present source context for the tactic script
127+getSourceLocation : Elab SourceLocation
128+getSourceLocation = prim__SourceLocation
129+
130+||| Attempt to solve the current goal with the source code location
131+sourceLocation : Elab ()
132+sourceLocation = do loc <- getSourceLocation
133+ fill (quote loc)
134+ solve
135+
136+rewriteWith : Raw -> Elab ()
137+rewriteWith rule = prim__Rewrite rule
138+
139+declareType : TyDecl -> Elab ()
140+declareType decl = prim__DeclareType decl
141+
142+defineFunction : FunDefn -> Elab ()
143+defineFunction defun = prim__DefineFunction defun
144+
145+debug : Elab a
146+debug = prim__Debug Nothing
147+
148+debugMessage : String -> Elab a
149+debugMessage msg = prim__Debug (Just msg)
libs/prelude/Language/Reflection/Tactical.idrdeleted−138
@@ -1,138 +0,0 @@
1−module Language.Reflection.Tactical
2−
3−import Builtins
4−import Prelude.Applicative
5−import Prelude.Functor
6−import Prelude.List
7−import Prelude.Maybe
8−import Prelude.Monad
9−import Language.Reflection
10−
11−data Arg : Type where
12− Explicit : TTName -> Raw -> Arg
13− Implicit : TTName -> Raw -> Arg
14− Constraint : TTName -> Raw -> Arg
15−
16−data TyDecl : Type where
17− Declare : TTName -> List Arg -> Raw -> TyDecl
18−
19−abstract
20−data Tactical : Type -> Type where
21− -- obligatory control stuff
22− prim__PureTactical : a -> Tactical a
23− prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
24−
25− prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
26− prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a
27−
28− prim__Env : Tactical (List (TTName, Binder TT))
29− prim__Goal : Tactical (TTName, TT)
30− prim__Holes : Tactical (List TTName)
31− prim__Guess : Tactical (Maybe TT)
32−
33− prim__SourceLocation : Tactical SourceLocation
34−
35− prim__Forget : TT -> Tactical Raw
36−
37− prim__Gensym : String -> Tactical TTName
38−
39− prim__Solve : Tactical ()
40− prim__Fill : Raw -> Tactical ()
41− prim__Focus : TTName -> Tactical ()
42− prim__Unfocus : TTName -> Tactical ()
43− prim__Attack : Tactical ()
44−
45− prim__Rewrite : Raw -> Tactical ()
46−
47− prim__Claim : TTName -> Raw -> Tactical ()
48− prim__Intro : Maybe TTName -> Tactical ()
49−
50− prim__DeclareType : TyDecl -> Tactical ()
51−
52− prim__Debug : {a : Type} -> Maybe String -> Tactical a
53−
54−
55−-------------
56−-- Public API
57−-------------
58−%access public
59−
60−instance Functor Tactical where
61− map f t = prim__BindTactical t (\x => prim__PureTactical (f x))
62−
63−instance Applicative Tactical where
64− pure x = prim__PureTactical x
65− f <*> x = prim__BindTactical f $ \g =>
66− prim__BindTactical x $ \y =>
67− prim__PureTactical $ g y
68−
69−instance Alternative Tactical where
70− empty = prim__Fail [TextPart "empty"]
71− x <|> y = prim__Try x y
72−
73−instance Monad Tactical where
74− x >>= f = prim__BindTactical x f
75−
76−fail : List ErrorReportPart -> Tactical a
77−fail err = prim__Fail err
78−
79−getEnv : Tactical (List (TTName, Binder TT))
80−getEnv = prim__Env
81−
82−getGoal : Tactical (TTName, TT)
83−getGoal = prim__Goal
84−
85−getHoles : Tactical (List TTName)
86−getHoles = prim__Holes
87−
88−getGuess : Tactical (Maybe TT)
89−getGuess = prim__Guess
90−
91−forgetTypes : TT -> Tactical Raw
92−forgetTypes tt = prim__Forget tt
93−
94−gensym : (hint : String) -> Tactical TTName
95−gensym hint = prim__Gensym hint
96−
97−solve : Tactical ()
98−solve = prim__Solve
99−
100−fill : Raw -> Tactical ()
101−fill tm = prim__Fill tm
102−
103−focus : (hole : TTName) -> Tactical ()
104−focus hole = prim__Focus hole
105−
106−unfocus : TTName -> Tactical ()
107−unfocus hole = prim__Unfocus hole
108−
109−attack : Tactical ()
110−attack = prim__Attack
111−
112−claim : TTName -> Raw -> Tactical ()
113−claim n ty = prim__Claim n ty
114−
115−intro : Maybe TTName -> Tactical ()
116−intro n = prim__Intro n
117−
118−||| Find out the present source context for the tactic script
119−getSourceLocation : Tactical SourceLocation
120−getSourceLocation = prim__SourceLocation
121−
122−||| Attempt to solve the current goal with the source code location
123−sourceLocation : Tactical ()
124−sourceLocation = do loc <- getSourceLocation
125− fill (quote loc)
126− solve
127−
128−rewriteWith : Raw -> Tactical ()
129−rewriteWith rule = prim__Rewrite rule
130−
131−declareType : TyDecl -> Tactical ()
132−declareType decl = prim__DeclareType decl
133−
134−debug : Tactical a
135−debug = prim__Debug Nothing
136−
137−debugMessage : String -> Tactical a
138−debugMessage msg = prim__Debug (Just msg)
libs/prelude/prelude.ipkg+1−1
@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12
12
13− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,
13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
14
14
15 Decidable.Equality
15 Decidable.Equality
16
16
src/Idris/AbsSyntax.hs+4−4
@@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1014− en (PRunTactics fc tm) = PRunTactics fc (en tm)
1014+ en (PRunElab fc tm) = PRunElab fc (en tm)
1015 en t = t
1015 en t = t
1016
1016
1017 nselem x [] = False
1017 nselem x [] = False
@@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1485 imps top env (PHidden tm) = imps False env tm
1485 imps top env (PHidden tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1487 imps top env (PNoImplicits tm) = imps False env tm
1487 imps top env (PNoImplicits tm) = imps False env tm
1488− imps top env (PRunTactics fc tm) = imps False env tm
1488+ imps top env (PRunElab fc tm) = imps False env tm
1489 imps top env _ = return ()
1489 imps top env _ = return ()
1490
1490
1491 pibind using [] sc = sc
1491 pibind using [] sc = sc
@@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1613 (fmap (ai True env ds) g)
1613 (fmap (ai True env ds) g)
1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1615− ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
1615+ ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)
1616 ai qq env ds tm = tm
1616 ai qq env ds tm = tm
1617
1617
1618 handleErr (Left err) = PElabError err
1618 handleErr (Left err) = PElabError err
@@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2152− mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
2152+ mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)
2153 mkUniq t = return t
2153 mkUniq t = return t
src/Idris/AbsSyntaxTree.hs+20−7
@@ -645,11 +645,16 @@ deriving instance Binary PDecl'
645deriving instance NFData PDecl'
645deriving instance NFData PDecl'
646!-}
646!-}
647
647
648+-- | A set of instructions for things that need to happen in IState
649+-- after a term elaboration when there's been reflected elaboration.
650+data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
651+ | RClausesInstrs Name [([Name], Term, Term)]
652+
648−-- For elaborator state
653+-- | For elaborator state
649data EState = EState {
654data EState = EState {
650 case_decls :: [PDecl],
655 case_decls :: [PDecl],
651 delayed_elab :: [Elab' EState ()],
656 delayed_elab :: [Elab' EState ()],
652− new_tyDecls :: [(Name, FC, [PArg], Type)]
657+ new_tyDecls :: [RDeclInstructions]
653 }
658 }
654
659
655initEState :: EState
660initEState :: EState
@@ -821,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
821 | PNoImplicits PTerm -- ^ never run implicit converions on the term
826 | PNoImplicits PTerm -- ^ never run implicit converions on the term
822 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
823 | PUnquote PTerm -- ^ ~Term
828 | PUnquote PTerm -- ^ ~Term
824− | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script
829+ | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
825 deriving (Eq, Data, Typeable)
830 deriving (Eq, Data, Typeable)
826
831
827
832
@@ -1428,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1428 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1429 prettySe p bnd (PLam fc n ty sc) =
1434 prettySe p bnd (PLam fc n ty sc) =
1430 bracket p startPrec . group . align . hang 2 $
1435 bracket p startPrec . group . align . hang 2 $
1431− text "\\" <> bindingOf n False <+> text "=>" <$>
1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1432 prettySe startPrec ((n, False):bnd) sc
1437 prettySe startPrec ((n, False):bnd) sc
1433 prettySe p bnd (PLet fc n ty v sc) =
1438 prettySe p bnd (PLet fc n ty v sc) =
1434 bracket p startPrec . group . align $
1439 bracket p startPrec . group . align $
1435− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1440+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1436 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1437 prettySe p bnd (PPi (Exp l s _) n ty sc)
1442 prettySe p bnd (PPi (Exp l s _) n ty sc)
1438 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1439 bracket p startPrec . group $
1444 bracket p startPrec . group $
1440− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1445+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1441 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1442 | otherwise =
1447 | otherwise =
1443 bracket p startPrec . group $
1448 bracket p startPrec . group $
@@ -1450,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1450 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1451 | ppopt_impl ppo =
1456 | ppopt_impl ppo =
1452 bracket p startPrec $
1457 bracket p startPrec $
1453− lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1458+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1454 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1455 | otherwise = prettySe startPrec ((n, True):bnd) sc
1460 | otherwise = prettySe startPrec ((n, True):bnd) sc
1456 where
1461 where
@@ -1607,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1607
1612
1608 prettySe p bnd _ = text "missing pretty-printer for term"
1613 prettySe p bnd _ = text "missing pretty-printer for term"
1609
1614
1615+ prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1616+ prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1617+ where display (UN n) = T.unpack n
1618+ display (MN _ n) = T.unpack n
1619+ -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1620+ display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1621+ display n = show n
1622+
1610 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1611 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1612 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
src/Idris/Core/TT.hs+4−3
@@ -117,9 +117,6 @@ data ErrorReportPart = TextPart String
117 deriving (Show, Eq, Data, Typeable)
117 deriving (Show, Eq, Data, Typeable)
118
118
119
119
120−-- Please remember to keep Err synchronised with
121−-- Language.Reflection.Errors.Err in the stdlib!
122−
123data Provenance = ExpectedType
120data Provenance = ExpectedType
124 | TooManyArgs Term
121 | TooManyArgs Term
125 | InferredVal
122 | InferredVal
@@ -131,6 +128,10 @@ deriving instance NFData Err
131deriving instance Binary Err
128deriving instance Binary Err
132!-}
129!-}
133
130
131+
132+-- NB: Please remember to keep Err synchronised with
133+-- Language.Reflection.Errors.Err in the stdlib!
134+
134-- | Idris errors. Used as exceptions in the compiler, but reported to users
135-- | Idris errors. Used as exceptions in the compiler, but reported to users
135-- if they reach the top level.
136-- if they reach the top level.
136data Err' t
137data Err' t
src/Idris/DSL.hs+2−2
@@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)
108 block b _ = PElabError (Msg "Invalid statement in do block")
108 block b _ = PElabError (Msg "Invalid statement in do block")
109
109
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
111−expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm
111+expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm
112expandDo dsl t = t
112expandDo dsl t = t
113
113
114-- | Replace DSL-bound variable in a term
114-- | Replace DSL-bound variable in a term
@@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
195 db' (PDPair fc p l t r) = do l' <- db' l
195 db' (PDPair fc p l t r) = do l' <- db' l
196 r' <- db' r
196 r' <- db' r
197 return (PDPair fc p l' t r')
197 return (PDPair fc p l' t r')
198− db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)
198+ db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)
199 db' t = return t
199 db' t = return t
200
200
201 dbArg a = do t' <- db' (getTm a)
201 dbArg a = do t' <- db' (getTm a)
src/Idris/DeepSeq.hs+1−1
@@ -243,7 +243,7 @@ instance NFData PTerm where
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
246− rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
246+ rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
247
247
248instance (NFData t) => NFData (PTactic' t) where
248instance (NFData t) => NFData (PTactic' t) where
249 rnf (Intro x1) = rnf x1 `seq` ()
249 rnf (Intro x1) = rnf x1 `seq` ()
src/Idris/ElabQuasiquote.hs+2−2
@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
172 extractUnquotes (n-1) tm
172 extractUnquotes (n-1) tm
173−extractUnquotes n (PRunTactics fc tm)
173+extractUnquotes n (PRunElab fc tm)
174− = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm
174+ = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm
175extractUnquotes n x = return (x, []) -- no subterms!
175extractUnquotes n x = return (x, []) -- no subterms!
176
176
177
177
src/Idris/ElabTerm.hs+71−863
@@ -1,4 +1,4 @@
1−{-# LANGUAGE PatternGuards, ViewPatterns #-}
1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.ElabTerm where
3module Idris.ElabTerm where
4
4
@@ -10,6 +10,7 @@ import Idris.Error
10import Idris.ProofSearch
10import Idris.ProofSearch
11import Idris.Output (pshow)
11import Idris.Output (pshow)
12
12
13+import Idris.Core.CaseTree (SC, SC'(STerm))
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
15import Idris.Core.TT
15import Idris.Core.Evaluate
16import Idris.Core.Evaluate
@@ -35,6 +36,7 @@ import Debug.Trace
35data ElabMode = ETyDecl | ELHS | ERHS
36data ElabMode = ETyDecl | ELHS | ERHS
36 deriving Eq
37 deriving Eq
37
38
39+
38data ElabResult =
40data ElabResult =
39 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
41 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
40 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
42 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -43,23 +45,28 @@ data ElabResult =
43 -- ^ Deferred declarations as the meaning of case blocks
45 -- ^ Deferred declarations as the meaning of case blocks
44 , resultContext :: Context
46 , resultContext :: Context
45 -- ^ The potentially extended context from new definitions
47 -- ^ The potentially extended context from new definitions
46− , resultTyDecls :: [(Name, FC, [PArg], Type)]
48+ , resultTyDecls :: [RDeclInstructions]
47 -- ^ Meta-info about the new type declarations
49 -- ^ Meta-info about the new type declarations
48 }
50 }
49
51
50−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()
52+processTacticDecls :: [RDeclInstructions] -> Idris ()
51processTacticDecls info =
53processTacticDecls info =
52− forM_ info $ \(n, fc, impls, ty) ->
54+ forM_ info $ \case
55+ RTyDeclInstrs n fc impls ty ->
53− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
56+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
54− logLvl 3 $ " It has impls " ++ show impls
57+ logLvl 3 $ " It has impls " ++ show impls
55− updateIState $ \i -> i { idris_implicits =
58+ updateIState $ \i -> i { idris_implicits =
56− addDef n impls (idris_implicits i) }
59+ addDef n impls (idris_implicits i) }
57− addIBC (IBCImp n)
60+ addIBC (IBCImp n)
58− ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
61+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
59− addIBC (IBCDef n)
62+ addIBC (IBCDef n)
60− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
63+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
61− addDeferred ds'
64+ addDeferred ds'
62−
65+ RClausesInstrs n cs ->
66+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
67+ solveDeferred n
68+ updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses
69+ addIBC (IBCDef n)
63
70
64-- Using the elaborator, convert a term in raw syntax to a fully
71-- Using the elaborator, convert a term in raw syntax to a fully
65-- elaborated, typechecked term.
72-- elaborated, typechecked term.
@@ -213,7 +220,7 @@ goal_polymorphic =
213
220
214-- | Returns the set of declarations we need to add to complete the
221-- | Returns the set of declarations we need to add to complete the
215-- definition (most likely case blocks to elaborate) as well as
222-- definition (most likely case blocks to elaborate) as well as
216−-- declarations resulting from user tactic scripts (%runTactics)
223+-- declarations resulting from user tactic scripts (%runElab)
217elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
218 ElabD ()
225 ElabD ()
219elab ist info emode opts fn tm
226elab ist info emode opts fn tm
@@ -1100,11 +1107,11 @@ elab ist info emode opts fn tm
1100 delayElab $ do focus h
1107 delayElab $ do focus h
1101 dotterm
1108 dotterm
1102 elab' ina fc t
1109 elab' ina fc t
1103− elab' ina fc (PRunTactics fc' tm) =
1110+ elab' ina fc (PRunElab fc' tm) =
1104 do attack
1111 do attack
1105 n <- getNameFrom (sMN 0 "tacticScript")
1112 n <- getNameFrom (sMN 0 "tacticScript")
1106 n' <- getNameFrom (sMN 0 "tacticExpr")
1113 n' <- getNameFrom (sMN 0 "tacticExpr")
1107− let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1114+ let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy)
1108 claim n scriptTy
1115 claim n scriptTy
1109 movelast n
1116 movelast n
1110 letbind n' scriptTy (Var n)
1117 letbind n' scriptTy (Var n)
@@ -1582,8 +1589,6 @@ case_ ind autoSolve ist fn tm = do
1582 else casetac (forget val)
1589 else casetac (forget val)
1583 when autoSolve solveAll
1590 when autoSolve solveAll
1584
1591
1585−tacN :: String -> Name
1586−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1587
1592
1588runTactical :: FC -> Env -> Term -> ElabD ()
1593runTactical :: FC -> Env -> Term -> ElabD ()
1589runTactical fc env tm = do tm' <- eval tm
1594runTactical fc env tm = do tm' <- eval tm
@@ -1595,6 +1600,45 @@ runTactical fc env tm = do tm' <- eval tm
1595
1600
1596 returnUnit = fmap fst $ get_type_val (Var unitCon)
1601 returnUnit = fmap fst $ get_type_val (Var unitCon)
1597
1602
1603+ patvars :: [Name] -> Term -> ([Name], Term)
1604+ patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
1605+ patvars ns tm = (ns, tm)
1606+
1607+ pullVars :: (Term, Term) -> ([Name], Term, Term)
1608+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1609+
1610+ defineFunction :: RFunDefn -> ElabD ()
1611+ defineFunction (RDefineFun n clauses) =
1612+ do ctxt <- get_context
1613+ ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
1614+ let info = CaseInfo True True False -- TODO document and figure out
1615+ clauses' <- forM clauses (\case
1616+ RMkFunClause lhs rhs ->
1617+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1618+ rhs' <- fmap fst . lift $ check ctxt [] rhs
1619+ return $ Right (lhs', rhs')
1620+ RMkImpossibleClause lhs ->
1621+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1622+ return $ Left lhs')
1623+ let clauses'' = map (\case Right c -> pullVars c
1624+ Left lhs -> let (ns, lhs') = patvars [] lhs'
1625+ in (ns, lhs', Impossible))
1626+ clauses'
1627+ set_context $
1628+ addCasedef n (const [])
1629+ info False (STerm Erased)
1630+ True False -- TODO what are these?
1631+ [] [] -- TODO argument types, inaccessible types
1632+ clauses'
1633+ clauses''
1634+ clauses''
1635+ clauses''
1636+ clauses''
1637+ ty
1638+ ctxt
1639+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1640+ return ()
1641+
1598 -- | Do a step in the reflected elaborator monad. The input is the
1642 -- | Do a step in the reflected elaborator monad. The input is the
1599 -- step, the output is the (reflected) term returned.
1643 -- step, the output is the (reflected) term returned.
1600 runTacTm :: Term -> ElabD Term
1644 runTacTm :: Term -> ElabD Term
@@ -1633,9 +1677,9 @@ runTactical fc env tm = do tm' <- eval tm
1633 = do errs' <- eval errs
1677 = do errs' <- eval errs
1634 parts <- reifyReportParts errs'
1678 parts <- reifyReportParts errs'
1635 lift . tfail $ ReflectionError [parts] (Msg "")
1679 lift . tfail $ ReflectionError [parts] (Msg "")
1636− | n == tacN "prim__PureTactical", [_a, tm] <- args
1680+ | n == tacN "prim__PureElab", [_a, tm] <- args
1637 = return tm
1681 = return tm
1638− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1682+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1639 = do first' <- eval first
1683 = do first' <- eval first
1640 res <- runTacTm first'
1684 res <- runTacTm first'
1641 next <- eval (App andThen res)
1685 next <- eval (App andThen res)
@@ -1662,7 +1706,7 @@ runTactical fc env tm = do tm' <- eval tm
1662 returnUnit
1706 returnUnit
1663 | n == tacN "prim__Forget", [tt] <- args
1707 | n == tacN "prim__Forget", [tt] <- args
1664 = do tt' <- reifyTT tt
1708 = do tt' <- reifyTT tt
1665− fmap fst . get_type_val $ reflect tt'
1709+ fmap fst . get_type_val . reflectRaw $ forget tt'
1666 | n == tacN "prim__Attack", [] <- args
1710 | n == tacN "prim__Attack", [] <- args
1667 = do attack
1711 = do attack
1668 returnUnit
1712 returnUnit
@@ -1703,10 +1747,14 @@ runTactical fc env tm = do tm' <- eval tm
1703 let decl = TyDecl Ref checked
1747 let decl = TyDecl Ref checked
1704 ctxt' = addCtxtDef n decl ctxt
1748 ctxt' = addCtxtDef n decl ctxt
1705 set_context ctxt'
1749 set_context ctxt'
1706− updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :
1750+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :
1707 new_tyDecls e }
1751 new_tyDecls e }
1708 aux <- getAux
1752 aux <- getAux
1709 returnUnit
1753 returnUnit
1754+ | n == tacN "prim__DefineFunction", [decl] <- args
1755+ = do defn <- reifyFunDefn decl
1756+ defineFunction defn
1757+ returnUnit
1710 | n == tacN "prim__Debug", [ty, msg] <- args
1758 | n == tacN "prim__Debug", [ty, msg] <- args
1711 = do let msg' = fromTTMaybe msg
1759 = do let msg' = fromTTMaybe msg
1712 case msg' of
1760 case msg' of
@@ -1968,780 +2016,6 @@ runTac autoSolve ist perhapsFC fn tac
1968 runReflected t = do t' <- reify ist t
2016 runReflected t = do t' <- reify ist t
1969 runTac autoSolve ist perhapsFC fn t'
2017 runTac autoSolve ist perhapsFC fn t'
1970
2018
1971−-- | Prefix a name with the "Language.Reflection" namespace
1972−reflm :: String -> Name
1973−reflm n = sNS (sUN n) ["Reflection", "Language"]
1974−
1975−
1976−-- | Reify tactics from their reflected representation
1977−reify :: IState -> Term -> ElabD PTactic
1978−reify _ (P _ n _) | n == reflm "Intros" = return Intros
1979−reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
1980−reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
1981−reify _ (P _ n _) | n == reflm "Solve" = return Solve
1982−reify _ (P _ n _) | n == reflm "Compute" = return Compute
1983−reify _ (P _ n _) | n == reflm "Skip" = return Skip
1984−reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1985−reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
1986−reify ist t@(App _ _)
1987− | (P _ f _, args) <- unApply t = reifyApp ist f args
1988−reify _ t = fail ("Unknown tactic " ++ show t)
1989−
1990−reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1991−reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1992−reifyApp _ t [Constant (I i)]
1993− | t == reflm "Search" = return (ProofSearch True True i Nothing [])
1994−reifyApp _ t [x]
1995− | t == reflm "Refine" = do n <- reifyTTName x
1996− return $ Refine n []
1997−reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
1998− goal <- reifyTT ty
1999− return $ Claim n' (delab ist goal)
2000−reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
2001−reifyApp ist t [Constant (Str n), x]
2002− | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
2003−reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
2004−reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
2005−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
2006−reifyApp ist t [t']
2007− | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
2008−reifyApp ist t [t']
2009− | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
2010−reifyApp ist t [t']
2011− | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
2012−reifyApp _ t [t']
2013− | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
2014−reifyApp ist t [t']
2015− | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
2016−reifyApp ist t [x]
2017− | t == reflm "Focus" = liftM Focus (reifyTTName x)
2018−reifyApp ist t [t']
2019− | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
2020−reifyApp ist t [n, t']
2021− | t == reflm "LetTac" = do n' <- reifyTTName n
2022− t'' <- reifyTT t'
2023− return $ LetTac n' (delab ist t')
2024−reifyApp ist t [n, tt', t']
2025− | t == reflm "LetTacTy" = do n' <- reifyTTName n
2026− tt'' <- reifyTT tt'
2027− t'' <- reifyTT t'
2028− return $ LetTacTy n' (delab ist tt'') (delab ist t'')
2029−reifyApp ist t [errs]
2030− | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
2031−reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
2032−
2033−reifyReportParts :: Term -> ElabD [ErrorReportPart]
2034−reifyReportParts errs =
2035− case unList errs of
2036− Nothing -> fail "Failed to reify errors"
2037− Just errs' ->
2038− let parts = mapM reifyReportPart errs' in
2039− case parts of
2040− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
2041− Right errs'' ->
2042− return errs''
2043−
2044−-- | Reify terms from their reflected representation
2045−reifyTT :: Term -> ElabD Term
2046−reifyTT t@(App _ _)
2047− | (P _ f _, args) <- unApply t = reifyTTApp f args
2048−reifyTT t@(P _ n _)
2049− | n == reflm "Erased" = return $ Erased
2050−reifyTT t@(P _ n _)
2051− | n == reflm "Impossible" = return $ Impossible
2052−reifyTT t = fail ("Unknown reflection term: " ++ show t)
2053−
2054−reifyTTApp :: Name -> [Term] -> ElabD Term
2055−reifyTTApp t [nt, n, x]
2056− | t == reflm "P" = do nt' <- reifyTTNameType nt
2057− n' <- reifyTTName n
2058− x' <- reifyTT x
2059− return $ P nt' n' x'
2060−reifyTTApp t [Constant (I i)]
2061− | t == reflm "V" = return $ V i
2062−reifyTTApp t [n, b, x]
2063− | t == reflm "Bind" = do n' <- reifyTTName n
2064− b' <- reifyTTBinder reifyTT (reflm "TT") b
2065− x' <- reifyTT x
2066− return $ Bind n' b' x'
2067−reifyTTApp t [f, x]
2068− | t == reflm "App" = do f' <- reifyTT f
2069− x' <- reifyTT x
2070− return $ App f' x'
2071−reifyTTApp t [c]
2072− | t == reflm "TConst" = liftM Constant (reifyTTConst c)
2073−reifyTTApp t [t', Constant (I i)]
2074− | t == reflm "Proj" = do t'' <- reifyTT t'
2075− return $ Proj t'' i
2076−reifyTTApp t [tt]
2077− | t == reflm "TType" = liftM TType (reifyTTUExp tt)
2078−reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
2079−
2080−-- | Reify raw terms from their reflected representation
2081−reifyRaw :: Term -> ElabD Raw
2082−reifyRaw t@(App _ _)
2083− | (P _ f _, args) <- unApply t = reifyRawApp f args
2084−reifyRaw t@(P _ n _)
2085− | n == reflm "RType" = return $ RType
2086−reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
2087−
2088−reifyRawApp :: Name -> [Term] -> ElabD Raw
2089−reifyRawApp t [n]
2090− | t == reflm "Var" = liftM Var (reifyTTName n)
2091−reifyRawApp t [n, b, x]
2092− | t == reflm "RBind" = do n' <- reifyTTName n
2093− b' <- reifyTTBinder reifyRaw (reflm "Raw") b
2094− x' <- reifyRaw x
2095− return $ RBind n' b' x'
2096−reifyRawApp t [f, x]
2097− | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
2098−reifyRawApp t [t']
2099− | t == reflm "RForce" = liftM RForce (reifyRaw t')
2100−reifyRawApp t [c]
2101− | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
2102−reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
2103−
2104−reifyTTName :: Term -> ElabD Name
2105−reifyTTName t
2106− | (P _ f _, args) <- unApply t = reifyTTNameApp f args
2107−reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
2108−
2109−reifyTTNameApp :: Name -> [Term] -> ElabD Name
2110−reifyTTNameApp t [Constant (Str n)]
2111− | t == reflm "UN" = return $ sUN n
2112−reifyTTNameApp t [n, ns]
2113− | t == reflm "NS" = do n' <- reifyTTName n
2114− ns' <- reifyTTNamespace ns
2115− return $ sNS n' ns'
2116−reifyTTNameApp t [Constant (I i), Constant (Str n)]
2117− | t == reflm "MN" = return $ sMN i n
2118−reifyTTNameApp t []
2119− | t == reflm "NErased" = return NErased
2120−reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
2121−
2122−reifyTTNamespace :: Term -> ElabD [String]
2123−reifyTTNamespace t@(App _ _)
2124− = case unApply t of
2125− (P _ f _, [Constant StrType])
2126− | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
2127− (P _ f _, [Constant StrType, Constant (Str n), ns])
2128− | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
2129− _ -> fail ("Unknown reflection namespace arg: " ++ show t)
2130−reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
2131−
2132−reifyTTNameType :: Term -> ElabD NameType
2133−reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
2134−reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
2135−reifyTTNameType t@(App _ _)
2136− = case unApply t of
2137− (P _ f _, [Constant (I tag), Constant (I num)])
2138− | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
2139− | f == reflm "TCon" -> return $ TCon tag num
2140− _ -> fail ("Unknown reflection name type: " ++ show t)
2141−reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
2142−
2143−reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
2144−reifyTTBinder reificator binderType t@(App _ _)
2145− = case unApply t of
2146− (P _ f _, bt:args) | forget bt == Var binderType
2147− -> reifyTTBinderApp reificator f args
2148− _ -> fail ("Mismatching binder reflection: " ++ show t)
2149−reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
2150−
2151−reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
2152−reifyTTBinderApp reif f [t]
2153− | f == reflm "Lam" = liftM Lam (reif t)
2154−reifyTTBinderApp reif f [t, k]
2155− | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
2156−reifyTTBinderApp reif f [x, y]
2157− | f == reflm "Let" = liftM2 Let (reif x) (reif y)
2158−reifyTTBinderApp reif f [x, y]
2159− | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
2160−reifyTTBinderApp reif f [t]
2161− | f == reflm "Hole" = liftM Hole (reif t)
2162−reifyTTBinderApp reif f [t]
2163− | f == reflm "GHole" = liftM (GHole 0) (reif t)
2164−reifyTTBinderApp reif f [x, y]
2165− | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
2166−reifyTTBinderApp reif f [t]
2167− | f == reflm "PVar" = liftM PVar (reif t)
2168−reifyTTBinderApp reif f [t]
2169− | f == reflm "PVTy" = liftM PVTy (reif t)
2170−reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
2171−
2172−reifyTTConst :: Term -> ElabD Const
2173−reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
2174−reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
2175−reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
2176−reifyTTConst t@(App _ _)
2177− | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
2178−reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
2179−
2180−reifyTTConstApp :: Name -> Term -> ElabD Const
2181−reifyTTConstApp f aty
2182− | f == reflm "AType" = fmap AType (reifyArithTy aty)
2183−reifyTTConstApp f (Constant c@(I _))
2184− | f == reflm "I" = return $ c
2185−reifyTTConstApp f (Constant c@(BI _))
2186− | f == reflm "BI" = return $ c
2187−reifyTTConstApp f (Constant c@(Fl _))
2188− | f == reflm "Fl" = return $ c
2189−reifyTTConstApp f (Constant c@(I _))
2190− | f == reflm "Ch" = return $ c
2191−reifyTTConstApp f (Constant c@(Str _))
2192− | f == reflm "Str" = return $ c
2193−reifyTTConstApp f (Constant c@(B8 _))
2194− | f == reflm "B8" = return $ c
2195−reifyTTConstApp f (Constant c@(B16 _))
2196− | f == reflm "B16" = return $ c
2197−reifyTTConstApp f (Constant c@(B32 _))
2198− | f == reflm "B32" = return $ c
2199−reifyTTConstApp f (Constant c@(B64 _))
2200− | f == reflm "B64" = return $ c
2201−reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
2202−
2203−reifyArithTy :: Term -> ElabD ArithTy
2204−reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
2205−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
2206−reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
2207−
2208−reifyNativeTy :: Term -> ElabD NativeTy
2209−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2210−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2211−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2212−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2213−reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
2214−
2215−reifyIntTy :: Term -> ElabD IntTy
2216−reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
2217−reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
2218−reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
2219−reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2220−reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
2221−
2222−reifyTTUExp :: Term -> ElabD UExp
2223−reifyTTUExp t@(App _ _)
2224− = case unApply t of
2225− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
2226− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
2227− _ -> fail ("Unknown reflection type universe expression: " ++ show t)
2228−reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
2229−
2230−-- | Create a reflected call to a named function/constructor
2231−reflCall :: String -> [Raw] -> Raw
2232−reflCall funName args
2233− = raw_apply (Var (reflm funName)) args
2234−
2235−-- | Lift a term into its Language.Reflection.TT representation
2236−reflect :: Term -> Raw
2237−reflect = reflectTTQuote []
2238−
2239−-- | Lift a term into its Language.Reflection.Raw representation
2240−reflectRaw :: Raw -> Raw
2241−reflectRaw = reflectRawQuote []
2242−
2243−claimTT :: Name -> ElabD Name
2244−claimTT n = do n' <- getNameFrom n
2245− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
2246− return n'
2247−
2248−-- | Convert a reflected term to a more suitable form for pattern-matching.
2249−-- In particular, the less-interesting bits are elaborated to _ patterns. This
2250−-- happens to NameTypes, universe levels, names that are bound but not used,
2251−-- and the type annotation field of the P constructor.
2252−reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2253−reflectTTQuotePattern unq (P _ n _)
2254− | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2255− do fill (Var n) ; solve
2256− | otherwise =
2257− do tyannot <- claimTT (sMN 0 "pTyAnnot")
2258− movelast tyannot -- use a _ pattern here
2259− nt <- getNameFrom (sMN 0 "nt")
2260− claim nt (Var (reflm "NameType"))
2261− movelast nt -- use a _ pattern here
2262− n' <- getNameFrom (sMN 0 "n")
2263− claim n' (Var (reflm "TTName"))
2264− fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2265− solve
2266− focus n'; reflectNameQuotePattern n
2267−reflectTTQuotePattern unq (V n)
2268− = do fill $ reflCall "V" [RConstant (I n)]
2269− solve
2270−reflectTTQuotePattern unq (Bind n b x)
2271− = do x' <- claimTT (sMN 0 "sc")
2272− movelast x'
2273− b' <- getNameFrom (sMN 0 "binder")
2274− claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
2275− (Var (sNS (sUN "TT") ["Reflection", "Language"])))
2276− if n `elem` freeNames x
2277− then do fill $ reflCall "Bind"
2278− [reflectName n,
2279− Var b',
2280− Var x']
2281− solve
2282− else do any <- getNameFrom (sMN 0 "anyName")
2283− claim any (Var (reflm "TTName"))
2284− movelast any
2285− fill $ reflCall "Bind"
2286− [Var any,
2287− Var b',
2288− Var x']
2289− solve
2290− focus x'; reflectTTQuotePattern unq x
2291− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
2292−reflectTTQuotePattern unq (App f x)
2293− = do f' <- claimTT (sMN 0 "f"); movelast f'
2294− x' <- claimTT (sMN 0 "x"); movelast x'
2295− fill $ reflCall "App" [Var f', Var x']
2296− solve
2297− focus f'; reflectTTQuotePattern unq f
2298− focus x'; reflectTTQuotePattern unq x
2299−reflectTTQuotePattern unq (Constant c)
2300− = do fill $ reflCall "TConst" [reflectConstant c]
2301− solve
2302−reflectTTQuotePattern unq (Proj t i)
2303− = do t' <- claimTT (sMN 0 "t"); movelast t'
2304− fill $ reflCall "Proj" [Var t', RConstant (I i)]
2305− solve
2306− focus t'; reflectTTQuotePattern unq t
2307−reflectTTQuotePattern unq (Erased)
2308− = do erased <- claimTT (sMN 0 "erased")
2309− movelast erased
2310− fill $ (Var erased)
2311− solve
2312−reflectTTQuotePattern unq (Impossible)
2313− = do fill $ Var (reflm "Impossible")
2314− solve
2315−reflectTTQuotePattern unq (TType exp)
2316− = do ue <- getNameFrom (sMN 0 "uexp")
2317− claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2318− movelast ue
2319− fill $ reflCall "TType" [Var ue]
2320− solve
2321−reflectTTQuotePattern unq (UType u)
2322− = do uH <- getNameFrom (sMN 0 "someUniv")
2323− claim uH (Var (reflm "Universe"))
2324− movelast uH
2325− fill $ reflCall "UType" [Var uH]
2326− solve
2327− focus uH
2328− fill (Var (reflm (case u of
2329− NullType -> "NullType"
2330− UniqueType -> "UniqueType"
2331− AllTypes -> "AllTypes")))
2332− solve
2333−
2334−reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2335−reflectRawQuotePattern unq (Var n)
2336− -- the unquoted names already have types, just use them
2337− | n `elem` unq = do fill (Var n); solve
2338− | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2339−reflectRawQuotePattern unq (RBind n b sc) =
2340− do scH <- getNameFrom (sMN 0 "sc")
2341− claim scH (Var (reflm "Raw"))
2342− movelast scH
2343− bH <- getNameFrom (sMN 0 "binder")
2344− claim bH (RApp (Var (reflm "Binder"))
2345− (Var (reflm "Raw")))
2346− if n `elem` freeNamesR sc
2347− then do fill $ reflCall "RBind" [reflectName n,
2348− Var bH,
2349− Var scH]
2350− solve
2351− else do any <- getNameFrom (sMN 0 "anyName")
2352− claim any (Var (reflm "TTName"))
2353− movelast any
2354− fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2355− solve
2356− focus scH; reflectRawQuotePattern unq sc
2357− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2358− where freeNamesR (Var n) = [n]
2359− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2360− freeNamesR body \\ [n],
2361− freeNamesR t]
2362− freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2363− (freeNamesR body \\ [n])
2364− freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2365− freeNamesR RType = []
2366− freeNamesR (RUType _) = []
2367− freeNamesR (RForce r) = freeNamesR r
2368− freeNamesR (RConstant _) = []
2369−reflectRawQuotePattern unq (RApp f x) =
2370− do fH <- getNameFrom (sMN 0 "f")
2371− claim fH (Var (reflm "Raw"))
2372− movelast fH
2373− xH <- getNameFrom (sMN 0 "x")
2374− claim xH (Var (reflm "Raw"))
2375− movelast xH
2376− fill $ reflCall "RApp" [Var fH, Var xH]
2377− solve
2378− focus fH; reflectRawQuotePattern unq f
2379− focus xH; reflectRawQuotePattern unq x
2380−reflectRawQuotePattern unq RType =
2381− do fill (Var (reflm "RType"))
2382− solve
2383−reflectRawQuotePattern unq (RUType univ) =
2384− do uH <- getNameFrom (sMN 0 "universe")
2385− claim uH (Var (reflm "Universe"))
2386− movelast uH
2387− fill $ reflCall "RUType" [Var uH]
2388− solve
2389− focus uH; fill (reflectUniverse univ); solve
2390−reflectRawQuotePattern unq (RForce r) =
2391− do rH <- getNameFrom (sMN 0 "raw")
2392− claim rH (Var (reflm "Raw"))
2393− movelast rH
2394− fill $ reflCall "RForce" [Var rH]
2395− solve
2396− focus rH; reflectRawQuotePattern unq r
2397−reflectRawQuotePattern unq (RConstant c) =
2398− do cH <- getNameFrom (sMN 0 "const")
2399− claim cH (Var (reflm "Constant"))
2400− movelast cH
2401− fill (reflCall "RConstant" [Var cH]); solve
2402− focus cH
2403− fill (reflectConstant c); solve
2404−
2405−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2406−reflectBinderQuotePattern q unq (Lam t)
2407− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2408− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2409− solve
2410− focus t'; q unq t
2411−reflectBinderQuotePattern q unq (Pi _ t k)
2412− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2413− k' <- claimTT (sMN 0 "k"); movelast k';
2414− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2415− solve
2416− focus t'; q unq t
2417−reflectBinderQuotePattern q unq (Let x y)
2418− = do x' <- claimTT (sMN 0 "ty"); movelast x';
2419− y' <- claimTT (sMN 0 "v"); movelast y';
2420− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2421− solve
2422− focus x'; q unq x
2423− focus y'; q unq y
2424−reflectBinderQuotePattern q unq (NLet x y)
2425− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2426− y' <- claimTT (sMN 0 "v"); movelast y'
2427− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2428− solve
2429− focus x'; q unq x
2430− focus y'; q unq y
2431−reflectBinderQuotePattern q unq (Hole t)
2432− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2433− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2434− solve
2435− focus t'; q unq t
2436−reflectBinderQuotePattern q unq (GHole _ t)
2437− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2438− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2439− solve
2440− focus t'; q unq t
2441−reflectBinderQuotePattern q unq (Guess x y)
2442− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2443− y' <- claimTT (sMN 0 "v"); movelast y'
2444− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2445− solve
2446− focus x'; q unq x
2447− focus y'; q unq y
2448−reflectBinderQuotePattern q unq (PVar t)
2449− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2450− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2451− solve
2452− focus t'; q unq t
2453−reflectBinderQuotePattern q unq (PVTy t)
2454− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2455− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2456− solve
2457− focus t'; q unq t
2458−
2459−reflectUniverse :: Universe -> Raw
2460−reflectUniverse u =
2461− (Var (reflm (case u of
2462− NullType -> "NullType"
2463− UniqueType -> "UniqueType"
2464− AllTypes -> "AllTypes")))
2465−
2466−-- | Create a reflected TT term, but leave refs to the provided name intact
2467−reflectTTQuote :: [Name] -> Term -> Raw
2468−reflectTTQuote unq (P nt n t)
2469− | n `elem` unq = Var n
2470− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2471−reflectTTQuote unq (V n)
2472− = reflCall "V" [RConstant (I n)]
2473−reflectTTQuote unq (Bind n b x)
2474− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
2475−reflectTTQuote unq (App f x)
2476− = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2477−reflectTTQuote unq (Constant c)
2478− = reflCall "TConst" [reflectConstant c]
2479−reflectTTQuote unq (Proj t i)
2480− = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2481−reflectTTQuote unq (Erased) = Var (reflm "Erased")
2482−reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2483−reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2484−reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2485−
2486−reflectRawQuote :: [Name] -> Raw -> Raw
2487−reflectRawQuote unq (Var n)
2488− | n `elem` unq = Var n
2489− | otherwise = reflCall "Var" [reflectName n]
2490−reflectRawQuote unq (RBind n b r) =
2491− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
2492−reflectRawQuote unq (RApp f x) =
2493− reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2494−reflectRawQuote unq RType = Var (reflm "RType")
2495−reflectRawQuote unq (RUType u) =
2496− reflCall "RUType" [reflectUniverse u]
2497−reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2498−reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
2499−
2500−reflectNameType :: NameType -> Raw
2501−reflectNameType (Bound) = Var (reflm "Bound")
2502−reflectNameType (Ref) = Var (reflm "Ref")
2503−reflectNameType (DCon x y _)
2504− = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
2505−reflectNameType (TCon x y)
2506− = reflCall "TCon" [RConstant (I x), RConstant (I y)]
2507−
2508−reflectName :: Name -> Raw
2509−reflectName (UN s)
2510− = reflCall "UN" [RConstant (Str (str s))]
2511−reflectName (NS n ns)
2512− = reflCall "NS" [ reflectName n
2513− , foldr (\ n s ->
2514− raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
2515− [ RConstant StrType, RConstant (Str n), s ])
2516− ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
2517− [ RConstant StrType ])
2518− (map str ns)
2519− ]
2520−reflectName (MN i n)
2521− = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
2522−reflectName (NErased) = Var (reflm "NErased")
2523−reflectName n = Var (reflm "NErased") -- special name, not yet implemented
2524−
2525−-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
2526−-- MNs corresponding to will care about the string but not the number. All
2527−-- others become _.
2528−reflectNameQuotePattern :: Name -> ElabD ()
2529−reflectNameQuotePattern n@(UN s)
2530− = do fill $ reflectName n
2531− solve
2532−reflectNameQuotePattern n@(NS _ _)
2533− = do fill $ reflectName n
2534− solve
2535−reflectNameQuotePattern (MN _ n)
2536− = do i <- getNameFrom (sMN 0 "mnCounter")
2537− claim i (RConstant (AType (ATInt ITNative)))
2538− movelast i
2539− fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
2540− solve
2541−reflectNameQuotePattern _ -- for all other names, match any
2542− = do nameHole <- getNameFrom (sMN 0 "name")
2543− claim nameHole (Var (reflm "TTName"))
2544− movelast nameHole
2545− fill (Var nameHole)
2546− solve
2547−
2548−reflectBinder :: Binder Term -> Raw
2549−reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
2550−
2551−reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
2552−reflectBinderQuote q ty unq (Lam t)
2553− = reflCall "Lam" [Var ty, q unq t]
2554−reflectBinderQuote q ty unq (Pi _ t k)
2555− = reflCall "Pi" [Var ty, q unq t, q unq k]
2556−reflectBinderQuote q ty unq (Let x y)
2557− = reflCall "Let" [Var ty, q unq x, q unq y]
2558−reflectBinderQuote q ty unq (NLet x y)
2559− = reflCall "NLet" [Var ty, q unq x, q unq y]
2560−reflectBinderQuote q ty unq (Hole t)
2561− = reflCall "Hole" [Var ty, q unq t]
2562−reflectBinderQuote q ty unq (GHole _ t)
2563− = reflCall "GHole" [Var ty, q unq t]
2564−reflectBinderQuote q ty unq (Guess x y)
2565− = reflCall "Guess" [Var ty, q unq x, q unq y]
2566−reflectBinderQuote q ty unq (PVar t)
2567− = reflCall "PVar" [Var ty, q unq t]
2568−reflectBinderQuote q ty unq (PVTy t)
2569− = reflCall "PVTy" [Var ty, q unq t]
2570−
2571−mkList :: Raw -> [Raw] -> Raw
2572−mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2573−mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
2574− x)
2575− (mkList ty xs)
2576−
2577−reflectConstant :: Const -> Raw
2578−reflectConstant c@(I _) = reflCall "I" [RConstant c]
2579−reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
2580−reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
2581−reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
2582−reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
2583−reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
2584−reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
2585−reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
2586−reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
2587−reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
2588−reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
2589−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
2590−reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
2591−reflectConstant StrType = Var (reflm "StrType")
2592−reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
2593−reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
2594−reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
2595−reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
2596−reflectConstant VoidType = Var (reflm "VoidType")
2597−reflectConstant Forgot = Var (reflm "Forgot")
2598−reflectConstant WorldType = Var (reflm "WorldType")
2599−reflectConstant TheWorld = Var (reflm "TheWorld")
2600−
2601−reflectUExp :: UExp -> Raw
2602−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2603−reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
2604−
2605−-- | Reflect the environment of a proof into a List (TTName, Binder TT)
2606−reflectEnv :: Env -> Raw
2607−reflectEnv = foldr consToEnvList emptyEnvList
2608− where
2609− consToEnvList :: (Name, Binder Term) -> Raw -> Raw
2610− consToEnvList (n, b) l
2611− = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
2612− [ envTupleType
2613− , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
2614− , (RApp (Var $ reflm "Binder")
2615− (Var $ reflm "TT"))
2616− , reflectName n
2617− , reflectBinder b
2618− ]
2619− , l
2620− ]
2621−
2622− emptyEnvList :: Raw
2623− emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
2624− [envTupleType]
2625−
2626−-- | Reflect an error into the internal datatype of Idris -- TODO
2627−rawBool :: Bool -> Raw
2628−rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
2629−rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
2630−
2631−rawNil :: Raw -> Raw
2632−rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
2633−
2634−rawCons :: Raw -> Raw -> Raw -> Raw
2635−rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
2636−
2637−rawList :: Raw -> [Raw] -> Raw
2638−rawList ty = foldr (rawCons ty) (rawNil ty)
2639−
2640−rawPairTy :: Raw -> Raw -> Raw
2641−rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
2642−
2643−rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
2644−rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
2645−
2646−reflectCtxt :: [(Name, Type)] -> Raw
2647−reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
2648− (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
2649− (reflectName n, reflect t)))
2650− ctxt)
2651−
2652−reflectErr :: Err -> Raw
2653−reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
2654−reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
2655−reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
2656− raw_apply (Var $ reflErrName "CantUnify")
2657− [ rawBool b
2658− , reflect t1
2659− , reflect t2
2660− , reflectErr e
2661− , reflectCtxt ctxt
2662− , RConstant (I i)]
2663−reflectErr (InfiniteUnify n tm ctxt) =
2664− raw_apply (Var $ reflErrName "InfiniteUnify")
2665− [ reflectName n
2666− , reflect tm
2667− , reflectCtxt ctxt
2668− ]
2669−reflectErr (CantConvert t t' ctxt) =
2670− raw_apply (Var $ reflErrName "CantConvert")
2671− [ reflect t
2672− , reflect t'
2673− , reflectCtxt ctxt
2674− ]
2675−reflectErr (CantSolveGoal t ctxt) =
2676− raw_apply (Var $ reflErrName "CantSolveGoal")
2677− [ reflect t
2678− , reflectCtxt ctxt
2679− ]
2680−reflectErr (UnifyScope n n' t ctxt) =
2681− raw_apply (Var $ reflErrName "UnifyScope")
2682− [ reflectName n
2683− , reflectName n'
2684− , reflect t
2685− , reflectCtxt ctxt
2686− ]
2687−reflectErr (CantInferType str) =
2688− raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
2689−reflectErr (NonFunctionType t t') =
2690− raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
2691−reflectErr (NotEquality t t') =
2692− raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
2693−reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
2694−reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
2695−reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
2696−reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
2697−reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
2698−reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
2699−reflectErr (NotInjective t1 t2 t3) =
2700− raw_apply (Var $ reflErrName "NotInjective")
2701− [ reflect t1
2702− , reflect t2
2703− , reflect t3
2704− ]
2705−reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2706−reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
2707−reflectErr (CantResolveAlts ss) =
2708− raw_apply (Var $ reflErrName "CantResolveAlts")
2709− [rawList (Var $ reflm "TTName") (map reflectName ss)]
2710−reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2711−reflectErr (NoEliminator str t)
2712− = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
2713− reflect t]
2714−reflectErr UniverseError = Var $ reflErrName "UniverseError"
2715−reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
2716−reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
2717−reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
2718−reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
2719−reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
2720−reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
2721−reflectErr (ProviderError str) =
2722− raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
2723−reflectErr (LoadingFailed str err) =
2724− raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2725−reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2726−
2727−-- | Reflect a file context
2728−reflectFC :: FC -> Raw
2729−reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2730− [ RConstant (Str (fc_fname fc))
2731− , raw_apply (Var pairCon) $
2732− [intTy, intTy] ++
2733− map (RConstant . I)
2734− [ fst (fc_start fc)
2735− , snd (fc_start fc)
2736− ]
2737− , raw_apply (Var pairCon) $
2738− [intTy, intTy] ++
2739− map (RConstant . I)
2740− [ fst (fc_end fc)
2741− , snd (fc_end fc)
2742− ]
2743− ]
2744− where intTy = RConstant (AType (ATInt ITNative))
2745
2019
2746elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2020elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2747elaboratingArgErr [] err = err
2021elaboratingArgErr [] err = err
@@ -2813,70 +2087,4 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2813 [] -> e
2087 [] -> e
2814 parts -> ReflectionError errorparts e
2088 parts -> ReflectionError errorparts e
2815
2089
2816−fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
2817−fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
2818− | just == txt "Just" = Just tm
2819−fromTTMaybe x = Nothing
2820−
2821−reflErrName :: String -> Name
2822−reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
2823−
2824−-- | Attempt to reify a report part from TT to the internal
2825−-- representation. Not in Idris or ElabD monads because it should be usable
2826−-- from either.
2827−reifyReportPart :: Term -> Either Err ErrorReportPart
2828−reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
2829− Right (TextPart msg)
2830−reifyReportPart (App (P (DCon _ _ _) n _) ttn)
2831− | n == reflm "NamePart" =
2832− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
2833− Error e -> Left . InternalMsg $
2834− "could not reify name term " ++
2835− show ttn ++
2836− " when reflecting an error:" ++ show e
2837− OK (n', _)-> Right $ NamePart n'
2838−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2839− | n == reflm "TermPart" =
2840− case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
2841− Error e -> Left . InternalMsg $
2842− "could not reify reflected term " ++
2843− show tm ++
2844− " when reflecting an error:" ++ show e
2845− OK (tm', _) -> Right $ TermPart tm'
2846−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2847− | n == reflm "SubReport" =
2848− case unList tm of
2849− Just xs -> do subParts <- mapM reifyReportPart xs
2850− Right (SubReport subParts)
2851− Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
2852−reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
2853−
2854−reifyTyDecl :: Term -> ElabD RTyDecl
2855−reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
2856− | n == tacN "Declare" =
2857− do tyN' <- reifyTTName tyN
2858− args' <- case unList args of
2859− Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
2860− Just xs -> mapM reifyRArg xs
2861− ret' <- reifyRaw ret
2862− return $ RDeclare tyN' args' ret'
2863− where reifyRArg :: Term -> ElabD RArg
2864− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)
2865− | n == tacN "Explicit" = liftM2 RExplicit
2866− (reifyTTName argN)
2867− (reifyRaw argTy)
2868− | n == tacN "Implicit" = liftM2 RImplicit
2869− (reifyTTName argN)
2870− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
2871− (reifyTTName argN)
2872− (reifyRaw argTy)
2873− reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
2874−reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
2875−
2876−envTupleType :: Raw
2877−envTupleType
2878− = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2879− , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
2880− ]
2881−
2882solveAll = try (do solve; solveAll) (return ())
2090solveAll = try (do solve; solveAll) (return ())
src/Idris/Error.hs+1−1
@@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
151−warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm
151+warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm
src/Idris/IBC.hs+4−4
@@ -1674,9 +1674,9 @@ instance Binary PTerm where
1674 put x2
1674 put x2
1675 PUniverse x1 -> do putWord8 38
1675 PUniverse x1 -> do putWord8 38
1676 put x1
1676 put x1
1677− PRunTactics x1 x2 -> do putWord8 39
1677+ PRunElab x1 x2 -> do putWord8 39
1678− put x1
1678+ put x1
1679− put x2
1679+ put x2
1680 PAs x1 x2 x3 -> do putWord8 40
1680 PAs x1 x2 x3 -> do putWord8 40
1681 put x1
1681 put x1
1682 put x2
1682 put x2
@@ -1809,7 +1809,7 @@ instance Binary PTerm where
1809 return (PUniverse x1)
1809 return (PUniverse x1)
1810 39 -> do x1 <- get
1810 39 -> do x1 <- get
1811 x2 <- get
1811 x2 <- get
1812− return (PRunTactics x1 x2)
1812+ return (PRunElab x1 x2)
1813 40 -> do x1 <- get
1813 40 -> do x1 <- get
1814 x2 <- get
1814 x2 <- get
1815 x3 <- get
1815 x3 <- get
src/Idris/IdrisDoc.hs+1−1
@@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
324−extractPTermNames (PRunTactics _ p) = extract p
324+extractPTermNames (PRunElab _ p) = extract p
325extractPTermNames _ = []
325extractPTermNames _ = []
326
326
327-- | Shorter name for extractPTermNames
327-- | Shorter name for extractPTermNames
src/Idris/ParseExpr.hs+9−9
@@ -220,7 +220,7 @@ InternalExpr ::=
220internalExpr :: SyntaxInfo -> IdrisParser PTerm
220internalExpr :: SyntaxInfo -> IdrisParser PTerm
221internalExpr syn =
221internalExpr syn =
222 unifyLog syn
222 unifyLog syn
223− <|> runTactics syn
223+ <|> runElab syn
224 <|> disamb syn
224 <|> disamb syn
225 <|> noImplicits syn
225 <|> noImplicits syn
226 <|> recordType syn
226 <|> recordType syn
@@ -497,16 +497,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
497
497
498{- | Parses a new-style tactics expression
498{- | Parses a new-style tactics expression
499RunTactics ::=
499RunTactics ::=
500− '%' 'runTactics' SimpleExpr
500+ '%' 'runElab' SimpleExpr
501 ;
501 ;
502-}
502-}
503−runTactics :: SyntaxInfo -> IdrisParser PTerm
503+runElab :: SyntaxInfo -> IdrisParser PTerm
504−runTactics syn = do try (lchar '%' *> reserved "runTactics")
504+runElab syn = do try (lchar '%' *> reserved "runElab")
505− fc <- getFC
505+ fc <- getFC
506− tm <- simpleExpr syn
506+ tm <- simpleExpr syn
507− i <- get
507+ i <- get
508− return $ PRunTactics fc tm
508+ return $ PRunElab fc tm
509− <?> "new-style tactics expression"
509+ <?> "new-style tactics expression"
510
510
511{- | Parses a disambiguation expression
511{- | Parses a disambiguation expression
512Disamb ::=
512Disamb ::=
src/Idris/Reflection.hs+883−3
@@ -1,10 +1,22 @@
1−{-|
1+{-| Code related to Idris's reflection system. This module contains
2−Handy tools for doing reflection.
2+quoters and unquoters along with some supporting datatypes.
3-}
3-}
4+{-# LANGUAGE PatternGuards #-}
5+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4module Idris.Reflection where
6module Idris.Reflection where
5
7
8+import Control.Monad (liftM, liftM2)
9+import Data.List ((\\))
10+import qualified Data.Text as T
11+
12+import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
13+ movelast, runElab, solve)
14+import Idris.Core.Evaluate (initContext)
6import Idris.Core.TT
15import Idris.Core.TT
16+
7−import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))
17+import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
18+ PTerm(..), initEState, pairCon, pairTy)
19+import Idris.Delaborate (delab)
8
20
9data RArg = RExplicit { argName :: Name, argTy :: Raw }
21data RArg = RExplicit { argName :: Name, argTy :: Raw }
10 | RImplicit { argName :: Name, argTy :: Raw }
22 | RImplicit { argName :: Name, argTy :: Raw }
@@ -16,3 +28,871 @@ rArgToPArg :: RArg -> PArg
16rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
28rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
29rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
30rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
31+
32+data RFunClause = RMkFunClause Raw Raw
33+ | RMkImpossibleClause Raw
34+ deriving Show
35+
36+data RFunDefn = RDefineFun Name [RFunClause] deriving Show
37+
38+-- | Prefix a name with the "Language.Reflection" namespace
39+reflm :: String -> Name
40+reflm n = sNS (sUN n) ["Reflection", "Language"]
41+
42+-- | Prefix a name with the "Language.Reflection.Elab" namespace
43+tacN :: String -> Name
44+tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
45+
46+-- | Reify tactics from their reflected representation
47+reify :: IState -> Term -> ElabD PTactic
48+reify _ (P _ n _) | n == reflm "Intros" = return Intros
49+reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
50+reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
51+reify _ (P _ n _) | n == reflm "Solve" = return Solve
52+reify _ (P _ n _) | n == reflm "Compute" = return Compute
53+reify _ (P _ n _) | n == reflm "Skip" = return Skip
54+reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
55+reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
56+reify ist t@(App _ _)
57+ | (P _ f _, args) <- unApply t = reifyApp ist f args
58+reify _ t = fail ("Unknown tactic " ++ show t)
59+
60+reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
61+reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
62+reifyApp _ t [Constant (I i)]
63+ | t == reflm "Search" = return (ProofSearch True True i Nothing [])
64+reifyApp _ t [x]
65+ | t == reflm "Refine" = do n <- reifyTTName x
66+ return $ Refine n []
67+reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
68+ goal <- reifyTT ty
69+ return $ Claim n' (delab ist goal)
70+reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
71+reifyApp ist t [Constant (Str n), x]
72+ | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
73+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
74+reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
75+reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
76+reifyApp ist t [t']
77+ | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
78+reifyApp ist t [t']
79+ | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
80+reifyApp ist t [t']
81+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
82+reifyApp _ t [t']
83+ | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
84+reifyApp ist t [t']
85+ | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
86+reifyApp ist t [x]
87+ | t == reflm "Focus" = liftM Focus (reifyTTName x)
88+reifyApp ist t [t']
89+ | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
90+reifyApp ist t [n, t']
91+ | t == reflm "LetTac" = do n' <- reifyTTName n
92+ t'' <- reifyTT t'
93+ return $ LetTac n' (delab ist t')
94+reifyApp ist t [n, tt', t']
95+ | t == reflm "LetTacTy" = do n' <- reifyTTName n
96+ tt'' <- reifyTT tt'
97+ t'' <- reifyTT t'
98+ return $ LetTacTy n' (delab ist tt'') (delab ist t'')
99+reifyApp ist t [errs]
100+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
101+reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
102+
103+reifyReportParts :: Term -> ElabD [ErrorReportPart]
104+reifyReportParts errs =
105+ case unList errs of
106+ Nothing -> fail "Failed to reify errors"
107+ Just errs' ->
108+ let parts = mapM reifyReportPart errs' in
109+ case parts of
110+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
111+ Right errs'' ->
112+ return errs''
113+
114+-- | Reify terms from their reflected representation
115+reifyTT :: Term -> ElabD Term
116+reifyTT t@(App _ _)
117+ | (P _ f _, args) <- unApply t = reifyTTApp f args
118+reifyTT t@(P _ n _)
119+ | n == reflm "Erased" = return $ Erased
120+reifyTT t@(P _ n _)
121+ | n == reflm "Impossible" = return $ Impossible
122+reifyTT t = fail ("Unknown reflection term: " ++ show t)
123+
124+reifyTTApp :: Name -> [Term] -> ElabD Term
125+reifyTTApp t [nt, n, x]
126+ | t == reflm "P" = do nt' <- reifyTTNameType nt
127+ n' <- reifyTTName n
128+ x' <- reifyTT x
129+ return $ P nt' n' x'
130+reifyTTApp t [Constant (I i)]
131+ | t == reflm "V" = return $ V i
132+reifyTTApp t [n, b, x]
133+ | t == reflm "Bind" = do n' <- reifyTTName n
134+ b' <- reifyTTBinder reifyTT (reflm "TT") b
135+ x' <- reifyTT x
136+ return $ Bind n' b' x'
137+reifyTTApp t [f, x]
138+ | t == reflm "App" = do f' <- reifyTT f
139+ x' <- reifyTT x
140+ return $ App f' x'
141+reifyTTApp t [c]
142+ | t == reflm "TConst" = liftM Constant (reifyTTConst c)
143+reifyTTApp t [t', Constant (I i)]
144+ | t == reflm "Proj" = do t'' <- reifyTT t'
145+ return $ Proj t'' i
146+reifyTTApp t [tt]
147+ | t == reflm "TType" = liftM TType (reifyTTUExp tt)
148+reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
149+
150+-- | Reify raw terms from their reflected representation
151+reifyRaw :: Term -> ElabD Raw
152+reifyRaw t@(App _ _)
153+ | (P _ f _, args) <- unApply t = reifyRawApp f args
154+reifyRaw t@(P _ n _)
155+ | n == reflm "RType" = return $ RType
156+reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
157+
158+reifyRawApp :: Name -> [Term] -> ElabD Raw
159+reifyRawApp t [n]
160+ | t == reflm "Var" = liftM Var (reifyTTName n)
161+reifyRawApp t [n, b, x]
162+ | t == reflm "RBind" = do n' <- reifyTTName n
163+ b' <- reifyTTBinder reifyRaw (reflm "Raw") b
164+ x' <- reifyRaw x
165+ return $ RBind n' b' x'
166+reifyRawApp t [f, x]
167+ | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
168+reifyRawApp t [t']
169+ | t == reflm "RForce" = liftM RForce (reifyRaw t')
170+reifyRawApp t [c]
171+ | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
172+reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
173+
174+reifyTTName :: Term -> ElabD Name
175+reifyTTName t
176+ | (P _ f _, args) <- unApply t = reifyTTNameApp f args
177+reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
178+
179+reifyTTNameApp :: Name -> [Term] -> ElabD Name
180+reifyTTNameApp t [Constant (Str n)]
181+ | t == reflm "UN" = return $ sUN n
182+reifyTTNameApp t [n, ns]
183+ | t == reflm "NS" = do n' <- reifyTTName n
184+ ns' <- reifyTTNamespace ns
185+ return $ sNS n' ns'
186+reifyTTNameApp t [Constant (I i), Constant (Str n)]
187+ | t == reflm "MN" = return $ sMN i n
188+reifyTTNameApp t []
189+ | t == reflm "NErased" = return NErased
190+reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
191+
192+reifyTTNamespace :: Term -> ElabD [String]
193+reifyTTNamespace t@(App _ _)
194+ = case unApply t of
195+ (P _ f _, [Constant StrType])
196+ | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
197+ (P _ f _, [Constant StrType, Constant (Str n), ns])
198+ | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
199+ _ -> fail ("Unknown reflection namespace arg: " ++ show t)
200+reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
201+
202+reifyTTNameType :: Term -> ElabD NameType
203+reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
204+reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
205+reifyTTNameType t@(App _ _)
206+ = case unApply t of
207+ (P _ f _, [Constant (I tag), Constant (I num)])
208+ | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
209+ | f == reflm "TCon" -> return $ TCon tag num
210+ _ -> fail ("Unknown reflection name type: " ++ show t)
211+reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
212+
213+reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
214+reifyTTBinder reificator binderType t@(App _ _)
215+ = case unApply t of
216+ (P _ f _, bt:args) | forget bt == Var binderType
217+ -> reifyTTBinderApp reificator f args
218+ _ -> fail ("Mismatching binder reflection: " ++ show t)
219+reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
220+
221+reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
222+reifyTTBinderApp reif f [t]
223+ | f == reflm "Lam" = liftM Lam (reif t)
224+reifyTTBinderApp reif f [t, k]
225+ | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
226+reifyTTBinderApp reif f [x, y]
227+ | f == reflm "Let" = liftM2 Let (reif x) (reif y)
228+reifyTTBinderApp reif f [x, y]
229+ | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
230+reifyTTBinderApp reif f [t]
231+ | f == reflm "Hole" = liftM Hole (reif t)
232+reifyTTBinderApp reif f [t]
233+ | f == reflm "GHole" = liftM (GHole 0) (reif t)
234+reifyTTBinderApp reif f [x, y]
235+ | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
236+reifyTTBinderApp reif f [t]
237+ | f == reflm "PVar" = liftM PVar (reif t)
238+reifyTTBinderApp reif f [t]
239+ | f == reflm "PVTy" = liftM PVTy (reif t)
240+reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
241+
242+reifyTTConst :: Term -> ElabD Const
243+reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
244+reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
245+reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
246+reifyTTConst t@(App _ _)
247+ | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
248+reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
249+
250+reifyTTConstApp :: Name -> Term -> ElabD Const
251+reifyTTConstApp f aty
252+ | f == reflm "AType" = fmap AType (reifyArithTy aty)
253+reifyTTConstApp f (Constant c@(I _))
254+ | f == reflm "I" = return $ c
255+reifyTTConstApp f (Constant c@(BI _))
256+ | f == reflm "BI" = return $ c
257+reifyTTConstApp f (Constant c@(Fl _))
258+ | f == reflm "Fl" = return $ c
259+reifyTTConstApp f (Constant c@(I _))
260+ | f == reflm "Ch" = return $ c
261+reifyTTConstApp f (Constant c@(Str _))
262+ | f == reflm "Str" = return $ c
263+reifyTTConstApp f (Constant c@(B8 _))
264+ | f == reflm "B8" = return $ c
265+reifyTTConstApp f (Constant c@(B16 _))
266+ | f == reflm "B16" = return $ c
267+reifyTTConstApp f (Constant c@(B32 _))
268+ | f == reflm "B32" = return $ c
269+reifyTTConstApp f (Constant c@(B64 _))
270+ | f == reflm "B64" = return $ c
271+reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
272+
273+reifyArithTy :: Term -> ElabD ArithTy
274+reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
275+reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
276+reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
277+
278+reifyNativeTy :: Term -> ElabD NativeTy
279+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
280+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
281+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
282+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
283+reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
284+
285+reifyIntTy :: Term -> ElabD IntTy
286+reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
287+reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
288+reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
289+reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
290+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
291+
292+reifyTTUExp :: Term -> ElabD UExp
293+reifyTTUExp t@(App _ _)
294+ = case unApply t of
295+ (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
296+ (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
297+ _ -> fail ("Unknown reflection type universe expression: " ++ show t)
298+reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
299+
300+-- | Create a reflected call to a named function/constructor
301+reflCall :: String -> [Raw] -> Raw
302+reflCall funName args
303+ = raw_apply (Var (reflm funName)) args
304+
305+-- | Lift a term into its Language.Reflection.TT representation
306+reflect :: Term -> Raw
307+reflect = reflectTTQuote []
308+
309+-- | Lift a term into its Language.Reflection.Raw representation
310+reflectRaw :: Raw -> Raw
311+reflectRaw = reflectRawQuote []
312+
313+claimTT :: Name -> ElabD Name
314+claimTT n = do n' <- getNameFrom n
315+ claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
316+ return n'
317+
318+-- | Convert a reflected term to a more suitable form for pattern-matching.
319+-- In particular, the less-interesting bits are elaborated to _ patterns. This
320+-- happens to NameTypes, universe levels, names that are bound but not used,
321+-- and the type annotation field of the P constructor.
322+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
323+reflectTTQuotePattern unq (P _ n _)
324+ | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
325+ do fill (Var n) ; solve
326+ | otherwise =
327+ do tyannot <- claimTT (sMN 0 "pTyAnnot")
328+ movelast tyannot -- use a _ pattern here
329+ nt <- getNameFrom (sMN 0 "nt")
330+ claim nt (Var (reflm "NameType"))
331+ movelast nt -- use a _ pattern here
332+ n' <- getNameFrom (sMN 0 "n")
333+ claim n' (Var (reflm "TTName"))
334+ fill $ reflCall "P" [Var nt, Var n', Var tyannot]
335+ solve
336+ focus n'; reflectNameQuotePattern n
337+reflectTTQuotePattern unq (V n)
338+ = do fill $ reflCall "V" [RConstant (I n)]
339+ solve
340+reflectTTQuotePattern unq (Bind n b x)
341+ = do x' <- claimTT (sMN 0 "sc")
342+ movelast x'
343+ b' <- getNameFrom (sMN 0 "binder")
344+ claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
345+ (Var (sNS (sUN "TT") ["Reflection", "Language"])))
346+ if n `elem` freeNames x
347+ then do fill $ reflCall "Bind"
348+ [reflectName n,
349+ Var b',
350+ Var x']
351+ solve
352+ else do any <- getNameFrom (sMN 0 "anyName")
353+ claim any (Var (reflm "TTName"))
354+ movelast any
355+ fill $ reflCall "Bind"
356+ [Var any,
357+ Var b',
358+ Var x']
359+ solve
360+ focus x'; reflectTTQuotePattern unq x
361+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
362+reflectTTQuotePattern unq (App f x)
363+ = do f' <- claimTT (sMN 0 "f"); movelast f'
364+ x' <- claimTT (sMN 0 "x"); movelast x'
365+ fill $ reflCall "App" [Var f', Var x']
366+ solve
367+ focus f'; reflectTTQuotePattern unq f
368+ focus x'; reflectTTQuotePattern unq x
369+reflectTTQuotePattern unq (Constant c)
370+ = do fill $ reflCall "TConst" [reflectConstant c]
371+ solve
372+reflectTTQuotePattern unq (Proj t i)
373+ = do t' <- claimTT (sMN 0 "t"); movelast t'
374+ fill $ reflCall "Proj" [Var t', RConstant (I i)]
375+ solve
376+ focus t'; reflectTTQuotePattern unq t
377+reflectTTQuotePattern unq (Erased)
378+ = do erased <- claimTT (sMN 0 "erased")
379+ movelast erased
380+ fill $ (Var erased)
381+ solve
382+reflectTTQuotePattern unq (Impossible)
383+ = do fill $ Var (reflm "Impossible")
384+ solve
385+reflectTTQuotePattern unq (TType exp)
386+ = do ue <- getNameFrom (sMN 0 "uexp")
387+ claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
388+ movelast ue
389+ fill $ reflCall "TType" [Var ue]
390+ solve
391+reflectTTQuotePattern unq (UType u)
392+ = do uH <- getNameFrom (sMN 0 "someUniv")
393+ claim uH (Var (reflm "Universe"))
394+ movelast uH
395+ fill $ reflCall "UType" [Var uH]
396+ solve
397+ focus uH
398+ fill (Var (reflm (case u of
399+ NullType -> "NullType"
400+ UniqueType -> "UniqueType"
401+ AllTypes -> "AllTypes")))
402+ solve
403+
404+reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
405+reflectRawQuotePattern unq (Var n)
406+ -- the unquoted names already have types, just use them
407+ | n `elem` unq = do fill (Var n); solve
408+ | otherwise = do fill (reflCall "Var" [reflectName n]); solve
409+reflectRawQuotePattern unq (RBind n b sc) =
410+ do scH <- getNameFrom (sMN 0 "sc")
411+ claim scH (Var (reflm "Raw"))
412+ movelast scH
413+ bH <- getNameFrom (sMN 0 "binder")
414+ claim bH (RApp (Var (reflm "Binder"))
415+ (Var (reflm "Raw")))
416+ if n `elem` freeNamesR sc
417+ then do fill $ reflCall "RBind" [reflectName n,
418+ Var bH,
419+ Var scH]
420+ solve
421+ else do any <- getNameFrom (sMN 0 "anyName")
422+ claim any (Var (reflm "TTName"))
423+ movelast any
424+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]
425+ solve
426+ focus scH; reflectRawQuotePattern unq sc
427+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
428+ where freeNamesR (Var n) = [n]
429+ freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
430+ freeNamesR body \\ [n],
431+ freeNamesR t]
432+ freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
433+ (freeNamesR body \\ [n])
434+ freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
435+ freeNamesR RType = []
436+ freeNamesR (RUType _) = []
437+ freeNamesR (RForce r) = freeNamesR r
438+ freeNamesR (RConstant _) = []
439+reflectRawQuotePattern unq (RApp f x) =
440+ do fH <- getNameFrom (sMN 0 "f")
441+ claim fH (Var (reflm "Raw"))
442+ movelast fH
443+ xH <- getNameFrom (sMN 0 "x")
444+ claim xH (Var (reflm "Raw"))
445+ movelast xH
446+ fill $ reflCall "RApp" [Var fH, Var xH]
447+ solve
448+ focus fH; reflectRawQuotePattern unq f
449+ focus xH; reflectRawQuotePattern unq x
450+reflectRawQuotePattern unq RType =
451+ do fill (Var (reflm "RType"))
452+ solve
453+reflectRawQuotePattern unq (RUType univ) =
454+ do uH <- getNameFrom (sMN 0 "universe")
455+ claim uH (Var (reflm "Universe"))
456+ movelast uH
457+ fill $ reflCall "RUType" [Var uH]
458+ solve
459+ focus uH; fill (reflectUniverse univ); solve
460+reflectRawQuotePattern unq (RForce r) =
461+ do rH <- getNameFrom (sMN 0 "raw")
462+ claim rH (Var (reflm "Raw"))
463+ movelast rH
464+ fill $ reflCall "RForce" [Var rH]
465+ solve
466+ focus rH; reflectRawQuotePattern unq r
467+reflectRawQuotePattern unq (RConstant c) =
468+ do cH <- getNameFrom (sMN 0 "const")
469+ claim cH (Var (reflm "Constant"))
470+ movelast cH
471+ fill (reflCall "RConstant" [Var cH]); solve
472+ focus cH
473+ fill (reflectConstant c); solve
474+
475+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
476+reflectBinderQuotePattern q unq (Lam t)
477+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
478+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
479+ solve
480+ focus t'; q unq t
481+reflectBinderQuotePattern q unq (Pi _ t k)
482+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'
483+ k' <- claimTT (sMN 0 "k"); movelast k';
484+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
485+ solve
486+ focus t'; q unq t
487+reflectBinderQuotePattern q unq (Let x y)
488+ = do x' <- claimTT (sMN 0 "ty"); movelast x';
489+ y' <- claimTT (sMN 0 "v"); movelast y';
490+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
491+ solve
492+ focus x'; q unq x
493+ focus y'; q unq y
494+reflectBinderQuotePattern q unq (NLet x y)
495+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
496+ y' <- claimTT (sMN 0 "v"); movelast y'
497+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
498+ solve
499+ focus x'; q unq x
500+ focus y'; q unq y
501+reflectBinderQuotePattern q unq (Hole t)
502+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
503+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
504+ solve
505+ focus t'; q unq t
506+reflectBinderQuotePattern q unq (GHole _ t)
507+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
508+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
509+ solve
510+ focus t'; q unq t
511+reflectBinderQuotePattern q unq (Guess x y)
512+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
513+ y' <- claimTT (sMN 0 "v"); movelast y'
514+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
515+ solve
516+ focus x'; q unq x
517+ focus y'; q unq y
518+reflectBinderQuotePattern q unq (PVar t)
519+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
520+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
521+ solve
522+ focus t'; q unq t
523+reflectBinderQuotePattern q unq (PVTy t)
524+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
525+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
526+ solve
527+ focus t'; q unq t
528+
529+reflectUniverse :: Universe -> Raw
530+reflectUniverse u =
531+ (Var (reflm (case u of
532+ NullType -> "NullType"
533+ UniqueType -> "UniqueType"
534+ AllTypes -> "AllTypes")))
535+
536+-- | Create a reflected TT term, but leave refs to the provided name intact
537+reflectTTQuote :: [Name] -> Term -> Raw
538+reflectTTQuote unq (P nt n t)
539+ | n `elem` unq = Var n
540+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
541+reflectTTQuote unq (V n)
542+ = reflCall "V" [RConstant (I n)]
543+reflectTTQuote unq (Bind n b x)
544+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
545+reflectTTQuote unq (App f x)
546+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
547+reflectTTQuote unq (Constant c)
548+ = reflCall "TConst" [reflectConstant c]
549+reflectTTQuote unq (Proj t i)
550+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
551+reflectTTQuote unq (Erased) = Var (reflm "Erased")
552+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
553+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
554+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
555+
556+reflectRawQuote :: [Name] -> Raw -> Raw
557+reflectRawQuote unq (Var n)
558+ | n `elem` unq = Var n
559+ | otherwise = reflCall "Var" [reflectName n]
560+reflectRawQuote unq (RBind n b r) =
561+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
562+reflectRawQuote unq (RApp f x) =
563+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
564+reflectRawQuote unq RType = Var (reflm "RType")
565+reflectRawQuote unq (RUType u) =
566+ reflCall "RUType" [reflectUniverse u]
567+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
568+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
569+
570+reflectNameType :: NameType -> Raw
571+reflectNameType (Bound) = Var (reflm "Bound")
572+reflectNameType (Ref) = Var (reflm "Ref")
573+reflectNameType (DCon x y _)
574+ = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
575+reflectNameType (TCon x y)
576+ = reflCall "TCon" [RConstant (I x), RConstant (I y)]
577+
578+reflectName :: Name -> Raw
579+reflectName (UN s)
580+ = reflCall "UN" [RConstant (Str (str s))]
581+reflectName (NS n ns)
582+ = reflCall "NS" [ reflectName n
583+ , foldr (\ n s ->
584+ raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
585+ [ RConstant StrType, RConstant (Str n), s ])
586+ ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
587+ [ RConstant StrType ])
588+ (map str ns)
589+ ]
590+reflectName (MN i n)
591+ = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
592+reflectName (NErased) = Var (reflm "NErased")
593+reflectName n = Var (reflm "NErased") -- special name, not yet implemented
594+
595+-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
596+-- MNs corresponding to will care about the string but not the number. All
597+-- others become _.
598+reflectNameQuotePattern :: Name -> ElabD ()
599+reflectNameQuotePattern n@(UN s)
600+ = do fill $ reflectName n
601+ solve
602+reflectNameQuotePattern n@(NS _ _)
603+ = do fill $ reflectName n
604+ solve
605+reflectNameQuotePattern (MN _ n)
606+ = do i <- getNameFrom (sMN 0 "mnCounter")
607+ claim i (RConstant (AType (ATInt ITNative)))
608+ movelast i
609+ fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
610+ solve
611+reflectNameQuotePattern _ -- for all other names, match any
612+ = do nameHole <- getNameFrom (sMN 0 "name")
613+ claim nameHole (Var (reflm "TTName"))
614+ movelast nameHole
615+ fill (Var nameHole)
616+ solve
617+
618+reflectBinder :: Binder Term -> Raw
619+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
620+
621+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
622+reflectBinderQuote q ty unq (Lam t)
623+ = reflCall "Lam" [Var ty, q unq t]
624+reflectBinderQuote q ty unq (Pi _ t k)
625+ = reflCall "Pi" [Var ty, q unq t, q unq k]
626+reflectBinderQuote q ty unq (Let x y)
627+ = reflCall "Let" [Var ty, q unq x, q unq y]
628+reflectBinderQuote q ty unq (NLet x y)
629+ = reflCall "NLet" [Var ty, q unq x, q unq y]
630+reflectBinderQuote q ty unq (Hole t)
631+ = reflCall "Hole" [Var ty, q unq t]
632+reflectBinderQuote q ty unq (GHole _ t)
633+ = reflCall "GHole" [Var ty, q unq t]
634+reflectBinderQuote q ty unq (Guess x y)
635+ = reflCall "Guess" [Var ty, q unq x, q unq y]
636+reflectBinderQuote q ty unq (PVar t)
637+ = reflCall "PVar" [Var ty, q unq t]
638+reflectBinderQuote q ty unq (PVTy t)
639+ = reflCall "PVTy" [Var ty, q unq t]
640+
641+mkList :: Raw -> [Raw] -> Raw
642+mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
643+mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
644+ x)
645+ (mkList ty xs)
646+
647+reflectConstant :: Const -> Raw
648+reflectConstant c@(I _) = reflCall "I" [RConstant c]
649+reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
650+reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
651+reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
652+reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
653+reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
654+reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
655+reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
656+reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
657+reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
658+reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
659+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
660+reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
661+reflectConstant StrType = Var (reflm "StrType")
662+reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
663+reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
664+reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
665+reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
666+reflectConstant VoidType = Var (reflm "VoidType")
667+reflectConstant Forgot = Var (reflm "Forgot")
668+reflectConstant WorldType = Var (reflm "WorldType")
669+reflectConstant TheWorld = Var (reflm "TheWorld")
670+
671+reflectUExp :: UExp -> Raw
672+reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
673+reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
674+
675+-- | Reflect the environment of a proof into a List (TTName, Binder TT)
676+reflectEnv :: Env -> Raw
677+reflectEnv = foldr consToEnvList emptyEnvList
678+ where
679+ consToEnvList :: (Name, Binder Term) -> Raw -> Raw
680+ consToEnvList (n, b) l
681+ = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
682+ [ envTupleType
683+ , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
684+ , (RApp (Var $ reflm "Binder")
685+ (Var $ reflm "TT"))
686+ , reflectName n
687+ , reflectBinder b
688+ ]
689+ , l
690+ ]
691+
692+ emptyEnvList :: Raw
693+ emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
694+ [envTupleType]
695+
696+-- | Reflect an error into the internal datatype of Idris -- TODO
697+rawBool :: Bool -> Raw
698+rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
699+rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
700+
701+rawNil :: Raw -> Raw
702+rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
703+
704+rawCons :: Raw -> Raw -> Raw -> Raw
705+rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
706+
707+rawList :: Raw -> [Raw] -> Raw
708+rawList ty = foldr (rawCons ty) (rawNil ty)
709+
710+rawPairTy :: Raw -> Raw -> Raw
711+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
712+
713+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
714+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
715+
716+reflectCtxt :: [(Name, Type)] -> Raw
717+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
718+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
719+ (reflectName n, reflect t)))
720+ ctxt)
721+
722+reflectErr :: Err -> Raw
723+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
724+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
725+reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
726+ raw_apply (Var $ reflErrName "CantUnify")
727+ [ rawBool b
728+ , reflect t1
729+ , reflect t2
730+ , reflectErr e
731+ , reflectCtxt ctxt
732+ , RConstant (I i)]
733+reflectErr (InfiniteUnify n tm ctxt) =
734+ raw_apply (Var $ reflErrName "InfiniteUnify")
735+ [ reflectName n
736+ , reflect tm
737+ , reflectCtxt ctxt
738+ ]
739+reflectErr (CantConvert t t' ctxt) =
740+ raw_apply (Var $ reflErrName "CantConvert")
741+ [ reflect t
742+ , reflect t'
743+ , reflectCtxt ctxt
744+ ]
745+reflectErr (CantSolveGoal t ctxt) =
746+ raw_apply (Var $ reflErrName "CantSolveGoal")
747+ [ reflect t
748+ , reflectCtxt ctxt
749+ ]
750+reflectErr (UnifyScope n n' t ctxt) =
751+ raw_apply (Var $ reflErrName "UnifyScope")
752+ [ reflectName n
753+ , reflectName n'
754+ , reflect t
755+ , reflectCtxt ctxt
756+ ]
757+reflectErr (CantInferType str) =
758+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
759+reflectErr (NonFunctionType t t') =
760+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
761+reflectErr (NotEquality t t') =
762+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
763+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
764+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
765+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
766+reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
767+reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
768+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
769+reflectErr (NotInjective t1 t2 t3) =
770+ raw_apply (Var $ reflErrName "NotInjective")
771+ [ reflect t1
772+ , reflect t2
773+ , reflect t3
774+ ]
775+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
776+reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
777+reflectErr (CantResolveAlts ss) =
778+ raw_apply (Var $ reflErrName "CantResolveAlts")
779+ [rawList (Var $ reflm "TTName") (map reflectName ss)]
780+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
781+reflectErr (NoEliminator str t)
782+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
783+ reflect t]
784+reflectErr UniverseError = Var $ reflErrName "UniverseError"
785+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
786+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
787+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
788+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
789+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
790+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
791+reflectErr (ProviderError str) =
792+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
793+reflectErr (LoadingFailed str err) =
794+ raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
795+reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
796+
797+-- | Reflect a file context
798+reflectFC :: FC -> Raw
799+reflectFC fc = raw_apply (Var (reflm "FileLoc"))
800+ [ RConstant (Str (fc_fname fc))
801+ , raw_apply (Var pairCon) $
802+ [intTy, intTy] ++
803+ map (RConstant . I)
804+ [ fst (fc_start fc)
805+ , snd (fc_start fc)
806+ ]
807+ , raw_apply (Var pairCon) $
808+ [intTy, intTy] ++
809+ map (RConstant . I)
810+ [ fst (fc_end fc)
811+ , snd (fc_end fc)
812+ ]
813+ ]
814+ where intTy = RConstant (AType (ATInt ITNative))
815+
816+fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
817+fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
818+ | just == txt "Just" = Just tm
819+fromTTMaybe x = Nothing
820+
821+reflErrName :: String -> Name
822+reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
823+
824+-- | Attempt to reify a report part from TT to the internal
825+-- representation. Not in Idris or ElabD monads because it should be usable
826+-- from either.
827+reifyReportPart :: Term -> Either Err ErrorReportPart
828+reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
829+ Right (TextPart msg)
830+reifyReportPart (App (P (DCon _ _ _) n _) ttn)
831+ | n == reflm "NamePart" =
832+ case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
833+ Error e -> Left . InternalMsg $
834+ "could not reify name term " ++
835+ show ttn ++
836+ " when reflecting an error:" ++ show e
837+ OK (n', _)-> Right $ NamePart n'
838+reifyReportPart (App (P (DCon _ _ _) n _) tm)
839+ | n == reflm "TermPart" =
840+ case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
841+ Error e -> Left . InternalMsg $
842+ "could not reify reflected term " ++
843+ show tm ++
844+ " when reflecting an error:" ++ show e
845+ OK (tm', _) -> Right $ TermPart tm'
846+reifyReportPart (App (P (DCon _ _ _) n _) tm)
847+ | n == reflm "SubReport" =
848+ case unList tm of
849+ Just xs -> do subParts <- mapM reifyReportPart xs
850+ Right (SubReport subParts)
851+ Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
852+reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
853+
854+reifyTyDecl :: Term -> ElabD RTyDecl
855+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
856+ | n == tacN "Declare" =
857+ do tyN' <- reifyTTName tyN
858+ args' <- case unList args of
859+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
860+ Just xs -> mapM reifyRArg xs
861+ ret' <- reifyRaw ret
862+ return $ RDeclare tyN' args' ret'
863+ where reifyRArg :: Term -> ElabD RArg
864+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)
865+ | n == tacN "Explicit" = liftM2 RExplicit
866+ (reifyTTName argN)
867+ (reifyRaw argTy)
868+ | n == tacN "Implicit" = liftM2 RImplicit
869+ (reifyTTName argN)
870+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
871+ (reifyTTName argN)
872+ (reifyRaw argTy)
873+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
874+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
875+
876+reifyFunDefn :: Term -> ElabD RFunDefn
877+reifyFunDefn (App (App (P _ n _) fnN) clauses)
878+ | n == tacN "DefineFun" =
879+ do fnN' <- reifyTTName fnN
880+ clauses' <- case unList clauses of
881+ Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
882+ Just cs -> mapM reifyC cs
883+ return $ RDefineFun fnN' clauses'
884+ where reifyC :: Term -> ElabD RFunClause
885+ reifyC (App (App (P (DCon _ _ _) n _) lhs) rhs)
886+ | n == tacN "MkFunClause" = liftM2 RMkFunClause
887+ (reifyRaw lhs)
888+ (reifyRaw rhs)
889+ reifyC (App (P (DCon _ _ _) n _) lhs)
890+ | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
891+ reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
892+reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
893+
894+envTupleType :: Raw
895+envTupleType
896+ = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
897+ , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
898+ ]
test/tactics001/Tactics.idr+10−10
@@ -1,6 +1,6 @@
1module Tactics
1module Tactics
2
2
3−import Language.Reflection.Tactical
3+import Language.Reflection.Elab
4
4
5import Data.Vect
5import Data.Vect
6
6
@@ -18,24 +18,24 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
19plusZeroRightNeutralNew Z = Refl
19plusZeroRightNeutralNew Z = Refl
20plusZeroRightNeutralNew (S k) =
20plusZeroRightNeutralNew (S k) =
21− %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
22− fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
22+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
23− solve)
23+ solve)
24
24
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
26plusSuccRightSuccNew Z k = Refl
26plusSuccRightSuccNew Z k = Refl
27plusSuccRightSuccNew (S j) k =
27plusSuccRightSuccNew (S j) k =
28− %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
28+ %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
29− fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
29+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
30− solve)
30+ solve)
31
31
32-- Test that side effects in new tactics work
32-- Test that side effects in new tactics work
33
33
34mkDecl : ()
34mkDecl : ()
35−mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
35+mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
36 [Implicit (UN "z") `(Nat)]
36 [Implicit (UN "z") `(Nat)]
37 `(Vect ~(Var (UN "z")) ())
37 `(Vect ~(Var (UN "z")) ())
38− fill `(() : ())
38+ fill `(() : ())
39− solve)
39+ solve)
40
40
41repUnit = pure ()
41repUnit = pure ()