]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationMatcher.ml
packaging cleanup: get rid of ancient debhelpers, use dh_install
[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.ml
index 39c82b7dadb66a1e095969c133ff2d9ab23d5078..b9809335cf491d493c683dd81f69fe842398ac42 100644 (file)
@@ -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
@@ -193,7 +195,8 @@ struct
   struct
     type pattern_t = Pt.term
     type term_t = Pt.term
-    let classify = function
+    let rec classify = function
+      | Pt.AttributedTerm (_, t) -> classify t
       | Pt.Variable _ -> Variable
       | Pt.Magic _
       | Pt.Layout _
@@ -248,29 +251,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 +331,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
@@ -390,6 +375,7 @@ struct
 
     let mask_of_appl_pattern = function
       | Pt.UriPattern uri -> Uri uri, []
+      | Pt.ImplicitPattern
       | Pt.VarPattern _ -> Blob, []
       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 
@@ -401,8 +387,10 @@ struct
     type term_t = Cic.annterm
 
     let classify = function
+      | Pt.ImplicitPattern
       | Pt.VarPattern _ -> Variable
-      | _ -> Constructor
+      | Pt.UriPattern _
+      | Pt.ApplPattern _ -> Constructor
   end
 
   module M = Matcher (Pattern32)
@@ -415,6 +403,7 @@ struct
           List.map2
             (fun p t ->
               match p with
+              | Pt.ImplicitPattern -> Util.fresh_name (), t
               | Pt.VarPattern name -> name, t
               | _ -> assert false)
             pl matched_terms