git.iko.soy/Idris-dev
on master help sign in
Elaborate qquotes in fresh proof state
commitf8ec2444ff27413a792bdf1471d7192a9f58a44b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 24 Jun 2014, 15:11 (12 years ago) parent766b955
2 files changed+19−6
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+2 src/Idris/ElabTerm.hs+17−6
src/Idris/AbsSyntax.hs+2
@@ -1272,6 +1272,7 @@ addImplBound ist ns = addImpl' False ns [] ist
12721272addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
12731273addImplBoundInf ist ns inf = addImpl' False ns inf ist
12741274
1275+-- | Add the implicit arguments to applications in the term
12751276addImpl :: IState -> PTerm -> PTerm
12761277addImpl = addImpl' False [] []
12771278
@@ -1358,6 +1359,7 @@ addImpl' inpat env infns ist ptm
13581359 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
13591360 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
13601361 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1362+ ai env ds (PQuasiquote tm) = PQuasiquote (ai env ds tm)
13611363 ai env ds tm = tm
13621364
13631365 handleErr (Left err) = PElabError err
src/Idris/ElabTerm.hs+17−6
@@ -630,7 +630,14 @@ elab ist info pattern opts fn tm
630630 elab' ina t
631631 unifyLog False
632632 elab' ina (PQuasiquote t)
633− = do -- Establish holes for the type and value of the term to be quasiquoted
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+
639+ -- Establish holes for the type and value of the term to be
640+ -- quasiquoted
634641 qTy <- getNameFrom (sMN 0 "qquoteTy")
635642 claim qTy RType
636643 qTm <- getNameFrom (sMN 0 "qquoteTm")
@@ -644,12 +651,16 @@ elab ist info pattern opts fn tm
644651 -- Elaborate the quasiquoted term into the hole that was
645652 focus qTm
646653 elab' ina t
647− -- We now have an elaborated term. Reflect it and solve the original goal
648− ctxt <- get_context
654+ -- We now have an elaborated term. Reflect it and solve the
655+ -- original goal
649656 env <- get_env
650− let qTerm = normalise ctxt env (P Bound nTm Erased)
651− fill $ reflect qTerm
652− solve
657+ let qTerm = fmap (reflect . binderVal) $ lookup nTm env
658+ case qTerm of
659+ Just q -> do loadState
660+ fill q
661+ solve
662+ Nothing -> fail "Broken elaboration of quasiquote"
663+
653664 elab' ina (PUnquote t) = fail "Elaboration of unquotes not yet implemented"
654665 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
655666