<src/xpath/*.cmx>: for-pack(Xpath)
<src/xpath>: include
-<src/utils/*.cmx>: for-pack(Utils)
-<src/utils>: include
-
-<src/tree/*.cmx>: for-pack(Tree)
-<src/tree>: include
-
-<src/auto/*.cmx>: for-pack(Auto)
-<src/auto>: include
<src>: include
#Enable warning for all but generated files:
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:46:50 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+open Format
+
+type predicate = | First_child
+ | Next_sibling
+ | Parent
+ | Previous_sibling
+ | Stay
+ | Is_first_child
+ | Is_next_sibling
+ | Is of (Tree.NodeKind.t)
+ | Has_first_child
+ | Has_next_sibling
+
+let is_move p = match p with
+| First_child | Next_sibling
+| Parent | Previous_sibling | Stay -> true
+| _ -> false
+
+
+type atom = predicate * bool * State.t
+
+module Atom : (Formula.ATOM with type data = atom) =
+struct
+
+ module Node =
+ struct
+ type t = atom
+ let equal n1 n2 = n1 = n2
+ let hash n = Hashtbl.hash n
+ end
+
+ include Hcons.Make(Node)
+
+ let print ppf a =
+ let p, b, q = a.node in
+ if not b then fprintf ppf "%s" Pretty.lnot;
+ match p with
+ | First_child -> fprintf ppf "FC(%a)" State.print q
+ | Next_sibling -> fprintf ppf "NS(%a)" State.print q
+ | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q
+ | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q
+ | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q
+ | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse
+ | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse
+ | Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k
+ | Has_first_child -> fprintf ppf "FC?"
+ | Has_next_sibling -> fprintf ppf "NS?"
+
+ let neg a =
+ let p, b, q = a.node in
+ make (p, not b, q)
+
+
+end
+
+module SFormula =
+struct
+ include Formula.Make(Atom)
+ open Tree.NodeKind
+ let mk_atom a b c = atom_ (Atom.make (a,b,c))
+ let mk_kind k = mk_atom (Is k) true State.dummy
+ let has_first_child =
+ (mk_atom Has_first_child true State.dummy)
+
+ let has_next_sibling =
+ (mk_atom Has_next_sibling true State.dummy)
+
+ let is_first_child =
+ (mk_atom Is_first_child true State.dummy)
+
+ let is_next_sibling =
+ (mk_atom Is_next_sibling true State.dummy)
+
+ let is_attribute =
+ (mk_atom (Is Attribute) true State.dummy)
+
+ let is_element =
+ (mk_atom (Is Element) true State.dummy)
+
+ let is_processing_instruction =
+ (mk_atom (Is ProcessingInstruction) true State.dummy)
+
+ let is_comment =
+ (mk_atom (Is Comment) true State.dummy)
+
+ let first_child q =
+ and_
+ (mk_atom First_child true q)
+ has_first_child
+
+ let next_sibling q =
+ and_
+ (mk_atom Next_sibling true q)
+ has_next_sibling
+
+ let parent q =
+ and_
+ (mk_atom Parent true q)
+ is_first_child
+
+ let previous_sibling q =
+ and_
+ (mk_atom Previous_sibling true q)
+ is_next_sibling
+
+ let stay q =
+ (mk_atom Stay true q)
+
+ let get_states phi =
+ fold (fun phi acc ->
+ match expr phi with
+ | Formula.Atom a -> let _, _, q = Atom.node a in
+ if q != State.dummy then StateSet.add q acc else acc
+ | _ -> acc
+ ) phi StateSet.empty
+
+end
+
+
+module Transition = Hcons.Make (struct
+ type t = State.t * QNameSet.t * SFormula.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), ((SFormula.uid c) :> int))
+end)
+
+
+module TransList : sig
+ include Hlist.S with type elt = Transition.t
+ val print : Format.formatter -> ?sep:string -> t -> unit
+end =
+ struct
+ include Hlist.Make(Transition)
+ let print ppf ?(sep="\n") l =
+ iter (fun t ->
+ let q, lab, f = Transition.node t in
+ fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l
+ end
+
+
+type t = {
+ id : Uid.t;
+ mutable states : StateSet.t;
+ mutable selection_states: StateSet.t;
+ transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+ mutable cache2 : TransList.t Cache.N2.t;
+ mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+}
+
+let next = Uid.make_maker ()
+
+let dummy2 = TransList.cons
+ (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
+ TransList.nil
+
+let dummy6 = (dummy2, StateSet.empty)
+
+
+let create s ss = { id = next ();
+ states = s;
+ selection_states = ss;
+ transitions = Hashtbl.create 17;
+ cache2 = Cache.N2.create dummy2;
+ cache6 = Cache.N6.create dummy6;
+ }
+
+let reset a =
+ a.cache2 <- Cache.N2.create dummy2;
+ a.cache6 <- Cache.N6.create dummy6
+
+
+let get_trans_aux 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_trans a tag states =
+ let trs =
+ Cache.N2.find a.cache2
+ (tag.QName.id :> int) (states.StateSet.id :> int)
+ in
+ if trs == dummy2 then
+ let trs = get_trans_aux a tag states in
+ (Cache.N2.add
+ a.cache2
+ (tag.QName.id :> int)
+ (states.StateSet.id :> int) trs; trs)
+ else trs
+
+
+
+let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind =
+ let rec loop phi =
+ begin match SFormula.expr phi with
+ Formula.True -> true
+ | Formula.False -> false
+ | Formula.Atom a ->
+ let p, b, q = Atom.node a in
+ let pos =
+ match p with
+ | First_child -> StateSet.mem q fcs
+ | Next_sibling -> StateSet.mem q nss
+ | Parent | Previous_sibling -> StateSet.mem q ps
+ | Stay -> StateSet.mem q ss
+ | Is_first_child -> is_left
+ | Is_next_sibling -> is_right
+ | Is k -> k == kind
+ | Has_first_child -> has_left
+ | Has_next_sibling -> has_right
+ in
+ if is_move p && (not b) then
+ eprintf "Warning: Invalid negative atom %a" Atom.print a;
+ b == pos
+ | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
+ | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
+ end
+ in
+ loop phi
+
+let int_of_conf is_left is_right has_left has_right kind =
+ ((Obj.magic kind) lsl 4) lor
+ ((Obj.magic is_left) lsl 3) lor
+ ((Obj.magic is_right) lsl 2) lor
+ ((Obj.magic has_left) lsl 1) lor
+ (Obj.magic has_right)
+
+let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind =
+ let i = int_of_conf is_left is_right has_left has_right kind
+ and k = (fcs.StateSet.id :> int)
+ and l = (nss.StateSet.id :> int)
+ and m = (ps.StateSet.id :> int)
+ in
+
+ let rec loop ltrs ss =
+ let j = (ltrs.TransList.id :> int)
+ and n = (ss.StateSet.id :> int) in
+ let (new_ltrs, new_ss) as res =
+ let res = Cache.N6.find auto.cache6 i j k l m n in
+ if res == dummy6 then
+ let res =
+ TransList.fold (fun trs (acct, accs) ->
+ let q, _, phi = Transition.node trs in
+ if StateSet.mem q accs then (acct, accs) else
+ if eval_form
+ phi fcs nss ps accs
+ is_left is_right has_left has_right kind
+ then
+ (acct, StateSet.add q accs)
+ else
+ (TransList.cons trs acct, accs)
+ ) ltrs (TransList.nil, ss)
+ in
+ Cache.N6.add auto.cache6 i j k l m n res; res
+ else
+ res
+ in
+ if new_ss == ss then res else
+ loop new_ltrs new_ss
+ in
+ loop ltrs ss
+
+
+
+
+
+(*
+ [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
+ automaton [a] but ensures that transitions remains pairwise disjoint
+*)
+
+let add_trans a q s f =
+ let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+ let cup, ntrs =
+ List.fold_left (fun (acup, atrs) (labs, phi) ->
+ let lab1 = QNameSet.inter labs s in
+ let lab2 = QNameSet.diff labs s in
+ let tr1 =
+ if QNameSet.is_empty lab1 then []
+ else [ (lab1, SFormula.or_ phi f) ]
+ in
+ let tr2 =
+ if QNameSet.is_empty lab2 then []
+ else [ (lab2, SFormula.or_ phi f) ]
+ in
+ (QNameSet.union acup labs, tr1@ tr2 @ atrs)
+ ) (QNameSet.empty, []) trs
+ in
+ let rem = QNameSet.diff s cup in
+ let ntrs = if QNameSet.is_empty rem then ntrs
+ else (rem, f) :: ntrs
+ in
+ Hashtbl.replace a.transitions q ntrs
+
+let _pr_buff = Buffer.create 50
+let _str_fmt = formatter_of_buffer _pr_buff
+let _flush_str_fmt () = pp_print_flush _str_fmt ();
+ let s = Buffer.contents _pr_buff in
+ Buffer.clear _pr_buff; s
+
+let print fmt a =
+ fprintf fmt
+ "\nInternal UID: %i@\n\
+ States: %a@\n\
+ Selection states: %a@\n\
+ Alternating transitions:@\n"
+ (a.id :> int)
+ StateSet.print a.states
+ StateSet.print a.selection_states;
+ let trs =
+ Hashtbl.fold
+ (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
+ a.transitions
+ []
+ in
+ let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
+ let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+ trs
+ in
+ let _ = _flush_str_fmt () in
+ let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+ let s1 = State.print _str_fmt q; _flush_str_fmt () in
+ let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
+ let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in
+ let pre = Pretty.length s1 + Pretty.length s2 in
+ let all = Pretty.length s3 in
+ ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+ ) ([], 0, 0) sorted_trs
+ in
+ let line = Pretty.line (max_all + max_pre + 6) in
+ let prev_q = ref State.dummy in
+ List.iter (fun (q, s1, s2, s3) ->
+ if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line;
+ prev_q := q;
+ fprintf fmt " %s, %s" s1 s2;
+ fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+ fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3;
+ ) strs_strings;
+ fprintf fmt " %s\n%!" line
+
+(*
+ [complete transitions a] ensures that for each state q
+ and each symbols s in the alphabet, a transition q, s exists.
+ (adding q, s -> F when necessary).
+*)
+
+let complete_transitions a =
+ StateSet.iter (fun q ->
+ let qtrans = Hashtbl.find a.transitions q in
+ let rem =
+ List.fold_left (fun rem (labels, _) ->
+ QNameSet.diff rem labels) QNameSet.any qtrans
+ in
+ let nqtrans =
+ if QNameSet.is_empty rem then qtrans
+ else
+ (rem, SFormula.false_) :: qtrans
+ in
+ Hashtbl.replace a.transitions q nqtrans
+ ) a.states
+
+let cleanup_states a =
+ let memo = ref StateSet.empty in
+ let rec loop q =
+ if not (StateSet.mem q !memo) then begin
+ memo := StateSet.add q !memo;
+ let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+ List.iter (fun (_, phi) ->
+ StateSet.iter loop (SFormula.get_states phi)) trs
+ end
+ in
+ StateSet.iter loop a.selection_states;
+ let unused = StateSet.diff a.states !memo in
+ eprintf "Unused states %a\n%!" StateSet.print unused;
+ StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
+ a.states <- !memo
+
+(* [normalize_negations a] removes negative atoms in the formula
+ complementing the sub-automaton in the negative states.
+ [TODO check the meaning of negative upward arrows]
+*)
+
+let normalize_negations auto =
+ eprintf "Automaton before normalize_trans:\n";
+ print err_formatter auto;
+ eprintf "--------------------\n%!";
+
+ let memo_state = Hashtbl.create 17 in
+ let todo = Queue.create () in
+ let rec flip b f =
+ match SFormula.expr f with
+ Formula.True | Formula.False -> if b then f else SFormula.not_ f
+ | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
+ | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
+ | Formula.Atom(a) -> begin
+ let l, b', q = Atom.node a in
+ if q == State.dummy then if b then f else SFormula.not_ f
+ else
+ if b == b' then begin
+ (* a appears positively, either no negation or double negation *)
+ if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
+ SFormula.atom_ (Atom.make (l, true, q))
+ end else begin
+ (* need to reverse the atom
+ either we have a positive state deep below a negation
+ or we have a negative state in a positive formula
+ b' = sign of the state
+ b = sign of the enclosing formula
+ *)
+ let not_q =
+ try
+ (* does the inverted state of q exist ? *)
+ Hashtbl.find memo_state (q, false)
+ with
+ Not_found ->
+ (* create a new state and add it to the todo queue *)
+ let nq = State.make () in
+ auto.states <- StateSet.add nq auto.states;
+ Hashtbl.add memo_state (q, false) nq;
+ Queue.add (q, false) todo; nq
+ in
+ SFormula.atom_ (Atom.make (l, true, not_q))
+ end
+ end
+ in
+ (* states that are not reachable from a selection stat are not interesting *)
+ StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states;
+
+ while not (Queue.is_empty todo) do
+ let (q, b) as key = Queue.pop todo in
+ let q' =
+ try
+ Hashtbl.find memo_state key
+ with
+ Not_found ->
+ let nq = if b then q else
+ let nq = State.make () in
+ auto.states <- StateSet.add nq auto.states;
+ nq
+ in
+ Hashtbl.add memo_state key nq; nq
+ in
+ let trans = Hashtbl.find auto.transitions q in
+ let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
+ Hashtbl.replace auto.transitions q' trans';
+ done;
+ cleanup_states auto
+
+
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:42:38 CEST by Kim Nguyen>
+*)
+
+type predicate =
+ First_child
+ | Next_sibling
+ | Parent
+ | Previous_sibling
+ | Stay
+ | Is_first_child
+ | Is_next_sibling
+ | Is of Tree.NodeKind.t
+ | Has_first_child
+ | Has_next_sibling
+
+val is_move : predicate -> bool
+
+type atom = predicate * bool * State.t
+
+module Atom : Formula.ATOM with type data = atom
+
+module SFormula :
+ sig
+ include module type of Formula.Make(Atom)
+ val mk_atom : predicate -> bool -> State.t -> t
+ val mk_kind : Tree.NodeKind.t -> t
+ val has_first_child : t
+ val has_next_sibling : t
+ val is_first_child : t
+ val is_next_sibling : t
+ val is_attribute : t
+ val is_element : t
+ val is_processing_instruction : t
+ val is_comment : t
+ val first_child : State.t -> t
+ val next_sibling : State.t -> t
+ val parent : State.t -> t
+ val previous_sibling : State.t -> t
+ val stay : State.t -> t
+ val get_states : t -> StateSet.t
+ end
+
+
+module Transition : Hcons.S with
+ type data = State.t * QNameSet.t * SFormula.t
+
+module TransList : sig
+ include Hlist.S with type elt = Transition.t
+ val print : Format.formatter -> ?sep:string -> t -> unit
+end
+
+
+type t = private {
+ id : Uid.t;
+ mutable states : StateSet.t;
+ mutable selection_states: StateSet.t;
+ transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+ mutable cache2 : TransList.t Cache.N2.t;
+ mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+}
+
+
+
+val create : StateSet.t -> StateSet.t -> t
+val reset : t -> unit
+val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
+
+val eval_trans : t -> TransList.t
+ -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
+ -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
+ -> TransList.t*StateSet.t
+
+val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
+val print : Format.formatter -> t -> unit
+val complete_transitions : t -> unit
+val cleanup_states : t -> unit
+val normalize_negations : t -> unit
+++ /dev/null
-auto/Ata
-auto/Formula
-auto/Eval
-auto/State
-auto/StateSet
-auto/Html
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-15 18:18:11 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-open Format
-open Utils
-
-type predicate = | First_child
- | Next_sibling
- | Parent
- | Previous_sibling
- | Stay
- | Is_first_child
- | Is_next_sibling
- | Is of (Tree.Common.NodeKind.t)
- | Has_first_child
- | Has_next_sibling
-
-let is_move p = match p with
-| First_child | Next_sibling
-| Parent | Previous_sibling | Stay -> true
-| _ -> false
-
-
-type atom = predicate * bool * State.t
-
-module Atom : (Formula.ATOM with type data = atom) =
-struct
-
- module Node =
- struct
- type t = atom
- let equal n1 n2 = n1 = n2
- let hash n = Hashtbl.hash n
- end
-
- include Hcons.Make(Node)
-
- let print ppf a =
- let p, b, q = a.node in
- if not b then fprintf ppf "%s" Pretty.lnot;
- match p with
- | First_child -> fprintf ppf "FC(%a)" State.print q
- | Next_sibling -> fprintf ppf "NS(%a)" State.print q
- | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q
- | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q
- | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q
- | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse
- | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse
- | Is k -> fprintf ppf "is-%a?" Tree.Common.NodeKind.print k
- | Has_first_child -> fprintf ppf "FC?"
- | Has_next_sibling -> fprintf ppf "NS?"
-
- let neg a =
- let p, b, q = a.node in
- make (p, not b, q)
-
-
-end
-
-module SFormula =
-struct
- include Formula.Make(Atom)
- open Tree.Common.NodeKind
- let mk_atom a b c = atom_ (Atom.make (a,b,c))
- let mk_kind k = mk_atom (Is k) true State.dummy
- let has_first_child =
- (mk_atom Has_first_child true State.dummy)
-
- let has_next_sibling =
- (mk_atom Has_next_sibling true State.dummy)
-
- let is_first_child =
- (mk_atom Is_first_child true State.dummy)
-
- let is_next_sibling =
- (mk_atom Is_next_sibling true State.dummy)
-
- let is_attribute =
- (mk_atom (Is Attribute) true State.dummy)
-
- let is_element =
- (mk_atom (Is Element) true State.dummy)
-
- let is_processing_instruction =
- (mk_atom (Is ProcessingInstruction) true State.dummy)
-
- let is_comment =
- (mk_atom (Is Comment) true State.dummy)
-
- let first_child q =
- and_
- (mk_atom First_child true q)
- has_first_child
-
- let next_sibling q =
- and_
- (mk_atom Next_sibling true q)
- has_next_sibling
-
- let parent q =
- and_
- (mk_atom Parent true q)
- is_first_child
-
- let previous_sibling q =
- and_
- (mk_atom Previous_sibling true q)
- is_next_sibling
-
- let stay q =
- (mk_atom Stay true q)
-
- let get_states phi =
- fold (fun phi acc ->
- match expr phi with
- | Formula.Atom a -> let _, _, q = Atom.node a in
- if q != State.dummy then StateSet.add q acc else acc
- | _ -> acc
- ) phi StateSet.empty
-
-end
-
-
-module Transition = Hcons.Make (struct
- type t = State.t * QNameSet.t * SFormula.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), ((SFormula.uid c) :> int))
-end)
-
-
-module TransList : sig
- include Hlist.S with type elt = Transition.t
- val print : Format.formatter -> ?sep:string -> t -> unit
-end =
- struct
- include Hlist.Make(Transition)
- let print ppf ?(sep="\n") l =
- iter (fun t ->
- let q, lab, f = Transition.node t in
- fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l
- end
-
-
-type t = {
- id : Uid.t;
- mutable states : StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
- mutable cache2 : TransList.t Cache.N2.t;
- mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
-}
-
-let next = Uid.make_maker ()
-
-let dummy2 = TransList.cons
- (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
- TransList.nil
-
-let dummy6 = (dummy2, StateSet.empty)
-
-
-let create s ss = { id = next ();
- states = s;
- selection_states = ss;
- transitions = Hashtbl.create 17;
- cache2 = Cache.N2.create dummy2;
- cache6 = Cache.N6.create dummy6;
- }
-
-let reset a =
- a.cache2 <- Cache.N2.create dummy2;
- a.cache6 <- Cache.N6.create dummy6
-
-
-let get_trans_aux 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_trans a tag states =
- let trs =
- Cache.N2.find a.cache2
- (tag.QName.id :> int) (states.StateSet.id :> int)
- in
- if trs == dummy2 then
- let trs = get_trans_aux a tag states in
- (Cache.N2.add
- a.cache2
- (tag.QName.id :> int)
- (states.StateSet.id :> int) trs; trs)
- else trs
-
-
-
-let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind =
- let rec loop phi =
- begin match SFormula.expr phi with
- Formula.True -> true
- | Formula.False -> false
- | Formula.Atom a ->
- let p, b, q = Atom.node a in
- let pos =
- match p with
- | First_child -> StateSet.mem q fcs
- | Next_sibling -> StateSet.mem q nss
- | Parent | Previous_sibling -> StateSet.mem q ps
- | Stay -> StateSet.mem q ss
- | Is_first_child -> is_left
- | Is_next_sibling -> is_right
- | Is k -> k == kind
- | Has_first_child -> has_left
- | Has_next_sibling -> has_right
- in
- if is_move p && (not b) then
- eprintf "Warning: Invalid negative atom %a" Atom.print a;
- b == pos
- | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
- | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
- end
- in
- loop phi
-
-let int_of_conf is_left is_right has_left has_right kind =
- ((Obj.magic kind) lsl 4) lor
- ((Obj.magic is_left) lsl 3) lor
- ((Obj.magic is_right) lsl 2) lor
- ((Obj.magic has_left) lsl 1) lor
- (Obj.magic has_right)
-
-let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind =
- let i = int_of_conf is_left is_right has_left has_right kind
- and k = (fcs.StateSet.id :> int)
- and l = (nss.StateSet.id :> int)
- and m = (ps.StateSet.id :> int)
- in
-
- let rec loop ltrs ss =
- let j = (ltrs.TransList.id :> int)
- and n = (ss.StateSet.id :> int) in
- let (new_ltrs, new_ss) as res =
- let res = Cache.N6.find auto.cache6 i j k l m n in
- if res == dummy6 then
- let res =
- TransList.fold (fun trs (acct, accs) ->
- let q, _, phi = Transition.node trs in
- if StateSet.mem q accs then (acct, accs) else
- if eval_form
- phi fcs nss ps accs
- is_left is_right has_left has_right kind
- then
- (acct, StateSet.add q accs)
- else
- (TransList.cons trs acct, accs)
- ) ltrs (TransList.nil, ss)
- in
- Cache.N6.add auto.cache6 i j k l m n res; res
- else
- res
- in
- if new_ss == ss then res else
- loop new_ltrs new_ss
- in
- loop ltrs ss
-
-
-
-
-
-(*
- [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
- automaton [a] but ensures that transitions remains pairwise disjoint
-*)
-
-let add_trans a q s f =
- let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
- let cup, ntrs =
- List.fold_left (fun (acup, atrs) (labs, phi) ->
- let lab1 = QNameSet.inter labs s in
- let lab2 = QNameSet.diff labs s in
- let tr1 =
- if QNameSet.is_empty lab1 then []
- else [ (lab1, SFormula.or_ phi f) ]
- in
- let tr2 =
- if QNameSet.is_empty lab2 then []
- else [ (lab2, SFormula.or_ phi f) ]
- in
- (QNameSet.union acup labs, tr1@ tr2 @ atrs)
- ) (QNameSet.empty, []) trs
- in
- let rem = QNameSet.diff s cup in
- let ntrs = if QNameSet.is_empty rem then ntrs
- else (rem, f) :: ntrs
- in
- Hashtbl.replace a.transitions q ntrs
-
-let _pr_buff = Buffer.create 50
-let _str_fmt = formatter_of_buffer _pr_buff
-let _flush_str_fmt () = pp_print_flush _str_fmt ();
- let s = Buffer.contents _pr_buff in
- Buffer.clear _pr_buff; s
-
-let print fmt a =
- fprintf fmt
- "\nInternal UID: %i@\n\
- States: %a@\n\
- Selection states: %a@\n\
- Alternating transitions:@\n"
- (a.id :> int)
- StateSet.print a.states
- StateSet.print a.selection_states;
- let trs =
- Hashtbl.fold
- (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
- a.transitions
- []
- in
- let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
- let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
- trs
- in
- let _ = _flush_str_fmt () in
- let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
- let s1 = State.print _str_fmt q; _flush_str_fmt () in
- let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
- let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in
- let pre = Pretty.length s1 + Pretty.length s2 in
- let all = Pretty.length s3 in
- ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
- ) ([], 0, 0) sorted_trs
- in
- let line = Pretty.line (max_all + max_pre + 6) in
- let prev_q = ref State.dummy in
- List.iter (fun (q, s1, s2, s3) ->
- if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line;
- prev_q := q;
- fprintf fmt " %s, %s" s1 s2;
- fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
- fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3;
- ) strs_strings;
- fprintf fmt " %s\n%!" line
-
-(*
- [complete transitions a] ensures that for each state q
- and each symbols s in the alphabet, a transition q, s exists.
- (adding q, s -> F when necessary).
-*)
-
-let complete_transitions a =
- StateSet.iter (fun q ->
- let qtrans = Hashtbl.find a.transitions q in
- let rem =
- List.fold_left (fun rem (labels, _) ->
- QNameSet.diff rem labels) QNameSet.any qtrans
- in
- let nqtrans =
- if QNameSet.is_empty rem then qtrans
- else
- (rem, SFormula.false_) :: qtrans
- in
- Hashtbl.replace a.transitions q nqtrans
- ) a.states
-
-let cleanup_states a =
- let memo = ref StateSet.empty in
- let rec loop q =
- if not (StateSet.mem q !memo) then begin
- memo := StateSet.add q !memo;
- let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
- List.iter (fun (_, phi) ->
- StateSet.iter loop (SFormula.get_states phi)) trs
- end
- in
- StateSet.iter loop a.selection_states;
- let unused = StateSet.diff a.states !memo in
- eprintf "Unused states %a\n%!" StateSet.print unused;
- StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
- a.states <- !memo
-
-(* [normalize_negations a] removes negative atoms in the formula
- complementing the sub-automaton in the negative states.
- [TODO check the meaning of negative upward arrows]
-*)
-
-let normalize_negations auto =
- eprintf "Automaton before normalize_trans:\n";
- print err_formatter auto;
- eprintf "--------------------\n%!";
-
- let memo_state = Hashtbl.create 17 in
- let todo = Queue.create () in
- let rec flip b f =
- match SFormula.expr f with
- Formula.True | Formula.False -> if b then f else SFormula.not_ f
- | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
- | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
- | Formula.Atom(a) -> begin
- let l, b', q = Atom.node a in
- if q == State.dummy then if b then f else SFormula.not_ f
- else
- if b == b' then begin
- (* a appears positively, either no negation or double negation *)
- if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
- SFormula.atom_ (Atom.make (l, true, q))
- end else begin
- (* need to reverse the atom
- either we have a positive state deep below a negation
- or we have a negative state in a positive formula
- b' = sign of the state
- b = sign of the enclosing formula
- *)
- let not_q =
- try
- (* does the inverted state of q exist ? *)
- Hashtbl.find memo_state (q, false)
- with
- Not_found ->
- (* create a new state and add it to the todo queue *)
- let nq = State.make () in
- auto.states <- StateSet.add nq auto.states;
- Hashtbl.add memo_state (q, false) nq;
- Queue.add (q, false) todo; nq
- in
- SFormula.atom_ (Atom.make (l, true, not_q))
- end
- end
- in
- (* states that are not reachable from a selection stat are not interesting *)
- StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states;
-
- while not (Queue.is_empty todo) do
- let (q, b) as key = Queue.pop todo in
- let q' =
- try
- Hashtbl.find memo_state key
- with
- Not_found ->
- let nq = if b then q else
- let nq = State.make () in
- auto.states <- StateSet.add nq auto.states;
- nq
- in
- Hashtbl.add memo_state key nq; nq
- in
- let trans = Hashtbl.find auto.transitions q in
- let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
- Hashtbl.replace auto.transitions q' trans';
- done;
- cleanup_states auto
-
-
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-15 18:18:23 CET by Kim Nguyen>
-*)
-
-type predicate =
- First_child
- | Next_sibling
- | Parent
- | Previous_sibling
- | Stay
- | Is_first_child
- | Is_next_sibling
- | Is of Tree.Common.NodeKind.t
- | Has_first_child
- | Has_next_sibling
-
-val is_move : predicate -> bool
-
-type atom = predicate * bool * State.t
-
-module Atom : Formula.ATOM with type data = atom
-
-module SFormula :
- sig
- include module type of Formula.Make(Atom)
- val mk_atom : predicate -> bool -> State.t -> t
- val mk_kind : Tree.Common.NodeKind.t -> t
- val has_first_child : t
- val has_next_sibling : t
- val is_first_child : t
- val is_next_sibling : t
- val is_attribute : t
- val is_element : t
- val is_processing_instruction : t
- val is_comment : t
- val first_child : State.t -> t
- val next_sibling : State.t -> t
- val parent : State.t -> t
- val previous_sibling : State.t -> t
- val stay : State.t -> t
- val get_states : t -> StateSet.t
- end
-
-
-module Transition : Utils.Hcons.S with
- type data = State.t * Utils.QNameSet.t * SFormula.t
-
-module TransList : sig
- include Utils.Hlist.S with type elt = Transition.t
- val print : Format.formatter -> ?sep:string -> t -> unit
-end
-
-
-type t = private {
- id : Utils.Uid.t;
- mutable states : StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (Utils.QNameSet.t*SFormula.t) list) Hashtbl.t;
- mutable cache2 : TransList.t Utils.Cache.N2.t;
- mutable cache6 : (TransList.t*StateSet.t) Utils.Cache.N6.t;
-}
-
-
-
-val create : StateSet.t -> StateSet.t -> t
-val reset : t -> unit
-val get_trans : t -> Utils.QNameSet.elt -> StateSet.t -> TransList.t
-
-val eval_trans : t -> TransList.t
- -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
- -> bool -> bool -> bool -> bool -> Tree.Common.NodeKind.t
- -> TransList.t*StateSet.t
-
-val add_trans : t -> State.t -> Utils.QNameSet.t -> SFormula.t -> unit
-val print : Format.formatter -> t -> unit
-val complete_transitions : t -> unit
-val cleanup_states : t -> unit
-val normalize_negations : t -> unit
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-15 18:32:22 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-open Format
-open Utils
-
-module Make (T : Tree.Sig.S) :
- sig
- val eval : Ata.t -> T.t -> T.node -> T.node list
- end
- = struct
-
-
-IFDEF HTMLTRACE
- THEN
-DEFINE TRACE(e) = (e)
- ELSE
-DEFINE TRACE(e) = ()
-END
-
-
-
- type cache = StateSet.t Cache.N1.t
- let get c t n = Cache.N1.find c (T.preorder t n)
-
- let set c t n v = Cache.N1.add c (T.preorder t n) v
-
-
- let top_down_run auto tree node cache _i =
- let redo = ref false in
- let rec loop node =
- if node != T.nil then begin
- let parent = T.parent tree node in
- let fc = T.first_child tree node in
- let ns = T.next_sibling tree node in
- let tag = T.tag tree node in
- let states0 = get cache tree node in
- let trans0 = Ata.get_trans auto tag auto.Ata.states in
- let () =
- TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a<br/>Pre Trans: %a<br/>"
- StateSet.print states0 (Ata.TransList.print ~sep:"<br/>") trans0)
- in
- let ps = get cache tree parent in
- let fcs = get cache tree fc in
- let nss = get cache tree ns in
- let is_left = node == T.first_child tree parent
- and is_right = node == T.next_sibling tree parent
- and has_left = fc != T.nil
- and has_right = ns != T.nil
- and kind = T.kind tree node
- in
- let trans1, states1 =
- Ata.eval_trans auto trans0
- fcs nss ps states0
- is_left is_right has_left has_right kind
- in
- let () =
- TRACE(Html.trace (T.preorder tree node) _i "TD States: %a<br/>TD Trans: %a<br/>" StateSet.print states1 (Ata.TransList.print ~sep:"<br/>") trans1)
- in
- if states1 != states0 then set cache tree node states1;
- let () = loop fc in
- let fcs1 = get cache tree fc in
- let trans2, states2 =
- Ata.eval_trans auto trans1
- fcs1 nss ps states1
- is_left is_right has_left has_right kind
- in
- let () =
- TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a<br/>Left BU Trans: %a<br/>" StateSet.print states2 (Ata.TransList.print ~sep:"<br/>") trans2)
- in
- if states2 != states1 then set cache tree node states2;
- let () = loop ns in
- let _trans3, states3 =
- Ata.eval_trans auto trans2
- fcs1 (get cache tree ns) ps states2
- is_left is_right has_left has_right kind
- in
- let () =
- TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a<br/>Right BU Trans: %a<br/>" StateSet.print states3 (Ata.TransList.print ~sep:"<br/>") _trans3)
- in
- if states3 != states2 then set cache tree node states3;
- if states0 != states3 && (not !redo) then redo := true
- end
- in
- loop node;
- !redo
-
- let get_results auto tree node cache =
- let rec loop node acc =
- if node == T.nil then acc
- else
- let acc0 = loop (T.next_sibling tree node) acc in
- let acc1 = loop (T.first_child tree node) acc0 in
-
- if StateSet.intersect (get cache tree node) auto.Ata.selection_states then
- node::acc1
- else
- acc1
- in
- loop node []
-
- let eval auto tree node =
- let cache = Cache.N1.create StateSet.empty in
- let redo = ref true in
- let iter = ref 0 in
- Ata.reset auto;
- while !redo do
- redo := top_down_run auto tree node cache !iter;
- incr iter;
- done;
- let r = get_results auto tree node cache in
- TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree));
- r
-
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 11:16:29 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-open Format
-open Utils
-
-(*
-
-(** Implementation of hashconsed Boolean formulae *)
-
-*)
-module type ATOM =
-sig
- type t
- val neg : t -> t
- include Hcons.Abstract with type t := t
- include Common_sig.Printable with type t := t
-end
-
-type ('formula,'atom) expr =
- | False
- | True
- | Or of 'formula * 'formula
- | And of 'formula * 'formula
- | Atom of 'atom
-
-module Make (P: ATOM) =
-struct
-
-
- type 'hcons node = {
- pos : ('hcons,P.t) expr;
- mutable neg : 'hcons;
- }
-
- external hash_const_variant : [> ] -> int = "%identity"
- external vb : bool -> int = "%identity"
-
- module rec Node : Hcons.S
- with type data = Data.t = Hcons.Make (Data)
- and Data : Common_sig.HashedType with type t = Node.t node =
- struct
- type t = Node.t node
- let equal x y =
- match x.pos, y.pos with
- | a,b when a == b -> true
- | Or(xf1, xf2), Or(yf1, yf2)
- | And(xf1, xf2), And(yf1,yf2) -> xf1 == yf1 && xf2 == yf2
- | Atom(p1), Atom(p2) -> p1 == p2
- | _ -> false
-
- let hash f =
- match f.pos with
- | False -> 0
- | True -> 1
- | Or (f1, f2) ->
- HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
- | And (f1, f2) ->
- HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
- | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p))
- end
-
- type t = Node.t
- let hash x = x.Node.hash
- let uid x = x.Node.id
- let equal = Node.equal
- let expr f = f.Node.node.pos
-
- let compare f1 f2 = compare f1.Node.id f2.Node.id
- let prio f =
- match expr f with
- | True | False -> 10
- | Atom _ -> 8
- | And _ -> 6
- | Or _ -> 1
-
- let rec print ?(parent=false) ppf f =
- if parent then fprintf ppf "(";
- let _ = match expr f with
- | True -> fprintf ppf "%s" Pretty.top
- | False -> fprintf ppf "%s" Pretty.bottom
- | And(f1,f2) ->
- print ~parent:(prio f > prio f1) ppf f1;
- fprintf ppf " %s " Pretty.wedge;
- print ~parent:(prio f > prio f2) ppf f2;
- | Or(f1,f2) ->
- (print ppf f1);
- fprintf ppf " %s " Pretty.vee;
- (print ppf f2);
- | Atom(p) -> fprintf ppf "%a" P.print p
-(* let _ = flush_str_formatter() in
- let fmt = str_formatter in
- let a_str, d_str =
- match dir with
- | `Left -> Pretty.down_arrow, Pretty.subscript 1
- | `Right -> Pretty.down_arrow, Pretty.subscript 2
- | `Epsilon -> Pretty.epsilon, ""
- | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
- | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
- in
- fprintf fmt "%s%s" a_str d_str;
- State.print fmt s;
- let str = flush_str_formatter() in
- if b then fprintf ppf "%s" str
- else Pretty.pp_overline ppf str *)
- in
- if parent then fprintf ppf ")"
-
-let print ppf f = print ~parent:false ppf f
-
-let is_true f = (expr f) == True
-let is_false f = (expr f) == False
-
-
-let cons pos neg =
- let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
- let pnode = Node.make { pos = pos; neg = nnode } in
- (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
- account for hashing ! *)
- pnode,nnode
-
-
-let true_,false_ = cons True False
-
-let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
-
-let not_ f = f.Node.node.neg
-
-let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
-
-let or_ f1 f2 =
- (* Tautologies: x|x, x|not(x) *)
-
- if equal f1 f2 then f1
- else if equal f1 (not_ f2) then true_
-
- (* simplification *)
- else if is_true f1 || is_true f2 then true_
- else if is_false f1 && is_false f2 then false_
- else if is_false f1 then f2
- else if is_false f2 then f1
-
- (* commutativity of | *)
- else
- let f1, f2 = order f1 f2 in
- fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
-
-
-let and_ f1 f2 =
- not_ (or_ (not_ f1) (not_ f2))
-
-
-let of_bool = function true -> true_ | false -> false_
-
-let fold f phi acc =
- let rec loop phi acc =
- match expr phi with
- | And (phi1, phi2) | Or(phi1, phi2) ->
- loop phi2 (loop phi1 (f phi acc))
- | _ -> f phi acc
- in
- loop phi acc
-
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 11:16:45 CET by Kim Nguyen>
-*)
-
-module type ATOM =
-sig
- type t
- val neg : t -> t
- include Utils.Hcons.Abstract with type t := t
- include Utils.Common_sig.Printable with type t := t
-end
-
-type ('formula,'atom) expr =
- | False
- | True
- | Or of 'formula * 'formula
- | And of 'formula * 'formula
- | Atom of 'atom
-
-(** View of the internal representation of a formula,
- used for pattern matching *)
-
-module Make(P : ATOM) :
-sig
- type t
-
- (** Abstract type representing hashconsed formulae *)
-
- val hash : t -> int
- (** Hash function for formulae *)
-
- val uid : t -> Utils.Uid.t
- (** Returns a unique ID for formulae *)
-
- val equal : t -> t -> bool
- (** Equality over formulae *)
-
- val expr : t -> (t,P.t) expr
- (** Return a view of the formulae *)
-
- val compare : t -> t -> int
- (** Comparison of formulae *)
-
- val print : Format.formatter -> t -> unit
- (** Pretty printer *)
-
- val is_true : t -> bool
- (** [is_true f] tests whether the formula is the atom True *)
-
- val is_false : t -> bool
- (** [is_false f] tests whether the formula is the atom False *)
-
- val true_ : t
- (** Atom True *)
-
- val false_ : t
- (** Atom False *)
-
- val atom_ : P.t -> t
- (** [atom_ dir b q] creates a down_left or down_right atom for state
- [q]. The atom is positive if [b == true].
- *)
-
- val not_ : t -> t
- val or_ : t -> t -> t
- val and_ : t -> t -> t
- (** Boolean connective *)
-
- val of_bool : bool -> t
- (** Convert an ocaml Boolean value to a formula *)
-
- val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
- (** [fold f phi acc] folds [f] over the formula structure *)
-
-end
+++ /dev/null
-open Format
-module M = Map.Make(struct type t = int let compare = compare end)
-
-let info = Hashtbl.create 2017
-
-
-let add_info (nodeid:int) (i:int) s =
- let m = try Hashtbl.find info nodeid with Not_found -> M.empty in
- let old_s = try M.find i m with Not_found -> "" in
- let s' = old_s ^ s in
- let m' = M.add i s' m in
- Hashtbl.replace info nodeid m'
-
-let buff = Buffer.create 20
-let fmt = formatter_of_buffer buff
-
-let trace nodeid i =
- let () = pp_print_flush fmt ();
- Buffer.clear buff
- in
- kfprintf (fun fmt ->
- pp_print_flush fmt ();
- let s = Buffer.contents buff in
- add_info nodeid i s) fmt
-
-
-let gen_trace (type s) = (); fun t tree ->
- let module T = (val (t) : Tree.Sig.S with type t = s) in
- let rec loop odot ohtml node parent =
- if node == T.nil then () else begin
- let s_node = "node" ^ (string_of_int (T.preorder tree node)) in
- fprintf odot "%s[ id=\"%s\" label=\"%s\"];\n"
- s_node s_node (Utils.QName.to_string (T.tag tree node));
- let m =
- try
- Hashtbl.find info (T.preorder tree node)
- with Not_found -> M.empty
- in
- fprintf ohtml "data['%s'] = new Array();\n" s_node;
- M.iter
- (fun i s -> fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i s)
- m;
- if parent != T.nil then
- fprintf odot "node%i -> %s;\n"
- (T.preorder tree parent) s_node;
- loop odot ohtml (T.first_child tree node) node;
- loop odot ohtml (T.next_sibling tree node) parent
- end
- in
- ignore (Sys.command "mkdir -p tests/trace");
- let odot_ = open_out "tests/trace/trace.dot" in
- let ohtml_ = open_out "tests/trace/trace.html" in
- let odot = formatter_of_out_channel odot_ in
- let ohtml = formatter_of_out_channel ohtml_ in
- fprintf odot "digraph G {\n node[shape=box, style=filled, fillcolor=white];splines=false;";
- fprintf ohtml "<html>\
-<head><title></title>
-<link rel='stylesheet' type='text/css' href='trace.css' />\
-<meta http-equiv='content-type' content='text/html;charset=utf-8'/>\
-</head>\
-<body>\
-<div id='data' > </div>\
-<script type='text/javascript'>";
- loop odot ohtml (T.root tree) (T.nil);
- fprintf odot "\n}\n%!";
- pp_print_flush odot ();
- close_out odot_;
- ignore (Sys.command "dot -o tests/trace/trace.svg -Tsvg tests/trace/trace.dot");
- ignore (Sys.command "./tools/add_onclick.sh tests/trace/trace.svg > tests/trace/trace2.svg");
- fprintf ohtml "var activate = function (id) {\
- var d = document.getElementById('data');
- var msg = '';
- for (i=0; i < data[id].length; i++)
- msg += ('<p>' + i + ':') + data[id][i] + '</p>\\n';
- d.innerHTML = msg;
- return;
- };\n";
-
- fprintf ohtml "</script>\n<div id='svg'>\n";
- let fi = open_in "tests/trace/trace2.svg" in
- try
- while true do
- let s = input_line fi in
- fprintf ohtml "%s\n" s;
- done
- with
- End_of_file ->
- fprintf ohtml "</div></body></html>\n%!";
- pp_print_flush ohtml ();
- close_out ohtml_;
- close_in fi
-
+++ /dev/null
-val trace : int -> int -> ('a, Format.formatter, unit, unit) format4 -> 'a
-val gen_trace : (module Tree.Sig.S with type t = 'a) -> 'a -> unit
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-02-07 10:03:52 CET by Kim Nguyen>
-*)
-
-open Format
-open Utils
-
-type t = int
-let make =
- let id = ref ~-1 in
- fun () -> incr id; !id
-
-let compare = (-)
-
-let equal = (==)
-
-external hash : t -> int = "%identity"
-
-let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
-
-let dump fmt x = print fmt x
-
-let check x =
- if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
-
-let dummy = max_int
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 23:02:21 CET by Kim Nguyen>
-*)
-
-(** Implementation of states *)
-
-include Common_sig.Type with type t = int
-
-val make : unit -> t
-(** Generate a fresh state *)
-
-val dummy : t
-(** Dummy state that can never be returned by [make ()] *)
-
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-02-07 09:57:17 CET by Kim Nguyen>
-*)
-
-open Format
-open Utils
-
-include Ptset.Make (Hcons.PosInt)
-
-let print ppf s =
- fprintf ppf "{ %a }"
- (Pretty.print_list ~sep:" " (State.print)) (elements s)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-02-07 09:57:11 CET by Kim Nguyen>
-*)
-
-(** Implementation of sets of states *)
-include Utils.Ptset.S with type elt = int
-
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-14 14:50:18 CET by Kim Nguyen>
+*)
+
+let realloc l old_size new_size dummy =
+ let l' = Array.create new_size dummy in
+ for i = 0 to (min old_size new_size) - 1 do
+ Array.unsafe_set l' i (Array.unsafe_get l i);
+ done;
+ l'
+
+module N1 =
+struct
+ type 'a t = { mutable line : 'a array;
+ dummy : 'a;
+ mutable offset : int;
+ }
+ let create a = {
+ line = Array.create 0 a;
+ dummy = a;
+ offset = ~-1;
+
+ }
+
+ let print fmt a =
+ Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!"
+ a.offset
+ (Pretty.print_array ~sep:", " (fun fmt x ->
+ if x==a.dummy then
+ Format.fprintf fmt "%s" "D"
+ else
+ Format.fprintf fmt "%s" "E")) a.line
+
+ let add a i v =
+ if a.offset == ~-1 then a.offset <- i;
+ let offset = a.offset in
+ let len = Array.length a.line in
+ if i >= offset && i < offset + len then
+ a.line.(i - offset) <- v
+ else
+ if i < offset then begin (* bottom resize *)
+ let pad = offset - i in
+ let nlen = len + pad in
+ let narray = Array.create nlen a.dummy in
+ for j = 0 to len - 1 do
+ narray.(j+pad) <- a.line.(j)
+ done;
+ a.offset <- i;
+ a.line <- narray;
+ narray.(0) <- v;
+ end else begin (* top resize *)
+ (* preventively allocate the space for the following elements *)
+ let nlen = ((i - offset + 1) lsl 1) + 1 in
+ let narray = Array.create nlen a.dummy in
+ for j = 0 to len - 1 do
+ narray.(j) <- a.line.(j);
+ done;
+ narray.(i - offset) <- v;
+ a.line <- narray
+ end
+
+ let find a i =
+ let idx = i - a.offset in
+ let len = Array.length a.line in
+ if idx >= 0 && idx < len then
+ Array.unsafe_get a.line idx
+ else a.dummy
+
+ let dummy a = a.dummy
+
+ let iteri f a =
+ let line = a.line in
+ if a.offset == ~-1 then () else
+ for i = 0 to Array.length line - 1 do
+ let v = line.(i) in
+ f (i+a.offset) v (v==a.dummy)
+ done
+
+
+end
+
+module N2 =
+struct
+ type 'a t = 'a N1.t N1.t
+ let create a =
+ let dummy1 = N1.create a in
+ N1.create dummy1
+
+ let add a i j v =
+ let line = N1.find a i in
+ if line == a.N1.dummy then
+ let nline = N1.create line.N1.dummy in
+ N1.add a i nline;
+ N1.add nline j v
+ else
+ N1.add line j v
+
+
+ let find a i j =
+ let v = N1.find a i in
+ if v == a.N1.dummy then v.N1.dummy
+ else N1.find v j
+
+
+ let dummy c = c.N1.dummy.N1.dummy
+
+ let iteri f a =
+ let line = a.N1.line in
+ if a.N1.offset == ~-1 then () else
+ for i = 0 to Array.length line - 1 do
+ N1.iteri (f i) line.(i)
+ done
+
+
+end
+
+module N3 =
+struct
+ type 'a t = 'a N2.t N1.t
+
+ let create a =
+ let dummy2 = N2.create a in
+ N1.create dummy2
+
+ let add a i j k v =
+ let line = N1.find a i in
+ if line == a.N1.dummy then
+ let nline = N1.create line.N1.dummy in
+ N1.add a i nline;
+ N2.add nline j k v
+ else
+ N2.add line j k v
+
+ let find a i j k =
+ let v = N1.find a i in
+ if v == a.N1.dummy then N2.dummy v
+ else N2.find v j k
+
+
+ let dummy a = N2.dummy a.N1.dummy
+ let iteri f a =
+ let line = a.N1.line in
+ if a.N1.offset == ~-1 then () else
+ for i = 0 to Array.length line - 1 do
+ N2.iteri (f i) line.(i)
+ done
+
+end
+
+module N4 =
+struct
+ type 'a t = 'a N3.t N1.t
+
+ let create a =
+ let dummy3 = N3.create a in
+ N1.create dummy3
+
+ let add a i j k l v =
+ let line = N1.find a i in
+ if line == N1.dummy a then
+ let nline = N3.create (N3.dummy line) in
+ N1.add a i nline;
+ N3.add nline j k l v
+ else
+ N3.add line j k l v
+
+ let find a i j k l =
+ let v = N1.find a i in
+ if v == (N1.dummy a) then N3.dummy v
+ else N3.find v j k l
+
+
+ let dummy a = N3.dummy (N1.dummy a)
+ let iteri f a =
+ N1.iteri (fun i v _ ->
+ N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a
+
+end
+
+module N5 =
+struct
+ type 'a t = 'a N4.t N1.t
+
+ let create a =
+ let dummy4 = N4.create a in
+ N1.create dummy4
+
+ let add a i j k l m v =
+ let line = N1.find a i in
+ if line == (N1.dummy a) then
+ let nline = N4.create (N4.dummy line) in
+ N1.add a i nline;
+ N4.add nline j k l m v
+ else
+ N4.add line j k l m v
+
+ let find a i j k l m =
+ let v = N1.find a i in
+ if v == (N1.dummy a) then N4.dummy v
+ else N4.find v j k l m
+
+
+ let dummy a = N4.dummy (N1.dummy a)
+ let iteri f a =
+ N1.iteri (fun i v _ ->
+ N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v
+ ) a
+end
+
+module N6 =
+struct
+ type 'a t = 'a N5.t N1.t
+
+ let create a =
+ let dummy5 = N5.create a in
+ N1.create dummy5
+
+ let add a i j k l m n v =
+ let line = N1.find a i in
+ if line == N1.dummy a then
+ let nline = N5.create (N5.dummy line) in
+ N1.add a i nline;
+ N5.add nline j k l m n v
+ else
+ N5.add line j k l m n v
+
+ let find a i j k l m n =
+ let v = N1.find a i in
+ if v == N1.dummy a then N5.dummy v
+ else N5.find v j k l m n
+
+
+ let dummy a = N5.dummy (N1.dummy a)
+ let iteri f a =
+ N1.iteri (fun i v _ ->
+ N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v
+ ) a
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-14 13:42:53 CET by Kim Nguyen>
+*)
+
+(** N-dimentional caches *)
+
+module N1 :
+sig
+
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> 'a
+ val add : 'a t -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit
+end
+
+module N2:
+sig
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> int -> 'a
+ val add : 'a t -> int -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+end
+
+module N3 :
+ sig
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> int -> int -> 'a
+ val add : 'a t -> int -> int -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+ end
+
+module N4 :
+ sig
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> int -> int -> int -> 'a
+ val add : 'a t -> int -> int -> int -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+ end
+
+module N5 :
+ sig
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> int -> int -> int -> int -> 'a
+ val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+ end
+
+module N6 :
+ sig
+ type 'a t
+ val create : 'a -> 'a t
+ val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
+ val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
+ val dummy : 'a t -> 'a
+ val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+ end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 23:01:55 CET by Kim Nguyen>
+*)
+
+(** Type equipped with an equality and hash function.
+ If [equal a b] then [(hash a) = (hash b)]
+*)
+module type HashedType =
+sig
+ type t
+
+ (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
+ *)
+ val hash : t -> int
+
+ (** Equality *)
+ val equal : t -> t -> bool
+
+end
+
+(** Type equiped with a total ordering *)
+module type OrderedType =
+sig
+ type t
+
+ (** Total ordering on values of type [t]. [compare a b] returns a
+ negative number if [a] is strictly smaller than [b], a positive
+ number if [a] is strictly greater than [b] and 0 if [a] is equal
+ to [b]. *)
+ val compare : t -> t -> int
+end
+
+module type Type =
+sig
+ type t
+ include HashedType with type t := t
+ include OrderedType with type t := t
+end
+
+(** Type equiped with a pretty-printer *)
+module type Printable =
+sig
+ type t
+ val print : Format.formatter -> t -> unit
+end
+
+(** Signature of a simple HashSet module *)
+module type HashSet =
+sig
+ type data
+ type t
+ val create : int -> t
+ val add : t -> data -> unit
+ val remove : t -> data -> unit
+ val find : t -> data -> data
+ val find_all : t -> data -> data list
+ val clear : t -> unit
+ val mem : t -> data -> bool
+end
+
+ (** Signature of simple Set module *)
+module type Set =
+sig
+ type elt
+ type t
+ val empty : t
+ val is_empty : t -> bool
+ val mem : elt -> t -> bool
+ val add : elt -> t -> t
+ val singleton : elt -> t
+ val remove : elt -> t -> t
+ val union : t -> t -> t
+ val inter : t -> t -> t
+ val diff : t -> t -> t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val subset : t -> t -> bool
+ val iter : (elt -> unit) -> t -> unit
+ val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+ val for_all : (elt -> bool) -> t -> bool
+ val exists : (elt -> bool) -> t -> bool
+ val filter : (elt -> bool) -> t -> t
+ val partition : (elt -> bool) -> t -> t * t
+ val cardinal : t -> int
+ val elements : t -> elt list
+ val min_elt : t -> elt
+ val max_elt : t -> elt
+ val choose : t -> elt
+ val split : elt -> t -> t * bool * t
+ val intersect : t -> t -> bool
+ val is_singleton : t -> bool
+ val from_list : elt list -> t
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:45:19 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+open Format
+
+module Make (T : Tree.S) :
+ sig
+ val eval : Ata.t -> T.t -> T.node -> T.node list
+ end
+ = struct
+
+
+IFDEF HTMLTRACE
+ THEN
+DEFINE TRACE(e) = (e)
+ ELSE
+DEFINE TRACE(e) = ()
+END
+
+
+
+ type cache = StateSet.t Cache.N1.t
+ let get c t n = Cache.N1.find c (T.preorder t n)
+
+ let set c t n v = Cache.N1.add c (T.preorder t n) v
+
+
+ let top_down_run auto tree node cache _i =
+ let redo = ref false in
+ let rec loop node =
+ if node != T.nil then begin
+ let parent = T.parent tree node in
+ let fc = T.first_child tree node in
+ let ns = T.next_sibling tree node in
+ let tag = T.tag tree node in
+ let states0 = get cache tree node in
+ let trans0 = Ata.get_trans auto tag auto.Ata.states in
+ let () =
+ TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a<br/>Pre Trans: %a<br/>"
+ StateSet.print states0 (Ata.TransList.print ~sep:"<br/>") trans0)
+ in
+ let ps = get cache tree parent in
+ let fcs = get cache tree fc in
+ let nss = get cache tree ns in
+ let is_left = node == T.first_child tree parent
+ and is_right = node == T.next_sibling tree parent
+ and has_left = fc != T.nil
+ and has_right = ns != T.nil
+ and kind = T.kind tree node
+ in
+ let trans1, states1 =
+ Ata.eval_trans auto trans0
+ fcs nss ps states0
+ is_left is_right has_left has_right kind
+ in
+ let () =
+ TRACE(Html.trace (T.preorder tree node) _i "TD States: %a<br/>TD Trans: %a<br/>" StateSet.print states1 (Ata.TransList.print ~sep:"<br/>") trans1)
+ in
+ if states1 != states0 then set cache tree node states1;
+ let () = loop fc in
+ let fcs1 = get cache tree fc in
+ let trans2, states2 =
+ Ata.eval_trans auto trans1
+ fcs1 nss ps states1
+ is_left is_right has_left has_right kind
+ in
+ let () =
+ TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a<br/>Left BU Trans: %a<br/>" StateSet.print states2 (Ata.TransList.print ~sep:"<br/>") trans2)
+ in
+ if states2 != states1 then set cache tree node states2;
+ let () = loop ns in
+ let _trans3, states3 =
+ Ata.eval_trans auto trans2
+ fcs1 (get cache tree ns) ps states2
+ is_left is_right has_left has_right kind
+ in
+ let () =
+ TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a<br/>Right BU Trans: %a<br/>" StateSet.print states3 (Ata.TransList.print ~sep:"<br/>") _trans3)
+ in
+ if states3 != states2 then set cache tree node states3;
+ if states0 != states3 && (not !redo) then redo := true
+ end
+ in
+ loop node;
+ !redo
+
+ let get_results auto tree node cache =
+ let rec loop node acc =
+ if node == T.nil then acc
+ else
+ let acc0 = loop (T.next_sibling tree node) acc in
+ let acc1 = loop (T.first_child tree node) acc0 in
+
+ if StateSet.intersect (get cache tree node) auto.Ata.selection_states then
+ node::acc1
+ else
+ acc1
+ in
+ loop node []
+
+ let eval auto tree node =
+ let cache = Cache.N1.create StateSet.empty in
+ let redo = ref true in
+ let iter = ref 0 in
+ Ata.reset auto;
+ while !redo do
+ redo := top_down_run auto tree node cache !iter;
+ incr iter;
+ done;
+ let r = get_results auto tree node cache in
+ TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree));
+ r
+
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+include FiniteCofinite_sig
+
+module type HConsBuilder =
+ functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (E : Ptset.S) :
+ S with type elt = E.elt and type set = E.t =
+struct
+ type elt = E.elt
+ type node = Finite of E.t | CoFinite of E.t
+ type set = E.t
+ module Node = HCB(struct
+ type t = node
+ let equal a b =
+ match a, b with
+ Finite s1, Finite s2
+ | CoFinite s1, CoFinite s2 -> E.equal s1 s2
+ | (Finite _| CoFinite _), _ -> false
+
+ let hash = function
+ | Finite s -> HASHINT2 (PRIME1, E.hash s)
+ | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
+ end)
+ include Node
+ let empty = make (Finite E.empty)
+ let any = make (CoFinite E.empty)
+ let finite x = make (Finite x)
+ let cofinite x = make (CoFinite x)
+
+ let is_empty t = match t.node with
+ | Finite s -> E.is_empty s
+ | CoFinite _ -> false
+
+ let is_any t = match t.node with
+ | CoFinite s -> E.is_empty s
+ | Finite _ -> false
+
+ let is_finite t = match t.node with
+ | Finite _ -> true
+ | CoFinite _ -> false
+
+ let kind t = match t.node with
+ | Finite _ -> `Finite
+ | CoFinite _ -> `Cofinite
+
+ let mem x t = match t.node with
+ | Finite s -> E.mem x s
+ | CoFinite s -> not (E.mem x s)
+
+ let singleton x = finite (E.singleton x)
+
+ let add e t = match t.node with
+ | Finite s -> finite (E.add e s)
+ | CoFinite s -> cofinite (E.remove e s)
+
+ let remove e t = match t.node with
+ | Finite s -> finite (E.remove e s)
+ | CoFinite s -> cofinite (E.add e s)
+
+ let union s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.union s t)
+ | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
+ | Finite s, CoFinite t -> cofinite (E.diff t s)
+ | CoFinite s, Finite t-> cofinite (E.diff s t)
+
+ let inter s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.inter s t)
+ | CoFinite s, CoFinite t -> cofinite (E.union s t)
+ | Finite s, CoFinite t -> finite (E.diff s t)
+ | CoFinite s, Finite t-> finite (E.diff t s)
+
+ let diff s t = match s.node, t.node with
+ | Finite s, Finite t -> finite (E.diff s t)
+ | Finite s, CoFinite t -> finite(E.inter s t)
+ | CoFinite s, Finite t -> cofinite(E.union t s)
+ | CoFinite s, CoFinite t -> finite (E.diff t s)
+
+ let complement t = match t.node with
+ | Finite s -> cofinite s
+ | CoFinite s -> finite s
+
+ let compare s t = match s.node, t.node with
+ | Finite s , Finite t -> E.compare s t
+ | CoFinite s , CoFinite t -> E.compare t s
+ | Finite _, CoFinite _ -> -1
+ | CoFinite _, Finite _ -> 1
+
+ let subset s t = match s.node, t.node with
+ | Finite s , Finite t -> E.subset s t
+ | CoFinite s , CoFinite t -> E.subset t s
+ | Finite s, CoFinite t -> E.is_empty (E.inter s t)
+ | CoFinite _, Finite _ -> false
+
+ (* given a list l of type t list,
+ returns two sets (f,c) where :
+ - f is the union of all the finite sets of l
+ - c is the union of all the cofinite sets of l
+ - f and c are disjoint
+ Invariant : cup f c = List.fold_left cup empty l
+ We treat the CoFinite part explicitely :
+ *)
+
+ let kind_split l =
+
+ let rec next_finite_cofinite facc cacc = function
+ | [] -> finite facc, cofinite (E.diff cacc facc)
+ | { node = Finite s; _ } ::r ->
+ next_finite_cofinite (E.union s facc) cacc r
+ | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
+ next_finite_cofinite facc cacc r
+ | { node = CoFinite s; _ } ::r ->
+ next_finite_cofinite facc (E.inter cacc s) r
+ in
+ let rec first_cofinite facc = function
+ | [] -> empty,empty
+ | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
+ | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
+ in
+ first_cofinite E.empty l
+
+ let exn = FiniteCofinite_sig.InfiniteSet
+
+ let fold f t a = match t.node with
+ | Finite s -> E.fold f s a
+ | CoFinite _ -> raise exn
+
+ let iter f t = match t.node with
+ | Finite t -> E.iter f t
+ | CoFinite _ -> raise exn
+
+ let for_all f t = match t.node with
+ | Finite s -> E.for_all f s
+ | CoFinite _ -> raise exn
+
+ let exists f t = match t.node with
+ | Finite s -> E.exists f s
+ | CoFinite _ -> raise exn
+
+ let filter f t = match t.node with
+ | Finite s -> finite (E.filter f s)
+ | CoFinite _ -> raise exn
+
+ let partition f t = match t.node with
+ | Finite s -> let a,b = E.partition f s in finite a,finite b
+ | CoFinite _ -> raise exn
+
+ let cardinal t = match t.node with
+ | Finite s -> E.cardinal s
+ | CoFinite _ -> raise exn
+
+ let elements t = match t.node with
+ | Finite s -> E.elements s
+ | CoFinite _ -> raise exn
+
+ let from_list l =
+ finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
+
+ let choose t = match t.node with
+ Finite s -> E.choose s
+ | CoFinite _ -> raise exn
+
+ let is_singleton t = match t.node with
+ | Finite s -> E.is_singleton s
+ | CoFinite _ -> false
+
+ let intersect s t = match s.node, t.node with
+ | Finite s, Finite t -> E.intersect s t
+ | CoFinite s, Finite t -> not (E.subset t s)
+ | Finite s, CoFinite t -> not (E.subset s t)
+ | CoFinite _ , CoFinite _ -> true
+
+ let split x s = match s.node with
+ | Finite s ->
+ let s1, b, s2 = E.split x s in
+ finite s1, b, finite s2
+
+ | CoFinite _ -> raise exn
+
+ let min_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | CoFinite _ -> raise exn
+
+ let max_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | CoFinite _ -> raise exn
+
+ let positive t = match t.node with
+ | Finite x -> x
+ | CoFinite _ -> E.empty
+
+ let negative t = match t.node with
+ | CoFinite x -> x
+ | Finite _ -> E.empty
+
+ let inj_positive t = finite t
+ let inj_negative t = cofinite t
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:44:50 CET by Kim Nguyen>
+*)
+
+(** Implementation of hashconsed finite or cofinite sets.
+*)
+
+include module type of FiniteCofinite_sig
+
+(** Output signature of the {!FiniteCofinite.Make} and
+ {!FiniteCofinite.Weak} functors.*)
+
+module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t
+(** Builds an implementation of hashconsed sets of hashconsed elements.
+ See {!Hcons.Make}.
+*)
+
+module Weak (E : Ptset.S) : S with type elt = E.elt and type set = E.t
+(** Builds an implementation of hashconsed sets of hashconsed elements
+ with weak internal storage. See {!Hcons.Weak}.
+*)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:44:15 CET by Kim Nguyen>
+*)
+
+exception InfiniteSet
+module type S =
+sig
+ include Hcons.S
+ include Common_sig.Set with type t := t
+ type set
+ val any : t
+ val is_any : t -> bool
+ val is_finite : t -> bool
+ val kind : t -> [ `Finite | `Cofinite ]
+ val complement : t -> t
+ val kind_split : t list -> t * t
+ val positive : t -> set
+ val negative : t -> set
+ val inj_positive : set -> t
+ val inj_negative : set -> t
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:46:09 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+open Format
+
+(*
+
+(** Implementation of hashconsed Boolean formulae *)
+
+*)
+module type ATOM =
+sig
+ type t
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Common_sig.Printable with type t := t
+end
+
+type ('formula,'atom) expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Atom of 'atom
+
+module Make (P: ATOM) =
+struct
+
+
+ type 'hcons node = {
+ pos : ('hcons,P.t) expr;
+ mutable neg : 'hcons;
+ }
+
+ external hash_const_variant : [> ] -> int = "%identity"
+ external vb : bool -> int = "%identity"
+
+ module rec Node : Hcons.S
+ with type data = Data.t = Hcons.Make (Data)
+ and Data : Common_sig.HashedType with type t = Node.t node =
+ struct
+ type t = Node.t node
+ let equal x y =
+ match x.pos, y.pos with
+ | a,b when a == b -> true
+ | Or(xf1, xf2), Or(yf1, yf2)
+ | And(xf1, xf2), And(yf1,yf2) -> xf1 == yf1 && xf2 == yf2
+ | Atom(p1), Atom(p2) -> p1 == p2
+ | _ -> false
+
+ let hash f =
+ match f.pos with
+ | False -> 0
+ | True -> 1
+ | Or (f1, f2) ->
+ HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+ | And (f1, f2) ->
+ HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+ | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p))
+ end
+
+ type t = Node.t
+ let hash x = x.Node.hash
+ let uid x = x.Node.id
+ let equal = Node.equal
+ let expr f = f.Node.node.pos
+
+ let compare f1 f2 = compare f1.Node.id f2.Node.id
+ let prio f =
+ match expr f with
+ | True | False -> 10
+ | Atom _ -> 8
+ | And _ -> 6
+ | Or _ -> 1
+
+ let rec print ?(parent=false) ppf f =
+ if parent then fprintf ppf "(";
+ let _ = match expr f with
+ | True -> fprintf ppf "%s" Pretty.top
+ | False -> fprintf ppf "%s" Pretty.bottom
+ | And(f1,f2) ->
+ print ~parent:(prio f > prio f1) ppf f1;
+ fprintf ppf " %s " Pretty.wedge;
+ print ~parent:(prio f > prio f2) ppf f2;
+ | Or(f1,f2) ->
+ (print ppf f1);
+ fprintf ppf " %s " Pretty.vee;
+ (print ppf f2);
+ | Atom(p) -> fprintf ppf "%a" P.print p
+(* let _ = flush_str_formatter() in
+ let fmt = str_formatter in
+ let a_str, d_str =
+ match dir with
+ | `Left -> Pretty.down_arrow, Pretty.subscript 1
+ | `Right -> Pretty.down_arrow, Pretty.subscript 2
+ | `Epsilon -> Pretty.epsilon, ""
+ | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+ | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
+ in
+ fprintf fmt "%s%s" a_str d_str;
+ State.print fmt s;
+ let str = flush_str_formatter() in
+ if b then fprintf ppf "%s" str
+ else Pretty.pp_overline ppf str *)
+ in
+ if parent then fprintf ppf ")"
+
+let print ppf f = print ~parent:false ppf f
+
+let is_true f = (expr f) == True
+let is_false f = (expr f) == False
+
+
+let cons pos neg =
+ let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
+ let pnode = Node.make { pos = pos; neg = nnode } in
+ (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
+ account for hashing ! *)
+ pnode,nnode
+
+
+let true_,false_ = cons True False
+
+let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
+
+let not_ f = f.Node.node.neg
+
+let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
+
+let or_ f1 f2 =
+ (* Tautologies: x|x, x|not(x) *)
+
+ if equal f1 f2 then f1
+ else if equal f1 (not_ f2) then true_
+
+ (* simplification *)
+ else if is_true f1 || is_true f2 then true_
+ else if is_false f1 && is_false f2 then false_
+ else if is_false f1 then f2
+ else if is_false f2 then f1
+
+ (* commutativity of | *)
+ else
+ let f1, f2 = order f1 f2 in
+ fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
+
+
+let and_ f1 f2 =
+ not_ (or_ (not_ f1) (not_ f2))
+
+
+let of_bool = function true -> true_ | false -> false_
+
+let fold f phi acc =
+ let rec loop phi acc =
+ match expr phi with
+ | And (phi1, phi2) | Or(phi1, phi2) ->
+ loop phi2 (loop phi1 (f phi acc))
+ | _ -> f phi acc
+ in
+ loop phi acc
+
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
+*)
+
+module type ATOM =
+sig
+ type t
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Common_sig.Printable with type t := t
+end
+
+type ('formula,'atom) expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Atom of 'atom
+
+(** View of the internal representation of a formula,
+ used for pattern matching *)
+
+module Make(P : ATOM) :
+sig
+ type t
+
+ (** Abstract type representing hashconsed formulae *)
+
+ val hash : t -> int
+ (** Hash function for formulae *)
+
+ val uid : t -> Uid.t
+ (** Returns a unique ID for formulae *)
+
+ val equal : t -> t -> bool
+ (** Equality over formulae *)
+
+ val expr : t -> (t,P.t) expr
+ (** Return a view of the formulae *)
+
+ val compare : t -> t -> int
+ (** Comparison of formulae *)
+
+ val print : Format.formatter -> t -> unit
+ (** Pretty printer *)
+
+ val is_true : t -> bool
+ (** [is_true f] tests whether the formula is the atom True *)
+
+ val is_false : t -> bool
+ (** [is_false f] tests whether the formula is the atom False *)
+
+ val true_ : t
+ (** Atom True *)
+
+ val false_ : t
+ (** Atom False *)
+
+ val atom_ : P.t -> t
+ (** [atom_ dir b q] creates a down_left or down_right atom for state
+ [q]. The atom is positive if [b == true].
+ *)
+
+ val not_ : t -> t
+ val or_ : t -> t -> t
+ val and_ : t -> t -> t
+ (** Boolean connective *)
+
+ val of_bool : bool -> t
+ (** Convert an ocaml Boolean value to a formula *)
+
+ val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** [fold f phi acc] folds [f] over the formula structure *)
+
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
+*)
+
+include Hcons_sig
+
+module type TableBuilder =
+ functor
+ (H : Common_sig.HashedType) ->
+ Common_sig.HashSet with type data = H.t
+
+module Builder (TB : TableBuilder) (H : Common_sig.HashedType) =
+struct
+ type data = H.t
+ type t = { id : Uid.t;
+ hash : int;
+ node : data }
+ let uid_make = ref (Uid.make_maker())
+ let node t = t.node
+ let uid t = t.id
+ let hash t = t.hash
+ let equal t1 t2 = t1 == t2
+ module HN =
+ struct
+ type _t = t
+ type t = _t
+ let hash = hash
+ let equal x y = x == y || H.equal x.node y.node
+ end
+ module T = TB(HN)
+
+ let pool = T.create 101
+ let init () =
+ T.clear pool;
+ uid_make := Uid.make_maker ()
+ let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
+
+ let make x =
+ let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
+ try
+ T.find pool cell
+ with
+ | Not_found ->
+ let cell = { cell with id = !uid_make(); } in
+ T.add pool cell;
+ cell
+end
+
+module Make = Builder (Misc.HashSet)
+module Weak = Builder (Weak.Make)
+
+module PosInt =
+struct
+ type data = int
+ type t = int
+ let make v =
+ if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
+ else v
+
+ let node v = v
+
+ let hash v = v
+
+ let uid v = Uid.of_int v
+ let dummy _ = ~-1
+ let equal x y = x == y
+
+ let init () = ()
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 23:05:14 CET by Kim Nguyen>
+*)
+
+(** Implementation of generic hashconsing. *)
+
+include module type of Hcons_sig
+
+(** Output signature of the functor {!Hcons.Make} *)
+
+module Make (H : Common_sig.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+ implementation of {!Common_sig.HashedType}. Hashconsed values are
+ persistent: the are kept in memory even if no external reference
+ remain. Calling [init()] explicitely will reclaim the space.
+*)
+
+module Weak (H : Common_sig.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+ implementation of {!Common_sig.HashedType}. Hashconsed values have a
+ weak semantics: they may be reclaimed as soon as no external
+ reference to them exists. The space may still be reclaimed
+ explicitely by calling [init].
+*)
+
+module PosInt : Abstract with type data = int and type t = int
+(** Compact implementation of hashconsed positive integer that
+ avoids boxing. [PosInt.make v] raises [Invalid_argument] if
+ [ v < 0 ]
+*)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:36:31 CET by Kim Nguyen>
+*)
+
+ (** Abstract signature of a module implementing an hashconsed datatype *)
+module type Abstract =
+sig
+
+ (** The type of the data to be hash-consed *)
+ type data
+
+ (** The type of hashconsed data *)
+ type t
+
+ (** [make v] internalizes the value [v], making it an hashconsed
+ value.
+ *)
+ val make : data -> t
+
+ (** [node h] extract the original data from its hashconsed value
+ *)
+ val node : t -> data
+
+ (** [hash h] returns a hash of [h], such that for every [h1] and
+ [h2], [equal h1 h2] implies [hash h1 = hash h2].
+ *)
+ val hash : t -> int
+
+ (** [uid h] returns a unique identifier *)
+ val uid : t -> Uid.t
+
+ (** Equality between hashconsed values. Equivalent to [==] *)
+ val equal : t -> t -> bool
+
+ (** Initializes the internal storage. Any previously hashconsed
+ element is discarded. *)
+ val init : unit -> unit
+
+ (** Create a dummy (non-hashconsed) node with a boggus identifer
+ and hash *)
+ val dummy : data -> t
+end
+
+
+ (** Concrete signature of a module implementing an hashconsed datatype *)
+module type S =
+sig
+ type data
+ type t = private { id : Uid.t;
+ hash : int;
+ node : data }
+ include Abstract with type data := data and type t := t
+end
--- /dev/null
+INCLUDE "utils.ml"
+
+include Hlist_sig
+
+module type HConsBuilder =
+ functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
+ S with type elt = H.t =
+struct
+ type elt = H.t
+
+ module rec Node : Hcons.S with type data = Data.t = HCB(Data)
+ and Data : Common_sig.HashedType with type t = (elt, Node.t) node =
+ struct
+ type t = (elt, Node.t) node
+ let equal x y =
+ match x,y with
+ | Nil, Nil -> true
+ | Cons(e1, l1), Cons(e2, l2) -> e1 == e2 && l1 == l2
+ | _ -> false
+
+ let hash = function
+ | Nil -> 0
+ | Cons(e, l) -> HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))
+ end
+
+ include Node
+
+ let nil = make Nil
+
+ let rec sorted_cons e l =
+ match l.Node.node with
+ | Nil -> Node.make (Cons(e, l))
+ | Cons (x, ll) ->
+ if H.uid e < H.uid x
+ then Node.make (Cons(e, l))
+ else Node.make (Cons(x, sorted_cons e ll))
+
+ let cons e l =
+ Node.make(Cons(e, l))
+
+ let cons ?(sorted=true) e l =
+ if sorted then sorted_cons e l else cons e l
+
+ let hd = function { Node.node = Cons(e, _); _ } -> e | _ -> failwith "hd"
+ let tl = function { Node.node = Cons(_, l); _ } -> l | _ -> failwith "tl"
+
+ let fold f l acc =
+ let rec loop acc l = match l.Node.node with
+ | Nil -> acc
+ | Cons (a, aa) -> loop (f a acc) aa
+ in
+ loop acc l
+
+ let map f l =
+ let rec loop l = match l.Node.node with
+ | Nil -> nil
+ | Cons(a, aa) -> cons (f a) (loop aa)
+ in
+ loop l
+
+ let iter f l =
+ let rec loop l = match l.Node.node with
+ | Nil -> ()
+ | Cons(a,aa) -> (f a);(loop aa)
+ in
+ loop l
+
+ let rev l = fold cons l nil
+ let rev_map f l = fold (fun x acc -> cons (f x) acc) l nil
+ let length l = fold (fun _ c -> c+1) l 0
+ let rec mem e l =
+ match l.Node.node with
+ | Nil -> false
+ | Cons (x, ll) -> x == e || mem e ll
+
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
+
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-13 18:30:59 CET by Kim Nguyen>
+*)
+
+include module type of Hlist_sig
+
+module Make (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed lists of hashconsed elements.
+ See {!Hcons.Make}.
+*)
+
+module Weak (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed lists of hashconsed elements
+ with weak internal storage. See {!Hcons.Weak}.
+*)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-13 18:21:28 CET by Kim Nguyen>
+*)
+type ('a,'b) node = Nil | Cons of ('a * 'b)
+
+module type S = sig
+ type elt
+ include Hcons.S
+ val nil : t
+ val cons : ?sorted:bool -> elt -> t -> t
+ val hd : t -> elt
+ val tl : t -> t
+ val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+ val map : (elt -> elt) -> t -> t
+ val iter : (elt -> 'a) -> t -> unit
+ val rev : t -> t
+ val rev_map : (elt -> elt) -> t -> t
+ val length : t -> int
+ val mem : elt -> t -> bool
+end
--- /dev/null
+open Format
+module M = Map.Make(struct type t = int let compare = compare end)
+
+let info = Hashtbl.create 2017
+
+
+let add_info (nodeid:int) (i:int) s =
+ let m = try Hashtbl.find info nodeid with Not_found -> M.empty in
+ let old_s = try M.find i m with Not_found -> "" in
+ let s' = old_s ^ s in
+ let m' = M.add i s' m in
+ Hashtbl.replace info nodeid m'
+
+let buff = Buffer.create 20
+let fmt = formatter_of_buffer buff
+
+let trace nodeid i =
+ let () = pp_print_flush fmt ();
+ Buffer.clear buff
+ in
+ kfprintf (fun fmt ->
+ pp_print_flush fmt ();
+ let s = Buffer.contents buff in
+ add_info nodeid i s) fmt
+
+
+let gen_trace (type s) = (); fun t tree ->
+ let module T = (val (t) : Tree.Sig.S with type t = s) in
+ let rec loop odot ohtml node parent =
+ if node == T.nil then () else begin
+ let s_node = "node" ^ (string_of_int (T.preorder tree node)) in
+ fprintf odot "%s[ id=\"%s\" label=\"%s\"];\n"
+ s_node s_node (Utils.QName.to_string (T.tag tree node));
+ let m =
+ try
+ Hashtbl.find info (T.preorder tree node)
+ with Not_found -> M.empty
+ in
+ fprintf ohtml "data['%s'] = new Array();\n" s_node;
+ M.iter
+ (fun i s -> fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i s)
+ m;
+ if parent != T.nil then
+ fprintf odot "node%i -> %s;\n"
+ (T.preorder tree parent) s_node;
+ loop odot ohtml (T.first_child tree node) node;
+ loop odot ohtml (T.next_sibling tree node) parent
+ end
+ in
+ ignore (Sys.command "mkdir -p tests/trace");
+ let odot_ = open_out "tests/trace/trace.dot" in
+ let ohtml_ = open_out "tests/trace/trace.html" in
+ let odot = formatter_of_out_channel odot_ in
+ let ohtml = formatter_of_out_channel ohtml_ in
+ fprintf odot "digraph G {\n node[shape=box, style=filled, fillcolor=white];splines=false;";
+ fprintf ohtml "<html>\
+<head><title></title>
+<link rel='stylesheet' type='text/css' href='trace.css' />\
+<meta http-equiv='content-type' content='text/html;charset=utf-8'/>\
+</head>\
+<body>\
+<div id='data' > </div>\
+<script type='text/javascript'>";
+ loop odot ohtml (T.root tree) (T.nil);
+ fprintf odot "\n}\n%!";
+ pp_print_flush odot ();
+ close_out odot_;
+ ignore (Sys.command "dot -o tests/trace/trace.svg -Tsvg tests/trace/trace.dot");
+ ignore (Sys.command "./tools/add_onclick.sh tests/trace/trace.svg > tests/trace/trace2.svg");
+ fprintf ohtml "var activate = function (id) {\
+ var d = document.getElementById('data');
+ var msg = '';
+ for (i=0; i < data[id].length; i++)
+ msg += ('<p>' + i + ':') + data[id][i] + '</p>\\n';
+ d.innerHTML = msg;
+ return;
+ };\n";
+
+ fprintf ohtml "</script>\n<div id='svg'>\n";
+ let fi = open_in "tests/trace/trace2.svg" in
+ try
+ while true do
+ let s = input_line fi in
+ fprintf ohtml "%s\n" s;
+ done
+ with
+ End_of_file ->
+ fprintf ohtml "</div></body></html>\n%!";
+ pp_print_flush ohtml ();
+ close_out ohtml_;
+ close_in fi
+
--- /dev/null
+val trace : int -> int -> ('a, Format.formatter, unit, unit) format4 -> 'a
+val gen_trace : (module Tree.Sig.S with type t = 'a) -> 'a -> unit
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 23:00:19 CET by Kim Nguyen>
+*)
+
+(** Various generic signatures and generic module and functor definitions
+*)
+INCLUDE "utils.ml"
+
+module HashSet (H : Hashtbl.HashedType) :
+ Common_sig.HashSet with type data = H.t =
+struct
+ module T = Hashtbl.Make(H)
+ type data = H.t
+ type t = data T.t
+ let create = T.create
+ let add h v = T.add h v v
+ let find = T.find
+ let remove = T.remove
+ let find_all = T.find_all
+ let clear = T.clear
+ let mem = T.mem
+end
+
+module Pair (X : Common_sig.Type) (Y : Common_sig.Type) :
+ Common_sig.Type with type t = X.t * Y.t =
+struct
+ type t = X.t * Y.t
+ let hash (x, y) = HASHINT2(X.hash x, Y.hash y)
+ let compare (x1, y1) (x2, y2) =
+ let r = X.compare x1 x2 in
+ if r != 0 then r else Y.compare y1 y2
+ let equal p1 p2 =
+ p1 == p2 ||
+ let x1, y1 = p1
+ and x2, y2 = p2 in X.equal x1 x2 && Y.equal y1 y2
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:47:30 CEST by Kim Nguyen>
+*)
+
+type node = {
+ tag : QName.t;
+ preorder : int;
+ mutable kind : Tree.NodeKind.t;
+ mutable data : string;
+ mutable first_child : node;
+ mutable next_sibling : node;
+ mutable parent: node;
+}
+
+
+
+let rec nil = {
+ tag = QName.nil;
+ kind = Tree.NodeKind.Element;
+ preorder = -1;
+ data = "";
+ first_child = nil;
+ next_sibling = nil;
+ parent = nil;
+}
+
+let dummy_tag = QName.of_string "#dummy"
+let rec dummy = {
+ tag = dummy_tag;
+ kind = Tree.NodeKind.Element;
+ preorder = -1;
+ data = "";
+ first_child = dummy;
+ next_sibling = dummy;
+ parent = dummy;
+}
+
+
+type t = {
+ root : node;
+ size : int;
+ (* TODO add other intersting stuff *)
+}
+
+
+
+module Parser =
+struct
+
+ type context = {
+ mutable stack : node list;
+ text_buffer : Buffer.t;
+ mutable current_preorder : int;
+ }
+
+ let print_node_ptr fmt n =
+ Format.fprintf fmt "<%s>"
+ (if n == nil then "NIL" else
+ if n == dummy then "DUMMY" else
+ "NODE " ^ string_of_int n.preorder)
+
+ let debug_node fmt node =
+ Format.fprintf fmt "{ tag=%s; preorder=%i; data=%S; first_child=%a; next_sibling=%a; parent=%a }"
+ (QName.to_string node.tag)
+ node.preorder
+ node.data
+ print_node_ptr node.first_child
+ print_node_ptr node.next_sibling
+ print_node_ptr node.parent
+
+
+ let debug_ctx fmt ctx =
+ Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\n-------------\n"
+ ctx.current_preorder
+ (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
+
+
+ let push n ctx = ctx.stack <- n :: ctx.stack
+ let pop ctx =
+ match ctx.stack with
+ [] -> failwith "XML parse error"
+ | e :: l -> ctx.stack <- l; e
+
+ let top ctx = match ctx.stack with
+ | [] -> failwith "XML parse error"
+ | e :: _ -> e
+
+ let next ctx =
+ let i = ctx.current_preorder in
+ ctx.current_preorder <- 1 + i;
+ i
+
+ let is_left n = n.next_sibling == dummy
+
+
+ let text_string = QName.to_string QName.text
+ let comment_string = QName.to_string QName.comment
+
+
+ let rec start_element_handler parser_ ctx tag attr_list =
+ do_text parser_ ctx;
+ let parent = top ctx in
+ let n = { tag = QName.of_string tag;
+ kind = Tree.NodeKind.Element;
+ preorder = next ctx;
+ data = "";
+ first_child = dummy;
+ next_sibling = dummy;
+ parent = parent;
+ }
+ in
+ if parent.first_child == dummy then parent.first_child <- n
+ else parent.next_sibling <- n;
+ push n ctx;
+ List.iter (do_attribute parser_ ctx) attr_list
+
+ and do_attribute parser_ ctx (att, value) =
+ let att_tag = QName.to_string (QName.attribute (QName.of_string att)) in
+ start_element_handler parser_ ctx att_tag [];
+ let n = top ctx in
+ n.data <- value;
+ n.kind <- Tree.NodeKind.Attribute;
+ end_element_handler parser_ ctx att_tag
+
+ and consume_closing ctx n =
+ if n.next_sibling != dummy then
+ let _ = pop ctx in consume_closing ctx (top ctx)
+
+ and end_element_handler parser_ ctx _ =
+ do_text parser_ ctx;
+ let node = top ctx in
+ if node.first_child == dummy then node.first_child <- nil
+ else begin
+ node.next_sibling <- nil;
+ consume_closing ctx node
+ end
+
+ and do_text parser_ ctx =
+ if Buffer.length ctx.text_buffer != 0 then
+ let s = Buffer.contents ctx.text_buffer in
+ Buffer.clear ctx.text_buffer;
+ start_element_handler parser_ ctx text_string [];
+ let node = top ctx in
+ node.data <- s;
+ node.kind <- Tree.NodeKind.Text;
+ end_element_handler parser_ ctx text_string
+
+ and comment_handler parser_ ctx s =
+ do_text parser_ ctx;
+ start_element_handler parser_ ctx comment_string [];
+ let node = top ctx in
+ node.data <- s;
+ node.kind <- Tree.NodeKind.Comment;
+ end_element_handler parser_ ctx comment_string
+
+ and processing_instruction_handler parser_ ctx tag data =
+ do_text parser_ ctx;
+ let pi = QName.to_string
+ (QName.processing_instruction (QName.of_string tag))
+ in
+ start_element_handler parser_ ctx pi [];
+ let node = top ctx in
+ node.data <- data;
+ node.kind <- Tree.NodeKind.ProcessingInstruction;
+ end_element_handler parser_ ctx pi
+
+
+ let character_data_handler _parser ctx text =
+ Buffer.add_string ctx.text_buffer text
+
+ let create_parser () =
+ let ctx = { text_buffer = Buffer.create 512;
+ current_preorder = 0;
+ stack = [] } in
+ let psr = Expat.parser_create ~encoding:None in
+ Expat.set_start_element_handler psr (start_element_handler psr ctx);
+ Expat.set_end_element_handler psr (end_element_handler psr ctx);
+ Expat.set_character_data_handler
+ psr (character_data_handler psr ctx);
+ Expat.set_comment_handler psr (comment_handler psr ctx);
+ Expat.set_processing_instruction_handler psr
+ (processing_instruction_handler psr ctx);
+ push { tag = QName.document;
+ preorder = next ctx;
+ kind = Tree.NodeKind.Document;
+ data = "";
+ first_child = dummy;
+ next_sibling = dummy;
+ parent = nil;
+ } ctx;
+ (psr,
+ fun () ->
+ let node = top ctx in
+ node.next_sibling <- nil;
+ consume_closing ctx node;
+ match ctx.stack with
+ [ root ] ->
+ root.next_sibling <- nil;
+ { root = root;
+ size = ctx.current_preorder
+ }
+ | _ -> raise (Expat.Expat_error Expat.UNCLOSED_TOKEN)
+ )
+
+
+ let parse_string s =
+ let parser_, finalize = create_parser () in
+ Expat.parse parser_ s;
+ finalize ()
+
+ let parse_file fd =
+ let buffer = String.create 4096 in
+ let parser_, finalize = create_parser () in
+ let rec loop () =
+ let read = input fd buffer 0 4096 in
+ if read != 0 then
+ let () = Expat.parse_sub parser_ buffer 0 read in
+ loop ()
+ in loop (); finalize ()
+
+end
+
+
+let load_xml_file = Parser.parse_file
+let load_xml_string = Parser.parse_string
+
+let output_escape_string out s =
+ for i = 0 to String.length s - 1 do
+ match s.[i] with
+ | '<' -> output_string out "<"
+ | '>' -> output_string out ">"
+ | '&' -> output_string out "&"
+ | '"' -> output_string out """
+ | '\'' -> output_string out "'"
+ | c -> output_char out c
+ done
+
+
+let rec print_attributes ?(sep=true) out tree_ node =
+ if (node.kind == Tree.NodeKind.Attribute) then
+ let tag = QName.to_string (QName.remove_prefix node.tag) in
+ if sep then output_char out ' ';
+ output_string out tag;
+ output_string out "=\"";
+ output_escape_string out node.data;
+ output_char out '\"';
+ print_attributes out tree_ node.next_sibling
+ else
+ node
+
+let rec print_xml out tree_ node =
+ if node != nil then
+ let () =
+ let open Tree.NodeKind in
+ match node.kind with
+ | Node -> ()
+ | Text -> output_escape_string out node.data
+ | Element | Document ->
+ let tag = QName.to_string node.tag in
+ output_char out '<';
+ output_string out tag;
+ let fchild = print_attributes out tree_ node.first_child in
+ if fchild == nil then output_string out "/>"
+ else begin
+ output_char out '>';
+ print_xml out tree_ fchild;
+ output_string out "</";
+ output_string out tag;
+ output_char out '>'
+ end
+ | Attribute -> ignore (print_attributes ~sep:false out tree_ node)
+ | Comment ->
+ output_string out "<!--";
+ output_string out node.data;
+ output_string out "-->"
+ | ProcessingInstruction ->
+ output_string out "<?";
+ output_string out (QName.to_string (QName.remove_prefix node.tag));
+ output_char out ' ';
+ output_string out node.data;
+ output_string out "?>"
+ in
+ print_xml out tree_ node.next_sibling
+
+let print_xml out tree_ node =
+ let nnode = { node with next_sibling = nil } in print_xml out tree_ nnode
+
+let root t = t.root
+let size t = t.size
+let first_child _ n = n.first_child
+let next_sibling _ n = n.next_sibling
+let parent _ n = n.parent
+let tag _ n = n.tag
+let data _ n = n.data
+let kind _ n = n.kind
+let preorder _ n = n.preorder
+
+let print_node fmt n = Parser.debug_node fmt n
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:44:39 CEST by Kim Nguyen>
+*)
+
+include Tree.S
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-09 10:41:21 CET by Kim Nguyen>
+*)
+
+open Format
+
+exception InvalidUtf8Codepoint of int
+
+let subscripts = "₀₁₂₃₄₅₆₇₈₉"
+let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
+
+let char_length c =
+ let code = Char.code c in
+ if code <= 0x7f then 1
+ else if 0xc2 <= code && code <= 0xdf then 2
+ else if 0xe0 <= code && code <= 0xef then 3
+ else if 0xf0 <= code && code <= 0xf4 then 4
+ else raise (InvalidUtf8Codepoint code)
+
+
+let next_char s i len =
+ let n = i + char_length s.[i] in
+ if n >= len then -1 else n
+
+let str_len s =
+ let len = String.length s in
+ let rec loop i acc =
+ if i == -1 then acc
+ else loop (next_char s i len) (acc+1)
+ in
+ loop 0 0
+
+let length = str_len
+
+let get_char s i =
+ let len = String.length s in
+ let rec loop j count =
+ if count == i then String.sub s j (char_length s.[j])
+ else loop (next_char s j len) (count+1)
+ in
+ loop 0 0
+
+
+let format_number digits i =
+ let s = string_of_int i in
+ let len = String.length s in
+ let buf = Buffer.create (len*4) in
+ for i = 0 to len - 1 do
+ let d = Char.code s.[i] - Char.code '0' in
+ Buffer.add_string buf (get_char digits d)
+ done;
+ Buffer.contents buf
+
+let rev_explode s =
+ let len = str_len s in
+ let rec loop i acc =
+ if i >= len then acc
+ else
+ loop (i+1) ((get_char s i) :: acc)
+ in
+ loop 0 []
+
+
+let explode s = List.rev (rev_explode s)
+
+let combine_all comp s =
+ let l = rev_explode s in
+ String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
+
+
+let subscript = format_number subscripts
+let superscript = format_number superscripts
+let down_arrow = "↓"
+let up_arrow = "↑"
+let right_arrow = "→"
+let left_arrow = "←"
+let epsilon = "ϵ"
+let big_sigma = "∑"
+let cap = "∩"
+let cup = "∪"
+let lnot = "¬"
+let wedge = "∧"
+let vee = "∨"
+let top = "⊤"
+let bottom = "⊥"
+let dummy = "☠"
+let inverse = "⁻¹"
+let double_right_arrow = "⇒"
+let combining_overbar = "\204\133"
+let combining_underbar = "\204\178"
+let combining_stroke = "\204\182"
+let combining_vertical_line = "\226\131\146"
+
+
+let overline s = combine_all combining_overbar s
+let underline s = combine_all combining_underbar s
+let strike s = combine_all combining_stroke s
+
+let padding i = String.make i ' '
+let line i = String.make i '_'
+
+
+
+
+let ppf f fmt s =
+ pp_print_string fmt (f s)
+
+let pp_overline = ppf overline
+let pp_underline = ppf underline
+let pp_strike = ppf strike
+let pp_subscript = ppf subscript
+let pp_superscript = ppf superscript
+let dummy_printer _ () = ()
+
+let pp_print_list ?(sep=dummy_printer) printer fmt l =
+ match l with
+ [] -> ()
+ | [ e ] -> printer fmt e
+ | e :: es -> printer fmt e; List.iter
+ (fun x ->
+ sep fmt ();
+ fprintf fmt "%a" printer x) es
+
+let pp_print_array ?(sep=dummy_printer) printer fmt a =
+ pp_print_list ~sep:sep printer fmt (Array.to_list a)
+
+let print_list ?(sep=" ") printer fmt l =
+ let sep_printer fmt () =
+ pp_print_string fmt sep
+ in
+ pp_print_list ~sep:sep_printer printer fmt l
+
+let print_array ?(sep=" ") printer fmt a =
+ print_list ~sep:sep printer fmt (Array.to_list a)
+
+
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-09 10:41:32 CET by Kim Nguyen>
+*)
+
+exception InvalidUtf8Codepoint of int
+
+val subscript : int -> string
+val superscript : int -> string
+val down_arrow : string
+val up_arrow : string
+val right_arrow : string
+val left_arrow : string
+val epsilon : string
+val big_sigma : string
+val cap : string
+val cup : string
+val lnot : string
+val wedge : string
+val vee : string
+val top : string
+val bottom : string
+val dummy : string
+val inverse : string
+val double_right_arrow : string
+val overline : string -> string
+val underline : string -> string
+val strike : string -> string
+val padding : int -> string
+val line : int -> string
+val length : string -> int
+val pp_overline : Format.formatter -> string -> unit
+val pp_underline : Format.formatter -> string -> unit
+val pp_strike : Format.formatter -> string -> unit
+val pp_subscript : Format.formatter -> int -> unit
+val pp_superscript : Format.formatter -> int -> unit
+
+val pp_print_list :
+ ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val pp_print_array :
+ ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
+val print_list : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val print_array : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
--- /dev/null
+(* Original file: *)
+(***********************************************************************)
+(* *)
+(* Copyright (C) Jean-Christophe Filliatre *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-10 18:18:54 CET by Kim Nguyen>
+*)
+
+(* Modified by Kim Nguyen *)
+(* The Patricia trees are themselves deeply hash-consed. The module
+ provides a Make (and Weak) functor to build hash-consed patricia
+ trees whose elements are Abstract hash-consed values.
+*)
+
+INCLUDE "utils.ml"
+
+include Ptset_sig
+
+module type HConsBuilder =
+ functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
+ S with type elt = H.t =
+struct
+ type elt = H.t
+
+ type 'a set =
+ | Empty
+ | Leaf of elt
+ | Branch of int * int * 'a * 'a
+
+ module rec Node : Hcons.S with type data = Data.t = HCB(Data)
+ and Data : Common_sig.HashedType with type t = Node.t set =
+ struct
+ type t = Node.t set
+ let equal x y =
+ match x,y with
+ | Empty,Empty -> true
+ | Leaf k1, Leaf k2 -> k1 == k2
+ | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
+ b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
+
+ | (Empty|Leaf _|Branch _), _ -> false
+
+ let hash = function
+ | Empty -> 0
+ | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
+ | Branch (b,i,l,r) ->
+ HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
+ end
+
+ include Node
+
+ let empty = Node.make Empty
+
+ let is_empty s = (Node.node s) == Empty
+
+ let branch p m l r = Node.make (Branch(p,m,l,r))
+
+ let leaf k = Node.make (Leaf k)
+
+ (* To enforce the invariant that a branch contains two non empty
+ sub-trees *)
+ let branch_ne p m t0 t1 =
+ if (is_empty t0) then t1
+ else if is_empty t1 then t0 else branch p m t0 t1
+
+ (******** from here on, only use the smart constructors ************)
+
+ let zero_bit k m = (k land m) == 0
+
+ let singleton k = leaf k
+
+ let is_singleton n =
+ match Node.node n with
+ | Leaf _ -> true
+ | Branch _ | Empty -> false
+
+ let mem (k:elt) n =
+ let kid = Uid.to_int (H.uid k) in
+ let rec loop n = match Node.node n with
+ | Empty -> false
+ | Leaf j -> k == j
+ | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
+ in loop n
+
+ let rec min_elt n = match Node.node n with
+ | Empty -> raise Not_found
+ | Leaf k -> k
+ | Branch (_,_,s,_) -> min_elt s
+
+ let rec max_elt n = match Node.node n with
+ | Empty -> raise Not_found
+ | Leaf k -> k
+ | Branch (_,_,_,t) -> max_elt t
+
+ let elements s =
+ let rec elements_aux acc n = match Node.node n with
+ | Empty -> acc
+ | Leaf k -> k :: acc
+ | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
+ in
+ elements_aux [] s
+
+ let mask k m = (k lor (m-1)) land (lnot m)
+
+ let naive_highest_bit x =
+ assert (x < 256);
+ let rec loop i =
+ if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
+ in
+ loop 7
+
+ let hbit = Array.init 256 naive_highest_bit
+ (*
+ external clz : int -> int = "caml_clz" "noalloc"
+ external leading_bit : int -> int = "caml_leading_bit" "noalloc"
+ *)
+ let highest_bit x =
+ try
+ let n = (x) lsr 24 in
+ if n != 0 then hbit.(n) lsl 24
+ else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
+ else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
+ else hbit.(x)
+ with
+ _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
+
+ let highest_bit64 x =
+ let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
+ else highest_bit x
+
+ let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
+
+ let join p0 t0 p1 t1 =
+ let m = branching_bit p0 p1 in
+ let msk = mask p0 m in
+ if zero_bit p0 m then
+ branch_ne msk m t0 t1
+ else
+ branch_ne msk m t1 t0
+
+ let match_prefix k p m = (mask k m) == p
+
+ let add k t =
+ let kid = Uid.to_int (H.uid k) in
+ assert (kid >=0);
+ let rec ins n = match Node.node n with
+ | Empty -> leaf k
+ | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
+ | Branch (p,m,t0,t1) ->
+ if match_prefix kid p m then
+ if zero_bit kid m then
+ branch_ne p m (ins t0) t1
+ else
+ branch_ne p m t0 (ins t1)
+ else
+ join kid (leaf k) p n
+ in
+ ins t
+
+ let remove k t =
+ let kid = Uid.to_int(H.uid k) in
+ let rec rmv n = match Node.node n with
+ | Empty -> empty
+ | Leaf j -> if k == j then empty else n
+ | Branch (p,m,t0,t1) ->
+ if match_prefix kid p m then
+ if zero_bit kid m then
+ branch_ne p m (rmv t0) t1
+ else
+ branch_ne p m t0 (rmv t1)
+ else
+ n
+ in
+ rmv t
+
+ (* should run in O(1) thanks to hash consing *)
+
+ let equal a b = Node.equal a b
+
+ let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
+
+ let rec merge s t =
+ if equal s t (* This is cheap thanks to hash-consing *)
+ then s
+ else
+ match Node.node s, Node.node t with
+ | Empty, _ -> t
+ | _, Empty -> s
+ | Leaf k, _ -> add k t
+ | _, Leaf k -> add k s
+ | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
+ if m == n && match_prefix q p m then
+ branch p m (merge s0 t0) (merge s1 t1)
+ else if m > n && match_prefix q p m then
+ if zero_bit q m then
+ branch_ne p m (merge s0 t) s1
+ else
+ branch_ne p m s0 (merge s1 t)
+ else if m < n && match_prefix p q n then
+ if zero_bit p n then
+ branch_ne q n (merge s t0) t1
+ else
+ branch_ne q n t0 (merge s t1)
+ else
+ (* The prefixes disagree. *)
+ join p s q t
+
+
+
+
+ let rec subset s1 s2 = (equal s1 s2) ||
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> true
+ | _, Empty -> false
+ | Leaf k1, _ -> mem k1 s2
+ | Branch _, Leaf _ -> false
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ if m1 == m2 && p1 == p2 then
+ subset l1 l2 && subset r1 r2
+ else if m1 < m2 && match_prefix p1 p2 m2 then
+ if zero_bit p1 m2 then
+ subset l1 l2 && subset r1 l2
+ else
+ subset l1 r2 && subset r1 r2
+ else
+ false
+
+
+ let union s1 s2 = merge s1 s2
+ (* Todo replace with e Memo Module *)
+
+ let rec inter s1 s2 =
+ if equal s1 s2
+ then s1
+ else
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> empty
+ | _, Empty -> empty
+ | Leaf k1, _ -> if mem k1 s2 then s1 else empty
+ | _, Leaf k2 -> if mem k2 s1 then s2 else empty
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ if m1 == m2 && p1 == p2 then
+ merge (inter l1 l2) (inter r1 r2)
+ else if m1 > m2 && match_prefix p2 p1 m1 then
+ inter (if zero_bit p2 m1 then l1 else r1) s2
+ else if m1 < m2 && match_prefix p1 p2 m2 then
+ inter s1 (if zero_bit p1 m2 then l2 else r2)
+ else
+ empty
+
+ let rec diff s1 s2 =
+ if equal s1 s2
+ then empty
+ else
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> empty
+ | _, Empty -> s1
+ | Leaf k1, _ -> if mem k1 s2 then empty else s1
+ | _, Leaf k2 -> remove k2 s1
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ if m1 == m2 && p1 == p2 then
+ merge (diff l1 l2) (diff r1 r2)
+ else if m1 > m2 && match_prefix p2 p1 m1 then
+ if zero_bit p2 m1 then
+ merge (diff l1 s2) r1
+ else
+ merge l1 (diff r1 s2)
+ else if m1 < m2 && match_prefix p1 p2 m2 then
+ if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
+ else
+ s1
+
+
+ (*s All the following operations ([cardinal], [iter], [fold], [for_all],
+ [exists], [filter], [partition], [choose], [elements]) are
+ implemented as for any other kind of binary trees. *)
+
+ let rec cardinal n = match Node.node n with
+ | Empty -> 0
+ | Leaf _ -> 1
+ | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
+
+ let rec iter f n = match Node.node n with
+ | Empty -> ()
+ | Leaf k -> f k
+ | Branch (_,_,t0,t1) -> iter f t0; iter f t1
+
+ let rec fold f s accu = match Node.node s with
+ | Empty -> accu
+ | Leaf k -> f k accu
+ | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
+
+
+ let rec for_all p n = match Node.node n with
+ | Empty -> true
+ | Leaf k -> p k
+ | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
+
+ let rec exists p n = match Node.node n with
+ | Empty -> false
+ | Leaf k -> p k
+ | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
+
+ let rec filter pr n = match Node.node n with
+ | Empty -> empty
+ | Leaf k -> if pr k then n else empty
+ | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
+
+ let partition p s =
+ let rec part (t,f as acc) n = match Node.node n with
+ | Empty -> acc
+ | Leaf k -> if p k then (add k t, f) else (t, add k f)
+ | Branch (_,_,t0,t1) -> part (part acc t0) t1
+ in
+ part (empty, empty) s
+
+ let rec choose n = match Node.node n with
+ | Empty -> raise Not_found
+ | Leaf k -> k
+ | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
+
+
+ let split x s =
+ let coll k (l, b, r) =
+ if k < x then add k l, b, r
+ else if k > x then l, b, add k r
+ else l, true, r
+ in
+ fold coll s (empty, false, empty)
+
+ (*s Additional functions w.r.t to [Set.S]. *)
+
+ let rec intersect s1 s2 = (equal s1 s2) ||
+ match (Node.node s1,Node.node s2) with
+ | Empty, _ -> false
+ | _, Empty -> false
+ | Leaf k1, _ -> mem k1 s2
+ | _, Leaf k2 -> mem k2 s1
+ | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+ if m1 == m2 && p1 == p2 then
+ intersect l1 l2 || intersect r1 r2
+ else if m1 > m2 && match_prefix p2 p1 m1 then
+ intersect (if zero_bit p2 m1 then l1 else r1) s2
+ else if m1 < m2 && match_prefix p1 p2 m2 then
+ intersect s1 (if zero_bit p1 m2 then l2 else r2)
+ else
+ false
+
+
+ let from_list l = List.fold_left (fun acc e -> add e acc) empty l
+
+
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
+
+module PosInt
+ =
+struct
+ include Make(Hcons.PosInt)
+ let print ppf s =
+ Format.pp_print_string ppf "{ ";
+ iter (fun i -> Format.fprintf ppf "%i " i) s;
+ Format.pp_print_string ppf "}";
+ Format.pp_print_flush ppf ()
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 22:42:37 CET by Kim Nguyen>
+*)
+
+include module type of Ptset_sig
+
+module Make (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed sets of hashconsed elements.
+ See {!Hcons.Make}.
+*)
+
+module Weak (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed sets of hashconsed elements
+ with weak internal storage. See {!Hcons.Weak}.
+*)
+
+module PosInt : S with type elt = int
+(** Implementation of hashconsed sets of positive integers *)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 23:32:36 CET by Kim Nguyen>
+*)
+
+module type S =
+sig
+ include Hcons.S
+ include Common_sig.Set with type t := t
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-10 23:05:56 CET by Kim Nguyen>
+*)
+
+include Hcons.Make (struct
+ include String
+ let hash s = Hashtbl.hash s
+ let equal s1 s2 = s1 = s2
+end)
+
+let print pp s = Format.fprintf pp "%s" s.node
+
+let of_string = make
+let to_string = node
+
+let document = of_string "#document"
+let text = of_string "#text"
+let comment = of_string "#comment"
+let nil = of_string "#"
+
+let attribute t = of_string ( "@" ^ (to_string t))
+let processing_instruction t = of_string ( "?" ^ (to_string t))
+
+let remove_prefix t =
+ let s = to_string t in
+ let lens = String.length s in
+ if lens == 0 then t
+ else
+ if s.[0] == '@' || s.[0] == '?' then
+ of_string (String.sub s 1 (lens-1))
+ else
+ t
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-10 23:02:12 CET by Kim Nguyen>
+*)
+
+(** Implementation of qualified names as hashconsed strings *)
+
+include Hcons.S with type data = string
+include Common_sig.Printable with type t := t
+
+
+val of_string : string -> t
+(** Utility function, equivalent to [make] *)
+
+val to_string : t -> string
+(** Utility function, equivalent to [node] *)
+
+
+(** Special constants, that denote the QName of nodes that are not
+ elements (using the nodeValue property of DOM for such nodes.
+*)
+
+val document : t
+(** Represents the QName of a document node. Equivalent to
+ [of_string "#document"]
+*)
+
+val text : t
+(** Represents the QName of a text node. Equivalent to
+ [of_string "#text"]
+*)
+
+val comment : t
+(** Represents the QName of a comment node. Equivalent to
+ [of_string "#comment"]
+*)
+
+val nil : t
+(** Represents the QName of a nil node. Equivalent to
+ [of_string "#"]
+*)
+
+val attribute : t -> t
+(** Adds a prefix character (@) to distinguish the name
+ from an element name
+*)
+
+val processing_instruction : t -> t
+(** Adds a prefix character (?) to distinguish the name
+ from an element name
+*)
+
+val remove_prefix : t -> t
+(** Removes the prefix of the qname given as argument. Does not
+ do anything if there is no prefix.
+*)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-09 17:54:35 CET by Kim Nguyen>
+*)
+
+include FiniteCofinite.Make(Ptset.Make(QName))
+
+let print_finite fmt e conv =
+ Format.fprintf fmt "{";
+ Pretty.print_list ~sep:"," QName.print fmt (conv e);
+ Format.fprintf fmt "}"
+
+let printer fmt e test conv inv is_any =
+ if test e then print_finite fmt e conv
+ else
+ let () = Format.fprintf fmt "%s" Pretty.big_sigma in
+ if not (is_any e) then begin Format.fprintf fmt "-";print_finite fmt (inv e) conv end
+
+let print fmt e = printer fmt e is_finite elements complement is_any
+
+let specials = [ QName.document; QName.text; QName.text ]
+let notstar = from_list specials
+let star = diff any notstar
+let node = any
+let text = singleton QName.text
+
+module Weak =
+struct
+ include FiniteCofinite.Weak(Ptset.Weak(QName))
+ let print fmt e = printer fmt e is_finite elements complement is_any
+ let notstar = from_list specials
+ let star = diff any notstar
+ let node = any
+ let text = singleton QName.text
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-09 17:53:53 CET by Kim Nguyen>
+*)
+
+(** Implementation of sets of Qualified Names that can be finite
+ or cofinite *)
+
+include FiniteCofinite.S with type elt = QName.t
+include Common_sig.Printable with type t := t
+val star : t
+val text : t
+val node : t
+
+module Weak :
+sig
+ include FiniteCofinite.S with type elt = QName.t
+ include Common_sig.Printable with type t := t
+ val star : t
+ val text : t
+ val node : t
+end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:45:59 CEST by Kim Nguyen>
+*)
+
+open Format
+
+type t = int
+let make =
+ let id = ref ~-1 in
+ fun () -> incr id; !id
+
+let compare = (-)
+
+let equal = (==)
+
+external hash : t -> int = "%identity"
+
+let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
+
+let dump fmt x = print fmt x
+
+let check x =
+ if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
+
+let dummy = max_int
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-03-04 23:02:21 CET by Kim Nguyen>
+*)
+
+(** Implementation of states *)
+
+include Common_sig.Type with type t = int
+
+val make : unit -> t
+(** Generate a fresh state *)
+
+val dummy : t
+(** Dummy state that can never be returned by [make ()] *)
+
+val print : Format.formatter -> t -> unit
+(** Pretty printer *)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:46:16 CEST by Kim Nguyen>
+*)
+
+open Format
+
+include Ptset.Make (Hcons.PosInt)
+
+let print ppf s =
+ fprintf ppf "{ %a }"
+ (Pretty.print_list ~sep:" " (State.print)) (elements s)
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:41:31 CEST by Kim Nguyen>
+*)
+
+(** Implementation of sets of states *)
+include Ptset.S with type elt = int
+
+val print : Format.formatter -> t -> unit
+(** Pretty printer *)
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 21:29:17 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:45:43 CEST by Kim Nguyen>
*)
let doc =
let fd = open_in Sys.argv.(1) in
- let d = Tree.Naive.load_xml_file fd in
+ let d = Naive_tree.load_xml_file fd in
close_in fd; d
let () =
fprintf err_formatter "Query: %a\n%!" Xpath.Ast.print_path query;
- fprintf err_formatter "Automata: %a\n%!" Auto.Ata.print auto;
+ fprintf err_formatter "Automata: %a\n%!" Ata.print auto;
fprintf err_formatter "Evaluating automaton:\n%!";
- let module Naive = Auto.Eval.Make(Tree.Naive) in
+ let module Naive = Eval.Make(Naive_tree) in
let t1 = Unix.gettimeofday() in
- let results = Naive.eval auto doc (Tree.Naive.root doc) in
+ let results = Naive.eval auto doc (Naive_tree.root doc) in
let teval = (Unix.gettimeofday () -. t1) *. 1000. in
let t1 = Unix.gettimeofday () in
output_string stdout "<xml_result>\n";
List.iter (fun n ->
- Tree.Naive.print_xml stdout doc n;
+ Naive_tree.print_xml stdout doc n;
output_char stdout '\n'
) results;
output_string stdout "</xml_result>\n";
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:40:39 CEST by Kim Nguyen>
+*)
+
+(** The different kind of XML nodes and utility functions *)
+
+module NodeKind =
+ struct
+ type t =
+ Document | Element | Text | Comment | Attribute | ProcessingInstruction | Node
+
+ let to_string =
+ function
+ Document -> "document"
+ | Element -> "element"
+ | Attribute -> "attribute"
+ | Text -> "text"
+ | Comment -> "comment"
+ | ProcessingInstruction -> "processing-instruction"
+ | Node -> "node"
+
+ let print ppf k = Format.fprintf ppf "%s" (to_string k)
+
+
+ let is_a k1 k2 =
+ k1 == Node || k2 == Node || k1 == k2
+end
+
+
+(** Signatures for trees *)
+
+module type S =
+sig
+ type node
+ (** The type of a tree node *)
+
+ type t
+ (** The type of trees *)
+
+ val size : t -> int
+ (** Return the number of nodes *)
+
+ val nil : node
+ (** Nil node, denoting the first/second child of a leaf or the parent of
+ the root *)
+
+ val dummy : node
+ (** Dummy node that is guaranteed to never occur in any tree *)
+
+ val load_xml_file : in_channel -> t
+ (** Takes a file descriptor and returns the XML data stored in the
+ corresponding file. Start at the current position in the file
+ descriptor (which is not necessarily the begining of file)
+ *)
+
+ val load_xml_string : string -> t
+ (** Loads XML data stored in a string *)
+
+ val print_xml : out_channel -> t -> node -> unit
+ (** Outputs the tree as an XML document on the given output_channel *)
+
+ val root : t -> node
+ (** Returns the root of the tree *)
+
+ val first_child : t -> node -> node
+ (** [first_child t n] returns the first child of node [n] in tree [t].
+ Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
+ *)
+
+ val next_sibling : t -> node -> node
+ (** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
+ Returns [nil] if [n] is the last child of a node.
+ Returns [nil] if [n == nil].
+ *)
+
+ val parent : t -> node -> node
+ (** [next_sibling t n] returns the parent of node [n] in tree [t].
+ Returns [nil] if [n] is the root of the tree.
+ Returns [nil] if [n == nil].
+ *)
+
+ val tag : t -> node -> QName.t
+ (** Returns the label of a given node *)
+
+ val data : t -> node -> string
+ (** Returns the character data associated with a node.
+ The only node having character data are those whose label is
+ QName.text, QName.cdata_section or QName.comment
+ *)
+
+ val kind : t -> node -> NodeKind.t
+ (** Returns the kind of the given node *)
+
+ val preorder : t -> node -> int
+ (** Returns the position of a node in pre-order in the tree. The
+ root has preorder 0. [nil] has pre-order [-1].
+ *)
+
+ val print_node : Format.formatter -> node -> unit
+end
+++ /dev/null
-tree/Naive
-tree/Sig
-tree/Common
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-11 00:11:53 CET by Kim Nguyen>
-*)
-
-module NodeKind =
- struct
- type t =
- Document | Element | Text | Comment | Attribute | ProcessingInstruction
- | Node
-
- let to_string =
- function
- Document -> "document"
- | Element -> "element"
- | Attribute -> "attribute"
- | Text -> "text"
- | Comment -> "comment"
- | ProcessingInstruction -> "processing-instruction"
- | Node -> "node"
- let print ppf k = Format.fprintf ppf "%s" (to_string k)
-
-
- let is_a k1 k2 =
- k1 == Node || k2 == Node || k1 == k2
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-13 18:47:18 CET by Kim Nguyen>
-*)
-open Utils
-
-type node = {
- tag : QName.t;
- preorder : int;
- mutable kind : Common.NodeKind.t;
- mutable data : string;
- mutable first_child : node;
- mutable next_sibling : node;
- mutable parent: node;
-}
-
-
-
-let rec nil = {
- tag = QName.nil;
- kind = Common.NodeKind.Element;
- preorder = -1;
- data = "";
- first_child = nil;
- next_sibling = nil;
- parent = nil;
-}
-
-let dummy_tag = QName.of_string "#dummy"
-let rec dummy = {
- tag = dummy_tag;
- kind = Common.NodeKind.Element;
- preorder = -1;
- data = "";
- first_child = dummy;
- next_sibling = dummy;
- parent = dummy;
-}
-
-
-type t = {
- root : node;
- size : int;
- (* TODO add other intersting stuff *)
-}
-
-
-
-module Parser =
-struct
-
- type context = {
- mutable stack : node list;
- text_buffer : Buffer.t;
- mutable current_preorder : int;
- }
-
- let print_node_ptr fmt n =
- Format.fprintf fmt "<%s>"
- (if n == nil then "NIL" else
- if n == dummy then "DUMMY" else
- "NODE " ^ string_of_int n.preorder)
-
- let debug_node fmt node =
- Format.fprintf fmt "{ tag=%s; preorder=%i; data=%S; first_child=%a; next_sibling=%a; parent=%a }"
- (QName.to_string node.tag)
- node.preorder
- node.data
- print_node_ptr node.first_child
- print_node_ptr node.next_sibling
- print_node_ptr node.parent
-
-
- let debug_ctx fmt ctx =
- Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\n-------------\n"
- ctx.current_preorder
- (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
-
-
- let push n ctx = ctx.stack <- n :: ctx.stack
- let pop ctx =
- match ctx.stack with
- [] -> failwith "XML parse error"
- | e :: l -> ctx.stack <- l; e
-
- let top ctx = match ctx.stack with
- | [] -> failwith "XML parse error"
- | e :: _ -> e
-
- let next ctx =
- let i = ctx.current_preorder in
- ctx.current_preorder <- 1 + i;
- i
-
- let is_left n = n.next_sibling == dummy
-
-
- let text_string = QName.to_string QName.text
- let comment_string = QName.to_string QName.comment
-
-
- let rec start_element_handler parser_ ctx tag attr_list =
- do_text parser_ ctx;
- let parent = top ctx in
- let n = { tag = QName.of_string tag;
- kind = Common.NodeKind.Element;
- preorder = next ctx;
- data = "";
- first_child = dummy;
- next_sibling = dummy;
- parent = parent;
- }
- in
- if parent.first_child == dummy then parent.first_child <- n
- else parent.next_sibling <- n;
- push n ctx;
- List.iter (do_attribute parser_ ctx) attr_list
-
- and do_attribute parser_ ctx (att, value) =
- let att_tag = QName.to_string (QName.attribute (QName.of_string att)) in
- start_element_handler parser_ ctx att_tag [];
- let n = top ctx in
- n.data <- value;
- n.kind <- Common.NodeKind.Attribute;
- end_element_handler parser_ ctx att_tag
-
- and consume_closing ctx n =
- if n.next_sibling != dummy then
- let _ = pop ctx in consume_closing ctx (top ctx)
-
- and end_element_handler parser_ ctx _ =
- do_text parser_ ctx;
- let node = top ctx in
- if node.first_child == dummy then node.first_child <- nil
- else begin
- node.next_sibling <- nil;
- consume_closing ctx node
- end
-
- and do_text parser_ ctx =
- if Buffer.length ctx.text_buffer != 0 then
- let s = Buffer.contents ctx.text_buffer in
- Buffer.clear ctx.text_buffer;
- start_element_handler parser_ ctx text_string [];
- let node = top ctx in
- node.data <- s;
- node.kind <- Common.NodeKind.Text;
- end_element_handler parser_ ctx text_string
-
- and comment_handler parser_ ctx s =
- do_text parser_ ctx;
- start_element_handler parser_ ctx comment_string [];
- let node = top ctx in
- node.data <- s;
- node.kind <- Common.NodeKind.Comment;
- end_element_handler parser_ ctx comment_string
-
- and processing_instruction_handler parser_ ctx tag data =
- do_text parser_ ctx;
- let pi = QName.to_string
- (QName.processing_instruction (QName.of_string tag))
- in
- start_element_handler parser_ ctx pi [];
- let node = top ctx in
- node.data <- data;
- node.kind <- Common.NodeKind.ProcessingInstruction;
- end_element_handler parser_ ctx pi
-
-
- let character_data_handler _parser ctx text =
- Buffer.add_string ctx.text_buffer text
-
- let create_parser () =
- let ctx = { text_buffer = Buffer.create 512;
- current_preorder = 0;
- stack = [] } in
- let psr = Expat.parser_create ~encoding:None in
- Expat.set_start_element_handler psr (start_element_handler psr ctx);
- Expat.set_end_element_handler psr (end_element_handler psr ctx);
- Expat.set_character_data_handler
- psr (character_data_handler psr ctx);
- Expat.set_comment_handler psr (comment_handler psr ctx);
- Expat.set_processing_instruction_handler psr
- (processing_instruction_handler psr ctx);
- push { tag = QName.document;
- preorder = next ctx;
- kind = Common.NodeKind.Document;
- data = "";
- first_child = dummy;
- next_sibling = dummy;
- parent = nil;
- } ctx;
- (psr,
- fun () ->
- let node = top ctx in
- node.next_sibling <- nil;
- consume_closing ctx node;
- match ctx.stack with
- [ root ] ->
- root.next_sibling <- nil;
- { root = root;
- size = ctx.current_preorder
- }
- | _ -> raise (Expat.Expat_error Expat.UNCLOSED_TOKEN)
- )
-
-
- let parse_string s =
- let parser_, finalize = create_parser () in
- Expat.parse parser_ s;
- finalize ()
-
- let parse_file fd =
- let buffer = String.create 4096 in
- let parser_, finalize = create_parser () in
- let rec loop () =
- let read = input fd buffer 0 4096 in
- if read != 0 then
- let () = Expat.parse_sub parser_ buffer 0 read in
- loop ()
- in loop (); finalize ()
-
-end
-
-
-let load_xml_file = Parser.parse_file
-let load_xml_string = Parser.parse_string
-
-let output_escape_string out s =
- for i = 0 to String.length s - 1 do
- match s.[i] with
- | '<' -> output_string out "<"
- | '>' -> output_string out ">"
- | '&' -> output_string out "&"
- | '"' -> output_string out """
- | '\'' -> output_string out "'"
- | c -> output_char out c
- done
-
-
-let rec print_attributes ?(sep=true) out tree_ node =
- if (node.kind == Common.NodeKind.Attribute) then
- let tag = QName.to_string (QName.remove_prefix node.tag) in
- if sep then output_char out ' ';
- output_string out tag;
- output_string out "=\"";
- output_escape_string out node.data;
- output_char out '\"';
- print_attributes out tree_ node.next_sibling
- else
- node
-
-let rec print_xml out tree_ node =
- if node != nil then
- let () =
- let open Common.NodeKind in
- match node.kind with
- | Node -> ()
- | Text -> output_escape_string out node.data
- | Element | Document ->
- let tag = QName.to_string node.tag in
- output_char out '<';
- output_string out tag;
- let fchild = print_attributes out tree_ node.first_child in
- if fchild == nil then output_string out "/>"
- else begin
- output_char out '>';
- print_xml out tree_ fchild;
- output_string out "</";
- output_string out tag;
- output_char out '>'
- end
- | Attribute -> ignore (print_attributes ~sep:false out tree_ node)
- | Comment ->
- output_string out "<!--";
- output_string out node.data;
- output_string out "-->"
- | ProcessingInstruction ->
- output_string out "<?";
- output_string out (QName.to_string (QName.remove_prefix node.tag));
- output_char out ' ';
- output_string out node.data;
- output_string out "?>"
- in
- print_xml out tree_ node.next_sibling
-
-let print_xml out tree_ node =
- let nnode = { node with next_sibling = nil } in print_xml out tree_ nnode
-
-let root t = t.root
-let size t = t.size
-let first_child _ n = n.first_child
-let next_sibling _ n = n.next_sibling
-let parent _ n = n.parent
-let tag _ n = n.tag
-let data _ n = n.data
-let kind _ n = n.kind
-let preorder _ n = n.preorder
-
-let print_node fmt n = Parser.debug_node fmt n
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-05 14:08:25 CET by Kim Nguyen>
-*)
-
-include Sig.S
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-13 18:46:18 CET by Kim Nguyen>
-*)
-
-(** Implementation of documents as binary trees *)
-
-module type S =
-sig
- type node
- (** The type of a tree node *)
-
- type t
- (** The type of trees *)
-
- val size : t -> int
- (** Return the number of nodes *)
-
- val nil : node
- (** Nil node, denoting the first/second child of a leaf or the parent of
- the root *)
-
- val dummy : node
- (** Dummy node that is guaranteed to never occur in any tree *)
-
- val load_xml_file : in_channel -> t
- (** Takes a file descriptor and returns the XML data stored in the
- corresponding file. Start at the current position in the file
- descriptor (which is not necessarily the begining of file)
- *)
-
- val load_xml_string : string -> t
- (** Loads XML data stored in a string *)
-
- val print_xml : out_channel -> t -> node -> unit
- (** Outputs the tree as an XML document on the given output_channel *)
-
- val root : t -> node
- (** Returns the root of the tree *)
-
- val first_child : t -> node -> node
- (** [first_child t n] returns the first child of node [n] in tree [t].
- Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
- *)
-
- val next_sibling : t -> node -> node
- (** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
- Returns [nil] if [n] is the last child of a node.
- Returns [nil] if [n == nil].
- *)
-
- val parent : t -> node -> node
- (** [next_sibling t n] returns the parent of node [n] in tree [t].
- Returns [nil] if [n] is the root of the tree.
- Returns [nil] if [n == nil].
- *)
-
- val tag : t -> node -> Utils.QName.t
- (** Returns the label of a given node *)
-
- val data : t -> node -> string
- (** Returns the character data associated with a node.
- The only node having character data are those whose label is
- QName.text, QName.cdata_section or QName.comment
- *)
-
- val kind : t -> node -> Common.NodeKind.t
- (** Returns the kind of the given node *)
-
- val preorder : t -> node -> int
- (** Returns the position of a node in pre-order in the tree. The
- root has preorder 0. [nil] has pre-order [-1].
- *)
-
- val print_node : Format.formatter -> node -> unit
-end
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-01-30 19:06:39 CET by Kim Nguyen>
+*)
+
+type t = int
+
+exception Overflow
+let make_maker () =
+ let _id = ref ~-1 in
+ fun () ->
+ incr _id;
+ let i = !_id in
+ if i < 0 then raise Overflow else i
+
+let dummy = -1
+
+external to_int : t -> int = "%identity"
+external of_int : int -> t= "%identity"
--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(*
+ Time-stamp: <Last modified on 2013-01-30 19:06:33 CET by Kim Nguyen>
+*)
+
+(** This modules implements unique identifiers represented by integers *)
+
+type t = private int
+(** The type of unique identifiers. *)
+
+exception Overflow
+(** Raised when the internal counters for IDs overflows. *)
+
+val make_maker : unit -> (unit -> t)
+(** Returns an uid generator.
+ [make_maker ()] returns a function that generates unique ids. Raises
+ [Overflow] if the internal counter overflows.
+*)
+
+val dummy : t
+(** A dummy identifier, guaranteed to be distinct from any value
+ returned by a generator.
+*)
+
+external to_int : t -> int = "%identity"
+(** Convert a unique id to an integer *)
+
+(**/**)
+
+external of_int : int -> t = "%identity"
+(** May break the invariant, use with caution *)
+++ /dev/null
-utils/Cache
-utils/Common_sig
-utils/FiniteCofinite
-utils/FiniteCofinite_sig
-utils/Hcons
-utils/Hcons_sig
-utils/Hlist
-utils/Hlist_sig
-utils/Misc
-utils/Pretty
-utils/Ptset
-utils/Ptset_sig
-utils/QName
-utils/QNameSet
-utils/Uid
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-14 14:50:18 CET by Kim Nguyen>
-*)
-
-let realloc l old_size new_size dummy =
- let l' = Array.create new_size dummy in
- for i = 0 to (min old_size new_size) - 1 do
- Array.unsafe_set l' i (Array.unsafe_get l i);
- done;
- l'
-
-module N1 =
-struct
- type 'a t = { mutable line : 'a array;
- dummy : 'a;
- mutable offset : int;
- }
- let create a = {
- line = Array.create 0 a;
- dummy = a;
- offset = ~-1;
-
- }
-
- let print fmt a =
- Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!"
- a.offset
- (Pretty.print_array ~sep:", " (fun fmt x ->
- if x==a.dummy then
- Format.fprintf fmt "%s" "D"
- else
- Format.fprintf fmt "%s" "E")) a.line
-
- let add a i v =
- if a.offset == ~-1 then a.offset <- i;
- let offset = a.offset in
- let len = Array.length a.line in
- if i >= offset && i < offset + len then
- a.line.(i - offset) <- v
- else
- if i < offset then begin (* bottom resize *)
- let pad = offset - i in
- let nlen = len + pad in
- let narray = Array.create nlen a.dummy in
- for j = 0 to len - 1 do
- narray.(j+pad) <- a.line.(j)
- done;
- a.offset <- i;
- a.line <- narray;
- narray.(0) <- v;
- end else begin (* top resize *)
- (* preventively allocate the space for the following elements *)
- let nlen = ((i - offset + 1) lsl 1) + 1 in
- let narray = Array.create nlen a.dummy in
- for j = 0 to len - 1 do
- narray.(j) <- a.line.(j);
- done;
- narray.(i - offset) <- v;
- a.line <- narray
- end
-
- let find a i =
- let idx = i - a.offset in
- let len = Array.length a.line in
- if idx >= 0 && idx < len then
- Array.unsafe_get a.line idx
- else a.dummy
-
- let dummy a = a.dummy
-
- let iteri f a =
- let line = a.line in
- if a.offset == ~-1 then () else
- for i = 0 to Array.length line - 1 do
- let v = line.(i) in
- f (i+a.offset) v (v==a.dummy)
- done
-
-
-end
-
-module N2 =
-struct
- type 'a t = 'a N1.t N1.t
- let create a =
- let dummy1 = N1.create a in
- N1.create dummy1
-
- let add a i j v =
- let line = N1.find a i in
- if line == a.N1.dummy then
- let nline = N1.create line.N1.dummy in
- N1.add a i nline;
- N1.add nline j v
- else
- N1.add line j v
-
-
- let find a i j =
- let v = N1.find a i in
- if v == a.N1.dummy then v.N1.dummy
- else N1.find v j
-
-
- let dummy c = c.N1.dummy.N1.dummy
-
- let iteri f a =
- let line = a.N1.line in
- if a.N1.offset == ~-1 then () else
- for i = 0 to Array.length line - 1 do
- N1.iteri (f i) line.(i)
- done
-
-
-end
-
-module N3 =
-struct
- type 'a t = 'a N2.t N1.t
-
- let create a =
- let dummy2 = N2.create a in
- N1.create dummy2
-
- let add a i j k v =
- let line = N1.find a i in
- if line == a.N1.dummy then
- let nline = N1.create line.N1.dummy in
- N1.add a i nline;
- N2.add nline j k v
- else
- N2.add line j k v
-
- let find a i j k =
- let v = N1.find a i in
- if v == a.N1.dummy then N2.dummy v
- else N2.find v j k
-
-
- let dummy a = N2.dummy a.N1.dummy
- let iteri f a =
- let line = a.N1.line in
- if a.N1.offset == ~-1 then () else
- for i = 0 to Array.length line - 1 do
- N2.iteri (f i) line.(i)
- done
-
-end
-
-module N4 =
-struct
- type 'a t = 'a N3.t N1.t
-
- let create a =
- let dummy3 = N3.create a in
- N1.create dummy3
-
- let add a i j k l v =
- let line = N1.find a i in
- if line == N1.dummy a then
- let nline = N3.create (N3.dummy line) in
- N1.add a i nline;
- N3.add nline j k l v
- else
- N3.add line j k l v
-
- let find a i j k l =
- let v = N1.find a i in
- if v == (N1.dummy a) then N3.dummy v
- else N3.find v j k l
-
-
- let dummy a = N3.dummy (N1.dummy a)
- let iteri f a =
- N1.iteri (fun i v _ ->
- N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a
-
-end
-
-module N5 =
-struct
- type 'a t = 'a N4.t N1.t
-
- let create a =
- let dummy4 = N4.create a in
- N1.create dummy4
-
- let add a i j k l m v =
- let line = N1.find a i in
- if line == (N1.dummy a) then
- let nline = N4.create (N4.dummy line) in
- N1.add a i nline;
- N4.add nline j k l m v
- else
- N4.add line j k l m v
-
- let find a i j k l m =
- let v = N1.find a i in
- if v == (N1.dummy a) then N4.dummy v
- else N4.find v j k l m
-
-
- let dummy a = N4.dummy (N1.dummy a)
- let iteri f a =
- N1.iteri (fun i v _ ->
- N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v
- ) a
-end
-
-module N6 =
-struct
- type 'a t = 'a N5.t N1.t
-
- let create a =
- let dummy5 = N5.create a in
- N1.create dummy5
-
- let add a i j k l m n v =
- let line = N1.find a i in
- if line == N1.dummy a then
- let nline = N5.create (N5.dummy line) in
- N1.add a i nline;
- N5.add nline j k l m n v
- else
- N5.add line j k l m n v
-
- let find a i j k l m n =
- let v = N1.find a i in
- if v == N1.dummy a then N5.dummy v
- else N5.find v j k l m n
-
-
- let dummy a = N5.dummy (N1.dummy a)
- let iteri f a =
- N1.iteri (fun i v _ ->
- N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v
- ) a
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-14 13:42:53 CET by Kim Nguyen>
-*)
-
-(** N-dimentional caches *)
-
-module N1 :
-sig
-
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> 'a
- val add : 'a t -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit
-end
-
-module N2:
-sig
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> int -> 'a
- val add : 'a t -> int -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-end
-
-module N3 :
- sig
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> int -> int -> 'a
- val add : 'a t -> int -> int -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
- end
-
-module N4 :
- sig
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> int -> int -> int -> 'a
- val add : 'a t -> int -> int -> int -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
- end
-
-module N5 :
- sig
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> int -> int -> int -> int -> 'a
- val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
- end
-
-module N6 :
- sig
- type 'a t
- val create : 'a -> 'a t
- val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
- val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
- val dummy : 'a t -> 'a
- val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
- end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 23:01:55 CET by Kim Nguyen>
-*)
-
-(** Type equipped with an equality and hash function.
- If [equal a b] then [(hash a) = (hash b)]
-*)
-module type HashedType =
-sig
- type t
-
- (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
- *)
- val hash : t -> int
-
- (** Equality *)
- val equal : t -> t -> bool
-
-end
-
-(** Type equiped with a total ordering *)
-module type OrderedType =
-sig
- type t
-
- (** Total ordering on values of type [t]. [compare a b] returns a
- negative number if [a] is strictly smaller than [b], a positive
- number if [a] is strictly greater than [b] and 0 if [a] is equal
- to [b]. *)
- val compare : t -> t -> int
-end
-
-module type Type =
-sig
- type t
- include HashedType with type t := t
- include OrderedType with type t := t
-end
-
-(** Type equiped with a pretty-printer *)
-module type Printable =
-sig
- type t
- val print : Format.formatter -> t -> unit
-end
-
-(** Signature of a simple HashSet module *)
-module type HashSet =
-sig
- type data
- type t
- val create : int -> t
- val add : t -> data -> unit
- val remove : t -> data -> unit
- val find : t -> data -> data
- val find_all : t -> data -> data list
- val clear : t -> unit
- val mem : t -> data -> bool
-end
-
- (** Signature of simple Set module *)
-module type Set =
-sig
- type elt
- type t
- val empty : t
- val is_empty : t -> bool
- val mem : elt -> t -> bool
- val add : elt -> t -> t
- val singleton : elt -> t
- val remove : elt -> t -> t
- val union : t -> t -> t
- val inter : t -> t -> t
- val diff : t -> t -> t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val subset : t -> t -> bool
- val iter : (elt -> unit) -> t -> unit
- val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
- val for_all : (elt -> bool) -> t -> bool
- val exists : (elt -> bool) -> t -> bool
- val filter : (elt -> bool) -> t -> t
- val partition : (elt -> bool) -> t -> t * t
- val cardinal : t -> int
- val elements : t -> elt list
- val min_elt : t -> elt
- val max_elt : t -> elt
- val choose : t -> elt
- val split : elt -> t -> t * bool * t
- val intersect : t -> t -> bool
- val is_singleton : t -> bool
- val from_list : elt list -> t
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-include FiniteCofinite_sig
-
-module type HConsBuilder =
- functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (E : Ptset.S) :
- S with type elt = E.elt and type set = E.t =
-struct
- type elt = E.elt
- type node = Finite of E.t | CoFinite of E.t
- type set = E.t
- module Node = HCB(struct
- type t = node
- let equal a b =
- match a, b with
- Finite s1, Finite s2
- | CoFinite s1, CoFinite s2 -> E.equal s1 s2
- | (Finite _| CoFinite _), _ -> false
-
- let hash = function
- | Finite s -> HASHINT2 (PRIME1, E.hash s)
- | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
- end)
- include Node
- let empty = make (Finite E.empty)
- let any = make (CoFinite E.empty)
- let finite x = make (Finite x)
- let cofinite x = make (CoFinite x)
-
- let is_empty t = match t.node with
- | Finite s -> E.is_empty s
- | CoFinite _ -> false
-
- let is_any t = match t.node with
- | CoFinite s -> E.is_empty s
- | Finite _ -> false
-
- let is_finite t = match t.node with
- | Finite _ -> true
- | CoFinite _ -> false
-
- let kind t = match t.node with
- | Finite _ -> `Finite
- | CoFinite _ -> `Cofinite
-
- let mem x t = match t.node with
- | Finite s -> E.mem x s
- | CoFinite s -> not (E.mem x s)
-
- let singleton x = finite (E.singleton x)
-
- let add e t = match t.node with
- | Finite s -> finite (E.add e s)
- | CoFinite s -> cofinite (E.remove e s)
-
- let remove e t = match t.node with
- | Finite s -> finite (E.remove e s)
- | CoFinite s -> cofinite (E.add e s)
-
- let union s t = match s.node, t.node with
- | Finite s, Finite t -> finite (E.union s t)
- | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
- | Finite s, CoFinite t -> cofinite (E.diff t s)
- | CoFinite s, Finite t-> cofinite (E.diff s t)
-
- let inter s t = match s.node, t.node with
- | Finite s, Finite t -> finite (E.inter s t)
- | CoFinite s, CoFinite t -> cofinite (E.union s t)
- | Finite s, CoFinite t -> finite (E.diff s t)
- | CoFinite s, Finite t-> finite (E.diff t s)
-
- let diff s t = match s.node, t.node with
- | Finite s, Finite t -> finite (E.diff s t)
- | Finite s, CoFinite t -> finite(E.inter s t)
- | CoFinite s, Finite t -> cofinite(E.union t s)
- | CoFinite s, CoFinite t -> finite (E.diff t s)
-
- let complement t = match t.node with
- | Finite s -> cofinite s
- | CoFinite s -> finite s
-
- let compare s t = match s.node, t.node with
- | Finite s , Finite t -> E.compare s t
- | CoFinite s , CoFinite t -> E.compare t s
- | Finite _, CoFinite _ -> -1
- | CoFinite _, Finite _ -> 1
-
- let subset s t = match s.node, t.node with
- | Finite s , Finite t -> E.subset s t
- | CoFinite s , CoFinite t -> E.subset t s
- | Finite s, CoFinite t -> E.is_empty (E.inter s t)
- | CoFinite _, Finite _ -> false
-
- (* given a list l of type t list,
- returns two sets (f,c) where :
- - f is the union of all the finite sets of l
- - c is the union of all the cofinite sets of l
- - f and c are disjoint
- Invariant : cup f c = List.fold_left cup empty l
- We treat the CoFinite part explicitely :
- *)
-
- let kind_split l =
-
- let rec next_finite_cofinite facc cacc = function
- | [] -> finite facc, cofinite (E.diff cacc facc)
- | { node = Finite s; _ } ::r ->
- next_finite_cofinite (E.union s facc) cacc r
- | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
- next_finite_cofinite facc cacc r
- | { node = CoFinite s; _ } ::r ->
- next_finite_cofinite facc (E.inter cacc s) r
- in
- let rec first_cofinite facc = function
- | [] -> empty,empty
- | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
- | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
- in
- first_cofinite E.empty l
-
- let exn = FiniteCofinite_sig.InfiniteSet
-
- let fold f t a = match t.node with
- | Finite s -> E.fold f s a
- | CoFinite _ -> raise exn
-
- let iter f t = match t.node with
- | Finite t -> E.iter f t
- | CoFinite _ -> raise exn
-
- let for_all f t = match t.node with
- | Finite s -> E.for_all f s
- | CoFinite _ -> raise exn
-
- let exists f t = match t.node with
- | Finite s -> E.exists f s
- | CoFinite _ -> raise exn
-
- let filter f t = match t.node with
- | Finite s -> finite (E.filter f s)
- | CoFinite _ -> raise exn
-
- let partition f t = match t.node with
- | Finite s -> let a,b = E.partition f s in finite a,finite b
- | CoFinite _ -> raise exn
-
- let cardinal t = match t.node with
- | Finite s -> E.cardinal s
- | CoFinite _ -> raise exn
-
- let elements t = match t.node with
- | Finite s -> E.elements s
- | CoFinite _ -> raise exn
-
- let from_list l =
- finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
-
- let choose t = match t.node with
- Finite s -> E.choose s
- | CoFinite _ -> raise exn
-
- let is_singleton t = match t.node with
- | Finite s -> E.is_singleton s
- | CoFinite _ -> false
-
- let intersect s t = match s.node, t.node with
- | Finite s, Finite t -> E.intersect s t
- | CoFinite s, Finite t -> not (E.subset t s)
- | Finite s, CoFinite t -> not (E.subset s t)
- | CoFinite _ , CoFinite _ -> true
-
- let split x s = match s.node with
- | Finite s ->
- let s1, b, s2 = E.split x s in
- finite s1, b, finite s2
-
- | CoFinite _ -> raise exn
-
- let min_elt s = match s.node with
- | Finite s -> E.min_elt s
- | CoFinite _ -> raise exn
-
- let max_elt s = match s.node with
- | Finite s -> E.min_elt s
- | CoFinite _ -> raise exn
-
- let positive t = match t.node with
- | Finite x -> x
- | CoFinite _ -> E.empty
-
- let negative t = match t.node with
- | CoFinite x -> x
- | Finite _ -> E.empty
-
- let inj_positive t = finite t
- let inj_negative t = cofinite t
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 22:44:50 CET by Kim Nguyen>
-*)
-
-(** Implementation of hashconsed finite or cofinite sets.
-*)
-
-include module type of FiniteCofinite_sig
-
-(** Output signature of the {!FiniteCofinite.Make} and
- {!FiniteCofinite.Weak} functors.*)
-
-module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t
-(** Builds an implementation of hashconsed sets of hashconsed elements.
- See {!Hcons.Make}.
-*)
-
-module Weak (E : Ptset.S) : S with type elt = E.elt and type set = E.t
-(** Builds an implementation of hashconsed sets of hashconsed elements
- with weak internal storage. See {!Hcons.Weak}.
-*)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 22:44:15 CET by Kim Nguyen>
-*)
-
-exception InfiniteSet
-module type S =
-sig
- include Hcons.S
- include Common_sig.Set with type t := t
- type set
- val any : t
- val is_any : t -> bool
- val is_finite : t -> bool
- val kind : t -> [ `Finite | `Cofinite ]
- val complement : t -> t
- val kind_split : t list -> t * t
- val positive : t -> set
- val negative : t -> set
- val inj_positive : set -> t
- val inj_negative : set -> t
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
-*)
-
-include Hcons_sig
-
-module type TableBuilder =
- functor
- (H : Common_sig.HashedType) ->
- Common_sig.HashSet with type data = H.t
-
-module Builder (TB : TableBuilder) (H : Common_sig.HashedType) =
-struct
- type data = H.t
- type t = { id : Uid.t;
- hash : int;
- node : data }
- let uid_make = ref (Uid.make_maker())
- let node t = t.node
- let uid t = t.id
- let hash t = t.hash
- let equal t1 t2 = t1 == t2
- module HN =
- struct
- type _t = t
- type t = _t
- let hash = hash
- let equal x y = x == y || H.equal x.node y.node
- end
- module T = TB(HN)
-
- let pool = T.create 101
- let init () =
- T.clear pool;
- uid_make := Uid.make_maker ()
- let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
-
- let make x =
- let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
- try
- T.find pool cell
- with
- | Not_found ->
- let cell = { cell with id = !uid_make(); } in
- T.add pool cell;
- cell
-end
-
-module Make = Builder (Misc.HashSet)
-module Weak = Builder (Weak.Make)
-
-module PosInt =
-struct
- type data = int
- type t = int
- let make v =
- if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
- else v
-
- let node v = v
-
- let hash v = v
-
- let uid v = Uid.of_int v
- let dummy _ = ~-1
- let equal x y = x == y
-
- let init () = ()
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 23:05:14 CET by Kim Nguyen>
-*)
-
-(** Implementation of generic hashconsing. *)
-
-include module type of Hcons_sig
-
-(** Output signature of the functor {!Hcons.Make} *)
-
-module Make (H : Common_sig.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
- implementation of {!Common_sig.HashedType}. Hashconsed values are
- persistent: the are kept in memory even if no external reference
- remain. Calling [init()] explicitely will reclaim the space.
-*)
-
-module Weak (H : Common_sig.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
- implementation of {!Common_sig.HashedType}. Hashconsed values have a
- weak semantics: they may be reclaimed as soon as no external
- reference to them exists. The space may still be reclaimed
- explicitely by calling [init].
-*)
-
-module PosInt : Abstract with type data = int and type t = int
-(** Compact implementation of hashconsed positive integer that
- avoids boxing. [PosInt.make v] raises [Invalid_argument] if
- [ v < 0 ]
-*)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 22:36:31 CET by Kim Nguyen>
-*)
-
- (** Abstract signature of a module implementing an hashconsed datatype *)
-module type Abstract =
-sig
-
- (** The type of the data to be hash-consed *)
- type data
-
- (** The type of hashconsed data *)
- type t
-
- (** [make v] internalizes the value [v], making it an hashconsed
- value.
- *)
- val make : data -> t
-
- (** [node h] extract the original data from its hashconsed value
- *)
- val node : t -> data
-
- (** [hash h] returns a hash of [h], such that for every [h1] and
- [h2], [equal h1 h2] implies [hash h1 = hash h2].
- *)
- val hash : t -> int
-
- (** [uid h] returns a unique identifier *)
- val uid : t -> Uid.t
-
- (** Equality between hashconsed values. Equivalent to [==] *)
- val equal : t -> t -> bool
-
- (** Initializes the internal storage. Any previously hashconsed
- element is discarded. *)
- val init : unit -> unit
-
- (** Create a dummy (non-hashconsed) node with a boggus identifer
- and hash *)
- val dummy : data -> t
-end
-
-
- (** Concrete signature of a module implementing an hashconsed datatype *)
-module type S =
-sig
- type data
- type t = private { id : Uid.t;
- hash : int;
- node : data }
- include Abstract with type data := data and type t := t
-end
+++ /dev/null
-INCLUDE "utils.ml"
-
-include Hlist_sig
-
-module type HConsBuilder =
- functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
- S with type elt = H.t =
-struct
- type elt = H.t
-
- module rec Node : Hcons.S with type data = Data.t = HCB(Data)
- and Data : Common_sig.HashedType with type t = (elt, Node.t) node =
- struct
- type t = (elt, Node.t) node
- let equal x y =
- match x,y with
- | Nil, Nil -> true
- | Cons(e1, l1), Cons(e2, l2) -> e1 == e2 && l1 == l2
- | _ -> false
-
- let hash = function
- | Nil -> 0
- | Cons(e, l) -> HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))
- end
-
- include Node
-
- let nil = make Nil
-
- let rec sorted_cons e l =
- match l.Node.node with
- | Nil -> Node.make (Cons(e, l))
- | Cons (x, ll) ->
- if H.uid e < H.uid x
- then Node.make (Cons(e, l))
- else Node.make (Cons(x, sorted_cons e ll))
-
- let cons e l =
- Node.make(Cons(e, l))
-
- let cons ?(sorted=true) e l =
- if sorted then sorted_cons e l else cons e l
-
- let hd = function { Node.node = Cons(e, _); _ } -> e | _ -> failwith "hd"
- let tl = function { Node.node = Cons(_, l); _ } -> l | _ -> failwith "tl"
-
- let fold f l acc =
- let rec loop acc l = match l.Node.node with
- | Nil -> acc
- | Cons (a, aa) -> loop (f a acc) aa
- in
- loop acc l
-
- let map f l =
- let rec loop l = match l.Node.node with
- | Nil -> nil
- | Cons(a, aa) -> cons (f a) (loop aa)
- in
- loop l
-
- let iter f l =
- let rec loop l = match l.Node.node with
- | Nil -> ()
- | Cons(a,aa) -> (f a);(loop aa)
- in
- loop l
-
- let rev l = fold cons l nil
- let rev_map f l = fold (fun x acc -> cons (f x) acc) l nil
- let length l = fold (fun _ c -> c+1) l 0
- let rec mem e l =
- match l.Node.node with
- | Nil -> false
- | Cons (x, ll) -> x == e || mem e ll
-
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
-
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-13 18:30:59 CET by Kim Nguyen>
-*)
-
-include module type of Hlist_sig
-
-module Make (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed lists of hashconsed elements.
- See {!Hcons.Make}.
-*)
-
-module Weak (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed lists of hashconsed elements
- with weak internal storage. See {!Hcons.Weak}.
-*)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-13 18:21:28 CET by Kim Nguyen>
-*)
-type ('a,'b) node = Nil | Cons of ('a * 'b)
-
-module type S = sig
- type elt
- include Hcons.S
- val nil : t
- val cons : ?sorted:bool -> elt -> t -> t
- val hd : t -> elt
- val tl : t -> t
- val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
- val map : (elt -> elt) -> t -> t
- val iter : (elt -> 'a) -> t -> unit
- val rev : t -> t
- val rev_map : (elt -> elt) -> t -> t
- val length : t -> int
- val mem : elt -> t -> bool
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 23:00:19 CET by Kim Nguyen>
-*)
-
-(** Various generic signatures and generic module and functor definitions
-*)
-INCLUDE "utils.ml"
-
-module HashSet (H : Hashtbl.HashedType) :
- Common_sig.HashSet with type data = H.t =
-struct
- module T = Hashtbl.Make(H)
- type data = H.t
- type t = data T.t
- let create = T.create
- let add h v = T.add h v v
- let find = T.find
- let remove = T.remove
- let find_all = T.find_all
- let clear = T.clear
- let mem = T.mem
-end
-
-module Pair (X : Common_sig.Type) (Y : Common_sig.Type) :
- Common_sig.Type with type t = X.t * Y.t =
-struct
- type t = X.t * Y.t
- let hash (x, y) = HASHINT2(X.hash x, Y.hash y)
- let compare (x1, y1) (x2, y2) =
- let r = X.compare x1 x2 in
- if r != 0 then r else Y.compare y1 y2
- let equal p1 p2 =
- p1 == p2 ||
- let x1, y1 = p1
- and x2, y2 = p2 in X.equal x1 x2 && Y.equal y1 y2
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 10:41:21 CET by Kim Nguyen>
-*)
-
-open Format
-
-exception InvalidUtf8Codepoint of int
-
-let subscripts = "₀₁₂₃₄₅₆₇₈₉"
-let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
-
-let char_length c =
- let code = Char.code c in
- if code <= 0x7f then 1
- else if 0xc2 <= code && code <= 0xdf then 2
- else if 0xe0 <= code && code <= 0xef then 3
- else if 0xf0 <= code && code <= 0xf4 then 4
- else raise (InvalidUtf8Codepoint code)
-
-
-let next_char s i len =
- let n = i + char_length s.[i] in
- if n >= len then -1 else n
-
-let str_len s =
- let len = String.length s in
- let rec loop i acc =
- if i == -1 then acc
- else loop (next_char s i len) (acc+1)
- in
- loop 0 0
-
-let length = str_len
-
-let get_char s i =
- let len = String.length s in
- let rec loop j count =
- if count == i then String.sub s j (char_length s.[j])
- else loop (next_char s j len) (count+1)
- in
- loop 0 0
-
-
-let format_number digits i =
- let s = string_of_int i in
- let len = String.length s in
- let buf = Buffer.create (len*4) in
- for i = 0 to len - 1 do
- let d = Char.code s.[i] - Char.code '0' in
- Buffer.add_string buf (get_char digits d)
- done;
- Buffer.contents buf
-
-let rev_explode s =
- let len = str_len s in
- let rec loop i acc =
- if i >= len then acc
- else
- loop (i+1) ((get_char s i) :: acc)
- in
- loop 0 []
-
-
-let explode s = List.rev (rev_explode s)
-
-let combine_all comp s =
- let l = rev_explode s in
- String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
-
-
-let subscript = format_number subscripts
-let superscript = format_number superscripts
-let down_arrow = "↓"
-let up_arrow = "↑"
-let right_arrow = "→"
-let left_arrow = "←"
-let epsilon = "ϵ"
-let big_sigma = "∑"
-let cap = "∩"
-let cup = "∪"
-let lnot = "¬"
-let wedge = "∧"
-let vee = "∨"
-let top = "⊤"
-let bottom = "⊥"
-let dummy = "☠"
-let inverse = "⁻¹"
-let double_right_arrow = "⇒"
-let combining_overbar = "\204\133"
-let combining_underbar = "\204\178"
-let combining_stroke = "\204\182"
-let combining_vertical_line = "\226\131\146"
-
-
-let overline s = combine_all combining_overbar s
-let underline s = combine_all combining_underbar s
-let strike s = combine_all combining_stroke s
-
-let padding i = String.make i ' '
-let line i = String.make i '_'
-
-
-
-
-let ppf f fmt s =
- pp_print_string fmt (f s)
-
-let pp_overline = ppf overline
-let pp_underline = ppf underline
-let pp_strike = ppf strike
-let pp_subscript = ppf subscript
-let pp_superscript = ppf superscript
-let dummy_printer _ () = ()
-
-let pp_print_list ?(sep=dummy_printer) printer fmt l =
- match l with
- [] -> ()
- | [ e ] -> printer fmt e
- | e :: es -> printer fmt e; List.iter
- (fun x ->
- sep fmt ();
- fprintf fmt "%a" printer x) es
-
-let pp_print_array ?(sep=dummy_printer) printer fmt a =
- pp_print_list ~sep:sep printer fmt (Array.to_list a)
-
-let print_list ?(sep=" ") printer fmt l =
- let sep_printer fmt () =
- pp_print_string fmt sep
- in
- pp_print_list ~sep:sep_printer printer fmt l
-
-let print_array ?(sep=" ") printer fmt a =
- print_list ~sep:sep printer fmt (Array.to_list a)
-
-
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 10:41:32 CET by Kim Nguyen>
-*)
-
-exception InvalidUtf8Codepoint of int
-
-val subscript : int -> string
-val superscript : int -> string
-val down_arrow : string
-val up_arrow : string
-val right_arrow : string
-val left_arrow : string
-val epsilon : string
-val big_sigma : string
-val cap : string
-val cup : string
-val lnot : string
-val wedge : string
-val vee : string
-val top : string
-val bottom : string
-val dummy : string
-val inverse : string
-val double_right_arrow : string
-val overline : string -> string
-val underline : string -> string
-val strike : string -> string
-val padding : int -> string
-val line : int -> string
-val length : string -> int
-val pp_overline : Format.formatter -> string -> unit
-val pp_underline : Format.formatter -> string -> unit
-val pp_strike : Format.formatter -> string -> unit
-val pp_subscript : Format.formatter -> int -> unit
-val pp_superscript : Format.formatter -> int -> unit
-
-val pp_print_list :
- ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-val pp_print_array :
- ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
-val print_list : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-val print_array : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
+++ /dev/null
-(* Original file: *)
-(***********************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2.1, with the special exception on linking *)
-(* described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
-(* *)
-(* This software is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-10 18:18:54 CET by Kim Nguyen>
-*)
-
-(* Modified by Kim Nguyen *)
-(* The Patricia trees are themselves deeply hash-consed. The module
- provides a Make (and Weak) functor to build hash-consed patricia
- trees whose elements are Abstract hash-consed values.
-*)
-
-INCLUDE "utils.ml"
-
-include Ptset_sig
-
-module type HConsBuilder =
- functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
- S with type elt = H.t =
-struct
- type elt = H.t
-
- type 'a set =
- | Empty
- | Leaf of elt
- | Branch of int * int * 'a * 'a
-
- module rec Node : Hcons.S with type data = Data.t = HCB(Data)
- and Data : Common_sig.HashedType with type t = Node.t set =
- struct
- type t = Node.t set
- let equal x y =
- match x,y with
- | Empty,Empty -> true
- | Leaf k1, Leaf k2 -> k1 == k2
- | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
- b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
-
- | (Empty|Leaf _|Branch _), _ -> false
-
- let hash = function
- | Empty -> 0
- | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
- | Branch (b,i,l,r) ->
- HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
- end
-
- include Node
-
- let empty = Node.make Empty
-
- let is_empty s = (Node.node s) == Empty
-
- let branch p m l r = Node.make (Branch(p,m,l,r))
-
- let leaf k = Node.make (Leaf k)
-
- (* To enforce the invariant that a branch contains two non empty
- sub-trees *)
- let branch_ne p m t0 t1 =
- if (is_empty t0) then t1
- else if is_empty t1 then t0 else branch p m t0 t1
-
- (******** from here on, only use the smart constructors ************)
-
- let zero_bit k m = (k land m) == 0
-
- let singleton k = leaf k
-
- let is_singleton n =
- match Node.node n with
- | Leaf _ -> true
- | Branch _ | Empty -> false
-
- let mem (k:elt) n =
- let kid = Uid.to_int (H.uid k) in
- let rec loop n = match Node.node n with
- | Empty -> false
- | Leaf j -> k == j
- | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
- in loop n
-
- let rec min_elt n = match Node.node n with
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,s,_) -> min_elt s
-
- let rec max_elt n = match Node.node n with
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,_,t) -> max_elt t
-
- let elements s =
- let rec elements_aux acc n = match Node.node n with
- | Empty -> acc
- | Leaf k -> k :: acc
- | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
- in
- elements_aux [] s
-
- let mask k m = (k lor (m-1)) land (lnot m)
-
- let naive_highest_bit x =
- assert (x < 256);
- let rec loop i =
- if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
- in
- loop 7
-
- let hbit = Array.init 256 naive_highest_bit
- (*
- external clz : int -> int = "caml_clz" "noalloc"
- external leading_bit : int -> int = "caml_leading_bit" "noalloc"
- *)
- let highest_bit x =
- try
- let n = (x) lsr 24 in
- if n != 0 then hbit.(n) lsl 24
- else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
- else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
- else hbit.(x)
- with
- _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
-
- let highest_bit64 x =
- let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
- else highest_bit x
-
- let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
-
- let join p0 t0 p1 t1 =
- let m = branching_bit p0 p1 in
- let msk = mask p0 m in
- if zero_bit p0 m then
- branch_ne msk m t0 t1
- else
- branch_ne msk m t1 t0
-
- let match_prefix k p m = (mask k m) == p
-
- let add k t =
- let kid = Uid.to_int (H.uid k) in
- assert (kid >=0);
- let rec ins n = match Node.node n with
- | Empty -> leaf k
- | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
- | Branch (p,m,t0,t1) ->
- if match_prefix kid p m then
- if zero_bit kid m then
- branch_ne p m (ins t0) t1
- else
- branch_ne p m t0 (ins t1)
- else
- join kid (leaf k) p n
- in
- ins t
-
- let remove k t =
- let kid = Uid.to_int(H.uid k) in
- let rec rmv n = match Node.node n with
- | Empty -> empty
- | Leaf j -> if k == j then empty else n
- | Branch (p,m,t0,t1) ->
- if match_prefix kid p m then
- if zero_bit kid m then
- branch_ne p m (rmv t0) t1
- else
- branch_ne p m t0 (rmv t1)
- else
- n
- in
- rmv t
-
- (* should run in O(1) thanks to hash consing *)
-
- let equal a b = Node.equal a b
-
- let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
-
- let rec merge s t =
- if equal s t (* This is cheap thanks to hash-consing *)
- then s
- else
- match Node.node s, Node.node t with
- | Empty, _ -> t
- | _, Empty -> s
- | Leaf k, _ -> add k t
- | _, Leaf k -> add k s
- | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
- if m == n && match_prefix q p m then
- branch p m (merge s0 t0) (merge s1 t1)
- else if m > n && match_prefix q p m then
- if zero_bit q m then
- branch_ne p m (merge s0 t) s1
- else
- branch_ne p m s0 (merge s1 t)
- else if m < n && match_prefix p q n then
- if zero_bit p n then
- branch_ne q n (merge s t0) t1
- else
- branch_ne q n t0 (merge s t1)
- else
- (* The prefixes disagree. *)
- join p s q t
-
-
-
-
- let rec subset s1 s2 = (equal s1 s2) ||
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> true
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | Branch _, Leaf _ -> false
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- subset l1 l2 && subset r1 r2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then
- subset l1 l2 && subset r1 l2
- else
- subset l1 r2 && subset r1 r2
- else
- false
-
-
- let union s1 s2 = merge s1 s2
- (* Todo replace with e Memo Module *)
-
- let rec inter s1 s2 =
- if equal s1 s2
- then s1
- else
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> empty
- | _, Empty -> empty
- | Leaf k1, _ -> if mem k1 s2 then s1 else empty
- | _, Leaf k2 -> if mem k2 s1 then s2 else empty
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (inter l1 l2) (inter r1 r2)
- else if m1 > m2 && match_prefix p2 p1 m1 then
- inter (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- inter s1 (if zero_bit p1 m2 then l2 else r2)
- else
- empty
-
- let rec diff s1 s2 =
- if equal s1 s2
- then empty
- else
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> empty
- | _, Empty -> s1
- | Leaf k1, _ -> if mem k1 s2 then empty else s1
- | _, Leaf k2 -> remove k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (diff l1 l2) (diff r1 r2)
- else if m1 > m2 && match_prefix p2 p1 m1 then
- if zero_bit p2 m1 then
- merge (diff l1 s2) r1
- else
- merge l1 (diff r1 s2)
- else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
- else
- s1
-
-
- (*s All the following operations ([cardinal], [iter], [fold], [for_all],
- [exists], [filter], [partition], [choose], [elements]) are
- implemented as for any other kind of binary trees. *)
-
- let rec cardinal n = match Node.node n with
- | Empty -> 0
- | Leaf _ -> 1
- | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
-
- let rec iter f n = match Node.node n with
- | Empty -> ()
- | Leaf k -> f k
- | Branch (_,_,t0,t1) -> iter f t0; iter f t1
-
- let rec fold f s accu = match Node.node s with
- | Empty -> accu
- | Leaf k -> f k accu
- | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
-
-
- let rec for_all p n = match Node.node n with
- | Empty -> true
- | Leaf k -> p k
- | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
-
- let rec exists p n = match Node.node n with
- | Empty -> false
- | Leaf k -> p k
- | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
-
- let rec filter pr n = match Node.node n with
- | Empty -> empty
- | Leaf k -> if pr k then n else empty
- | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
-
- let partition p s =
- let rec part (t,f as acc) n = match Node.node n with
- | Empty -> acc
- | Leaf k -> if p k then (add k t, f) else (t, add k f)
- | Branch (_,_,t0,t1) -> part (part acc t0) t1
- in
- part (empty, empty) s
-
- let rec choose n = match Node.node n with
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
-
-
- let split x s =
- let coll k (l, b, r) =
- if k < x then add k l, b, r
- else if k > x then l, b, add k r
- else l, true, r
- in
- fold coll s (empty, false, empty)
-
- (*s Additional functions w.r.t to [Set.S]. *)
-
- let rec intersect s1 s2 = (equal s1 s2) ||
- match (Node.node s1,Node.node s2) with
- | Empty, _ -> false
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | _, Leaf k2 -> mem k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- intersect l1 l2 || intersect r1 r2
- else if m1 > m2 && match_prefix p2 p1 m1 then
- intersect (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- intersect s1 (if zero_bit p1 m2 then l2 else r2)
- else
- false
-
-
- let from_list l = List.fold_left (fun acc e -> add e acc) empty l
-
-
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
-
-module PosInt
- =
-struct
- include Make(Hcons.PosInt)
- let print ppf s =
- Format.pp_print_string ppf "{ ";
- iter (fun i -> Format.fprintf ppf "%i " i) s;
- Format.pp_print_string ppf "}";
- Format.pp_print_flush ppf ()
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 22:42:37 CET by Kim Nguyen>
-*)
-
-include module type of Ptset_sig
-
-module Make (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed sets of hashconsed elements.
- See {!Hcons.Make}.
-*)
-
-module Weak (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed sets of hashconsed elements
- with weak internal storage. See {!Hcons.Weak}.
-*)
-
-module PosInt : S with type elt = int
-(** Implementation of hashconsed sets of positive integers *)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-04 23:32:36 CET by Kim Nguyen>
-*)
-
-module type S =
-sig
- include Hcons.S
- include Common_sig.Set with type t := t
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-10 23:05:56 CET by Kim Nguyen>
-*)
-
-include Hcons.Make (struct
- include String
- let hash s = Hashtbl.hash s
- let equal s1 s2 = s1 = s2
-end)
-
-let print pp s = Format.fprintf pp "%s" s.node
-
-let of_string = make
-let to_string = node
-
-let document = of_string "#document"
-let text = of_string "#text"
-let comment = of_string "#comment"
-let nil = of_string "#"
-
-let attribute t = of_string ( "@" ^ (to_string t))
-let processing_instruction t = of_string ( "?" ^ (to_string t))
-
-let remove_prefix t =
- let s = to_string t in
- let lens = String.length s in
- if lens == 0 then t
- else
- if s.[0] == '@' || s.[0] == '?' then
- of_string (String.sub s 1 (lens-1))
- else
- t
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-10 23:02:12 CET by Kim Nguyen>
-*)
-
-(** Implementation of qualified names as hashconsed strings *)
-
-include Hcons.S with type data = string
-include Common_sig.Printable with type t := t
-
-
-val of_string : string -> t
-(** Utility function, equivalent to [make] *)
-
-val to_string : t -> string
-(** Utility function, equivalent to [node] *)
-
-
-(** Special constants, that denote the QName of nodes that are not
- elements (using the nodeValue property of DOM for such nodes.
-*)
-
-val document : t
-(** Represents the QName of a document node. Equivalent to
- [of_string "#document"]
-*)
-
-val text : t
-(** Represents the QName of a text node. Equivalent to
- [of_string "#text"]
-*)
-
-val comment : t
-(** Represents the QName of a comment node. Equivalent to
- [of_string "#comment"]
-*)
-
-val nil : t
-(** Represents the QName of a nil node. Equivalent to
- [of_string "#"]
-*)
-
-val attribute : t -> t
-(** Adds a prefix character (@) to distinguish the name
- from an element name
-*)
-
-val processing_instruction : t -> t
-(** Adds a prefix character (?) to distinguish the name
- from an element name
-*)
-
-val remove_prefix : t -> t
-(** Removes the prefix of the qname given as argument. Does not
- do anything if there is no prefix.
-*)
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 17:54:35 CET by Kim Nguyen>
-*)
-
-include FiniteCofinite.Make(Ptset.Make(QName))
-
-let print_finite fmt e conv =
- Format.fprintf fmt "{";
- Pretty.print_list ~sep:"," QName.print fmt (conv e);
- Format.fprintf fmt "}"
-
-let printer fmt e test conv inv is_any =
- if test e then print_finite fmt e conv
- else
- let () = Format.fprintf fmt "%s" Pretty.big_sigma in
- if not (is_any e) then begin Format.fprintf fmt "-";print_finite fmt (inv e) conv end
-
-let print fmt e = printer fmt e is_finite elements complement is_any
-
-let specials = [ QName.document; QName.text; QName.text ]
-let notstar = from_list specials
-let star = diff any notstar
-let node = any
-let text = singleton QName.text
-
-module Weak =
-struct
- include FiniteCofinite.Weak(Ptset.Weak(QName))
- let print fmt e = printer fmt e is_finite elements complement is_any
- let notstar = from_list specials
- let star = diff any notstar
- let node = any
- let text = singleton QName.text
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-03-09 17:53:53 CET by Kim Nguyen>
-*)
-
-(** Implementation of sets of Qualified Names that can be finite
- or cofinite *)
-
-include FiniteCofinite.S with type elt = QName.t
-include Common_sig.Printable with type t := t
-val star : t
-val text : t
-val node : t
-
-module Weak :
-sig
- include FiniteCofinite.S with type elt = QName.t
- include Common_sig.Printable with type t := t
- val star : t
- val text : t
- val node : t
-end
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-01-30 19:06:39 CET by Kim Nguyen>
-*)
-
-type t = int
-
-exception Overflow
-let make_maker () =
- let _id = ref ~-1 in
- fun () ->
- incr _id;
- let i = !_id in
- if i < 0 then raise Overflow else i
-
-let dummy = -1
-
-external to_int : t -> int = "%identity"
-external of_int : int -> t= "%identity"
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-01-30 19:06:33 CET by Kim Nguyen>
-*)
-
-(** This modules implements unique identifiers represented by integers *)
-
-type t = private int
-(** The type of unique identifiers. *)
-
-exception Overflow
-(** Raised when the internal counters for IDs overflows. *)
-
-val make_maker : unit -> (unit -> t)
-(** Returns an uid generator.
- [make_maker ()] returns a function that generates unique ids. Raises
- [Overflow] if the internal counter overflows.
-*)
-
-val dummy : t
-(** A dummy identifier, guaranteed to be distinct from any value
- returned by a generator.
-*)
-
-external to_int : t -> int = "%identity"
-(** Convert a unique id to an integer *)
-
-(**/**)
-
-external of_int : int -> t = "%identity"
-(** May break the invariant, use with caution *)
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 10:59:20 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:43:04 CEST by Kim Nguyen>
*)
-open Utils
type path = single_path list
and single_path = Absolute of step list | Relative of step list
| PrecedingSibling
| Preceding | Following
-and test = QNameSet.t * Tree.Common.NodeKind.t
+and test = QNameSet.t * Tree.NodeKind.t
and binop = Eq | Neq | Lt | Gt | Lte | Gte | Or | And | Add | Sub | Mult | Div | Mod
and unop = Neg
end
and print_test fmt (ts,kind) =
- let open Tree.Common.NodeKind in
+ let open Tree.NodeKind in
match kind with
Text -> pp fmt "%s" "text()"
| Element | Attribute ->
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 10:59:27 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:41:03 CEST by Kim Nguyen>
*)
type path = single_path list
| PrecedingSibling
| Preceding | Following
-and test = Utils.QNameSet.t * Tree.Common.NodeKind.t
+and test = QNameSet.t * Tree.NodeKind.t
and binop = Eq | Neq | Lt | Gt | Lte | Gte | Or | And | Add | Sub | Mult | Div | Mod
and unop = Neg
and expr =
| Number of [ `Int of int | `Float of float ]
| String of string
- | Fun_call of Utils.QName.t * expr list
+ | Fun_call of QName.t * expr list
| Path of path
| Binop of expr * binop * expr
| Unop of unop * expr
type t = path
-val text : Utils.QNameSet.t
-val node : Utils.QNameSet.t
-val star : Utils.QNameSet.t
+val text : QNameSet.t
+val node : QNameSet.t
+val star : QNameSet.t
val print_binop : Format.formatter -> binop -> unit
val print_unop : Format.formatter -> unop -> unit
val print_path : Format.formatter -> path -> unit
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-15 18:17:50 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:43:48 CEST by Kim Nguyen>
*)
open Ast
-open Auto
-open Utils
let ( => ) a b = (a, b)
let compile_axis_test axis (test,kind) phi trans states =
let q = State.make () in
let phi = match kind with
- Tree.Common.NodeKind.Node -> phi
+ Tree.NodeKind.Node -> phi
| _ -> phi %% F.mk_kind kind
in
let phi', trans', states' =
match p with
| Absolute steps ->
(Ancestor false, (QNameSet.singleton QName.document,
- Tree.Common.NodeKind.Node), [])
+ Tree.NodeKind.Node), [])
:: steps
| Relative steps -> steps
in
| (axis, (test,kind), elist) :: ll ->
let phi0, trans0, states0 =
compile_axis_test (invert_axis axis)
- (QNameSet.any, Tree.Common.NodeKind.Node)
+ (QNameSet.any, Tree.NodeKind.Node)
phi_above trans states
in
(* Only select attribute nodes if the previous axis
let phi0, trans0, states0 =
compile_axis_test
Self
- (QNameSet.singleton QName.document, Tree.Common.NodeKind.Node)
+ (QNameSet.singleton QName.document, Tree.NodeKind.Node)
Ata.SFormula.true_
trans
states
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-04 16:36:21 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:41:11 CEST by Kim Nguyen>
*)
-val path : Ast.path -> Auto.Ata.t
+val path : Ast.path -> Ata.t
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 14:21:53 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:44:13 CEST by Kim Nguyen>
*)
open Ast
- open Tree.Common
+ open Tree
%}
%token <string> TAG
axis_test:
AXIS COLONCOLON test { let a, (t,k) = $1, $3 in
match a with
- Attribute when Utils.QNameSet.is_finite t ->
- [ a, ((Utils.QNameSet.fold
+ Attribute when QNameSet.is_finite t ->
+ [ a, ((QNameSet.fold
(fun t a ->
- Utils.QNameSet.add
- (Utils.QName.attribute t) a)
- t Utils.QNameSet.empty), k) ]
+ QNameSet.add
+ (QName.attribute t) a)
+ t QNameSet.empty), k) ]
| Preceding|Following ->
[ (Descendant true, (t,k));
if a == Preceding then
let _ = Format.flush_str_formatter () in
let () = Format.fprintf Format.str_formatter "%a" Ast.print_axis $1 in
let a = Format.flush_str_formatter () in
- [Child, (Utils.QNameSet.singleton (Utils.QName.of_string a),NodeKind.Element)]
+ [Child, (QNameSet.singleton (QName.of_string a),NodeKind.Element)]
}
| ATTNAME { [(Attribute,
- (Utils.QNameSet.singleton (Utils.QName.of_string $1),
+ (QNameSet.singleton (QName.of_string $1),
NodeKind.Attribute))] }
;
NODE { node, NodeKind.Node }
| TEXT { text, NodeKind.Text }
| STAR { star, NodeKind.Element }
-| COMMENT { Utils.QNameSet.singleton(Utils.QName.comment),
+| COMMENT { QNameSet.singleton(QName.comment),
NodeKind.Comment
}
| PI { (if $1 = "" then star
- else Utils.QNameSet.singleton(
- Utils.QName.processing_instruction (
- Utils.QName.of_string $1)
+ else QNameSet.singleton(
+ QName.processing_instruction (
+ QName.of_string $1)
)), NodeKind.ProcessingInstruction
}
-| TAG { Utils.QNameSet.singleton(Utils.QName.of_string $1),
+| TAG { QNameSet.singleton(QName.of_string $1),
NodeKind.Element
}
;
| expr LTE expr { Binop($1, Lte, $3) }
| expr GT expr { Binop($1, Gt, $3) }
| expr GTE expr { Binop($1, Gte, $3) }
-| TAG LP arg_list RP { Fun_call(Utils.QName.of_string $1, $3) }
+| TAG LP arg_list RP { Fun_call(QName.of_string $1, $3) }
| LP expr RP { $2 }
| path { Path $1 }
;
projects / tatoo.git / commitdiff