git.iko.soy/Idris-dev
on master help sign in
Initial support for unquotes
6a5a1f3David Raymond Christiansen
idris.cabal+1
compare with master
unifiedsplit
@@ -543,6 +543,7 @@ Library
543 , Idris.Docs
543 , Idris.Docs
544 , Idris.Docstrings
544 , Idris.Docstrings
545 , Idris.ElabDecls
545 , Idris.ElabDecls
546+ , Idris.ElabQuasiquote
546 , Idris.ElabTerm
547 , Idris.ElabTerm
547 , Idris.Erasure
548 , Idris.Erasure
548 , Idris.Error
549 , Idris.Error
src/Idris/ElabQuasiquote.hsnew file+128
@@ -0,0 +1,128 @@
1+module Idris.ElabQuasiquote (extractUnquotes) where
2+
3+import Idris.Core.Elaborate
4+import Idris.Core.TT
5+import Idris.AbsSyntax
6+
7+
8+extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
9+extractTUnquotes = undefined -- TODO
10+
11+extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
12+extractPArgUnquotes (PImp p m opts n t) =
13+ do (t', ex) <- extractUnquotes t
14+ return (PImp p m opts n t', ex)
15+extractPArgUnquotes (PExp p opts n t) =
16+ do (t', ex) <- extractUnquotes t
17+ return (PExp p opts n t', ex)
18+extractPArgUnquotes (PConstraint p opts n t) =
19+ do (t', ex) <- extractUnquotes t
20+ return (PConstraint p opts n t', ex)
21+extractPArgUnquotes (PTacImplicit p opts n scpt t) =
22+ do (scpt', ex1) <- extractUnquotes scpt
23+ (t', ex2) <- extractUnquotes t
24+ return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
25+
26+extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
27+extractDoUnquotes (DoExp fc tm)
28+ = do (tm', ex) <- extractUnquotes tm
29+ return (DoExp fc tm', ex)
30+extractDoUnquotes (DoBind fc n tm)
31+ = do (tm', ex) <- extractUnquotes tm
32+ return (DoBind fc n tm', ex)
33+extractDoUnquotes (DoBindP fc t t' alts)
34+ = fail "not done yet" -- TODO
35+extractDoUnquotes (DoLet fc n t t') = fail "not done yet" -- TODO
36+extractDoUnquotes (DoLetP fc t t') = fail "not done yet" -- TODO
37+
38+
39+extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
40+extractUnquotes (PLam n ty body)
41+ = do (ty', ex1) <- extractUnquotes ty
42+ (body', ex2) <- extractUnquotes body
43+ return (PLam n ty' body', ex1 ++ ex2)
44+extractUnquotes (PPi plicity n ty body)
45+ = do (ty', ex1) <- extractUnquotes ty
46+ (body', ex2) <- extractUnquotes body
47+ return (PPi plicity n ty' body', ex1 ++ ex2)
48+extractUnquotes (PLet n ty val body)
49+ = do (ty', ex1) <- extractUnquotes ty
50+ (val', ex2) <- extractUnquotes val
51+ (body', ex3) <- extractUnquotes body
52+ return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
53+extractUnquotes (PTyped tm ty)
54+ = do (tm', ex1) <- extractUnquotes tm
55+ (ty', ex2) <- extractUnquotes ty
56+ return (PTyped tm' ty', ex1 ++ ex2)
57+extractUnquotes (PApp fc f args)
58+ = do (f', ex1) <- extractUnquotes f
59+ args' <- mapM extractPArgUnquotes args
60+ let (args'', exs) = unzip args'
61+ return (PApp fc f' args'', ex1 ++ concat exs)
62+extractUnquotes (PAppBind fc f args)
63+ = do (f', ex1) <- extractUnquotes f
64+ args' <- mapM extractPArgUnquotes args
65+ let (args'', exs) = unzip args'
66+ return (PAppBind fc f' args'', ex1 ++ concat exs)
67+extractUnquotes (PCase fc expr cases)
68+ = do (expr', ex1) <- extractUnquotes expr
69+ let (pats, rhss) = unzip cases
70+ (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
71+ (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
72+ return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
73+extractUnquotes (PRefl fc x)
74+ = do (x', ex) <- extractUnquotes x
75+ return (PRefl fc x', ex)
76+extractUnquotes (PEq fc a b)
77+ = do (a', ex1) <- extractUnquotes a
78+ (b', ex2) <- extractUnquotes b
79+ return (PEq fc a' b', ex1 ++ ex2)
80+extractUnquotes (PRewrite fc x y z)
81+ = do (x', ex1) <- extractUnquotes x
82+ (y', ex2) <- extractUnquotes y
83+ case z of
84+ Just zz -> do (z', ex3) <- extractUnquotes zz
85+ return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
86+ Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
87+extractUnquotes (PPair fc info l r)
88+ = do (l', ex1) <- extractUnquotes l
89+ (r', ex2) <- extractUnquotes r
90+ return (PPair fc info l' r', ex1 ++ ex2)
91+extractUnquotes (PDPair fc info a b c)
92+ = do (a', ex1) <- extractUnquotes a
93+ (b', ex2) <- extractUnquotes b
94+ (c', ex3) <- extractUnquotes c
95+ return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
96+extractUnquotes (PAlternative b alts)
97+ = do alts' <- mapM extractUnquotes alts
98+ let (alts'', exs) = unzip alts'
99+ return (PAlternative b alts'', concat exs)
100+extractUnquotes (PHidden tm)
101+ = do (tm', ex) <- extractUnquotes tm
102+ return (PHidden tm', ex)
103+extractUnquotes (PGoal fc a n b)
104+ = do (a', ex1) <- extractUnquotes a
105+ (b', ex2) <- extractUnquotes b
106+ return (PGoal fc a' n b', ex1 ++ ex2)
107+extractUnquotes (PDoBlock steps)
108+ = do steps' <- mapM extractDoUnquotes steps
109+ let (steps'', exs) = unzip steps'
110+ return (PDoBlock steps'', concat exs)
111+extractUnquotes (PIdiom fc tm)
112+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
113+extractUnquotes (PProof tacs) = fail "not implemented yet"
114+extractUnquotes (PTactics tacs) = fail "not implemented yet"
115+extractUnquotes (PElabError err) = fail "not implemented yet"
116+extractUnquotes (PCoerced tm) = fail "not implemented yet"
117+extractUnquotes (PDisamb xs tm) = fail "not implemented yet"
118+extractUnquotes (PUnifyLog tm)
119+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
120+extractUnquotes (PNoImplicits tm)
121+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
122+extractUnquotes (PQuasiquote tm) = fail "Nested quasiquotes not supported"
123+extractUnquotes (PUnquote tm) =
124+ do n <- getNameFrom (sMN 0 "unquotation")
125+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
126+extractUnquotes x = return (x, []) -- no subterms!
127+
128+
src/Idris/ElabTerm.hs+62−36
@@ -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
@@ -630,11 +631,22 @@ elab ist info pattern opts fn tm
630 elab' ina t
631 elab' ina t
631 unifyLog False
632 unifyLog False
632 elab' ina (PQuasiquote t)
633 elab' ina (PQuasiquote t)
634+ = do -- First elaborate the unquoted subterms, replacing them with
635+ -- fresh names in the quasiquoted term
636+ (t, unq) <- extractUnquotes t
637+ mapM_ elabUnquote unq
638+ let unquoteNames = map fst unq
639+
633− = do -- Save the old state - we need a fresh proof state for this to
640+ -- Save the old state - we need a fresh proof state for this to
634 -- avoid capture
641 -- avoid capture
635 ctxt <- get_context
642 ctxt <- get_context
636 saveState
643 saveState
644+ updatePS (const .
645+ newProof (sMN 0 "q") ctxt $
637− updatePS (const $ newProof (sMN 0 "q") ctxt (P Ref (sNS (sUN "TT") ["Reflection", "Language"]) Erased))
646+ P Ref (sNS (sUN "TT") ["Reflection", "Language"]) Erased)
647+
648+ -- Re-add the unquotes
649+ mapM_ (flip claim (Var (sNS (sUN "TT") ["Reflection", "Language"]))) unquoteNames
638
650
639 -- Establish holes for the type and value of the term to be
651 -- Establish holes for the type and value of the term to be
640 -- quasiquoted
652 -- quasiquoted
@@ -654,14 +666,20 @@ elab ist info pattern opts fn tm
654 -- We now have an elaborated term. Reflect it and solve the
666 -- We now have an elaborated term. Reflect it and solve the
655 -- original goal
667 -- original goal
656 env <- get_env
668 env <- get_env
657− let qTerm = fmap (reflect . binderVal) $ lookup nTm env
669+ let qTerm = fmap (reflectQuote unquoteNames . binderVal) $ lookup nTm env
658 case qTerm of
670 case qTerm of
659 Just q -> do loadState
671 Just q -> do loadState
660 fill q
672 fill q
661 solve
673 solve
662 Nothing -> fail "Broken elaboration of quasiquote"
674 Nothing -> fail "Broken elaboration of quasiquote"
663−
675+ where elabUnquote (n, tm)
676+ = do qn <- getNameFrom (sMN 0 "unquotHole")
677+ let tt = sNS (sUN "TT") ["Reflection", "Language"]
678+ claim qn (Var tt)
679+ letbind n (Var tt) (Var qn)
680+ focus qn
681+ elab' ina tm
664− elab' ina (PUnquote t) = fail "Elaboration of unquotes not yet implemented"
682+ elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
665 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
683 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
666
684
667 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
685 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
@@ -1474,21 +1492,26 @@ reflCall funName args
1474
1492
1475-- | Lift a term into its Language.Reflection.TT representation
1493-- | Lift a term into its Language.Reflection.TT representation
1476reflect :: Term -> Raw
1494reflect :: Term -> Raw
1477−reflect (P nt n t)
1495+reflect = reflectQuote []
1496+
1497+-- | Create a reflected term, but leave refs to the provided name intact
1498+reflectQuote :: [Name] -> Term -> Raw
1499+reflectQuote unq (P nt n t)
1500+ | n `elem` unq = Var n
1478− = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1501+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
1479−reflect (V n)
1502+reflectQuote unq (V n)
1480 = reflCall "V" [RConstant (I n)]
1503 = reflCall "V" [RConstant (I n)]
1481−reflect (Bind n b x)
1504+reflectQuote unq (Bind n b x)
1482− = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1505+ = reflCall "Bind" [reflectName n, reflectBinder b, reflectQuote unq x]
1483−reflect (App f x)
1506+reflectQuote unq (App f x)
1484− = reflCall "App" [reflect f, reflect x]
1507+ = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
1485−reflect (Constant c)
1508+reflectQuote unq (Constant c)
1486 = reflCall "TConst" [reflectConstant c]
1509 = reflCall "TConst" [reflectConstant c]
1487−reflect (Proj t i)
1510+reflectQuote unq (Proj t i)
1488− = reflCall "Proj" [reflect t, RConstant (I i)]
1511+ = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
1489−reflect (Erased) = Var (reflm "Erased")
1512+reflectQuote unq (Erased) = Var (reflm "Erased")
1490−reflect (Impossible) = Var (reflm "Impossible")
1513+reflectQuote unq (Impossible) = Var (reflm "Impossible")
1491−reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1514+reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
1492
1515
1493reflectNameType :: NameType -> Raw
1516reflectNameType :: NameType -> Raw
1494reflectNameType (Bound) = Var (reflm "Bound")
1517reflectNameType (Bound) = Var (reflm "Bound")
@@ -1516,24 +1539,27 @@ reflectName (NErased) = Var (reflm "NErased")
1516reflectName n = Var (reflm "NErased") -- special name, not yet implemented
1539reflectName n = Var (reflm "NErased") -- special name, not yet implemented
1517
1540
1518reflectBinder :: Binder Term -> Raw
1541reflectBinder :: Binder Term -> Raw
1519−reflectBinder (Lam t)
1542+reflectBinder = reflectBinderQuote []
1543+
1544+reflectBinderQuote :: [Name] -> Binder Term -> Raw
1545+reflectBinderQuote unq (Lam t)
1520− = reflCall "Lam" [Var (reflm "TT"), reflect t]
1546+ = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
1521−reflectBinder (Pi t)
1547+reflectBinderQuote unq (Pi t)
1522− = reflCall "Pi" [Var (reflm "TT"), reflect t]
1548+ = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t]
1523−reflectBinder (Let x y)
1549+reflectBinderQuote unq (Let x y)
1524− = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1550+ = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1525−reflectBinder (NLet x y)
1551+reflectBinderQuote unq (NLet x y)
1526− = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1552+ = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1527−reflectBinder (Hole t)
1553+reflectBinderQuote unq (Hole t)
1528− = reflCall "Hole" [Var (reflm "TT"), reflect t]
1554+ = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
1529−reflectBinder (GHole _ t)
1555+reflectBinderQuote unq (GHole _ t)
1530− = reflCall "GHole" [Var (reflm "TT"), reflect t]
1556+ = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
1531−reflectBinder (Guess x y)
1557+reflectBinderQuote unq (Guess x y)
1532− = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1558+ = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
1533−reflectBinder (PVar t)
1559+reflectBinderQuote unq (PVar t)
1534− = reflCall "PVar" [Var (reflm "TT"), reflect t]
1560+ = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
1535−reflectBinder (PVTy t)
1561+reflectBinderQuote unq (PVTy t)
1536− = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1562+ = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
1537
1563
1538reflectConstant :: Const -> Raw
1564reflectConstant :: Const -> Raw
1539reflectConstant c@(I _) = reflCall "I" [RConstant c]
1565reflectConstant c@(I _) = reflCall "I" [RConstant c]