Merge PR#594: An example showing the benefit of Econstr

4 files changed, 50 insertions, 32 deletions

diff --git a/lib/option.ml b/lib/option.ml
index fbb883d30..50fdd079d 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -20,24 +20,24 @@ let has_some = function
   | _ -> true
 
 let is_empty = function
-| None -> true
-| Some _ -> false
+  | None -> true
+  | Some _ -> false
 
 (** Lifting equality onto option types. *)
 let equal f x y = match x, y with
-| None, None -> true
-| Some x, Some y -> f x y
-| _, _ -> false
+  | None, None -> true
+  | Some x, Some y -> f x y
+  | _, _ -> false
 
 let compare f x y = match x, y with
-| None, None -> 0
-| Some x, Some y -> f x y
-| None, Some _ -> -1
-| Some _, None -> 1
+  | None, None -> 0
+  | Some x, Some y -> f x y
+  | None, Some _ -> -1
+  | Some _, None -> 1
 
 let hash f = function
-| None -> 0
-| Some x -> f x
+  | None -> 0
+  | Some x -> f x
 
 exception IsNone
 
@@ -57,13 +57,11 @@ let init b x =
   else
     None
 
-
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 let flatten = function
   | Some (Some y) -> Some y
   | _ -> None
 
-
 (** [append x y] is the first element of the concatenation of [x] and
     [y] seen as lists. *)
 let append o1 o2 =
@@ -134,6 +132,7 @@ let cata f a = function
   | Some c -> f c
   | None -> a
 
+
 (** {6 More Specific operations} ***)
 
 (** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
@@ -165,7 +164,6 @@ let lift2 f x y =
   | _,_ -> None
 
 
-
 (** {6 Operations with Lists} *)
 
 module List =
@@ -183,9 +181,19 @@ module List =
     | [] -> []
 
   let rec find f = function
-    |[] -> None
-    |h :: t -> match f h with
-	 |None -> find f t
-	 |x -> x
+    | [] -> None
+    | h :: t -> match f h with
+	 | None -> find f t
+	 | x -> x
+
+  let map f l =
+    let rec aux f l = match l with
+    | [] -> []
+    | x :: l ->
+      match f x with
+      | None -> raise Exit
+      | Some y -> y :: aux f l
+    in
+    try Some (aux f l) with Exit -> None
 
 end
diff --git a/lib/option.mli b/lib/option.mli
index 5e085620e..f06ad9f1d 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -122,5 +122,14 @@ module List : sig
       [Some y] (in the same order). *)
   val flatten : 'a option list -> 'a list
 
+  (** [List.find f l] is the first [f a] different from [None],
+      scrolling through elements [a] of [l] in left-to-right order;
+      it is [None] if no such element exists. *)
   val find : ('a -> 'b option) -> 'a list -> 'b option
+
+  (** [List.map f [a1;...;an]] is the list [Some [b1;...;bn]] if
+      for all i, there is a [bi] such that [f ai] is [Some bi]; it is
+      [None] if, for at least one i, [f ai] is [None]. *)
+  val map : ('a -> 'b option) -> 'a list -> 'b list option
+
 end
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0d011477..4ada91eb5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -470,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let map_all f l =
-  let rec map_aux f l = match l with
-  | [] -> []
-  | x :: l ->
-    match f x with
-    | None -> raise Exit
-    | Some y -> y :: map_aux f l
-  in
-  try Some (map_aux f l) with Exit -> None
-
 let expand_and_check_vars sigma aliases l =
   let map a = match get_alias_chain_of sigma aliases a with
   | None, [] -> Some a
   | None, a :: _ -> Some a
   | Some _, _ -> None
   in
-  map_all map l
+  Option.List.map map l
 
 let alias_distinct l =
   let rec check (rels, vars) = function
@@ -540,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t =
   | Rel n -> if n <= nb then Some (RelAlias n) else None
   | _ -> None
   in
-  match map_all map l with
+  match Option.List.map map l with
   | Some l ->
     begin match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (mkMeta m) t) -> x
@@ -550,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  match map_all (fun c -> to_alias evd c) l with
+  match Option.List.map (fun c -> to_alias evd c) l with
   | Some l when noccur_evar env evd evk t ->
     let args = remove_instance_local_defs evd evk args in
-    let args = map_all (fun c -> to_alias evd c) args in
+    let args = Option.List.map (fun c -> to_alias evd c) args in
     begin match args with
     | None -> None
     | Some args ->
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 296686e16..6f7498d65 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -188,3 +188,14 @@ Proof.
   apply idpath.
   apply idpath.
 Defined.
+
+(* An example where it is necessary to evar-normalize the instance of
+   an evar to evaluate if it is a pattern *)
+
+Check
+  let a := ?[P] in
+  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
+      x (p:x=0) =>
+    H ?[y] a p : x = 0.
+(* We have to solve "?P ?y[x] == x = 0" knowing from
+   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)