7cc7c32 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make top level type 'Type*'

UniqueType : Type 1 Type : Type 1 Type* indicates that either UniqueType or Type is allowed (which means uniqueness must be preserved in the definition)

commit7cc7c32367ddaa5fb3b9eecf0d49bd8a7c5667d3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 14 Aug 2014, 09:41 (12 years ago) parent9ceece1

2 files changed+6−2

compare with master

unifiedsplit

src/Idris/Core/TT.hs+5−1 src/Idris/ParseExpr.hs+1−1

src/Idris/Core/TT.hs+5−1

@@ -594,7 +594,11 @@ constDocs (B64V v) = "A vector of sixty-four-bit values"

594594constDocs prim = "Undocumented"

595595

596596data Universe = UniqueType | AllTypes

597− deriving (Show, Eq, Ord)

597+ deriving (Eq, Ord)

598+

599+instance Show Universe where

600+ show UniqueType = "UniqueType"

601+ show AllTypes = "Type*"

598602

599603data Raw = Var Name

600604 | RBind Name (Binder Raw) Raw

src/Idris/ParseExpr.hs+1−1

@@ -307,9 +307,9 @@ simpleExpr syn =

307307 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

308308 <|> proofExpr syn

309309 <|> tacticsExpr syn

310+ <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

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

311312 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

312− <|> do reserved "AllTypes"; return $ PUniverse AllTypes

313313 <|> do c <- constant

314314 fc <- getFC

315315 return (modifyConst syn fc (PConstant c))