| `Previous_sibling
| `Stay ]
+module Move =
+ struct
+ type t = move
+ type 'a table = 'a array
+ let idx = function
+ | `First_child -> 0
+ | `Next_sibling -> 1
+ | `Parent -> 2
+ | `Previous_sibling -> 3
+ | `Stay -> 4
+ let ridx = function
+ | 0 -> `First_child
+ | 1 -> `Next_sibling
+ | 2 -> `Parent
+ | 3 -> `Previous_sibling
+ | 4 -> `Stay
+ | _ -> assert false
+
+ let create_table a = Array.make 5 a
+ let get m k = m.(idx k)
+ let set m k v = m.(idx k) <- v
+ let iter f m = Array.iteri (fun i v -> f (ridx i) v) m
+ let fold f m acc =
+ let acc = ref acc in
+ iter (fun i v -> acc := f i v !acc) m;
+ !acc
+ let for_all p m =
+ try
+ iter (fun i v -> if not (p i v) then raise Exit) m;
+ true
+ with
+ Exit -> false
+ let exists p m =
+ try
+ iter (fun i v -> if p i v then raise Exit) m;
+ false
+ with
+ Exit -> true
+ let print ppf m =
+ match m with
+ `First_child -> fprintf ppf "%s" Pretty.down_arrow
+ | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
+ | `Parent -> fprintf ppf "%s" Pretty.up_arrow
+ | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
+ | `Stay -> fprintf ppf "%s" Pretty.bullet
+
+ let print_table pr_e ppf m =
+ iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v;
+ if (idx i) < 4 then fprintf ppf ", ") m
+ end
+
type predicate = Move of move * State.t
| Is_first_child
| Is_next_sibling
let print ppf a =
match a.node with
- | Move (m, q) -> begin
- match m with
- `First_child -> fprintf ppf "%s" Pretty.down_arrow
- | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
- | `Parent -> fprintf ppf "%s" Pretty.up_arrow
- | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
- | `Stay -> fprintf ppf "%s" Pretty.bullet
- end;
- fprintf ppf "%a" State.print q
+ | Move (m, q) ->
+ fprintf ppf "%a%a" Move.print m State.print q
| Is_first_child -> fprintf ppf "%s?" Pretty.up_arrow
| Is_next_sibling -> fprintf ppf "%s?" Pretty.left_arrow
| Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k
let stay q = mk_move `Stay q
- let get_states phi =
- fold (fun phi acc ->
+ let get_states_by_move phi =
+ let table = Move.create_table StateSet.empty in
+ iter (fun phi ->
match expr phi with
- | Boolean.Atom ({ Atom.node = Move(_,q) ; _ }, _) -> StateSet.add q acc
- | _ -> acc
- ) phi StateSet.empty
+ | Boolean.Atom ({ Atom.node = Move(v,q) ; _ }, _) ->
+ let s = Move.get table v in
+ Move.set table v (StateSet.add q s)
+ | _ -> ()
+ ) phi;
+ table
+ let get_states phi =
+ let table = get_states_by_move phi in
+ Move.fold (fun _ s acc -> StateSet.union s acc) table StateSet.empty
end
-module Transition = Hcons.Make (struct
+module Transition =
+ struct
+ include Hcons.Make (struct
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
let hash (a, b, c) =
HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
end)
+ let print ppf t =
+ let q, l, f = t.node in
+ fprintf ppf "%a, %a %s %a"
+ State.print q
+ QNameSet.print l
+ Pretty.double_right_arrow
+ Formula.print f
+ end
module TransList : sig
transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
}
-
+let uid t = t.id
let get_states a = a.states
let get_starting_states a = a.starting_states
let get_selecting_states a = a.selecting_states
-let get_trans a tag states =
- StateSet.fold (fun q acc0 ->
- try
- let trs = Hashtbl.find a.transitions q in
- List.fold_left (fun acc1 (labs, phi) ->
- if QNameSet.mem tag labs then
- TransList.cons (Transition.make (q, labs, phi)) acc1
- else acc1) acc0 trs
- with Not_found -> acc0
- ) states TransList.nil
-
-
let _pr_buff = Buffer.create 50
let _str_fmt = formatter_of_buffer _pr_buff
Buffer.clear _pr_buff; s
let print fmt a =
+ let _ = _flush_str_fmt() in
fprintf fmt
"Internal UID: %i@\n\
States: %a@\n\
+ Number of states: %i@\n\
Starting states: %a@\n\
Selection states: %a@\n\
Alternating transitions:@\n"
(a.id :> int)
StateSet.print a.states
+ (StateSet.cardinal a.states)
StateSet.print a.starting_states
StateSet.print a.selecting_states;
let trs =
) strs_strings;
fprintf fmt "%s@\n" line
+
+let get_trans a tag states =
+ StateSet.fold (fun q acc0 ->
+ try
+ let trs = Hashtbl.find a.transitions q in
+ List.fold_left (fun acc1 (labs, phi) ->
+ if QNameSet.mem tag labs then
+ TransList.cons (Transition.make (q, labs, phi)) acc1
+ else acc1) acc0 trs
+ with Not_found -> acc0
+ ) states TransList.nil
+
+
+let get_form a tag q =
+ try
+ let trs = Hashtbl.find a.transitions q in
+ List.fold_left (fun aphi (labs, phi) ->
+ if QNameSet.mem tag labs then Formula.or_ aphi phi else aphi
+ ) Formula.false_ trs
+ with
+ Not_found -> Formula.false_
+
(*
[complete transitions a] ensures that for each state q
and each symbols s in the alphabet, a transition q, s exists.
StateSet.iter (fun q ->
if StateSet.mem q a.starting_states then ()
else
- let qtrans = try Hashtbl.find a.transitions q with Not_found -> eprintf "Not found here 226\n%!"; raise Not_found in
+ let qtrans = Hashtbl.find a.transitions q in
let rem =
List.fold_left (fun rem (labels, _) ->
QNameSet.diff rem labels) QNameSet.any qtrans
in
Hashtbl.add memo_state key nq; nq
in
- let trans = try Hashtbl.find auto.transitions q with Not_found -> eprintf "Not_found here 318\n%!"; [] in
+ let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in
let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
Hashtbl.replace auto.transitions q' trans';
done;
cleanup_states auto
+
+
+
module Builder =
struct
type auto = t
normalize_negations a;
a
end
+
+
+let map_set f s =
+ StateSet.fold (fun q a -> StateSet.add (f q) a) s StateSet.empty
+
+let map_hash fk fv h =
+ let h' = Hashtbl.create (Hashtbl.length h) in
+ let () = Hashtbl.iter (fun k v -> Hashtbl.add h' (fk k) (fv v)) h in
+ h'
+
+let rec map_form f phi =
+ match Formula.expr phi with
+ | Boolean.Or(phi1, phi2) -> Formula.or_ (map_form f phi1) (map_form f phi2)
+ | Boolean.And(phi1, phi2) -> Formula.and_ (map_form f phi1) (map_form f phi2)
+ | Boolean.Atom({ Atom.node = Move(m,q); _}, b) ->
+ let a = Formula.mk_atom (Move (m,f q)) in
+ if b then a else Formula.not_ a
+ | _ -> phi
+
+let rename_states mapper a =
+ let rename q = try Hashtbl.find mapper q with Not_found -> q in
+ { Builder.make () with
+ states = map_set rename a.states;
+ starting_states = map_set rename a.starting_states;
+ selecting_states = map_set rename a.selecting_states;
+ transitions =
+ map_hash
+ rename
+ (fun l ->
+ (List.map (fun (labels, form) -> (labels, map_form rename form)) l))
+ a.transitions;
+ }
+
+let copy a =
+ let mapper = Hashtbl.create MED_H_SIZE in
+ let () =
+ StateSet.iter (fun q -> Hashtbl.add mapper q (State.make())) a.states
+ in
+ rename_states mapper a
+
+
+let concat a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ let link_phi =
+ StateSet.fold
+ (fun q phi -> Formula.(or_ (stay q) phi))
+ a1.selecting_states Formula.false_
+ in
+ Hashtbl.iter (fun q trs -> Hashtbl.add a1.transitions q trs)
+ a2.transitions;
+ StateSet.iter
+ (fun q ->
+ Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)])
+ a2.starting_states;
+ { a1 with
+ states = StateSet.union a1.states a2.states;
+ selecting_states = a2.selecting_states;
+ transitions = a1.transitions;
+ }
+
+let merge a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ { a1 with
+ states = StateSet.union a1.states a2.states;
+ selecting_states = StateSet.union a1.selecting_states a2.selecting_states;
+ starting_states = StateSet.union a1.starting_states a2.starting_states;
+ transitions =
+ let () =
+ Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions
+ in
+ a1.transitions
+ }
+
+
+let link a1 a2 q link_phi =
+ { a1 with
+ states = StateSet.union a1.states a2.states;
+ selecting_states = StateSet.singleton q;
+ starting_states = StateSet.union a1.starting_states a2.starting_states;
+ transitions =
+ let () =
+ Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions
+ in
+ Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)];
+ a1.transitions
+ }
+
+let union a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ let q = State.make () in
+ let link_phi =
+ StateSet.fold
+ (fun q phi -> Formula.(or_ (stay q) phi))
+ (StateSet.union a1.selecting_states a2.selecting_states)
+ Formula.false_
+ in
+ link a1 a2 q link_phi
+
+let inter a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ let q = State.make () in
+ let link_phi =
+ StateSet.fold
+ (fun q phi -> Formula.(and_ (stay q) phi))
+ (StateSet.union a1.selecting_states a2.selecting_states)
+ Formula.true_
+ in
+ link a1 a2 q link_phi
+
+let neg a =
+ let a = copy a in
+ let q = State.make () in
+ let link_phi =
+ StateSet.fold
+ (fun q phi -> Formula.(and_ (not_(stay q)) phi))
+ a.selecting_states
+ Formula.true_
+ in
+ let () = Hashtbl.add a.transitions q [(QNameSet.any, link_phi)] in
+ let a =
+ { a with
+ selecting_states = StateSet.singleton q;
+ }
+ in
+ normalize_negations a; a
+
+let diff a1 a2 = inter a1 (neg a2)
+
projects / tatoo.git / blobdiff