* added backtracking in matching code (hairy code!)

[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.ml

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 6b1266ec8c41bd62410c3f68f443f1e18af10fa1..1a0c024104feaaab9f730ed16c5101c3f72ce965 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -139,7 +139,18 @@ struct
         k
       else if are_empty t then
         let res = match_cb (matched t) in
-        (fun matched_terms _ -> res matched_terms)
+        (fun matched_terms terms ->
+          match res 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)
       else
         match horizontal_split t with
         | _, [], _ -> assert false
@@ -331,12 +342,9 @@ struct
          (fun term env ->
             prerr_endline "GUARDIA?" ;
             match compiled_guard term with
-              | None -> 
-                  prerr_endline "SONO CAZZI H2SO4" ;
-                  None
+              | None -> None
               | Some _ ->
                   begin
-                    prerr_endline "OKKKKKKKKKKKKKK" ;
                     match compiled_p term with
                       | None -> None
                       | Some (env', _) ->