60b43b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add raw name quotes

The raw quote of name n, written `{{n}}, quotes n directly to its AST without performing any lookup or resolution, allowing a much shorter syntax.

commit60b43b48b754c8f425af070896330bebd5acc8ac authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 7 Sep 2015, 14:08 (11 years ago) parentd952c94

7 files changed+30−16

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntaxTree.hs+6−4 src/Idris/DeepSeq.hs+1−1 src/Idris/Elab/Term.hs+4−1 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+7−5 src/Idris/ParseExpr.hs+9−4

CHANGELOG+2

@@ -5,6 +5,8 @@ Language updates

55----------------

77* Improved unification by implementing a pattern unification rule

8+* The syntax `{{n}} quotes n without resolving it, allowing short syntax

9+ for defining new names. `{n} still quotes n to an existing name in scope.

810

911Library updates

1012---------------

src/Idris/AbsSyntaxTree.hs+6−4

@@ -969,7 +969,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

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

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

971971 | PUnquote PTerm -- ^ ~Term

972− | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular

972+ | PQuoteName Name Bool FC -- ^ `{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.

973973 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

974974 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.

975975 deriving (Eq, Data, Typeable)

@@ -1032,7 +1032,7 @@ mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapP

10321032mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)

10331033mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns

10341034mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)

1035−mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)

1035+mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)

10361036

10371037{-!

10381038dg instance Binary PTerm

@@ -1259,7 +1259,7 @@ highestFC (PUnifyLog tm) = highestFC tm

12591259highestFC (PNoImplicits tm) = highestFC tm

12601260highestFC (PQuasiquote _ _) = Nothing

12611261highestFC (PUnquote tm) = highestFC tm

1262−highestFC (PQuoteName _ fc) = Just fc

1262+highestFC (PQuoteName _ _ fc) = Just fc

12631263highestFC (PRunElab fc _ _) = Just fc

12641264highestFC (PConstSugar fc _) = Just fc

12651265highestFC (PAppImpl t _) = highestFC t

@@ -1870,7 +1870,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18701870 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"

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

18721872 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t

1873− prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"

1873+ prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end

1874+ where start = if res then "`{" else "`{{"

1875+ end = if res then "}" else "}}"

18741876 prettySe d p bnd (PRunElab _ tm _) =

18751877 bracket p funcAppPrec . group . align . hang 2 $

18761878 text "%runElab" <$>

src/Idris/DeepSeq.hs+1−1

@@ -270,7 +270,7 @@ instance NFData PTerm where

270270 rnf (PNoImplicits x1) = rnf x1 `seq` ()

271271 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

272272 rnf (PUnquote x1) = rnf x1 `seq` ()

273− rnf (PQuoteName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

273+ rnf (PQuoteName x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

274274 rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

275275 rnf (PConstSugar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

276276

src/Idris/Elab/Term.hs+4−1

@@ -1204,7 +1204,10 @@ elab ist info emode opts fn tm

12041204

12051205

12061206 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

1207− elab' ina fc (PQuoteName n nfc) =

1207+ elab' ina fc (PQuoteName n False nfc) =

1208+ do fill $ reflectName n

1209+ solve

1210+ elab' ina fc (PQuoteName n True nfc) =

12081211 do ctxt <- get_context

12091212 env <- get_env

12101213 case lookup n env of

src/Idris/Error.hs+1−1

@@ -147,7 +147,7 @@ warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm

147147warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>

148148 Foldable.mapM_ (warnDisamb ist) goal

149149warnDisamb ist (PUnquote tm) = warnDisamb ist tm

150−warnDisamb ist (PQuoteName _ _) = return ()

150+warnDisamb ist (PQuoteName _ _ _) = return ()

151151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

152152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

153153warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm

src/Idris/IBC.hs+7−5

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 119

43+ibcVersion = 120

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -1674,9 +1674,10 @@ instance Binary PTerm where

16741674 put x2

16751675 PUnquote x1 -> do putWord8 43

16761676 put x1

1677− PQuoteName x1 x2 -> do putWord8 44

1678− put x1

1679− put x2

1677+ PQuoteName x1 x2 x3 -> do putWord8 44

1678+ put x1

1679+ put x2

1680+ put x3

16801681 PIfThenElse x1 x2 x3 x4 -> do putWord8 45

16811682 put x1

16821683 put x2

@@ -1822,7 +1823,8 @@ instance Binary PTerm where

18221823 return (PUnquote x1)

18231824 44 -> do x1 <- get

18241825 x2 <- get

1825− return (PQuoteName x1 x2)

1826+ x3 <- get

1827+ return (PQuoteName x1 x2 x3)

18261828 45 -> do x1 <- get

18271829 x2 <- get

18281830 x3 <- get

src/Idris/ParseExpr.hs+9−4

@@ -226,7 +226,8 @@ updateSynMatch = update

226226 update ns (PNoImplicits t) = PNoImplicits $ update ns t

227227 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)

228228 update ns (PUnquote t) = PUnquote $ update ns t

229− update ns (PQuoteName n fc) = uncurry PQuoteName (updateB ns (n, fc))

229+ update ns (PQuoteName n res fc) = let (n', fc') = (updateB ns (n, fc))

230+ in PQuoteName n' res fc'

230231 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp

231232 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t

232233 -- PConstSugar probably can't contain anything substitutable, but it's hard to track

@@ -736,15 +737,19 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

736737

737738-}

738739namequote :: SyntaxInfo -> IdrisParser PTerm

739−namequote syn = do startFC <- symbolFC "`{"

740+namequote syn = do (startFC, res) <-

741+ try (do fc <- symbolFC "`{{"

742+ return (fc, False)) <|>

743+ (do fc <- symbolFC "`{"

744+ return (fc, True))

740745 (n, nfc) <- fnName

741− endFC <- symbolFC "}"

746+ endFC <- if res then symbolFC "}" else symbolFC "}}"

742747 mapM_ (uncurry highlightP)

743748 [ (startFC, AnnKeyword)

744749 , (endFC, AnnKeyword)

745750 , (spanFC startFC endFC, AnnQuasiquote)

746751 ]

747− return $ PQuoteName n nfc

752+ return $ PQuoteName n res nfc

748753 <?> "quoted name"

749754

750755