From b7acf39c39bfd2e78fda3b2821c9128debdf2f50 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 5 Mar 2023 16:48:29 +0100 Subject: [PATCH] remove universe type --- lib/Quox/Parser/Syntax.idr | 2 +- lib/Quox/Syntax.idr | 1 - lib/Quox/Syntax/Term/Base.idr | 5 ++++- lib/Quox/Syntax/Term/Pretty.idr | 10 ++++++++++ lib/Quox/Syntax/Universe.idr | 34 --------------------------------- lib/quox-lib.ipkg | 1 - tests/Tests/Equal.idr | 8 ++++---- tests/TypingImpls.idr | 4 ++-- 8 files changed, 21 insertions(+), 44 deletions(-) delete mode 100644 lib/Quox/Syntax/Universe.idr diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 80bb2a1..001570f 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -84,7 +84,7 @@ mutual (t : Term Three d n) -> (0 _ : NotClo t) => PTerm toPTermWith' ds ns s = case s of - TYPE (U l) => + TYPE l => TYPE l Pi qty arg (S [x] res) => Pi qty (Just x) (toPTermWith ds ns arg) diff --git a/lib/Quox/Syntax.idr b/lib/Quox/Syntax.idr index 5cfd888..969661c 100644 --- a/lib/Quox/Syntax.idr +++ b/lib/Quox/Syntax.idr @@ -6,5 +6,4 @@ import public Quox.Syntax.Qty import public Quox.Syntax.Shift import public Quox.Syntax.Subst import public Quox.Syntax.Term -import public Quox.Syntax.Universe import public Quox.Syntax.Var diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 4e50f88..f694ace 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -3,7 +3,6 @@ module Quox.Syntax.Term.Base import public Quox.Syntax.Var import public Quox.Syntax.Shift import public Quox.Syntax.Subst -import public Quox.Syntax.Universe import public Quox.Syntax.Qty import public Quox.Syntax.Dim import public Quox.Name @@ -32,6 +31,10 @@ public export 0 TSubstLike : Type TSubstLike = Type -> Nat -> Nat -> Nat -> Type +public export +0 Universe : Type +Universe = Nat + public export 0 TagVal : Type TagVal = String diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 0da58c8..d23c4a1 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -32,6 +32,16 @@ ofD = hl Syntax "of" returnD = hl Syntax "return" +export +prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL) +prettyUnivSuffix l = + ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l) + where + sub : Char -> Char + sub c = case c of + '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄' + '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c + export prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q => Pretty.HasEnv m => diff --git a/lib/Quox/Syntax/Universe.idr b/lib/Quox/Syntax/Universe.idr deleted file mode 100644 index 586af05..0000000 --- a/lib/Quox/Syntax/Universe.idr +++ /dev/null @@ -1,34 +0,0 @@ -module Quox.Syntax.Universe - -import Quox.Pretty - -import Data.Fin -import Derive.Prelude - -%default total -%language ElabReflection - - -public export -data Universe = U Nat -%name Universe l - -%runElab derive "Universe" [Eq, Ord, Show] - -export -PrettyHL Universe where - prettyM (U l) = pure $ hl Free $ pretty l - -export -prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL) -prettyUnivSuffix (U l) = - ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l) - where - sub : Char -> Char - sub c = case c of - '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄' - '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c - -export %inline -fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Universe -fromInteger x = U $ fromInteger x diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 99e0005..de96f7c 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -26,7 +26,6 @@ modules = Quox.Syntax.Term.Pretty, Quox.Syntax.Term.Split, Quox.Syntax.Term.Subst, - Quox.Syntax.Universe, Quox.Syntax.Var, Quox.Definition, Quox.Reduce, diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 31ad5c9..eef697d 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -260,11 +260,11 @@ tests = "equality & subtyping" :- [ "free var" :- let au_bu = fromList - [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), - ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))] + [("A", mkDef Any (TYPE 1) (TYPE 0)), + ("B", mkDef Any (TYPE 1) (TYPE 0))] au_ba = fromList - [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), - ("B", mkDef Any (TYPE (U 1)) (FT "A"))] + [("A", mkDef Any (TYPE 1) (TYPE 0)), + ("B", mkDef Any (TYPE 1) (FT "A"))] in [ testEq "A = A" $ equalE empty (F "A") (F "A"), diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index 592a2af..98a60c3 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -63,8 +63,8 @@ PrettyHL q => ToInfo (Error q) where toInfo (ClashU mode k l) = [("type", "ClashU"), ("mode", show mode), - ("left", prettyStr True k), - ("right", prettyStr True l)] + ("left", show k), + ("right", show l)] toInfo (ClashQ pi rh) = [("type", "ClashQ"), ("left", prettyStr True pi),