diff options
| -rw-r--r-- | pretyping/evarconv.ml | 28 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 28 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | test-suite/csdp.cache | bin | 795146 -> 748 bytes | |||
| -rw-r--r-- | test-suite/failure/evar1.v | 3 |
6 files changed, 50 insertions, 13 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bc4222175..f197f7a9a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c = | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) | _ -> c +let position_problem l2r = function + | CONV -> None + | CUMUL -> Some l2r + (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem (t1 l1) = (t2 l2) into a problem @@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 = let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,destEvar term1,term2) else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,destEvar term2,term1) else evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) @@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev2,applist(term1,deb1))); + (position_problem false pbty,ev2,applist(term1,deb1))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2)] else let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev1,applist(term2,deb2))); + (position_problem true pbty,ev1,applist(term2,deb2))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2)] and f2 i = @@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar evd (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else if List.length l1 <= List.length l2 then @@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar evd (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else if List.length l2 <= List.length l1 then @@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar evd (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar evd (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -505,7 +515,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) = if is_defined_evar i ev1 then evar_conv_x env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))] + solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find evd evk in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index bc23fcec2..cd2dc5d20 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1131,6 +1131,22 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in Evd.add_conv_pb pb evd +(* Util *) + +let check_instance_type conv_algo env evd ev1 t2 = + let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in + let typ1 = existential_type evd ev1 in + match kind_of_term (whd_evar evd typ2) with + | Evar _ -> + (* No firm constraints: don't want to commit to an equal + solution while only subtyping is requested *) + evd + | _ -> + let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in + if b then evd else + user_err_loc (fst (evar_source (fst ev1) evd),"", + str "Unable to find a well-typed instantiation") + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1145,10 +1161,18 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) if evk1 = evk2 then solve_refl conv_algo env evd evk1 args1 args2 else - if pbty = Reduction.CONV + if pbty = None then solve_evar_evar evar_define env evd ev1 ev2 - else add_conv_pb (pbty,env,mkEvar ev1,t2) evd + else if pbty = Some true then + add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd + else + add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd | _ -> + let evd = + if pbty = Some false then + check_instance_type conv_algo env evd ev1 t2 + else + evd in let evd = evar_define ~choose env ev1 t2 evd in let evi = Evd.find evd evk1 in if occur_existential evd evi.evar_concl then diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d35616ae2..8df301c66 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -80,7 +80,7 @@ val solve_refl : evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr -> + -> ?choose:bool -> env -> evar_defs -> bool option * existential * constr -> evar_defs * bool (* [check_evars env initial_sigma extended_sigma c] fails if some diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d48c002e2..92c176593 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -600,7 +600,7 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn env evd ev rhs = - let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in if not b then error_cannot_unify env evd (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache Binary files differindex 0a971d56c..f6f068c04 100644 --- a/test-suite/csdp.cache +++ b/test-suite/csdp.cache diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v new file mode 100644 index 000000000..1a4e42a89 --- /dev/null +++ b/test-suite/failure/evar1.v @@ -0,0 +1,3 @@ +(* This used to succeed by producing an ill-typed term in v8.2 *) + +Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A). |