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

src/Idris/AbsSyntax.hs+10−10

compare with master

unifiedsplit

@@ -379,8 +379,8 @@ bi = FC "builtin" 0

379inferTy = MN 0 "__Infer"

380inferCon = MN 0 "__infer"

381inferDecl = PDatadecl inferTy

382− PSet

382+ PType

383− [("", inferCon, PPi impl (MN 0 "A") PSet (

383+ [("", inferCon, PPi impl (MN 0 "A") PType (

384 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

385 (PRef bi inferTy)), bi)]

386

@@ -403,17 +403,17 @@ primNames = [unitTy, unitCon,

403

404unitTy = MN 0 "__Unit"

405unitCon = MN 0 "__II"

406−unitDecl = PDatadecl unitTy PSet

406+unitDecl = PDatadecl unitTy PType

407 [("", unitCon, PRef bi unitTy, bi)]

408

409falseTy = MN 0 "__False"

410−falseDecl = PDatadecl falseTy PSet []

410+falseDecl = PDatadecl falseTy PType []

411

412pairTy = MN 0 "__Pair"

413pairCon = MN 0 "__MkPair"

414−pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

414+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

415− [("", pairCon, PPi impl (n "A") PSet (

415+ [("", pairCon, PPi impl (n "A") PType (

416− PPi impl (n "B") PSet (

416+ PPi impl (n "B") PType (

417 PPi expl (n "a") (PRef bi (n "A")) (

418 PPi expl (n "b") (PRef bi (n "B"))

419 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

@@ -422,10 +422,10 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

422

423eqTy = UN "="

424eqCon = UN "refl"

425−eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

425+eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

426 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

427− PSet)

427+ PType)

428− [("", eqCon, PPi impl (n "a") PSet (

428+ [("", eqCon, PPi impl (n "a") PType (

429 PPi impl (n "x") (PRef bi (n "a"))

430 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,

431 pimp (n "b") Placeholder,

src/Idris/AbsSyntaxTree.hs+4−4

@@ -428,7 +428,7 @@ data PTerm = PQuote Raw

428 | PDPair FC PTerm PTerm PTerm

429 | PAlternative Bool [PTerm] -- True if only one may work

430 | PHidden PTerm -- irrelevant or hidden pattern

431− | PSet

431+ | PType

432 | PConstant Const

433 | Placeholder

434 | PDoBlock [PDo]

@@ -873,7 +873,7 @@ prettyImp impl = prettySe 10

873 where

874 prettyAs =

875 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as

876− prettySe p PSet = text "Set"

876+ prettySe p PType = text "Set"

877 prettySe p (PConstant c) = pretty c

878 -- XXX: add pretty for tactics

879 prettySe p (PProof ts) =

@@ -965,7 +965,7 @@ showImp impl tm = se 10 tm where

965 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

966 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

967 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

968− se p PSet = "Set"

968+ se p PType = "Set"

969 se p (PConstant c) = show c

970 se p (PProof ts) = "proof { " ++ show ts ++ "}"

971 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

@@ -1009,7 +1009,7 @@ instance Sized PTerm where

1009 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1010 size (PAlternative a alts) = 1 + size alts

1011 size (PHidden hidden) = size hidden

1012− size PSet = 1

1012+ size PType = 1

1013 size (PConstant const) = 1 + size const

1014 size Placeholder = 1

1015 size (PDoBlock dos) = 1 + size dos

src/Idris/Delaborate.hs+1−1

@@ -38,7 +38,7 @@ delab' ist tm fullname = de [] tm

38 de env (Constant i) = PConstant i

39 de env Erased = Placeholder

40 de env Impossible = Placeholder

41− de env (Set i) = PSet

41+ de env (Set i) = PType

42

43 dens x | fullname = x

44 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of

src/Idris/ElabDecls.hs+1−1

@@ -713,7 +713,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

713 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

714elabClass info syn doc fc constraints tn ps ds

715 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

716− let tty = pibind ps PSet

716+ let tty = pibind ps PType

717 let constraint = PApp fc (PRef fc tn)

718 (map (pexp . PRef fc) (map fst ps))

719 -- build data declaration

src/Idris/ElabTerm.hs+1−1

@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm

101 local f = do e <- get_env

102 return (f `elem` map fst e)

103

104− elab' ina PSet = do apply RSet []; solve

104+ elab' ina PType = do apply RSet []; solve

105 elab' ina (PConstant c) = do apply (RConstant c) []; solve

106 elab' ina (PQuote r) = do fill r; solve

107 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

src/Idris/IBC.hs+2−2

@@ -1210,7 +1210,7 @@ instance Binary PTerm where

1210 put x2

1211 PHidden x1 -> do putWord8 16

1212 put x1

1213− PSet -> putWord8 17

1213+ PType -> putWord8 17

1214 PConstant x1 -> do putWord8 18

1215 put x1

1216 Placeholder -> putWord8 19

@@ -1294,7 +1294,7 @@ instance Binary PTerm where

1294 return (PAlternative x1 x2)

1295 16 -> do x1 <- get

1296 return (PHidden x1)

1297− 17 -> return PSet

1297+ 17 -> return PType

1298 18 -> do x1 <- get

1299 return (PConstant x1)

1300 19 -> return Placeholder

src/Idris/Parser.hs+3−3

@@ -551,7 +551,7 @@ pClass syn = do doc <- option "" (pDocComment '|')

551 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

552 return (i, ty)

553 <|> do i <- pName;

554− return (i, PSet)

554+ return (i, PType)

555

556pInstance :: SyntaxInfo -> IParser [PDecl]

557pInstance syn = do reserved "instance"; fc <- pfc

@@ -760,7 +760,7 @@ pSimpleExpr syn =

760 <|> try (do c <- pConstant

761 fc <- pfc

762 return (modifyConst syn fc (PConstant c)))

763− <|> do reserved "Type"; return PSet

763+ <|> do reserved "Type"; return PType

764 <|> try (do symbol "()"

765 fc <- pfc

766 return (PTrue fc))

@@ -1193,7 +1193,7 @@ pData syn = try (do doc <- option "" (pDocComment '|')

1193 fc <- pfc

1194 tyn_in <- pfName

1195 args <- many pName

1196− let ty = bindArgs (map (const PSet) args) PSet

1196+ let ty = bindArgs (map (const PType) args) PType

1197 let tyn = expandNS syn tyn_in

1198 option (PData doc syn fc co (PLaterdecl tyn ty)) (do

1199 try (lchar '=') <|> do reserved "where"