git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1331 from david-christiansen/quasiquote
871c8b2David Christiansen
CHANGELOG+5
compare with master
unifiedsplit
@@ -10,6 +10,11 @@ New in 0.9.14:
10* Experimental 'neweffects' library, with simplified API
10* Experimental 'neweffects' library, with simplified API
11* All new JavaScript backend (avoids callstack overflows)
11* All new JavaScript backend (avoids callstack overflows)
12* Add support for %lib directive for NodeJS
12* 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+
13
18
14New in 0.9.13:
19New in 0.9.13:
15--------------
20--------------
idris.cabal+5
@@ -415,6 +415,10 @@ Extra-source-files:
415 test/proof004/*.idr
415 test/proof004/*.idr
416 test/proof004/expected
416 test/proof004/expected
417
417
418+ test/quasiquote001/run
419+ test/quasiquote001/*.idr
420+ test/quasiquote001/expected
421+
418 test/records001/run
422 test/records001/run
419 test/records001/*.idr
423 test/records001/*.idr
420 test/records001/expected
424 test/records001/expected
@@ -548,6 +552,7 @@ Library
548 , Idris.Docs
552 , Idris.Docs
549 , Idris.Docstrings
553 , Idris.Docstrings
550 , Idris.ElabDecls
554 , Idris.ElabDecls
555+ , Idris.ElabQuasiquote
551 , Idris.ElabTerm
556 , Idris.ElabTerm
552 , Idris.Erasure
557 , Idris.Erasure
553 , Idris.Error
558 , Idris.Error
src/Idris/AbsSyntax.hs+68−64
@@ -1270,6 +1270,7 @@ addImplBound ist ns = addImpl' False ns [] ist
1270addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1270addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1271addImplBoundInf ist ns inf = addImpl' False ns inf ist
1271addImplBoundInf ist ns inf = addImpl' False ns inf ist
1272
1272
1273+-- | Add the implicit arguments to applications in the term
1273addImpl :: IState -> PTerm -> PTerm
1274addImpl :: IState -> PTerm -> PTerm
1274addImpl = addImpl' False [] []
1275addImpl = addImpl' False [] []
1275
1276
@@ -1277,86 +1278,89 @@ addImpl = addImpl' False [] []
1277-- and *not* inside a PHidden
1278-- and *not* inside a PHidden
1278
1279
1279addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1280addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1280−addImpl' inpat env infns ist ptm
1281+addImpl' inpat env infns ist ptm
1281− = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1282+ = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1282 where
1283 where
1284+ ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1283− ai env ds (PRef fc f)
1285+ ai qq env ds (PRef fc f)
1284 | f `elem` infns = PInferRef fc f
1286 | f `elem` infns = PInferRef fc f
1285− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1287+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1286− ai env ds (PHidden (PRef fc f))
1288+ ai qq env ds (PHidden (PRef fc f))
1287− | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1289+ | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1288− ai env ds (PEq fc l r)
1290+ ai qq env ds (PEq fc l r)
1289− = let l' = ai env ds l
1291+ = let l' = ai qq env ds l
1290− r' = ai env ds r in
1292+ r' = ai qq env ds r in
1291 PEq fc l' r'
1293 PEq fc l' r'
1292− ai env ds (PRewrite fc l r g)
1294+ ai qq env ds (PRewrite fc l r g)
1293− = let l' = ai env ds l
1295+ = let l' = ai qq env ds l
1294− r' = ai env ds r
1296+ r' = ai qq env ds r
1295− g' = fmap (ai env ds) g in
1297+ g' = fmap (ai qq env ds) g in
1296 PRewrite fc l' r' g'
1298 PRewrite fc l' r' g'
1297− ai env ds (PTyped l r)
1299+ ai qq env ds (PTyped l r)
1298− = let l' = ai env ds l
1300+ = let l' = ai qq env ds l
1299− r' = ai env ds r in
1301+ r' = ai qq env ds r in
1300 PTyped l' r'
1302 PTyped l' r'
1301− ai env ds (PPair fc p l r)
1303+ ai qq env ds (PPair fc p l r)
1302− = let l' = ai env ds l
1304+ = let l' = ai qq env ds l
1303− r' = ai env ds r in
1305+ r' = ai qq env ds r in
1304 PPair fc p l' r'
1306 PPair fc p l' r'
1305− ai env ds (PDPair fc p l t r)
1307+ ai qq env ds (PDPair fc p l t r)
1306− = let l' = ai env ds l
1308+ = let l' = ai qq env ds l
1307− t' = ai env ds t
1309+ t' = ai qq env ds t
1308− r' = ai env ds r in
1310+ r' = ai qq env ds r in
1309 PDPair fc p l' t' r'
1311 PDPair fc p l' t' r'
1310− ai env ds (PAlternative a as)
1312+ ai qq env ds (PAlternative a as)
1311− = let as' = map (ai env ds) as in
1313+ = let as' = map (ai qq env ds) as in
1312 PAlternative a as'
1314 PAlternative a as'
1313− ai env _ (PDisamb ds' as) = ai env ds' as
1315+ ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1314− ai env ds (PApp fc (PInferRef _ f) as)
1316+ ai qq env ds (PApp fc (PInferRef _ f) as)
1315− = let as' = map (fmap (ai env ds)) as in
1317+ = let as' = map (fmap (ai qq env ds)) as in
1316 PApp fc (PInferRef fc f) as'
1318 PApp fc (PInferRef fc f) as'
1317− ai env ds (PApp fc ftm@(PRef _ f) as)
1319+ ai qq env ds (PApp fc ftm@(PRef _ f) as)
1318− | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1320+ | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1319 | not (f `elem` map fst env)
1321 | not (f `elem` map fst env)
1320− = let as' = map (fmap (ai env ds)) as in
1322+ = let as' = map (fmap (ai qq env ds)) as in
1321− handleErr $ aiFn inpat False ist fc f ds as'
1323+ handleErr $ aiFn inpat False qq ist fc f ds as'
1322 | Just (Just ty) <- lookup f env =
1324 | 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
1324 arity = getPArity ty in
1326 arity = getPArity ty in
1325 mkPApp fc arity ftm as'
1327 mkPApp fc arity ftm as'
1326− ai env ds (PApp fc f as)
1328+ ai qq env ds (PApp fc f as)
1327− = let f' = ai env ds f
1329+ = let f' = ai qq env ds f
1328− as' = map (fmap (ai env ds)) as in
1330+ as' = map (fmap (ai qq env ds)) as in
1329 mkPApp fc 1 f' as'
1331 mkPApp fc 1 f' as'
1330− ai env ds (PCase fc c os)
1332+ ai qq env ds (PCase fc c os)
1331− = let c' = ai env ds c in
1333+ = let c' = ai qq env ds c in
1332 -- leave os alone, because they get lifted into a new pattern match
1334 -- leave os alone, because they get lifted into a new pattern match
1333 -- definition which is passed through addImpl again with more scope
1335 -- definition which is passed through addImpl again with more scope
1334 -- information
1336 -- information
1335 PCase fc c' os
1337 PCase fc c' os
1336− ai env ds (PLam n ty sc)
1338+ ai qq env ds (PLam n ty sc)
1337− = let ty' = ai env ds ty
1339+ = let ty' = ai qq env ds ty
1338− sc' = ai ((n, Just ty):env) ds sc in
1340+ sc' = ai qq ((n, Just ty):env) ds sc in
1339 PLam n ty' sc'
1341 PLam n ty' sc'
1340− ai env ds (PLet n ty val sc)
1342+ ai qq env ds (PLet n ty val sc)
1341− = let ty' = ai env ds ty
1343+ = let ty' = ai qq env ds ty
1342− val' = ai env ds val
1344+ val' = ai qq env ds val
1343− sc' = ai ((n, Just ty):env) ds sc in
1345+ sc' = ai qq ((n, Just ty):env) ds sc in
1344 PLet n ty' val' sc'
1346 PLet n ty' val' sc'
1345− ai env ds (PPi p n ty sc)
1347+ ai qq env ds (PPi p n ty sc)
1346− = let ty' = ai env ds ty
1348+ = let ty' = ai qq env ds ty
1347− sc' = ai ((n, Just ty):env) ds sc in
1349+ sc' = ai qq ((n, Just ty):env) ds sc in
1348 PPi p n ty' sc'
1350 PPi p n ty' sc'
1349− ai env ds (PGoal fc r n sc)
1351+ ai qq env ds (PGoal fc r n sc)
1350− = let r' = ai env ds r
1352+ = let r' = ai qq env ds r
1351− sc' = ai ((n, Nothing):env) ds sc in
1353+ sc' = ai qq ((n, Nothing):env) ds sc in
1352 PGoal fc r' n sc'
1354 PGoal fc r' n sc'
1353− ai env ds (PHidden tm) = PHidden (ai env ds tm)
1355+ ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1354− ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1356+ ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)
1355− ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1357+ ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)
1356− ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1358+ ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1357− ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1359+ ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1358− ai env ds (PNoImplicits tm) = PNoImplicits (ai 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)
1359− ai env ds tm = tm
1363+ ai qq env ds tm = tm
1360
1364
1361 handleErr (Left err) = PElabError err
1365 handleErr (Left err) = PElabError err
1362 handleErr (Right x) = x
1366 handleErr (Right x) = x
@@ -1364,8 +1368,8 @@ addImpl' inpat env infns ist ptm
1364-- if in a pattern, and there are no arguments, and there's no possible
1368-- if in a pattern, and there are no arguments, and there's no possible
1365-- names with zero explicit arguments, don't add implicits.
1369-- names with zero explicit arguments, don't add implicits.
1366
1370
1367−aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1371+aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1368−aiFn inpat True ist fc f ds []
1372+aiFn inpat True qq ist fc f ds []
1369 = case lookupDef f (tt_ctxt ist) of
1373 = case lookupDef f (tt_ctxt ist) of
1370 [] -> Right $ PPatvar fc f
1374 [] -> Right $ PPatvar fc f
1371 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1375 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
@@ -1373,7 +1377,7 @@ aiFn inpat True ist fc f ds []
1373 if (not (vname f) || tcname f
1377 if (not (vname f) || tcname f
1374 || any (conCaf (tt_ctxt ist)) ialts)
1378 || any (conCaf (tt_ctxt ist)) ialts)
1375-- any constructor alts || any allImp ialts))
1379-- 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
1377 else Right $ PPatvar fc f
1381 else Right $ PPatvar fc f
1378 where imp (PExp _ _ _ _) = False
1382 where imp (PExp _ _ _ _) = False
1379 imp _ = True
1383 imp _ = True
@@ -1382,14 +1386,14 @@ aiFn inpat True ist fc f ds []
1382 constructor (TyDecl (DCon _ _) _) = True
1386 constructor (TyDecl (DCon _ _) _) = True
1383 constructor _ = False
1387 constructor _ = False
1384
1388
1385− conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1389+ conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1386
1390
1387 vname (UN n) = True -- non qualified
1391 vname (UN n) = True -- non qualified
1388 vname _ = False
1392 vname _ = False
1389
1393
1390−aiFn inpat expat ist fc f ds as
1394+aiFn inpat expat qq ist fc f ds as
1391 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1395 | 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
1393 -- This is where namespaces get resolved by adding PAlternative
1397 -- This is where namespaces get resolved by adding PAlternative
1394 = do let ns = lookupCtxtName f (idris_implicits ist)
1398 = do let ns = lookupCtxtName f (idris_implicits ist)
1395 let nh = filter (\(n, _) -> notHidden n) ns
1399 let nh = filter (\(n, _) -> notHidden n) ns
src/Idris/AbsSyntaxTree.hs+8−3
@@ -702,6 +702,8 @@ data PTerm = PQuote Raw
702 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
702 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
703 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
703 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
704 | PNoImplicits PTerm -- ^ never run implicit converions on the term
704 | PNoImplicits PTerm -- ^ never run implicit converions on the term
705+ | PQuasiquote PTerm -- ^ `(Term)
706+ | PUnquote PTerm -- ^ ,Term
705 deriving Eq
707 deriving Eq
706
708
707
709
@@ -969,14 +971,15 @@ data SyntaxInfo = Syn { using :: [Using],
969 implicitAllowed :: Bool,
971 implicitAllowed :: Bool,
970 maxline :: Maybe Int,
972 maxline :: Maybe Int,
971 mut_nesting :: Int,
973 mut_nesting :: Int,
972− dsl_info :: DSL }
974+ dsl_info :: DSL,
975+ syn_in_quasiquote :: Bool }
973 deriving Show
976 deriving Show
974{-!
977{-!
975deriving instance NFData SyntaxInfo
978deriving instance NFData SyntaxInfo
976deriving instance Binary SyntaxInfo
979deriving instance Binary SyntaxInfo
977!-}
980!-}
978
981
979−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL
982+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
980
983
981expandNS :: SyntaxInfo -> Name -> Name
984expandNS :: SyntaxInfo -> Name -> Name
982expandNS syn n@(NS _ _) = n
985expandNS syn n@(NS _ _) = n
@@ -1351,8 +1354,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1351 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1354 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1352 prettySe p bnd (PCoerced t) = prettySe p bnd t
1355 prettySe p bnd (PCoerced t) = prettySe p bnd t
1353 prettySe p bnd (PElabError s) = pretty s
1356 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
1354
1359
1355− prettySe p bnd _ = text "test"
1360+ prettySe p bnd _ = text "missing pretty-printer for term"
1356
1361
1357 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1362 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1358 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1363 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
src/Idris/Core/Elaborate.hs+1
@@ -380,6 +380,7 @@ casetac tm = processTactic' (CaseTac tm)
380equiv :: Raw -> Elab' aux ()
380equiv :: Raw -> Elab' aux ()
381equiv tm = processTactic' (Equiv tm)
381equiv tm = processTactic' (Equiv tm)
382
382
383+-- | Turn the current hole into a pattern variable with the provided name, made unique if MN
383patvar :: Name -> Elab' aux ()
384patvar :: Name -> Elab' aux ()
384patvar n = do env <- get_env
385patvar n = do env <- get_env
385 hs <- get_holes
386 hs <- get_holes
src/Idris/DeepSeq.hs+4−3
@@ -320,13 +320,14 @@ instance NFData Using where
320 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
320 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
321 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
321 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
322
322
323−
324instance NFData SyntaxInfo where
323instance 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)
326 = rnf x1 `seq`
325 = rnf x1 `seq`
327 rnf x2 `seq`
326 rnf x2 `seq`
328 rnf x3 `seq`
327 rnf x3 `seq`
328+ rnf x4 `seq`
329+ rnf x5 `seq`
329− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
330+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()
330
331
331
332
332
333
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
16import Idris.Core.Unify
16import Idris.Core.Unify
17import Idris.Core.Typecheck (check)
17import Idris.Core.Typecheck (check)
18import Idris.ErrReverse (errReverse)
18import Idris.ErrReverse (errReverse)
19+import Idris.ElabQuasiquote (extractUnquotes)
19
20
20import Control.Applicative ((<$>))
21import Control.Applicative ((<$>))
21import Control.Monad
22import Control.Monad
@@ -123,7 +124,7 @@ elab ist info pattern opts fn tm
123 = do let loglvl = opt_logLevel (idris_options ist)
124 = do let loglvl = opt_logLevel (idris_options ist)
124 when (loglvl > 5) $ unifyLog True
125 when (loglvl > 5) $ unifyLog True
125 compute -- expand type synonyms, etc
126 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)
127 end_unify
128 end_unify
128 when pattern -- convert remaining holes to pattern vars
129 when pattern -- convert remaining holes to pattern vars
129 (do update_term orderPats
130 (do update_term orderPats
@@ -133,7 +134,7 @@ elab ist info pattern opts fn tm
133 mkPat)
134 mkPat)
134 where
135 where
135 tcgen = Dictionary `elem` opts
136 tcgen = Dictionary `elem` opts
136− reflect = Reflection `elem` opts
137+ reflection = Reflection `elem` opts
137
138
138 isph arg = case getTm arg of
139 isph arg = case getTm arg of
139 Placeholder -> (True, priority arg)
140 Placeholder -> (True, priority arg)
@@ -153,8 +154,12 @@ elab ist info pattern opts fn tm
153 (h: hs) -> do patvar h; mkPat
154 (h: hs) -> do patvar h; mkPat
154 [] -> return ()
155 [] -> return ()
155
156
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
156− elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
161+ elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()
157− elabE ina t =
162+ elabE ina t =
158 --do g <- goal
163 --do g <- goal
159 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
160 do ct <- insertCoerce ina t
165 do ct <- insertCoerce ina t
@@ -203,13 +208,15 @@ elab ist info pattern opts fn tm
203 constType VoidType = True
208 constType VoidType = True
204 constType _ = False
209 constType _ = False
205
210
211+ -- "guarded" means immediately under a constructor, to help find patvars
212+
206− elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
213+ elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)
207 -> PTerm -- ^ The term to elaborate
214 -> PTerm -- ^ The term to elaborate
208 -> ElabD ()
215 -> ElabD ()
209 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
216 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
210 elab' ina PType = do apply RType []; solve
217 elab' ina PType = do apply RType []; solve
211-- elab' (_,_,inty) (PConstant c)
218-- elab' (_,_,inty) (PConstant c)
212−-- | constType c && pattern && not reflect && not inty
219+-- | constType c && pattern && not reflection && not inty
213-- = lift $ tfail (Msg "Typecase is not allowed")
220-- = lift $ tfail (Msg "Typecase is not allowed")
214 elab' ina (PConstant c) = do apply (RConstant c) []; solve
221 elab' ina (PConstant c) = do apply (RConstant c) []; solve
215 elab' ina (PQuote r) = do fill r; solve
222 elab' ina (PQuote r) = do fill r; solve
@@ -232,16 +239,16 @@ elab ist info pattern opts fn tm
232 [pimp (sMN 0 "A") Placeholder True,
239 [pimp (sMN 0 "A") Placeholder True,
233 pimp (sMN 0 "B") Placeholder False,
240 pimp (sMN 0 "B") Placeholder False,
234 pexp l, pexp r])
241 pexp l, pexp r])
235− elab' ina@(_, a, inty) (PPair fc _ l r)
242+ elab' ina@(_, a, inty, qq) (PPair fc _ l r)
236 = do hnf_compute
243 = do hnf_compute
237 g <- goal
244 g <- goal
238 case g of
245 case g of
239− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
246+ TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
240− [pexp l,pexp r])
247+ [pexp l,pexp r])
241− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
248+ _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
242− [pimp (sMN 0 "A") Placeholder True,
249+ [pimp (sMN 0 "A") Placeholder True,
243− pimp (sMN 0 "B") Placeholder True,
250+ pimp (sMN 0 "B") Placeholder True,
244− pexp l, pexp r])
251+ pexp l, pexp r])
245 elab' ina (PDPair fc p l@(PRef _ n) t r)
252 elab' ina (PDPair fc p l@(PRef _ n) t r)
246 = case t of
253 = case t of
247 Placeholder ->
254 Placeholder ->
@@ -285,9 +292,9 @@ elab ist info pattern opts fn tm
285 = try' (elab' ina x) (trySeq' deferr xs) True
292 = try' (elab' ina x) (trySeq' deferr xs) True
286 elab' ina (PPatvar fc n) | pattern = patvar n
293 elab' ina (PPatvar fc n) | pattern = patvar n
287-- elab' (_, _, inty) (PRef fc f)
294-- elab' (_, _, inty) (PRef fc f)
288−-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
295+-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
289−-- = lift $ tfail (Msg "Typecase is not allowed")
296+-- = lift $ tfail (Msg "Typecase is not allowed")
290− elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
297+ elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n) && not qq
291 = do ctxt <- get_context
298 = do ctxt <- get_context
292 let defined = case lookupTy n ctxt of
299 let defined = case lookupTy n ctxt of
293 [] -> False
300 [] -> False
@@ -304,7 +311,7 @@ elab ist info pattern opts fn tm
304 _ -> True
311 _ -> True
305 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
312 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
306 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
313 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)
308 = do -- if n is a type constructor name, this makes no sense...
315 = do -- if n is a type constructor name, this makes no sense...
309 ctxt <- get_context
316 ctxt <- get_context
310 when (isTConName n ctxt) $
317 when (isTConName n ctxt) $
@@ -312,8 +319,8 @@ elab ist info pattern opts fn tm
312 checkPiGoal n
319 checkPiGoal n
313 attack; intro (Just n);
320 attack; intro (Just n);
314 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
321 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
315− elabE (True, a, inty) sc; solve
322+ elabE (True, a, inty, qq) sc; solve
316− elab' ina@(_, a, inty) (PLam n ty sc)
323+ elab' ina@(_, a, inty, qq) (PLam n ty sc)
317 = do tyn <- getNameFrom (sMN 0 "lamty")
324 = do tyn <- getNameFrom (sMN 0 "lamty")
318 -- if n is a type constructor name, this makes no sense...
325 -- if n is a type constructor name, this makes no sense...
319 ctxt <- get_context
326 ctxt <- get_context
@@ -327,12 +334,12 @@ elab ist info pattern opts fn tm
327 hs <- get_holes
334 hs <- get_holes
328 introTy (Var tyn) (Just n)
335 introTy (Var tyn) (Just n)
329 focus tyn
336 focus tyn
330− elabE (True, a, True) ty
337+ elabE (True, a, True, qq) ty
331− elabE (True, a, inty) sc
338+ elabE (True, a, inty, qq) sc
332 solve
339 solve
333− elab' ina@(_, a, _) (PPi _ n Placeholder sc)
340+ elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)
334− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
341+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve
335− elab' ina@(_, a, _) (PPi _ n ty sc)
342+ elab' ina@(_, a, _, qq) (PPi _ n ty sc)
336 = do attack; tyn <- getNameFrom (sMN 0 "ty")
343 = do attack; tyn <- getNameFrom (sMN 0 "ty")
337 claim tyn RType
344 claim tyn RType
338 n' <- case n of
345 n' <- case n of
@@ -340,10 +347,10 @@ elab ist info pattern opts fn tm
340 _ -> return n
347 _ -> return n
341 forall n' (Var tyn)
348 forall n' (Var tyn)
342 focus tyn
349 focus tyn
343− elabE (True, a, True) ty
350+ elabE (True, a, True, qq) ty
344− elabE (True, a, True) sc
351+ elabE (True, a, True, qq) sc
345 solve
352 solve
346− elab' ina@(_, a, inty) (PLet n ty val sc)
353+ elab' ina@(_, a, inty, qq) (PLet n ty val sc)
347 = do attack;
354 = do attack;
348 tyn <- getNameFrom (sMN 0 "letty")
355 tyn <- getNameFrom (sMN 0 "letty")
349 claim tyn RType
356 claim tyn RType
@@ -355,17 +362,17 @@ elab ist info pattern opts fn tm
355 Placeholder -> return ()
362 Placeholder -> return ()
356 _ -> do focus tyn
363 _ -> do focus tyn
357 explicit tyn
364 explicit tyn
358− elabE (True, a, True) ty
365+ elabE (True, a, True, qq) ty
359 focus valn
366 focus valn
360− elabE (True, a, True) val
367+ elabE (True, a, True, qq) val
361 env <- get_env
368 env <- get_env
362− elabE (True, a, inty) sc
369+ elabE (True, a, inty, qq) sc
363 -- HACK: If the name leaks into its type, it may leak out of
370 -- HACK: If the name leaks into its type, it may leak out of
364 -- scope outside, so substitute in the outer scope.
371 -- scope outside, so substitute in the outer scope.
365 expandLet n (case lookup n env of
372 expandLet n (case lookup n env of
366 Just (Let t v) -> v)
373 Just (Let t v) -> v)
367 solve
374 solve
368− elab' ina@(_, a, inty) (PGoal fc r n sc) = do
375+ elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do
369 rty <- goal
376 rty <- goal
370 attack
377 attack
371 tyn <- getNameFrom (sMN 0 "letty")
378 tyn <- getNameFrom (sMN 0 "letty")
@@ -374,10 +381,10 @@ elab ist info pattern opts fn tm
374 claim valn (Var tyn)
381 claim valn (Var tyn)
375 letbind n (Var tyn) (Var valn)
382 letbind n (Var tyn) (Var valn)
376 focus valn
383 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)])
378 env <- get_env
385 env <- get_env
379 computeLet n
386 computeLet n
380− elabE (True, a, inty) sc
387+ elabE (True, a, inty, qq) sc
381 solve
388 solve
382-- elab' ina (PLet n Placeholder
389-- elab' ina (PLet n Placeholder
383-- (PApp fc r [pexp (delab ist rty)]) sc)
390-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -433,16 +440,16 @@ elab ist info pattern opts fn tm
433 _ -> lift $ tfail (NoSuchVariable fn)
440 _ -> lift $ tfail (NoSuchVariable fn)
434 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
441 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
435 solve
442 solve
436− elab' (_, _, inty) (PApp fc (PRef _ f) args')
443+ elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')
437− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
444+ | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
438 = lift $ tfail (Msg "Typecase is not allowed")
445 = lift $ tfail (Msg "Typecase is not allowed")
439 -- if f is local, just do a simple_app
446 -- 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)
441 = do env <- get_env
448 = do env <- get_env
442 if (f `elem` map fst env && length args == 1)
449 if (f `elem` map fst env && length args == 1)
443 then -- simple app, as below
450 then -- simple app, as below
444− do simple_app (elabE (ina, g, inty) (PRef fc f))
451+ do simple_app (elabE (ina, g, inty, qq) (PRef fc f))
445− (elabE (True, g, inty) (getTm (head args)))
452+ (elabE (True, g, inty, qq) (getTm (head args)))
446 (show tm)
453 (show tm)
447 solve
454 solve
448 else
455 else
@@ -468,7 +475,7 @@ elab ist info pattern opts fn tm
468 -- Sort so that the implicit tactics and alternatives go last
475 -- Sort so that the implicit tactics and alternatives go last
469 let (ns', eargs) = unzip $
476 let (ns', eargs) = unzip $
470 sortBy cmpArg (zip ns args)
477 sortBy cmpArg (zip ns args)
471− elabArgs ist (ina || not isinf, guarded, inty)
478+ elabArgs ist (ina || not isinf, guarded, inty, qq)
472 [] fc False f ns'
479 [] fc False f ns'
473 (f == sUN "Force")
480 (f == sUN "Force")
474 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
481 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
@@ -542,9 +549,9 @@ elab ist info pattern opts fn tm
542 setInjective (PApp _ (PRef _ n) _) = setinj n
549 setInjective (PApp _ (PRef _ n) _) = setinj n
543 setInjective _ = return ()
550 setInjective _ = return ()
544
551
545− elab' ina@(_, a, inty) tm@(PApp fc f [arg])
552+ elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])
546 = erun fc $
553 = 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))
548 (show tm)
555 (show tm)
549 solve
556 solve
550 elab' ina Placeholder = do (h : hs) <- get_holes
557 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -593,7 +600,7 @@ elab ist info pattern opts fn tm
593 elab' ina sc
600 elab' ina sc
594 elab' ina (PRef fc letn)
601 elab' ina (PRef fc letn)
595 solve
602 solve
596− elab' ina@(_, a, inty) c@(PCase fc scr opts)
603+ elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)
597 = do attack
604 = do attack
598 tyn <- getNameFrom (sMN 0 "scty")
605 tyn <- getNameFrom (sMN 0 "scty")
599 claim tyn RType
606 claim tyn RType
@@ -602,7 +609,7 @@ elab ist info pattern opts fn tm
602 claim valn (Var tyn)
609 claim valn (Var tyn)
603 letbind scvn (Var tyn) (Var valn)
610 letbind scvn (Var tyn) (Var valn)
604 focus valn
611 focus valn
605− elabE (True, a, inty) scr
612+ elabE (True, a, inty, qq) scr
606 args <- get_env
613 args <- get_env
607 cname <- unique_hole' True (mkCaseName fn)
614 cname <- unique_hole' True (mkCaseName fn)
608 let cname' = mkN cname
615 let cname' = mkN cname
@@ -629,6 +636,75 @@ elab ist info pattern opts fn tm
629 elab' ina (PUnifyLog t) = do unifyLog True
636 elab' ina (PUnifyLog t) = do unifyLog True
630 elab' ina t
637 elab' ina t
631 unifyLog False
638 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"
632 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
708 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
633
709
634 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
710 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
@@ -720,7 +796,7 @@ elab ist info pattern opts fn tm
720
796
721 -- | Elaborate the arguments to a function
797 -- | Elaborate the arguments to a function
722 elabArgs :: IState -- ^ The current Idris state
798 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)
724 -> [Bool]
800 -> [Bool]
725 -> FC -- ^ Source location
801 -> FC -- ^ Source location
726 -> Bool
802 -> Bool
@@ -1441,21 +1517,159 @@ reflCall funName args
1441
1517
1442-- | Lift a term into its Language.Reflection.TT representation
1518-- | Lift a term into its Language.Reflection.TT representation
1443reflect :: Term -> Raw
1519reflect :: Term -> Raw
1444−reflect (P nt n t)
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
1445− = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1659+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
1446−reflect (V n)
1660+reflectQuote unq (V n)
1447 = reflCall "V" [RConstant (I n)]
1661 = reflCall "V" [RConstant (I n)]
1448−reflect (Bind n b x)
1662+reflectQuote unq (Bind n b x)
1449− = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1663+ = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
1450−reflect (App f x)
1664+reflectQuote unq (App f x)
1451− = reflCall "App" [reflect f, reflect x]
1665+ = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
1452−reflect (Constant c)
1666+reflectQuote unq (Constant c)
1453 = reflCall "TConst" [reflectConstant c]
1667 = reflCall "TConst" [reflectConstant c]
1454−reflect (Proj t i)
1668+reflectQuote unq (Proj t i)
1455− = reflCall "Proj" [reflect t, RConstant (I i)]
1669+ = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
1456−reflect (Erased) = Var (reflm "Erased")
1670+reflectQuote unq (Erased) = Var (reflm "Erased")
1457−reflect (Impossible) = Var (reflm "Impossible")
1671+reflectQuote unq (Impossible) = Var (reflm "Impossible")
1458−reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1672+reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
1459
1673
1460reflectNameType :: NameType -> Raw
1674reflectNameType :: NameType -> Raw
1461reflectNameType (Bound) = Var (reflm "Bound")
1675reflectNameType (Bound) = Var (reflm "Bound")
@@ -1482,25 +1696,44 @@ reflectName (MN i n)
1482reflectName (NErased) = Var (reflm "NErased")
1696reflectName (NErased) = Var (reflm "NErased")
1483reflectName n = Var (reflm "NErased") -- special name, not yet implemented
1697reflectName n = Var (reflm "NErased") -- special name, not yet implemented
1484
1698
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+
1485reflectBinder :: Binder Term -> Raw
1715reflectBinder :: Binder Term -> Raw
1486−reflectBinder (Lam t)
1716+reflectBinder = reflectBinderQuote []
1717+
1718+reflectBinderQuote :: [Name] -> Binder Term -> Raw
1719+reflectBinderQuote unq (Lam t)
1487− = reflCall "Lam" [Var (reflm "TT"), reflect t]
1720+ = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
1488−reflectBinder (Pi t)
1721+reflectBinderQuote unq (Pi t)
1489− = reflCall "Pi" [Var (reflm "TT"), reflect t]
1722+ = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t]
1490−reflectBinder (Let x y)
1723+reflectBinderQuote unq (Let x y)
1491− = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1724+ = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1492−reflectBinder (NLet x y)
1725+reflectBinderQuote unq (NLet x y)
1493− = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1726+ = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1494−reflectBinder (Hole t)
1727+reflectBinderQuote unq (Hole t)
1495− = reflCall "Hole" [Var (reflm "TT"), reflect t]
1728+ = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
1496−reflectBinder (GHole _ t)
1729+reflectBinderQuote unq (GHole _ t)
1497− = reflCall "GHole" [Var (reflm "TT"), reflect t]
1730+ = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
1498−reflectBinder (Guess x y)
1731+reflectBinderQuote unq (Guess x y)
1499− = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1732+ = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1500−reflectBinder (PVar t)
1733+reflectBinderQuote unq (PVar t)
1501− = reflCall "PVar" [Var (reflm "TT"), reflect t]
1734+ = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
1502−reflectBinder (PVTy t)
1735+reflectBinderQuote unq (PVTy t)
1503− = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1736+ = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
1504
1737
1505reflectConstant :: Const -> Raw
1738reflectConstant :: Const -> Raw
1506reflectConstant c@(I _) = reflCall "I" [RConstant c]
1739reflectConstant c@(I _) = reflCall "I" [RConstant c]
src/Idris/IBC.hs+2−2
@@ -1239,7 +1239,7 @@ instance Binary Using where
1239 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1239 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
1240
1240
1241instance Binary SyntaxInfo where
1241instance Binary SyntaxInfo where
1242− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)
1242+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)
1243 = do put x1
1243 = do put x1
1244 put x2
1244 put x2
1245 put x3
1245 put x3
@@ -1255,7 +1255,7 @@ instance Binary SyntaxInfo where
1255 x5 <- get
1255 x5 <- get
1256 x6 <- get
1256 x6 <- get
1257 x7 <- get
1257 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)
1259
1259
1260instance (Binary t) => Binary (PClause' t) where
1260instance (Binary t) => Binary (PClause' t) where
1261 put x
1261 put x
src/Idris/ParseExpr.hs+29
@@ -289,6 +289,8 @@ SimpleExpr ::=
289 | Constant
289 | Constant
290 | Type
290 | Type
291 | '_|_'
291 | '_|_'
292+ | Quasiquote
293+ | Unquote
292 | '_'
294 | '_'
293 ;
295 ;
294@
296@
@@ -326,6 +328,8 @@ simpleExpr syn =
326 <|> do symbol "_|_"
328 <|> do symbol "_|_"
327 fc <- getFC
329 fc <- getFC
328 return (PFalse fc)
330 return (PFalse fc)
331+ <|> quasiquote syn
332+ <|> unquote syn
329 <|> do lchar '_'; return Placeholder
333 <|> do lchar '_'; return Placeholder
330 <?> "expression"
334 <?> "expression"
331
335
@@ -587,6 +591,31 @@ constraintArg syn = do symbol "@{"
587 return (pconst e)
591 return (pconst e)
588 <?> "constraint argument"
592 <?> "constraint argument"
589
593
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+
590
619
591{-| Parses a record field setter expression
620{-| Parses a record field setter expression
592@
621@
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