X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=b9809335cf491d493c683dd81f69fe842398ac42;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=1a0c024104feaaab9f730ed16c5101c3f72ce965;hpb=fa143d13b855aa48a11f3230a139f39ce2df0984;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 1a0c02410..b9809335c 100644
--- 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
@@ -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,36 +251,30 @@ 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
 		let env' = Env.remove_names env (List.map fst magic_map) in
 		Some (env', pid)))
         (fun _ -> None)
-        candidates
+        (List.rev candidates)
     in
     let match_cb rows =
       let candidates =
@@ -334,23 +331,21 @@ struct
           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
           | _ -> assert false)
 
-    | Pt.If (guard, p) ->
-	prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ;
-	prerr_endline ("p = " ^ CicNotationPp.pp_term 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 ->
-	     prerr_endline "GUARDIA?" ;
-	     match compiled_guard term with
-	       | None -> None
-	       | Some _ ->
-		   begin
-		     match compiled_p term with
-		       | None -> None
-		       | Some (env', _) ->
-			   prerr_endline "guardia ok" ;
-			   Some (env' @ env)
-		   end)
+	     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
@@ -380,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
 
@@ -391,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)
@@ -405,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