Commit 4219614b authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix apply rule in typer

- refactoring in types.ml
- add Types.squareapply
- other fixes
parent fd4c762b
......@@ -78,6 +78,9 @@ let fresharg =
let s = Printf.sprintf "__ARG%d" !count in
incr count;
(0,U.mk s)
(*
(Ns.Uri.mk (U.mk ""),U.mk s)
*)
;;
(* Comp for Lambda.sigma but simplify if possible. *)
......@@ -189,7 +192,6 @@ and compile_abstr env a =
let d = domain(env.sigma) in
Var.Set.is_empty (Var.Set.inter d vars)
in
let (slots,nb_slots,fun_env) =
(* we add a nameless empty slot for the argument *)
if is_mono then ([Dummy],1,fun_env)
......@@ -197,7 +199,6 @@ and compile_abstr env a =
let (x, y) = fresharg () in
([Dummy;Dummy],2,Env.add (Ns.Uri.from_int x, y) (Env 1) fun_env)
in
let (slots,nb_slots,fun_env) =
(* here De Bruijn indexes are reshuffled *)
List.fold_left
......@@ -215,7 +216,6 @@ and compile_abstr env a =
)
(slots,nb_slots,fun_env) (IdSet.get a.Typed.fun_fv)
in
let slots = Array.of_list (List.rev slots) in
let env =
{ env with vars = fun_env;
......@@ -224,18 +224,18 @@ and compile_abstr env a =
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let rec lift = function
|Sel(Env i, iface, s) -> Sel(Env (i+nb_slots),iface,lift s)
|Comp(s1,s2) -> Comp(lift s1,lift s2)
let rec lift n = function
|Sel(Env i, iface, s) -> Sel(Env (i+n),iface,lift n s)
|Comp(s1,s2) -> Comp(lift n s1,lift n s2)
|s -> s
in
if is_mono then
Abstraction(slots, a.Typed.fun_iface, body, !(env.max_stack))
else
let sigma = match env.sigma with
| Identity -> Identity
| _ -> Sel(Env 1,a.Typed.fun_iface,lift(env.sigma)) in
| _ -> Sel(Env 1,a.Typed.fun_iface,lift nb_slots (env.sigma))
in
PolyAbstraction(slots, a.Typed.fun_iface, body, !(env.max_stack), sigma)
and compile_branches env (brs : Typed.branches) =
......@@ -316,15 +316,17 @@ let eval ~run ~show (tenv,cenv,codes) e =
let run_show ~run ~show tenv cenv codes ids =
if run then
let () = Eval.eval_toplevel codes in
List.iter
(fun (id,_) -> show (Some id)
(Typer.find_value id tenv)
(Some (Eval.eval_var (find id cenv)))) ids
List.iter (fun (id,_) ->
show (Some id)
(Typer.find_value id tenv)
(Some (Eval.eval_var (find id cenv)))
) ids
else
List.iter
(fun (id,_) -> show (Some id)
(Typer.find_value id tenv)
None) ids
List.iter (fun (id,_) ->
show (Some id)
(Typer.find_value id tenv)
None
) ids
let let_decl ~run ~show (tenv,cenv,codes) p e =
let (tenv,decl,ids) = Typer.type_let_decl tenv p e in
......
......@@ -5,6 +5,8 @@ open Schema_pcre
open Schema_common
open Schema_types
module Pcre = Re_pcre
(* TODO dates: boundary checks (e.g. 95/26/2003) *)
(* TODO a lot of almost cut-and-paste code, expecially in gFoo types validation
*)
......
open Encodings.Utf8
module Pcre = Re_pcre
let pcre_replace ~rex ?templ s =
match templ with
| None -> mk (Pcre.replace ~rex (get_str s))
......
......@@ -2,6 +2,7 @@
* Given Pcre.regexp regular expressions should be compiled with `UTF8 flag
* or with pcre_regexp below *)
open Encodings.Utf8
module Pcre = Re_pcre
val pcre_regexp: string -> Pcre.regexp (* compile using `UTF8 flag *)
val pcre_replace: rex:Pcre.regexp -> ?templ:t -> t -> t
val pcre_extract: rex:Pcre.regexp -> t -> t array
......
let l = ["`$A0 -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"`$A0 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1"] ;
"`$A0 -> (`$A0)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int"] ;
"(`$A00 -> `$A0) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)"] ;
"(`$A00 -> `$A0) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1"] ;
"`$A0 -> `$A1 -> Int" , ["`$A0 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)"] ;
"`$A0 -> `$A1 -> `$A0" , ["`$A0 -> `$A0" ;
"(`$A00 -> `$A0) -> `$A1"] ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0"] ;
"`$A0 -> `$A1 -> `$A2 -> Int" , ["`$A0 -> `$A1 -> `$A2 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" , ["`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1"] ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"`$A0 -> `$A1 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"(`$A00 -> `$A0) -> `$A1"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" , ["`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> `$A1 -> `$A0"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> `$A1" , ["`$A0 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A2 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A0" ;
"`$A0 -> `$A1 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" , ["(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A0" ;
"`$A0 -> `$A1 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"(`$A00 -> `$A0) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int" , ["`$A0 -> Int" ;
"`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" ;
"`$A0 -> `$A1 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" , ["`$A0 -> Int" ;
"`$A0 -> `$A0" ;
"`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"(`$A00 -> `$A0) -> `$A1" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> `$A1"]]
......@@ -185,6 +185,14 @@ let norm_tests () = [
[P(V "A","Int");P(V "B","Bool")]
];
"{a=(`$A , `$B)}","{a=(Int , Bool)}", mk_s [
[P(V "A","Empty")];
[P(V "B","Empty")];
[P(V "A","Int");P(V "B","Bool")]
];
"{a=(Int , Bool)}","{a=(`$A , `$B)}", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
"(Int , Bool)","(`$A , `$B)", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
"(Bool , Bool)","(`$A , `$B)", mk_s [ [N("Bool", V "A");N("Bool", V "B")] ];
......@@ -315,7 +323,11 @@ let tallying_tests = [
[("{a=Int}","Any")], [[]];
[("{a=`$A}","Any")], [[]];
[("{a=Int}","{a=(Int|Bool)}")], [[]];
(*
[("{a=Bool -> Bool}","{b=Int -> `$A}")], [[]];
[("{a=(Int -> Int) | (Bool -> Bool)}","{b=(`$A -> `$B)}")], [[]];
[("{a=Int} -> Int", "{a=`$A} -> `$A")], [[]];
*)
]
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
......@@ -339,10 +351,6 @@ let test_tallying =
) (Types.subtype s_sigma t_sigma) true
) sigma
) l
(*
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
SubStSet.assert_equal (elem expected) (elem result)
*)
with Tallying.Step1Fail -> assert_equal expected []
)
) tallying_tests
......@@ -458,7 +466,7 @@ let test_apply =
(print_test msg s t) >:: (fun _ ->
try
let (s,t) = (parse_typ s,parse_typ t) in
let (sl,s,t,g) = Types.apply_raw s t in
let (sl,s,t,g) = Types.apply_raw Var.Set.empty s t in
let gamma = Types.cons (Types.var (Var.mk "Gamma")) in
......
......@@ -130,6 +130,7 @@ let test_set_operations =
;;
let squaresubtype_tests = [
"`$A -> `$A", "Bool -> Bool", [], true;
"`$A -> `$B", "Int -> Bool", [], true;
"`$A -> `$B", "Int -> Bool", ["A"], false;
"`$A -> `$A", "(Int -> Int) & (Bool -> Bool)", [], true;
......@@ -200,7 +201,6 @@ let test_rec_subtitutions =
) rec_subst_tests
;;
let subtype_tests = [
"Int" , "Any", true;
"`A | Int" , "`A", false;
......@@ -221,6 +221,10 @@ let subtype_tests = [
"0--*" , "Int", true;
"1--5" , "1--*", true;
"1--5" , "1--5", true;
"3" , "Int", true;
"Int" , "0--*", false ;
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"Any -> `A" , "Any", true;
......@@ -244,12 +248,10 @@ let subtype_tests = [
"Any -> `A" , "Any -> Empty", false ;
"`A -> `B" , "`A -> `C", false ;
"Int" , "0--*", false ;
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"Int -> Int", "Empty -> Any", true;
"Any", "Any \\ Char", false;
(* polymorphic cduce extension *)
"`$X" , "Any", true;
......@@ -257,7 +259,6 @@ let subtype_tests = [
"Any", "`$X | (Any \\ `$X)", true;
"Any", "(42 & `$X) | (Any \\ (42 & `$X))", true;
"Any", "(41 & `$X) | (Any \\ (42 & `$X))", false;
"Any", "Any \\ Char", false;
"(`$A -> Bool, `$B -> `$B)", "(Int | Bool -> Int, `$A -> `$B)", false;
(* ({ (int , true) } , { }) *)
"Int -> Int", "`$A -> `$A", false;
......
......@@ -1507,6 +1507,131 @@ struct
r
end
module Arrow =
struct
let check_simple left (s1,s2) =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_line_non_empty (left,right) =
not (List.exists (check_simple left) right)
let sample t =
let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
{ empty with arrow = any.arrow } left
let check_strenghten t s =
if subtype t s then t else raise Not_found
let check_simple_iface left s1 s2 =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_iface iface s =
let rec aux = function
| [] -> false
| (p,n) :: rem ->
((List.for_all (fun (a,b) -> check_simple_iface iface a b) p) &&
(List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
|| (aux rem)
in
(* considering only arrows here and not poly variables is correct as
* the iface is just an intersection of arrows *)
aux (Pair.get (BoolPair.leafconj s.arrow))
type t = descr * (descr * descr) list list
let get t =
List.fold_left
(fun ((dom,arr) as accu) (left,right) ->
if check_line_non_empty (left,right)
then
let left = List.map (fun (t,s) -> (descr t, descr s)) left in
let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
(cap dom d, left :: arr)
else accu
)
(any, [])
(Pair.get (BoolPair.leafconj t.arrow))
let domain (dom,_) = dom
let apply_simple t result left =
let rec aux result accu1 accu2 = function
| (t1,s1)::left ->
let result =
let accu1 = diff accu1 t1 in
if non_empty accu1 then aux result accu1 accu2 left
else result
in
let result =
let accu2 = cap accu2 s1 in
aux result accu1 accu2 left
in
result
| [] ->
if subtype accu2 result then result else cup result accu2
in
aux result t any left
let apply (_,arr) t =
List.fold_left (apply_simple t) empty arr
let need_arg (dom, arr) =
List.exists (function [_] -> false | _ -> true) arr
let apply_noarg (_,arr) =
List.fold_left
(fun accu ->
function
| [(t,s)] -> cup accu s
| _ -> assert false
)
empty arr
let any = { empty with arrow = any.arrow }
let is_empty (_,arr) = arr == []
end
module Int = struct
let has_int d i = Intervals.contains i (BoolIntervals.leafconj d.ints)
let get d = d.ints
let any = { empty with ints = any.ints }
let any = { empty with ints = BoolIntervals.full }
end
module Atom = struct
let has_atom d a = Atoms.contains a (BoolAtoms.leafconj d.atoms)
let get d = d.atoms
let any = { empty with atoms = any.atoms }
end
module OldChar = Char
module Char = struct
let has_char d c = Chars.contains c (BoolChars.leafconj d.chars)
let is_empty d = Chars.is_empty (BoolChars.leafconj d.chars)
let get d = d.chars
let any = { empty with chars = any.chars }
end
module Print =
struct
......@@ -1517,12 +1642,11 @@ struct
| Pair (x,y) -> Format.fprintf ppf "(%a,%a)" print_const x print_const y
| Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" print_const x print_const y
| Record r ->
Format.fprintf ppf "Record{";
LabelMap.iteri
(fun l c ->
Format.fprintf ppf "%a : %a; " Label.print_attr l print_const c)
r;
Format.fprintf ppf "}"
let pp ppf =
LabelMap.iteri (fun l c ->
Format.fprintf ppf "%a : %a; " Label.print_attr l print_const c)
in
Format.fprintf ppf "Record{%a}" pp r
| String (i,j,s,c) ->
Format.fprintf ppf "\"%a\" %a"
U.print (U.mk (U.get_substr s i j))
......@@ -1540,12 +1664,16 @@ struct
type gname = string * Ns.QName.t
type nd = { id : int;
mutable def : d list;
mutable state :
[ `Expand | `None | `Marked
| `GlobalName of gname
| `Named of U.t ] }
type nd = {
id : int;
mutable def : d list;
mutable state :[
| `Expand
| `None
| `Marked
| `GlobalName of gname
| `Named of U.t ]
}
and d =
| Name of gname
| Regexp of nd Pretty.regexp
......@@ -1558,6 +1686,7 @@ struct
| Intersection of nd
| Neg of nd
| Abs of nd
let compare x y = x.id - y.id
module S = struct
......@@ -1576,6 +1705,7 @@ struct
let c',r = Cache.find (fun t -> t) t !memo in
memo := c';
r
let lookup t = match Cache.lookup t !memo with Some t -> t | None -> t
let named = ref DescrMap.empty
......@@ -1780,33 +1910,33 @@ struct
slot
and decompile d =
Decompile.decompile
(fun t ->
let tr = Product.get t in
let tr = Product.merge_same_first tr in
let tr = Product.clean_normal tr in
let eps = Atoms.contains nil_atom (BoolAtoms.leafconj t.atoms) in
let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in
try
let (l0,t0) = List.find
(fun ((l0,t0) as tr0) ->
let t'' =
List.fold_left
(fun accu ((li,ti) as tri) ->
if tr0 == tri then accu
else cup accu (times li ti)
)
(if eps then nil_type else empty)
tr_cons
in
equiv (descr t0) t'' ) tr_cons in
`Eps (prepare (descr l0), descr t0)
with Not_found ->
let tr = List.map (fun (l,t) -> prepare l, t) tr in
`T (tr, eps))
d
let aux t =
let tr = Product.get t in
let tr = Product.merge_same_first tr in
let tr = Product.clean_normal tr in
let eps = Atoms.contains nil_atom (BoolAtoms.leafconj t.atoms) in
let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in
try
let (l0,t0) = List.find
(fun ((l0,t0) as tr0) ->
let t'' =
List.fold_left
(fun accu ((li,ti) as tri) ->
if tr0 == tri then accu
else cup accu (times li ti)
)
(if eps then nil_type else empty)
tr_cons
in
equiv (descr t0) t'' ) tr_cons in
`Eps (prepare (descr l0), descr t0)
with Not_found ->
let tr = List.map (fun (l,t) -> prepare l, t) tr in
`T (tr, eps)
in
Decompile.decompile aux d
let gen = ref 0
......@@ -2194,7 +2324,6 @@ struct
in aux t;;
end
let memo_normalize = ref DescrMap.empty
let rec rec_normalize d =
......@@ -2220,132 +2349,6 @@ let rec rec_normalize d =
let normalize n =
descr (internalize (rec_normalize n))
module Arrow =
struct
let check_simple left (s1,s2) =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_line_non_empty (left,right) =
not (List.exists (check_simple left) right)
let sample t =
let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in