- bugfix: when backtracking restore the appropriate matched terms instead of keeping...

- changed column order while matching constructors, this should speed up the matching since often application head discriminate if a row can be applied or not

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index a10d0a8bddd92068e77fb4bd598e092a8876c2c1..8ac7dcdf50db0d888ddf72e5626d557eb24e8a9c 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -116,47 +116,47 @@ struct
         | _ -> assert false)
       t
 
-  let variable_closure k =
+  let variable_closure ksucc =
     (fun matched_terms terms ->
+(* prerr_endline "variable_closure"; *)
       match terms with
-      | hd :: tl -> k (hd :: matched_terms) tl
+      | hd :: tl -> ksucc (hd :: matched_terms) tl
       | _ -> assert false)
 
-  let success_closure ks k =
+  let success_closure ksucc =
     (fun matched_terms terms ->
-       match ks matched_terms with
-          None ->
-            begin
-              (* the match has failed, we rollback the last matched term
-               * into the unmatched ones and call the failure continuation
-               *)
-              match matched_terms with
-                  hd :: tl -> k tl (hd :: terms)
-                | _ -> assert false
-            end
-        | Some v -> Some v)
-
-  let constructor_closure ks k =
+(* prerr_endline "success_closure"; *)
+       ksucc matched_terms)
+
+  let constructor_closure ksuccs =
     (fun matched_terms terms ->
+(* prerr_endline "constructor_closure"; *)
       match terms with
       | t :: tl ->
           (try
             let tag, subterms = P.tag_of_term t in
-            let k' = List.assoc tag ks in
+            let k' = List.assoc tag ksuccs in
             k' matched_terms (subterms @ tl)
-          with Not_found -> k matched_terms terms)
+          with Not_found -> None)
       | [] -> assert false)
 
+  let backtrack_closure ksucc kfail =
+    (fun matched_terms terms ->
+(* prerr_endline "backtrack_closure"; *)
+      match ksucc matched_terms terms with
+      | Some x -> Some x
+      | None -> kfail matched_terms terms)
+
   let compiler rows match_cb fail_k =
-    let rec aux t k =
+    let rec aux t =
       if t = [] then
-        k
+        (fun _ _ -> fail_k ())
       else if are_empty t then
-        success_closure (match_cb (matched t)) k
+        success_closure (match_cb (matched t))
       else
         match horizontal_split t with
         | _, [], _ -> assert false
-        | Variable, t', [] -> variable_closure (aux (vertical_split t') k)
+        | Variable, t', [] -> variable_closure (aux (vertical_split t'))
         | Constructor, t', [] ->
             let tagl =
               List.map
@@ -166,7 +166,7 @@ struct
                 t'
             in
             let clusters = partition t' tagl in
-            let ks =
+            let ksuccs =
               List.map
                 (fun (tag, cluster) ->
                   let cluster' =
@@ -178,14 +178,14 @@ struct
                         | _ -> assert false)
                       cluster
                   in
-                  tag, aux cluster' k)
+                  tag, aux cluster')
                 clusters
             in
-            constructor_closure ks k
-        | _, t', t'' -> aux t' (aux t'' k)
+            constructor_closure ksuccs
+        | _, t', t'' -> backtrack_closure (aux t') (aux t'')
     in
     let t = List.map (fun (p, pid) -> [], [p], pid) rows in
-    let matcher = aux t (fun _ _ -> fail_k ()) in
+    let matcher = aux t in
     (fun term -> matcher [] [term])
 end
 
@@ -203,7 +203,7 @@ struct
       | Ast.Literal _ as t -> assert false
       | _ -> Constructor
     let tag_of_pattern = CicNotationTag.get_tag
-    let tag_of_term = CicNotationTag.get_tag
+    let tag_of_term t = CicNotationTag.get_tag t
   end
 
   module M = Matcher (Pattern21)
@@ -227,17 +227,19 @@ struct
     term', !magic_map
 
   let env_of_matched pl tl =
-    List.map2
-      (fun p t ->
-        match p, t with
-          Ast.Variable (Ast.TermVar name), _ ->
-            name, (Env.TermType, Env.TermValue t)
-        | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
-            name, (Env.NumType, Env.NumValue s)
-        | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
-            name, (Env.StringType, Env.StringValue s)
-        | _ -> assert false)
-      pl tl
+    try
+      List.map2
+        (fun p t ->
+          match p, t with
+            Ast.Variable (Ast.TermVar name), _ ->
+              name, (Env.TermType, Env.TermValue t)
+          | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
+              name, (Env.NumType, Env.NumValue s)
+          | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+              name, (Env.StringType, Env.StringValue s)
+          | _ -> assert false)
+        pl tl
+    with Invalid_argument _ -> assert false
 
   let rec compiler rows =
     let rows', magic_maps =
@@ -255,8 +257,7 @@ struct
           (fun env ->
             match m_checker (Env.lookup_term env name) env with
             | None -> None
-            | Some env' ->
-               f env'))
+            | Some env' -> f env'))
         (fun env -> Some env)
         map
     in
@@ -286,7 +287,7 @@ struct
             pid, pl, magichecker magic_map)
           rows
       in
-       magichooser candidates
+      magichooser candidates
     in
     M.compiler rows' match_cb (fun _ -> None)
 
@@ -400,13 +401,15 @@ struct
       let pl, pid = try List.hd rows with Not_found -> assert false in
       (fun matched_terms ->
         let env =
-          List.map2
-            (fun p t ->
-              match p with
-              | Ast.ImplicitPattern -> Util.fresh_name (), t
-              | Ast.VarPattern name -> name, t
-              | _ -> assert false)
-            pl matched_terms
+          try
+            List.map2
+              (fun p t ->
+                match p with
+                | Ast.ImplicitPattern -> Util.fresh_name (), t
+                | Ast.VarPattern name -> name, t
+                | _ -> assert false)
+              pl matched_terms
+          with Invalid_argument _ -> assert false
         in
         Some (env, pid))
     in

diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml
index 53ac5e2d13416f505b241dc51f3cd9a87045d6cc..3cbffa2db885425ebc2ee84946ba9caf4eee5159 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationTag.ml
+++ b/helm/ocaml/cic_notation/cicNotationTag.ml
@@ -41,5 +41,5 @@ let get_tag term0 =
   in
   let term_mask = aux term0 in
   let tag = Hashtbl.hash term_mask in
-  tag, !subterms
+  tag, List.rev !subterms