git.iko.soy/Idris-dev
on master help sign in
Update display of Set to Type
55a55ccEdwin Brady
src/Core/TT.hs+4−4
compare with master
unifiedsplit
@@ -14,7 +14,7 @@ import Util.Pretty hiding (Str)
14
14
15{- The language has:
15{- The language has:
16 * Full dependent types
16 * Full dependent types
17− * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
17+ * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
18 * Pattern matching letrec binding
18 * Pattern matching letrec binding
19 * (primitive types defined externally)
19 * (primitive types defined externally)
20
20
@@ -123,7 +123,7 @@ instance Show a => Show (TC a) where
123 show (Error str) = "Error: " ++ show str
123 show (Error str) = "Error: " ++ show str
124
124
125-- at some point, this instance should also carry type checking options
125-- at some point, this instance should also carry type checking options
126−-- (e.g. Set:Set)
126+-- (e.g. Type:Type)
127
127
128instance Monad TC where
128instance Monad TC where
129 return = OK
129 return = OK
@@ -719,7 +719,7 @@ prettyEnv env t = prettyEnv' env t False
719 prettySe 1 env x debug <+> text ("!" ++ show i)
719 prettySe 1 env x debug <+> text ("!" ++ show i)
720 prettySe p env (Constant c) debug = pretty c
720 prettySe p env (Constant c) debug = pretty c
721 prettySe p env Erased debug = text "[_]"
721 prettySe p env Erased debug = text "[_]"
722− prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
722+ prettySe p env (Set i) debug = text "Type" <+> (text . show $ i)
723
723
724 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
724 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
725 prettySb env n (Hole t) = prettyB env "?defer" "." n t
725 prettySb env n (Hole t) = prettyB env "?defer" "." n t
@@ -751,7 +751,7 @@ showEnv' env t dbg = se 10 env t where
751 se p env (Constant c) = show c
751 se p env (Constant c) = show c
752 se p env Erased = "[__]"
752 se p env Erased = "[__]"
753 se p env Impossible = "[impossible]"
753 se p env Impossible = "[impossible]"
754− se p env (Set i) = "Set " ++ show i
754+ se p env (Set i) = "Type " ++ show i
755
755
756 sb env n (Lam t) = showb env "\\ " " => " n t
756 sb env n (Lam t) = showb env "\\ " " => " n t
757 sb env n (Hole t) = showb env "? " ". " n t
757 sb env n (Hole t) = showb env "? " ". " n t
src/Idris/AbsSyntaxTree.hs+2−2
@@ -873,7 +873,7 @@ prettyImp impl = prettySe 10
873 where
873 where
874 prettyAs =
874 prettyAs =
875 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
875 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
876− prettySe p PSet = text "Set"
876+ prettySe p PSet = text "Type"
877 prettySe p (PConstant c) = pretty c
877 prettySe p (PConstant c) = pretty c
878 -- XXX: add pretty for tactics
878 -- XXX: add pretty for tactics
879 prettySe p (PProof ts) =
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 ++ ")"
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 ++ ")"
966 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
967 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
967 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
968− se p PSet = "Set"
968+ se p PSet = "Type"
969 se p (PConstant c) = show c
969 se p (PConstant c) = show c
970 se p (PProof ts) = "proof { " ++ show ts ++ "}"
970 se p (PProof ts) = "proof { " ++ show ts ++ "}"
971 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
971 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"