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

CHANGELOG+4

compare with master

unifiedsplit

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

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+ 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.

17

21

18

22

19New in 0.9.13:

23New in 0.9.13:

idris.cabal+3

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

418 test/quasiquote001/run

419 test/quasiquote001/*.idr

420 test/quasiquote001/expected

421+ test/quasiquote002/run

422+ test/quasiquote002/*.idr

423+ test/quasiquote002/expected

421

424

422 test/records001/run

425 test/records001/run

423 test/records001/*.idr

426 test/records001/*.idr

src/Idris/AbsSyntax.hs+2−1

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

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

1359 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq 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)

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

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

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

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

1363 ai qq env ds tm = tm

1364 ai qq env ds tm = tm

1364

1365

src/Idris/AbsSyntaxTree.hs+4−2

@@ -702,7 +702,7 @@ data PTerm = PQuote Raw

702 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces

703 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

704 | PNoImplicits PTerm -- ^ never run implicit converions on the term

705− | PQuasiquote PTerm -- ^ `(Term)

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

706 | PUnquote PTerm -- ^ ,Term

707 deriving Eq

708

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

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

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

1356 prettySe p bnd (PElabError s) = pretty s

1357+ -- Quasiquote pprinting ignores bound vars

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

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

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

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

1359

1361

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

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

src/Idris/ElabQuasiquote.hs+1−1

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

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

161extractUnquotes (PNoImplicits tm)

162 = 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"

164extractUnquotes (PUnquote tm) =

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

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

src/Idris/ElabTerm.hs+9−3

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

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

637 elab' ina t

638 unifyLog False

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

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

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.

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

663 movelast n)

664 unquoteNames

665

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

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

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

667 -- quasiquoted

668 -- quasiquoted

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

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

669 claim qTy RType

670 claim qTy RType

671+ movelast qTy

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

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

671 claim qTm (Var qTy)

673 claim qTm (Var qTy)

674+

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

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

673 -- the hole doesn't disappear

676 -- the hole doesn't disappear

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

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

675 letbind nTm (Var qTy) (Var qTm)

678 letbind nTm (Var qTy) (Var qTm)

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

677− movelast qTy

678

679

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

679

685

680 -- Elaborate the quasiquoted term into the hole

686 -- Elaborate the quasiquoted term into the hole

681 focus qTm

687 focus qTm

src/Idris/ParseExpr.hs+4−1

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

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

601 symbol "`("

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

603+ g <- optional $ do

604+ symbol ":"

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

603 symbol ")"

606 symbol ")"

604− return $ PQuasiquote e

607+ return $ PQuasiquote e g

605 <?> "quasiquotation"

608 <?> "quasiquotation"

606

609

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

610{-| 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

2+

3+import Language.Reflection

4+import Language.Reflection.Utils

5+

6+uCon : TT

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

8+

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