git.iko.soy/Idris-dev
on master help sign in
PSet -> PType
commit7fefa89e2f23942107dd52d30828c109968066f4 authorraichoo <raichoo@googlemail.com> dateWed 12 Dec 2012, 18:32 (14 years ago) parente4da568
7 files changed+22−22
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+10−10 src/Idris/AbsSyntaxTree.hs+4−4 src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+1−1 src/Idris/IBC.hs+2−2 src/Idris/Parser.hs+3−3
src/Idris/AbsSyntax.hs+10−10
@@ -379,8 +379,8 @@ bi = FC "builtin" 0
379379inferTy = MN 0 "__Infer"
380380inferCon = MN 0 "__infer"
381381inferDecl = PDatadecl inferTy
382− PSet
383− [("", inferCon, PPi impl (MN 0 "A") PSet (
382+ PType
383+ [("", inferCon, PPi impl (MN 0 "A") PType (
384384 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
385385 (PRef bi inferTy)), bi)]
386386
@@ -403,17 +403,17 @@ primNames = [unitTy, unitCon,
403403
404404unitTy = MN 0 "__Unit"
405405unitCon = MN 0 "__II"
406−unitDecl = PDatadecl unitTy PSet
406+unitDecl = PDatadecl unitTy PType
407407 [("", unitCon, PRef bi unitTy, bi)]
408408
409409falseTy = MN 0 "__False"
410−falseDecl = PDatadecl falseTy PSet []
410+falseDecl = PDatadecl falseTy PType []
411411
412412pairTy = MN 0 "__Pair"
413413pairCon = MN 0 "__MkPair"
414−pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
415− [("", pairCon, PPi impl (n "A") PSet (
416− PPi impl (n "B") PSet (
414+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
415+ [("", pairCon, PPi impl (n "A") PType (
416+ PPi impl (n "B") PType (
417417 PPi expl (n "a") (PRef bi (n "A")) (
418418 PPi expl (n "b") (PRef bi (n "B"))
419419 (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)
422422
423423eqTy = UN "="
424424eqCon = UN "refl"
425−eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
425+eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
426426 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
427− PSet)
428− [("", eqCon, PPi impl (n "a") PSet (
427+ PType)
428+ [("", eqCon, PPi impl (n "a") PType (
429429 PPi impl (n "x") (PRef bi (n "a"))
430430 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
431431 pimp (n "b") Placeholder,
src/Idris/AbsSyntaxTree.hs+4−4
@@ -428,7 +428,7 @@ data PTerm = PQuote Raw
428428 | PDPair FC PTerm PTerm PTerm
429429 | PAlternative Bool [PTerm] -- True if only one may work
430430 | PHidden PTerm -- irrelevant or hidden pattern
431− | PSet
431+ | PType
432432 | PConstant Const
433433 | Placeholder
434434 | PDoBlock [PDo]
@@ -873,7 +873,7 @@ prettyImp impl = prettySe 10
873873 where
874874 prettyAs =
875875 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
876− prettySe p PSet = text "Set"
876+ prettySe p PType = text "Set"
877877 prettySe p (PConstant c) = pretty c
878878 -- XXX: add pretty for tactics
879879 prettySe p (PProof ts) =
@@ -965,7 +965,7 @@ showImp impl tm = se 10 tm where
965965 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
966966 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
967967 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
968− se p PSet = "Set"
968+ se p PType = "Set"
969969 se p (PConstant c) = show c
970970 se p (PProof ts) = "proof { " ++ show ts ++ "}"
971971 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
@@ -1009,7 +1009,7 @@ instance Sized PTerm where
10091009 size (PDPair fs left ty right) = 1 + size left + size ty + size right
10101010 size (PAlternative a alts) = 1 + size alts
10111011 size (PHidden hidden) = size hidden
1012− size PSet = 1
1012+ size PType = 1
10131013 size (PConstant const) = 1 + size const
10141014 size Placeholder = 1
10151015 size (PDoBlock dos) = 1 + size dos
src/Idris/Delaborate.hs+1−1
@@ -38,7 +38,7 @@ delab' ist tm fullname = de [] tm
3838 de env (Constant i) = PConstant i
3939 de env Erased = Placeholder
4040 de env Impossible = Placeholder
41− de env (Set i) = PSet
41+ de env (Set i) = PType
4242
4343 dens x | fullname = x
4444 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 ->
713713 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
714714elabClass info syn doc fc constraints tn ps ds
715715 = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
716− let tty = pibind ps PSet
716+ let tty = pibind ps PType
717717 let constraint = PApp fc (PRef fc tn)
718718 (map (pexp . PRef fc) (map fst ps))
719719 -- build data declaration
src/Idris/ElabTerm.hs+1−1
@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm
101101 local f = do e <- get_env
102102 return (f `elem` map fst e)
103103
104− elab' ina PSet = do apply RSet []; solve
104+ elab' ina PType = do apply RSet []; solve
105105 elab' ina (PConstant c) = do apply (RConstant c) []; solve
106106 elab' ina (PQuote r) = do fill r; solve
107107 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
src/Idris/IBC.hs+2−2
@@ -1210,7 +1210,7 @@ instance Binary PTerm where
12101210 put x2
12111211 PHidden x1 -> do putWord8 16
12121212 put x1
1213− PSet -> putWord8 17
1213+ PType -> putWord8 17
12141214 PConstant x1 -> do putWord8 18
12151215 put x1
12161216 Placeholder -> putWord8 19
@@ -1294,7 +1294,7 @@ instance Binary PTerm where
12941294 return (PAlternative x1 x2)
12951295 16 -> do x1 <- get
12961296 return (PHidden x1)
1297− 17 -> return PSet
1297+ 17 -> return PType
12981298 18 -> do x1 <- get
12991299 return (PConstant x1)
13001300 19 -> return Placeholder
src/Idris/Parser.hs+3−3
@@ -551,7 +551,7 @@ pClass syn = do doc <- option "" (pDocComment '|')
551551 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
552552 return (i, ty)
553553 <|> do i <- pName;
554− return (i, PSet)
554+ return (i, PType)
555555
556556pInstance :: SyntaxInfo -> IParser [PDecl]
557557pInstance syn = do reserved "instance"; fc <- pfc
@@ -760,7 +760,7 @@ pSimpleExpr syn =
760760 <|> try (do c <- pConstant
761761 fc <- pfc
762762 return (modifyConst syn fc (PConstant c)))
763− <|> do reserved "Type"; return PSet
763+ <|> do reserved "Type"; return PType
764764 <|> try (do symbol "()"
765765 fc <- pfc
766766 return (PTrue fc))
@@ -1193,7 +1193,7 @@ pData syn = try (do doc <- option "" (pDocComment '|')
11931193 fc <- pfc
11941194 tyn_in <- pfName
11951195 args <- many pName
1196− let ty = bindArgs (map (const PSet) args) PSet
1196+ let ty = bindArgs (map (const PType) args) PType
11971197 let tyn = expandNS syn tyn_in
11981198 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
11991199 try (lchar '=') <|> do reserved "where"