55a55cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update display of Set to Type

commit55a55cc6eaa9ffa4ea54683c667a62e0e8c8b42c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 13 Dec 2012, 10:57 (14 years ago) parente4da568

2 files changed+6−6

compare with master

unifiedsplit

src/Core/TT.hs+4−4 src/Idris/AbsSyntaxTree.hs+2−2

src/Core/TT.hs+4−4

@@ -14,7 +14,7 @@ import Util.Pretty hiding (Str)

1414

1515{- The language has:

1616 * 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, ...

1818 * Pattern matching letrec binding

1919 * (primitive types defined externally)

2020

@@ -123,7 +123,7 @@ instance Show a => Show (TC a) where

123123 show (Error str) = "Error: " ++ show str

124124

125125-- at some point, this instance should also carry type checking options

126−-- (e.g. Set:Set)

126+-- (e.g. Type:Type)

127127

128128instance Monad TC where

129129 return = OK

@@ -719,7 +719,7 @@ prettyEnv env t = prettyEnv' env t False

719719 prettySe 1 env x debug <+> text ("!" ++ show i)

720720 prettySe p env (Constant c) debug = pretty c

721721 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)

723723

724724 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

725725 prettySb env n (Hole t) = prettyB env "?defer" "." n t

@@ -751,7 +751,7 @@ showEnv' env t dbg = se 10 env t where

751751 se p env (Constant c) = show c

752752 se p env Erased = "[__]"

753753 se p env Impossible = "[impossible]"

754− se p env (Set i) = "Set " ++ show i

754+ se p env (Set i) = "Type " ++ show i

755755

756756 sb env n (Lam t) = showb env "\\ " " => " n t

757757 sb env n (Hole t) = showb env "? " ". " n t

src/Idris/AbsSyntaxTree.hs+2−2

@@ -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 PSet = text "Type"

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 PSet = "Type"

969969 se p (PConstant c) = show c

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

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