Rename types_or_terms and the unification function types

4 files changed, 74 insertions, 42 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0e69dd43d5..8f7c88b0db 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -424,7 +424,10 @@ let conv_fun f flags on_types =
   in
   let termfn env evd pbty term1 term2 =
     f flags env evd pbty term1 term2
-  in if on_types then typefn else termfn
+  in
+    match on_types with
+    | TypeUnification -> typefn
+    | TermUnification -> termfn
 
 let rec evar_conv_x flags env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -735,7 +738,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
 	    |None, Success i' ->
               Success (solve_refl flags (fun p env i pbty a1 a2 ->
-                let flags = if p then default_flags env else flags in
+                let flags =
+                  match p with
+                  | TypeUnification -> default_flags env
+                  | TermUnification -> flags
+                in
                 is_success (evar_conv_x flags env i pbty a1 a2))
                 env i' (position_problem true pbty) sp1 al1 al2)
 	    |_, (UnifFailure _ as x) -> x
@@ -967,7 +974,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             |None, Success i' ->
               (** FIXME: solve_refl can restrict the evar, do we want to allow that? *)
               Success (solve_refl flags (fun p env i pbty a1 a2 ->
-                let flags = if p then default_flags env else flags in
+                let flags =
+                  match p with
+                  | TypeUnification -> default_flags env
+                  | TermUnification -> flags
+                in
                 is_success (evar_conv_x flags env i pbty a1 a2))
                 env i' (position_problem true pbty) sp1 al1 al2)
             |_, (UnifFailure _ as x) -> x
@@ -1544,8 +1555,12 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
          UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
      let f ontype env evd pbty x y =
-       let reds = if ontype then full_transparent_state else flags.open_ts in
-       is_fconv ~reds pbty env evd x y in
+       let reds =
+         match ontype with
+         | TypeUnification -> full_transparent_state
+         | TermUnification -> flags.open_ts
+       in is_fconv ~reds pbty env evd x y
+     in
       Success (solve_refl ~can_drop:true flags f env evd
                  (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 when app_empty ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index c2ad4e6678..bd55b952a6 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -24,7 +24,7 @@ val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> uni
 type unify_fun = unify_flags ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 
-val conv_fun : unify_fun -> unify_flags -> Evarsolve.conv_fun
+val conv_fun : unify_fun -> unify_flags -> Evarsolve.unifier
 
 exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aad21ad932..2ff52d1657 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -33,6 +33,34 @@ type unify_flags = {
   allow_K_at_toplevel : bool;
   with_cs : bool }
 
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(************************)
+(* Unification results  *)
+(************************)
+
+type unification_result =
+  | Success of evar_map
+  | UnifFailure of evar_map * unification_error
+
+let is_success = function Success _ -> true | UnifFailure _ -> false
+
+let test_success conv_algo b env evd c c' rhs =
+  is_success (conv_algo b env evd c c' rhs)
+
+(** A unification function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to unify. *)
+type unifier = unification_kind ->
+  env -> evar_map -> conv_pb -> constr -> constr -> unification_result
+
+(** A conversion function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to convert.
+    Conversion is not allowed to instantiate evars contrary to unification. *)
+type conversion_check = unification_kind ->
+  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -138,20 +166,6 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
     refresh_universes (Some false) env sigma ty
-		      
-
-(************************)
-(* Unification results  *)
-(************************)
-
-type unification_result =
-  | Success of evar_map
-  | UnifFailure of evar_map * unification_error
-
-let is_success = function Success _ -> true | UnifFailure _ -> false
-
-let test_success conv_algo b env evd c c' rhs =
-  is_success (conv_algo b env evd c c' rhs)
 
 let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
@@ -174,7 +188,7 @@ let recheck_applications conv_algo env evdref t =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
-            (match conv_algo true env !evdref Reduction.CUMUL argsty.(i) dom with
+            (match conv_algo TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
 			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
@@ -752,7 +766,7 @@ let check_evar_instance evd evk1 body conv_algo =
     try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
   in
-  match conv_algo true evenv evd Reduction.CUMUL ty evi.evar_concl with
+  match conv_algo TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
@@ -1135,7 +1149,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
 
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
-  match conv_algo false env evd Reduction.CONV rhs c' with
+  match conv_algo TermUnification env evd Reduction.CONV rhs c' with
   | Success evd -> Some (c,evd)
   | UnifFailure _ -> None
 
@@ -1331,14 +1345,6 @@ let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (e
       evd in
   solve_evar_evar_aux force flags f g env evd pbty ev1 ev2
 
-type types_or_terms = bool
-
-type conv_fun =
-  types_or_terms -> env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result
-
-type conv_fun_bool =
-  types_or_terms -> env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool
-
 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
  * definitions. We try to unify the ti with the ui pairwise. The pairs
  * that don't unify are discarded (i.e. ?e is redefined so that it does not
@@ -1357,7 +1363,7 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
     restrict_upon_filter evd evk
-      (fun (a1,a2) -> conv_algo false env evd Reduction.CONV a1 a2) args in
+      (fun (a1,a2) -> conv_algo TermUnification env evd Reduction.CONV a1 a2) args in
   let candidates = filter_candidates evd evk untypedfilter NoUpdate in
   let filter = closure_of_filter evd evk untypedfilter in
   let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
@@ -1696,7 +1702,7 @@ let reconsider_unif_constraints conv_algo evd =
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
        | Success evd ->
-           (match conv_algo true env evd pbty t1 t2 with
+           (match conv_algo TermUnification env evd pbty t1 t2 with
            | Success _ as x -> x
            | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
        | UnifFailure _ as x -> x)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 94f17de6cc..87804f01b6 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -40,15 +40,26 @@ val expand_vars_in_term : env -> evar_map -> constr -> constr
    some problems that cannot be solved in a unique way (except if choose is
    true); fails if the instance is not valid for the given [ev] *)
 
-type types_or_terms = bool
+(** One might want to use different conversion strategies for types and terms:
+    e.g. preventing delta reductions when doing term unifications but allowing
+    arbitrary delta conversion when checking the types of evar instances. *)
 
-type conv_fun = types_or_terms ->
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(** A unification function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to unify. *)
+type unifier = unification_kind ->
   env -> evar_map -> conv_pb -> constr -> constr -> unification_result
 
-type conv_fun_bool = types_or_terms ->
+(** A conversion function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to convert.
+    Conversion is not allowed to instantiate evars contrary to unification. *)
+type conversion_check = unification_kind ->
   env ->  evar_map -> conv_pb -> constr -> constr -> bool
 
-val evar_define : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool ->
+val evar_define : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool ->
   env -> evar_map -> bool option -> existential -> constr -> evar_map
 
 val refresh_universes :
@@ -60,18 +71,18 @@ val refresh_universes :
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-val solve_refl : ?can_drop:bool -> unify_flags -> conv_fun_bool -> env ->  evar_map ->
+val solve_refl : ?can_drop:bool -> unify_flags -> conversion_check -> env ->  evar_map ->
   bool option -> Evar.t -> constr array -> constr array -> evar_map
 
 val solve_evar_evar : ?force:bool -> unify_flags ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
-  conv_fun ->
+  unifier ->
   env ->  evar_map -> bool option -> existential -> existential -> evar_map
 
-val solve_simple_eqn : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
+val solve_simple_eqn : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
-val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+val reconsider_unif_constraints : unifier -> evar_map -> unification_result
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
@@ -87,7 +98,7 @@ exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
 val check_evar_instance :
-  evar_map -> Evar.t -> constr -> conv_fun -> evar_map
+  evar_map -> Evar.t -> constr -> unifier -> evar_map
 
 val remove_instance_local_defs :
   evar_map -> Evar.t -> 'a array -> 'a list