@@ -1,12 +1,42 @@
1module Idris.ElabQuasiquote (extractUnquotes) where
1module Idris.ElabQuasiquote (extractUnquotes) where
3−import Idris.Core.Elaborate
3+import Idris.Core.Elaborate hiding (Tactic(..))
4import Idris.Core.TT
4import Idris.Core.TT
5import Idris.AbsSyntax
5import Idris.AbsSyntax
8+extract1 :: (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9+extract1 c tm = do (tm', ex) <- extractUnquotes tm
12+extract2 :: (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
13+extract2 c a b = do (a', ex1) <- extractUnquotes a
14+ (b', ex2) <- extractUnquotes b
15+ return (c a' b', ex1 ++ ex2)
8extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
17extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
9−extractTUnquotes = undefined -- TODO
18+extractTUnquotes (Rewrite t) = extract1 Rewrite t
19+extractTUnquotes (Induction t) = extract1 Induction t
20+extractTUnquotes (LetTac n t) = extract1 (LetTac n) t
21+extractTUnquotes (LetTacTy n t1 t2) = extract2 (LetTacTy n) t1 t2
22+extractTUnquotes (Exact tm) = extract1 Exact tm
23+extractTUnquotes (Try tac1 tac2)
24+ = do (tac1', ex1) <- extractTUnquotes tac1
25+ (tac2', ex2) <- extractTUnquotes tac2
26+ return (Try tac1' tac2', ex1 ++ ex2)
27+extractTUnquotes (TSeq tac1 tac2)
28+ = do (tac1', ex1) <- extractTUnquotes tac1
29+ (tac2', ex2) <- extractTUnquotes tac2
30+ return (TSeq tac1' tac2', ex1 ++ ex2)
31+extractTUnquotes (ApplyTactic t) = extract1 ApplyTactic t
32+extractTUnquotes (ByReflection t) = extract1 ByReflection t
33+extractTUnquotes (Reflect t) = extract1 Reflect t
34+extractTUnquotes (GoalType s tac)
35+ = do (tac', ex) <- extractTUnquotes tac
36+ return (GoalType s tac', ex)
37+extractTUnquotes (TCheck t) = extract1 TCheck t
38+extractTUnquotes (TEval t) = extract1 TEval t
39+extractTUnquotes tac = return (tac, []) -- the rest don't contain PTerms
11extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
41extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
12extractPArgUnquotes (PImp p m opts n t) =
42extractPArgUnquotes (PImp p m opts n t) =
@@ -31,9 +61,12 @@ extractDoUnquotes (DoBind fc n tm)
31 = do (tm', ex) <- extractUnquotes tm
61 = do (tm', ex) <- extractUnquotes tm
32 return (DoBind fc n tm', ex)
62 return (DoBind fc n tm', ex)
33extractDoUnquotes (DoBindP fc t t' alts)
63extractDoUnquotes (DoBindP fc t t' alts)
34− = fail "not done yet" -- TODO
64+ = fail "Pattern-matching binds cannot be quasiquoted"
35−extractDoUnquotes (DoLet fc n t t') = fail "not done yet" -- TODO
65+extractDoUnquotes (DoLet fc n v b)
66+ = do (v', ex1) <- extractUnquotes v
67+ (b', ex2) <- extractUnquotes b
68+ return (DoLet fc n v' b', ex1 ++ ex2)
36−extractDoUnquotes (DoLetP fc t t') = fail "not done yet" -- TODO
69+extractDoUnquotes (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
39extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
72extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
@@ -110,11 +143,19 @@ extractUnquotes (PDoBlock steps)
110 return (PDoBlock steps'', concat exs)
143 return (PDoBlock steps'', concat exs)
111extractUnquotes (PIdiom fc tm)
144extractUnquotes (PIdiom fc tm)
112 = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
145 = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
113−extractUnquotes (PProof tacs) = fail "not implemented yet"
146+extractUnquotes (PProof tacs)
147+ = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
148+ return (PProof tacs', concat exs)
114−extractUnquotes (PTactics tacs) = fail "not implemented yet"
149+extractUnquotes (PTactics tacs)
150+ = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
151+ return (PTactics tacs', concat exs)
115−extractUnquotes (PElabError err) = fail "not implemented yet"
152+extractUnquotes (PElabError err) = fail "Can't quasiquote an error"
116−extractUnquotes (PCoerced tm) = fail "not implemented yet"
153+extractUnquotes (PCoerced tm)
154+ = do (tm', ex) <- extractUnquotes tm
155+ return (PCoerced tm', ex)
117−extractUnquotes (PDisamb xs tm) = fail "not implemented yet"
156+extractUnquotes (PDisamb ns tm)
157+ = do (tm', ex) <- extractUnquotes tm
158+ return (PDisamb ns tm', ex)
118extractUnquotes (PUnifyLog tm)
159extractUnquotes (PUnifyLog tm)
119 = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
160 = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
120extractUnquotes (PNoImplicits tm)
161extractUnquotes (PNoImplicits tm)