d6458bb · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -31,6 +31,8 @@ New in 0.9.18:

31* The return types of `Vect.findIndex`, `Vect.elemIndex` and

32 `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`

33* A new :browse command shows the contents of a namespace

34+* `{n} is syntax for a quotation of the reflected representation of the global

35+ name n, if it is uniquely determined

34

36

35New in 0.9.17:

37New in 0.9.17:

36--------------

38--------------

idris.cabal+3−1

@@ -568,7 +568,9 @@ Extra-source-files:

568 test/quasiquote005/run

569 test/quasiquote005/*.idr

570 test/quasiquote005/expected

571−

571+ test/quasiquote006/run

572+ test/quasiquote006/*.idr

573+ test/quasiquote006/expected

572

574

573 test/records001/run

575 test/records001/run

574 test/records001/*.idr

576 test/records001/*.idr

libs/base/Language/Reflection/Utils.idr+40−12

@@ -61,18 +61,46 @@ binderTy (Guess t1 t2) = t1

61binderTy (PVar t) = t

62binderTy (PVTy t) = t

63

64+mutual

64−instance Show TTName where

65+ instance Show SpecialName where

66+ show (WhereN i n1 n2) = "(WhereN " ++ show i ++ " " ++

67+ show n1 ++ " " ++ show n2 ++ ")"

68+ show (WithN i n) = "(WithN " ++ show i ++ " " ++ show n ++ ")"

69+ show (InstanceN i ss) = "(InstanceN " ++ show i ++ " " ++ show ss ++ ")"

70+ show (ParentN n s) = "(ParentN " ++ show n ++ " " ++ show s ++ ")"

71+ show (MethodN n) = "(MethodN " ++ show n ++ ")"

72+ show (CaseN n) = "(CaseN " ++ show n ++ ")"

73+ show (ElimN n) = "(ElimN " ++ show n ++ ")"

74+ show (InstanceCtorN n) = "(InstanceCtorN " ++ show n ++ ")"

75+ show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"

76+

77+ instance Show TTName where

65− show (UN str) = "(UN " ++ str ++ ")"

78+ show (UN str) = "(UN " ++ str ++ ")"

66− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"

79+ show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"

67− show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"

80+ show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"

81+ show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"

68− show NErased = "NErased"

82+ show NErased = "NErased"

69−

83+

84+mutual

70−instance Eq TTName where

85+ instance Eq TTName where

71− (UN str1) == (UN str2) = str1 == str2

86+ (UN str1) == (UN str2) = str1 == str2

72− (NS n ns) == (NS n' ns') = n == n' && ns == ns'

87+ (NS n ns) == (NS n' ns') = n == n' && ns == ns'

73− (MN i str) == (MN i' str') = i == i' && str == str'

88+ (MN i str) == (MN i' str') = i == i' && str == str'

74− NErased == NErased = True

89+ NErased == NErased = True

90+ (SN sn) == (SN sn') = assert_total $ sn == sn'

75− x == y = False

91+ x == y = False

92+

93+ instance Eq SpecialName where

94+ (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'

95+ (WithN i n) == (WithN i' n') = i == i' && n == n'

96+ (InstanceN i ss) == (InstanceN i' ss') = i == i' && ss == ss'

97+ (ParentN n s) == (ParentN n' s') = n == n' && s == s'

98+ (MethodN n) == (MethodN n') = n == n'

99+ (CaseN n) == (CaseN n') = n == n'

100+ (ElimN n) == (ElimN n') = n == n'

101+ (InstanceCtorN n) == (InstanceCtorN n') = n == n'

102+ (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

103+ _ == _ = False

76

104

77instance Show TTUExp where

105instance Show TTUExp where

78 show (UVar i) = "(UVar " ++ show i ++ ")"

106 show (UVar i) = "(UVar " ++ show i ++ ")"

src/Idris/AbsSyntaxTree.hs+3

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

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

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

821 | PUnquote PTerm -- ^ ~Term

822+ | PQuoteName Name -- ^ `{n}

822 | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

823 | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

823 deriving (Eq, Data, Typeable)

824 deriving (Eq, Data, Typeable)

824

825

@@ -1038,6 +1039,7 @@ highestFC (PUnifyLog tm) = highestFC tm

1038highestFC (PNoImplicits tm) = highestFC tm

1039highestFC (PNoImplicits tm) = highestFC tm

1039highestFC (PQuasiquote _ _) = Nothing

1040highestFC (PQuasiquote _ _) = Nothing

1040highestFC (PUnquote tm) = highestFC tm

1041highestFC (PUnquote tm) = highestFC tm

1042+highestFC (PQuoteName _) = Nothing

1041

1043

1042-- Type class data

1044-- Type class data

1043

1045

@@ -1589,6 +1591,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

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

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

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

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

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

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

1594+ prettySe p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"

1592

1595

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

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

1594

1597

src/Idris/DeepSeq.hs+1

@@ -243,6 +243,7 @@ instance NFData PTerm where

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

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

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

246+ rnf (PQuoteName x1) = rnf x1 `seq` ()

246 rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

247 rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

247

248

248instance (NFData t) => NFData (PTactic' t) where

249instance (NFData t) => NFData (PTactic' t) where

src/Idris/Elab/Term.hs+7

@@ -1074,6 +1074,13 @@ elab ist info emode opts fn tm

1074

1075

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

1077+ elab' ina fc (PQuoteName n) =

1078+ do ctxt <- get_context

1079+ case lookupNameDef n ctxt of

1080+ [(n', _)] -> do fill $ reflectName n'

1081+ solve

1082+ [] -> lift . tfail . NoSuchVariable $ n

1083+ more -> lift . tfail . CantResolveAlts $ map fst more

1077 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

1084 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

1078 elab' ina fc (PHidden t)

1085 elab' ina fc (PHidden t)

1079 | reflection = elab' ina fc t

1086 | reflection = elab' ina fc t

src/Idris/Error.hs+1

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

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

147 Foldable.mapM_ (warnDisamb ist) goal

148warnDisamb ist (PUnquote tm) = warnDisamb ist tm

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

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

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

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

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

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

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

src/Idris/ParseExpr.hs+14

@@ -311,6 +311,7 @@ SimpleExpr ::=

311 | Type

312 | 'Void'

313 | Quasiquote

314+ | NameQuote

314 | Unquote

315 | Unquote

315 | '_'

316 | '_'

316 ;

317 ;

@@ -355,6 +356,7 @@ simpleExpr syn =

355 return (PAppBind fc s [])

356 return (PAppBind fc s [])

356 <|> bracketed (disallowImp syn)

357 <|> bracketed (disallowImp syn)

357 <|> quasiquote syn

358 <|> quasiquote syn

359+ <|> namequote syn

358 <|> unquote syn

360 <|> unquote syn

359 <|> do lchar '_'; return Placeholder

361 <|> do lchar '_'; return Placeholder

360 <?> "expression"

362 <?> "expression"

@@ -639,6 +641,18 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

639 return $ PUnquote e

641 return $ PUnquote e

640 <?> "unquotation"

642 <?> "unquotation"

641

643

644+{-| Parses a quotation of a name (for using the elaborator to resolve boring details)

645+

646+> NameQuote ::= '`{' Name '}'

647+

648+-}

649+namequote :: SyntaxInfo -> IdrisParser PTerm

650+namequote syn = do symbol "`{"

651+ n <- fnName

652+ symbol "}"

653+ return $ PQuoteName n

654+ <?> "quoted name"

655+

642

656

643{-| Parses a record field setter expression

657{-| Parses a record field setter expression

644@

658@

test/quasiquote006/expectednew file+13

@@ -0,0 +1,13 @@

1+quasiquote006.idr:9:3:

2+When elaborating right hand side of b:

3+Can't disambiguate name: ForeignEnv.Nil,

4+ Prelude.List.Nil

5+quasiquote006.idr:12:3:

6+When elaborating right hand side of c:

7+No such variable alsdkjflkj

8+quasiquote006.idr:15:3:

9+When elaborating right hand side of d:

10+Can't disambiguate name: ForeignEnv.::,

11+ Prelude.List.::,

12+ Prelude.Stream.::

13+quasiquote006.idr:17:3:Main.d already defined

test/quasiquote006/quasiquote006.idrnew file+21

@@ -0,0 +1,21 @@

1+

2+a : TTName

3+a = `{Nat}

4+

5+aOK : a = NS (UN "Nat") ["Nat", "Prelude"]

6+aOK = Refl

7+

8+b : TTName

9+b = `{Nil}

10+

11+c : TTName

12+c = `{alsdkjflkj}

13+

14+d : TTName

15+d = `{(::)}

16+

17+d : TTName

18+d = `{List.(::)}

19+

20+dOK : d = NS (UN "::") ["List", "Prelude"]

21+dOK = Refl

test/quasiquote006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --check --nocolour --quiet --consolewidth 70 quasiquote006.idr

3+rm -f *.ibc