From: Kim Nguyễn Date: Wed, 12 Oct 2016 15:44:32 +0000 (+0200) Subject: Simplify the automaton encoding a bit (remove redundant predicates in formulae). X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=fe2ba1820282783ae8c10fbbbd2b65d3dc4c67f2;hp=fed343e8df1900043dc993ac5458c757d3ac2ee0 Simplify the automaton encoding a bit (remove redundant predicates in formulae). --- diff --git a/src/naive_tree.ml b/src/naive_tree.ml index 3cefe18..89b9e86 100644 --- a/src/naive_tree.ml +++ b/src/naive_tree.ml @@ -130,12 +130,11 @@ first_child=%a; next_sibling=%a; parent=%a }" List.iter (do_attribute parser_ ctx) attr_list and do_attribute parser_ ctx (att, value) = - let att_tag = QName.to_string (QName.attribute (QName.of_string att)) in - start_element_handler parser_ ctx att_tag []; + start_element_handler parser_ ctx att []; let n = top ctx in n.data <- value; n.kind <- Tree.NodeKind.Attribute; - end_element_handler parser_ ctx att_tag + end_element_handler parser_ ctx att and consume_closing ctx n = if n.next_sibling != dummy then @@ -170,14 +169,11 @@ first_child=%a; next_sibling=%a; parent=%a }" and processing_instruction_handler parser_ ctx tag data = do_text parser_ ctx; - let pi = QName.to_string - (QName.processing_instruction (QName.of_string tag)) - in - start_element_handler parser_ ctx pi []; + start_element_handler parser_ ctx tag []; let node = top ctx in node.data <- data; node.kind <- Tree.NodeKind.ProcessingInstruction; - end_element_handler parser_ ctx pi + end_element_handler parser_ ctx tag let character_data_handler _parser ctx text = @@ -276,7 +272,7 @@ let output_escape_string out s = let rec print_attributes ?(sep=true) out tree_ node = if (node.kind == Tree.NodeKind.Attribute) then - let tag = QName.to_string (QName.remove_prefix node.tag) in + let tag = QName.to_string node.tag in if sep then output_char out ' '; output_string out tag; output_string out "=\""; @@ -313,7 +309,7 @@ let rec print_xml out tree_ node = output_string out "-->" | ProcessingInstruction -> output_string out "" diff --git a/src/qName.mli b/src/qName.mli index e738af5..7a892e9 100644 --- a/src/qName.mli +++ b/src/qName.mli @@ -49,7 +49,7 @@ val nil : t (** Represents the QName of a nil node. Equivalent to [of_string "#"] *) - +(* val attribute : t -> t (** Adds a prefix character (@) to distinguish the name from an element name @@ -64,3 +64,4 @@ val remove_prefix : t -> t (** Removes the prefix of the qname given as argument. Does not do anything if there is no prefix. *) +*) diff --git a/src/xpath/ast.ml b/src/xpath/ast.ml index 21ab5df..5b322a4 100644 --- a/src/xpath/ast.ml +++ b/src/xpath/ast.ml @@ -128,7 +128,7 @@ and print_test fmt (ts,kind) = | Element | Attribute -> pp fmt "%s" begin if QNameSet.is_finite ts then - QName.to_string (QName.remove_prefix (QNameSet.choose ts)) + QName.to_string (QNameSet.choose ts) else "*" end | Comment -> pp fmt "%s" "comment()" @@ -136,7 +136,7 @@ and print_test fmt (ts,kind) = pp fmt "processing-instruction(%s)" begin if ts == star then "" - else "\"" ^ (QName.to_string (QName.remove_prefix (QNameSet.choose ts))) ^ "\"" + else "\"" ^ (QName.to_string (QNameSet.choose ts)) ^ "\"" end | Node -> pp fmt "%s" "node()" | Document -> pp fmt "%s" "" diff --git a/src/xpath/ast.mli b/src/xpath/ast.mli index 07a410d..f2b2a1d 100644 --- a/src/xpath/ast.mli +++ b/src/xpath/ast.mli @@ -14,6 +14,8 @@ (***********************************************************************) type path = single_path list + (* the step are given in reverse with the last step of the query + being the first of the step list *) and single_path = Absolute of step list | Relative of step list and step = axis * test * expr list and axis = Self | Attribute | Child diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index 20f06be..d33fbb4 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -42,8 +42,8 @@ let root_set = QNameSet.singleton QName.document let compile_axis_test axis (test,kind) phi trans states = let q = State.next () in let phi = match kind with - Tree.NodeKind.Node -> phi - | _ -> phi %% F.is kind + Tree.NodeKind.Node -> phi + | _ -> phi %% F.is kind in let phi', trans', states' = match axis with @@ -156,9 +156,9 @@ and compile_step_list l trans states = aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist (** - Compile the top-level XPath query in reverse (doing downward + Compile the top-level XPath query in reverse (going downward to the last top-level state): - /a0::t0[p0]/.../an-1::tn-1[pn-1]/an::tn[pn] becomes: + /a0::t0[p0]/../an-1::tn-1[pn-1]/an::tn[pn] becomes: self::node()[ pn and self::tn[pn]/inv(an)::(tn-1)[pn-1]/.../inv(a1)::t0[p0]/inv(a0)::document()] @@ -179,34 +179,34 @@ let compile_top_level_step_list l trans states = (* Only select attribute nodes if the previous axis is attribute *) let phi0 = - if axis != Attribute then + if axis != Attribute && kind == Tree.NodeKind.Node then phi0 %% (F.not_ F.is_attribute) else phi0 in match ll with [] -> - let phi1, trans1, states1 = - List.fold_left (fun (aphi, atrans, astates) e -> + let phi1, trans1, states1 = + List.fold_left (fun (aphi, atrans, astates) e -> let ephi, etrans, estates = compile_expr e atrans astates in aphi %% ephi, etrans, estates) (phi0, trans0, states0) elist - in - let _, trans2, states2 = - compile_axis_test Self (test,kind) phi1 trans1 states1 - in - let marking_state = - StateSet.choose (StateSet.diff states2 states1) - in - marking_state, trans2, states2 + in + let _, trans2, states2 = + compile_axis_test Self (test,kind) phi1 trans1 states1 + in + let marking_state = + StateSet.choose (StateSet.diff states2 states1) + in + marking_state, trans2, states2 | _ -> - let phi1, trans1, states1 = - compile_axis_test Self (test,kind) phi0 trans0 states0 - in - let phi2, trans2, states2 = - List.fold_left (fun (aphi, atrans, astates) e -> + let phi1, trans1, states1 = + compile_axis_test Self (test,kind) phi0 trans0 states0 + in + let phi2, trans2, states2 = + List.fold_left (fun (aphi, atrans, astates) e -> let ephi, etrans, estates = compile_expr e atrans astates in aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist - in - loop ll trans2 states2 phi2 + in + loop ll trans2 states2 phi2 in let starting = State.next () in let phi0, trans0, states0 = diff --git a/src/xpath/ulexer.ml b/src/xpath/ulexer.ml index baa794d..02b6e02 100644 --- a/src/xpath/ulexer.ml +++ b/src/xpath/ulexer.ml @@ -122,7 +122,8 @@ let rec token = lexer | "node()" -> NODE | "text()" -> TEXT | "comment()" -> COMMENT - | '@' ncname -> ATTNAME (L.utf8_lexeme lexbuf) + | '@' ncname -> let l = L.utf8_lexeme lexbuf in + ATTNAME (String.sub l 1 (String.length l - 1)) | "processing-instruction()" -> PI "" | "processing-instruction('"ncname"')" | "processing-instruction(\""ncname"\")"-> diff --git a/src/xpath/xpath_internal_parser.mly b/src/xpath/xpath_internal_parser.mly index e5c0700..6395b6e 100644 --- a/src/xpath/xpath_internal_parser.mly +++ b/src/xpath/xpath_internal_parser.mly @@ -99,12 +99,7 @@ step: axis_test: AXIS COLONCOLON test { let a, (t,k) = $1, $3 in match a with - Attribute when QNameSet.is_finite t -> - [ a, ((QNameSet.fold - (fun t a -> - QNameSet.add - (QName.attribute t) a) - t QNameSet.empty), k) ] + | Attribute -> [ a, (t, NodeKind.Attribute) ] | Preceding|Following -> [ (Descendant true, (t,k)); if a == Preceding then @@ -136,8 +131,7 @@ test: } | PI { (if $1 = "" then star else QNameSet.singleton( - QName.processing_instruction ( - QName.of_string $1) + QName.of_string $1 )), NodeKind.ProcessingInstruction } | TAG { QNameSet.singleton(QName.of_string $1),