From 435845d1d408237dfd1943a7b74a8bc319d8b1ba Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 27 Jul 2022 22:45:10 -0400
Subject: [PATCH] update tests

---
 unittest/core-ast/t1.expected |  7 +++++++
 unittest/core-ast/t1.ml       | 19 +++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/unittest/core-ast/t1.expected b/unittest/core-ast/t1.expected
index f64d188c..292f26fc 100644
--- a/unittest/core-ast/t1.expected
+++ b/unittest/core-ast/t1.expected
@@ -10,3 +10,10 @@ 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))
+  type: (Bool -> (Bool -> Bool))
+lxy_px a b: ((\x:Bool. (\y:Bool. p x))) a b
+  type: Bool
diff --git a/unittest/core-ast/t1.ml b/unittest/core-ast/t1.ml
index 04872627..0afd0d19 100644
--- a/unittest/core-ast/t1.ml
+++ b/unittest/core-ast/t1.ml
@@ -35,5 +35,24 @@ let () = Fmt.printf "p(b): %a@." pp_debug pb
 let () = Fmt.printf "q(a): %a@." pp_debug qa
 let () = Fmt.printf "q(b): %a@." pp_debug qb
 let () = assert (equal pa (app store p a))
+
+(* *)
+
 let ty_pa = ty_exn pa
 let () = Fmt.printf "typeof(p a): %a@." pp_debug ty_pa
+
+(* *)
+
+let v_x = Var.make "x" bool
+let v_y = Var.make "y" bool
+let x = var store v_x
+let y = var store v_y
+let lxy_px = lam store v_x @@ lam store v_y @@ app store p x
+
+let () =
+  Fmt.printf "@[<v2>lxy_px: %a@ type: %a@]@." pp_debug lxy_px pp_debug
+    (ty_exn lxy_px)
+
+let () =
+  let t = app_l store lxy_px [ a; b ] in
+  Fmt.printf "@[<v2>lxy_px a b: %a@ type: %a@]@." pp_debug t pp_debug (ty_exn t)