Commit 5d472f2b authored by Kim Nguyễn's avatar Kim Nguyễn

Remove the over-engineered iterators from types. Use the dispatch field to implement Iter.compute.

parent 9dfb61db
......@@ -350,7 +350,7 @@ sig
(** returns the union of all leaves in the BDD *)
val leafconj: t -> Atom.t
val get_kind : t -> (Var.t list * Var.t list * Atom.t option) list
val get_kind : t -> (Var.t list * Var.t list * Atom.t) list
val is_empty : t -> bool
val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
......@@ -436,18 +436,14 @@ struct
let rec split_vars l acc =
match l with
`Var v :: r -> split_vars r (v :: acc)
| [ `Atm a ] -> List.rev acc, Some a
| [] -> List.rev acc, None
| [ `Atm a ] -> List.rev acc, a
| [] -> List.rev acc, Atom.full
| _ -> assert false
in
List.map (fun (pos, neg) ->
let pos, atm = split_vars pos [] in
let neg = List.map (function `Var v -> v | _ -> assert false) neg in
let oatm = match atm with
Some a when T.equal a T.full -> None
| _ -> atm
in
(pos, neg, oatm)) (get t)
(pos, neg, atm)) (get t)
......
......@@ -40,7 +40,7 @@ sig
(** returns the union of all leaves in the BDD *)
val leafconj : t -> Atom.t
val get_kind : t -> (Var.t list * Var.t list * Atom.t option) list
val get_kind : t -> (Var.t list * Var.t list * Atom.t) list
val is_empty : t -> bool
val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ]
......
......@@ -1653,92 +1653,22 @@ module Iter =
DescrHash.add memo res res;
res
module type Ops = sig
type t
val cup : t list -> t
val cap : t list -> t
val neg : t -> t
val var : Var.t list * Var.t list -> t
val atoms : Atoms.t -> t
val ints : Intervals.t -> t
val chars : Chars.t -> t
val times : Pair.t -> t
val xml : Pair.t -> t
val arrow : Pair.t -> t
val record : Rec.t -> t
val abstract : Abstracts.t -> t
val absent : bool -> t
end
let any_pair = Pair.atom (any_node, any_node)
let any_record = Rec.atom (true,LabelMap.empty)
let any_arrow = Pair.atom (empty_node,any_node)
let compute_ops (type res) (module O : Ops with type t = res) t =
let compute ~default ?cup ?cap ?neg ?var ?atoms ?ints ?chars ?times
?xml ?arrow ?record ?abstract ?absent t
=
let t = simplify t in
let module P = struct
include O
let any_pair = Pair.atom (any_node, any_node)
let any_record = Rec.atom (true,LabelMap.empty)
let any_arrow = Pair.atom (empty_node,any_node)
let oatm cap any f x = match x with None -> f any | Some a -> f (cap a any)
let atoms = oatm Atoms.cap Atoms.full atoms
let ints = oatm Intervals.cap Intervals.full ints
let chars = oatm Chars.cap Chars.full chars
let times = oatm Pair.cap any_pair times
let xml = oatm Pair.cap any_pair xml
let arrow = oatm Pair.cap any_arrow arrow
let record = oatm Rec.cap any_record record
let abstract = oatm Abstracts.cap Abstracts.full abstract
end
in
let bdd (type atom) do_atom (module V : VarType with type Atom.t = atom) acc t
=
List.fold_left (fun acc (vpos, vneg, oatm) ->
let res = [(do_atom oatm) ; P.var (vpos, vneg)] in
(P.cap res) :: acc) acc V.(get_kind (proj t))
let mkatm (type a) (module V : VarType with type Atom.t = a) (any : a) f x =
f (V.Atom.cap (V.leafconj (V.proj x)) any)
in
let acc = [ P.absent (Descr.get_absent t) ] in
let acc = bdd P.atoms (module VarAtoms) acc t in
let acc = bdd P.ints (module VarIntervals) acc t in
let acc = bdd P.chars (module VarChars) acc t in
let acc = bdd P.times (module VarTimes) acc t in
let acc = bdd P.xml (module VarXml) acc t in
let acc = bdd P.arrow (module VarArrow) acc t in
let acc = bdd P.record (module VarRec) acc t in
let acc = bdd P.abstract (module VarAbstracts) acc t in
O.cup acc
let compute (type res) ~default
?cup ?cap ?neg ?var ?atoms ?ints ?chars ?times ?xml ?arrow ?record ?abstract ?absent
t =
let get f x = match f with None -> default | Some f -> f x in
let module O = struct
type t = res
let cup = get cup
let cap = get cap
let neg = get neg
let var (vpos, vneg) =
let var = get var in
cap ((List.map var vpos) @ (List.map (fun x -> neg (var x)) vneg))
let atoms = get atoms
let ints = get ints
let chars = get chars
let times = get times
let xml = get xml
let arrow = get arrow
let record = get record
let abstract = get abstract
let absent = get absent
end
let get f = match f with None -> fun _ -> default
| Some f -> fun x -> f x
in
compute_ops (module O : Ops with type t = res) t
let compute_deep ~default ?cup ?cap ?neg ?var ?atoms ?ints ?chars ?times ?xml ?arrow ?record ?abstract ?absent t =
let get f x = match f with None -> default | Some f -> f x in
let cup = get cup in
let cap = get cap in
let times = get times in
let xml = get xml in
let record = get record in
let neg = get neg in
let cup = get cup and cap = get cap and neg = get neg
and absent = get absent and var = get var in
let bdd (type bdd) (type atom)
do_atom
(module B : Bool.S with type t = bdd and type elem = atom)
......@@ -1753,13 +1683,36 @@ module Iter =
| l1, l2 -> cap (l1 @ List.map neg l2) :: acc
) [] (B.get bv))
in
compute ~default
~cup ~cap ~neg ~var:(get var) ~atoms:(get atoms) ~ints:(get ints) ~chars:(get chars)
~times:(bdd times (module Pair))
~xml:(bdd xml (module Pair))
~arrow:(bdd (get arrow) (module Pair))
~record:(bdd record (module Rec))
~abstract:(get abstract) ~absent:(get absent) t
let dispatch k t =
match k with
`atoms -> mkatm (module VarAtoms) Atoms.full (get atoms) t
| `intervals -> mkatm (module VarIntervals) Intervals.full (get ints) t
| `chars -> mkatm (module VarChars) Chars.full (get chars) t
| `abstracts ->
mkatm (module VarAbstracts) Abstracts.full (get abstract) t
| `times ->
mkatm (module VarTimes) any_pair (bdd (get times) (module Pair)) t
| `xml -> mkatm (module VarXml) any_pair (bdd (get xml) (module Pair)) t
| `arrow ->
mkatm (module VarArrow) any_arrow (bdd (get arrow) (module Pair)) t
| `record ->
mkatm (module VarRec) any_record (bdd (get record) (module Rec)) t
in
let bdd (module V : VarType) t acc =
List.fold_left (fun acc (vpos, vneg, atm) ->
let vpos = List.map var vpos in
let vneg = List.map (fun x -> neg (var x)) vneg in
let otype = V.inj (V.atom (`Atm atm)) in
let atm = dispatch V.kind otype in
(cap ((atm :: vpos) @ vneg)) :: acc
) acc
V.(get_kind (proj t))
in
let acc = [ absent (Descr.get_absent t) ] in
let acc = fold bdd t acc in
cup acc
end
......@@ -1784,7 +1737,7 @@ module Variable =
Not_found ->
DescrHash.add memo t empty3;
let res =
Iter.compute_deep ~default:empty3 ~cup:merge ~cap:merge
Iter.compute ~default:empty3 ~cup:merge ~cap:merge
~neg:(fun (a, b, c) -> (a , c , b))
~var:(fun v -> let e = Var.Set.singleton v in e,e,Var.Set.empty)
~times:prod ~xml:prod ~arrow:arrow ~record:record
......@@ -1816,7 +1769,7 @@ module Variable =
with
Not_found ->
DescrHash.add memo t ();
Iter.compute_deep ~default:()
Iter.compute ~default:()
~var:(fun _ -> raise Not_found)
~xml:prod ~times:prod ~arrow:prod ~record:record
t
......@@ -2236,7 +2189,7 @@ module Print = struct
if found_any then begin
(slot.def <- [Neg (alloc [])]; slot)
end else
let all_descrs = List.map (fun (vars, t) -> (vars, Iter.clean_type t))
let all_descrs = List.map (fun (vars, t) -> (vars, Iter.simplify t))
all_descrs
in
let merge_column_with (v1,t1) l =
......@@ -2746,7 +2699,7 @@ module Print = struct
let pair (n1, n2) =
nodes := NodeSet.add n1 (NodeSet.add n2 !nodes)
in
Iter.compute_deep ~default:()
Iter.compute ~default:()
~times:pair ~xml:pair ~arrow:pair ~record:(fun (_,lm) ->
LabelMap.iter (fun n -> nodes := NodeSet.add n !nodes) lm) t;
match NodeSet.elements !nodes with
......@@ -3107,43 +3060,21 @@ module Positive = struct
let var d = cons (`Variable d)
let neg v = cons (`Neg v)
let empty = ty empty
let default = empty
let any = ty any
let binop e f may_flat mk vl =
let has_f = ref false in
let vl = List.map (fun v ->
match may_flat v with
| Some vl -> vl
| None ->
if v == e then [] else if v == f then (has_f := true; [])
else [ v ]
) vl
in
if !has_f then f else
match List.concat vl with
[ v ] -> v
| vl -> mk vl
let cup = binop empty any
(function { def = `Cup (_::_ as vl) ; _ } -> Some vl | _ -> None)
(fun l -> cons (`Cup l))
let cap = binop any empty
(function { def = `Cap (_::_ as vl) ; _ } -> Some vl | _ -> None)
(fun l -> cons (`Cap l))
let cap l = cons (`Cap l)
let cup l = cons (`Cup l)
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2))
let interval i = ty (interval i)
let char c = ty (char c)
let atom a = ty (atom a)
let ints i = ty (interval i)
let chars c = ty (char c)
let atoms a = ty (atom a)
let abstract a = ty (abstract a)
let record b vlst = cons (`Record (b, vlst))
let define v1 v2 = def v1 (`Cup [v2])
let diff v1 v2 = cap [v1 ; (neg v2)]
let get_opt = function Some t -> t | None -> T.any
let decompose ?(stop=(fun _ -> None)) t =
let memo = DescrHash.create 17 in
let rec loop t =
......@@ -3165,12 +3096,8 @@ module Positive = struct
in
res.descr <- Some t; res
and loop_struct t =
Iter.compute_deep ~default:(cup[])
~cup ~cap ~neg ~var
~ints:interval
~chars:char
~atoms:atom
~abstract:abstract
Iter.compute ~default
~cup ~cap ~neg ~var ~ints ~chars ~atoms ~abstract
~xml:(fun (t1, t2) -> xml (loop (descr t1)) (loop (descr t2)))
~times:(fun (t1, t2) -> times (loop (descr t1)) (loop (descr t2)))
~arrow:(fun (t1, t2) -> arrow (loop (descr t1)) (loop (descr t2)))
......
......@@ -172,24 +172,6 @@ module Iter : sig
val map : ?abs:(bool -> bool) -> (var_type -> t -> t) -> t -> t
val iter : ?abs:(bool -> unit) ->(var_type -> t -> unit) -> t -> unit
val fold : ?abs:(bool -> 'a -> 'a) -> (var_type -> t -> 'a -> 'a) -> t -> 'a -> 'a
module type Ops = sig
type t
val cup : t list -> t
val cap : t list -> t
val neg : t -> t
val var : Var.t list * Var.t list -> t
val atoms : Atoms.t -> t
val ints : Intervals.t -> t
val chars : Chars.t -> t
val times : Pair.t -> t
val xml : Pair.t -> t
val arrow : Pair.t -> t
val record : Rec.t -> t
val abstract : Abstracts.t -> t
val absent : bool -> t
end
val compute_ops : (module Ops with type t = 'a) -> t -> 'a
end
(** Positive systems and least solutions **)
......
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