aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/subtac/subtac_coercion.ml2
-rw-r--r--pretyping/evarutil.ml102
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--test-suite/success/evars.v4
4 files changed, 80 insertions, 30 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index a09fa3dcc..5a2d84057 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -202,7 +202,7 @@ module Coercion = struct
| Lambda (n, t, t') -> c, t'
(*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
- let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+ let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
isevars := evs;
let (n, dom, rng) = destLambda t in
let (domk, args) = destEvar dom in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0da6c39be..0f71e47fb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1479,35 +1479,81 @@ let empty_valcon = None
(* Builds a value constraint *)
let mk_valcon c = Some c
-(* Refining an evar to a product or a sort *)
+(* Refining an evar to a product
-(* Declaring any type to be in the sort Type shouldn't be harmful since
- cumulativity now includes Prop and Set in Type...
- It is, but that's not too bad *)
-let define_evar_as_abstraction abs evd (ev,args) =
- let evi = Evd.find_undefined evd ev in
+ I.e., solve x1..xq |- ?e:T(x1..xq) with e:=Πy:?dom[x1..xq].?rng[x1..xq,y]
+ where x1..xq |- ?dom:Type and x1..xq,y |- ?rng:Type
+
+ Note: Declaring any type to be in the sort Type shouldn't be harmful
+ since cumulativity now includes Prop and Set in Type...
+ It is, but that's not too bad
+
+ To do: should we check that T is Type and instantiate it by a sort
+ if an evar?
+*)
+
+let idx = id_of_string "x"
+
+let define_pure_evar_as_product evd evk =
+ let evi = Evd.find_undefined evd evk in
+ let evenv = evar_unfiltered_env evi in
+ let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
+ let evd1,dom = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
+ let evd2,rng =
+ let newenv = push_named (id, None, dom) evenv in
+ let src = evar_source evk evd1 in
+ let filter = true::evar_filter evi in
+ new_evar evd1 newenv ~src (new_Type()) ~filter in
+ let prod = mkProd (Name id, dom, subst_var id rng) in
+ let evd3 = Evd.define evk prod evd2 in
+ evd3,prod
+
+(* Refine an applied evar to a product and returns its instantiation *)
+
+let define_evar_as_product evd (evk,args) =
+ let evd,prod = define_pure_evar_as_product evd evk in
+ (* Quick way to compute the instantiation of evk with args *)
+ let na,dom,rng = destProd prod in
+ let evdom = mkEvar (fst (destEvar dom), args) in
+ let evrngargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+ let evrng = mkEvar (fst (destEvar rng), evrngargs) in
+ evd,mkProd (na, evdom, evrng)
+
+(* Refine an evar with an abstraction
+
+ I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where:
+ - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y)
+ or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B
+ with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type
+ - x1..xq,y:A |- ?e':B
+*)
+
+let define_pure_evar_as_lambda env evd evk =
+ let evi = Evd.find_undefined evd evk in
let evenv = evar_unfiltered_env evi in
- let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
- let nvar =
- next_ident_away (id_of_string "x")
- (ids_of_named_context (evar_context evi)) in
- let newenv = push_named (nvar, None, dom) evenv in
- let (evd2,rng) =
- new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type())
- ~filter:(true::evar_filter evi) in
- let prod = abs (Name nvar, dom, subst_var nvar rng) in
- let evd3 = Evd.define ev prod evd2 in
- let evdom = fst (destEvar dom), args in
- let evrng =
- fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
- let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
- (evd3,prod')
-
-let define_evar_as_product evd (ev,args) =
- define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
-
-let define_evar_as_lambda evd (ev,args) =
- define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args)
+ let typ = whd_betadeltaiota env evd (evar_concl evi) in
+ let evd1,(na,dom,rng) = match kind_of_term typ with
+ | Prod (na,dom,rng) -> (evd,(na,dom,rng))
+ | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
+ | _ -> error_not_product_loc dummy_loc env evd typ in
+ let avoid = ids_of_named_context (evar_context evi) in
+ let id = next_name_away_with_default "x" na avoid in
+ let newenv = push_named (id, None, dom) evenv in
+ let filter = true::evar_filter evi in
+ let src = evar_source evk evd1 in
+ let evd2,body = new_evar evd1 newenv ~src rng ~filter in
+ let lam = mkLambda (Name id, dom, subst_var id body) in
+ Evd.define evk lam evd2, lam
+
+let define_evar_as_lambda env evd (evk,args) =
+ let evd,lam = define_pure_evar_as_lambda env evd evk in
+ (* Quick way to compute the instantiation of evk with args *)
+ let na,dom,body = destLambda lam in
+ let evbodyargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+ let evbody = mkEvar (fst (destEvar body), evbodyargs) in
+ evd,mkLambda (na, dom, evbody)
+
+(* Refining an evar to a sort *)
let define_evar_as_sort evd (ev,args) =
let s = new_Type () in
@@ -1537,7 +1583,7 @@ let split_tycon loc env evd tycon =
let (_,dom,rng) = destProd prod in
evd',(Anonymous, dom, rng)
| App (c,args) when isEvar c ->
- let (evd',lam) = define_evar_as_lambda evd (destEvar c) in
+ let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
real_split evd' (mkApp (lam,args))
| _ -> error_not_product_loc loc env evd c
in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 38da53683..a4c07a019 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -87,7 +87,7 @@ val solve_simple_eqn :
val check_evars : env -> evar_map -> evar_map -> constr -> unit
val define_evar_as_product : evar_map -> existential -> evar_map * types
-val define_evar_as_lambda : evar_map -> existential -> evar_map * types
+val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
val is_unification_pattern_evar : env -> existential -> constr list ->
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 69f7164c7..52c4f2daa 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -254,3 +254,7 @@ Proof.
(* error message with V8.3 :
Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *)
Abort.
+
+(* Regression test *)
+
+Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.