Commit c5413fb8 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

* Simplify the representation of sets of constraints and sets of sets of constraints.

* More agressive simplifications of unused variables, and variable beautification of remaining variable (i.e.
rename _fresh_xxx, _fresh_yyy into $A, $B, ...
parent 32448f02
......@@ -3,7 +3,7 @@ open Types
let parse_typ ?(variance=`Covariant) s =
let st = Stream.of_string s in
let astpat = Parser.pat st in
let astpat = Parser.pat st in
let nodepat = Typer.typ ~variance Builtin.env astpat in
Types.descr nodepat
;;
......@@ -14,9 +14,9 @@ let to_string pp t =
;;
(* the abstract field is ignored in the comparison *)
module ESet = OUnitDiff.SetMake (struct
module ESet = OUnitDiff.SetMake (struct
type t = (Var.var * Types.t)
let compare (v1,t1) (v2,t2) =
let compare (v1,t1) (v2,t2) =
let a = Types.abstract Abstract.any in
if (v1,t1) == (v2,t2) then 0
else let c = Var.compare v1 v2 in if c <> 0 then c
......@@ -25,20 +25,20 @@ module ESet = OUnitDiff.SetMake (struct
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
module SubStSet = OUnitDiff.SetMake (struct
module SubStSet = OUnitDiff.SetMake (struct
type t = ESet.t
let compare a b = ESet.compare a b
let pp_printer ppf l = ESet.pp_printer ppf l
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
module MSet = OUnitDiff.SetMake (struct
module MSet = OUnitDiff.SetMake (struct
type t = Tallying.CS.m
let compare =
let compare =
(* the abstract field is ignored in the comparison *)
let a = Types.abstract Abstract.any in
let cmp t1 t2 = Types.compare (diff t1 a) (diff t2 a) in
Tallying.CS.M.compare cmp
Tallying.CS.M.compare (*cmp *)
let pp_printer = Tallying.CS.pp_m
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
......@@ -49,8 +49,8 @@ and vv = V of string
let mk_s ll =
let aux l =
List.fold_left (fun acc -> function
|P(V alpha,t) -> Tallying.CS.M.add (true,Var.mk alpha) (parse_typ t) acc
|N(t,V alpha) -> Tallying.CS.M.add (false,Var.mk alpha) (parse_typ t) acc
|P(V alpha,t) -> Tallying.CS.M.add ((*true,*)Var.mk alpha) (Types.empty,parse_typ t) acc
|N(t,V alpha) -> Tallying.CS.M.add ((*false,*)Var.mk alpha) (parse_typ t,Types.any) acc
) Tallying.CS.M.empty l
in
List.fold_left (fun acc l ->
......@@ -66,12 +66,12 @@ let mk_union_res l1 l2 =
|((true,v),Some x,Some y) -> assert false
|((false,v),Some x,Some y) -> assert false
in
let aux l =
let aux l =
List.fold_left (fun acc -> function
|P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,Var.mk v) (parse_typ s))
|N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,Var.mk v) (parse_typ s))
|P(V v,s) -> Tallying.CS.M.merge (*aux_merge*) acc (Tallying.CS.M.singleton ((*true,*)Var.mk v) (Types.empty, parse_typ s))
|N(s,V v) -> Tallying.CS.M.merge (*aux_merge*) acc (Tallying.CS.M.singleton ((*false,*)Var.mk v) (parse_typ s, Types.any))
) Tallying.CS.M.empty l
in
in
match l1,l2 with
|[],[] -> Tallying.CS.sat
|l1,[] -> (Tallying.CS.S.singleton (aux l1))
......@@ -98,8 +98,8 @@ let test_constraint_ops () = [
"prod neg",mk_prod [N("Int",V "B");N("Bool",V "B")], mk_pp (N("Int | Bool",V "B"));
"prod var",mk_prod [N("`$B",V "A");P(V "B","Bool | Int")],
mk_union_res
[N("`$B",V "A");P(V "B","Bool | Int")]
mk_union_res
[N("`$B",V "A");P(V "B","Bool | Int")]
[];
"empty", mk_union [P(V "A","Empty")] [P(V "A","Empty")], mk_pp (P(V "A","Empty"));
......@@ -114,7 +114,7 @@ let test_constraint_ops () = [
"union 1",mk_union [P(V "A","Empty")] [P(V "A","Empty");N("Int",V "B")], mk_pp (P(V "A","Empty"));
"union 2",mk_union [P(V "A","Empty")] [P(V "A","Int");P(V "A","Bool")],
mk_union_res
mk_union_res
[P(V "A","Int & Bool")]
[P(V "A","Empty")];
......@@ -128,7 +128,7 @@ let test_constraint_ops () = [
"union 4",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Int")], mk_pp (P(V "A","Empty"));
"union 5",mk_union [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")] [P(V "A","Empty");P(V "B","Empty")],
mk_union_res
mk_union_res
[P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
[P(V "A","Empty");P(V "B","Empty")];
......@@ -216,7 +216,8 @@ let norm_tests () = [
];
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
"((`$A , Int) & (`$B , Bool))","(Int , (*Int & Bool*) Empty)",Tallying.CS.sat;
"((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
......@@ -238,7 +239,7 @@ let test_norm =
;;
let merge_tests () = [
"empty empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
"empty empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
mk_s [
[P(V "A","Empty");P(V "B","Empty")]
];
......@@ -252,7 +253,7 @@ let merge_tests () = [
[N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
];
"add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
"add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
mk_s [[N("`$B", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];
"A B", mk_s [[P(V "A", "`$B")]], mk_pp (P(V "A","`$B"));
......@@ -269,12 +270,12 @@ let test_merge =
"merge" >:::
List.map (fun (test,s,expected) ->
test >:: (fun _ ->
let result =
let result =
try
Tallying.CS.S.fold (fun c acc ->
Tallying.CS.union (Tallying.merge c) acc
) s Tallying.CS.S.empty
with Tallying.UnSatConstr -> Tallying.CS.unsat
with Tallying.UnSatConstr _ -> Tallying.CS.unsat
in
let elem s = MSet.of_list (Tallying.CS.S.elements s) in
MSet.assert_equal (elem expected) (elem result)
......@@ -317,9 +318,9 @@ let tallying_tests = [
[("Bool -> Bool","Int -> `$A")], [];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
(* map even *)
[("(`$A -> `$B) -> [`$A* ] -> [`$B* ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
[("(`$A -> `$B) -> [`$A ] -> [`$B ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
[("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e []
]
......@@ -334,11 +335,11 @@ let test_tallying =
try
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let result = Tallying.tallying l in
List.iter (fun (s,t) ->
List.iter (fun (s,t) ->
List.iter (fun sigma ->
let s_sigma = Tallying.apply_subst s sigma in
let t_sigma = Tallying.apply_subst t sigma in
assert_equal ~pp_diff:(fun fmt _ ->
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
) (Types.subtype s_sigma t_sigma) true
......@@ -360,10 +361,9 @@ let suite =
test_merge;
test_tallying;
]
let main () =
OUnit.run_test_tt_main suite
;;
main ()
main ()
This diff is collapsed.
......@@ -112,7 +112,7 @@ val any : t
val no_var : t -> bool
val is_var : t -> bool
val has_tlv : t -> bool
val has_tlv : t -> bool
val any_node : Node.t
val empty_node : Node.t
......@@ -262,7 +262,7 @@ module Arrow : sig
val check_iface: (t * t) list -> t -> bool
type t
type t = descr * (descr * descr) list list
val is_empty: t -> bool
val get: descr -> t
(* Always succeed; no check <= Arrow.any *)
......@@ -359,14 +359,22 @@ module Tallying : sig
|Pos of (Var.var * t) (** alpha <= t | alpha \in P *)
|Neg of (t * Var.var) (** t <= alpha | alpha \in N *)
exception UnSatConstr
exception UnSatConstr of string
exception Step1Fail
exception Step2Fail
module CS : sig
module M : sig
include Map.S with type key = (bool * Var.var)
val print : Format.formatter -> descr t -> unit
type key = Var.var
type t
(* include Map.S with type key = (bool * Var.var)*)
val compare : t -> t -> int
val empty : t
val add : key -> descr*descr -> t -> t
val singleton : key -> descr*descr -> t
val print : Format.formatter -> t -> unit
val merge : t -> t -> t
end
module E : sig
include Map.S with type key = Var.var
......@@ -377,12 +385,19 @@ module Tallying : sig
val print : Format.formatter -> t -> unit
end
module S : sig
include Set.S with type elt = descr M.t
type t = M.t list
val empty : t
val add : M.t -> t -> t
val singleton : M.t -> t
val union : t -> t -> t
val elements : t -> M.t list
val fold : (M.t -> 'b -> 'b) -> M.t list -> 'b -> 'b
(*include Set.S with type elt = descr M.t*)
val print : Format.formatter -> t -> unit
end
type s = S.t
type m = t M.t
type m = M.t
type e = t E.t
type es = ES.t
type sigma = (Var.var * t) list
......
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