test: add more to unittest/core-logic

unittest/core-logic/t1.expected

@@ -1,19 +1,21 @@
-type0 : type
-typeof(type0) : type_1
-type tower: [type;type_1;type_2;type_3;type_4;type_5;type_6;type_7;type_8;
-             type_9]
+type0 : Type
+typeof(type0) : Type(1)
+type tower: [Type;Type(1);Type(2);Type(3);Type(4)]
 a: a, b: b, typeof(a): Bool
-pi Bool Bool
 b2b: (Bool -> Bool)
 p(a): p a
 p(b): p b
 q(a): q a
 q(b): q b
 typeof(p a): Bool
-pi Bool Bool
-pi Bool Bool
-pi Bool (Bool -> Bool)
-lxy_px: (\x:Bool. (\y:Bool. p x))
+lxy_px: (\x:Bool. (\y:Bool. p x[1]))
   type: (Bool -> (Bool -> Bool))
-lxy_px a b: ((\x:Bool. (\y:Bool. p x))) a b
+  type of type: Type
+lxy_px a b: ((\x:Bool. (\y:Bool. p x[1]))) a b
+  type: Bool
+(=): =
+  type: (Pi Alpha:Type. (Pi _:Alpha[0]. (Alpha[1] -> Bool)))
+p2: p2
+  type: (tau -> (tau -> Bool))
+t2: = ((tau -> (tau -> Bool))) ((\x:tau. (\y:tau. p2 x[1] y[0]))) (= tau)
   type: Bool

unittest/core-logic/t1.ml

@@ -1,13 +1,13 @@
 open Sidekick_core_logic
 
 let store = Store.create ()
-let t0 = Term.type_ store
-let () = Fmt.printf "type0 : %a@." Term.pp_debug t0
-let () = Fmt.printf "typeof(type0) : %a@." Term.pp_debug (Term.get_ty store t0)
+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_)
 
 let l =
-  CCSeq.unfold (fun ty -> Some (ty, Term.get_ty store ty)) t0
-  |> CCSeq.take 10 |> CCSeq.to_list
+  CCSeq.unfold (fun ty -> Some (ty, Term.ty ty)) type_
+  |> CCSeq.take 5 |> CCSeq.to_list
 
 let () = Fmt.printf "type tower: %a@." (Fmt.Dump.list Term.pp_debug) l
 let () = assert (Term.(equal (type_ store) (type_ store)))
@@ -18,7 +18,7 @@ let b = Term.const store @@ Str_const.make "b" ~ty:bool
 
 let () =
   Fmt.printf "a: %a, b: %a, typeof(a): %a@." Term.pp_debug a Term.pp_debug b
-    Term.pp_debug (Term.ty_exn a)
+    Term.pp_debug (Term.ty a)
 
 let () = assert (Term.(equal a a))
 let () = assert (not Term.(equal a b))
@@ -38,7 +38,7 @@ let () = assert (Term.(equal pa (app store p a)))
 
 (* *)
 
-let ty_pa = Term.ty_exn pa
+let ty_pa = Term.ty pa
 let () = Fmt.printf "typeof(p a): %a@." Term.pp_debug ty_pa
 
 (* *)
@@ -50,10 +50,50 @@ let y = Term.var store v_y
 let lxy_px = Term.lam store v_x @@ Term.lam store v_y @@ Term.app store p x
 
 let () =
-  Fmt.printf "@[<v2>lxy_px: %a@ type: %a@]@." Term.pp_debug lxy_px Term.pp_debug
-    (Term.ty_exn lxy_px)
+  Fmt.printf "@[<v2>lxy_px: %a@ type: %a@ type of type: %a@]@." Term.pp_debug
+    lxy_px Term.pp_debug (Term.ty lxy_px) Term.pp_debug
+    (Term.ty @@ Term.ty lxy_px)
 
 let () =
   let t = Term.app_l store lxy_px [ a; b ] in
   Fmt.printf "@[<v2>lxy_px a b: %a@ type: %a@]@." Term.pp_debug t Term.pp_debug
-    (Term.ty_exn t)
+    (Term.ty t)
+
+(* *)
+
+let tau = Term.const store @@ Str_const.make "tau" ~ty:type_
+
+let f_eq =
+  let vAlpha = Var.make "Alpha" type_ in
+  let tAlpha = Term.var store vAlpha in
+  Term.const store
+  @@ Str_const.make "="
+       ~ty:Term.(pi store vAlpha @@ arrow_l store [ tAlpha; tAlpha ] bool)
+
+let () =
+  Fmt.printf "@[<v2>(=): %a@ type: %a@]@." Term.pp_debug f_eq Term.pp_debug
+    (Term.ty f_eq)
+
+let app_eq store x y = Term.app_l store f_eq [ Term.ty x; x; y ]
+
+let p2 =
+  Term.const store
+  @@ Str_const.make "p2" ~ty:Term.(arrow_l store [ tau; tau ] bool)
+
+let () =
+  Fmt.printf "@[<v2>p2: %a@ type: %a@]@." Term.pp_debug p2 Term.pp_debug
+    (Term.ty p2)
+
+let t2 =
+  let vx = Var.make "x" tau in
+  let vy = Var.make "y" tau in
+  let tX = Term.var store vx in
+  let tY = Term.var store vy in
+  Term.(
+    let t1 = lam store vx @@ lam store vy @@ app_l store p2 [ tX; tY ]
+    and t2 = app store f_eq tau in
+    app_eq store t1 t2)
+
+let () =
+  Fmt.printf "@[<v2>t2: %a@ type: %a@]@." Term.pp_debug t2 Term.pp_debug
+    (Term.ty t2)