git.iko.soy/Idris-dev
on master help sign in
Elaborate qquotes in fresh proof state
f8ec244David Raymond Christiansen
src/Idris/AbsSyntax.hs+2
compare with master
unifiedsplit
@@ -1272,6 +1272,7 @@ addImplBound ist ns = addImpl' False ns [] ist
1272addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1272addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1273addImplBoundInf ist ns inf = addImpl' False ns inf ist
1273addImplBoundInf ist ns inf = addImpl' False ns inf ist
1274
1274
1275+-- | Add the implicit arguments to applications in the term
1275addImpl :: IState -> PTerm -> PTerm
1276addImpl :: IState -> PTerm -> PTerm
1276addImpl = addImpl' False [] []
1277addImpl = addImpl' False [] []
1277
1278
@@ -1358,6 +1359,7 @@ addImpl' inpat env infns ist ptm
1358 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1359 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1359 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1360 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1360 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1361 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1362+ ai env ds (PQuasiquote tm) = PQuasiquote (ai env ds tm)
1361 ai env ds tm = tm
1363 ai env ds tm = tm
1362
1364
1363 handleErr (Left err) = PElabError err
1365 handleErr (Left err) = PElabError err
src/Idris/ElabTerm.hs+17−6
@@ -630,7 +630,14 @@ elab ist info pattern opts fn tm
630 elab' ina t
630 elab' ina t
631 unifyLog False
631 unifyLog False
632 elab' ina (PQuasiquote t)
632 elab' ina (PQuasiquote t)
633+ = do -- Save the old state - we need a fresh proof state for this to
634+ -- avoid capture
635+ ctxt <- get_context
636+ saveState
637+ updatePS (const $ newProof (sMN 0 "q") ctxt (P Ref (sNS (sUN "TT") ["Reflection", "Language"]) Erased))
638+
633− = do -- Establish holes for the type and value of the term to be quasiquoted
639+ -- Establish holes for the type and value of the term to be
640+ -- quasiquoted
634 qTy <- getNameFrom (sMN 0 "qquoteTy")
641 qTy <- getNameFrom (sMN 0 "qquoteTy")
635 claim qTy RType
642 claim qTy RType
636 qTm <- getNameFrom (sMN 0 "qquoteTm")
643 qTm <- getNameFrom (sMN 0 "qquoteTm")
@@ -644,12 +651,16 @@ elab ist info pattern opts fn tm
644 -- Elaborate the quasiquoted term into the hole that was
651 -- Elaborate the quasiquoted term into the hole that was
645 focus qTm
652 focus qTm
646 elab' ina t
653 elab' ina t
647− -- We now have an elaborated term. Reflect it and solve the original goal
654+ -- We now have an elaborated term. Reflect it and solve the
648− ctxt <- get_context
655+ -- original goal
649 env <- get_env
656 env <- get_env
650− let qTerm = normalise ctxt env (P Bound nTm Erased)
657+ let qTerm = fmap (reflect . binderVal) $ lookup nTm env
651− fill $ reflect qTerm
658+ case qTerm of
659+ Just q -> do loadState
660+ fill q
652− solve
661+ solve
662+ Nothing -> fail "Broken elaboration of quasiquote"
663+
653 elab' ina (PUnquote t) = fail "Elaboration of unquotes not yet implemented"
664 elab' ina (PUnquote t) = fail "Elaboration of unquotes not yet implemented"
654 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
665 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
655
666