c486513 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added label type 'name

This is intended for field/effect disambiguation. "name" can be any valid identifier. Two labels are definitionally equal if they have the same name.

commitc4865138aabc6046949211c8ac8693c9de7e9047 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 13 Jan 2014, 12:42 (13 years ago) parent23787c2

3 files changed+13−3

unifiedsplit

CHANGELOG+4

@@ -3,6 +3,10 @@ New in 0.9.11:

44* Agda-style equational reasoning (in Syntax.PreorderReasoning)

55* 'case' construct now abstracts over the scrutinee in its type

6+* Added label type 'name (equivalent to the empty type).

7+ This is intended for field/effect disambiguation. "name" can be any

8+ valid identifier. Two labels are definitionally equal if they have the

9+ same name.

610

711New in 0.9.10:

812--------------

libs/prelude/Builtins.idr+3

@@ -12,6 +12,9 @@ getProof (a ** v) = v

1212

1313FalseElim : _|_ -> a

1414

15+-- For 'symbol syntax. 'foo becomes Symbol_ "foo"

16+data Symbol_ : String -> Type where

17+

1518-- ------------------------------------------------------ [ For rewrite tactic ]

1619replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

1720replace refl prf = prf

src/Idris/ParseExpr.hs+6−3

@@ -287,9 +287,12 @@ simpleExpr syn =

287287 <|> tacticsExpr syn

288288 <|> caseExpr syn

289289 <|> do reserved "Type"; return PType

290− <|> do c <- constant

291− fc <- getFC

292− return (modifyConst syn fc (PConstant c))

290+ <|> try (do c <- constant

291+ fc <- getFC

292+ return (modifyConst syn fc (PConstant c)))

293+ <|> try (do symbol "'"; fc <- getFC; str <- name

294+ return (PApp fc (PRef fc (UN "Symbol_"))

295+ [pexp (PConstant (Str (show str)))]))

293296 <|> do fc <- getFC

294297 x <- fnName

295298 return (PRef fc x)