aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml74
1 files changed, 36 insertions, 38 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d37090a65..6d08f66c1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option {
(* XXX: we would like to search for this with late binding
"data.id.type" etc... *)
let impossible_default_case () =
- let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+ let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
let (_, u) = Constr.destConst c in
Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
@@ -114,9 +114,6 @@ let flex_kind_of_term ts env evd c sk =
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
| Cast _ | App _ | Case _ -> assert false
-let add_conv_pb (pb, env, x, y) sigma =
- Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma
-
let apprec_nohdbeta ts env evd c =
let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
if Stack.not_purely_applicative sk
@@ -213,7 +210,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
else match (Stack.strip_n_app (l_us-1) sk2_effective) with
| None -> raise Not_found
| Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
- let u, ctx' = Universes.fresh_instance_from ctx None in
+ let u, ctx' = UnivGen.fresh_instance_from ctx None in
let subst = Univ.make_inverse_instance_subst u in
let c = EConstr.of_constr c in
let c' = subst_univs_level_constr subst c in
@@ -369,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
let ground_test =
if is_ground_term evd term1 && is_ground_term evd term2 then (
let e =
- try
- let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
- env evd term1 term2
- in
- if b then Success evd
- else UnifFailure (evd, ConversionFailed (env,term1,term2))
- with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+ match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+ | Some evd -> Success evd
+ | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
+ | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
in
match e with
| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
@@ -1045,7 +1039,7 @@ let choose_less_dependent_instance evk evd term args =
let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in
match subst' with
| [] -> None
- | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
+ | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
let apply_on_subterm env evdref f c t =
let rec applyrec (env,(k,c) as acc) t =
@@ -1085,7 +1079,7 @@ let filter_possible_projections evd c ty ctxt args =
let a = Array.unsafe_get args i in
(match decl with
| NamedDecl.LocalAssum _ -> false
- | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) ||
+ | NamedDecl.LocalDef (_,c,_) -> not (isRel evd c || isVar evd c)) ||
a == c ||
(* Here we make an approximation, for instance, we could also be *)
(* interested in finding a term u convertible to c such that a occurs *)
@@ -1135,7 +1129,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
end
| decl'::ctxt', c::l, occs::occsl ->
let id = NamedDecl.get_id decl' in
- let t = EConstr.of_constr (NamedDecl.get_type decl') in
+ let t = NamedDecl.get_type decl' in
let evs = ref [] in
let ty = Retyping.get_type_of env_rhs evd c in
let filter' = filter_possible_projections evd c ty ctxt args in
@@ -1162,17 +1156,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let subst = make_subst (ctxt,Array.to_list args,argoccs) in
- let evdref = ref evd in
- let rhs = set_holes evdref rhs subst in
- let evd = !evdref in
+ let evd, rhs =
+ let evdref = ref evd in
+ let rhs = set_holes evdref rhs subst in
+ !evdref, rhs
+ in
(* We instantiate the evars of which the value is forced by typing *)
let evd,rhs =
- let evdref = ref evd in
- try let c = !solve_evars env_evar evdref rhs in !evdref,c
+ try !solve_evars env_evar evd rhs
with e when Pretype_errors.precatchable_exception e ->
(* Could not revert all subterms *)
- raise (TypingFailed !evdref) in
+ raise (TypingFailed evd) in
let rec abstract_free_holes evd = function
| (id,idty,c,_,evsref,_,_)::l ->
@@ -1183,7 +1178,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* We force abstraction over this unconstrained occurrence *)
(* and we use typing to propagate this instantiation *)
(* This is an arbitrary choice *)
- let evd = Evd.define evk (Constr.mkVar id) evd in
+ let evd = Evd.define evk (mkVar id) evd in
match evar_conv_x ts env_evar evd CUMUL idty evty with
| UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
@@ -1205,14 +1200,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(evar_conv_x full_transparent_state)
with IllTypedInstance _ -> raise (TypingFailed evd)
in
- Evd.define evk (EConstr.Unsafe.to_constr rhs) evd
+ Evd.define evk rhs evd
in
abstract_free_holes evd subst, true
with TypingFailed evd -> evd, false
-let to_pb (pb, env, t1, t2) =
- (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
-
let second_order_matching_with_args ts env evd pbty ev l t =
(*
let evd,ev = evar_absorb_arguments env evd ev l in
@@ -1222,7 +1214,7 @@ let second_order_matching_with_args ts env evd pbty ev l t =
else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
if b then Success evd else
*)
- let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in
+ let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
@@ -1245,7 +1237,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
&& List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
(remove_instance_local_defs evd evk2 args2) ->
@@ -1255,7 +1247,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
Success (solve_refl ~can_drop:true f env evd
@@ -1295,10 +1287,10 @@ let error_cannot_unify env evd pb ?reason t1 t2 =
let check_problems_are_solved env evd =
match snd (extract_all_conv_pbs evd) with
- | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2)
+ | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
| _ -> ()
-exception MaxUndefined of (Evar.t * evar_info * Constr.t list)
+exception MaxUndefined of (Evar.t * evar_info * EConstr.t list)
let max_undefined_with_candidates evd =
let fold evk evi () = match evi.evar_candidates with
@@ -1326,7 +1318,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
| a::l ->
try
let conv_algo = evar_conv_x ts in
- let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
+ let evd = check_evar_instance evd evk a conv_algo in
let evd = Evd.define evk a evd in
match reconsider_unif_constraints conv_algo evd with
| Success evd -> solve_unconstrained_evars_with_candidates ts evd
@@ -1348,7 +1340,7 @@ let solve_unconstrained_impossible_cases env evd =
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
let evd' = check_evar_instance evd' evk ty conv_algo in
- Evd.define evk (EConstr.Unsafe.to_constr ty) evd'
+ Evd.define evk ty evd'
| _ -> evd') evd evd
let solve_unif_constraints_with_heuristics env
@@ -1357,8 +1349,6 @@ let solve_unif_constraints_with_heuristics env
let rec aux evd pbs progress stuck =
match pbs with
| (pbty,env,t1,t2 as pb) :: pbs ->
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
(match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
| Success evd' ->
let (evd', rest) = extract_all_conv_pbs evd' in
@@ -1375,9 +1365,7 @@ let solve_unif_constraints_with_heuristics env
match stuck with
| [] -> (* We're finished *) evd
| (pbty,env,t1,t2 as pb) :: _ ->
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
- (* There remains stuck problems *)
+ (* There remains stuck problems *)
error_cannot_unify env evd pb t1 t2
in
let (evd,pbs) = extract_all_conv_pbs evd in
@@ -1404,6 +1392,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
| Success evd' -> evd'
| UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
+let make_opt = function
+ | Success evd -> Some evd
+ | UnifFailure _ -> None
+
+let conv env ?(ts=default_transparent_state env) evd t1 t2 =
+ make_opt(evar_conv_x ts env evd CONV t1 t2)
+
+let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
+ make_opt(evar_conv_x ts env evd CUMUL t1 t2)
+
let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
match evar_conv_x ts env !evdref CONV t1 t2 with
| Success evd' -> evdref := evd'; true
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 22:08:02 +0000