From e235a6556756d005214ab55a6d40541c39308030 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 28 Jul 2022 14:51:43 -0400 Subject: [PATCH] test: add more to unittest/core-logic --- unittest/core-logic/t1.expected | 22 ++++++------ unittest/core-logic/t1.ml | 60 +++++++++++++++++++++++++++------ 2 files changed, 62 insertions(+), 20 deletions(-) diff --git a/unittest/core-logic/t1.expected b/unittest/core-logic/t1.expected index 292f26fc..cee32dd0 100644 --- a/unittest/core-logic/t1.expected +++ b/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 diff --git a/unittest/core-logic/t1.ml b/unittest/core-logic/t1.ml index 30f09da3..4d6cec06 100644 --- a/unittest/core-logic/t1.ml +++ b/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 "@[lxy_px: %a@ type: %a@]@." Term.pp_debug lxy_px Term.pp_debug - (Term.ty_exn lxy_px) + Fmt.printf "@[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 "@[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 "@[(=): %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 "@[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 "@[t2: %a@ type: %a@]@." Term.pp_debug t2 Term.pp_debug + (Term.ty t2)