Commit 823cb976 authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix functional tests for apply_raw

parent b1f88f1e
......@@ -461,21 +461,20 @@ let test_apply =
let (s,t) = (parse_typ s,parse_typ t) in
let (sl,s,t,g) = Types.apply_raw s t in
let s_sigma = sigmacup sl s in
let t_sigma = sigmacup sl t in
let t_sigma_domain = (Types.Arrow.domain(Types.Arrow.get t_sigma)) in
let gamma = Types.cons (Types.var (Var.mk "Gamma")) in
let t1 = sigmacup sl s in
let t2_gamma = sigmacup sl (Types.arrow (Types.cons t) gamma) in
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "t @@ sl < 0 -> 1 = %a\n" Types.Print.print t_sigma
) (Types.subtype t_sigma (parse_typ "Empty -> Any")) true;
Format.fprintf fmt "t1 < 0 -> 1 = %a\n" Types.Print.print t1
) (Types.subtype t1 (parse_typ "Empty -> Any")) true;
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
Format.fprintf fmt "(s @@ sl) = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "(t @@ sl) = %a\n" Types.Print.print t_sigma;
Format.fprintf fmt "g = %a\n" Types.Print.print g;
Format.fprintf fmt "domain(t @@ sl) = %a\n" Types.Print.print t_sigma_domain
) (Types.subtype s_sigma t_sigma) true
Format.fprintf fmt "t1 = %a\n" Types.Print.print t1;
Format.fprintf fmt "t2 -> gamma = %a\n" Types.Print.print t2_gamma;
) (Types.subtype t1 t2_gamma) true
with Tallying.Step1Fail -> assert_equal [] []
)
) apply_raw_tests
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment