Skip to content

GitLab

Commit 7f614b4d authored by Pietro Abate's avatar Pietro Abate
Browse files

Clean up and commit all unit tests for norm

parent 066ee893
Hide whitespace changes
Inline Side-by-side
Showing with 134 additions and 78 deletions
tests/libtest/tallyingTest.ml
View file @ 7f614b4d
open OUnit
(* open Types *)
open Types
let parse_typ s =
let st = Stream.of_string s in
......@@ -9,31 +8,50 @@ let parse_typ s =
Types.descr nodepat
;;
let cup = Types.Tallying.CS.S.cup
let cap = Types.Tallying.CS.cap
let singleton = Types.Tallying.CS.singleton
let cup = Tallying.CS.cup
let cap = Tallying.CS.cap
let singleton = Tallying.CS.singleton
let mk_pos (alpha,t) = singleton (Tallying.Pos (`Var alpha,parse_typ t))
let mk_neg (t,alpha) = singleton (Tallying.Neg (parse_typ t,`Var alpha))
let norm_tests = [
"Int \\ (`$A | `$B)", singleton (false,`Var "A",parse_typ "Int \\ `$B");
"(`$A -> Int) \\ (`$B -> `$B)",
cup
(singleton (true,`Var "B",parse_typ "Empty"))
"(`$A -> Bool)", "(`$B -> `$B)",
cup (mk_pos ("B","Empty"))
(cap
(mk_neg ("`$B","A"))
(mk_neg ("Bool","B"))
);
"`$B", "`$A", mk_neg ("`$B","A");
"`$B", "Empty", mk_pos ("B","Empty");
"Int", "`$B", mk_neg ("Int","B");
"Int", "(`$A | `$B)", mk_neg ("Int \\ `$B","A");
"(Int -> Bool)", "(`$A -> `$B)",
cup (mk_pos ("A","Empty"))
(cap
(singleton (false , `Var "B",parse_typ "`$A"))
(singleton (false , `Var "B",parse_typ "Int"))
(mk_pos ("A","Int"))
(mk_neg ("Bool","B"))
);
"`$B", singleton (true,`Var "B",parse_typ "Empty");
"`$B \\ `$A", singleton (false , `Var "B",parse_typ "`$A");
"Int \\ `$B", singleton (false , `Var "B",parse_typ "Int");
"(Int & Bool -> Int) \\ (`$A -> `$B)"
]
let m_compare = Tallying.CS.M.compare Types.compare
module ECS = OUnitDiff.ListSimpleMake (struct
type t = Tallying.CS.m
let compare = m_compare
let pp_printer = Tallying.CS.print_m
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
let test_norm =
"test tallying norm" >:::
List.map (fun (t,expected) ->
(Printf.sprintf " %s " t) >:: (fun _ ->
let ll = Types.Tallying.norm (parse_typ t) in
assert_equal ll expected
List.map (fun (s,t,expected) ->
(Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
let s = parse_typ s in
let t = parse_typ t in
let result = Tallying.norm (diff s t) in
let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
ECS.assert_equal (elem expected) (elem result)
)
) norm_tests
;;
......
tests/libtest/typesTest.ml
View file @ 7f614b4d
......@@ -15,6 +15,26 @@ let t2 = Types.descr (Typer.typ Builtin.env (Parser.pat (Stream.of_string "Any")
Types.subtype t1 t2 ;;
*)
let set_op_tests = [
"Int & `$B", "`$B & Int";
"Int | `$B", "`$B | Int";
"(Int | Bool) & `$A", "(Int & `$A) | (Bool & `$A)";
"Int & Bool", "Empty";
"`$A & `$B", "`$A & `$B"
]
let test_set_operations =
"test set operations" >:::
List.map (fun (s1,s2) ->
(Printf.sprintf " %s <: %s " s1 s2) >:: (fun _ ->
let t1 = parse_typ s1 in
let t2 = parse_typ s2 in
assert_equal ~cmp:Types.equal (* ~printer:(fun t -> Format.sprintf "%a" Types.Print.print t) *) t1 t2
)
) set_op_tests
;;
let subtype_tests = [
"Int" , "Any", true;
"`A | Int" , "`A", false;
......@@ -149,8 +169,9 @@ let test_witness =
let all =
"all tests" >::: [
test_set_operations;
test_subtype;
test_witness;
(* test_witness; *)
]
let main () =
......
types/types.ml
View file @ 7f614b4d
......@@ -114,7 +114,7 @@ struct
let print = function
| Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
| Cofinite l ->
| Cofinite l ->
[ fun ppf ->
Format.fprintf ppf "@[Abstract";
List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
......@@ -196,13 +196,16 @@ struct
List.iter (fun f -> f ppf; Format.fprintf ppf " |")
let dump ppf d =
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) record(%a) xml(%a)>"
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>"
BoolAtoms.dump d.atoms
BoolIntervals.dump d.ints
BoolChars.dump d.chars
BoolPair.dump d.times
BoolPair.dump d.arrow
BoolRec.dump d.record
BoolPair.dump d.xml
Abstract.dump d.abstract
d.absent
let empty = {
times = BoolPair.empty;
......@@ -217,6 +220,17 @@ struct
toplvars = { s = Var.Set.empty ; b = true }
}
let check a =
BoolChars.check a.chars;
BoolIntervals.check a.ints;
BoolAtoms.check a.atoms;
BoolPair.check a.times;
BoolPair.check a.xml;
BoolPair.check a.arrow;
BoolRec.check a.record;
Abstract.check a.abstract;
()
let equal a b =
(a == b) || (
(BoolAtoms.equal a.atoms b.atoms) &&
......@@ -256,17 +270,6 @@ struct
let accu = if a.absent then accu+5 else accu in
accu
let check a =
BoolChars.check a.chars;
BoolIntervals.check a.ints;
BoolAtoms.check a.atoms;
BoolPair.check a.times;
BoolPair.check a.xml;
BoolPair.check a.arrow;
BoolRec.check a.record;
Abstract.check a.abstract;
()
end
and Node :
sig
......@@ -367,7 +370,7 @@ let var a = {
ints = BoolIntervals.vars a;
atoms = BoolAtoms.vars a;
chars = BoolChars.vars a;
abstract = Abstract.any;
abstract = Abstract.empty;
absent= false;
toplvars = { s = Var.Set.singleton a; b = true }
}
......@@ -1113,7 +1116,6 @@ struct
(t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
don't call normal_aux *)
let get ?(kind=`Normal) d =
match kind with
| `Normal -> get_aux any d.times
......@@ -1546,7 +1548,7 @@ struct
let d = lookup d in
try DescrHash.find memo d
with Not_found ->
try
try
let n = DescrMap.find d !named in
let s = alloc [] in
s.state <- `GlobalName n;
......@@ -2250,10 +2252,11 @@ let cond_partition univ qs =
module Tallying = struct
exception UnSatConstr
type constr = (bool * Var.var * s)
type constr =
|Pos of (Var.var * s) (** alpha <= t | alpha \in P *)
|Neg of (s * Var.var) (** t <= alpha | alpha \in N *)
module CS = struct
......@@ -2272,15 +2275,18 @@ module Tallying = struct
module M = struct
include Map.Make(struct
type t = (bool * Var.var)
let compare = Pervasives.compare
let compare (b1,v1) (b2,v2) =
if b1 == b2 then
Var.compare v1 v2
else Pervasives.compare b1 b2
end)
let print ppf m =
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s,%a)" v Print.print s
Format.fprintf ppf "(`$%s,%a)" v dump s
else
Format.fprintf ppf "(%a,`$%s)" Print.print s v
Format.fprintf ppf "(%a,`$%s)" dump s v
) ppf (bindings m);
end
......@@ -2289,7 +2295,7 @@ module Tallying = struct
module E = struct
include Map.Make(struct
type t = Var.var
let compare = Pervasives.compare
let compare = Var.compare
end)
let print ppf e =
......@@ -2314,8 +2320,9 @@ module Tallying = struct
type m = Descr.s M.t
type e = Descr.s E.t
let singleton (b,v,s) =
S.singleton (M.singleton (b,v) s)
let singleton = function
|Pos (v,s) -> S.singleton (M.singleton (true,v) s)
|Neg (s,v) -> S.singleton (M.singleton (false,v) s)
let print = S.print
let print_m = M.print
......@@ -2347,12 +2354,11 @@ module Tallying = struct
end
(* Correct ??? *)
let normatoms (t,_) = if Atoms.is_empty t then CS.sat else raise UnSatConstr
let normchars (t,_) = if Chars.is_empty t then CS.sat else raise UnSatConstr
let normints (t,_) = if Intervals.is_empty t then CS.sat else raise UnSatConstr
let single_aux constr (b,v,p,n) =
let single_aux constr (b,v,p,n) =
let aux f constr acc l =
List.fold_left (fun acc ->
function
......@@ -2362,7 +2368,12 @@ module Tallying = struct
in
let id = (fun x -> x) in
let t = cap (aux id constr any p) (aux neg constr any n) in
if b then neg t else t
(* XXX the abstract field could be messed up ... maybe *)
if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
let t1 = neg t in
{ t1 with abstract = Abstract.empty }
else (* t = bigdisj ... alpha \in N --> t <= alpha *)
{ t with abstract = Abstract.empty }
let single_atoms = single_aux atom
......@@ -2381,24 +2392,28 @@ module Tallying = struct
(* check if there exists a toplevel varaible : fun (pos,neg) *)
let toplevel single norm_rec mem (p,n) = match (p,n) with
|([],(`Var x)::neg) ->
CS.singleton (false,`Var x,single (false,x,p,n))
let t = single (false,x,[],neg) in
CS.singleton (Neg (t,`Var x))
|((`Var x)::pos,[]) ->
CS.singleton (true ,`Var x,single (true,x,pos,[]))
let t = single (true,x,pos,[]) in
CS.singleton (Pos (`Var x,t))
|((`Var x)::pos, (`Var y)::neg) ->
(* XXX this compare must be changed *)
if Pervasives.compare (`Var x) (`Var y) < 0 then
CS.singleton (true,`Var x,single (true,x,pos,n))
if Var.compare (`Var x) (`Var y) < 0 then
let t = single (true,x,pos,n) in
CS.singleton (Pos (`Var x,t))
else
CS.singleton (false, `Var y,single (false,y,p,neg))
let t = single (false,y,p,neg) in
CS.singleton (Neg (t,`Var y))
|([`Atm a], (`Var x)::neg) ->
CS.singleton (false,`Var x,single (false,x,p,neg))
let t = single (false,x,p,neg) in
CS.singleton (Neg (t,`Var x))
|((`Var x)::pos, [`Atm _]) -> failwith "impossible5"
|([`Atm t], []) -> norm_rec (t,mem)
|([],[`Atm t]) -> failwith "impossible0" (* norm_rec (t,mem) *)
|((`Var x)::pos, [`Atm _]) -> failwith "impossible5"
|([],[]) -> failwith "impossible"
|([],_) -> failwith "impossible2"
|(_,[]) -> failwith "impossible3"
......@@ -2406,22 +2421,20 @@ module Tallying = struct
let rec norm ( (t,m) : (s * DescrSet.t)) =
if DescrSet.mem t m then CS.sat else begin
(* try *)
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
CS.cap acc (toplevel single norm_aux m (pos,neg))
) acc l
in
let accu = CS.sat in
let accu = aux_base single_atoms normatoms accu (BoolAtoms.get t.atoms) in
let accu = aux_base single_chars normchars accu (BoolChars.get t.chars) in
let accu = aux_base single_ints normints accu (BoolIntervals.get t.ints) in
let accu = aux_base single_times normpair accu (BoolPair.get t.times) in
let accu = aux_base single_xml normpair accu (BoolPair.get t.xml) in
let accu = aux_base single_record normrec accu (BoolRec.get t.record) in
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
accu
(* with UnSatConstr -> CS.unsat *)
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
CS.cap acc (toplevel single norm_aux m (pos,neg))
) acc l
in
let accu = CS.sat in
let accu = aux_base single_atoms normatoms accu (BoolAtoms.get t.atoms) in
let accu = aux_base single_chars normchars accu (BoolChars.get t.chars) in
let accu = aux_base single_ints normints accu (BoolIntervals.get t.ints) in
let accu = aux_base single_times normpair accu (BoolPair.get t.times) in
let accu = aux_base single_xml normpair accu (BoolPair.get t.xml) in
let accu = aux_base single_record normrec accu (BoolRec.get t.record) in
let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
accu
end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
......@@ -2434,7 +2447,6 @@ module Tallying = struct
* [t2\s2] ^ prod'(t1,t2\s2,n)
* *)
and normpair ( (t,mem) : (BoolPair.s * DescrSet.t) ) =
(* this should be called with xml !!! *)
let mem = DescrSet.add { empty with times = BoolPair.atom (`Atm t) } mem in
let norm_prod pos neg =
let rec aux (t1 : s) (t2 : s ) = function
......
types/types.mli
View file @ 7f614b4d
......@@ -127,7 +127,7 @@ val times : Node.t -> Node.t -> t
val xml : Node.t -> Node.t -> t
val arrow : Node.t -> Node.t -> t
val record : label -> Node.t -> t
(* bool = true -> open record; bool = false -> closed record *)
(** bool = true -> open record; bool = false -> closed record *)
val record_fields : bool * Node.t label_map -> t
val char : Chars.t -> t
val constant : const -> t
......@@ -350,7 +350,10 @@ module Cache : sig
end
module Tallying : sig
type constr = (bool * Var.var * t)
type constr =
|Pos of (Var.var * t) (** alpha <= t | alpha \in P *)
|Neg of (t * Var.var) (** t <= alpha | alpha \in N *)
module CS : sig
module M : sig
......
types/var.ml
View file @ 7f614b4d
......@@ -3,20 +3,22 @@ type t = String.t
type var = [ `Var of t ]
type 'a pairvar = [ `Atm of 'a | var ]
let compare (x : var) (y : var) = Pervasives.compare x y
let hash (v : var) = Hashtbl.hash v
module Make (X : Custom.T) = struct
type t = X.t pairvar
let hash = function `Atm t -> X.hash t | `Var s -> Hashtbl.hash (`Var s)
let hash = function `Atm t -> X.hash t | `Var s -> hash (`Var s)
let check = function `Atm t -> X.check t | `Var _ -> ()
let compare t1 t2 =
match t1,t2 with
|`Var x, `Var y -> compare (`Var x) (`Var y)
|`Atm x, `Atm y -> X.compare x y
|`Var x, `Var y when x = y -> 0
(* HACK fix BoolVar.get to get variables in the correct order *)
|`Var x, `Var y -> if String.compare x y = -1 then 1 else -1
|`Var _, `Atm _ -> -1
|`Atm _, `Var _ -> 1
let equal t1 t2 = (compare t1 t2) = 0
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> Format.fprintf ppf "`$%s" x
......
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