9040aba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1348 from david-christiansen/quasiquote

Add goal types to quasiquotes.

commit9040aba62b37f2ad6e1fa0edbd682d604dc37aed authorDavid Christiansen <david@davidchristiansen.dk> dateMon 30 Jun 2014, 20:14 (12 years ago) parenta3ccdef dac312b

10 files changed+62−8

compare with master

unifiedsplit

CHANGELOG+4 idris.cabal+3 src/Idris/AbsSyntax.hs+2−1 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/ElabQuasiquote.hs+1−1 src/Idris/ElabTerm.hs+9−3 src/Idris/ParseExpr.hs+4−1 test/quasiquote002/GoalQQuote.idr+30 test/quasiquote002/expected+1 test/quasiquote002/run+4

CHANGELOG+4

@@ -14,6 +14,10 @@ New in 0.9.14:

1414 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected

1515 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected

1616 terms to splice in, while on the LHS they are patterns.

17+ A quasiquote expression can be given a goal type for the elaborator, which helps with

18+ disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)

19+ quotes the unit type.

20+ Both goal types and quasiquote are typechecked in the global environment.

1721

1822

1923New in 0.9.13:

idris.cabal+3

@@ -418,6 +418,9 @@ Extra-source-files:

418418 test/quasiquote001/run

419419 test/quasiquote001/*.idr

420420 test/quasiquote001/expected

421+ test/quasiquote002/run

422+ test/quasiquote002/*.idr

423+ test/quasiquote002/expected

421424

422425 test/records001/run

423426 test/records001/*.idr

src/Idris/AbsSyntax.hs+2−1

@@ -1358,7 +1358,8 @@ addImpl' inpat env infns ist ptm

13581358 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

13591359 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

13601360 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)

1361+ ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1362+ (fmap (ai True env ds) g)

13621363 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

13631364 ai qq env ds tm = tm

13641365

src/Idris/AbsSyntaxTree.hs+4−2

@@ -702,7 +702,7 @@ 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)

705+ | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

706706 | PUnquote PTerm -- ^ ,Term

707707 deriving Eq

708708

@@ -1354,7 +1354,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13541354 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

13551355 prettySe p bnd (PCoerced t) = prettySe p bnd t

13561356 prettySe p bnd (PElabError s) = pretty s

1357− prettySe p bnd (PQuasiquote t) = text "`(" <> prettySe p bnd t <> text ")"

1357+ -- Quasiquote pprinting ignores bound vars

1358+ prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"

1359+ prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"

13581360 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t

13591361

13601362 prettySe p bnd _ = text "missing pretty-printer for term"

src/Idris/ElabQuasiquote.hs+1−1

@@ -160,7 +160,7 @@ extractUnquotes (PUnifyLog tm)

160160 = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm

161161extractUnquotes (PNoImplicits tm)

162162 = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm

163−extractUnquotes (PQuasiquote tm) = fail "Nested quasiquotes not supported"

163+extractUnquotes (PQuasiquote _ _) = fail "Nested quasiquotes not supported"

164164extractUnquotes (PUnquote tm) =

165165 do n <- getNameFrom (sMN 0 "unquotation")

166166 return (PRef (fileFC "(unquote)") n, [(n, tm)])

src/Idris/ElabTerm.hs+9−3

@@ -636,7 +636,7 @@ elab ist info pattern opts fn tm

636636 elab' ina (PUnifyLog t) = do unifyLog True

637637 elab' ina t

638638 unifyLog False

639− elab' (ina, g, inty, qq) (PQuasiquote t)

639+ elab' (ina, g, inty, qq) (PQuasiquote t goal) -- TODO: goal type

640640 = do -- First extract the unquoted subterms, replacing them with fresh

641641 -- names in the quasiquoted term. Claim their reflections to be

642642 -- of type TT.

@@ -663,19 +663,25 @@ elab ist info pattern opts fn tm

663663 movelast n)

664664 unquoteNames

665665

666+ -- Determine whether there's an explicit goal type, and act accordingly

666667 -- Establish holes for the type and value of the term to be

667668 -- quasiquoted

668669 qTy <- getNameFrom (sMN 0 "qquoteTy")

669670 claim qTy RType

671+ movelast qTy

670672 qTm <- getNameFrom (sMN 0 "qquoteTm")

671673 claim qTm (Var qTy)

674+

672675 -- Let-bind the result of elaborating the contained term, so that

673676 -- the hole doesn't disappear

674677 nTm <- getNameFrom (sMN 0 "quotedTerm")

675678 letbind nTm (Var qTy) (Var qTm)

676− -- We must solve the type later through unification

677− movelast qTy

678679

680+ -- Fill out the goal type, if relevant

681+ case goal of

682+ Nothing -> return ()

683+ Just gTy -> do focus qTy

684+ elabE (ina, g, inty, True) gTy

679685

680686 -- Elaborate the quasiquoted term into the hole

681687 focus qTm

src/Idris/ParseExpr.hs+4−1

@@ -600,8 +600,11 @@ quasiquote :: SyntaxInfo -> IdrisParser PTerm

600600quasiquote syn = do guard (not (syn_in_quasiquote syn))

601601 symbol "`("

602602 e <- expr syn { syn_in_quasiquote = True , inPattern = False}

603+ g <- optional $ do

604+ symbol ":"

605+ expr syn { inPattern = False } -- don't allow antiquotes

603606 symbol ")"

604− return $ PQuasiquote e

607+ return $ PQuasiquote e g

605608 <?> "quasiquotation"

606609

607610{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

test/quasiquote002/GoalQQuote.idrnew file+30

@@ -0,0 +1,30 @@

1+module GoalQQuote

3+import Language.Reflection

4+import Language.Reflection.Utils

6+uCon : TT

7+uCon = `(() : ())

9+uTy : TT

10+uTy = `(() : Type)

11+

12+isDefault : TT -> Bool

13+isDefault `(()) = True

14+isDefault _ = False

15+

16+pTy : TT -> TT -> TT

17+pTy a b = `((~a, ~b) : Type)

18+

19+pair : TT -> TT -> TT

20+pair a b = `((~a, ~b) : (Nat, Nat))

21+

22+vect : TT

23+vect = `([1,2] : Vect 2 Nat)

24+

25+namespace Main

26+ main : IO ()

27+ main = putStrLn $

28+ if isDefault uCon then "con"

29+ else if isDefault uTy then "ty"

30+ else "neither"

test/quasiquote002/expectednew file+1

@@ -0,0 +1 @@

1+con

test/quasiquote002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ GoalQQuote.idr -o quasiquote002

3+./quasiquote002

4+rm -f quasiquote002 *.ibc