Skip to content

GitLab

Commit a699b619 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2006-04-21 15:53:55 by afrisch] Compute witnesses during subtyping 

Original author: afrisch
Date: 2006-04-21 15:53:56+00:00
parent b7e03bbe
Hide whitespace changes
Inline Side-by-side
Showing with 311 additions and 91 deletions
driver/cduce.ml
View file @ a699b619
......@@ -191,7 +191,8 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "[DEBUG:sample]@.";
(try
let t = Types.descr (Typer.typ tenv t) in
Format.fprintf ppf "%a@." print_sample (Sample.get t)
Format.fprintf ppf "%a@." print_sample (Sample.get t);
Format.fprintf ppf "witness: %a@." Types.print_witness (Types.witness t);
with Not_found ->
Format.fprintf ppf "Empty type : no sample !@.")
| `Filter (t,p) ->
......
types/atoms.ml
View file @ a699b619
......@@ -95,3 +95,12 @@ let mk_map l =
let mtags = Imap.create (Array.of_list !all_tags) in
let mns = Imap.create (Array.of_list !all_ns) in
(mtags,mns,!def)
type sample = (Ns.Uri.t * Ns.Label.t option) option
let contains_sample s t =
match s,(get t) with
| None, `Cofinite _ -> true
| None, `Finite _ -> false
| Some (_,Some tag),_ -> contains tag t
| Some (ns, None),_ -> is_empty (diff (any_in_ns ns) t)
types/atoms.mli
View file @ a699b619
......@@ -32,6 +32,10 @@ val print_tag : t -> (Format.formatter -> unit) option
val single : t -> V.t
type sample = (Ns.Uri.t * Ns.Label.t option) option
val sample : t -> sample
val contains_sample: sample -> t -> bool
type 'a map
val mk_map: (t * 'a) list -> 'a map
val get_map: V.t -> 'a map -> 'a
......
types/sequence.ml
View file @ a699b619
......@@ -45,7 +45,7 @@ let mapping f t queue =
let aux_concat = mapping (fun t v -> V.times (V.ty t) v)
let aux_flatten t = mapping aux_concat t (V.ty nil_type)
let aux_map f t =
let f = memoize f in
let f = memoize f in
mapping (fun t v -> V.times (V.ty (f t)) v) t (V.ty nil_type)
let solve x = Types.descr (V.solve x)
......
types/sortedList.ml
View file @ a699b619
......@@ -410,6 +410,7 @@ module type FiniteCofinite = sig
val contains: elem -> t -> bool
val disjoint: t -> t -> bool
val is_empty: t -> bool
val sample: t -> elem option
end
module FiniteCofinite(X : Custom.T) = struct
......@@ -438,6 +439,11 @@ module FiniteCofinite(X : Custom.T) = struct
| Finite s -> Format.fprintf ppf "Finite[%a]" SList.dump s
| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" SList.dump s
let sample = function
| Finite (x::_) -> Some x
| Finite [] -> raise Not_found
| Cofinite _ -> None
let empty = Finite []
let any = Cofinite []
......@@ -491,6 +497,12 @@ struct
module T = T0.Map
type t = Finite of TMap.t | Cofinite of TMap.t
let sample = function
| Cofinite _ -> None
| Finite l -> (match T.get l with
| [] -> raise Not_found
| (x,y)::_ -> Some (x, SymbolSet.sample y))
let get = function
| Finite l -> `Finite (T.get l)
| Cofinite l -> `Cofinite (T.get l)
......
types/sortedList.mli
View file @ a699b619
......@@ -91,6 +91,8 @@ module type FiniteCofinite = sig
val contains: elem -> t -> bool
val disjoint: t -> t -> bool
val is_empty: t -> bool
val sample: t -> elem option
end
module FiniteCofinite(X : Custom.T) : FiniteCofinite with type elem = X.t
......@@ -114,4 +116,7 @@ sig
val get: t -> [ `Finite of (X.t * SymbolSet.t) list
| `Cofinite of (X.t * SymbolSet.t) list ]
val sample: t -> (X.t * SymbolSet.elem option) option
end
types/types.ml
View file @ a699b619
......@@ -95,6 +95,12 @@ struct
List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
Format.fprintf ppf "@]" ]
let contains_sample s t = match s,t with
| None, Cofinite _ -> true
| None, Finite _ -> false
| Some s, t -> contains s t
end
......@@ -480,53 +486,60 @@ let rec exists max f =
exception NotEmpty
type witness =
| WInt of Intervals.V.t
| WAtom of Atoms.sample
| WChar of Chars.V.t
| WPair of witness * witness
| WXml of witness * witness
| WRecord of witness label_map * bool
| WFun of (witness * witness option) list
| WAbstract of Abstract.elem option
| WAbsent
let eps_witness = WAtom (Atoms.sample (Atoms.atom (Atoms.V.mk_ascii "nil")))
type slot = { mutable status : status;
mutable notify : notify;
mutable active : bool }
and status = Empty | NEmpty | Maybe
and notify = Nothing | Do of slot * (slot -> unit) * notify
and status = Empty | NEmpty of witness | Maybe
and notify = Nothing | Do of slot * (witness -> unit) * notify
let slot_empty = { status = Empty; active = false; notify = Nothing }
let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }
let slot_nempty w = { status = NEmpty w;
active = false; notify = Nothing }
let slot_eps = slot_nempty eps_witness
let rec notify = function
let rec notify w = function
| Nothing -> ()
| Do (n,f,rem) ->
if n.status == Maybe then (try f n with NotEmpty -> ());
notify rem
if n.status == Maybe then (try f w with NotEmpty -> ());
notify w rem
let rec iter_s s f = function
| [] -> ()
| arg::rem -> f arg s; iter_s s f rem
let set s =
s.status <- NEmpty;
notify s.notify;
let set s w =
s.status <- NEmpty w;
notify w s.notify;
s.notify <- Nothing;
raise NotEmpty
let rec big_conj f l n =
let rec big_conj f l n w =
match l with
| [] -> set n
| [arg] -> f arg n
| [] -> set n w
| [arg] -> f w arg n
| arg::rem ->
let s =
{ status = Maybe; active = false;
notify = Do (n,(big_conj f rem), Nothing) } in
notify = Do (n,(big_conj f rem n), Nothing) } in
try
f arg s;
f w arg s;
if s.active then n.active <- true
with NotEmpty -> if n.status == NEmpty then raise NotEmpty
let guard a f n =
match a with
| { status = Empty } -> ()
| { status = Maybe } as s ->
n.active <- true;
s.notify <- Do (n,f,s.notify)
| { status = NEmpty } -> f n
with NotEmpty when n.status == Empty || n.status == Maybe -> ()
(* Fast approximation *)
......@@ -541,7 +554,7 @@ let rec slot d =
(Atoms.is_empty d.atoms) &&
(Chars.is_empty d.chars) &&
(Abstract.is_empty d.abstract) &&
(not d.absent)) then slot_not_empty
(not d.absent)) then slot_eps
else try DescrHash.find memo d
with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in
......@@ -556,53 +569,60 @@ let rec slot d =
NotEmpty -> ());
s
and guard n t f = match (slot t) with
| { status = Empty } -> ()
| { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
| { status = NEmpty v } -> f v
and check_times (left,right) s =
let (accu1,accu2) = cap_product any any left in
let single_right (t1,t2) s =
let single_right w (t1,t2) s =
let t1 = descr t1 and t2 = descr t2 in
if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s
if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s w
else
let accu1 = diff accu1 t1 in guard (slot accu1) set s;
let accu2 = diff accu2 t2 in guard (slot accu2) set s in
guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s
let accu1 = diff accu1 t1 in guard s accu1 (set s);
let accu2 = diff accu2 t2 in guard s accu2 (set s) in
guard s accu1
(fun _ -> guard s accu2 (big_conj single_right right s))
and check_xml (left,right) s =
let (accu1,accu2) = cap_product any any_pair left in
let single_right (t1,t2) s =
let single_right w (t1,t2) s =
let t1 = descr t1 and t2 = descr t2 in
if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s
if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s w
else
let accu1 = diff accu1 t1 in guard (slot accu1) set s;
let accu2 = diff accu2 t2 in guard (slot accu2) set s in
guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s
let accu1 = diff accu1 t1 in guard s accu1 (set s);
let accu2 = diff accu2 t2 in guard s accu2 (set s) in
guard s accu1
(fun _ -> guard s accu2 (big_conj single_right right s))
and check_arrow (left,right) s =
let single_right (s1,s2) s =
let single_right w (s1,s2) s =
let accu1 = descr s1 and accu2 = neg (descr s2) in
let single_left (t1,t2) s =
let accu1 = diff_t accu1 t1 in guard (slot accu1) set s;
let accu2 = cap_t accu2 t2 in guard (slot accu2) set s
let single_left w (t1,t2) s =
let accu1 = diff_t accu1 t1 in guard s accu1 (set s);
let accu2 = cap_t accu2 t2 in guard s accu2 (set s)
in
guard (slot accu1) (big_conj single_left left) s
guard s accu1 (big_conj single_left left s)
in
big_conj single_right right s
big_conj single_right right s eps_witness
and check_record (labels,(oleft,left),rights) s =
let rec single_right (oright,right) s =
let rec single_right w (oright,right) s =
let next =
(oleft && (not oright)) ||
exists (Array.length left)
(fun i -> trivially_disjoint left.(i) right.(i))
in
if next then set s
if next then set s w
else
for i = 0 to Array.length left - 1 do
let di = diff left.(i) right.(i) in guard (slot di) set s
let di = diff left.(i) right.(i) in guard s di (set s)
done
in
let rec start i s =
if (i < 0) then big_conj single_right rights s
else guard (slot left.(i)) (start (i - 1)) s
let rec start i s w =
if (i < 0) then big_conj single_right rights s w
else guard s left.(i) (start (i - 1) s)
in
start (Array.length left - 1) s
......@@ -638,11 +658,15 @@ let complex = ref 0
let rec slot d =
incr complex;
Stats.Counter.incr count_subtype;
if not ((Intervals.is_empty d.ints) &&
(Atoms.is_empty d.atoms) &&
(Chars.is_empty d.chars) &&
(Abstract.is_empty d.abstract) &&
(not d.absent)) then slot_not_empty
if not (Intervals.is_empty d.ints)
then slot_nempty (WInt (Intervals.sample d.ints))
else if not (Atoms.is_empty d.atoms)
then slot_nempty (WAtom (Atoms.sample d.atoms))
else if not (Chars.is_empty d.chars)
then slot_nempty (WChar (Chars.sample d.chars))
else if not (Abstract.is_empty d.abstract)
then slot_nempty (WAbstract (Abstract.sample d.abstract))
else if d.absent then slot_nempty WAbsent
else try DescrHash.find memo d
with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in
......@@ -657,94 +681,109 @@ let rec slot d =
NotEmpty -> ());
s
and guard n t f = match (slot t) with
| { status = Empty } -> ()
| { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
| { status = NEmpty v } -> f v
and check_times (left,right) s =
let rec aux accu1 accu2 right s = match right with
let rec aux w1 w2 accu1 accu2 right = match right with
| (n1,n2)::right ->
let t1 = descr n1 and t2 = descr n2 in
if trivially_disjoint accu1 t1 ||
trivially_disjoint accu2 t2 then (
aux accu1 accu2 right s )
trivially_disjoint accu2 t2 then
aux w1 w2 accu1 accu2 right
else (
let accu1' = diff accu1 t1 in
guard (slot accu1') (aux accu1' accu2 right) s;
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 right);
let accu2' = diff accu2 t2 in
guard (slot accu2') (aux accu1 accu2' right) s
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' right)
)
| [] -> set s
| [] -> set s (WPair (w1,w2))
in
let (accu1,accu2) = cap_product any any left in
let rec check_trivial l s = match l with
| [] -> aux accu1 accu2 right s
let rec check_trivial w1 w2 l = match l with
| [] -> aux w1 w2 accu1 accu2 right
| (n1,n2)::l ->
let t1 = diff accu1 (descr n1) in
if Descr.equal t1 empty then
let t2 = diff accu2 (descr n2) in
guard (slot t2) (check_trivial l) s
guard s t2 (fun _ -> check_trivial w1 w2 l)
else
check_trivial l s
check_trivial w1 w2 l
in
guard (slot accu1) (guard (slot accu2) (check_trivial right)) s
guard s accu1
(fun w1 -> guard s accu2
(fun w2 -> check_trivial w1 w2 right))
and check_xml (left,right) s =
let rec aux accu1 accu2 right s = match right with
let rec aux w1 w2 accu1 accu2 right = match right with
| (n1,n2)::right ->
let t1 = descr n1 and t2 = descr n2 in
if clearly_disjoint accu1 t1 ||
trivially_disjoint accu2 t2 then (
aux accu1 accu2 right s )
trivially_disjoint accu2 t2 then
aux w1 w2 accu1 accu2 right
else (
let accu1' = diff accu1 t1 in
guard (slot accu1') (aux accu1' accu2 right) s;
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 right);
let accu2' = diff accu2 t2 in
guard (slot accu2') (aux accu1 accu2' right) s
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' right)
)
| [] -> set s
| [] -> set s (WXml (w1,w2))
in
let (accu1,accu2) = cap_product any any_pair left in
guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
guard s accu1
(fun w1 ->
guard s accu2
(fun w2 -> aux w1 w2 accu1 accu2 right))
and check_arrow (left,right) s =
let single_right (s1,s2) s =
let rec aux accu1 accu2 left s = match left with
let single_right f (s1,s2) s =
let rec aux w1 w2 accu1 accu2 left = match left with
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
guard (slot accu1') (aux accu1' accu2 left) s;
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
let accu2' = cap_t accu2 t2 in
guard (slot accu2') (aux accu1 accu2' left) s
| [] -> set s
guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
| [] -> (match f with WFun l -> set s (WFun ((w1,w2)::l))
| _ -> assert false)
in
let accu1 = descr s1 in
guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
in
big_conj single_right right s
big_conj single_right right s (WFun [])
and check_record (labels,(oleft,left),rights) s =
let rec aux left rights s = match rights with
| [] -> set s
let rec aux ws left rights = match rights with
| [] ->
let rec aux w i = function
| [] -> assert (i == Array.length ws); w
| l::labs -> aux (LabelMap.add l ws.(i) w) (succ i) labs in
set s (WRecord (aux LabelMap.empty 0 labels,oleft))
| (oright,right)::rights ->
let next =
(oleft && (not oright)) ||
exists (Array.length left)
(fun i -> trivially_disjoint left.(i) right.(i))
in
if next then aux left rights s
if next then aux ws left rights
else
for i = 0 to Array.length left - 1 do
let left' = Array.copy left in
let di = diff left.(i) right.(i) in
left'.(i) <- di;
guard (slot di) (aux left' rights) s;
guard s di (fun w ->
let left' = Array.copy left in left'.(i) <- di;
let ws' = Array.copy ws in ws'.(i) <- w;
aux ws' left' rights);
done
in
let rec start i s =
if (i < 0) then aux left rights s
else
guard (slot left.(i)) (start (i - 1)) s
let rec start wl i =
if (i < 0) then aux (Array.of_list wl) left rights
else guard s left.(i) (fun w -> start (w::wl) (i - 1))
in
start (Array.length left - 1) s
start [] (Array.length left - 1)
......@@ -762,6 +801,49 @@ let is_empty d =
Stats.Timer.stop timer_subtype
(s.status == Empty)
let rec print_witness ppf = function
| WInt i ->
Format.fprintf ppf "%a" Intervals.V.print i
| WChar c ->
Format.fprintf ppf "%a" Chars.V.print c
| WAtom None ->
Format.fprintf ppf "`#:#"
| WAtom (Some (ns,None)) ->
Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
| WAtom (Some (_,Some t)) ->
Format.fprintf ppf "`%a" Ns.Label.print_attr t
| WPair (w1,w2) ->
Format.fprintf ppf "(%a,%a)" print_witness w1 print_witness w2
| WXml (w1,w2) ->
Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
| WRecord (ws,o) ->
Format.fprintf ppf "{";
LabelMap.iteri
(fun l w -> Format.fprintf ppf " %a=%a"
Label.print_attr l print_witness w)
ws;
if o then Format.fprintf ppf " ..";
Format.fprintf ppf " }"
| WFun f ->
Format.fprintf ppf "{";
List.iter (fun (x,y) ->
Format.fprintf ppf " %a->" print_witness x;
match y with
| None -> Format.fprintf ppf "#"
| Some y -> print_witness ppf y) f;
Format.fprintf ppf " }"
| WAbstract None ->
Format.fprintf ppf "Abstract(..)"
| WAbstract (Some s) ->
Format.fprintf ppf "Abstract(%s)" s
| WAbsent ->
Format.fprintf ppf "Absent"
let witness t =
if is_empty t then raise Not_found
else match (slot t).status with NEmpty w -> w | _ -> assert false
(*
let is_empty d =
(* let b1 = ClearlyEmpty.is_empty d in
......@@ -1144,6 +1226,99 @@ struct
end
module Cache = struct
let bool_pair f =
BoolPair.compute
~empty:false ~full:true
~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
~atom:f
let bool_rec f =
BoolRec.compute
~empty:false ~full:true
~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
~atom:f
let rec type_has_witness t = function (* Special case for empty, any ? *)
| WInt i -> Intervals.contains i t.ints
| WChar c -> Chars.contains c t.chars
| WAtom a -> Atoms.contains_sample a t.atoms
| WPair (w1,w2) ->
bool_pair (fun (n1,n2) ->
type_has_witness (descr n1) w1 &&
type_has_witness (descr n2) w2) t.times
| WXml (w1,w2) ->
bool_pair (fun (n1,n2) ->
type_has_witness (descr n1) w1 &&
type_has_witness (descr n2) w2) t.xml
| WFun f ->
bool_pair (fun (n1,n2) ->
let t1 = descr n1 and t2 = descr n2 in
List.for_all
(fun (x,y) ->
not (type_has_witness t1 x) ||
(match y with None -> false
| Some y -> type_has_witness t2 y))
f) t.arrow
| WRecord (f,o) ->
bool_rec (fun (o',f') ->
(not o || o') &&
(try LabelMap.iteri
(fun l w ->
try
let t = descr (LabelMap.assoc l f') in
if not (type_has_witness t w) then raise Exit
with Not_found -> if not o' then raise Exit
) f;
true
with Exit -> false)) t.record
| WAbsent -> t.absent
| WAbstract a -> Abstract.contains_sample a t.abstract
type 'a cache =
| Empty
| Type of t * 'a
| Split of witness * 'a cache * 'a cache
let rec find f t = function
| Empty ->
let r = f t in Type (t,r), r
| Split (w,yes,no) ->
if type_has_witness t w
then let yes,r = find f t yes in Split (w,yes,no), r
else let no,r = find f t no in Split (w,yes,no), r
| Type (s,rs) as c ->
try
let w = witness (diff t s) in
let rt = f t in
Split (w, Type (t,rt), c), rt
with Not_found -> try
let w = witness (diff s t) in
let rt = f t in
Split (w, c, Type (t,rt)), rt
with Not_found ->
c, rs
let emp = Empty