Commit 410fcd0c by Pietro Abate

### Implementation of the Tallying problem

- revert a few chances I did before in the code
- add new unit tests functions for the Tallying problem
parent d3591e7e
 ... @@ -180,7 +180,9 @@ module Var (X : T) = struct ... @@ -180,7 +180,9 @@ module Var (X : T) = struct let compare t1 t2 = let compare t1 t2 = match t1,t2 with match t1,t2 with |Atm x, Atm y -> X.compare x y |Atm x, Atm y -> X.compare x y |Var x, Var y -> String.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 |Var _, Atm _ -> -1 |Atm _, Var _ -> 1 |Atm _, Var _ -> 1 ... ...
 ... @@ -3,9 +3,10 @@ open Ocamlbuild_plugin;; ... @@ -3,9 +3,10 @@ open Ocamlbuild_plugin;; Options.use_ocamlfind := true ;; Options.use_ocamlfind := true ;; open Command ;; open Command ;; (* let _ = dispatch begin function let _ = dispatch begin function | After_rules -> | After_rules -> ocaml_lib ~extern:true ~dir:"_build" "typesOUnit" ocaml_lib ~extern:true ~dir:"_build" "typesOUnit" | _ -> () | _ -> () end;; end;; *)
 ... @@ -40,12 +40,12 @@ and toplevel_directive = ... @@ -40,12 +40,12 @@ and toplevel_directive = | Builtins | Builtins ] ] and pexpr = and pexpr = | LocatedExpr of loc * pexpr | LocatedExpr of loc * pexpr (* CDuce is a Lambda-calculus ... *) (* CDuce is a Lambda-calculus ... *) | Var of U.t | Var of U.t (* this TVar must be moved to patt *) | TVar of BoolVar.Vars.V.t | TVar of BoolVar.Vars.V.t | Apply of pexpr * pexpr | Apply of pexpr * pexpr | Abstraction of abstr | Abstraction of abstr ... @@ -80,7 +80,6 @@ and pexpr = ... @@ -80,7 +80,6 @@ and pexpr = | Check of pexpr * ppat | Check of pexpr * ppat | Ref of pexpr * ppat | Ref of pexpr * ppat (* CQL *) (* CQL *) | SelectFW of pexpr * (ppat * pexpr) list * pexpr list | SelectFW of pexpr * (ppat * pexpr) list * pexpr list ... @@ -90,6 +89,14 @@ and abstr = { ... @@ -90,6 +89,14 @@ and abstr = { fun_name : (Cduce_loc.loc * U.t) option; fun_name : (Cduce_loc.loc * U.t) option; fun_iface : (ppat * ppat) list; fun_iface : (ppat * ppat) list; fun_body : branches fun_body : branches (* add deco : (sigma) symbolic representation of set type substitutions *) (* plus a flag that is true if interesection of the free varbialbes of S that are not intruduced * by the lambda astractions are domain of sigma. * if oldvar(S) ^ dom(sigma) = empty then s < t else s[eval(sigma, env)] < t * (biginter_{sigma_i \in eval} s (sigma_i) ) < t * * see Evaluation, section 5.3 Article part 1 * *) } } and branches = (ppat * pexpr) list and branches = (ppat * pexpr) list ... ...
 ... @@ -62,7 +62,7 @@ let tuple_queue = ... @@ -62,7 +62,7 @@ let tuple_queue = List.fold_right (fun x q -> Pair (x, q)) List.fold_right (fun x q -> Pair (x, q)) let char = mknoloc (Internal (Types.char (Types.BoolChars.atom (Atm Chars.any)))) let char = mknoloc (Internal (Types.char Chars.any)) let string_regexp = Star (Elem char) let string_regexp = Star (Elem char) let seq_of_string s = let seq_of_string s = ... @@ -298,7 +298,7 @@ EXTEND Gram ... @@ -298,7 +298,7 @@ EXTEND Gram | e1 = expr; "&&"; e2 = expr -> exp _loc (logical_and e1 e2) | e1 = expr; "&&"; e2 = expr -> exp _loc (logical_and e1 e2) | e = expr; op = "/"; p = pat LEVEL "simple" -> | e = expr; op = "/"; p = pat LEVEL "simple" -> (* transform e with <(Atom)>[($$::t|_)*] -> [$$$] *) (* transform e with <(Atom)>[($$::t|_)*] -> [$$$] *) let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Atm (Atoms.any))))) in let tag = mk _loc (Internal (Types.atom Atoms.any)) in let att = mk _loc (Internal Types.Record.any) in let att = mk _loc (Internal Types.Record.any) in let any = mk _loc (Internal Types.any) in let any = mk _loc (Internal Types.any) in let re = Star(Alt(SeqCapture(noloc,id_dummy,Elem p), Elem any)) in let re = Star(Alt(SeqCapture(noloc,id_dummy,Elem p), Elem any)) in ... @@ -307,7 +307,7 @@ EXTEND Gram ... @@ -307,7 +307,7 @@ EXTEND Gram exp _loc (Transform (e,[p, Var id_dummy])) exp _loc (Transform (e,[p, Var id_dummy])) | e = expr; "/@"; a = ident_or_keyword -> | e = expr; "/@"; a = ident_or_keyword -> (* transform e with <(Atom) {a=$$}>_ -> [$$$] *) (* transform e with <(Atom) {a=$$}>_ -> [$$$] *) let tag = mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Atm (Atoms.any))))) in let tag = mk _loc (Internal (Types.atom Atoms.any)) in let any = mk _loc (Internal Types.any) in let any = mk _loc (Internal Types.any) in let att = mk _loc (Record let att = mk _loc (Record (true, [(label a, (true, [(label a, ... @@ -330,7 +330,7 @@ EXTEND Gram ... @@ -330,7 +330,7 @@ EXTEND Gram set_ref set_ref (Var stk) (Var stk) (concat (get_ref (Var stk)) (Pair (Var id_dummy,cst_nil))) in (concat (get_ref (Var stk)) (Pair (Var id_dummy,cst_nil))) in let tag = mknoloc (Internal (Types.atom (Types.BoolAtoms.atom (Atm (Atoms.any))))) in let tag = mknoloc (Internal (Types.atom Atoms.any)) in let att = mknoloc (Internal Types.Record.any) in let att = mknoloc (Internal Types.Record.any) in let any = mknoloc (Internal Types.any) in let any = mknoloc (Internal Types.any) in let re = (SeqCapture(noloc,y,Star(Elem(any)))) in let re = (SeqCapture(noloc,y,Star(Elem(any)))) in ... @@ -403,7 +403,7 @@ EXTEND Gram ... @@ -403,7 +403,7 @@ EXTEND Gram tag: [ [ a = ident_or_keyword -> exp _loc (Atom (ident a)) ] ]; tag: [ [ a = ident_or_keyword -> exp _loc (Atom (ident a)) ] ]; tag_type: [ tag_type: [ [ "_" -> mk _loc (Internal (Types.atom (Types.BoolAtoms.atom (Atm (Atoms.any))))) [ "_" -> mk _loc (Internal (Types.atom Atoms.any)) | "$"; a = ident_or_keyword -> mk _loc (Cst (TVar a)) | "$"; a = ident_or_keyword -> mk _loc (Cst (TVar a)) | a = ident_or_keyword -> mk _loc (Cst (Atom (ident a))) | a = ident_or_keyword -> mk _loc (Cst (Atom (ident a))) | t = ANY_IN_NS -> mk _loc (NsT (ident t)) | t = ANY_IN_NS -> mk _loc (NsT (ident t)) ... @@ -569,13 +569,13 @@ EXTEND Gram ... @@ -569,13 +569,13 @@ EXTEND Gram | i = STRING1; "--"; j = STRING1 -> | i = STRING1; "--"; j = STRING1 -> let i = Chars.V.mk_int (parse_char _loc i) let i = Chars.V.mk_int (parse_char _loc i) and j = Chars.V.mk_int (parse_char _loc j) in and j = Chars.V.mk_int (parse_char _loc j) in Elem (mk _loc (Internal (Types.char (Types.BoolChars.atom (Atm (Chars.char_class i j)))))) Elem (mk _loc (Internal (Types.char (Chars.char_class i j)))) | s = STRING1 -> | s = STRING1 -> List.fold_right List.fold_right (fun c accu -> (fun c accu -> let c = Chars.V.mk_int c in let c = Chars.V.mk_int c in let c = Chars.atom c in let c = Chars.atom c in Seq (Elem (mknoloc (Internal (Types.char (Types.BoolChars.atom (Atm c))))), accu)) Seq (Elem (mknoloc (Internal (Types.char c))), accu)) (seq_of_string s) (seq_of_string s) Epsilon ] Epsilon ] | [ e = pat LEVEL "simple" -> Elem e | [ e = pat LEVEL "simple" -> Elem e ... @@ -619,20 +619,20 @@ EXTEND Gram ... @@ -619,20 +619,20 @@ EXTEND Gram | i = INT ; "--"; j = INT -> | i = INT ; "--"; j = INT -> let i = Intervals.V.mk i let i = Intervals.V.mk i and j = Intervals.V.mk j in and j = Intervals.V.mk j in mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Atm (Intervals.bounded i j))))) mk _loc (Internal (Types.interval (Intervals.bounded i j))) | i = INT -> | i = INT -> let i = Intervals.V.mk i in let i = Intervals.V.mk i in mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Atm (Intervals.atom i))))) mk _loc (Internal (Types.interval (Intervals.atom i))) | "*"; "--"; j = INT -> | "*"; "--"; j = INT -> let j = Intervals.V.mk j in let j = Intervals.V.mk j in mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Atm (Intervals.left j))))) mk _loc (Internal (Types.interval (Intervals.left j))) | i = INT; "--"; "*" -> | i = INT; "--"; "*" -> let i = Intervals.V.mk i in let i = Intervals.V.mk i in mk _loc (Internal (Types.interval (Types.BoolIntervals.atom (Atm (Intervals.right i))))) mk _loc (Internal (Types.interval (Intervals.right i))) | i = char -> | i = char -> mk _loc (Internal (Types.char (Types.BoolChars.atom (Atm (Chars.char_class i i))))) mk _loc (Internal (Types.char (Chars.char_class i i))) | i = char ; "--"; j = char -> | i = char ; "--"; j = char -> mk _loc (Internal (Types.char (Types.BoolChars.atom (Atm (Chars.char_class i j))))) mk _loc (Internal (Types.char (Chars.char_class i j))) | ""; c = tag_type -> c | ""; c = tag_type -> c | "("; l = LIST1 pat SEP ","; ")" -> multi_prod _loc l | "("; l = LIST1 pat SEP ","; ")" -> multi_prod _loc l | "["; r = [ r = regexp -> r | -> Epsilon ]; | "["; r = [ r = regexp -> r | -> Epsilon ]; ... @@ -657,9 +657,8 @@ EXTEND Gram ... @@ -657,9 +657,8 @@ EXTEND Gram (fun c -> (fun c -> mknoloc (Internal mknoloc (Internal (Types.char (Types.char (Types.BoolChars.atom (Atm ( (Chars.atom (Chars.atom (Chars.V.mk_int c)))))))) (Chars.V.mk_int c))))) (seq_of_string s) in (seq_of_string s) in let s = s @ [mknoloc (Internal (Sequence.nil_type))] in let s = s @ [mknoloc (Internal (Sequence.nil_type))] in multi_prod _loc s multi_prod _loc s ... ...
 ... @@ -480,7 +480,7 @@ let int_type (name,min,max) = ... @@ -480,7 +480,7 @@ let int_type (name,min,max) = | None, None -> | None, None -> Intervals.any Intervals.any in in ignore (primitive name (Types.interval (Types.BoolIntervals.atom (Atm ival))) (validate_interval ival name)) ignore (primitive name (Types.interval ival) (validate_interval ival name)) let () = let () = List.iter int_type [ List.iter int_type [ ... ...
 ... @@ -192,7 +192,7 @@ let simple_union name members = ... @@ -192,7 +192,7 @@ let simple_union name members = let xsi_nil_atom = Atoms.V.mk (Schema_xml.xsi, Utf8.mk "nil") let xsi_nil_atom = Atoms.V.mk (Schema_xml.xsi, Utf8.mk "nil") let xsi_nil_type = Types.atom (Types.BoolAtoms.atom (Atm (Atoms.atom xsi_nil_atom))) let xsi_nil_type = Types.atom (Atoms.atom xsi_nil_atom) let xsi_nil_label = Ns.Label.mk (Schema_xml.xsi, Utf8.mk "nil") let xsi_nil_label = Ns.Label.mk (Schema_xml.xsi, Utf8.mk "nil") let merge_attribute_uses l = let merge_attribute_uses l = ... ...
 open OUnit (* open Types *) let parse_typ s = let st = Stream.of_string s in let astpat = Parser.pat st in let nodepat = Typer.typ Builtin.env astpat in Types.descr nodepat ;; let norm_tests = [ "Int \\ ($A | $B)", [[(false,Var "A",parse_typ "Int \\ \$B")]]; ] 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 ) ) norm_tests ;; let all = "all tests" >::: [ test_norm; ] let main () = OUnit.run_test_tt_main all ;; main ()
 ... @@ -42,6 +42,8 @@ sig ... @@ -42,6 +42,8 @@ sig val cap : t -> t -> t val cap : t -> t -> t val diff : t -> t -> t val diff : t -> t -> t val atom : elem -> t val atom : elem -> t (* vars a : return a bdd that is ( Any ^ Var a ) *) val vars : Custom.var -> t val vars : Custom.var -> t val iter: (elem-> unit) -> t -> unit val iter: (elem-> unit) -> t -> unit ... @@ -196,7 +198,7 @@ struct ... @@ -196,7 +198,7 @@ struct * of positive and negative elements on a branch *) * of positive and negative elements on a branch *) let get x = let get x = let rec aux accu pos neg = function let rec aux accu pos neg = function | True -> (pos,neg) :: accu | True -> (List.rev pos, List.rev neg) :: accu | False -> accu | False -> accu | Split (_,x, p,i,n) -> | Split (_,x, p,i,n) -> (*OPT: can avoid creating this list cell when pos or neg =False *) (*OPT: can avoid creating this list cell when pos or neg =False *) ... ...
 ... @@ -13,7 +13,7 @@ let types = ... @@ -13,7 +13,7 @@ let types = "Empty", Types.empty; "Empty", Types.empty; "Any", any; "Any", any; "Int", int; "Int", int; "Char", Types.char (Types.BoolChars.atom (Atm ( Chars.any ))); "Char", Types.char Chars.any; "Byte", char_latin1; "Byte", char_latin1; "Atom", atom; "Atom", atom; "Pair", Types.Product.any; "Pair", Types.Product.any; ... @@ -167,7 +167,7 @@ binary_op_cst ">" ... @@ -167,7 +167,7 @@ binary_op_cst ">" (* I/O *) (* I/O *) register_fun "char_of_int" register_fun "char_of_int" int (Types.char (Types.BoolChars.atom (Atm ( Chars.any ) ))) int (Types.char Chars.any) (function (function | Value.Integer x -> | Value.Integer x -> (try Value.Char (Chars.V.mk_int (Intervals.V.get_int x)) (try Value.Char (Chars.V.mk_int (Intervals.V.get_int x)) ... @@ -175,7 +175,7 @@ register_fun "char_of_int" ... @@ -175,7 +175,7 @@ register_fun "char_of_int" | _ -> assert false);; | _ -> assert false);; register_fun "int_of_char" register_fun "int_of_char" (Types.char (Types.BoolChars.atom (Atm ( Chars.any) ))) int (Types.char Chars.any) int (function (function | Value.Char x -> | Value.Char x -> Value.Integer (Intervals.V.from_int (Chars.V.to_int x)) Value.Integer (Intervals.V.from_int (Chars.V.to_int x)) ... @@ -342,7 +342,7 @@ binary_op_cst "dump_to_file_utf8" ... @@ -342,7 +342,7 @@ binary_op_cst "dump_to_file_utf8" let intop f x y = let intop f x y = let s = Types.BoolIntervals.leafconj x in let s = Types.BoolIntervals.leafconj x in let t = Types.BoolIntervals.leafconj y in let t = Types.BoolIntervals.leafconj y in Types.BoolIntervals.atom (Atm (f s t)) (f s t) ;; ;; binary_op_gen "+" binary_op_gen "+" ... ...
 open Encodings open Encodings let pos_int = Types.interval (Types.BoolIntervals.atom (Atm (Intervals.right (Intervals.V.mk "1")))) let pos_int = Types.interval (Intervals.right (Intervals.V.mk "1")) let non_neg_int = Types.interval (Types.BoolIntervals.atom (Atm(Intervals.right (Intervals.V.mk "0")))) let non_neg_int = Types.interval (Intervals.right (Intervals.V.mk "0")) let neg_int = Types.interval (Types.BoolIntervals.atom (Atm(Intervals.left (Intervals.V.mk "-1")))) let neg_int = Types.interval (Intervals.left (Intervals.V.mk "-1")) let non_pos_int = Types.interval (Types.BoolIntervals.atom (Atm(Intervals.left (Intervals.V.mk "0")))) let non_pos_int = Types.interval (Intervals.left (Intervals.V.mk "0")) let mk_interval_type l r = let mk_interval_type l r = Types.interval (Types.BoolIntervals.atom (Atm(Intervals.bounded (Intervals.V.mk l) (Intervals.V.mk r)))) Types.interval (Intervals.bounded (Intervals.V.mk l) (Intervals.V.mk r)) let long_int = mk_interval_type "-9223372036854775808" "9223372036854775807" let long_int = mk_interval_type "-9223372036854775808" "9223372036854775807" let int_int = mk_interval_type "-2147483648" "2147483647" let int_int = mk_interval_type "-2147483648" "2147483647" let short_int = mk_interval_type "-32768" "32767" let short_int = mk_interval_type "-32768" "32767" ... @@ -17,58 +17,58 @@ let byte_int = mk_interval_type "0" "255" ... @@ -17,58 +17,58 @@ let byte_int = mk_interval_type "0" "255" let non_zero_int = Types.cup pos_int neg_int let non_zero_int = Types.cup pos_int neg_int let decimal_intstr = let decimal_intstr = Sequence.plus (Types.char (Types.BoolChars.atom (Atm (Chars.char_class Sequence.plus (Types.char (Chars.char_class (Chars.V.mk_char '0') (Chars.V.mk_char '0') (Chars.V.mk_char '9') (Chars.V.mk_char '9') ) ) ))) ) let octal_intstr = let octal_intstr = Sequence.plus (Types.char (Types.BoolChars.atom (Atm (Chars.char_class Sequence.plus (Types.char (Chars.char_class (Chars.V.mk_char '0') (Chars.V.mk_char '0') (Chars.V.mk_char '7') (Chars.V.mk_char '7') ) ) ))) ) let binary_intstr = let binary_intstr = Sequence.plus (Types.char (Types.BoolChars.atom (Atm (Chars.char_class Sequence.plus (Types.char (Chars.char_class (Chars.V.mk_char '0') (Chars.V.mk_char '0') (Chars.V.mk_char '1') (Chars.V.mk_char '1') ) ) ))) ) let hex_intstr = let hex_intstr = Sequence.plus ( Sequence.plus ( Types.cup Types.cup (Types.char (Types.BoolChars.atom (Atm (Chars.char_class (Types.char (Chars.char_class (Chars.V.mk_char '0') (Chars.V.mk_char '0') (Chars.V.mk_char '9') (Chars.V.mk_char '9') ) ) ))) ) (Types.cup (Types.cup (Types.char (Types.BoolChars.atom (Atm (Chars.char_class (Types.char (Chars.char_class (Chars.V.mk_char 'a') (Chars.V.mk_char 'a') (Chars.V.mk_char 'f') (Chars.V.mk_char 'f') ) ) ))) ) (Types.char (Types.BoolChars.atom (Atm (Chars.char_class (Types.char (Chars.char_class (Chars.V.mk_char 'A') (Chars.V.mk_char 'A') (Chars.V.mk_char 'F') (Chars.V.mk_char 'F') ) ) ))) ) ) ) ) ) let hex_str = let hex_str = Types.times Types.times (Types.cons (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char '0')))))) (Types.cons (Types.char (Chars.atom (Chars.V.mk_char '0')))) (Types.cons( (Types.cons( Types.times Types.times (Types.cons( (Types.cons( Types.cup Types.cup (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char 'X'))))) (Types.char (Chars.atom (Chars.V.mk_char 'X'))) (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char 'x'))))) (Types.char (Chars.atom (Chars.V.mk_char 'x'))) ) ) ) ) (Types.cons hex_intstr) (Types.cons hex_intstr) ... @@ -77,13 +77,13 @@ let hex_str = ... @@ -77,13 +77,13 @@ let hex_str = let oct_str = let oct_str = Types.times Types.times (Types.cons (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char '0')))))) (Types.cons (Types.char (Chars.atom (Chars.V.mk_char '0')))) (Types.cons( (Types.cons( Types.times Types.times (Types.cons( (Types.cons( Types.cup Types.cup (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char 'O'))))) (Types.char (Chars.atom (Chars.V.mk_char 'O'))) (Types.char (Types.BoolChars.atom (Atm(Chars.atom (Chars.V.mk_char 'o'))))) (Types.char (Chars.atom (Chars.V.mk_char 'o'))) ) ) ) ) (Types.cons octal_intstr) (Types.cons octal_intstr) ... @@ -93,13 +93,13 @@ let oct_str = ... @@ -93,13 +93,13 @@ let oct_str = let bin_str = let bin_str = Types.times Types.times (Types.cons (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char '0')))))) (Types.cons (Types.char (Chars.atom (Chars.V.mk_char '0')))) (Types.cons( (Types.cons( Types.times Types.times (Types.cons( (Types.cons( Types.cup Types.cup (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char 'B'))))) (Types.char (Chars.atom (Chars.V.mk_char 'B'))) (Types.char (Types.BoolChars.atom (Atm (Chars.atom (Chars.V.mk_char 'b'))))) (Types.char (Chars.atom (Chars.V.mk_char 'b'))) ) ) ) ) (Types.cons binary_intstr) (Types.cons binary_intstr) ... @@ -111,7 +111,7 @@ let pos_intstr = ... @@ -111,7 +111,7 @@ let pos_intstr = let neg_intstr = let neg_intstr = Types.times Types.times (Types.cons (Types.char (Types.BoolChars.atom (`Atm (Chars.atom (Chars.V.mk_char '-')))))) (Types.cons (Types.char (Chars.atom (Chars.V.mk_char '-')))) (Types.cons pos_intstr) (Types.cons pos_intstr) let intstr = Types.cup pos_intstr neg_intstr (* [ '-'? '0'--'9'+ ] *) let intstr = Types.cup pos_intstr neg_intstr (* [ '-'? '0'--'9'+ ] *) ... @@ -119,8 +119,8 @@ let intstr = Types.cup pos_intstr neg_intstr (* [ '-'? '0'--'9'+ ] *) ... @@ -119,8 +119,8 @@ let intstr = Types.cup pos_intstr neg_intstr (* [ '-'? '0'--'9'+ ] *) let true_atom = Atoms.V.mk_ascii "true"