git.iko.soy/Idris-dev
on master help sign in
Support nested quasiquotation
7383b1cDavid Raymond Christiansen
src/Idris/AbsSyntaxTree.hs+2−2
compare with master
unifiedsplit
@@ -1019,14 +1019,14 @@ data SyntaxInfo = Syn { using :: [Using],
1019 maxline :: Maybe Int,
1019 maxline :: Maybe Int,
1020 mut_nesting :: Int,
1020 mut_nesting :: Int,
1021 dsl_info :: DSL,
1021 dsl_info :: DSL,
1022− syn_in_quasiquote :: Bool }
1022+ syn_in_quasiquote :: Int }
1023 deriving Show
1023 deriving Show
1024{-!
1024{-!
1025deriving instance NFData SyntaxInfo
1025deriving instance NFData SyntaxInfo
1026deriving instance Binary SyntaxInfo
1026deriving instance Binary SyntaxInfo
1027!-}
1027!-}
1028
1028
1029−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
1029+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1030
1030
1031expandNS :: SyntaxInfo -> Name -> Name
1031expandNS :: SyntaxInfo -> Name -> Name
1032expandNS syn n@(NS _ _) = n
1032expandNS syn n@(NS _ _) = n
src/Idris/ElabQuasiquote.hs+125−122
@@ -5,167 +5,170 @@ import Idris.Core.TT
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6
6
7
7
8−extract1 :: (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
8+extract1 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9−extract1 c tm = do (tm', ex) <- extractUnquotes tm
9+extract1 n c tm = do (tm', ex) <- extractUnquotes n tm
10− return (c tm', ex)
10+ return (c tm', ex)
11
11
12−extract2 :: (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
12+extract2 :: Int -> (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
13−extract2 c a b = do (a', ex1) <- extractUnquotes a
13+extract2 n c a b = do (a', ex1) <- extractUnquotes n a
14− (b', ex2) <- extractUnquotes b
14+ (b', ex2) <- extractUnquotes n b
15− return (c a' b', ex1 ++ ex2)
15+ return (c a' b', ex1 ++ ex2)
16
16
17−extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
17+extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
18−extractTUnquotes (Rewrite t) = extract1 Rewrite t
18+extractTUnquotes n (Rewrite t) = extract1 n Rewrite t
19−extractTUnquotes (Induction t) = extract1 Induction t
19+extractTUnquotes n (Induction t) = extract1 n Induction t
20−extractTUnquotes (LetTac n t) = extract1 (LetTac n) t
20+extractTUnquotes n (LetTac name t) = extract1 n (LetTac name) t
21−extractTUnquotes (LetTacTy n t1 t2) = extract2 (LetTacTy n) t1 t2
21+extractTUnquotes n (LetTacTy name t1 t2) = extract2 n (LetTacTy name) t1 t2
22−extractTUnquotes (Exact tm) = extract1 Exact tm
22+extractTUnquotes n (Exact tm) = extract1 n Exact tm
23−extractTUnquotes (Try tac1 tac2)
23+extractTUnquotes n (Try tac1 tac2)
24− = do (tac1', ex1) <- extractTUnquotes tac1
24+ = do (tac1', ex1) <- extractTUnquotes n tac1
25− (tac2', ex2) <- extractTUnquotes tac2
25+ (tac2', ex2) <- extractTUnquotes n tac2
26 return (Try tac1' tac2', ex1 ++ ex2)
26 return (Try tac1' tac2', ex1 ++ ex2)
27−extractTUnquotes (TSeq tac1 tac2)
27+extractTUnquotes n (TSeq tac1 tac2)
28− = do (tac1', ex1) <- extractTUnquotes tac1
28+ = do (tac1', ex1) <- extractTUnquotes n tac1
29− (tac2', ex2) <- extractTUnquotes tac2
29+ (tac2', ex2) <- extractTUnquotes n tac2
30 return (TSeq tac1' tac2', ex1 ++ ex2)
30 return (TSeq tac1' tac2', ex1 ++ ex2)
31−extractTUnquotes (ApplyTactic t) = extract1 ApplyTactic t
31+extractTUnquotes n (ApplyTactic t) = extract1 n ApplyTactic t
32−extractTUnquotes (ByReflection t) = extract1 ByReflection t
32+extractTUnquotes n (ByReflection t) = extract1 n ByReflection t
33−extractTUnquotes (Reflect t) = extract1 Reflect t
33+extractTUnquotes n (Reflect t) = extract1 n Reflect t
34−extractTUnquotes (GoalType s tac)
34+extractTUnquotes n (GoalType s tac)
35− = do (tac', ex) <- extractTUnquotes tac
35+ = do (tac', ex) <- extractTUnquotes n tac
36 return (GoalType s tac', ex)
36 return (GoalType s tac', ex)
37−extractTUnquotes (TCheck t) = extract1 TCheck t
37+extractTUnquotes n (TCheck t) = extract1 n TCheck t
38−extractTUnquotes (TEval t) = extract1 TEval t
38+extractTUnquotes n (TEval t) = extract1 n TEval t
39−extractTUnquotes tac = return (tac, []) -- the rest don't contain PTerms
39+extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms
40
40
41−extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
41+extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
42−extractPArgUnquotes (PImp p m opts n t) =
42+extractPArgUnquotes d (PImp p m opts n t) =
43− do (t', ex) <- extractUnquotes t
43+ do (t', ex) <- extractUnquotes d t
44 return (PImp p m opts n t', ex)
44 return (PImp p m opts n t', ex)
45−extractPArgUnquotes (PExp p opts n t) =
45+extractPArgUnquotes d (PExp p opts n t) =
46− do (t', ex) <- extractUnquotes t
46+ do (t', ex) <- extractUnquotes d t
47 return (PExp p opts n t', ex)
47 return (PExp p opts n t', ex)
48−extractPArgUnquotes (PConstraint p opts n t) =
48+extractPArgUnquotes d (PConstraint p opts n t) =
49− do (t', ex) <- extractUnquotes t
49+ do (t', ex) <- extractUnquotes d t
50 return (PConstraint p opts n t', ex)
50 return (PConstraint p opts n t', ex)
51−extractPArgUnquotes (PTacImplicit p opts n scpt t) =
51+extractPArgUnquotes d (PTacImplicit p opts n scpt t) =
52− do (scpt', ex1) <- extractUnquotes scpt
52+ do (scpt', ex1) <- extractUnquotes d scpt
53− (t', ex2) <- extractUnquotes t
53+ (t', ex2) <- extractUnquotes d t
54 return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
54 return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
55
55
56−extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
56+extractDoUnquotes :: Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
57−extractDoUnquotes (DoExp fc tm)
57+extractDoUnquotes d (DoExp fc tm)
58− = do (tm', ex) <- extractUnquotes tm
58+ = do (tm', ex) <- extractUnquotes d tm
59 return (DoExp fc tm', ex)
59 return (DoExp fc tm', ex)
60−extractDoUnquotes (DoBind fc n tm)
60+extractDoUnquotes d (DoBind fc n tm)
61− = do (tm', ex) <- extractUnquotes tm
61+ = do (tm', ex) <- extractUnquotes d tm
62 return (DoBind fc n tm', ex)
62 return (DoBind fc n tm', ex)
63−extractDoUnquotes (DoBindP fc t t' alts)
63+extractDoUnquotes d (DoBindP fc t t' alts)
64 = fail "Pattern-matching binds cannot be quasiquoted"
64 = fail "Pattern-matching binds cannot be quasiquoted"
65−extractDoUnquotes (DoLet fc n v b)
65+extractDoUnquotes d (DoLet fc n v b)
66− = do (v', ex1) <- extractUnquotes v
66+ = do (v', ex1) <- extractUnquotes d v
67− (b', ex2) <- extractUnquotes b
67+ (b', ex2) <- extractUnquotes d b
68 return (DoLet fc n v' b', ex1 ++ ex2)
68 return (DoLet fc n v' b', ex1 ++ ex2)
69−extractDoUnquotes (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
69+extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
70
70
71
71
72−extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
72+extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
73−extractUnquotes (PLam n ty body)
73+extractUnquotes n (PLam name ty body)
74− = do (ty', ex1) <- extractUnquotes ty
74+ = do (ty', ex1) <- extractUnquotes n ty
75− (body', ex2) <- extractUnquotes body
75+ (body', ex2) <- extractUnquotes n body
76− return (PLam n ty' body', ex1 ++ ex2)
76+ return (PLam name ty' body', ex1 ++ ex2)
77−extractUnquotes (PPi plicity n ty body)
77+extractUnquotes n (PPi plicity name ty body)
78− = do (ty', ex1) <- extractUnquotes ty
78+ = do (ty', ex1) <- extractUnquotes n ty
79− (body', ex2) <- extractUnquotes body
79+ (body', ex2) <- extractUnquotes n body
80− return (PPi plicity n ty' body', ex1 ++ ex2)
80+ return (PPi plicity name ty' body', ex1 ++ ex2)
81−extractUnquotes (PLet n ty val body)
81+extractUnquotes n (PLet name ty val body)
82− = do (ty', ex1) <- extractUnquotes ty
82+ = do (ty', ex1) <- extractUnquotes n ty
83− (val', ex2) <- extractUnquotes val
83+ (val', ex2) <- extractUnquotes n val
84− (body', ex3) <- extractUnquotes body
84+ (body', ex3) <- extractUnquotes n body
85− return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
85+ return (PLet name ty' val' body', ex1 ++ ex2 ++ ex3)
86−extractUnquotes (PTyped tm ty)
86+extractUnquotes n (PTyped tm ty)
87− = do (tm', ex1) <- extractUnquotes tm
87+ = do (tm', ex1) <- extractUnquotes n tm
88− (ty', ex2) <- extractUnquotes ty
88+ (ty', ex2) <- extractUnquotes n ty
89 return (PTyped tm' ty', ex1 ++ ex2)
89 return (PTyped tm' ty', ex1 ++ ex2)
90−extractUnquotes (PApp fc f args)
90+extractUnquotes n (PApp fc f args)
91− = do (f', ex1) <- extractUnquotes f
91+ = do (f', ex1) <- extractUnquotes n f
92− args' <- mapM extractPArgUnquotes args
92+ args' <- mapM (extractPArgUnquotes n) args
93 let (args'', exs) = unzip args'
93 let (args'', exs) = unzip args'
94 return (PApp fc f' args'', ex1 ++ concat exs)
94 return (PApp fc f' args'', ex1 ++ concat exs)
95−extractUnquotes (PAppBind fc f args)
95+extractUnquotes n (PAppBind fc f args)
96− = do (f', ex1) <- extractUnquotes f
96+ = do (f', ex1) <- extractUnquotes n f
97− args' <- mapM extractPArgUnquotes args
97+ args' <- mapM (extractPArgUnquotes n) args
98 let (args'', exs) = unzip args'
98 let (args'', exs) = unzip args'
99 return (PAppBind fc f' args'', ex1 ++ concat exs)
99 return (PAppBind fc f' args'', ex1 ++ concat exs)
100−extractUnquotes (PCase fc expr cases)
100+extractUnquotes n (PCase fc expr cases)
101− = do (expr', ex1) <- extractUnquotes expr
101+ = do (expr', ex1) <- extractUnquotes n expr
102 let (pats, rhss) = unzip cases
102 let (pats, rhss) = unzip cases
103− (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
103+ (pats', exs1) <- fmap unzip $ mapM (extractUnquotes n) pats
104− (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
104+ (rhss', exs2) <- fmap unzip $ mapM (extractUnquotes n) rhss
105 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
105 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
106−extractUnquotes (PRefl fc x)
106+extractUnquotes n (PRefl fc x)
107− = do (x', ex) <- extractUnquotes x
107+ = do (x', ex) <- extractUnquotes n x
108 return (PRefl fc x', ex)
108 return (PRefl fc x', ex)
109−extractUnquotes (PEq fc at bt a b)
109+extractUnquotes n (PEq fc at bt a b)
110− = do (at', ex1) <- extractUnquotes at
110+ = do (at', ex1) <- extractUnquotes n at
111− (bt', ex2) <- extractUnquotes bt
111+ (bt', ex2) <- extractUnquotes n bt
112− (a', ex1) <- extractUnquotes a
112+ (a', ex1) <- extractUnquotes n a
113− (b', ex2) <- extractUnquotes b
113+ (b', ex2) <- extractUnquotes n b
114 return (PEq fc at' bt' a' b', ex1 ++ ex2)
114 return (PEq fc at' bt' a' b', ex1 ++ ex2)
115−extractUnquotes (PRewrite fc x y z)
115+extractUnquotes n (PRewrite fc x y z)
116− = do (x', ex1) <- extractUnquotes x
116+ = do (x', ex1) <- extractUnquotes n x
117− (y', ex2) <- extractUnquotes y
117+ (y', ex2) <- extractUnquotes n y
118 case z of
118 case z of
119− Just zz -> do (z', ex3) <- extractUnquotes zz
119+ Just zz -> do (z', ex3) <- extractUnquotes n zz
120 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
120 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
121 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
121 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
122−extractUnquotes (PPair fc info l r)
122+extractUnquotes n (PPair fc info l r)
123− = do (l', ex1) <- extractUnquotes l
123+ = do (l', ex1) <- extractUnquotes n l
124− (r', ex2) <- extractUnquotes r
124+ (r', ex2) <- extractUnquotes n r
125 return (PPair fc info l' r', ex1 ++ ex2)
125 return (PPair fc info l' r', ex1 ++ ex2)
126−extractUnquotes (PDPair fc info a b c)
126+extractUnquotes n (PDPair fc info a b c)
127− = do (a', ex1) <- extractUnquotes a
127+ = do (a', ex1) <- extractUnquotes n a
128− (b', ex2) <- extractUnquotes b
128+ (b', ex2) <- extractUnquotes n b
129− (c', ex3) <- extractUnquotes c
129+ (c', ex3) <- extractUnquotes n c
130 return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
130 return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
131−extractUnquotes (PAlternative b alts)
131+extractUnquotes n (PAlternative b alts)
132− = do alts' <- mapM extractUnquotes alts
132+ = do alts' <- mapM (extractUnquotes n) alts
133 let (alts'', exs) = unzip alts'
133 let (alts'', exs) = unzip alts'
134 return (PAlternative b alts'', concat exs)
134 return (PAlternative b alts'', concat exs)
135−extractUnquotes (PHidden tm)
135+extractUnquotes n (PHidden tm)
136− = do (tm', ex) <- extractUnquotes tm
136+ = do (tm', ex) <- extractUnquotes n tm
137 return (PHidden tm', ex)
137 return (PHidden tm', ex)
138−extractUnquotes (PGoal fc a n b)
138+extractUnquotes n (PGoal fc a name b)
139− = do (a', ex1) <- extractUnquotes a
139+ = do (a', ex1) <- extractUnquotes n a
140− (b', ex2) <- extractUnquotes b
140+ (b', ex2) <- extractUnquotes n b
141− return (PGoal fc a' n b', ex1 ++ ex2)
141+ return (PGoal fc a' name b', ex1 ++ ex2)
142−extractUnquotes (PDoBlock steps)
142+extractUnquotes n (PDoBlock steps)
143− = do steps' <- mapM extractDoUnquotes steps
143+ = do steps' <- mapM (extractDoUnquotes n) steps
144 let (steps'', exs) = unzip steps'
144 let (steps'', exs) = unzip steps'
145 return (PDoBlock steps'', concat exs)
145 return (PDoBlock steps'', concat exs)
146−extractUnquotes (PIdiom fc tm)
146+extractUnquotes n (PIdiom fc tm)
147− = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
147+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes n tm
148−extractUnquotes (PProof tacs)
148+extractUnquotes n (PProof tacs)
149− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
149+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
150 return (PProof tacs', concat exs)
150 return (PProof tacs', concat exs)
151−extractUnquotes (PTactics tacs)
151+extractUnquotes n (PTactics tacs)
152− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
152+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
153 return (PTactics tacs', concat exs)
153 return (PTactics tacs', concat exs)
154−extractUnquotes (PElabError err) = fail "Can't quasiquote an error"
154+extractUnquotes n (PElabError err) = fail "Can't quasiquote an error"
155−extractUnquotes (PCoerced tm)
155+extractUnquotes n (PCoerced tm)
156− = do (tm', ex) <- extractUnquotes tm
156+ = do (tm', ex) <- extractUnquotes n tm
157 return (PCoerced tm', ex)
157 return (PCoerced tm', ex)
158−extractUnquotes (PDisamb ns tm)
158+extractUnquotes n (PDisamb ns tm)
159− = do (tm', ex) <- extractUnquotes tm
159+ = do (tm', ex) <- extractUnquotes n tm
160 return (PDisamb ns tm', ex)
160 return (PDisamb ns tm', ex)
161−extractUnquotes (PUnifyLog tm)
161+extractUnquotes n (PUnifyLog tm)
162− = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
162+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes n tm
163−extractUnquotes (PNoImplicits tm)
163+extractUnquotes n (PNoImplicits tm)
164− = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
164+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes n tm
165−extractUnquotes (PQuasiquote _ _) = fail "Nested quasiquotes not supported"
165+extractUnquotes n (PQuasiquote tm goal)
166+ = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm
166−extractUnquotes (PUnquote tm) =
167+extractUnquotes n (PUnquote tm)
167− do n <- getNameFrom (sMN 0 "unquotation")
168+ | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")
168− return (PRef (fileFC "(unquote)") n, [(n, tm)])
169+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
170+ | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
169−extractUnquotes x = return (x, []) -- no subterms!
171+ extractUnquotes (n-1) tm
172+extractUnquotes n x = return (x, []) -- no subterms!
170
173
171
174
src/Idris/ElabTerm.hs+1−1
@@ -791,7 +791,7 @@ elab ist info emode opts fn tm
791 = do -- First extract the unquoted subterms, replacing them with fresh
791 = do -- First extract the unquoted subterms, replacing them with fresh
792 -- names in the quasiquoted term. Claim their reflections to be
792 -- names in the quasiquoted term. Claim their reflections to be
793 -- of type TT.
793 -- of type TT.
794− (t, unq) <- extractUnquotes t
794+ (t, unq) <- extractUnquotes 0 t
795 let unquoteNames = map fst unq
795 let unquoteNames = map fst unq
796 mapM_ (flip claim (Var tt)) unquoteNames
796 mapM_ (flip claim (Var tt)) unquoteNames
797
797
src/Idris/IBC.hs+2−2
@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)
32import Util.Zlib (decompressEither)
32import Util.Zlib (decompressEither)
33
33
34ibcVersion :: Word8
34ibcVersion :: Word8
35−ibcVersion = 81
35+ibcVersion = 82
36
36
37data IBCFile = IBCFile { ver :: Word8,
37data IBCFile = IBCFile { ver :: Word8,
38 sourcefile :: FilePath,
38 sourcefile :: FilePath,
@@ -1293,7 +1293,7 @@ instance Binary SyntaxInfo where
1293 x5 <- get
1293 x5 <- get
1294 x6 <- get
1294 x6 <- get
1295 x7 <- get
1295 x7 <- get
1296− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 False)
1296+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)
1297
1297
1298instance (Binary t) => Binary (PClause' t) where
1298instance (Binary t) => Binary (PClause' t) where
1299 put x
1299 put x
src/Idris/ParseExpr.hs+5−5
@@ -605,9 +605,9 @@ constraintArg syn = do symbol "@{"
605
605
606-}
606-}
607quasiquote :: SyntaxInfo -> IdrisParser PTerm
607quasiquote :: SyntaxInfo -> IdrisParser PTerm
608−quasiquote syn = do guard (not (syn_in_quasiquote syn))
608+quasiquote syn = do symbol "`("
609− symbol "`("
610− e <- expr syn { syn_in_quasiquote = True , inPattern = False}
609+ e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
610+ inPattern = False }
611 g <- optional $ do
611 g <- optional $ do
612 symbol ":"
612 symbol ":"
613 expr syn { inPattern = False } -- don't allow antiquotes
613 expr syn { inPattern = False } -- don't allow antiquotes
@@ -621,9 +621,9 @@ quasiquote syn = do guard (not (syn_in_quasiquote syn))
621
621
622-}
622-}
623unquote :: SyntaxInfo -> IdrisParser PTerm
623unquote :: SyntaxInfo -> IdrisParser PTerm
624−unquote syn = do guard (syn_in_quasiquote syn)
624+unquote syn = do guard (syn_in_quasiquote syn > 0)
625 symbol "~"
625 symbol "~"
626− e <- simpleExpr syn { syn_in_quasiquote = False }
626+ e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
627 return $ PUnquote e
627 return $ PUnquote e
628 <?> "unquotation"
628 <?> "unquotation"
629
629