Commit 32780738 authored by Kim Nguyễn's avatar Kim Nguyễn

Code refactoring. Move the Tallying code outside of the Types module.

parent ae31d5c7
......@@ -167,7 +167,7 @@ OBJECTS = \
\
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo types/bool.cmo \
types/intervals.cmo types/chars.cmo types/atoms.cmo types/normal.cmo \
types/types.cmo compile/auto_pat.cmo \
types/types.cmo compile/auto_pat.cmo types/type_tallying.cmo \
types/sequence.cmo types/builtin_defs.cmo \
\
runtime/value.cmo \
......
......@@ -75,13 +75,13 @@ let enter_global_cu cu env x =
let rec domain = function
|Identity -> Var.Set.empty
|List l -> Types.Tallying.domain l
|List l -> Type_tallying.domain l
|Comp (s1,s2) -> Var.Set.cup (domain s1) (domain s2)
|Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| List(l) -> Type_tallying.codomain l
| Comp(s1,s2) -> Var.Set.cup (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
......
......@@ -26,7 +26,7 @@ type iface = (Types.descr * Types.descr) list
type sigma =
| Identity (* this is basically as Types.Tallying.CS.sat *)
| List of Types.Tallying.CS.sl
| List of Type_tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......@@ -104,7 +104,7 @@ module Print = struct
) ppf
in
function
|List ll -> Types.Tallying.CS.pp_sl ppf ll
|List ll -> Type_tallying.CS.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_vloc x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......
......@@ -26,7 +26,7 @@ type iface = (Types.t * Types.t) list
type sigma =
| Identity
| List of Types.Tallying.CS.sl
| List of Type_tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......
......@@ -56,6 +56,12 @@ compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi compile/auto_pat.cmi
compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \
types/atoms.cmx compile/auto_pat.cmi
types/type_tallying.cmo : types/var.cmi misc/utils.cmo types/types.cmi \
types/sortedList.cmi types/intervals.cmi misc/custom.cmo types/chars.cmi \
types/atoms.cmi types/type_tallying.cmi
types/type_tallying.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
types/sortedList.cmx types/intervals.cmx misc/custom.cmx types/chars.cmx \
types/atoms.cmx types/type_tallying.cmi
types/sequence.cmo : types/types.cmi misc/custom.cmo types/chars.cmi \
types/atoms.cmi types/sequence.cmi
types/sequence.cmx : types/types.cmx misc/custom.cmx types/chars.cmx \
......@@ -67,13 +73,13 @@ types/builtin_defs.cmx : types/types.cmx types/sequence.cmx \
types/intervals.cmx types/ident.cmx misc/encodings.cmx types/chars.cmx \
types/atoms.cmx types/builtin_defs.cmi
runtime/value.cmo : types/var.cmi misc/utils.cmo misc/upool.cmi \
types/types.cmi types/sequence.cmi misc/ns.cmi types/intervals.cmi \
misc/imap.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi \
types/atoms.cmi runtime/value.cmi
types/types.cmi types/type_tallying.cmi types/sequence.cmi misc/ns.cmi \
types/intervals.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/chars.cmi types/atoms.cmi runtime/value.cmi
runtime/value.cmx : types/var.cmx misc/utils.cmx misc/upool.cmx \
types/types.cmx types/sequence.cmx misc/ns.cmx types/intervals.cmx \
misc/imap.cmx types/ident.cmx misc/encodings.cmx types/chars.cmx \
types/atoms.cmx runtime/value.cmi
types/types.cmx types/type_tallying.cmx types/sequence.cmx misc/ns.cmx \
types/intervals.cmx misc/imap.cmx types/ident.cmx misc/encodings.cmx \
types/chars.cmx types/atoms.cmx runtime/value.cmi
schema/schema_pcre.cmo : misc/encodings.cmi schema/schema_pcre.cmi
schema/schema_pcre.cmx : misc/encodings.cmx schema/schema_pcre.cmi
schema/schema_types.cmo : runtime/value.cmi misc/ns.cmi misc/encodings.cmi \
......@@ -121,19 +127,21 @@ compile/print_auto.cmo : types/types.cmi types/ident.cmo \
compile/print_auto.cmx : types/types.cmx types/ident.cmx \
compile/auto_pat.cmx compile/print_auto.cmi
compile/lambda.cmo : runtime/value.cmi misc/utils.cmo misc/upool.cmi \
types/types.cmi schema/schema_validator.cmi misc/ns.cmi misc/imap.cmi \
types/ident.cmo misc/encodings.cmi types/compunit.cmi \
compile/auto_pat.cmi compile/lambda.cmi
types/types.cmi types/type_tallying.cmi schema/schema_validator.cmi \
misc/ns.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/compunit.cmi compile/auto_pat.cmi compile/lambda.cmi
compile/lambda.cmx : runtime/value.cmx misc/utils.cmx misc/upool.cmx \
types/types.cmx schema/schema_validator.cmx misc/ns.cmx misc/imap.cmx \
types/ident.cmx misc/encodings.cmx types/compunit.cmx \
compile/auto_pat.cmx compile/lambda.cmi
types/types.cmx types/type_tallying.cmx schema/schema_validator.cmx \
misc/ns.cmx misc/imap.cmx types/ident.cmx misc/encodings.cmx \
types/compunit.cmx compile/auto_pat.cmx compile/lambda.cmi
runtime/run_dispatch.cmo : runtime/value.cmi misc/upool.cmi types/types.cmi \
misc/imap.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi \
compile/auto_pat.cmi types/atoms.cmi runtime/run_dispatch.cmi
types/type_tallying.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/chars.cmi compile/auto_pat.cmi types/atoms.cmi \
runtime/run_dispatch.cmi
runtime/run_dispatch.cmx : runtime/value.cmx misc/upool.cmx types/types.cmx \
misc/imap.cmx types/ident.cmx misc/encodings.cmx types/chars.cmx \
compile/auto_pat.cmx types/atoms.cmx runtime/run_dispatch.cmi
types/type_tallying.cmx misc/imap.cmx types/ident.cmx misc/encodings.cmx \
types/chars.cmx compile/auto_pat.cmx types/atoms.cmx \
runtime/run_dispatch.cmi
runtime/explain.cmo : runtime/value.cmi misc/upool.cmi types/types.cmi \
runtime/run_dispatch.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/chars.cmi compile/auto_pat.cmi types/atoms.cmi runtime/explain.cmi
......@@ -169,13 +177,15 @@ parser/parser.cmx : types/var.cmx parser/ulexer.cmx types/types.cmx \
misc/encodings.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx \
parser/ast.cmx parser/parser.cmi
typing/typed.cmo : types/var.cmi misc/utils.cmo misc/upool.cmi \
types/types.cmi schema/schema_validator.cmi types/patterns.cmi \
misc/ns.cmi types/intervals.cmi types/ident.cmo misc/encodings.cmi \
types/compunit.cmi types/chars.cmi parser/cduce_loc.cmi types/atoms.cmi
types/types.cmi types/type_tallying.cmi schema/schema_validator.cmi \
types/patterns.cmi misc/ns.cmi types/intervals.cmi types/ident.cmo \
misc/encodings.cmi types/compunit.cmi types/chars.cmi \
parser/cduce_loc.cmi types/atoms.cmi
typing/typed.cmx : types/var.cmx misc/utils.cmx misc/upool.cmx \
types/types.cmx schema/schema_validator.cmx types/patterns.cmx \
misc/ns.cmx types/intervals.cmx types/ident.cmx misc/encodings.cmx \
types/compunit.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx
types/types.cmx types/type_tallying.cmx schema/schema_validator.cmx \
types/patterns.cmx misc/ns.cmx types/intervals.cmx types/ident.cmx \
misc/encodings.cmx types/compunit.cmx types/chars.cmx \
parser/cduce_loc.cmx types/atoms.cmx
typing/typepat.cmo : types/types.cmi types/sequence.cmi types/patterns.cmi \
types/ident.cmo misc/encodings.cmi types/chars.cmi typing/typepat.cmi
typing/typepat.cmx : types/types.cmx types/sequence.cmx types/patterns.cmx \
......@@ -183,26 +193,26 @@ typing/typepat.cmx : types/types.cmx types/sequence.cmx types/patterns.cmx \
types/externals.cmo : parser/cduce_loc.cmi types/externals.cmi
types/externals.cmx : parser/cduce_loc.cmx types/externals.cmi
typing/typer.cmo : types/var.cmi misc/utils.cmo types/types.cmi \
typing/typepat.cmi typing/typed.cmo types/sequence.cmi \
schema/schema_validator.cmi types/patterns.cmi misc/ns.cmi \
types/ident.cmo types/externals.cmi types/compunit.cmi types/chars.cmi \
parser/cduce_loc.cmi types/builtin_defs.cmi types/atoms.cmi \
parser/ast.cmo typing/typer.cmi
typing/typepat.cmi typing/typed.cmo types/type_tallying.cmi \
types/sequence.cmi schema/schema_validator.cmi types/patterns.cmi \
misc/ns.cmi types/ident.cmo types/externals.cmi types/compunit.cmi \
types/chars.cmi parser/cduce_loc.cmi types/builtin_defs.cmi \
types/atoms.cmi parser/ast.cmo typing/typer.cmi
typing/typer.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
typing/typepat.cmx typing/typed.cmx types/sequence.cmx \
schema/schema_validator.cmx types/patterns.cmx misc/ns.cmx \
types/ident.cmx types/externals.cmx types/compunit.cmx types/chars.cmx \
parser/cduce_loc.cmx types/builtin_defs.cmx types/atoms.cmx \
parser/ast.cmx typing/typer.cmi
typing/typepat.cmx typing/typed.cmx types/type_tallying.cmx \
types/sequence.cmx schema/schema_validator.cmx types/patterns.cmx \
misc/ns.cmx types/ident.cmx types/externals.cmx types/compunit.cmx \
types/chars.cmx parser/cduce_loc.cmx types/builtin_defs.cmx \
types/atoms.cmx parser/ast.cmx typing/typer.cmi
compile/compile.cmo : types/var.cmi runtime/value.cmi misc/upool.cmi \
types/types.cmi typing/typer.cmi typing/typed.cmo types/patterns.cmi \
misc/ns.cmi compile/lambda.cmi misc/imap.cmi types/ident.cmo \
runtime/eval.cmi types/compunit.cmi parser/cduce_loc.cmi \
types/types.cmi typing/typer.cmi typing/typed.cmo types/type_tallying.cmi \
types/patterns.cmi misc/ns.cmi compile/lambda.cmi misc/imap.cmi \
types/ident.cmo runtime/eval.cmi types/compunit.cmi parser/cduce_loc.cmi \
compile/auto_pat.cmi parser/ast.cmo compile/compile.cmi
compile/compile.cmx : types/var.cmx runtime/value.cmx misc/upool.cmx \
types/types.cmx typing/typer.cmx typing/typed.cmx types/patterns.cmx \
misc/ns.cmx compile/lambda.cmx misc/imap.cmx types/ident.cmx \
runtime/eval.cmx types/compunit.cmx parser/cduce_loc.cmx \
types/types.cmx typing/typer.cmx typing/typed.cmx types/type_tallying.cmx \
types/patterns.cmx misc/ns.cmx compile/lambda.cmx misc/imap.cmx \
types/ident.cmx runtime/eval.cmx types/compunit.cmx parser/cduce_loc.cmx \
compile/auto_pat.cmx parser/ast.cmx compile/compile.cmi
schema/schema_parser.cmo : parser/url.cmi schema/schema_xml.cmi \
schema/schema_validator.cmi schema/schema_types.cmi \
......@@ -290,9 +300,9 @@ query/query_aggregates.cmo : runtime/value.cmi types/sequence.cmi \
compile/operators.cmi types/intervals.cmi types/builtin_defs.cmi
query/query_aggregates.cmx : runtime/value.cmx types/sequence.cmx \
compile/operators.cmx types/intervals.cmx types/builtin_defs.cmx
parser/cduce_netclient.cmo : runtime/value.cmi parser/url.cmi \
parser/cduce_curl.cmo : runtime/value.cmi parser/url.cmi \
driver/cduce_config.cmi
parser/cduce_netclient.cmx : runtime/value.cmx parser/url.cmx \
parser/cduce_curl.cmx : runtime/value.cmx parser/url.cmx \
driver/cduce_config.cmx
runtime/cduce_pxp.cmo : runtime/value.cmi parser/url.cmi \
schema/schema_xml.cmi runtime/load_xml.cmi driver/cduce_config.cmi \
......@@ -376,11 +386,12 @@ types/types.cmi : types/var.cmi misc/ns.cmi types/intervals.cmi \
types/atoms.cmi
compile/auto_pat.cmi : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi
types/type_tallying.cmi : types/var.cmi types/types.cmi
types/sequence.cmi : types/types.cmi types/atoms.cmi
types/builtin_defs.cmi : types/types.cmi types/ident.cmo types/atoms.cmi
runtime/value.cmi : types/types.cmi misc/ns.cmi types/intervals.cmi \
misc/imap.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi \
types/atoms.cmi
runtime/value.cmi : types/types.cmi types/type_tallying.cmi misc/ns.cmi \
types/intervals.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/chars.cmi types/atoms.cmi
schema/schema_pcre.cmi : misc/encodings.cmi
schema/schema_types.cmi : runtime/value.cmi misc/ns.cmi misc/encodings.cmi \
types/atoms.cmi
......@@ -396,8 +407,8 @@ types/patterns.cmi : types/types.cmi types/ident.cmo misc/custom.cmo \
compile/auto_pat.cmi
compile/print_auto.cmi : compile/auto_pat.cmi
compile/lambda.cmi : runtime/value.cmi types/types.cmi \
schema/schema_validator.cmi misc/ns.cmi misc/imap.cmi types/ident.cmo \
types/compunit.cmi compile/auto_pat.cmi
types/type_tallying.cmi schema/schema_validator.cmi misc/ns.cmi \
misc/imap.cmi types/ident.cmo types/compunit.cmi compile/auto_pat.cmi
runtime/run_dispatch.cmi : runtime/value.cmi compile/auto_pat.cmi
runtime/explain.cmi : runtime/value.cmi compile/auto_pat.cmi
runtime/eval.cmi : runtime/value.cmi misc/ns.cmi compile/lambda.cmi \
......
......@@ -201,7 +201,7 @@ let rec eval_sigma env =
List.fold_left (fun acc sigma_j ->
let exists_sub =
List.exists (fun (_,s_i) ->
inzero env env.(x) (Types.Tallying.(s_i >> sigma_j))
inzero env env.(x) (Type_tallying.(s_i >> sigma_j))
) iface
in
if exists_sub then sigma_j::acc else acc
......@@ -219,7 +219,7 @@ and inzero env v t =
| Abstraction (Some iface,_,sigma) ->
let s = List.fold_left (fun acc t -> Types.cap acc (snd t)) Types.any iface in
List.for_all (fun si ->
Types.subtype (Types.Tallying.(s >> si)) t
Types.subtype (Type_tallying.(s >> si)) t
) (eval_sigma env sigma)
| _ -> true
......
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Types.Tallying.CS.sl
| List of Type_tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......@@ -26,13 +26,13 @@ and t =
let rec domain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.domain l
| List(l) -> Type_tallying.domain l
| Comp(s1,s2) -> Var.Set.cup (domain s1) (domain s2)
| Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| List(l) -> Type_tallying.codomain l
| Comp(s1,s2) -> Var.Set.cup (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
......@@ -313,7 +313,7 @@ module Print = struct
) ppf
in
function
|List ll -> Types.Tallying.CS.pp_sl ppf ll
|List ll -> Type_tallying.CS.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......@@ -506,7 +506,7 @@ let rec compare_sigma x y =
| List(sl1), List(sl2) ->
if List.for_all2 (fun v1 v2 ->
Types.Tallying.E.comparea v1 v2 ) sl1 sl2 = 0 then 0
Type_tallying.E.comparea v1 v2 ) sl1 sl2 = 0 then 0
else (List.length sl1) - (List.length sl2)
| Sel(t1,if1,s1), Sel(t2,if2,s2) ->
......
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Types.Tallying.CS.sl
| List of Type_tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......
open Types
let cap_t d t = cap d (descr t)
let cap_product any_left any_right l =
List.fold_left
(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
(any_left,any_right)
l
type constr =
|Pos of (Var.var * Types.t) (** alpha <= t | alpha \in P *)
|Neg of (Types.t * Var.var) (** t <= alpha | alpha \in N *)
exception UnSatConstr of string
module CS = struct
(* we require that types are semantically equivalent and not structurally
* equivalent *)
let semantic_compare t1 t2 =
let c = Types.compare t1 t2 in
if c = 0 then 0 else
if equiv t1 t2 then 0
else c
(* constraint set : map to store constraints of the form (s <= alpha <= t) *)
module M = struct
module Key = struct
type t = Var.var
let compare v1 v2 = Var.compare v1 v2
end
type key = Key.t
module VarMap = Map.Make(Key)
type t = (Types.t * Types.t) VarMap.t
let singleton = VarMap.singleton
let cardinal = VarMap.cardinal
(* a set of constraints m1 subsumes a set of constraints m2,
that is the solutions for m1 contains all the solutions for
m2 if:
forall i1 <= v <= s1 in m1,
there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
*)
let subsumes map1 map2 =
VarMap.for_all (fun v (i1, s1) ->
try let i2, s2 = VarMap.find v map2 in
subtype i1 i2 && subtype s2 s1
with Not_found -> false
) map1
let pp ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.pp v Print.pp_type s
) ppf (VarMap.bindings map)
let compare map1 map2 =
VarMap.compare (fun (i1,s1) (i2,s2) ->
let c = semantic_compare i1 i2 in
if c == 0 then semantic_compare s1 s2
else c) map1 map2
let add delta v (inf, sup) map =
let new_i, new_s =
try
let old_i, old_s = VarMap.find v map in
cup old_i inf,
cap old_s sup
with
Not_found -> inf, sup
in
if Var.Set.mem delta v then map
else VarMap.add v (new_i, new_s) map
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold
let empty = VarMap.empty
let for_all = VarMap.for_all
end
(* equation set : (s < alpha < t) stored as
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module E = struct
include Map.Make(struct
type t = Var.var
let compare = Var.compare
end)
let pp ppf e =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
) ppf (bindings e)
end
(* Set of equation sets *)
module ES = struct
include Set.Make(struct
type t = Types.t E.t
let compare = E.compare semantic_compare
end)
let pp ppf s = Utils.pp_list ~delim:("{","}") E.pp ppf (elements s)
end
(* Set of constraint sets *)
module S = struct
(* A set of constraint-sets is just a list of constraint-sets,
that are pairwise "non-subsumable"
*)
type t = M.t list
let elements t = t
let empty = []
let add m l =
let rec loop m l acc =
match l with
[] -> m :: acc
| mm :: ll ->
if M.subsumes m mm then List.rev_append ll (m::acc)
else if M.subsumes mm m then List.rev_append ll (mm::acc)
else loop m ll (mm::acc)
in
loop m l []
let singleton m = add m empty
let pp ppf s = Utils.pp_list ~delim:("{","}") M.pp ppf s
let fold f l a = List.fold_left (fun e a -> f a e) a l
let is_empty l = l == []
(* Square union : *)
let union s1 s2 =
match s1, s2 with
[], _ -> s2
| _, [] -> s1
| _ ->
(* Invariant: all elements of s1 (resp s2) are pairwise
incomparable (they don't subsume one another)
let e1 be an element of s1:
- if e1 subsumes no element of s2, add e1 to the result
- if e1 subsumes an element e2 of s2, add e1 to the
result and remove e2 from s2
- if an element e2 of s2 subsumes e1, add e2 to the
result and remove e2 from s2 (and discard e1)
once we are done for all e1, add the remaining elements from
s2 to the result.
*)
let append e1 s2 result =
let rec loop s2 accs2 =
match s2 with
[] -> accs2, e1::result
| e2 :: ss2 ->
if M.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
else if M.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
else loop ss2 (e2::accs2)
in
loop s2 []
in
let rec loop s1 s2 result =
match s1 with
[] -> List.rev_append s2 result
| e1 :: ss1 ->
let new_s2, new_result = append e1 s2 result in
loop ss1 new_s2 new_result
in
loop s1 s2 []
(* Square intersection *)
let inter delta s1 s2 =
match s1,s2 with
[], _ | _, [] -> []
| _ ->
(* Perform the cartesian product. For each constraint m1 in s1,
m2 in s2, we add M.inter m1 m2 to the result.
Optimisations:
- we use add to ensure that we do not add something that subsumes
a constraint set that is already in the result
- if m1 subsumes m2, it means that whenever m2 holds, so does m1, so
we only add m2 (note that the condition is reversed w.r.t. union).
*)
fold (fun m1 acc1 ->
fold (fun m2 acc2 ->
let merged = if M.subsumes m1 m2 then m2
else if M.subsumes m2 m1 then m1
else M.inter delta m1 m2
in
add merged acc2
)
s2 acc1) s1 []
let filter = List.filter
end
type s = S.t
type m = M.t
type es = ES.t
type sigma = Types.t E.t
module SUB = SortedList.FiniteCofinite(struct
type t = Types.t E.t
let compare = E.compare compare
let equal = E.equal equal
let hash = Hashtbl.hash
let dump = E.pp
let check _ = ()
end)
type sl = sigma list
let singleton c =
let constr =
match c with
|Pos (v,s) -> M.singleton v (empty,s)
|Neg (s,v) -> M.singleton v (s,any)
in
S.singleton constr
let pp_s = S.pp
let pp_m = M.pp
let pp_e = E.pp
let pp_sl ppf ll = Utils.pp_list ~delim:("{","}") E.pp ppf ll
let sat = S.singleton M.empty
let unsat = S.empty
let union = S.union
let prod delta = S.inter delta
let merge delta = M.inter delta
end
let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let normabstract (t,_,_) = if Abstracts.is_empty t then CS.sat else CS.unsat
let single_aux constr (b,v,p,n) =
let aux f constr l =
List.fold_left (fun acc ->
function
|`Var a -> cap acc (f(var a))
|`Atm a -> cap acc (f(constr a))
) any l
in
let id = (fun x -> x) in
let t = cap (aux id constr p) (aux neg constr n) in
(* t = bigdisj ... alpha \in P --> alpha <= neg t *)
(* t = bigdisj ... alpha \in N --> t <= alpha *)
if b then (neg t) else t
let single_atoms = single_aux atom
let single_abstract = single_aux abstract
let single_chars = single_aux char
let single_ints = single_aux interval
let single_times = single_aux (fun p -> VarTimes.(inj (atom (`Atm p))))
let single_xml = single_aux (fun p -> VarXml.(inj (atom (`Atm p))))
let single_record = single_aux (fun p -> VarRec.(inj (atom (`Atm p))))
let single_arrow = single_aux (fun p -> VarArrow.(inj (atom (`Atm p))))
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
let _compare delta v1 v2 =
let monov1 = Var.Set.mem delta v1 in
let monov2 = Var.Set.mem delta v2 in
if monov1 == monov2 then
Var.compare v1 v2
else
if monov1 then 1 else -1
in
match (p,n) with
|([], (`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton (Neg (t, x))
|((`Var x)::pos,[]) ->
let t = single (true,x,pos,[]) in
CS.singleton (Pos (x,t))
|((`Var x)::pos, (`Var y)::neg) ->
if _compare delta x y < 0 then
let t = single (true,x,pos,n) in
CS.singleton (Pos (x,t))
else
let t = single (false,y,p,neg) in
CS.singleton (Neg (t, y))
|([`Atm a], (`Var x)::neg) ->
let t = single (false,x,p,neg) in
CS.singleton (Neg (t,x))
|([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false
let big_prod delta f acc l =
List.fold_left (fun acc (pos,neg) ->
(* if CS.S.is_empty acc then acc else *)
CS.prod delta acc (f pos neg)
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17
let () = Format.pp_set_margin Format.err_formatter 100
let rec norm (t,delta,mem) =
DEBUG normrec (
Format.eprintf
" @[Entering norm rec(%a):@\n" Print.pp_type t);
let res =
try
(* If we find it in the global hashtable, we are finished *)
let res = NormMemoHash.find memo_norm (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in global table @]@\n");
res
with
Not_found ->
try
let finished, cst = NormMemoHash.find mem (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in local table, finished = %b @]@\n" finished);
if finished then cst else CS.sat
with
Not_found ->
begin
let res =
(* base cases *)
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
CS.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
CS.unsat
end else if is_var t then begin
let (v,p) = Variable.extract t in
if Var.Set.mem delta v then begin
DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
CS.unsat (* if it is monomorphic, unsat *)
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
end
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in
let t = Iter.simplify t in
let aux single norm_aux acc l =
big_prod delta (toplevel delta single norm_aux mem) acc l
in
let acc = aux single_atoms normatoms CS.sat VarAtoms.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_chars normchars acc VarChars.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_ints normints acc VarIntervals.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_times normpair acc VarTimes.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_xml normpair acc VarXml.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_arrow normarrow acc VarArrow.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_abstract normabstract acc VarAbstracts.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
(* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc VarRec.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);
let acc = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) ->
if Var.Set.mem delta v then
(* constraint on a monomorphic variables must be trivial *)
let x = var v in subtype s x && subtype x t
else true (*
subtype s t || (non_empty (cap s t)) *)
) m)
acc
in
DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@]@\n");
acc
end
in
NormMemoHash.replace mem (t, delta) (true,res); res
end
in
DEBUG normrec (Format.eprintf
"Leaving norm rec(%a) = %a@]@\n%!"
Print.pp_type t
CS.pp_s res
);
res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
* [t1] v [t2] v ( [t1 \ s1] ^ [t2 \ s2] ^
* [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ... )
*
* prod(p,n) = [t1] v [t2] v prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
* ([t2\s2] v prod'(t1,t2\s2,n))
* *)
and normpair (t,delta,mem) =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> CS.unsat
|(s1,s2) :: rest -> begin
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
let con1 = norm (z1, delta, mem) in
let con2 = norm (z2, delta, mem) in
let con10 = aux z1 t2 rest in
let con20 = aux t1 z2 rest in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod delta con11 con22
end
in
(* cap_product return the intersection of all (fst pos,snd pos) *)