From 1eeb5a464d583bbbaa3155a18a99ccc5651f9fd8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 23 Feb 2023 22:08:50 -0500
Subject: [PATCH] test: update test with levels

---
 unittest/core-logic/t1.expected |  9 ++++++---
 unittest/core-logic/t1.ml       | 24 ++++++++++++++++++++++++
 unittest/core/t_trace.expected  |  2 +-
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/unittest/core-logic/t1.expected b/unittest/core-logic/t1.expected
index 37c23abb..e42405d4 100644
--- a/unittest/core-logic/t1.expected
+++ b/unittest/core-logic/t1.expected
@@ -1,6 +1,6 @@
 type0 : Type
-typeof(type0) : Type(1)
-type tower: [Type;Type(1);Type(2);Type(3);Type(4)]
+typeof(type0) : Type.{2}
+type tower: [Type;Type.{2};Type.{3};Type.{4};Type.{5}]
 Bool: [true, false]
 a: a, b: b, typeof(a): Bool
 b2b: (Bool -> Bool)
@@ -22,4 +22,7 @@ t2: (= (tau -> (tau -> Bool)) (\x:tau. (\y:tau. (p2 x[1] y[0]))) (= tau))
   type: Bool
 f_vec: vec
   type: (Type -> (nat -> Type))
-  type of type: Type(1)
+  type of type: Type.{2}
+f_vec_weird: vec?
+  type: (Pi A:Type.{l1}. (Pi n:Type.{l2 + 1}. Type.{max(l1, l2)}))
+  type of type: Type.{imax(l1, imax(l2 + 1, max(l1, l2))) + 1}
diff --git a/unittest/core-logic/t1.ml b/unittest/core-logic/t1.ml
index 0619a06a..b6c74252 100644
--- a/unittest/core-logic/t1.ml
+++ b/unittest/core-logic/t1.ml
@@ -1,6 +1,7 @@
 open Sidekick_core_logic
 
 let store = Store.create ()
+let lvl_store = Store.lvl_store store
 let type_ = Term.type_ store
 let () = Fmt.printf "type0 : %a@." Term.pp_debug type_
 let () = Fmt.printf "typeof(type0) : %a@." Term.pp_debug (Term.ty type_)
@@ -110,3 +111,26 @@ let () =
   Fmt.printf "@[<v2>f_vec: %a@ type: %a@ type of type: %a@]@." Term.pp_debug
     f_vec Term.pp_debug (Term.ty f_vec) Term.pp_debug
     (Term.ty @@ Term.ty f_vec)
+
+(* now with some universes *)
+
+let f_vec_weird =
+  let v_A =
+    Var.make "A" @@ Term.type_of_univ store Level.(var lvl_store "l1")
+  in
+  let v_n =
+    Var.make "n"
+    @@ Term.type_of_univ store Level.(succ lvl_store @@ var lvl_store "l2")
+  in
+  Term.const store
+  @@ Str_const.make "vec?"
+       ~ty:
+         Term.(
+           pi store v_A @@ pi store v_n
+           @@ Term.type_of_univ store
+                Level.(max lvl_store (var lvl_store "l2") (var lvl_store "l1")))
+
+let () =
+  Fmt.printf "@[<v2>f_vec_weird: %a@ type: %a@ type of type: %a@]@."
+    Term.pp_debug f_vec_weird Term.pp_debug (Term.ty f_vec_weird) Term.pp_debug
+    (Term.ty @@ Term.ty f_vec_weird)
diff --git a/unittest/core/t_trace.expected b/unittest/core/t_trace.expected
index adba8b16..edc666fc 100644
--- a/unittest/core/t_trace.expected
+++ b/unittest/core/t_trace.expected
@@ -1,4 +1,4 @@
-buf containing pa: li0e2:Tyi0ee
+buf containing pa: li0e2:Ty1:1e
 li13e2:Tcd3:tag1:B2:tyi0e1:v4:Boolee
 li50e2:Tcd3:tag5:c.str2:tyi13e1:v1:aee
 li89e2:Tpl0:i13ei13eee