git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1331 from david-christiansen/quasiquote

Quasiquote support

commit871c8b24213941a39ad4a9e7a546a094b3bceea0 authorDavid Christiansen <david@davidchristiansen.dk> dateSun 29 Jun 2014, 01:49 (12 years ago) parent86b1a78e08a18d
13 files changed+642−147
compare with master
unifiedsplit
CHANGELOG+5 idris.cabal+5 src/Idris/AbsSyntax.hs+68−64 src/Idris/AbsSyntaxTree.hs+8−3 src/Idris/Core/Elaborate.hs+1 src/Idris/DeepSeq.hs+4−3 src/Idris/ElabQuasiquote.hs+169 src/Idris/ElabTerm.hs+308−75 src/Idris/IBC.hs+2−2 src/Idris/ParseExpr.hs+29 test/quasiquote001/QuasiquoteBasics.idr+34 test/quasiquote001/expected+5 test/quasiquote001/run+4
CHANGELOG+5
@@ -10,6 +10,11 @@ New in 0.9.14:
1010* Experimental 'neweffects' library, with simplified API
1111* All new JavaScript backend (avoids callstack overflows)
1212* Add support for %lib directive for NodeJS
13+* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
14+ `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
15+ version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
16+ terms to splice in, while on the LHS they are patterns.
17+
1318
1419New in 0.9.13:
1520--------------
idris.cabal+5
@@ -415,6 +415,10 @@ Extra-source-files:
415415 test/proof004/*.idr
416416 test/proof004/expected
417417
418+ test/quasiquote001/run
419+ test/quasiquote001/*.idr
420+ test/quasiquote001/expected
421+
418422 test/records001/run
419423 test/records001/*.idr
420424 test/records001/expected
@@ -548,6 +552,7 @@ Library
548552 , Idris.Docs
549553 , Idris.Docstrings
550554 , Idris.ElabDecls
555+ , Idris.ElabQuasiquote
551556 , Idris.ElabTerm
552557 , Idris.Erasure
553558 , Idris.Error
src/Idris/AbsSyntax.hs+68−64
@@ -1270,6 +1270,7 @@ addImplBound ist ns = addImpl' False ns [] ist
12701270addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
12711271addImplBoundInf ist ns inf = addImpl' False ns inf ist
12721272
1273+-- | Add the implicit arguments to applications in the term
12731274addImpl :: IState -> PTerm -> PTerm
12741275addImpl = addImpl' False [] []
12751276
@@ -1277,86 +1278,89 @@ addImpl = addImpl' False [] []
12771278-- and *not* inside a PHidden
12781279
12791280addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1280−addImpl' inpat env infns ist ptm
1281− = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1281+addImpl' inpat env infns ist ptm
1282+ = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
12821283 where
1283− ai env ds (PRef fc f)
1284+ ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1285+ ai qq env ds (PRef fc f)
12841286 | f `elem` infns = PInferRef fc f
1285− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1286− ai env ds (PHidden (PRef fc f))
1287− | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1288− ai env ds (PEq fc l r)
1289− = let l' = ai env ds l
1290− r' = ai env ds r in
1287+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1288+ ai qq env ds (PHidden (PRef fc f))
1289+ | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1290+ ai qq env ds (PEq fc l r)
1291+ = let l' = ai qq env ds l
1292+ r' = ai qq env ds r in
12911293 PEq fc l' r'
1292− ai env ds (PRewrite fc l r g)
1293− = let l' = ai env ds l
1294− r' = ai env ds r
1295− g' = fmap (ai env ds) g in
1294+ ai qq env ds (PRewrite fc l r g)
1295+ = let l' = ai qq env ds l
1296+ r' = ai qq env ds r
1297+ g' = fmap (ai qq env ds) g in
12961298 PRewrite fc l' r' g'
1297− ai env ds (PTyped l r)
1298− = let l' = ai env ds l
1299− r' = ai env ds r in
1299+ ai qq env ds (PTyped l r)
1300+ = let l' = ai qq env ds l
1301+ r' = ai qq env ds r in
13001302 PTyped l' r'
1301− ai env ds (PPair fc p l r)
1302− = let l' = ai env ds l
1303− r' = ai env ds r in
1303+ ai qq env ds (PPair fc p l r)
1304+ = let l' = ai qq env ds l
1305+ r' = ai qq env ds r in
13041306 PPair fc p l' r'
1305− ai env ds (PDPair fc p l t r)
1306− = let l' = ai env ds l
1307− t' = ai env ds t
1308− r' = ai env ds r in
1307+ ai qq env ds (PDPair fc p l t r)
1308+ = let l' = ai qq env ds l
1309+ t' = ai qq env ds t
1310+ r' = ai qq env ds r in
13091311 PDPair fc p l' t' r'
1310− ai env ds (PAlternative a as)
1311− = let as' = map (ai env ds) as in
1312+ ai qq env ds (PAlternative a as)
1313+ = let as' = map (ai qq env ds) as in
13121314 PAlternative a as'
1313− ai env _ (PDisamb ds' as) = ai env ds' as
1314− ai env ds (PApp fc (PInferRef _ f) as)
1315− = let as' = map (fmap (ai env ds)) as in
1315+ ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1316+ ai qq env ds (PApp fc (PInferRef _ f) as)
1317+ = let as' = map (fmap (ai qq env ds)) as in
13161318 PApp fc (PInferRef fc f) as'
1317− ai env ds (PApp fc ftm@(PRef _ f) as)
1318− | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1319+ ai qq env ds (PApp fc ftm@(PRef _ f) as)
1320+ | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
13191321 | not (f `elem` map fst env)
1320− = let as' = map (fmap (ai env ds)) as in
1321− handleErr $ aiFn inpat False ist fc f ds as'
1322+ = let as' = map (fmap (ai qq env ds)) as in
1323+ handleErr $ aiFn inpat False qq ist fc f ds as'
13221324 | Just (Just ty) <- lookup f env =
1323− let as' = map (fmap (ai env ds)) as
1325+ let as' = map (fmap (ai qq env ds)) as
13241326 arity = getPArity ty in
13251327 mkPApp fc arity ftm as'
1326− ai env ds (PApp fc f as)
1327− = let f' = ai env ds f
1328− as' = map (fmap (ai env ds)) as in
1328+ ai qq env ds (PApp fc f as)
1329+ = let f' = ai qq env ds f
1330+ as' = map (fmap (ai qq env ds)) as in
13291331 mkPApp fc 1 f' as'
1330− ai env ds (PCase fc c os)
1331− = let c' = ai env ds c in
1332+ ai qq env ds (PCase fc c os)
1333+ = let c' = ai qq env ds c in
13321334 -- leave os alone, because they get lifted into a new pattern match
13331335 -- definition which is passed through addImpl again with more scope
13341336 -- information
13351337 PCase fc c' os
1336− ai env ds (PLam n ty sc)
1337− = let ty' = ai env ds ty
1338− sc' = ai ((n, Just ty):env) ds sc in
1338+ ai qq env ds (PLam n ty sc)
1339+ = let ty' = ai qq env ds ty
1340+ sc' = ai qq ((n, Just ty):env) ds sc in
13391341 PLam n ty' sc'
1340− ai env ds (PLet n ty val sc)
1341− = let ty' = ai env ds ty
1342− val' = ai env ds val
1343− sc' = ai ((n, Just ty):env) ds sc in
1342+ ai qq env ds (PLet n ty val sc)
1343+ = let ty' = ai qq env ds ty
1344+ val' = ai qq env ds val
1345+ sc' = ai qq ((n, Just ty):env) ds sc in
13441346 PLet n ty' val' sc'
1345− ai env ds (PPi p n ty sc)
1346− = let ty' = ai env ds ty
1347− sc' = ai ((n, Just ty):env) ds sc in
1347+ ai qq env ds (PPi p n ty sc)
1348+ = let ty' = ai qq env ds ty
1349+ sc' = ai qq ((n, Just ty):env) ds sc in
13481350 PPi p n ty' sc'
1349− ai env ds (PGoal fc r n sc)
1350− = let r' = ai env ds r
1351− sc' = ai ((n, Nothing):env) ds sc in
1351+ ai qq env ds (PGoal fc r n sc)
1352+ = let r' = ai qq env ds r
1353+ sc' = ai qq ((n, Nothing):env) ds sc in
13521354 PGoal fc r' n sc'
1353− ai env ds (PHidden tm) = PHidden (ai env ds tm)
1354− ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1355− ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1356− ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1357− ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1358− ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1359− ai env ds tm = tm
1355+ ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1356+ ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)
1357+ ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)
1358+ ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1359+ ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1360+ ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1361+ ai qq env ds (PQuasiquote tm) = PQuasiquote (ai True env ds tm)
1362+ ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1363+ ai qq env ds tm = tm
13601364
13611365 handleErr (Left err) = PElabError err
13621366 handleErr (Right x) = x
@@ -1364,8 +1368,8 @@ addImpl' inpat env infns ist ptm
13641368-- if in a pattern, and there are no arguments, and there's no possible
13651369-- names with zero explicit arguments, don't add implicits.
13661370
1367−aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1368−aiFn inpat True ist fc f ds []
1371+aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1372+aiFn inpat True qq ist fc f ds []
13691373 = case lookupDef f (tt_ctxt ist) of
13701374 [] -> Right $ PPatvar fc f
13711375 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
@@ -1373,7 +1377,7 @@ aiFn inpat True ist fc f ds []
13731377 if (not (vname f) || tcname f
13741378 || any (conCaf (tt_ctxt ist)) ialts)
13751379-- any constructor alts || any allImp ialts))
1376− then aiFn inpat False ist fc f ds [] -- use it as a constructor
1380+ then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
13771381 else Right $ PPatvar fc f
13781382 where imp (PExp _ _ _ _) = False
13791383 imp _ = True
@@ -1382,14 +1386,14 @@ aiFn inpat True ist fc f ds []
13821386 constructor (TyDecl (DCon _ _) _) = True
13831387 constructor _ = False
13841388
1385− conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1389+ conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
13861390
13871391 vname (UN n) = True -- non qualified
13881392 vname _ = False
13891393
1390−aiFn inpat expat ist fc f ds as
1394+aiFn inpat expat qq ist fc f ds as
13911395 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1392−aiFn inpat expat ist fc f ds as
1396+aiFn inpat expat qq ist fc f ds as
13931397 -- This is where namespaces get resolved by adding PAlternative
13941398 = do let ns = lookupCtxtName f (idris_implicits ist)
13951399 let nh = filter (\(n, _) -> notHidden n) ns
src/Idris/AbsSyntaxTree.hs+8−3
@@ -702,6 +702,8 @@ data PTerm = PQuote Raw
702702 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
703703 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
704704 | PNoImplicits PTerm -- ^ never run implicit converions on the term
705+ | PQuasiquote PTerm -- ^ `(Term)
706+ | PUnquote PTerm -- ^ ,Term
705707 deriving Eq
706708
707709
@@ -969,14 +971,15 @@ data SyntaxInfo = Syn { using :: [Using],
969971 implicitAllowed :: Bool,
970972 maxline :: Maybe Int,
971973 mut_nesting :: Int,
972− dsl_info :: DSL }
974+ dsl_info :: DSL,
975+ syn_in_quasiquote :: Bool }
973976 deriving Show
974977{-!
975978deriving instance NFData SyntaxInfo
976979deriving instance Binary SyntaxInfo
977980!-}
978981
979−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL
982+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
980983
981984expandNS :: SyntaxInfo -> Name -> Name
982985expandNS syn n@(NS _ _) = n
@@ -1351,8 +1354,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13511354 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
13521355 prettySe p bnd (PCoerced t) = prettySe p bnd t
13531356 prettySe p bnd (PElabError s) = pretty s
1357+ prettySe p bnd (PQuasiquote t) = text "`(" <> prettySe p bnd t <> text ")"
1358+ prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
13541359
1355− prettySe p bnd _ = text "test"
1360+ prettySe p bnd _ = text "missing pretty-printer for term"
13561361
13571362 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
13581363 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
src/Idris/Core/Elaborate.hs+1
@@ -380,6 +380,7 @@ casetac tm = processTactic' (CaseTac tm)
380380equiv :: Raw -> Elab' aux ()
381381equiv tm = processTactic' (Equiv tm)
382382
383+-- | Turn the current hole into a pattern variable with the provided name, made unique if MN
383384patvar :: Name -> Elab' aux ()
384385patvar n = do env <- get_env
385386 hs <- get_holes
src/Idris/DeepSeq.hs+4−3
@@ -320,13 +320,14 @@ instance NFData Using where
320320 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
321321 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
322322
323−
324323instance NFData SyntaxInfo where
325− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
326325 = rnf x1 `seq`
327326 rnf x2 `seq`
328327 rnf x3 `seq`
329− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
328+ rnf x4 `seq`
329+ rnf x5 `seq`
330+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()
330331
331332
332333
src/Idris/ElabQuasiquote.hsnew file+169
@@ -0,0 +1,169 @@
1+module Idris.ElabQuasiquote (extractUnquotes) where
2+
3+import Idris.Core.Elaborate hiding (Tactic(..))
4+import Idris.Core.TT
5+import Idris.AbsSyntax
6+
7+
8+extract1 :: (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9+extract1 c tm = do (tm', ex) <- extractUnquotes tm
10+ return (c tm', ex)
11+
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)
16+
17+extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
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
40+
41+extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
42+extractPArgUnquotes (PImp p m opts n t) =
43+ do (t', ex) <- extractUnquotes t
44+ return (PImp p m opts n t', ex)
45+extractPArgUnquotes (PExp p opts n t) =
46+ do (t', ex) <- extractUnquotes t
47+ return (PExp p opts n t', ex)
48+extractPArgUnquotes (PConstraint p opts n t) =
49+ do (t', ex) <- extractUnquotes t
50+ return (PConstraint p opts n t', ex)
51+extractPArgUnquotes (PTacImplicit p opts n scpt t) =
52+ do (scpt', ex1) <- extractUnquotes scpt
53+ (t', ex2) <- extractUnquotes t
54+ return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
55+
56+extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
57+extractDoUnquotes (DoExp fc tm)
58+ = do (tm', ex) <- extractUnquotes tm
59+ return (DoExp fc tm', ex)
60+extractDoUnquotes (DoBind fc n tm)
61+ = do (tm', ex) <- extractUnquotes tm
62+ return (DoBind fc n tm', ex)
63+extractDoUnquotes (DoBindP fc t t' alts)
64+ = fail "Pattern-matching binds cannot be quasiquoted"
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)
69+extractDoUnquotes (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
70+
71+
72+extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
73+extractUnquotes (PLam n ty body)
74+ = do (ty', ex1) <- extractUnquotes ty
75+ (body', ex2) <- extractUnquotes body
76+ return (PLam n ty' body', ex1 ++ ex2)
77+extractUnquotes (PPi plicity n ty body)
78+ = do (ty', ex1) <- extractUnquotes ty
79+ (body', ex2) <- extractUnquotes body
80+ return (PPi plicity n ty' body', ex1 ++ ex2)
81+extractUnquotes (PLet n ty val body)
82+ = do (ty', ex1) <- extractUnquotes ty
83+ (val', ex2) <- extractUnquotes val
84+ (body', ex3) <- extractUnquotes body
85+ return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
86+extractUnquotes (PTyped tm ty)
87+ = do (tm', ex1) <- extractUnquotes tm
88+ (ty', ex2) <- extractUnquotes ty
89+ return (PTyped tm' ty', ex1 ++ ex2)
90+extractUnquotes (PApp fc f args)
91+ = do (f', ex1) <- extractUnquotes f
92+ args' <- mapM extractPArgUnquotes args
93+ let (args'', exs) = unzip args'
94+ return (PApp fc f' args'', ex1 ++ concat exs)
95+extractUnquotes (PAppBind fc f args)
96+ = do (f', ex1) <- extractUnquotes f
97+ args' <- mapM extractPArgUnquotes args
98+ let (args'', exs) = unzip args'
99+ return (PAppBind fc f' args'', ex1 ++ concat exs)
100+extractUnquotes (PCase fc expr cases)
101+ = do (expr', ex1) <- extractUnquotes expr
102+ let (pats, rhss) = unzip cases
103+ (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
104+ (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
105+ return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
106+extractUnquotes (PRefl fc x)
107+ = do (x', ex) <- extractUnquotes x
108+ return (PRefl fc x', ex)
109+extractUnquotes (PEq fc a b)
110+ = do (a', ex1) <- extractUnquotes a
111+ (b', ex2) <- extractUnquotes b
112+ return (PEq fc a' b', ex1 ++ ex2)
113+extractUnquotes (PRewrite fc x y z)
114+ = do (x', ex1) <- extractUnquotes x
115+ (y', ex2) <- extractUnquotes y
116+ case z of
117+ Just zz -> do (z', ex3) <- extractUnquotes zz
118+ return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
119+ Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
120+extractUnquotes (PPair fc info l r)
121+ = do (l', ex1) <- extractUnquotes l
122+ (r', ex2) <- extractUnquotes r
123+ return (PPair fc info l' r', ex1 ++ ex2)
124+extractUnquotes (PDPair fc info a b c)
125+ = do (a', ex1) <- extractUnquotes a
126+ (b', ex2) <- extractUnquotes b
127+ (c', ex3) <- extractUnquotes c
128+ return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
129+extractUnquotes (PAlternative b alts)
130+ = do alts' <- mapM extractUnquotes alts
131+ let (alts'', exs) = unzip alts'
132+ return (PAlternative b alts'', concat exs)
133+extractUnquotes (PHidden tm)
134+ = do (tm', ex) <- extractUnquotes tm
135+ return (PHidden tm', ex)
136+extractUnquotes (PGoal fc a n b)
137+ = do (a', ex1) <- extractUnquotes a
138+ (b', ex2) <- extractUnquotes b
139+ return (PGoal fc a' n b', ex1 ++ ex2)
140+extractUnquotes (PDoBlock steps)
141+ = do steps' <- mapM extractDoUnquotes steps
142+ let (steps'', exs) = unzip steps'
143+ return (PDoBlock steps'', concat exs)
144+extractUnquotes (PIdiom fc tm)
145+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
146+extractUnquotes (PProof tacs)
147+ = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
148+ return (PProof tacs', concat exs)
149+extractUnquotes (PTactics tacs)
150+ = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
151+ return (PTactics tacs', concat exs)
152+extractUnquotes (PElabError err) = fail "Can't quasiquote an error"
153+extractUnquotes (PCoerced tm)
154+ = do (tm', ex) <- extractUnquotes tm
155+ return (PCoerced tm', ex)
156+extractUnquotes (PDisamb ns tm)
157+ = do (tm', ex) <- extractUnquotes tm
158+ return (PDisamb ns tm', ex)
159+extractUnquotes (PUnifyLog tm)
160+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
161+extractUnquotes (PNoImplicits tm)
162+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
163+extractUnquotes (PQuasiquote tm) = fail "Nested quasiquotes not supported"
164+extractUnquotes (PUnquote tm) =
165+ do n <- getNameFrom (sMN 0 "unquotation")
166+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
167+extractUnquotes x = return (x, []) -- no subterms!
168+
169+
src/Idris/ElabTerm.hs+308−75
@@ -16,6 +16,7 @@ import Idris.Core.Evaluate
1616import Idris.Core.Unify
1717import Idris.Core.Typecheck (check)
1818import Idris.ErrReverse (errReverse)
19+import Idris.ElabQuasiquote (extractUnquotes)
1920
2021import Control.Applicative ((<$>))
2122import Control.Monad
@@ -123,7 +124,7 @@ elab ist info pattern opts fn tm
123124 = do let loglvl = opt_logLevel (idris_options ist)
124125 when (loglvl > 5) $ unifyLog True
125126 compute -- expand type synonyms, etc
126− elabE (False, False, False) tm -- (in argument, guarded, in type)
127+ elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)
127128 end_unify
128129 when pattern -- convert remaining holes to pattern vars
129130 (do update_term orderPats
@@ -133,7 +134,7 @@ elab ist info pattern opts fn tm
133134 mkPat)
134135 where
135136 tcgen = Dictionary `elem` opts
136− reflect = Reflection `elem` opts
137+ reflection = Reflection `elem` opts
137138
138139 isph arg = case getTm arg of
139140 Placeholder -> (True, priority arg)
@@ -153,8 +154,12 @@ elab ist info pattern opts fn tm
153154 (h: hs) -> do patvar h; mkPat
154155 [] -> return ()
155156
156− elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
157− elabE ina t =
157+ -- | elabE elaborates an expression, possibly wrapping implicit coercions
158+ -- and forces/delays. If you make a recursive call in elab', it is
159+ -- normally correct to call elabE - the ones that don't are desugarings
160+ -- typically
161+ elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()
162+ elabE ina t =
158163 --do g <- goal
159164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
160165 do ct <- insertCoerce ina t
@@ -203,13 +208,15 @@ elab ist info pattern opts fn tm
203208 constType VoidType = True
204209 constType _ = False
205210
206− elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
211+ -- "guarded" means immediately under a constructor, to help find patvars
212+
213+ elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)
207214 -> PTerm -- ^ The term to elaborate
208215 -> ElabD ()
209216 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
210217 elab' ina PType = do apply RType []; solve
211218-- elab' (_,_,inty) (PConstant c)
212−-- | constType c && pattern && not reflect && not inty
219+-- | constType c && pattern && not reflection && not inty
213220-- = lift $ tfail (Msg "Typecase is not allowed")
214221 elab' ina (PConstant c) = do apply (RConstant c) []; solve
215222 elab' ina (PQuote r) = do fill r; solve
@@ -232,16 +239,16 @@ elab ist info pattern opts fn tm
232239 [pimp (sMN 0 "A") Placeholder True,
233240 pimp (sMN 0 "B") Placeholder False,
234241 pexp l, pexp r])
235− elab' ina@(_, a, inty) (PPair fc _ l r)
242+ elab' ina@(_, a, inty, qq) (PPair fc _ l r)
236243 = do hnf_compute
237244 g <- goal
238245 case g of
239− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
240− [pexp l,pexp r])
241− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
242− [pimp (sMN 0 "A") Placeholder True,
243− pimp (sMN 0 "B") Placeholder True,
244− pexp l, pexp r])
246+ TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
247+ [pexp l,pexp r])
248+ _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
249+ [pimp (sMN 0 "A") Placeholder True,
250+ pimp (sMN 0 "B") Placeholder True,
251+ pexp l, pexp r])
245252 elab' ina (PDPair fc p l@(PRef _ n) t r)
246253 = case t of
247254 Placeholder ->
@@ -285,9 +292,9 @@ elab ist info pattern opts fn tm
285292 = try' (elab' ina x) (trySeq' deferr xs) True
286293 elab' ina (PPatvar fc n) | pattern = patvar n
287294-- elab' (_, _, inty) (PRef fc f)
288−-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
289−-- = lift $ tfail (Msg "Typecase is not allowed")
290− elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
295+-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
296+-- = lift $ tfail (Msg "Typecase is not allowed")
297+ elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n) && not qq
291298 = do ctxt <- get_context
292299 let defined = case lookupTy n ctxt of
293300 [] -> False
@@ -304,7 +311,7 @@ elab ist info pattern opts fn tm
304311 _ -> True
305312 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
306313 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
307− elab' ina@(_, a, inty) (PLam n Placeholder sc)
314+ elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)
308315 = do -- if n is a type constructor name, this makes no sense...
309316 ctxt <- get_context
310317 when (isTConName n ctxt) $
@@ -312,8 +319,8 @@ elab ist info pattern opts fn tm
312319 checkPiGoal n
313320 attack; intro (Just n);
314321 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
315− elabE (True, a, inty) sc; solve
316− elab' ina@(_, a, inty) (PLam n ty sc)
322+ elabE (True, a, inty, qq) sc; solve
323+ elab' ina@(_, a, inty, qq) (PLam n ty sc)
317324 = do tyn <- getNameFrom (sMN 0 "lamty")
318325 -- if n is a type constructor name, this makes no sense...
319326 ctxt <- get_context
@@ -327,12 +334,12 @@ elab ist info pattern opts fn tm
327334 hs <- get_holes
328335 introTy (Var tyn) (Just n)
329336 focus tyn
330− elabE (True, a, True) ty
331− elabE (True, a, inty) sc
337+ elabE (True, a, True, qq) ty
338+ elabE (True, a, inty, qq) sc
332339 solve
333− elab' ina@(_, a, _) (PPi _ n Placeholder sc)
334− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
335− elab' ina@(_, a, _) (PPi _ n ty sc)
340+ elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)
341+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve
342+ elab' ina@(_, a, _, qq) (PPi _ n ty sc)
336343 = do attack; tyn <- getNameFrom (sMN 0 "ty")
337344 claim tyn RType
338345 n' <- case n of
@@ -340,10 +347,10 @@ elab ist info pattern opts fn tm
340347 _ -> return n
341348 forall n' (Var tyn)
342349 focus tyn
343− elabE (True, a, True) ty
344− elabE (True, a, True) sc
350+ elabE (True, a, True, qq) ty
351+ elabE (True, a, True, qq) sc
345352 solve
346− elab' ina@(_, a, inty) (PLet n ty val sc)
353+ elab' ina@(_, a, inty, qq) (PLet n ty val sc)
347354 = do attack;
348355 tyn <- getNameFrom (sMN 0 "letty")
349356 claim tyn RType
@@ -355,17 +362,17 @@ elab ist info pattern opts fn tm
355362 Placeholder -> return ()
356363 _ -> do focus tyn
357364 explicit tyn
358− elabE (True, a, True) ty
365+ elabE (True, a, True, qq) ty
359366 focus valn
360− elabE (True, a, True) val
367+ elabE (True, a, True, qq) val
361368 env <- get_env
362− elabE (True, a, inty) sc
369+ elabE (True, a, inty, qq) sc
363370 -- HACK: If the name leaks into its type, it may leak out of
364371 -- scope outside, so substitute in the outer scope.
365372 expandLet n (case lookup n env of
366373 Just (Let t v) -> v)
367374 solve
368− elab' ina@(_, a, inty) (PGoal fc r n sc) = do
375+ elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do
369376 rty <- goal
370377 attack
371378 tyn <- getNameFrom (sMN 0 "letty")
@@ -374,10 +381,10 @@ elab ist info pattern opts fn tm
374381 claim valn (Var tyn)
375382 letbind n (Var tyn) (Var valn)
376383 focus valn
377− elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
384+ elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])
378385 env <- get_env
379386 computeLet n
380− elabE (True, a, inty) sc
387+ elabE (True, a, inty, qq) sc
381388 solve
382389-- elab' ina (PLet n Placeholder
383390-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -433,16 +440,16 @@ elab ist info pattern opts fn tm
433440 _ -> lift $ tfail (NoSuchVariable fn)
434441 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
435442 solve
436− elab' (_, _, inty) (PApp fc (PRef _ f) args')
437− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
443+ elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')
444+ | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
438445 = lift $ tfail (Msg "Typecase is not allowed")
439446 -- if f is local, just do a simple_app
440− elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
447+ elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)
441448 = do env <- get_env
442449 if (f `elem` map fst env && length args == 1)
443450 then -- simple app, as below
444− do simple_app (elabE (ina, g, inty) (PRef fc f))
445− (elabE (True, g, inty) (getTm (head args)))
451+ do simple_app (elabE (ina, g, inty, qq) (PRef fc f))
452+ (elabE (True, g, inty, qq) (getTm (head args)))
446453 (show tm)
447454 solve
448455 else
@@ -468,7 +475,7 @@ elab ist info pattern opts fn tm
468475 -- Sort so that the implicit tactics and alternatives go last
469476 let (ns', eargs) = unzip $
470477 sortBy cmpArg (zip ns args)
471− elabArgs ist (ina || not isinf, guarded, inty)
478+ elabArgs ist (ina || not isinf, guarded, inty, qq)
472479 [] fc False f ns'
473480 (f == sUN "Force")
474481 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
@@ -542,9 +549,9 @@ elab ist info pattern opts fn tm
542549 setInjective (PApp _ (PRef _ n) _) = setinj n
543550 setInjective _ = return ()
544551
545− elab' ina@(_, a, inty) tm@(PApp fc f [arg])
552+ elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])
546553 = erun fc $
547− do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
554+ do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))
548555 (show tm)
549556 solve
550557 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -593,7 +600,7 @@ elab ist info pattern opts fn tm
593600 elab' ina sc
594601 elab' ina (PRef fc letn)
595602 solve
596− elab' ina@(_, a, inty) c@(PCase fc scr opts)
603+ elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)
597604 = do attack
598605 tyn <- getNameFrom (sMN 0 "scty")
599606 claim tyn RType
@@ -602,7 +609,7 @@ elab ist info pattern opts fn tm
602609 claim valn (Var tyn)
603610 letbind scvn (Var tyn) (Var valn)
604611 focus valn
605− elabE (True, a, inty) scr
612+ elabE (True, a, inty, qq) scr
606613 args <- get_env
607614 cname <- unique_hole' True (mkCaseName fn)
608615 let cname' = mkN cname
@@ -629,6 +636,75 @@ elab ist info pattern opts fn tm
629636 elab' ina (PUnifyLog t) = do unifyLog True
630637 elab' ina t
631638 unifyLog False
639+ elab' (ina, g, inty, qq) (PQuasiquote t)
640+ = do -- First extract the unquoted subterms, replacing them with fresh
641+ -- names in the quasiquoted term. Claim their reflections to be
642+ -- of type TT.
643+ (t, unq) <- extractUnquotes t
644+ let unquoteNames = map fst unq
645+ mapM_ (flip claim (Var tt)) unquoteNames
646+
647+
648+ -- Save the old state - we need a fresh proof state to avoid
649+ -- capturing lexically available variables in the quoted term.
650+ ctxt <- get_context
651+ saveState
652+ updatePS (const .
653+ newProof (sMN 0 "q") ctxt $
654+ P Ref tt Erased)
655+
656+ -- Re-add the unquotes, letting Idris infer the (fictional)
657+ -- types. Here, they represent the real type rather than the type
658+ -- of their reflection.
659+ mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
660+ claim ty RType
661+ movelast ty
662+ claim n (Var ty)
663+ movelast n)
664+ unquoteNames
665+
666+ -- Establish holes for the type and value of the term to be
667+ -- quasiquoted
668+ qTy <- getNameFrom (sMN 0 "qquoteTy")
669+ claim qTy RType
670+ qTm <- getNameFrom (sMN 0 "qquoteTm")
671+ claim qTm (Var qTy)
672+ -- Let-bind the result of elaborating the contained term, so that
673+ -- the hole doesn't disappear
674+ nTm <- getNameFrom (sMN 0 "quotedTerm")
675+ letbind nTm (Var qTy) (Var qTm)
676+ -- We must solve the type later through unification
677+ movelast qTy
678+
679+
680+ -- Elaborate the quasiquoted term into the hole
681+ focus qTm
682+ elabE (ina, g, inty, True) t
683+ end_unify
684+
685+ -- We now have an elaborated term. Reflect it and solve the
686+ -- original goal in the original proof state.
687+ env <- get_env
688+ loadState
689+ case fmap (explicitNames . binderVal) $ lookup nTm env of
690+ Just q
691+ | pattern -> reflectQuotePattern unquoteNames q
692+ | otherwise -> do fill $ reflectQuote unquoteNames q
693+ solve
694+ Nothing -> fail "Broken elaboration of quasiquote"
695+
696+ -- Finally fill in the terms or patterns from the unquotes. This
697+ -- happens last so that their holes still exist while elaborating
698+ -- the main quotation.
699+ mapM_ elabUnquote unq
700+ where tt = sNS (sUN "TT") ["Reflection", "Language"]
701+
702+ elabUnquote (n, tm)
703+ = do focus n
704+ elabE (ina, g, inty, False) tm
705+
706+
707+ elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
632708 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
633709
634710 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
@@ -720,7 +796,7 @@ elab ist info pattern opts fn tm
720796
721797 -- | Elaborate the arguments to a function
722798 elabArgs :: IState -- ^ The current Idris state
723− -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
799+ -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)
724800 -> [Bool]
725801 -> FC -- ^ Source location
726802 -> Bool
@@ -1441,21 +1517,159 @@ reflCall funName args
14411517
14421518-- | Lift a term into its Language.Reflection.TT representation
14431519reflect :: Term -> Raw
1444−reflect (P nt n t)
1445− = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1446−reflect (V n)
1520+reflect = reflectQuote []
1521+
1522+claimTT :: Name -> ElabD Name
1523+claimTT n = do n' <- getNameFrom n
1524+ claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
1525+ return n'
1526+
1527+-- | Convert a reflected term to a more suitable form for pattern-matching.
1528+-- In particular, the less-interesting bits are elaborated to _ patterns. This
1529+-- happens to NameTypes, universe levels, names that are bound but not used,
1530+-- and the type annotation field of the P constructor.
1531+reflectQuotePattern :: [Name] -> Term -> ElabD ()
1532+reflectQuotePattern unq (P _ n _)
1533+ | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
1534+ do fill (Var n) ; solve
1535+ | otherwise =
1536+ do tyannot <- claimTT (sMN 0 "pTyAnnot")
1537+ movelast tyannot -- use a _ pattern here
1538+ nt <- getNameFrom (sMN 0 "nt")
1539+ claim nt (Var (reflm "NameType"))
1540+ movelast nt -- use a _ pattern here
1541+ n' <- getNameFrom (sMN 0 "n")
1542+ claim n' (Var (reflm "TTName"))
1543+ fill $ reflCall "P" [Var nt, Var n', Var tyannot]
1544+ solve
1545+ focus n'; reflectNameQuotePattern n
1546+reflectQuotePattern unq (V n)
1547+ = do fill $ reflCall "V" [RConstant (I n)]
1548+ solve
1549+reflectQuotePattern unq (Bind n b x)
1550+ = do x' <- claimTT (sMN 0 "sc")
1551+ movelast x'
1552+ b' <- getNameFrom (sMN 0 "binder")
1553+ claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
1554+ (Var (sNS (sUN "TT") ["Reflection", "Language"])))
1555+ if n `elem` freeNames x
1556+ then do fill $ reflCall "Bind"
1557+ [reflectName n,
1558+ Var b',
1559+ Var x']
1560+ solve
1561+ else do any <- getNameFrom (sMN 0 "anyName")
1562+ claim any (Var (reflm "TTName"))
1563+ movelast any
1564+ fill $ reflCall "Bind"
1565+ [Var any,
1566+ Var b',
1567+ Var x']
1568+ solve
1569+ focus x'; reflectQuotePattern unq x
1570+ focus b'; reflectBinderQuotePattern unq b
1571+
1572+ where
1573+ reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()
1574+ reflectBinderQuotePattern unq (Lam t)
1575+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
1576+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
1577+ solve
1578+ focus t'; reflectQuotePattern unq t
1579+ reflectBinderQuotePattern unq (Pi t)
1580+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'
1581+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t']
1582+ solve
1583+ focus t'; reflectQuotePattern unq t
1584+ reflectBinderQuotePattern unq (Let x y)
1585+ = do x' <- claimTT (sMN 0 "ty"); movelast x';
1586+ y' <- claimTT (sMN 0 "v"); movelast y';
1587+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
1588+ solve
1589+ focus x'; reflectQuotePattern unq x
1590+ focus y'; reflectQuotePattern unq y
1591+ reflectBinderQuotePattern unq (NLet x y)
1592+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
1593+ y' <- claimTT (sMN 0 "v"); movelast y'
1594+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
1595+ solve
1596+ focus x'; reflectQuotePattern unq x
1597+ focus y'; reflectQuotePattern unq y
1598+ reflectBinderQuotePattern unq (Hole t)
1599+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
1600+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
1601+ solve
1602+ focus t'; reflectQuotePattern unq t
1603+ reflectBinderQuotePattern unq (GHole _ t)
1604+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
1605+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
1606+ solve
1607+ focus t'; reflectQuotePattern unq t
1608+ reflectBinderQuotePattern unq (Guess x y)
1609+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
1610+ y' <- claimTT (sMN 0 "v"); movelast y'
1611+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
1612+ solve
1613+ focus x'; reflectQuotePattern unq x
1614+ focus y'; reflectQuotePattern unq y
1615+ reflectBinderQuotePattern unq (PVar t)
1616+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
1617+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
1618+ solve
1619+ focus t'; reflectQuotePattern unq t
1620+ reflectBinderQuotePattern unq (PVTy t)
1621+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
1622+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
1623+ solve
1624+ focus t'; reflectQuotePattern unq t
1625+reflectQuotePattern unq (App f x)
1626+ = do f' <- claimTT (sMN 0 "f"); movelast f'
1627+ x' <- claimTT (sMN 0 "x"); movelast x'
1628+ fill $ reflCall "App" [Var f', Var x']
1629+ solve
1630+ focus f'; reflectQuotePattern unq f
1631+ focus x'; reflectQuotePattern unq x
1632+reflectQuotePattern unq (Constant c)
1633+ = do fill $ reflCall "TConst" [reflectConstant c]
1634+ solve
1635+reflectQuotePattern unq (Proj t i)
1636+ = do t' <- claimTT (sMN 0 "t"); movelast t'
1637+ fill $ reflCall "Proj" [Var t', RConstant (I i)]
1638+ solve
1639+ focus t'; reflectQuotePattern unq t
1640+reflectQuotePattern unq (Erased)
1641+ = do erased <- claimTT (sMN 0 "erased")
1642+ movelast erased
1643+ fill $ (Var erased)
1644+ solve
1645+reflectQuotePattern unq (Impossible)
1646+ = do fill $ Var (reflm "Impossible")
1647+ solve
1648+reflectQuotePattern unq (TType exp)
1649+ = do ue <- getNameFrom (sMN 0 "uexp")
1650+ claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
1651+ movelast ue
1652+ fill $ reflCall "TType" [Var ue]
1653+ solve
1654+
1655+-- | Create a reflected term, but leave refs to the provided name intact
1656+reflectQuote :: [Name] -> Term -> Raw
1657+reflectQuote unq (P nt n t)
1658+ | n `elem` unq = Var n
1659+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
1660+reflectQuote unq (V n)
14471661 = reflCall "V" [RConstant (I n)]
1448−reflect (Bind n b x)
1449− = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1450−reflect (App f x)
1451− = reflCall "App" [reflect f, reflect x]
1452−reflect (Constant c)
1662+reflectQuote unq (Bind n b x)
1663+ = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
1664+reflectQuote unq (App f x)
1665+ = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
1666+reflectQuote unq (Constant c)
14531667 = reflCall "TConst" [reflectConstant c]
1454−reflect (Proj t i)
1455− = reflCall "Proj" [reflect t, RConstant (I i)]
1456−reflect (Erased) = Var (reflm "Erased")
1457−reflect (Impossible) = Var (reflm "Impossible")
1458−reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1668+reflectQuote unq (Proj t i)
1669+ = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
1670+reflectQuote unq (Erased) = Var (reflm "Erased")
1671+reflectQuote unq (Impossible) = Var (reflm "Impossible")
1672+reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
14591673
14601674reflectNameType :: NameType -> Raw
14611675reflectNameType (Bound) = Var (reflm "Bound")
@@ -1482,25 +1696,44 @@ reflectName (MN i n)
14821696reflectName (NErased) = Var (reflm "NErased")
14831697reflectName n = Var (reflm "NErased") -- special name, not yet implemented
14841698
1699+-- | Elaborate a name to a pattern. This means that NS and UN will be intact,
1700+-- while all others become _
1701+reflectNameQuotePattern :: Name -> ElabD ()
1702+reflectNameQuotePattern n@(UN s)
1703+ = do fill $ reflectName n
1704+ solve
1705+reflectNameQuotePattern n@(NS _ _)
1706+ = do fill $ reflectName n
1707+ solve
1708+reflectNameQuotePattern _ -- for all other names, match any
1709+ = do nameHole <- getNameFrom (sMN 0 "name")
1710+ claim nameHole (Var (reflm "TTName"))
1711+ movelast nameHole
1712+ fill (Var nameHole)
1713+ solve
1714+
14851715reflectBinder :: Binder Term -> Raw
1486−reflectBinder (Lam t)
1487− = reflCall "Lam" [Var (reflm "TT"), reflect t]
1488−reflectBinder (Pi t)
1489− = reflCall "Pi" [Var (reflm "TT"), reflect t]
1490−reflectBinder (Let x y)
1491− = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1492−reflectBinder (NLet x y)
1493− = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1494−reflectBinder (Hole t)
1495− = reflCall "Hole" [Var (reflm "TT"), reflect t]
1496−reflectBinder (GHole _ t)
1497− = reflCall "GHole" [Var (reflm "TT"), reflect t]
1498−reflectBinder (Guess x y)
1499− = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1500−reflectBinder (PVar t)
1501− = reflCall "PVar" [Var (reflm "TT"), reflect t]
1502−reflectBinder (PVTy t)
1503− = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1716+reflectBinder = reflectBinderQuote []
1717+
1718+reflectBinderQuote :: [Name] -> Binder Term -> Raw
1719+reflectBinderQuote unq (Lam t)
1720+ = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
1721+reflectBinderQuote unq (Pi t)
1722+ = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t]
1723+reflectBinderQuote unq (Let x y)
1724+ = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1725+reflectBinderQuote unq (NLet x y)
1726+ = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1727+reflectBinderQuote unq (Hole t)
1728+ = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
1729+reflectBinderQuote unq (GHole _ t)
1730+ = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
1731+reflectBinderQuote unq (Guess x y)
1732+ = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1733+reflectBinderQuote unq (PVar t)
1734+ = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
1735+reflectBinderQuote unq (PVTy t)
1736+ = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
15041737
15051738reflectConstant :: Const -> Raw
15061739reflectConstant c@(I _) = reflCall "I" [RConstant c]
src/Idris/IBC.hs+2−2
@@ -1239,7 +1239,7 @@ instance Binary Using where
12391239 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
12401240
12411241instance Binary SyntaxInfo where
1242− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)
1242+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)
12431243 = do put x1
12441244 put x2
12451245 put x3
@@ -1255,7 +1255,7 @@ instance Binary SyntaxInfo where
12551255 x5 <- get
12561256 x6 <- get
12571257 x7 <- get
1258− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7)
1258+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 False)
12591259
12601260instance (Binary t) => Binary (PClause' t) where
12611261 put x
src/Idris/ParseExpr.hs+29
@@ -289,6 +289,8 @@ SimpleExpr ::=
289289 | Constant
290290 | Type
291291 | '_|_'
292+ | Quasiquote
293+ | Unquote
292294 | '_'
293295 ;
294296@
@@ -326,6 +328,8 @@ simpleExpr syn =
326328 <|> do symbol "_|_"
327329 fc <- getFC
328330 return (PFalse fc)
331+ <|> quasiquote syn
332+ <|> unquote syn
329333 <|> do lchar '_'; return Placeholder
330334 <?> "expression"
331335
@@ -587,6 +591,31 @@ constraintArg syn = do symbol "@{"
587591 return (pconst e)
588592 <?> "constraint argument"
589593
594+{-| Parses a quasiquote expression (for building reflected terms using the elaborator)
595+
596+> Quasiquote ::= '`(' Expr ')'
597+
598+-}
599+quasiquote :: SyntaxInfo -> IdrisParser PTerm
600+quasiquote syn = do guard (not (syn_in_quasiquote syn))
601+ symbol "`("
602+ e <- expr syn { syn_in_quasiquote = True , inPattern = False}
603+ symbol ")"
604+ return $ PQuasiquote e
605+ <?> "quasiquotation"
606+
607+{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)
608+
609+> Unquote ::= ',' Expr
610+
611+-}
612+unquote :: SyntaxInfo -> IdrisParser PTerm
613+unquote syn = do guard (syn_in_quasiquote syn)
614+ symbol "~"
615+ e <- simpleExpr syn { syn_in_quasiquote = False }
616+ return $ PUnquote e
617+ <?> "unquotation"
618+
590619
591620{-| Parses a record field setter expression
592621@
test/quasiquote001/QuasiquoteBasics.idrnew file+34
@@ -0,0 +1,34 @@
1+module QuasiquoteBasics
2+
3+import Language.Reflection
4+import Language.Reflection.Utils
5+
6+nat : TT
7+nat = `(Nat)
8+
9+three : TT
10+three = `(S (S (S Z)))
11+
12+twoElems : TT
13+twoElems = `(with List [(), ()])
14+
15+copy : TT -> TT
16+copy q = `((~q,~q))
17+
18+thing : TT -> TT
19+thing tm = `(with List [Type, ~tm])
20+
21+getTyArg : TT -> Maybe TT
22+getTyArg `(~f ~x) = Just x
23+getTyArg _ = Nothing
24+
25+
26+
27+
28+namespace Main
29+ main : IO ()
30+ main = do putStrLn . show $ thing (copy nat)
31+ putStrLn "--------------"
32+ putStrLn . show $ getTyArg nat
33+ putStrLn "--------------"
34+ putStrLn . show $ getTyArg (twoElems)
test/quasiquote001/expectednew file+5
@@ -0,0 +1,5 @@
1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (TType (UVal 0))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (P Bound (MN 106 "A") (TType (UVal 0)))) (P Bound (MN 107 "B") (TType (UVal 0)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVal 0)))))
2+--------------
3+Nothing
4+--------------
5+Just (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))))
test/quasiquote001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ QuasiquoteBasics.idr -o quasiquote001
3+./quasiquote001
4+rm -f quasiquote001 *.ibc