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

update tests

Browse source
This commit is contained in:
Simon Cruanes 2022-07-27 22:45:10 -04:00
parent 88eb2575c3
commit 435845d1d4
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
unittest/core-ast/t1.expected
View file

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

19
unittest/core-ast/t1.ml
View file

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