From: Kim Nguyễn Date: Thu, 7 Feb 2013 09:36:30 +0000 (+0100) Subject: Refactor module organisation and build process. X-Git-Tag: v0.1~185 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=30bc0bb1291426e5e26eb2dee1ffc41e4c246349 Refactor module organisation and build process. --- diff --git a/Makefile b/Makefile index 83aeb8f..5e3c1ad 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,8 @@ -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 diff --git a/_tags b/_tags index cf9b611..11dbbef 100644 --- a/_tags +++ b/_tags @@ -1 +1,4 @@ -: for-pack(XPath) +: for-pack(Xpath) +: for-pack(Utils) +: for-pack(Tree) +: for-pack(Auto) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 1bb2410..2d9913e 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -1,177 +1,28 @@ -(***********************************************************************) -(* *) -(* 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: -*) - 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 diff --git a/myocamlbuild_config.ml b/myocamlbuild_config.ml deleted file mode 100644 index ef9d2e6..0000000 --- a/myocamlbuild_config.ml +++ /dev/null @@ -1,34 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 = [];; diff --git a/scripts/gen_mlpack.sh b/scripts/gen_mlpack.sh new file mode 100755 index 0000000..95f78ec --- /dev/null +++ b/scripts/gen_mlpack.sh @@ -0,0 +1,29 @@ +#!/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 diff --git a/src/XPath/ast.ml b/src/XPath/ast.ml deleted file mode 100644 index a097024..0000000 --- a/src/XPath/ast.ml +++ /dev/null @@ -1,164 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - - -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 "" - ) - -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 ")" - diff --git a/src/XPath/ast.mli b/src/XPath/ast.mli deleted file mode 100644 index a2b0579..0000000 --- a/src/XPath/ast.mli +++ /dev/null @@ -1,49 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 - diff --git a/src/XPath/parser.ml b/src/XPath/parser.ml deleted file mode 100644 index 69e76e1..0000000 --- a/src/XPath/parser.ml +++ /dev/null @@ -1,24 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -include Xpath_internal_parser - -let parse (l : Ulexing.lexbuf) = - xpath (fun _ -> Ulexer.token l) (Lexing.from_string "!!dummy!!") - diff --git a/src/XPath/ulexer.ml b/src/XPath/ulexer.ml deleted file mode 100644 index aa66179..0000000 --- a/src/XPath/ulexer.ml +++ /dev/null @@ -1,169 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 - - diff --git a/src/XPath/xpath_internal_parser.mly b/src/XPath/xpath_internal_parser.mly deleted file mode 100644 index cd32ebb..0000000 --- a/src/XPath/xpath_internal_parser.mly +++ /dev/null @@ -1,145 +0,0 @@ -%{ -(***********************************************************************) -(* *) -(* 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: -*) - - open Ast - let f () = () -%} - -%token TAG -%token STRING -%token INT -%token FLOAT -%token 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 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 } -; - diff --git a/src/ata.ml b/src/ata.ml deleted file mode 100644 index 6ec859c..0000000 --- a/src/ata.ml +++ /dev/null @@ -1,160 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/auto.mlpack b/src/auto.mlpack new file mode 100644 index 0000000..af2dae6 --- /dev/null +++ b/src/auto.mlpack @@ -0,0 +1,4 @@ +auto/Ata +auto/Formula +auto/State +auto/StateSet diff --git a/src/auto/ata.ml b/src/auto/ata.ml new file mode 100644 index 0000000..5001ebc --- /dev/null +++ b/src/auto/ata.ml @@ -0,0 +1,162 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/auto/formula.ml b/src/auto/formula.ml new file mode 100644 index 0000000..70407cf --- /dev/null +++ b/src/auto/formula.ml @@ -0,0 +1,186 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/auto/formula.mli b/src/auto/formula.mli new file mode 100644 index 0000000..3cf240d --- /dev/null +++ b/src/auto/formula.mli @@ -0,0 +1,91 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/auto/state.ml b/src/auto/state.ml new file mode 100644 index 0000000..83ad4b4 --- /dev/null +++ b/src/auto/state.ml @@ -0,0 +1,41 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/auto/state.mli b/src/auto/state.mli new file mode 100644 index 0000000..f86ddcd --- /dev/null +++ b/src/auto/state.mli @@ -0,0 +1,31 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 *) diff --git a/src/auto/stateSet.ml b/src/auto/stateSet.ml new file mode 100644 index 0000000..e99cd5e --- /dev/null +++ b/src/auto/stateSet.ml @@ -0,0 +1,27 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +open Format +open Utils + +include Ptset.Make (Hcons.PosInt) + +let print ppf s = + fprintf ppf "{ %a }" + (Pretty.print_list ~sep:" " (State.print)) (elements s) diff --git a/src/auto/stateSet.mli b/src/auto/stateSet.mli new file mode 100644 index 0000000..96b5b6d --- /dev/null +++ b/src/auto/stateSet.mli @@ -0,0 +1,24 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** Implementation of sets of states *) +include Utils.Ptset.S with type elt = int + +val print : Format.formatter -> t -> unit +(** Pretty printer *) diff --git a/src/finiteCofinite.ml b/src/finiteCofinite.ml deleted file mode 100644 index 8d3c3ee..0000000 --- a/src/finiteCofinite.ml +++ /dev/null @@ -1,222 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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) diff --git a/src/finiteCofinite.mli b/src/finiteCofinite.mli deleted file mode 100644 index 44ec882..0000000 --- a/src/finiteCofinite.mli +++ /dev/null @@ -1,36 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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}. -*) diff --git a/src/formula.ml b/src/formula.ml deleted file mode 100644 index ad774ea..0000000 --- a/src/formula.ml +++ /dev/null @@ -1,186 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/formula.mli b/src/formula.mli deleted file mode 100644 index e83bca1..0000000 --- a/src/formula.mli +++ /dev/null @@ -1,91 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/hcons.ml b/src/hcons.ml deleted file mode 100644 index 1fc059c..0000000 --- a/src/hcons.ml +++ /dev/null @@ -1,84 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/hcons.mli b/src/hcons.mli deleted file mode 100644 index c1e8c00..0000000 --- a/src/hcons.mli +++ /dev/null @@ -1,45 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 ] -*) diff --git a/src/pretty.ml b/src/pretty.ml deleted file mode 100644 index c54d0ed..0000000 --- a/src/pretty.ml +++ /dev/null @@ -1,156 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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) - - diff --git a/src/pretty.mli b/src/pretty.mli deleted file mode 100644 index 42ec6cb..0000000 --- a/src/pretty.mli +++ /dev/null @@ -1,56 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/ptset.ml b/src/ptset.ml deleted file mode 100644 index ee0370a..0000000 --- a/src/ptset.ml +++ /dev/null @@ -1,380 +0,0 @@ -(* 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: -*) - -(* 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 diff --git a/src/ptset.mli b/src/ptset.mli deleted file mode 100644 index dc80b4a..0000000 --- a/src/ptset.mli +++ /dev/null @@ -1,33 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 *) diff --git a/src/qName.ml b/src/qName.ml deleted file mode 100644 index ca4a5a3..0000000 --- a/src/qName.ml +++ /dev/null @@ -1,37 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 "#" diff --git a/src/qName.mli b/src/qName.mli deleted file mode 100644 index 081c24d..0000000 --- a/src/qName.mli +++ /dev/null @@ -1,71 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 "#"] -*) diff --git a/src/qNameSet.ml b/src/qNameSet.ml deleted file mode 100644 index e1fa8a1..0000000 --- a/src/qNameSet.ml +++ /dev/null @@ -1,40 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/qNameSet.mli b/src/qNameSet.mli deleted file mode 100644 index ae182b6..0000000 --- a/src/qNameSet.mli +++ /dev/null @@ -1,30 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 diff --git a/src/sigs.ml b/src/sigs.ml deleted file mode 100644 index 1022404..0000000 --- a/src/sigs.ml +++ /dev/null @@ -1,237 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 diff --git a/src/state.ml b/src/state.ml deleted file mode 100644 index bd1c72c..0000000 --- a/src/state.ml +++ /dev/null @@ -1,40 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 diff --git a/src/state.mli b/src/state.mli deleted file mode 100644 index f86ddcd..0000000 --- a/src/state.mli +++ /dev/null @@ -1,31 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 *) diff --git a/src/stateSet.ml b/src/stateSet.ml deleted file mode 100644 index 5871c7e..0000000 --- a/src/stateSet.ml +++ /dev/null @@ -1,26 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -open Format - -include Ptset.Make (Hcons.PosInt) - -let print ppf s = - fprintf ppf "{ %a }" - (Pretty.print_list ~sep:" " (State.print)) (elements s) diff --git a/src/stateSet.mli b/src/stateSet.mli deleted file mode 100644 index 1de4dee..0000000 --- a/src/stateSet.mli +++ /dev/null @@ -1,24 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** Implementation of sets of states *) -include Ptset.S with type elt = int - -val print : Format.formatter -> t -> unit -(** Pretty printer *) diff --git a/src/test.ml b/src/test.ml index dec8918..e854f44 100644 --- a/src/test.ml +++ b/src/test.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** use: xml_file "XPath querie" @@ -22,26 +22,26 @@ 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 diff --git a/src/tree.ml b/src/tree.ml deleted file mode 100644 index 71f9a98..0000000 --- a/src/tree.ml +++ /dev/null @@ -1,272 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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 "' - 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 diff --git a/src/tree.mli b/src/tree.mli deleted file mode 100644 index 72cd077..0000000 --- a/src/tree.mli +++ /dev/null @@ -1,80 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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]. -*) diff --git a/src/tree.mlpack b/src/tree.mlpack new file mode 100644 index 0000000..933b481 --- /dev/null +++ b/src/tree.mlpack @@ -0,0 +1 @@ +tree/Naive diff --git a/src/tree/naive.ml b/src/tree/naive.ml new file mode 100644 index 0000000..1086b1e --- /dev/null +++ b/src/tree/naive.ml @@ -0,0 +1,273 @@ +(***********************************************************************) +(* *) +(* 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: +*) +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 "' + 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 diff --git a/src/tree/naive.mli b/src/tree/naive.mli new file mode 100644 index 0000000..60d1258 --- /dev/null +++ b/src/tree/naive.mli @@ -0,0 +1,80 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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]. +*) diff --git a/src/uid.ml b/src/uid.ml deleted file mode 100644 index 0cb9688..0000000 --- a/src/uid.ml +++ /dev/null @@ -1,33 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -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" diff --git a/src/uid.mli b/src/uid.mli deleted file mode 100644 index 286cacc..0000000 --- a/src/uid.mli +++ /dev/null @@ -1,45 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 *) diff --git a/src/utils.ml b/src/utils.ml deleted file mode 100644 index 960ec46..0000000 --- a/src/utils.ml +++ /dev/null @@ -1,51 +0,0 @@ -(***********************************************************************) -(* *) -(* 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: -*) - -(** 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 diff --git a/src/utils.mlpack b/src/utils.mlpack new file mode 100644 index 0000000..27622d0 --- /dev/null +++ b/src/utils.mlpack @@ -0,0 +1,9 @@ +utils/FiniteCofinite +utils/Hcons +utils/Misc +utils/Pretty +utils/Ptset +utils/QName +utils/QNameSet +utils/Sigs +utils/Uid diff --git a/src/utils/finiteCofinite.ml b/src/utils/finiteCofinite.ml new file mode 100644 index 0000000..8d3c3ee --- /dev/null +++ b/src/utils/finiteCofinite.ml @@ -0,0 +1,222 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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) diff --git a/src/utils/finiteCofinite.mli b/src/utils/finiteCofinite.mli new file mode 100644 index 0000000..44ec882 --- /dev/null +++ b/src/utils/finiteCofinite.mli @@ -0,0 +1,36 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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}. +*) diff --git a/src/utils/hcons.ml b/src/utils/hcons.ml new file mode 100644 index 0000000..eba8bac --- /dev/null +++ b/src/utils/hcons.ml @@ -0,0 +1,84 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/utils/hcons.mli b/src/utils/hcons.mli new file mode 100644 index 0000000..c1e8c00 --- /dev/null +++ b/src/utils/hcons.mli @@ -0,0 +1,45 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 ] +*) diff --git a/src/utils/misc.ml b/src/utils/misc.ml new file mode 100644 index 0000000..960ec46 --- /dev/null +++ b/src/utils/misc.ml @@ -0,0 +1,51 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml new file mode 100644 index 0000000..c54d0ed --- /dev/null +++ b/src/utils/pretty.ml @@ -0,0 +1,156 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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) + + diff --git a/src/utils/pretty.mli b/src/utils/pretty.mli new file mode 100644 index 0000000..42ec6cb --- /dev/null +++ b/src/utils/pretty.mli @@ -0,0 +1,56 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/utils/ptset.ml b/src/utils/ptset.ml new file mode 100644 index 0000000..ee0370a --- /dev/null +++ b/src/utils/ptset.ml @@ -0,0 +1,380 @@ +(* 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: +*) + +(* 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 diff --git a/src/utils/ptset.mli b/src/utils/ptset.mli new file mode 100644 index 0000000..dc80b4a --- /dev/null +++ b/src/utils/ptset.mli @@ -0,0 +1,33 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 *) diff --git a/src/utils/qName.ml b/src/utils/qName.ml new file mode 100644 index 0000000..ca4a5a3 --- /dev/null +++ b/src/utils/qName.ml @@ -0,0 +1,37 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 "#" diff --git a/src/utils/qName.mli b/src/utils/qName.mli new file mode 100644 index 0000000..081c24d --- /dev/null +++ b/src/utils/qName.mli @@ -0,0 +1,71 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 "#"] +*) diff --git a/src/utils/qNameSet.ml b/src/utils/qNameSet.ml new file mode 100644 index 0000000..e1fa8a1 --- /dev/null +++ b/src/utils/qNameSet.ml @@ -0,0 +1,40 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 diff --git a/src/utils/qNameSet.mli b/src/utils/qNameSet.mli new file mode 100644 index 0000000..ae182b6 --- /dev/null +++ b/src/utils/qNameSet.mli @@ -0,0 +1,30 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 diff --git a/src/utils/sigs.ml b/src/utils/sigs.ml new file mode 100644 index 0000000..1022404 --- /dev/null +++ b/src/utils/sigs.ml @@ -0,0 +1,237 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 diff --git a/src/utils/uid.ml b/src/utils/uid.ml new file mode 100644 index 0000000..0cb9688 --- /dev/null +++ b/src/utils/uid.ml @@ -0,0 +1,33 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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" diff --git a/src/utils/uid.mli b/src/utils/uid.mli new file mode 100644 index 0000000..286cacc --- /dev/null +++ b/src/utils/uid.mli @@ -0,0 +1,45 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +(** 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 *) diff --git a/src/xPath.mlpack b/src/xPath.mlpack deleted file mode 100644 index e062c25..0000000 --- a/src/xPath.mlpack +++ /dev/null @@ -1,4 +0,0 @@ -Ast -Parser -Ulexer -Xpath_internal_parser diff --git a/src/xpath.mlpack b/src/xpath.mlpack new file mode 100644 index 0000000..7619c15 --- /dev/null +++ b/src/xpath.mlpack @@ -0,0 +1,4 @@ +xpath/Ast +xpath/Parser +xpath/Ulexer +xpath/Xpath_internal_parser diff --git a/src/xpath/ast.ml b/src/xpath/ast.ml new file mode 100644 index 0000000..c3c00d9 --- /dev/null +++ b/src/xpath/ast.ml @@ -0,0 +1,165 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 "" + ) + +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 ")" + diff --git a/src/xpath/ast.mli b/src/xpath/ast.mli new file mode 100644 index 0000000..f2a4df7 --- /dev/null +++ b/src/xpath/ast.mli @@ -0,0 +1,49 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 + diff --git a/src/xpath/parser.ml b/src/xpath/parser.ml new file mode 100644 index 0000000..ed5283e --- /dev/null +++ b/src/xpath/parser.ml @@ -0,0 +1,24 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +include Xpath_internal_parser + +let parse (l : Ulexing.lexbuf) = + xpath_query (fun _ -> Ulexer.token l) (Lexing.from_string "!!dummy!!") + diff --git a/src/xpath/ulexer.ml b/src/xpath/ulexer.ml new file mode 100644 index 0000000..aa66179 --- /dev/null +++ b/src/xpath/ulexer.ml @@ -0,0 +1,169 @@ +(***********************************************************************) +(* *) +(* 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: +*) + +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 + + diff --git a/src/xpath/xpath_internal_parser.mly b/src/xpath/xpath_internal_parser.mly new file mode 100644 index 0000000..04ecf36 --- /dev/null +++ b/src/xpath/xpath_internal_parser.mly @@ -0,0 +1,145 @@ +%{ +(***********************************************************************) +(* *) +(* 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: +*) + + open Ast + let f () = () +%} + +%token TAG +%token STRING +%token INT +%token FLOAT +%token 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 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 } +; +