d6458bb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add `{n} for quotations of the global name n

commitd6458bb2df9aaad800723465e1c2030ba08802be authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 22 Apr 2015, 15:47 (12 years ago) parent3592edb

11 files changed+108−13

compare with master

unifiedsplit

CHANGELOG+2 idris.cabal+3−1 libs/base/Language/Reflection/Utils.idr+40−12 src/Idris/AbsSyntaxTree.hs+3 src/Idris/DeepSeq.hs+1 src/Idris/Elab/Term.hs+7 src/Idris/Error.hs+1 src/Idris/ParseExpr.hs+14 test/quasiquote006/expected+13 test/quasiquote006/quasiquote006.idr+21 test/quasiquote006/run+3

CHANGELOG+2

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

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

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

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

3436

3537New in 0.9.17:

3638--------------

idris.cabal+3−1

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

568568 test/quasiquote005/run

569569 test/quasiquote005/*.idr

570570 test/quasiquote005/expected

571−

571+ test/quasiquote006/run

572+ test/quasiquote006/*.idr

573+ test/quasiquote006/expected

572574

573575 test/records001/run

574576 test/records001/*.idr

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

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

6161binderTy (PVar t) = t

6262binderTy (PVTy t) = t

6363

64−instance Show TTName where

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

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

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

68− show NErased = "NErased"

69−

70−instance Eq TTName where

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

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

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

74− NErased == NErased = True

75− x == y = False

64+mutual

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

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

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

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

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

82+ show NErased = "NErased"

83+

84+mutual

85+ instance Eq TTName where

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

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

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

89+ NErased == NErased = True

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

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

76104

77105instance Show TTUExp where

78106 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

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

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

821821 | PUnquote PTerm -- ^ ~Term

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

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

823824 deriving (Eq, Data, Typeable)

824825

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

10381039highestFC (PNoImplicits tm) = highestFC tm

10391040highestFC (PQuasiquote _ _) = Nothing

10401041highestFC (PUnquote tm) = highestFC tm

1042+highestFC (PQuoteName _) = Nothing

10411043

10421044-- Type class data

10431045

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

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

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

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

15921595

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

15941597

src/Idris/DeepSeq.hs+1

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

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

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

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

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

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

247248

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

src/Idris/Elab/Term.hs+7

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

10741074

10751075

10761076 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

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

10781085 elab' ina fc (PHidden t)

10791086 | reflection = elab' ina fc t

src/Idris/Error.hs+1

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

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

147147 Foldable.mapM_ (warnDisamb ist) goal

148148warnDisamb ist (PUnquote tm) = warnDisamb ist tm

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

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

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

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

src/Idris/ParseExpr.hs+14

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

311311 | Type

312312 | 'Void'

313313 | Quasiquote

314+ | NameQuote

314315 | Unquote

315316 | '_'

316317 ;

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

355356 return (PAppBind fc s [])

356357 <|> bracketed (disallowImp syn)

357358 <|> quasiquote syn

359+ <|> namequote syn

358360 <|> unquote syn

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

360362 <?> "expression"

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

639641 return $ PUnquote e

640642 <?> "unquotation"

641643

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+

642656

643657{-| Parses a record field setter expression

644658@

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 @@

2+a : TTName

3+a = `{Nat}

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

6+aOK = Refl

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