diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenvtac.ml | 3 | ||||
-rw-r--r-- | proofs/logic.ml | 41 | ||||
-rw-r--r-- | proofs/logic.mli | 6 | ||||
-rw-r--r-- | proofs/pfedit.ml | 3 | ||||
-rw-r--r-- | proofs/pfedit.mli | 4 | ||||
-rw-r--r-- | proofs/proof_global.ml | 20 | ||||
-rw-r--r-- | proofs/proof_global.mli | 5 | ||||
-rw-r--r-- | proofs/refiner.ml | 4 | ||||
-rw-r--r-- | proofs/refiner.mli | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 11 | ||||
-rw-r--r-- | proofs/tacmach.mli | 8 |
11 files changed, 46 insertions, 61 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4a92c3856..8bd5d98cb 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then raise - (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs (** Use our own fast path, more informative than from Typeclasses *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a9ad606a0..1d86a0909 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,7 +40,7 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * Evd.evar_map * refiner_error open Pretype_errors @@ -69,7 +69,7 @@ let catchable_exception = function | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) +let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -78,10 +78,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp check sign id f = +let apply_to_hyp env sigma check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if check then error_no_such_hypothesis id + if check then error_no_such_hypothesis env sigma id else sign let check_typability env sigma c = @@ -147,7 +147,7 @@ let reorder_context env sigma sign ord = step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with - | [] -> error_no_such_hypothesis (List.hd ord) + | [] -> error_no_such_hypothesis env sigma (List.hd ord) | d :: ctxt -> let x = NamedDecl.get_id d in if Id.Set.mem x expected then @@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let split_sign hfrom hto l = +let split_sign env sigma hfrom hto l = let rec splitrec left toleft = function - | [] -> error_no_such_hypothesis hfrom + | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then @@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then - error_no_such_hypothesis (hyp_of_move_location hto); + error_no_such_hypothesis env sigma (hyp_of_move_location hto); List.rev first @ List.rev middle | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right @@ -258,10 +258,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context sigma hfrom hto sign = +let move_hyp_in_named_context env sigma hfrom hto sign = let open EConstr in let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in + split_sign env sigma hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto let insert_decl_in_named_context sigma decl hto sign = @@ -293,15 +293,15 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then - raise (RefinerError (NonLinearProof c)) + raise (RefinerError (env, sigma, NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = if !check then let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm - else raise (RefinerError (BadType (arg,ty,conclty))) + else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then - raise (RefinerError (MetaInType conclty)); + raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in let conclty = EConstr.Unsafe.to_constr conclty in @@ -477,7 +477,9 @@ and mk_arggoals sigma goal goalacc funty allargs = | Prod (_, c1, b) -> let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in (acc, subst1 harg b, sigma), arg - | _ -> raise (RefinerError (CannotApply (t, harg))) + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs @@ -497,10 +499,10 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env() in + let env = Global.env () in let reorder = ref [] in let sign' = - apply_to_hyp check sign id + apply_to_hyp env sigma check sign id (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in @@ -514,19 +516,18 @@ let convert_hyp check sign sigma d = map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder - - (************************************************************************) (************************************************************************) (* Primitive tactics are handled here *) let prim_refiner r sigma goal = + let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in match r with (* Logical rules *) | Refine c -> let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables c; + check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in diff --git a/proofs/logic.mli b/proofs/logic.mli index 7df7fd66b..afd1ecf70 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -50,16 +50,16 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * evar_map * refiner_error -val error_no_such_hypothesis : Id.t -> 'a +val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c526ae000..6b503a011 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,7 +140,8 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); - const, status, fst univs + let univs = UState.demote_seff_univs const univs in + const, status, univs with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 2acb678d7..5a317a956 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -35,11 +35,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) val cook_proof : unit -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) (** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c1e1c2eda..167d6bda0 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,17 +68,16 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -350,13 +348,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in - (* Universes for private constants are relevant to the body *) - let used_univs_body = - List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) - used_univs_body (Safe_typing.universes_of_private eff) - in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in @@ -364,7 +358,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) @@ -409,7 +403,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 059459042..27e99f218 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -37,18 +37,17 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3e3313eb5..cd2b10906 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -30,8 +30,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34e517aed..52dc8bfd8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.constraints -> tactic +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca..d41541251 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = + let env, sigma = pf_env gls, project gls in try Context.Named.lookup id (pf_hyps gls) with Not_found -> - raise (RefinerError (NoSuchHyp id)) + raise (RefinerError (env, sigma, NoSuchHyp id)) let pf_get_hyp_typ gls id = id |> pf_get_hyp gls |> NamedDecl.get_type @@ -102,9 +103,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -185,9 +183,10 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in + let sigma = project gl in let sign = try EConstr.lookup_named id hyps - with Not_found -> raise (RefinerError (NoSuchHyp id)) + with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id)) in sign @@ -223,8 +222,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4..e0fb8fbc5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end |