X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=46469e769928bc0029fbb52f7db98a9cf1171012;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=f8f73e66bf9cba5dd2aadabb71feed686dcdcd91;hpb=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index f8f73e66b..46469e769 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -187,7 +187,9 @@ struct
       | Pt.Variable _ -> Variable
       | Pt.Magic _
       | Pt.Layout _
-      | Pt.Literal _ -> assert false
+      | Pt.Literal _ as t ->
+          prerr_endline (CicNotationPp.pp_term t);
+          assert false
       | _ -> Constructor
     let tag_of_pattern = CicNotationTag.get_tag
     let tag_of_term = CicNotationTag.get_tag
@@ -226,9 +228,6 @@ struct
         | _ -> assert false)
       pl tl
 
-  let decls_of_pattern p = 
-    List.map Env.declaration_of_var (Util.variables_of_term p)
-
   let rec compiler rows =
     let rows', magic_maps =
       List.split
@@ -273,14 +272,13 @@ struct
       in
       magichooser candidates
     in
-    M.compiler rows match_cb (fun _ -> None)
+    M.compiler rows' match_cb (fun _ -> None)
 
   and compile_magic = function
     | Pt.Fold (kind, p_base, names, p_rec) ->
-        let p_rec_decls = decls_of_pattern p_rec in
+        let p_rec_decls = Env.declarations_of_term p_rec in
         let acc_name = try List.hd names with Failure _ -> assert false in
-        let t_magic = [p_base, 0; p_rec, 1] in
-        let compiled = compiler t_magic in
+        let compiled = compiler [p_base, 0; p_rec, 1] in
         (fun term env ->
           let rec aux term =
             match compiled term with
@@ -301,6 +299,15 @@ struct
             | None -> None
             | Some (base_env, rec_envl) ->
                 Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
+    | Pt.Default (p_some, p_none) ->  (* p_none can't bound names *)
+        let p_some_decls = Env.declarations_of_term p_some in
+        let none_env = List.map Env.opt_binding_of_name p_some_decls in
+        let compiled = compiler [p_some, 0] in
+        (fun term env ->
+          match compiled term with
+          | None -> Some none_env
+          | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+          | _ -> assert false)
     | _ -> assert false
 end
 
@@ -310,7 +317,7 @@ struct
   struct
     type cic_mask_t =
       Blob
-    | Uri of string
+    | Uri of UriManager.uri
     | Appl of cic_mask_t list
 
     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
@@ -328,7 +335,7 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Pt.UriPattern s -> Uri s, []
+      | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), []
       | Pt.VarPattern _ -> Blob, []
       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl