X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2astMatcher.ml;h=2062b6c0651800235dd089d326e71b966f762b8e;hb=cd415135f0bcf53f10ed7649fcacc3247bc7a3f1;hp=d62786cc7a77316e65d11d4c8a6709bc31a42882;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/acic_content/acic2astMatcher.ml b/helm/software/components/acic_content/acic2astMatcher.ml
index d62786cc7..2062b6c06 100644
--- a/helm/software/components/acic_content/acic2astMatcher.ml
+++ b/helm/software/components/acic_content/acic2astMatcher.ml
@@ -35,6 +35,7 @@ struct
     type cic_mask_t =
       Blob
     | Uri of UriManager.uri
+    | NRef of NReference.reference
     | Appl of cic_mask_t list
 
     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
@@ -52,6 +53,7 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
+      | Ast.NRefPattern nref -> NRef nref, []
       | Ast.UriPattern uri -> Uri uri, []
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> Blob, []
@@ -71,15 +73,16 @@ struct
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> PatternMatcher.Variable
       | Ast.UriPattern _
+      | Ast.NRefPattern _
       | Ast.ApplPattern _ -> PatternMatcher.Constructor
   end
 
   module M = PatternMatcher.Matcher (Pattern32)
 
   let compiler rows =
-    let match_cb rows =
-      let pl, pid = try List.hd rows with Not_found -> assert false in
-      (fun matched_terms constructors ->
+    let match_cb rows matched_terms constructors =
+     HExtlib.list_findopt
+      (fun (pl,pid) _ ->
         let env =
           try
             List.map2
@@ -89,9 +92,23 @@ struct
                 | Ast.VarPattern name -> name, t
                 | _ -> assert false)
               pl matched_terms
-          with Invalid_argument _ -> assert false
+          with Invalid_argument _ -> assert false in
+        let rec check_non_linear_patterns =
+         function
+            [] -> true
+          | (name,t)::tl ->
+             List.for_all
+              (fun (name',t') ->
+                name <> name' ||
+                CicUtil.alpha_equivalence
+                 (Deannotate.deannotate_term t) (Deannotate.deannotate_term t')
+              ) tl && check_non_linear_patterns tl
         in
-        Some (env, constructors, pid))
+         if check_non_linear_patterns env then
+          Some (env, constructors, pid)
+         else
+          None
+      ) rows
     in
     M.compiler rows match_cb (fun () -> None)
 end