bugfix in default magic handling: consider as having option type only names

which appear in the some branch and in the none one (previously all names
appearing in the some branch where considered optional)

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 3ef1ff7e0deada79265cf44c8d6628b231facd5b..bf4b3e38e7beb17623542f91ed2ec1b2260696c6 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -35,8 +35,7 @@ let unopt_names names env =
         | Env.OptType ty, Env.OptValue (Some v) ->
             aux ((name, (ty, v)) :: acc) tl
         | _ -> assert false)
-    | _ :: tl -> aux acc tl
-      (* some pattern may contain only meta names, thus we trash all others *)
+    | hd :: tl -> aux (hd :: acc) tl
     | [] -> acc
   in
   aux [] env
@@ -77,6 +76,7 @@ let instantiate_level2 env term =
       new_name
   in
   let rec aux env term =
+(*     prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
     match term with
     | Ast.AttributedTerm (_, term) -> aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
@@ -129,7 +129,14 @@ let instantiate_level2 env term =
     | Ast.Ascription (term, name) -> assert false
   and aux_magic env = function
     | Ast.Default (some_pattern, none_pattern) ->
-        (match CicNotationUtil.names_of_term some_pattern with
+        let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
+        let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
+        let opt_names =
+          List.filter
+            (fun name -> not (List.mem name none_pattern_names))
+            some_pattern_names
+        in
+        (match opt_names with
         | [] -> assert false (* some pattern must contain at least 1 name *)
         | (name :: _) as names ->
             (match Env.lookup_value env name with
@@ -139,7 +146,11 @@ let instantiate_level2 env term =
                  *)
                 aux (unopt_names names env) some_pattern
             | Env.OptValue None -> aux env none_pattern
-            | _ -> assert false))
+            | _ ->
+                prerr_endline (sprintf
+                  "lookup of %s in env %s did not return an optional value"
+                  name (CicNotationPp.pp_env env));
+                assert false))
     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
         let meta_names =

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 8ac7dcdf50db0d888ddf72e5626d557eb24e8a9c..318361c447cbc787d8c1ad22b635b850ff81b37c 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -324,12 +324,27 @@ struct
 
     | Ast.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 p_none_decls = Env.declarations_of_term p_none in
+        let p_opt_decls =
+          List.filter
+            (fun decl -> not (List.mem decl p_none_decls))
+            p_some_decls
+        in
+        let none_env = List.map Env.opt_binding_of_name p_opt_decls in
         let compiled = compiler [p_some, 0] in
         (fun term env ->
           match compiled term with
           | None -> Some none_env (* LUCA: @ env ??? *)
-          | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+          | Some (env', 0) ->
+              let env' =
+                List.map
+                  (fun (name, (ty, v)) as binding ->
+                    if List.exists (fun (name', _) -> name = name') p_opt_decls
+                    then Env.opt_binding_some binding
+                    else binding)
+                  env'
+              in
+              Some (env' @ env)
           | _ -> assert false)
 
     | Ast.If (p_test, p_true, p_false) ->