-SOURCE_DIR=src,src/XPath
+SOURCE_DIR=src,src/xpath,src/utils,src/tree,src/auto
TARGET=main.otarget
-
all:
ocamlbuild -Is $(SOURCE_DIR) $(TARGET)
-
clean:
ocamlbuild -clean
-<src/XPath/*.cmx>: for-pack(XPath)
+<src/xpath/*.cmx>: for-pack(Xpath)
+<src/utils/*.cmx>: for-pack(Utils)
+<src/tree/*.cmx>: for-pack(Tree)
+<src/auto/*.cmx>: for-pack(Auto)
-(***********************************************************************)
-(* *)
-(* 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-01-30 19:09:57 CET by Kim Nguyen>
-*)
-
open Ocamlbuild_plugin
open Command
-open Myocamlbuild_config
-open Format
-
-let print_list l =
- eprintf "%![%s]%!\n" (String.concat ", " l)
-
-let _A x = A x
-let _S ?(extra=N) l = S (List.map (fun e -> (S [extra; _A e] )) l)
-;;
-let cxx_flags_for_ml = [ _S ~extra:(_A "-ccopt") cxx_flags ]
-let cxx_flags = ref [ _S cxx_flags ]
-let project_dirs = [ src_path; include_path ]
-let cxx_include_flags = _S cxx_includes
-let cxx_link_flags = ref [ _S cxx_lpaths; _S cxx_libs]
-let native_link_flags = ref (List.map (fun s -> s ^ ".cmxa") ocaml_link)
-let byte_link_flags = ref ("-custom" :: (List.map (fun s -> s ^ ".cma") ocaml_link))
-let link_flags = [ A"-linkpkg" ]
-let libs_files = List.map (fun s -> "file:" ^ s) cxx_libs_objects
-
-
-let native_compile_flags = ref [A"-fno-PIC"]
-let compile_flags = ref []
-
-let dwsize = sprintf "-DWORDSIZE%i" Sys.word_size
-
-(* Utils *)
-let ( @= ) r l = r := !r @ l
-let ( =:: ) r e = r := e :: !r
-
-(* Pre-processed files *)
-let pp_macro_options = ref
- [ A dwsize; A "-I"; P include_path ]
-
-let include_full_path = Pathname.pwd / include_path
-module Depends =
-struct
-open Scanf
-let scan_include ml =
- let ic = open_in ml and includes = ref [] in
- begin
- try
- while true do
- let s = input_line ic in
- if String.length s > 0 then
- try
- sscanf s " INCLUDE \"%s@\"" (fun s -> includes =:: include_path /s)
- with Scan_failure _ -> ()
- done
- with End_of_file -> close_in ic
- end;
- !includes
-
-let ocaml ml =
- let rec loop file =
- let includes = scan_include file in
- List.fold_left (fun a i -> (loop i) @ a) includes includes
- in
- let includes = loop ml in
- dep [ "file:" ^ ml ] includes
-let parse_depends depfile =
- let ichan = open_in depfile in
- let iscan = Scanning.from_channel ichan in
- let includes = ref [] in
- bscanf iscan " %_s@: %s " ignore;
- try
- while true do
- bscanf iscan " %s " (
- function "" -> raise End_of_file
- | "\\" -> ()
- | s -> includes =::s)
- done; []
- with
- _ -> close_in ichan;!includes
+let ocamlfind_packages = "unix,ulex,expat,camlp4,camlp4.lib,camlp4.macro"
-let cxx cpp =
- let depfile = !Options.build_dir /" __cxx_depends.tmp" in
- let cmd = Cmd (S[ A cxx_cmd ; S !cxx_flags; cxx_include_flags ; A"-MM";
- A "-MF"; P depfile; P cpp])
- in
- let () = Command.execute ~quiet:true ~pretend:false cmd in
- let includes = parse_depends depfile in
- let includes' = (List.filter (Pathname.is_relative) includes) in
- dep [ "compile"; "file:" ^ cpp ] includes'
-end
-
-let cxx_compile env _build =
- let cpp = env "%.cpp" and obj = env "%.o" in
- let tags = (tags_of_pathname cpp) ++ "compile" ++ "c++" in
- Cmd(S[T tags; A cxx_cmd; A "-o" ; P obj; A "-c"; S !cxx_flags; cxx_include_flags; P cpp])
-
-(* Native compile and link action *)
-
-let ocamlfind x = S[ T (Tags.singleton "ocamlfind"); A"ocamlfind"; x ; A "-package"; A ocamlfind_packages; A "-syntax"; A "camlp4o" ]
-
-let ppopt l = List.map (fun e -> S[ A"-ppopt"; e ]) l
+let ocamlfind x = S[ T (Tags.singleton "ocamlfind");
+ A "ocamlfind"; x ;
+ A "-package";
+ A ocamlfind_packages;
+ A "-syntax";
+ A "camlp4o";
+ A "-ppopt"; A "-I"; A"-ppopt"; A"include"
+ ]
let () = dispatch begin
function
| Before_rules ->
-
Options.ocamlc := ocamlfind (A"ocamlc");
Options.ocamlopt := ocamlfind (A"ocamlopt");
Options.ocamldep := ocamlfind (A"ocamldep");
Options.ocamldoc := ocamlfind (A"ocamldoc");
Options.ocamlmktop := ocamlfind (A"ocamlmktop");
-
- if not (List.mem "log" !Options.tags) then begin
- pp_macro_options @= [ A "-DNLOG" ];
- end;
- if (List.mem "profile" !Options.tags) then begin
- pp_macro_options @= [ A "-DPROFILE" ];
- native_compile_flags @= [A "-p" ];
- native_link_flags @= [ "-p" ];
- cxx_flags @= [ A "-pg" ];
- cxx_link_flags @= [ A "-pg" ];
- end;
-
- if (List.mem "debug" !Options.tags) then begin
- pp_macro_options @= [ A "-DDEBUG" ];
- cxx_flags @= [ A "-O0"; A "-g" ];
- cxx_link_flags @= [ A "-g" ];
- end
- else begin
- compile_flags @= [A "-noassert"];
- pp_macro_options @= [ A "-unsafe" ];
- native_compile_flags @= [ A "-inline"; A ocaml_inline ];
- cxx_flags @= [ A "-O3" ]
- end;
-
- let dir_path = Pathname.pwd / src_path in
- let dir = Pathname.readdir dir_path in
-
- Array.iter (fun entry ->
- if Pathname.check_extension entry "ml" then
- Depends.ocaml (src_path / entry)
- else if Pathname.check_extension entry "cpp" then
- Depends.cxx (src_path / entry)
- ) dir;
-
- | After_rules ->
- dep [ "link" ] cstub_lib;
- rule "c++: cpp & depends -> o" ~prod:"%.o" ~deps:[ "%.cpp" ] cxx_compile;
- let syntax_flags = S[ S (ppopt !pp_macro_options) ]
- in
- flag [ "ocaml"; "ocamldep"] syntax_flags;
- flag [ "ocaml"; "compile" ] (S[ A "-cc"; A cxx_cmd; S cxx_flags_for_ml ; syntax_flags; S !compile_flags ]);
- flag [ "ocaml"; "native"; "compile" ] (S !native_compile_flags);
- flag [ "ocaml"; "link" ]
- (S [ S link_flags ; A "-cc"; A cxx_cmd; S cxx_flags_for_ml; A "-cclib" ;
- Quote (S [ _S cstub_lib; S !cxx_link_flags]) ]);
- flag [ "ocaml"; "byte"; "link" ] (_S !byte_link_flags);
- flag [ "ocaml"; "native"; "link" ] (_S !native_link_flags);
- flag [ "c"; "ocamlmklib"] (A "-custom")
+ dep [ "extension:ml" ]
+ (List.map (fun s -> "include/" ^ s )
+ (Array.to_list (Pathname.readdir "include")));
+ flag [ "ocaml"; "link" ] (A"-linkpkg")
| _ -> ()
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-01-30 19:10:05 CET by Kim Nguyen>
-*)
-
-let ocaml_inline = "1000";;
-let include_path = "include";;
-let src_path = "src";;
-let ocaml_link = [ ];;
-let ocamlfind_packages = "unix,ulex,expat,camlp4,camlp4.lib,camlp4.macro";;
-let cxx_flags = [ "-fno-PIC"; "-std=c++0x"; "-O3" ];;
-let main_targets = [ "native","src/main.native";
- "byte", "src/main.byte" ];;
-let cstub_lib = [ ];;
-
-let cxx_cmd = "g++";;
-let cxx_includes = [ ]
-let cxx_lpaths = [ ]
-let cxx_libs = [ ];;
-let cxx_libs_objects = [];;
--- /dev/null
+#!/bin/sh
+
+cd src
+echo `pwd`
+for dir in *
+do
+ if [ -d "$dir" ]
+ then
+ echo "$dir"
+ rm -f "$dir".mlpack
+ cd "$dir"
+ for i in *.ml *.mly *.mll
+ do
+ if [ ! -f "$i" ]
+ then
+ continue
+ fi
+ echo "$i"
+ f=`echo "$i" | cut -b1`
+ l=`basename "$i" .mll`
+ l=`basename "$l" .mly`
+ l=`basename "$l" .ml | cut -b2-`
+ o=`echo "$f" | tr a-z A-Z`
+ echo "$dir"/"$o""$l" >> ../"$dir".mlpack
+ done
+ cd ..
+ fi
+done
+cd ..
\ No newline at end of file
+++ /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-05 14:34:06 CET by Kim Nguyen>
-*)
-
-
-type path = single_path list
-and single_path = Absolute of step list | Relative of step list
-and step = axis * test * expr list
-and axis = Self | Attribute | Child | Descendant | DescendantOrSelf | FollowingSibling
- | Parent | Ancestor | AncestorOrSelf | PrecedingSibling | Preceding | Following
-
-and test = QNameSet.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 QName.t * expr list
- | Path of path
- | Binop of expr * binop * expr
- | Unop of unop * expr
-
-
-type t = path
-
-
-let text = QNameSet.singleton QName.text
-let node = QNameSet.any
-let star =
- QNameSet.complement (
- QNameSet.from_list [ QName.text;
- QName.document;
- QName.cdata_section;
- QName.comment])
-
-
-
-let pp fmt e = Format.fprintf fmt e
-
-let prio e =
- match e with
- | Unop (Neg, _) -> 11
- | Path _ -> 10
- | Number _ | String _ | Fun_call _ -> 9
- | Binop (_,op,_) -> begin match op with
- | Lt | Lte | Gt | Gte -> 7
- | Neq | Eq -> 6
- | And -> 5
- | Or -> 4
- | Mult | Div | Mod -> 3
- | Add | Sub -> 2
- end
-
-let print_binop fmt o =
- pp fmt "%s" begin match o with
- | Eq -> "="
- | Neq -> "!="
- | Lt -> "<"
- | Gt -> ">"
- | Lte -> "<="
- | Gte -> ">="
- | Or -> "or"
- | And -> "and"
- | Add -> "+"
- | Sub -> "-"
- | Mult -> "*"
- | Div -> "div"
- | Mod -> "mod"
- end
-let print_unop fmt o =
- pp fmt "%s" begin match o with
- | Neg -> "-"
- end
-
-let rec print_path fmt p =
- Pretty.print_list ~sep:" | " print_single_path fmt p
-
-and print_single_path fmt p =
- let l = match p with
- | Absolute l -> pp fmt "/"; l
- | Relative l -> l
- in
- Pretty.print_list ~sep:"/" print_step fmt l
-
-and print_step fmt (axis, test, expr) =
- pp fmt "%a::%a" print_axis axis print_test test;
- match expr with
- [] -> ()
- | l -> pp fmt "[ ";
- Pretty.print_list ~sep:" ][ " print_expr fmt l;
- pp fmt " ]"
-
-and print_axis fmt a = pp fmt "%s" begin
- match a with
- Self -> "self"
- | Child -> "child"
- | Descendant -> "descendant"
- | DescendantOrSelf -> "descendant-or-self"
- | FollowingSibling -> "following-sibling"
- | Attribute -> "attribute"
- | Ancestor -> "ancestor"
- | AncestorOrSelf -> "ancestor-or-self"
- | PrecedingSibling -> "preceding-sibling"
- | Parent -> "parent"
- | Preceding -> "preceding"
- | Following -> "following"
-end
-
-and print_test fmt ts =
- try
- pp fmt "%s" (List.assoc ts
- [ text,"text()";
- node,"node()";
- star, "*" ] )
- with
- Not_found -> pp fmt "%s"
- (if QNameSet.is_finite ts
- then QName.to_string (QNameSet.choose ts)
- else "<INFINITE>"
- )
-
-and print_expr fmt = function
-| Number (`Int(i)) -> pp fmt "%i" i
-| Number (`Float(f)) -> pp fmt "%f" f
-| String s -> pp fmt "'%S'" s
-| Fun_call (n, args) ->
- pp fmt "%a(" QName.print n;
- Pretty.print_list ~sep:", " print_expr fmt args;
- pp fmt ")"
-| Path p -> print_path fmt p
-| Binop (e1, op, e2) as e ->
- let pe = prio e in
- let need_par1 = prio e1 < pe in
- if need_par1 then pp fmt "(";
- pp fmt "%a" print_expr e1;
- if need_par1 then pp fmt ")";
- pp fmt " %a " print_binop op;
- let need_par2 = prio e2 < pe in
- if need_par2 then pp fmt "(";
- pp fmt "%a" print_expr e2;
- if need_par2 then pp fmt ")"
-| Unop (op, e0) as e ->
- let need_par0 = prio e0 < prio e in
- print_unop fmt op;
- if need_par0 then pp fmt "(";
- print_expr fmt e0;
- if need_par0 then pp fmt ")"
-
+++ /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-02-05 14:34:37 CET by Kim Nguyen>
-*)
-
-type path = single_path list
-and single_path = Absolute of step list | Relative of step list
-and step = axis * test * expr list
-and axis = Self | Attribute | Child | Descendant | DescendantOrSelf | FollowingSibling
- | Parent | Ancestor | AncestorOrSelf | PrecedingSibling | Preceding | Following
-
-and test = QNameSet.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 QName.t * expr list
- | Path of path
- | Binop of expr * binop * expr
- | Unop of unop * expr
-type t = path
-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
-val print_single_path : Format.formatter -> single_path -> unit
-val print_step : Format.formatter -> step -> unit
-val print_axis : Format.formatter -> axis -> unit
-val print_test : Format.formatter -> test -> unit
-val print_expr : Format.formatter -> expr -> 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-02-05 14:40:30 CET by Kim Nguyen>
-*)
-
-include Xpath_internal_parser
-
-let parse (l : Ulexing.lexbuf) =
- xpath (fun _ -> Ulexer.token l) (Lexing.from_string "!!dummy!!")
-
+++ /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-02-05 14:53:12 CET by Kim Nguyen>
-*)
-
-open Xpath_internal_parser
-
-module L = Ulexing
-
-exception Error of int * int * string
-
-let error i j s = raise (Error (i,j,s))
-
-(***********************************************************)
-(* Buffer for string literals *)
-
-let string_buff = Buffer.create 1024
-
-let store_lexeme lexbuf =
- Buffer.add_string string_buff (Ulexing.utf8_lexeme lexbuf)
-let store_ascii = Buffer.add_char string_buff
-let store_code = Utf8.store string_buff
-let clear_buff () = Buffer.clear string_buff
-let get_stored_string () =
- let s = Buffer.contents string_buff in
- clear_buff ();
- Buffer.clear string_buff;
- s
-
-(***********************************************************)
-(* Lexer *)
-
-let illegal lexbuf =
- error
- (L.lexeme_start lexbuf)
- (L.lexeme_end lexbuf)
- "Illegal character"
-
-let return lexbuf tok = (tok, L.loc lexbuf)
-let return_loc i j tok = (tok, (i,j))
-
-let regexp ncname_char =
- xml_letter | xml_digit | [ '-' '_' ] | xml_combining_char | xml_extender | "\\."
-
-let hexa_digit = function
- | '0'..'9' as c -> (Char.code c) - (Char.code '0')
- | 'a'..'f' as c -> (Char.code c) - (Char.code 'a') + 10
- | 'A'..'F' as c -> (Char.code c) - (Char.code 'A') + 10
- | _ -> -1
-
-let regexp ncname = ( xml_letter ncname_char* ) | ('_' ncname_char+)
-let regexp digit = ['0'-'9']
-let regexp float = '-'? digit+ ('.' digit+ (['e''E'] digit+)?)?
-
-let parse_char lexbuf base i =
- let s = L.latin1_sub_lexeme lexbuf i (L.lexeme_length lexbuf - i - 1) in
- let r = ref 0 in
- for i = 0 to String.length s - 1 do
- let c = hexa_digit s.[i] in
- if (c >= base) || (c < 0) then
- error (L.lexeme_start lexbuf) (L.lexeme_end lexbuf) "invalid digit";
- r := !r * base + c;
- done;
- !r
-
-let keyword_or_tag s =
- try
- List.assoc s [
- "self", AXIS Ast.Self;
- "descendant", AXIS Ast.Descendant;
- "child", AXIS Ast.Child;
- "descendant-or-self", AXIS Ast.DescendantOrSelf;
- "attribute", AXIS Ast.Attribute;
- "following-sibling", AXIS Ast.FollowingSibling;
- "preceding-sibling", AXIS Ast.PrecedingSibling;
- "parent", AXIS Ast.Parent;
- "ancestor", AXIS Ast.Ancestor;
- "ancestor-or-self", AXIS Ast.AncestorOrSelf;
- "preceding", AXIS Ast.Preceding;
- "following", AXIS Ast.Following;
- "and", AND;
- "or" , OR;
- "div", DIV;
- "mod", MOD;
- ]
- with
- _ -> TAG s
-
-
-let rec token = lexer
- | [' ' '\t' '\n'] -> token lexbuf
- | "*" -> STAR
- | "/" -> SLASH
- | "//" -> SLASHSLASH
- | "::" -> COLONCOLON
- | "(" -> LP
- | ")" -> RP
- | "[" -> LB
- | "]" -> RB
- | "," -> COMMA
- | "|" -> PIPE
- | "+" -> ADD
- | "-" -> SUB
- | "<" -> LT
- | "<=" -> LTE
- | ">" -> GT
- | ">=" -> GTE
- | "=" -> EQ
- | "!=" -> NEQ
- | "node()" -> NODE
- | "text()" -> TEXT
- | ncname -> keyword_or_tag (L.utf8_lexeme lexbuf)
- | float ->
- let s = L.utf8_lexeme lexbuf in
- (try
- INT (int_of_string s)
- with
- _ -> FLOAT (float_of_string s))
- | '"' | "'" ->
- let double_quote = L.latin1_lexeme_char lexbuf 0 = '"' in
- string (L.lexeme_start lexbuf) double_quote lexbuf;
- let s = get_stored_string () in
- STRING s
-
- | eof -> EOF
- | _ -> illegal lexbuf
-
-and string start double = lexer
- | '"' | "'" ->
- let d = L.latin1_lexeme_char lexbuf 0 = '"' in
- if d != double then (store_lexeme lexbuf; string start double lexbuf)
- | '\\' ['\\' '"' '\''] ->
- store_ascii (L.latin1_lexeme_char lexbuf 1);
- string start double lexbuf
- | "\\n" ->
- store_ascii '\n'; string start double lexbuf
- | "\\t" ->
- store_ascii '\t'; string start double lexbuf
- | "\\r" ->
- store_ascii '\r'; string start double lexbuf
- | '\\' ['0'-'9']+ ';' ->
- store_code (parse_char lexbuf 10 1);
- string start double lexbuf
- | '\\' 'x' ['0'-'9' 'a'-'f' 'A'-'F']+ ';' ->
- store_code (parse_char lexbuf 16 2);
- string start double lexbuf
- | '\\' ->
- illegal lexbuf;
- | eof ->
- error start (start+1) "Unterminated string"
- | _ ->
- store_lexeme lexbuf;
- string start double lexbuf
-
-
+++ /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-05 14:54:19 CET by Kim Nguyen>
-*)
-
- open Ast
- let f () = ()
-%}
-
-%token <string> TAG
-%token <string> STRING
-%token <int> INT
-%token <float> FLOAT
-%token <Ast.axis> AXIS
-%token RB LB LP RP
-%token SLASH SLASHSLASH COLONCOLON STAR PIPE
-%token EQ NEQ LT GT LTE GTE OR AND ADD SUB DIV MOD
-%token NODE TEXT
-%token COMMA
-%token EOF
-
-%left OR
-%left AND
-%left EQ NEQ
-%left LT GT LTE GTE
-%left ADD SUB
-%left MOD DIV STAR
-%nonassoc uminus
-
-%start xpath
-%type <Ast.path> xpath
-
-
-%%
-xpath:
-path EOF { $1 }
-;
-
-path:
- path_rev { List.rev $1 }
-;
-
-path_rev:
- simple_path { [ $1 ] }
-| path_rev PIPE simple_path { $3 :: $1 }
-;
-
-
-simple_path:
- absolute_path { Absolute (List.rev $1) }
-| relative_path { Relative (List.rev $1) }
-;
-
-absolute_path:
- SLASH relative_path { $2 }
-| SLASHSLASH relative_path { (DescendantOrSelf, node, []) :: $2 }
-;
-
-relative_path:
- step { [ $1 ] }
-| relative_path SLASH step { $3 :: $1 }
-| relative_path SLASHSLASH step { $3
- :: (DescendantOrSelf, node, [])
- :: $1 }
-;
-
-step:
- axis_test pred_list { let a, b = $1 in a, b, $2 }
-;
-
-axis_test:
- AXIS COLONCOLON test { $1, $3 }
-| test { Child, $1 }
-| AXIS {
- 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, QNameSet.singleton (QName.of_string a)
-}
-;
-
-test:
- NODE { node }
-| TEXT { text }
-| STAR { star }
-| TAG { QNameSet.singleton(QName.of_string $1) }
-;
-
-pred_list:
- pred_list_rev { List.rev $1 }
-;
-
-pred_list_rev:
- { [] }
-| pred_list LB expr RB { $3 :: $1 }
-;
-
-expr:
- INT { Number(`Int($1)) }
-| FLOAT { Number(`Float($1)) }
-| STRING { String $1 }
-| SUB expr %prec uminus { Unop(Neg, $2) }
-| expr AND expr { Binop($1, And, $3) }
-| expr OR expr { Binop($1, Or, $3) }
-| expr ADD expr { Binop($1, Add, $3) }
-| expr SUB expr { Binop($1, Sub, $3) }
-| expr STAR expr { Binop($1, Mult, $3) }
-| expr DIV expr { Binop($1, Div, $3) }
-| expr MOD expr { Binop($1, Mod, $3) }
-| expr EQ expr { Binop($1, Eq, $3) }
-| expr NEQ expr { Binop($1, Neq, $3) }
-| expr LT expr { Binop($1, Lt, $3) }
-| 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(QName.of_string $1, $3) }
-| LP expr RP { $2 }
-| path { Path $1 }
-;
-
-arg_list:
- { [] }
-| arg_list1 { List.rev $1 }
-;
-
-arg_list1:
- expr { [ $1 ] }
-| arg_list1 COMMA expr { $3 :: $1 }
-;
-
+++ /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-02-06 14:24:24 CET by Kim Nguyen>
-*)
-
-open Format
-type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
-type state_ctx = { left : StateSet.t;
- right : StateSet.t;
- up1 : StateSet.t;
- up2 : StateSet.t;
- epsilon : StateSet.t}
-type ctx_ = { mutable positive : state_ctx;
- mutable negative : state_ctx }
-type pred_ = move * bool * State.t
-
-module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
-struct
-
- module Node =
- struct
- type t = move * bool * State.t
- let equal n1 n2 = n1 = n2
- let hash n = Hashtbl.hash n
- end
-
- type ctx = ctx_
- let make_ctx a b c d e =
- { left = a; right = b; up1 = c; up2 = d; epsilon = e }
-
- include Hcons.Make(Node)
-
- let print ppf a =
- let _ = flush_str_formatter() in
- let fmt = str_formatter in
-
- let m, b, s = a.node in
- let dir,num =
- match m 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" dir num;
- State.print fmt s;
- let str = flush_str_formatter() in
- if b then fprintf ppf "%s" str
- else Pretty.pp_overline ppf str
-
- let neg p =
- let l, b, s = p.node in
- make (l, not b, s)
-
- let eval ctx p =
- let l, b, s = p.node in
- let nctx = if b then ctx.positive else ctx.negative in
- StateSet.mem s begin
- match l with
- `Left -> nctx.left
- | `Right -> nctx.right
- | `Up1 -> nctx.up1
- | `Up2 -> nctx.up2
- | `Epsilon -> nctx.epsilon
- end
-end
-
-module SFormula = Formula.Make(Move)
-type t = {
- id : Uid.t;
- mutable states : StateSet.t;
- mutable top_states : StateSet.t;
- mutable bottom_states: StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
-}
-
-
-
-let next = Uid.make_maker ()
-
-let create () = { id = next ();
- states = StateSet.empty;
- top_states = StateSet.empty;
- bottom_states = StateSet.empty;
- selection_states = StateSet.empty;
- transitions = Hashtbl.create 17;
- }
-
-let add_trans a q s f =
- let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
- let rem, ntrs =
- List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
- let nlabs = QNameSet.inter labs rem in
- if QNameSet.is_empty nlabs then
- (rem, tr :: atrs)
- else
- let nrem = QNameSet.diff rem labs in
- nrem, (nlabs, SFormula.or_ phi f)::atrs
- ) (s, []) trs
- in
- let ntrs = if QNameSet.is_empty rem then ntrs
- else (rem, f) :: ntrs
- in
- Hashtbl.replace a.transitions q ntrs
-
-
-let print fmt a =
- fprintf fmt
- "Unique ID: %i@\n\
- States %a@\n\
- Top states: %a@\n\
- Bottom states: %a@\n\
- Selection states: %a@\n\
- Alternating transitions:@\n"
- (a.id :> int)
- StateSet.print a.states
- StateSet.print a.top_states
- StateSet.print a.bottom_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, phi1) (q2, s2, phi2) ->
- let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
- trs
- in
- let sfmt = str_formatter in
- let _ = flush_str_formatter () in
- let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
- let s1 = State.print sfmt q; flush_str_formatter () in
- let s2 = QNameSet.print sfmt s; flush_str_formatter () in
- let s3 = SFormula.print sfmt f; flush_str_formatter () in
- ( (s1, s2, s3) :: accl,
- max
- accm (2 + String.length s1 + String.length s2))
- ) ([], 0) sorted_trs
- in
- List.iter (fun (s1, s2, s3) ->
- fprintf fmt "%s, %s" s1 s2;
- fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
- fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings
--- /dev/null
+auto/Ata
+auto/Formula
+auto/State
+auto/StateSet
--- /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-02-07 10:02:38 CET by Kim Nguyen>
+*)
+
+open Format
+open Utils
+
+type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
+type state_ctx = { left : StateSet.t;
+ right : StateSet.t;
+ up1 : StateSet.t;
+ up2 : StateSet.t;
+ epsilon : StateSet.t}
+type ctx_ = { mutable positive : state_ctx;
+ mutable negative : state_ctx }
+type pred_ = move * bool * State.t
+
+module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
+struct
+
+ module Node =
+ struct
+ type t = move * bool * State.t
+ let equal n1 n2 = n1 = n2
+ let hash n = Hashtbl.hash n
+ end
+
+ type ctx = ctx_
+ let make_ctx a b c d e =
+ { left = a; right = b; up1 = c; up2 = d; epsilon = e }
+
+ include Hcons.Make(Node)
+
+ let print ppf a =
+ let _ = flush_str_formatter() in
+ let fmt = str_formatter in
+
+ let m, b, s = a.node in
+ let dir,num =
+ match m 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" dir num;
+ State.print fmt s;
+ let str = flush_str_formatter() in
+ if b then fprintf ppf "%s" str
+ else Pretty.pp_overline ppf str
+
+ let neg p =
+ let l, b, s = p.node in
+ make (l, not b, s)
+
+ let eval ctx p =
+ let l, b, s = p.node in
+ let nctx = if b then ctx.positive else ctx.negative in
+ StateSet.mem s begin
+ match l with
+ `Left -> nctx.left
+ | `Right -> nctx.right
+ | `Up1 -> nctx.up1
+ | `Up2 -> nctx.up2
+ | `Epsilon -> nctx.epsilon
+ end
+end
+
+module SFormula = Formula.Make(Move)
+type t = {
+ id : Uid.t;
+ mutable states : StateSet.t;
+ mutable top_states : StateSet.t;
+ mutable bottom_states: StateSet.t;
+ mutable selection_states: StateSet.t;
+ transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+}
+
+
+
+let next = Uid.make_maker ()
+
+let create () = { id = next ();
+ states = StateSet.empty;
+ top_states = StateSet.empty;
+ bottom_states = StateSet.empty;
+ selection_states = StateSet.empty;
+ transitions = Hashtbl.create 17;
+ }
+
+let add_trans a q s f =
+ let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+ let rem, ntrs =
+ List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
+ let nlabs = QNameSet.inter labs rem in
+ if QNameSet.is_empty nlabs then
+ (rem, tr :: atrs)
+ else
+ let nrem = QNameSet.diff rem labs in
+ nrem, (nlabs, SFormula.or_ phi f)::atrs
+ ) (s, []) trs
+ in
+ let ntrs = if QNameSet.is_empty rem then ntrs
+ else (rem, f) :: ntrs
+ in
+ Hashtbl.replace a.transitions q ntrs
+
+
+let print fmt a =
+ fprintf fmt
+ "Unique ID: %i@\n\
+ States %a@\n\
+ Top states: %a@\n\
+ Bottom states: %a@\n\
+ Selection states: %a@\n\
+ Alternating transitions:@\n"
+ (a.id :> int)
+ StateSet.print a.states
+ StateSet.print a.top_states
+ StateSet.print a.bottom_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, phi1) (q2, s2, phi2) ->
+ let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+ trs
+ in
+ let sfmt = str_formatter in
+ let _ = flush_str_formatter () in
+ let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
+ let s1 = State.print sfmt q; flush_str_formatter () in
+ let s2 = QNameSet.print sfmt s; flush_str_formatter () in
+ let s3 = SFormula.print sfmt f; flush_str_formatter () in
+ ( (s1, s2, s3) :: accl,
+ max
+ accm (2 + String.length s1 + String.length s2))
+ ) ([], 0) sorted_trs
+ in
+ List.iter (fun (s1, s2, s3) ->
+ fprintf fmt "%s, %s" s1 s2;
+ fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
+ fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings
--- /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-02-07 10:00:33 CET by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+open Format
+open Utils
+
+(*
+
+(** Implementation of hashconsed Boolean formulae *)
+
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+
+(** Direction for automata predicates *)
+*)
+module type PREDICATE =
+sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Sigs.AUX.Printable with type t := t
+end
+
+type ('formula,'pred) expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Atom of 'pred
+
+module Make (P: PREDICATE) =
+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 : Hashtbl.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 rec eval ctx f =
+ match f.Node.node.pos with
+ True -> true
+ | False -> false
+ | Atom p -> P.eval ctx p
+ | And(f1, f2) -> eval ctx f1 && eval ctx f2
+ | Or(f1, f2) -> eval ctx f1 || eval ctx f2
+
+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-02-07 10:03:26 CET by Kim Nguyen>
+*)
+
+module type PREDICATE =
+sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include Utils.Hcons.Abstract with type t := t
+ include Utils.Sigs.AUX.Printable with type t := t
+end
+
+type ('formula,'pred) expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Atom of 'pred
+
+(** View of the internal representation of a formula,
+ used for pattern matching *)
+
+module Make(P : PREDICATE) :
+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
+ (** Equality over 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 eval : P.ctx -> t -> bool
+ (** Evaluate a formula given a context for atomic predicates *)
+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-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-01-30 19:07:11 CET by Kim Nguyen>
+*)
+
+(** Implementation of states *)
+
+include Sigs.AUX.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-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:09:01 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-include Sigs.FINITECOFINITE
-
-module type HConsBuilder =
- functor (H : Sigs.AUX.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
- | _ -> 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 = function
- | { node = Finite s } when E.is_empty s -> true
- | _ -> false
-
- let is_any = function
- | { node = CoFinite s } when E.is_empty s -> true
- | _ -> false
-
- let is_finite t = match t.node with
- | Finite _ -> true | _ -> false
-
- let kind t = match t.node with
- | Finite _ -> `Finite
- | _ -> `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 = Sigs.FINITECOFINITE.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
- | _ -> raise exn
-
- let is_singleton t = match t.node with
- | Finite s -> E.is_singleton s
- | _ -> 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 s, CoFinite t -> 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
-
- | _ -> raise exn
-
- let min_elt s = match s.node with
- | Finite s -> E.min_elt s
- | _ -> raise exn
-
- let max_elt s = match s.node with
- | Finite s -> E.min_elt s
- | _ -> raise exn
-
- let positive t =
- match t.node with
- | Finite x -> x
- | _ -> E.empty
-
- let negative t =
- match t.node with
- | CoFinite x -> x
- | _ -> 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-01-30 19:08:57 CET by Kim Nguyen>
-*)
-
-(** Implementation of hashconsed finite or cofinite sets.
-*)
-
-include module type of Sigs.FINITECOFINITE
-
-(** 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-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-02-06 14:30:27 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-open Format
-
-
-(*
-
-(** Implementation of hashconsed Boolean formulae *)
-
-type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-
-(** Direction for automata predicates *)
-*)
-module type PREDICATE =
-sig
- type t
- type ctx
- val eval : ctx -> t -> bool
- val neg : t -> t
- include Hcons.Abstract with type t := t
- include Sigs.AUX.Printable with type t := t
-end
-
-type ('formula,'pred) expr =
- | False
- | True
- | Or of 'formula * 'formula
- | And of 'formula * 'formula
- | Atom of 'pred
-
-module Make (P: PREDICATE) =
-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 : Hashtbl.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 rec eval ctx f =
- match f.Node.node.pos with
- True -> true
- | False -> false
- | Atom p -> P.eval ctx p
- | And(f1, f2) -> eval ctx f1 && eval ctx f2
- | Or(f1, f2) -> eval ctx f1 || eval ctx f2
-
-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-02-05 16:11:43 CET by Kim Nguyen>
-*)
-
-module type PREDICATE =
-sig
- type t
- type ctx
- val eval : ctx -> t -> bool
- val neg : t -> t
- include Hcons.Abstract with type t := t
- include Sigs.AUX.Printable with type t := t
-end
-
-type ('formula,'pred) expr =
- | False
- | True
- | Or of 'formula * 'formula
- | And of 'formula * 'formula
- | Atom of 'pred
-
-(** View of the internal representation of a formula,
- used for pattern matching *)
-
-module Make(P : PREDICATE) :
-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
- (** Equality over 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 eval : P.ctx -> t -> bool
- (** Evaluate a formula given a context for atomic predicates *)
-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-02-06 14:26:22 CET by Kim Nguyen>
-*)
-
-include Sigs.HCONS
-
-module type TableBuilder =
- functor
- (H : Sigs.AUX.HashedType) ->
- Sigs.AUX.HashSet with type data = H.t
-
-module Builder (TB : TableBuilder) (H : Sigs.AUX.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 (Utils.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-01-30 19:08:42 CET by Kim Nguyen>
-*)
-
-(** Implementation of generic hashconsing. *)
-
-include module type of Sigs.HCONS
-
-(** Output signature of the functor {!Hcons.Make} *)
-
-module Make (H : Sigs.AUX.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
- implementation of {!Sigs.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 : Sigs.AUX.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
- implementation of {!Sigs.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-01-30 19:08:11 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 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 mk_repeater c =
- let mk_str i = String.make i c in
- let _table = Array.init 16 mk_str in
- fun i -> try
- if i < 16 then _table.(i) else mk_str i
- with e -> print_int i; print_newline(); raise e
-let padding = mk_repeater ' '
-let line = mk_repeater '_'
-
-
-
-
-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 fmt () = ()
-
-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-01-30 19:08:06 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 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-01-30 19:07:53 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 Sigs.PTSET
-
-module type HConsBuilder =
- functor (H : Sigs.AUX.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 : Sigs.AUX.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)
-
- | _ -> 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
- | _ -> 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-01-30 19:07:42 CET by Kim Nguyen>
-*)
-
-include module type of Sigs.PTSET
-
-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-01-30 19:07:38 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 cdata_section = of_string "#cdata-section"
-let comment = of_string "#comment"
-let document_fragment = of_string "#document-fragment"
-let attribute_map = of_string "#attribute-map"
-let nil = of_string "#"
+++ /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:07:34 CET by Kim Nguyen>
-*)
-
-(** Implementation of qualified names as hashconsed strings *)
-
-include Sigs.HCONS.S with type data = string
-include Sigs.AUX.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 cdata_section : t
-(** Represents the QName of a document node. Equivalent to
- [of_string "#cdata-section"]
-*)
-
-val comment : t
-(** Represents the QName of a comment node. Equivalent to
- [of_string "#cdata-section"]
-*)
-
-val document_fragment : t
-(** Represents the QName of a document fragment. Equivalent to
- [of_string "#document-fragment"]
-*)
-
-val attribute_map : t
-(** Represents the QName of a dummy document node holding the
- attributes of the current element. Equivalent to
- [of_string "#attribute-map"]
-*)
-
-val nil : t
-(** Represents the QName of a nil node. Equivalent to
- [of_string "#"]
-*)
+++ /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:07:29 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 =
- if test e then print_finite fmt e conv
- else begin
- Format.fprintf fmt "%s \\ " Pretty.big_sigma;
- print_finite fmt (inv e) conv
- end
-
-let print fmt e = printer fmt e is_finite elements complement
-
-module Weak =
-struct
- include FiniteCofinite.Weak(Ptset.Weak(QName))
- let print fmt e = printer fmt e is_finite elements complement
-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:07:23 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 Sigs.AUX.Printable with type t := t
-
-module Weak :
- sig
- include FiniteCofinite.S with type elt = QName.t
- include Sigs.AUX.Printable 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-02-05 15:58:13 CET by Kim Nguyen>
-*)
-
-(** This module contains all the signatures of the project, to avoid
- code duplication. Each toplevel module (HCONS, PTSET, ...)
- corresponds to an existing module in the project. The AUX modules
- regroups common auxiliary signatures.
-*)
-
-
-(** The [AUX] module regroups the definitions of common interfaces *)
-module AUX =
-struct
-
- (** 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
-
- (** Type equiped with a pretty-printer *)
- module type Printable =
- sig
- type t
- val print : Format.formatter -> t -> unit
- end
-
- (** Type with both total ordering and hashing functions.
- All modules of that type must enforce than:
- [equal a b] if and only if [compare a b = 0]
- *)
- module type Type =
- sig
- type t
- include HashedType with type t := t
- include OrderedType with type t := t
- 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
-end
-
-module HCONS =
-struct
- (** 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
-
-end
-
-
-module PTSET =
-struct
- module type S =
- sig
- include HCONS.S
- include AUX.Set with type t := t
- end
-end
-
-module FINITECOFINITE =
-struct
- exception InfiniteSet
- module type S =
- sig
- include HCONS.S
- include AUX.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
-end
-
-module FORMULA =
-struct
- module type ATOM =
- sig
- type t
- type ctx
- val eval : ctx -> t -> bool
- val neg : t -> t
- include HCONS.S with type t := t
- include AUX.Printable with type t := t
- end
- module type S =
- sig
- module Atom : ATOM
- include HCONS.S
- include AUX.Printable with type t := t
- val of_bool : bool -> t
- val true_ : t
- val false_ : t
- val or_ : t -> t -> t
- val and_ : t -> t -> t
- val not_ : t -> t
- val diff_ : t -> t -> t
- val eval : Atom.ctx -> t -> bool
- end
-
-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:07:15 CET 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-01-30 19:07:11 CET by Kim Nguyen>
-*)
-
-(** Implementation of states *)
-
-include Sigs.AUX.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-01-30 19:07:06 CET 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-01-30 19:07:02 CET 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-02-05 14:39:43 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-02-07 10:25:30 CET by Kim Nguyen>
*)
(** use: xml_file "XPath querie"
only the first line of XPath_querie_file is read
*)
-module F = Formula
-module A = Ata
+module F = Auto.Formula
+module A = Auto.Ata
(* to force ocaml build to add Formula to the dependency chain even if
we don't use it yet*)
let doc =
let fd = open_in Sys.argv.(1) in
- let d = Tree.load_xml_file fd in
+ let d = Tree.Naive.load_xml_file fd in
close_in fd; d
let query =
let arg2 = Sys.argv.(2) in
- XPath.Parser.parse (Ulexing.from_latin1_string arg2)
+ Xpath.Parser.parse (Ulexing.from_latin1_string arg2)
open Format
let () =
- fprintf err_formatter "Query: %a\n%!" XPath.Ast.print_path query;
+ fprintf err_formatter "Query: %a\n%!" Xpath.Ast.print_path query;
fprintf err_formatter "Document:\n%!";
- Tree.print_xml stderr doc (Tree.root doc);
+ Tree.Naive.print_xml stderr doc (Tree.Naive.root doc);
exit 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-02-05 13:56:52 CET by Kim Nguyễn>
-*)
-
-type node = {
- tag : QName.t;
- preorder : int;
- mutable data : string;
- mutable first_child : node;
- mutable next_sibling : node;
- mutable parent: node;
-}
-
-
-
-let rec nil = {
- tag = QName.nil;
- preorder = -1;
- data = "";
- first_child = nil;
- next_sibling = nil;
- parent = nil;
-}
-
-let dummy_tag = QName.of_string "#dummy"
-let rec dummy = {
- tag = dummy_tag;
- preorder = -1;
- data = "";
- first_child = dummy;
- next_sibling = dummy;
- parent = dummy;
-}
-
-
-type t = {
- root : node;
- (* 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 attr_map_string = QName.to_string QName.attribute_map
-
- 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;
- 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;
- match attr_list with
- [] -> ()
- | _ ->
- start_element_handler parser_ ctx attr_map_string [];
- List.iter (do_attribute parser_ ctx) attr_list;
- end_element_handler parser_ ctx attr_map_string
-
- and do_attribute parser_ ctx (att, value) =
- let att_tag = " " ^ att in
- start_element_handler parser_ ctx att_tag [];
- start_element_handler parser_ ctx text_string [];
- let n = top ctx in n.data <- value;
- end_element_handler parser_ ctx text_string;
- 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 tag =
- 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;
- end_element_handler parser_ ctx text_string
-
-
-
- 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 parser_ = Expat.parser_create ~encoding:None in
- Expat.set_start_element_handler parser_ (start_element_handler parser_ ctx);
- Expat.set_end_element_handler parser_ (end_element_handler parser_ ctx);
- Expat.set_character_data_handler parser_ (character_data_handler parser_ ctx);
- push { tag = QName.document;
- preorder = next ctx;
- data = "";
- first_child = dummy;
- next_sibling = dummy;
- parent = nil;
- } ctx;
- (parser_,
- 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 }
- | _ -> 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 out tree_ node =
- if node != nil then begin
- output_string out (QName.to_string node.tag);
- output_string out "=\"";
- output_escape_string out node.first_child.data;
- output_char out '"';
- print_attributes out tree_ node.next_sibling
- end
-
-let rec print_xml out tree_ node =
- if node != nil then
- let () =
- if node.tag == QName.text then
- output_escape_string out node.data
- else
- let tag = QName.to_string node.tag in
- output_char out '<';
- output_string out tag;
- let fchild =
- if node.first_child.tag == QName.attribute_map then
- let () =
- print_attributes out tree_ node.first_child.first_child
- in
- node.first_child.next_sibling
- else
- 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
- in
- print_xml out tree_ node.next_sibling
-
-
-let root t = t.root
-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 preorder _ n = n.preorder
+++ /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:46 CET by Kim Nguyen>
-*)
-
-(** Implementation of documents as binary trees *)
-
-type node
-(** The type of a tree node *)
-
-type t
-(** The type of trees *)
-
-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 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].
-*)
--- /dev/null
+tree/Naive
--- /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:59:37 CET by Kim Nguyen>
+*)
+open Utils
+
+type node = {
+ tag : QName.t;
+ preorder : int;
+ mutable data : string;
+ mutable first_child : node;
+ mutable next_sibling : node;
+ mutable parent: node;
+}
+
+
+
+let rec nil = {
+ tag = QName.nil;
+ preorder = -1;
+ data = "";
+ first_child = nil;
+ next_sibling = nil;
+ parent = nil;
+}
+
+let dummy_tag = QName.of_string "#dummy"
+let rec dummy = {
+ tag = dummy_tag;
+ preorder = -1;
+ data = "";
+ first_child = dummy;
+ next_sibling = dummy;
+ parent = dummy;
+}
+
+
+type t = {
+ root : node;
+ (* 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 attr_map_string = QName.to_string QName.attribute_map
+
+ 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;
+ 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;
+ match attr_list with
+ [] -> ()
+ | _ ->
+ start_element_handler parser_ ctx attr_map_string [];
+ List.iter (do_attribute parser_ ctx) attr_list;
+ end_element_handler parser_ ctx attr_map_string
+
+ and do_attribute parser_ ctx (att, value) =
+ let att_tag = " " ^ att in
+ start_element_handler parser_ ctx att_tag [];
+ start_element_handler parser_ ctx text_string [];
+ let n = top ctx in n.data <- value;
+ end_element_handler parser_ ctx text_string;
+ 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 tag =
+ 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;
+ end_element_handler parser_ ctx text_string
+
+
+
+ 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 parser_ = Expat.parser_create ~encoding:None in
+ Expat.set_start_element_handler parser_ (start_element_handler parser_ ctx);
+ Expat.set_end_element_handler parser_ (end_element_handler parser_ ctx);
+ Expat.set_character_data_handler parser_ (character_data_handler parser_ ctx);
+ push { tag = QName.document;
+ preorder = next ctx;
+ data = "";
+ first_child = dummy;
+ next_sibling = dummy;
+ parent = nil;
+ } ctx;
+ (parser_,
+ 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 }
+ | _ -> 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 out tree_ node =
+ if node != nil then begin
+ output_string out (QName.to_string node.tag);
+ output_string out "=\"";
+ output_escape_string out node.first_child.data;
+ output_char out '"';
+ print_attributes out tree_ node.next_sibling
+ end
+
+let rec print_xml out tree_ node =
+ if node != nil then
+ let () =
+ if node.tag == QName.text then
+ output_escape_string out node.data
+ else
+ let tag = QName.to_string node.tag in
+ output_char out '<';
+ output_string out tag;
+ let fchild =
+ if node.first_child.tag == QName.attribute_map then
+ let () =
+ print_attributes out tree_ node.first_child.first_child
+ in
+ node.first_child.next_sibling
+ else
+ 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
+ in
+ print_xml out tree_ node.next_sibling
+
+
+let root t = t.root
+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 preorder _ n = n.preorder
--- /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:59:48 CET by Kim Nguyen>
+*)
+
+(** Implementation of documents as binary trees *)
+
+type node
+(** The type of a tree node *)
+
+type t
+(** The type of trees *)
+
+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 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].
+*)
+++ /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
-(***********************************************************************)
-(* *)
-(* 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:05:20 CET by Kim Nguyen>
-*)
-
-(** Various generic signatures and generic module and functor definitions
-*)
-INCLUDE "utils.ml"
-
-module HashSet (H : Hashtbl.HashedType) :
- Sigs.AUX.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 : Sigs.AUX.Type) (Y : Sigs.AUX.Type) :
- Sigs.AUX.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
+utils/FiniteCofinite
+utils/Hcons
+utils/Misc
+utils/Pretty
+utils/Ptset
+utils/QName
+utils/QNameSet
+utils/Sigs
+utils/Uid
--- /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:09:01 CET by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+include Sigs.FINITECOFINITE
+
+module type HConsBuilder =
+ functor (H : Sigs.AUX.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
+ | _ -> 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 = function
+ | { node = Finite s } when E.is_empty s -> true
+ | _ -> false
+
+ let is_any = function
+ | { node = CoFinite s } when E.is_empty s -> true
+ | _ -> false
+
+ let is_finite t = match t.node with
+ | Finite _ -> true | _ -> false
+
+ let kind t = match t.node with
+ | Finite _ -> `Finite
+ | _ -> `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 = Sigs.FINITECOFINITE.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
+ | _ -> raise exn
+
+ let is_singleton t = match t.node with
+ | Finite s -> E.is_singleton s
+ | _ -> 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 s, CoFinite t -> 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
+
+ | _ -> raise exn
+
+ let min_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | _ -> raise exn
+
+ let max_elt s = match s.node with
+ | Finite s -> E.min_elt s
+ | _ -> raise exn
+
+ let positive t =
+ match t.node with
+ | Finite x -> x
+ | _ -> E.empty
+
+ let negative t =
+ match t.node with
+ | CoFinite x -> x
+ | _ -> 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-01-30 19:08:57 CET by Kim Nguyen>
+*)
+
+(** Implementation of hashconsed finite or cofinite sets.
+*)
+
+include module type of Sigs.FINITECOFINITE
+
+(** 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-02-06 18:43:46 CET by Kim Nguyen>
+*)
+
+include Sigs.HCONS
+
+module type TableBuilder =
+ functor
+ (H : Sigs.AUX.HashedType) ->
+ Sigs.AUX.HashSet with type data = H.t
+
+module Builder (TB : TableBuilder) (H : Sigs.AUX.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-01-30 19:08:42 CET by Kim Nguyen>
+*)
+
+(** Implementation of generic hashconsing. *)
+
+include module type of Sigs.HCONS
+
+(** Output signature of the functor {!Hcons.Make} *)
+
+module Make (H : Sigs.AUX.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+ implementation of {!Sigs.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 : Sigs.AUX.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+ implementation of {!Sigs.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-01-30 19:05:20 CET by Kim Nguyen>
+*)
+
+(** Various generic signatures and generic module and functor definitions
+*)
+INCLUDE "utils.ml"
+
+module HashSet (H : Hashtbl.HashedType) :
+ Sigs.AUX.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 : Sigs.AUX.Type) (Y : Sigs.AUX.Type) :
+ Sigs.AUX.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-01-30 19:08:11 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 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 mk_repeater c =
+ let mk_str i = String.make i c in
+ let _table = Array.init 16 mk_str in
+ fun i -> try
+ if i < 16 then _table.(i) else mk_str i
+ with e -> print_int i; print_newline(); raise e
+let padding = mk_repeater ' '
+let line = mk_repeater '_'
+
+
+
+
+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 fmt () = ()
+
+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-01-30 19:08:06 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 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-01-30 19:07:53 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 Sigs.PTSET
+
+module type HConsBuilder =
+ functor (H : Sigs.AUX.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 : Sigs.AUX.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)
+
+ | _ -> 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
+ | _ -> 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-01-30 19:07:42 CET by Kim Nguyen>
+*)
+
+include module type of Sigs.PTSET
+
+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-01-30 19:07:38 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 cdata_section = of_string "#cdata-section"
+let comment = of_string "#comment"
+let document_fragment = of_string "#document-fragment"
+let attribute_map = of_string "#attribute-map"
+let nil = of_string "#"
--- /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:07:34 CET by Kim Nguyen>
+*)
+
+(** Implementation of qualified names as hashconsed strings *)
+
+include Sigs.HCONS.S with type data = string
+include Sigs.AUX.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 cdata_section : t
+(** Represents the QName of a document node. Equivalent to
+ [of_string "#cdata-section"]
+*)
+
+val comment : t
+(** Represents the QName of a comment node. Equivalent to
+ [of_string "#cdata-section"]
+*)
+
+val document_fragment : t
+(** Represents the QName of a document fragment. Equivalent to
+ [of_string "#document-fragment"]
+*)
+
+val attribute_map : t
+(** Represents the QName of a dummy document node holding the
+ attributes of the current element. Equivalent to
+ [of_string "#attribute-map"]
+*)
+
+val nil : t
+(** Represents the QName of a nil node. Equivalent to
+ [of_string "#"]
+*)
--- /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:07:29 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 =
+ if test e then print_finite fmt e conv
+ else begin
+ Format.fprintf fmt "%s \\ " Pretty.big_sigma;
+ print_finite fmt (inv e) conv
+ end
+
+let print fmt e = printer fmt e is_finite elements complement
+
+module Weak =
+struct
+ include FiniteCofinite.Weak(Ptset.Weak(QName))
+ let print fmt e = printer fmt e is_finite elements complement
+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:07:23 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 Sigs.AUX.Printable with type t := t
+
+module Weak :
+ sig
+ include FiniteCofinite.S with type elt = QName.t
+ include Sigs.AUX.Printable 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-02-05 15:58:13 CET by Kim Nguyen>
+*)
+
+(** This module contains all the signatures of the project, to avoid
+ code duplication. Each toplevel module (HCONS, PTSET, ...)
+ corresponds to an existing module in the project. The AUX modules
+ regroups common auxiliary signatures.
+*)
+
+
+(** The [AUX] module regroups the definitions of common interfaces *)
+module AUX =
+struct
+
+ (** 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
+
+ (** Type equiped with a pretty-printer *)
+ module type Printable =
+ sig
+ type t
+ val print : Format.formatter -> t -> unit
+ end
+
+ (** Type with both total ordering and hashing functions.
+ All modules of that type must enforce than:
+ [equal a b] if and only if [compare a b = 0]
+ *)
+ module type Type =
+ sig
+ type t
+ include HashedType with type t := t
+ include OrderedType with type t := t
+ 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
+end
+
+module HCONS =
+struct
+ (** 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
+
+end
+
+
+module PTSET =
+struct
+ module type S =
+ sig
+ include HCONS.S
+ include AUX.Set with type t := t
+ end
+end
+
+module FINITECOFINITE =
+struct
+ exception InfiniteSet
+ module type S =
+ sig
+ include HCONS.S
+ include AUX.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
+end
+
+module FORMULA =
+struct
+ module type ATOM =
+ sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include HCONS.S with type t := t
+ include AUX.Printable with type t := t
+ end
+ module type S =
+ sig
+ module Atom : ATOM
+ include HCONS.S
+ include AUX.Printable with type t := t
+ val of_bool : bool -> t
+ val true_ : t
+ val false_ : t
+ val or_ : t -> t -> t
+ val and_ : t -> t -> t
+ val not_ : t -> t
+ val diff_ : t -> t -> t
+ val eval : Atom.ctx -> t -> bool
+ end
+
+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
-Ast
-Parser
-Ulexer
-Xpath_internal_parser
--- /dev/null
+xpath/Ast
+xpath/Parser
+xpath/Ulexer
+xpath/Xpath_internal_parser
--- /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:04:30 CET by Kim Nguyen>
+*)
+
+open Utils
+
+type path = single_path list
+and single_path = Absolute of step list | Relative of step list
+and step = axis * test * expr list
+and axis = Self | Attribute | Child | Descendant | DescendantOrSelf | FollowingSibling
+ | Parent | Ancestor | AncestorOrSelf | PrecedingSibling | Preceding | Following
+
+and test = QNameSet.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 QName.t * expr list
+ | Path of path
+ | Binop of expr * binop * expr
+ | Unop of unop * expr
+
+
+type t = path
+
+
+let text = QNameSet.singleton QName.text
+let node = QNameSet.any
+let star =
+ QNameSet.complement (
+ QNameSet.from_list [ QName.text;
+ QName.document;
+ QName.cdata_section;
+ QName.comment])
+
+
+
+let pp fmt e = Format.fprintf fmt e
+
+let prio e =
+ match e with
+ | Unop (Neg, _) -> 11
+ | Path _ -> 10
+ | Number _ | String _ | Fun_call _ -> 9
+ | Binop (_,op,_) -> begin match op with
+ | Lt | Lte | Gt | Gte -> 7
+ | Neq | Eq -> 6
+ | And -> 5
+ | Or -> 4
+ | Mult | Div | Mod -> 3
+ | Add | Sub -> 2
+ end
+
+let print_binop fmt o =
+ pp fmt "%s" begin match o with
+ | Eq -> "="
+ | Neq -> "!="
+ | Lt -> "<"
+ | Gt -> ">"
+ | Lte -> "<="
+ | Gte -> ">="
+ | Or -> "or"
+ | And -> "and"
+ | Add -> "+"
+ | Sub -> "-"
+ | Mult -> "*"
+ | Div -> "div"
+ | Mod -> "mod"
+ end
+let print_unop fmt o =
+ pp fmt "%s" begin match o with
+ | Neg -> "-"
+ end
+
+let rec print_path fmt p =
+ Pretty.print_list ~sep:" | " print_single_path fmt p
+
+and print_single_path fmt p =
+ let l = match p with
+ | Absolute l -> pp fmt "/"; l
+ | Relative l -> l
+ in
+ Pretty.print_list ~sep:"/" print_step fmt l
+
+and print_step fmt (axis, test, expr) =
+ pp fmt "%a::%a" print_axis axis print_test test;
+ match expr with
+ [] -> ()
+ | l -> pp fmt "[ ";
+ Pretty.print_list ~sep:" ][ " print_expr fmt l;
+ pp fmt " ]"
+
+and print_axis fmt a = pp fmt "%s" begin
+ match a with
+ Self -> "self"
+ | Child -> "child"
+ | Descendant -> "descendant"
+ | DescendantOrSelf -> "descendant-or-self"
+ | FollowingSibling -> "following-sibling"
+ | Attribute -> "attribute"
+ | Ancestor -> "ancestor"
+ | AncestorOrSelf -> "ancestor-or-self"
+ | PrecedingSibling -> "preceding-sibling"
+ | Parent -> "parent"
+ | Preceding -> "preceding"
+ | Following -> "following"
+end
+
+and print_test fmt ts =
+ try
+ pp fmt "%s" (List.assoc ts
+ [ text,"text()";
+ node,"node()";
+ star, "*" ] )
+ with
+ Not_found -> pp fmt "%s"
+ (if QNameSet.is_finite ts
+ then QName.to_string (QNameSet.choose ts)
+ else "<INFINITE>"
+ )
+
+and print_expr fmt = function
+| Number (`Int(i)) -> pp fmt "%i" i
+| Number (`Float(f)) -> pp fmt "%f" f
+| String s -> pp fmt "'%S'" s
+| Fun_call (n, args) ->
+ pp fmt "%a(" QName.print n;
+ Pretty.print_list ~sep:", " print_expr fmt args;
+ pp fmt ")"
+| Path p -> print_path fmt p
+| Binop (e1, op, e2) as e ->
+ let pe = prio e in
+ let need_par1 = prio e1 < pe in
+ if need_par1 then pp fmt "(";
+ pp fmt "%a" print_expr e1;
+ if need_par1 then pp fmt ")";
+ pp fmt " %a " print_binop op;
+ let need_par2 = prio e2 < pe in
+ if need_par2 then pp fmt "(";
+ pp fmt "%a" print_expr e2;
+ if need_par2 then pp fmt ")"
+| Unop (op, e0) as e ->
+ let need_par0 = prio e0 < prio e in
+ print_unop fmt op;
+ if need_par0 then pp fmt "(";
+ print_expr fmt e0;
+ if need_par0 then pp fmt ")"
+
--- /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-02-07 09:35:40 CET by Kim Nguyen>
+*)
+
+type path = single_path list
+and single_path = Absolute of step list | Relative of step list
+and step = axis * test * expr list
+and axis = Self | Attribute | Child | Descendant | DescendantOrSelf | FollowingSibling
+ | Parent | Ancestor | AncestorOrSelf | PrecedingSibling | Preceding | Following
+
+and test = Utils.QNameSet.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
+ | 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 print_binop : Format.formatter -> binop -> unit
+val print_unop : Format.formatter -> unop -> unit
+val print_path : Format.formatter -> path -> unit
+val print_single_path : Format.formatter -> single_path -> unit
+val print_step : Format.formatter -> step -> unit
+val print_axis : Format.formatter -> axis -> unit
+val print_test : Format.formatter -> test -> unit
+val print_expr : Format.formatter -> expr -> 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-02-07 10:31:20 CET by Kim Nguyen>
+*)
+
+include Xpath_internal_parser
+
+let parse (l : Ulexing.lexbuf) =
+ xpath_query (fun _ -> Ulexer.token l) (Lexing.from_string "!!dummy!!")
+
--- /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-02-05 14:53:12 CET by Kim Nguyen>
+*)
+
+open Xpath_internal_parser
+
+module L = Ulexing
+
+exception Error of int * int * string
+
+let error i j s = raise (Error (i,j,s))
+
+(***********************************************************)
+(* Buffer for string literals *)
+
+let string_buff = Buffer.create 1024
+
+let store_lexeme lexbuf =
+ Buffer.add_string string_buff (Ulexing.utf8_lexeme lexbuf)
+let store_ascii = Buffer.add_char string_buff
+let store_code = Utf8.store string_buff
+let clear_buff () = Buffer.clear string_buff
+let get_stored_string () =
+ let s = Buffer.contents string_buff in
+ clear_buff ();
+ Buffer.clear string_buff;
+ s
+
+(***********************************************************)
+(* Lexer *)
+
+let illegal lexbuf =
+ error
+ (L.lexeme_start lexbuf)
+ (L.lexeme_end lexbuf)
+ "Illegal character"
+
+let return lexbuf tok = (tok, L.loc lexbuf)
+let return_loc i j tok = (tok, (i,j))
+
+let regexp ncname_char =
+ xml_letter | xml_digit | [ '-' '_' ] | xml_combining_char | xml_extender | "\\."
+
+let hexa_digit = function
+ | '0'..'9' as c -> (Char.code c) - (Char.code '0')
+ | 'a'..'f' as c -> (Char.code c) - (Char.code 'a') + 10
+ | 'A'..'F' as c -> (Char.code c) - (Char.code 'A') + 10
+ | _ -> -1
+
+let regexp ncname = ( xml_letter ncname_char* ) | ('_' ncname_char+)
+let regexp digit = ['0'-'9']
+let regexp float = '-'? digit+ ('.' digit+ (['e''E'] digit+)?)?
+
+let parse_char lexbuf base i =
+ let s = L.latin1_sub_lexeme lexbuf i (L.lexeme_length lexbuf - i - 1) in
+ let r = ref 0 in
+ for i = 0 to String.length s - 1 do
+ let c = hexa_digit s.[i] in
+ if (c >= base) || (c < 0) then
+ error (L.lexeme_start lexbuf) (L.lexeme_end lexbuf) "invalid digit";
+ r := !r * base + c;
+ done;
+ !r
+
+let keyword_or_tag s =
+ try
+ List.assoc s [
+ "self", AXIS Ast.Self;
+ "descendant", AXIS Ast.Descendant;
+ "child", AXIS Ast.Child;
+ "descendant-or-self", AXIS Ast.DescendantOrSelf;
+ "attribute", AXIS Ast.Attribute;
+ "following-sibling", AXIS Ast.FollowingSibling;
+ "preceding-sibling", AXIS Ast.PrecedingSibling;
+ "parent", AXIS Ast.Parent;
+ "ancestor", AXIS Ast.Ancestor;
+ "ancestor-or-self", AXIS Ast.AncestorOrSelf;
+ "preceding", AXIS Ast.Preceding;
+ "following", AXIS Ast.Following;
+ "and", AND;
+ "or" , OR;
+ "div", DIV;
+ "mod", MOD;
+ ]
+ with
+ _ -> TAG s
+
+
+let rec token = lexer
+ | [' ' '\t' '\n'] -> token lexbuf
+ | "*" -> STAR
+ | "/" -> SLASH
+ | "//" -> SLASHSLASH
+ | "::" -> COLONCOLON
+ | "(" -> LP
+ | ")" -> RP
+ | "[" -> LB
+ | "]" -> RB
+ | "," -> COMMA
+ | "|" -> PIPE
+ | "+" -> ADD
+ | "-" -> SUB
+ | "<" -> LT
+ | "<=" -> LTE
+ | ">" -> GT
+ | ">=" -> GTE
+ | "=" -> EQ
+ | "!=" -> NEQ
+ | "node()" -> NODE
+ | "text()" -> TEXT
+ | ncname -> keyword_or_tag (L.utf8_lexeme lexbuf)
+ | float ->
+ let s = L.utf8_lexeme lexbuf in
+ (try
+ INT (int_of_string s)
+ with
+ _ -> FLOAT (float_of_string s))
+ | '"' | "'" ->
+ let double_quote = L.latin1_lexeme_char lexbuf 0 = '"' in
+ string (L.lexeme_start lexbuf) double_quote lexbuf;
+ let s = get_stored_string () in
+ STRING s
+
+ | eof -> EOF
+ | _ -> illegal lexbuf
+
+and string start double = lexer
+ | '"' | "'" ->
+ let d = L.latin1_lexeme_char lexbuf 0 = '"' in
+ if d != double then (store_lexeme lexbuf; string start double lexbuf)
+ | '\\' ['\\' '"' '\''] ->
+ store_ascii (L.latin1_lexeme_char lexbuf 1);
+ string start double lexbuf
+ | "\\n" ->
+ store_ascii '\n'; string start double lexbuf
+ | "\\t" ->
+ store_ascii '\t'; string start double lexbuf
+ | "\\r" ->
+ store_ascii '\r'; string start double lexbuf
+ | '\\' ['0'-'9']+ ';' ->
+ store_code (parse_char lexbuf 10 1);
+ string start double lexbuf
+ | '\\' 'x' ['0'-'9' 'a'-'f' 'A'-'F']+ ';' ->
+ store_code (parse_char lexbuf 16 2);
+ string start double lexbuf
+ | '\\' ->
+ illegal lexbuf;
+ | eof ->
+ error start (start+1) "Unterminated string"
+ | _ ->
+ store_lexeme lexbuf;
+ string start double lexbuf
+
+
--- /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:31:01 CET by Kim Nguyen>
+*)
+
+ open Ast
+ let f () = ()
+%}
+
+%token <string> TAG
+%token <string> STRING
+%token <int> INT
+%token <float> FLOAT
+%token <Ast.axis> AXIS
+%token RB LB LP RP
+%token SLASH SLASHSLASH COLONCOLON STAR PIPE
+%token EQ NEQ LT GT LTE GTE OR AND ADD SUB DIV MOD
+%token NODE TEXT
+%token COMMA
+%token EOF
+
+%left OR
+%left AND
+%left EQ NEQ
+%left LT GT LTE GTE
+%left ADD SUB
+%left MOD DIV STAR
+%nonassoc uminus
+
+%start xpath_query
+%type <Ast.path> xpath_query
+
+
+%%
+xpath_query:
+path EOF { $1 }
+;
+
+path:
+ path_rev { List.rev $1 }
+;
+
+path_rev:
+ simple_path { [ $1 ] }
+| path_rev PIPE simple_path { $3 :: $1 }
+;
+
+
+simple_path:
+ absolute_path { Absolute (List.rev $1) }
+| relative_path { Relative (List.rev $1) }
+;
+
+absolute_path:
+ SLASH relative_path { $2 }
+| SLASHSLASH relative_path { (DescendantOrSelf, node, []) :: $2 }
+;
+
+relative_path:
+ step { [ $1 ] }
+| relative_path SLASH step { $3 :: $1 }
+| relative_path SLASHSLASH step { $3
+ :: (DescendantOrSelf, node, [])
+ :: $1 }
+;
+
+step:
+ axis_test pred_list { let a, b = $1 in a, b, $2 }
+;
+
+axis_test:
+ AXIS COLONCOLON test { $1, $3 }
+| test { Child, $1 }
+| AXIS {
+ 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)
+}
+;
+
+test:
+ NODE { node }
+| TEXT { text }
+| STAR { star }
+| TAG { Utils.QNameSet.singleton(Utils.QName.of_string $1) }
+;
+
+pred_list:
+ pred_list_rev { List.rev $1 }
+;
+
+pred_list_rev:
+ { [] }
+| pred_list LB expr RB { $3 :: $1 }
+;
+
+expr:
+ INT { Number(`Int($1)) }
+| FLOAT { Number(`Float($1)) }
+| STRING { String $1 }
+| SUB expr %prec uminus { Unop(Neg, $2) }
+| expr AND expr { Binop($1, And, $3) }
+| expr OR expr { Binop($1, Or, $3) }
+| expr ADD expr { Binop($1, Add, $3) }
+| expr SUB expr { Binop($1, Sub, $3) }
+| expr STAR expr { Binop($1, Mult, $3) }
+| expr DIV expr { Binop($1, Div, $3) }
+| expr MOD expr { Binop($1, Mod, $3) }
+| expr EQ expr { Binop($1, Eq, $3) }
+| expr NEQ expr { Binop($1, Neq, $3) }
+| expr LT expr { Binop($1, Lt, $3) }
+| 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) }
+| LP expr RP { $2 }
+| path { Path $1 }
+;
+
+arg_list:
+ { [] }
+| arg_list1 { List.rev $1 }
+;
+
+arg_list1:
+ expr { [ $1 ] }
+| arg_list1 COMMA expr { $3 :: $1 }
+;
+