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

CHANGELOG+2

compare with master

unifiedsplit

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

5----------------

6

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

8

10

9Library updates

11Library updates

10---------------

12---------------

src/Idris/AbsSyntaxTree.hs+6−4

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

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

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

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

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

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

975 deriving (Eq, Data, Typeable)

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

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

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

1034mapPTermFC 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)

1036

1037{-!

1038dg instance Binary PTerm

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

1259highestFC (PNoImplicits tm) = highestFC tm

1260highestFC (PQuasiquote _ _) = Nothing

1261highestFC (PUnquote tm) = highestFC tm

1262−highestFC (PQuoteName _ fc) = Just fc

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

1263highestFC (PRunElab fc _ _) = Just fc

1264highestFC (PConstSugar fc _) = Just fc

1265highestFC (PAppImpl t _) = highestFC t

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

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

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

1872 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 "}}"

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

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

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

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

1876 text "%runElab" <$>

1878 text "%runElab" <$>

src/Idris/DeepSeq.hs+1−1

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

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

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

272 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` ()

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

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

276

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

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

1204

1205

1206 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) =

1208 do ctxt <- get_context

1211 do ctxt <- get_context

1209 env <- get_env

1212 env <- get_env

1210 case lookup n env of

1213 case lookup n env of

src/Idris/Error.hs+1−1

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

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

148 Foldable.mapM_ (warnDisamb ist) goal

149warnDisamb ist (PUnquote tm) = warnDisamb ist tm

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

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

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

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

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

src/Idris/IBC.hs+7−5

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 119

43+ibcVersion = 120

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

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

1674 put x2

1675 PUnquote x1 -> do putWord8 43

1676 put x1

1677− PQuoteName x1 x2 -> do putWord8 44

1677+ PQuoteName x1 x2 x3 -> do putWord8 44

1678− put x1

1678+ put x1

1679− put x2

1679+ put x2

1680+ put x3

1680 PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1681 PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1681 put x1

1682 put x1

1682 put x2

1683 put x2

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

1822 return (PUnquote x1)

1823 return (PUnquote x1)

1823 44 -> do x1 <- get

1824 44 -> do x1 <- get

1824 x2 <- get

1825 x2 <- get

1826+ x3 <- get

1825− return (PQuoteName x1 x2)

1827+ return (PQuoteName x1 x2 x3)

1826 45 -> do x1 <- get

1828 45 -> do x1 <- get

1827 x2 <- get

1829 x2 <- get

1828 x3 <- get

1830 x3 <- get

src/Idris/ParseExpr.hs+9−4

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

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

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

228 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'

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

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

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

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

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

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

736

737

737-}

738-}

738namequote :: SyntaxInfo -> IdrisParser PTerm

739namequote :: 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))

740 (n, nfc) <- fnName

745 (n, nfc) <- fnName

741− endFC <- symbolFC "}"

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

742 mapM_ (uncurry highlightP)

747 mapM_ (uncurry highlightP)

743 [ (startFC, AnnKeyword)

748 [ (startFC, AnnKeyword)

744 , (endFC, AnnKeyword)

749 , (endFC, AnnKeyword)

745 , (spanFC startFC endFC, AnnQuasiquote)

750 , (spanFC startFC endFC, AnnQuasiquote)

746 ]

751 ]

747− return $ PQuoteName n nfc

752+ return $ PQuoteName n res nfc

748 <?> "quoted name"

753 <?> "quoted name"

749

754

750

755