snapshot

[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 39c82b7dadb66a1e095969c133ff2d9ab23d5078..9d879db5ea1c3ef6943b2ae2e36c04ec007ca95c 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -122,6 +122,20 @@ struct
       | hd :: tl -> k (hd :: matched_terms) tl
       | _ -> assert false)
 
+  let success_closure ks k =
+    (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 =
     (fun matched_terms terms ->
       match terms with
@@ -138,19 +152,7 @@ struct
       if t = [] then
         k
       else if are_empty t then
-        let res = match_cb (matched t) in
-        (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)
+        success_closure (match_cb (matched t)) k
       else
         match horizontal_split t with
         | _, [], _ -> assert false
@@ -248,29 +250,23 @@ struct
     let magichecker map =
       List.fold_left
         (fun f (name, m) ->
-          prerr_endline ("compiling magichecker for " ^ name) ;
           let m_checker = compile_magic m in
           (fun env ->
             match m_checker (Env.lookup_term env name) env with
             | None -> None
             | Some env' ->
                f env'))
-        (fun env ->
-            prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ;       
-          Some env)
+        (fun env -> Some env)
         map
     in
     let magichooser candidates =
       List.fold_left
         (fun f (pid, pl, checker) ->
-          List.iter (fun p -> prerr_endline ("P = " ^ Pp.pp_term p)) pl ;
           (fun matched_terms ->
             let env = env_of_matched pl matched_terms in
             match checker env with
             | None -> f matched_terms
             | Some env ->
-               prerr_endline (String.concat " / " (List.map Pp.pp_term pl)) ;
-               prerr_endline ("magichoose found a match for " ^ Pp.pp_env env ^ " " ^ string_of_int pid) ;
                let magic_map =
                  try List.assoc pid magic_maps with Not_found -> assert false
                in
@@ -334,33 +330,21 @@ struct
           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
           | _ -> assert false)
 
-    | Pt.If (guard, p) ->
-       let compiled_guard = compiler [guard, 0]
-       and compiled_p = compiler [p, 0] in
-         (fun term env ->
-            match compiled_guard term with
-              | None -> None
-              | Some _ ->
-                  begin
-                    match compiled_p term with
-                      | None -> None
-                      | Some (env', _) ->
-                          Some (env' @ env)
-                  end)
-
-    | Pt.Unless (guard, p) ->
-       let compiled_guard = compiler [guard, 0]
-       and compiled_p = compiler [p, 0] in
+    | Pt.If (p_test, p_true, p_false) ->
+       let compiled_test = compiler [p_test, 0]
+       and compiled_true = compiler [p_true, 0]
+       and compiled_false = compiler [p_false, 0] in
          (fun term env ->
-            match compiled_guard term with
-              | None ->
-                  begin
-                    match compiled_p term with
-                      | None -> None
-                      | Some (env', _) ->
-                          Some (env' @ env)
-                  end
-              | Some _ -> None)
+            let branch =
+              match compiled_test term with
+                | None -> compiled_false
+                | Some _ -> compiled_true
+            in
+              match branch term with
+                | None -> None
+                | Some (env', _) -> Some (env' @ env))
+
+    | Pt.Fail -> (fun _ _ -> None)
 
     | _ -> assert false
 end