diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 109 |
1 files changed, 55 insertions, 54 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d37090a6..7d480b8d 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) @@ -71,7 +71,7 @@ let coq_unit_judge = let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - Some (mkProj (Projection.make cst true, c)) + Some (mkProj (Projection.unfold p, c)) else None let eval_flexible_term ts env evd c = @@ -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 @@ -295,8 +292,8 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i'' -> ise_stack2 true i'' q1 q2 | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) - | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if Constant.equal (Projection.constant p1) (Projection.constant p2) + | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> + if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, @@ -337,8 +334,8 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) - | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if Constant.equal (Projection.constant p1) (Projection.constant p2) + | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> + if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> @@ -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 @@ -516,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -584,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty i,mkEvar ev else i,Stack.zip evd apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) tF tR else UnifFailure (evd,OccurCheck (fst ev,tR)))]) @@ -594,7 +588,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in + Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -990,10 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = + let open Declarations in let mib = lookup_mind (fst ind) env in - match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> - let pars = mib.Declarations.mind_nparams in + match get_projections env ind with + | Some projs when mib.mind_finite == BiFinite -> + let pars = mib.mind_nparams in (try let l1' = Stack.tail pars sk1 in let l2' = @@ -1045,7 +1040,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 +1080,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 +1130,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 +1157,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 +1179,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 +1201,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 +1215,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 = @@ -1232,8 +1225,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 - ++ cut () ++ print_constr t2 ++ cut ())) in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ + Termops.Internal.print_constr_env env evd t1 ++ cut () ++ + Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty @@ -1245,7 +1239,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 +1249,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 +1289,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 @@ -1324,9 +1318,10 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let rec aux = function | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> + (* In case of variables, most recent ones come first *) 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 @@ -1334,9 +1329,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = with | IllTypedInstance _ -> aux l | e when Pretype_errors.precatchable_exception e -> aux l in - (* List.rev is there to favor most dependent solutions *) - (* and favor progress when used with the refine tactics *) - let evd = aux (List.rev l) in + (* Expected invariant: most dependent solutions come first *) + (* so as to favor progress when used with the refine tactics *) + let evd = aux l in solve_unconstrained_evars_with_candidates ts evd let solve_unconstrained_impossible_cases env evd = @@ -1348,7 +1343,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 +1352,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 +1368,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 +1395,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 |