From 7446e3e1555c0f41373b71b92a3f01f060e8e0e0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Jun 2017 15:51:47 +0200 Subject: Exporting general-purpose functions on goal contexts from "logic.ml" to "tactics.ml". This is in preparation of move of "assert" from old to new proof engine. --- proofs/logic.ml | 4 ++++ proofs/logic.mli | 6 ++++++ 2 files changed, 10 insertions(+) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 6af1b2d837..0621af4e80 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -282,6 +282,10 @@ let move_hyp_in_named_context sigma hfrom hto sign = split_sign 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 = + let open EConstr in + move_hyp sigma false ([],decl,named_context_of_val sign) hto + (**********************************************************************) diff --git a/proofs/logic.mli b/proofs/logic.mli index f98248e4d1..8dd29bc174 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -52,6 +52,8 @@ type refiner_error = exception RefinerError of refiner_error +val error_no_such_hypothesis : Id.t -> 'a + val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> @@ -59,3 +61,7 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map -> val move_hyp_in_named_context : 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 -> + EConstr.named_declaration -> Id.t Misctypes.move_location -> + Environ.named_context_val -> Environ.named_context_val -- cgit v1.2.3 From 9e1372f77218ca6f0baf4ed7c590c91ad84b6313 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Jun 2017 16:24:30 +0200 Subject: Moving "assert" (internally "Cut") to the new proof engine. It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "". --- proofs/logic.ml | 46 ---------------------------------------------- proofs/proof_type.mli | 2 -- proofs/tacmach.ml | 10 ---------- proofs/tacmach.mli | 3 --- 4 files changed, 61 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 0621af4e80..db9e847c06 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -22,7 +22,6 @@ open Proof_type open Type_errors open Retyping open Misctypes -open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -93,15 +92,6 @@ let check_typability env sigma c = (* Implementation of the structural rules (moving and deleting hypotheses around) *) -(* The Clear tactic: it scans the context for hypotheses to be removed - (instead of iterating on the list of identifier to be removed, which - forces the user to give them in order). *) - -let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - (* The ClearBody tactic *) (* Reordering of the context *) @@ -200,14 +190,6 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let rec get_hyp_after h = function - | [] -> error_no_such_hypothesis h - | d :: right -> - if Id.equal (NamedDecl.get_id d) h then - match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst - else - get_hyp_after h right - let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom @@ -539,37 +521,9 @@ let convert_hyp check sign sigma d = (* Primitive tactics are handled here *) let prim_refiner r sigma goal = - let env = Goal.V82.env sigma goal in - let sign = Goal.V82.hyps sigma goal in let cl = Goal.V82.concl sigma goal in - let mk_goal hyps concl = - Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) - in - let open EConstr in match r with (* Logical rules *) - | Cut (b,replace,id,t) -> -(* if !check && not (Retyping.get_sort_of env sigma t) then*) - let t = EConstr.of_constr t in - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in - let sign,t,cl,sigma = - if replace then - let nexthyp = get_hyp_after id (named_context_of_val sign) in - let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) - nexthyp, - t,cl,sigma - else - (if !check && mem_named_context_val id sign then - user_err ~hdr:"Logic.prim_refiner" - (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in - let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in - let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in - if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | Refine c -> let cl = EConstr.Unsafe.to_constr cl in check_meta_variables c; diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e59db9e427..ec4af86b9c 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -9,14 +9,12 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Names open Term (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) type prim_rule = - | Cut of bool * bool * Id.t * types | Refine of constr (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index f9d9f25ccf..bdfa399aa4 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -115,22 +115,12 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c let refiner = refiner -let internal_cut_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (true,replace,id,t)) gl - -let internal_cut_rev_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (false,replace,id,t)) gl - let refine_no_check c gl = let c = EConstr.Unsafe.to_constr c in refiner (Refine c) gl (* Versions with consistency checks *) -let internal_cut b d t = with_check (internal_cut_no_check b d t) -let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3d2fa72c17..aac7b90ee4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -84,13 +84,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> types -> tactic -val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) -- cgit v1.2.3