@@ -0,0 +1,128 @@
1+module Idris.ElabQuasiquote (extractUnquotes) where
2+
3+import Idris.Core.Elaborate
4+import Idris.Core.TT
5+import Idris.AbsSyntax
6+
7+
8+extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
9+extractTUnquotes = undefined -- TODO
10+
11+extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
12+extractPArgUnquotes (PImp p m opts n t) =
13+ do (t', ex) <- extractUnquotes t
14+ return (PImp p m opts n t', ex)
15+extractPArgUnquotes (PExp p opts n t) =
16+ do (t', ex) <- extractUnquotes t
17+ return (PExp p opts n t', ex)
18+extractPArgUnquotes (PConstraint p opts n t) =
19+ do (t', ex) <- extractUnquotes t
20+ return (PConstraint p opts n t', ex)
21+extractPArgUnquotes (PTacImplicit p opts n scpt t) =
22+ do (scpt', ex1) <- extractUnquotes scpt
23+ (t', ex2) <- extractUnquotes t
24+ return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
25+
26+extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
27+extractDoUnquotes (DoExp fc tm)
28+ = do (tm', ex) <- extractUnquotes tm
29+ return (DoExp fc tm', ex)
30+extractDoUnquotes (DoBind fc n tm)
31+ = do (tm', ex) <- extractUnquotes tm
32+ return (DoBind fc n tm', ex)
33+extractDoUnquotes (DoBindP fc t t' alts)
34+ = fail "not done yet" -- TODO
35+extractDoUnquotes (DoLet fc n t t') = fail "not done yet" -- TODO
36+extractDoUnquotes (DoLetP fc t t') = fail "not done yet" -- TODO
37+
38+
39+extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
40+extractUnquotes (PLam n ty body)
41+ = do (ty', ex1) <- extractUnquotes ty
42+ (body', ex2) <- extractUnquotes body
43+ return (PLam n ty' body', ex1 ++ ex2)
44+extractUnquotes (PPi plicity n ty body)
45+ = do (ty', ex1) <- extractUnquotes ty
46+ (body', ex2) <- extractUnquotes body
47+ return (PPi plicity n ty' body', ex1 ++ ex2)
48+extractUnquotes (PLet n ty val body)
49+ = do (ty', ex1) <- extractUnquotes ty
50+ (val', ex2) <- extractUnquotes val
51+ (body', ex3) <- extractUnquotes body
52+ return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
53+extractUnquotes (PTyped tm ty)
54+ = do (tm', ex1) <- extractUnquotes tm
55+ (ty', ex2) <- extractUnquotes ty
56+ return (PTyped tm' ty', ex1 ++ ex2)
57+extractUnquotes (PApp fc f args)
58+ = do (f', ex1) <- extractUnquotes f
59+ args' <- mapM extractPArgUnquotes args
60+ let (args'', exs) = unzip args'
61+ return (PApp fc f' args'', ex1 ++ concat exs)
62+extractUnquotes (PAppBind fc f args)
63+ = do (f', ex1) <- extractUnquotes f
64+ args' <- mapM extractPArgUnquotes args
65+ let (args'', exs) = unzip args'
66+ return (PAppBind fc f' args'', ex1 ++ concat exs)
67+extractUnquotes (PCase fc expr cases)
68+ = do (expr', ex1) <- extractUnquotes expr
69+ let (pats, rhss) = unzip cases
70+ (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
71+ (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
72+ return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
73+extractUnquotes (PRefl fc x)
74+ = do (x', ex) <- extractUnquotes x
75+ return (PRefl fc x', ex)
76+extractUnquotes (PEq fc a b)
77+ = do (a', ex1) <- extractUnquotes a
78+ (b', ex2) <- extractUnquotes b
79+ return (PEq fc a' b', ex1 ++ ex2)
80+extractUnquotes (PRewrite fc x y z)
81+ = do (x', ex1) <- extractUnquotes x
82+ (y', ex2) <- extractUnquotes y
83+ case z of
84+ Just zz -> do (z', ex3) <- extractUnquotes zz
85+ return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
86+ Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
87+extractUnquotes (PPair fc info l r)
88+ = do (l', ex1) <- extractUnquotes l
89+ (r', ex2) <- extractUnquotes r
90+ return (PPair fc info l' r', ex1 ++ ex2)
91+extractUnquotes (PDPair fc info a b c)
92+ = do (a', ex1) <- extractUnquotes a
93+ (b', ex2) <- extractUnquotes b
94+ (c', ex3) <- extractUnquotes c
95+ return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
96+extractUnquotes (PAlternative b alts)
97+ = do alts' <- mapM extractUnquotes alts
98+ let (alts'', exs) = unzip alts'
99+ return (PAlternative b alts'', concat exs)
100+extractUnquotes (PHidden tm)
101+ = do (tm', ex) <- extractUnquotes tm
102+ return (PHidden tm', ex)
103+extractUnquotes (PGoal fc a n b)
104+ = do (a', ex1) <- extractUnquotes a
105+ (b', ex2) <- extractUnquotes b
106+ return (PGoal fc a' n b', ex1 ++ ex2)
107+extractUnquotes (PDoBlock steps)
108+ = do steps' <- mapM extractDoUnquotes steps
109+ let (steps'', exs) = unzip steps'
110+ return (PDoBlock steps'', concat exs)
111+extractUnquotes (PIdiom fc tm)
112+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
113+extractUnquotes (PProof tacs) = fail "not implemented yet"
114+extractUnquotes (PTactics tacs) = fail "not implemented yet"
115+extractUnquotes (PElabError err) = fail "not implemented yet"
116+extractUnquotes (PCoerced tm) = fail "not implemented yet"
117+extractUnquotes (PDisamb xs tm) = fail "not implemented yet"
118+extractUnquotes (PUnifyLog tm)
119+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
120+extractUnquotes (PNoImplicits tm)
121+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
122+extractUnquotes (PQuasiquote tm) = fail "Nested quasiquotes not supported"
123+extractUnquotes (PUnquote tm) =
124+ do n <- getNameFrom (sMN 0 "unquotation")
125+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
126+extractUnquotes x = return (x, []) -- no subterms!
127+
128+