simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

test: update test with levels

Browse source
This commit is contained in:
Simon Cruanes 2023-02-23 22:08:50 -05:00
parent 9ea96a6b61
commit 1eeb5a464d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 31 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
unittest/core-logic/t1.expected
View file

@ -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}

24
unittest/core-logic/t1.ml
View file

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

2
unittest/core/t_trace.expected
View file

@ -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