From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- proofs/evar_refiner.ml | 23 +++--- proofs/logic.ml | 200 +++++++++++++++++++------------------------------ proofs/proof_type.ml | 20 ++++- proofs/proof_type.mli | 21 +++++- proofs/refiner.ml | 33 ++++---- proofs/tacexpr.ml | 50 ++++++++----- proofs/tacmach.ml | 24 +++--- proofs/tacmach.mli | 17 ++--- 8 files changed, 189 insertions(+), 199 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 99ab7ef1..d19d81e0 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 11047 2008-06-03 23:08:00Z msozeau $ *) +(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -22,25 +22,28 @@ open Refiner (* w_tactic pour instantiate *) -let w_refine ev rawc evd = - if Evd.is_defined (evars_of evd) ev then +let w_refine evk rawc evd = + if Evd.is_defined (evars_of evd) evk then error "Instantiate called on already-defined evar"; - let e_info = Evd.find (evars_of evd) ev in + let e_info = Evd.find (evars_of evd) evk in let env = Evd.evar_env e_info in - let sigma,typed_c = + let sigma,typed_c = try Pretyping.Default.understand_tcc ~resolve_classes:false (evars_of evd) env ~expected_type:e_info.evar_concl rawc - with _ -> error ("The term is not well-typed in the environment of " ^ - string_of_existential ev) + with _ -> + let loc = Rawterm.loc_of_rawconstr rawc in + user_err_loc + (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ + string_of_existential evk)) in - evar_define ev typed_c (evars_reset_evd sigma evd) + evar_define evk typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in let sigma = gls.sigma in - let (sp,evi) (* as evc *) = + let (evk,evi) = let evl = Evarutil.non_instantiated sigma in if (n <= 0) then error "incorrect existential variable index" @@ -52,5 +55,5 @@ let instantiate_pf_com n com pfts = let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in let evd = create_goal_evar_defs sigma in - let evd' = w_refine sp rawc evd in + let evd' = w_refine evk rawc evd in change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/logic.ml b/proofs/logic.ml index 6e78f134..21ee9a9f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 10877 2008-04-30 21:58:41Z herbelin $ *) +(* $Id: logic.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -27,6 +27,7 @@ open Typeops open Type_errors open Retyping open Evarutil +open Tacexpr type refiner_error = @@ -47,13 +48,15 @@ open Pretype_errors let rec catchable_exception = function | Stdpp.Exc_located(_,e) -> catchable_exception e + | LtacLocated(_,e) -> catchable_exception e | Util.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) (* unification errors *) | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ - |CannotFindWellTypedAbstraction _)) -> true + |CannotFindWellTypedAbstraction _ + |UnsolvableImplicit _)) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not @@ -70,11 +73,10 @@ let with_check = Flags.with_option check (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) -let clear_hyps sigma ids gl = +let clear_hyps sigma ids sign cl = let evdref = ref (Evd.create_goal_evar_defs sigma) in - let (hyps,concl) = - Evarutil.clear_hyps_in_evi evdref gl.evar_hyps gl.evar_concl ids in - (mk_goal hyps concl gl.evar_extra, evars_of !evdref) + let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in + (hyps,concl,evars_of !evdref) (* The ClearBody tactic *) @@ -83,13 +85,13 @@ let clear_hyps sigma ids gl = let apply_to_hyp sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error "No such assumption" + if !check then error "No such assumption." else sign let apply_to_hyp_and_dependent_on sign id f g = try apply_to_hyp_and_dependent_on sign id f g with Hyp_not_found -> - if !check then error "No such assumption" + if !check then error "No such assumption." else sign let check_typability env sigma c = @@ -109,7 +111,7 @@ let remove_hyp_body env sigma id = apply_to_hyp_and_dependent_on (named_context_val env) id (fun (_,c,t) _ -> match c with - | None -> error ((string_of_id id)^" is not a local definition") + | None -> error ((string_of_id id)^" is not a local definition.") | Some c ->(id,None,t)) (fun (id',c,t as d) sign -> (if !check then @@ -126,24 +128,42 @@ let remove_hyp_body env sigma id = (* Auxiliary functions for primitive MOVE tactic * - * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves - * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the + * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves + * hyp [hfrom] at location [hto] which belongs to the hyps on the * left side [left] of the full signature if [toleft=true] or to the hyps * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +let error_no_such_hypothesis id = + error ("No such hypothesis: " ^ string_of_id id ^ ".") + +let rec get_hyp_after h = function + | [] -> error_no_such_hypothesis h + | (hyp,_,_) :: right -> + if hyp = h then + match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false + else + get_hyp_after h right + let split_sign hfrom hto l = let rec splitrec left toleft = function - | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom)) + | [] -> error_no_such_hypothesis hfrom | (hyp,c,typ) as d :: right -> if hyp = hfrom then - (left,right,d,toleft) - else - splitrec (d::left) (toleft or (hyp = hto)) right + (left,right,d, toleft or hto = MoveToEnd true) + else + splitrec (d::left) + (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) + right in splitrec [] false l -let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = +let hyp_of_move_location = function + | MoveAfter id -> id + | MoveBefore id -> id + | _ -> assert false + +let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = let env = Global.env() in let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = if toleft @@ -151,23 +171,27 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = else occur_var_in_decl env hyp d2 in let rec moverec first middle = function - | [] -> error ("No such hypothesis : " ^ (string_of_id hto)) + | [] -> + if match hto with MoveToEnd _ -> false | _ -> true then + error_no_such_hypothesis (hyp_of_move_location hto); + List.rev first @ List.rev middle + | (hyp,_,_) :: _ as right when hto = MoveBefore hyp -> + List.rev first @ List.rev middle @ right | (hyp,_,_) as d :: right -> let (first',middle') = if List.exists (test_dep d) middle then - if with_dep & (hyp <> hto) then + if with_dep & hto <> MoveAfter hyp then (first, d::middle) else - error - ("Cannot move "^(string_of_id idfrom)^" after " - ^(string_of_id hto) - ^(if toleft then ": it occurs in " else ": it depends on ") - ^(string_of_id hyp)) - else + errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++ + pr_move_location pr_id hto ++ + str (if toleft then ": it occurs in " else ": it depends on ") + ++ pr_id hyp ++ str ".") + else (d::first, middle) in - if hyp = hto then - (List.rev first')@(List.rev middle')@right + if hto = MoveAfter hyp then + List.rev first' @ List.rev middle' @ right else moverec first' middle' right in @@ -183,53 +207,11 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let check_backward_dependencies sign d = - if not (Idset.for_all - (fun id -> mem_named_context id sign) - (global_vars_set_of_decl (Global.env()) d)) - then - error "Can't introduce at that location: free variable conflict" - - -let check_forward_dependencies id tail = - let env = Global.env() in - List.iter - (function (id',_,_ as decl) -> - if occur_var_in_decl env id decl then - error ((string_of_id id) ^ " is used in hypothesis " - ^ (string_of_id id'))) - tail - -let check_goal_dependency id cl = - let env = Global.env() in - if Idset.mem id (global_vars_set env cl) then - error (string_of_id id^" is used in conclusion") - let rename_hyp id1 id2 sign = apply_to_hyp_and_dependent_on sign id1 (fun (_,b,t) _ -> (id2,b,t)) (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) -let replace_hyp sign id d cl = - if !check then - check_goal_dependency id cl; - apply_to_hyp sign id - (fun sign _ tail -> - if !check then - (check_backward_dependencies sign d; - check_forward_dependencies id tail); - d) - -(* why we dont check that id does not appear in tail ??? *) -let insert_after_hyp sign id d = - try - insert_after_hyp sign id d - (fun sign -> - if !check then check_backward_dependencies sign d) - with Hyp_not_found -> - if !check then error "No such assumption" - else sign - (************************************************************************) (************************************************************************) (* Implementation of the logical rules *) @@ -375,19 +357,14 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty) -let error_use_instantiate () = - errorlabstrm "Logic.prim_refiner" - (str"cannot intro when there are open metavars in the domain type" ++ - spc () ++ str"- use Instantiate") - let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if !check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(string_of_id id)); + error ("Incorrect change of the type of "^(string_of_id id)^"."); if !check && not (Option.Misc.compare (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(string_of_id id)); + error ("Incorrect change of the body of "^(string_of_id id)^"."); d) (* Normalizing evars in a goal. Called by tactic Local_constraints @@ -420,12 +397,10 @@ let prim_refiner r sigma goal = error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> - if occur_meta c1 then error_use_instantiate(); let sg = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in ([sg], sigma) | LetIn (_,c1,t1,b) -> - if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let sg = mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in @@ -433,28 +408,19 @@ let prim_refiner r sigma goal = | _ -> raise (RefinerError IntroNeedsProduct)) - | Intro_replacing id -> - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,c1,b) -> - if occur_meta c1 then error_use_instantiate(); - let sign' = replace_hyp sign id (id,None,c1) cl in - let sg = mk_goal sign' (subst1 (mkVar id) b) in - ([sg], sigma) - | LetIn (_,c1,t1,b) -> - if occur_meta c1 then error_use_instantiate(); - let sign' = replace_hyp sign id (id,Some c1,t1) cl in - let sg = mk_goal sign' (subst1 (mkVar id) b) in - ([sg], sigma) - | _ -> - raise (RefinerError IntroNeedsProduct)) - - | Cut (b,id,t) -> - if !check && mem_named_context id (named_context_of_val sign) then - error "New variable is already declared"; - if occur_meta t then error_use_instantiate(); + | Cut (b,replace,id,t) -> let sg1 = mk_goal sign (nf_betaiota t) in - let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in - if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma) + let sign,cl,sigma = + if replace then + let nexthyp = get_hyp_after id (named_context_of_val sign) in + let sign,cl,sigma = clear_hyps sigma [id] sign cl in + move_hyp true false ([],(id,None,t),named_context_of_val sign) + nexthyp, + cl,sigma + else + (push_named_context_val (id,None,t) sign),cl,sigma in + let sg2 = mk_goal sign cl in + if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | FixRule (f,n,rest) -> let rec check_ind env k cl = @@ -464,10 +430,10 @@ let prim_refiner r sigma goal = try fst (find_inductive env sigma c1) with Not_found -> - error "cannot do a fixpoint on a non inductive type" + error "Cannot do a fixpoint on a non inductive type." else check_ind (push_rel (na,None,c1) env) (k-1) b - | _ -> error "not enough products" + | _ -> error "Not enough products." in let (sp,_) = check_ind env n cl in let all = (f,n,cl)::rest in @@ -475,10 +441,10 @@ let prim_refiner r sigma goal = | (f,n,ar)::oth -> let (sp',_) = check_ind env n ar in if not (sp=sp') then - error ("fixpoints should be on the same " ^ - "mutual inductive declaration"); + error ("Fixpoints should be on the same " ^ + "mutual inductive declaration."); if !check && mem_named_context f (named_context_of_val sign) then - error "name already used in the environment"; + error "Name already used in the environment"; mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all @@ -495,8 +461,7 @@ let prim_refiner r sigma goal = let _ = find_coinductive env sigma b in () with Not_found -> error ("All methods must construct elements " ^ - "in coinductiv-> goal -e types") + "in coinductive types.") in let all = (f,cl)::others in List.iter (fun (_,c) -> check_is_coind env c) all; @@ -504,7 +469,7 @@ e types") | (f,ar)::oth -> (try (let _ = lookup_named_val f sign in - error "name already used in the environment") + error "Name already used in the environment.") with | Not_found -> mk_sign (push_named_context_val (f,None,ar) sign) oth) @@ -533,8 +498,8 @@ e types") (* And now the structural rules *) | Thin ids -> - let (ngl, nsigma) = clear_hyps sigma ids goal in - ([ngl], nsigma) + let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in + ([mk_goal hyps concl], nsigma) | ThinBody ids -> let clear_aux env id = @@ -550,13 +515,13 @@ e types") let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in let hyps' = - move_after withdep toleft (left,declfrom,right) hto in + move_hyp withdep toleft (left,declfrom,right) hto in ([mk_goal hyps' cl], sigma) | Rename (id1,id2) -> if !check & id1 <> id2 && List.mem id2 (ids_of_named_context (named_context_of_val sign)) then - error ((string_of_id id2)^" is already used"); + error ((string_of_id id2)^" is already used."); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in ([mk_goal sign' cl'], sigma) @@ -617,20 +582,9 @@ let prim_extractor subfun vl pft = let cb = subst_proof_vars vl b in let cty = subst_proof_vars vl ty in mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) - | _ -> error "incomplete proof!") + | _ -> error "Incomplete proof!") - | Some (Prim (Intro_replacing id),[spf]) -> - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,ty,_) -> - let cty = subst_proof_vars vl ty in - mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) - | LetIn (_,b,ty,_) -> - let cb = subst_proof_vars vl b in - let cty = subst_proof_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) - | _ -> error "incomplete proof!") - - | Some (Prim (Cut (b,id,t)),[spf1;spf2]) -> + | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) -> let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t, subfun (add_proof_var id vl) spf2) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index dbe40780..41935c9c 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *) +(*i $Id: proof_type.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (*i*) open Environ @@ -28,8 +28,7 @@ open Pattern type prim_rule = | Intro of identifier - | Intro_replacing of identifier - | Cut of bool * identifier * types + | Cut of bool * bool * identifier * types | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr @@ -37,7 +36,7 @@ type prim_rule = | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list - | Move of bool * identifier * identifier + | Move of bool * identifier * identifier move_location | Rename of identifier * identifier | Change_evars @@ -94,3 +93,16 @@ and tactic_arg = type hyp_location = identifier Tacexpr.raw_hyp_location +type ltac_call_kind = + | LtacNotationCall of string + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref + | LtacVarCall of identifier * glob_tactic_expr + | LtacConstrInterp of rawconstr * + ((identifier * constr) list * (identifier * identifier option) list) + +type ltac_trace = (loc * ltac_call_kind) list + +exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn + +let abstract_tactic_box = ref (ref None) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 4fbcda4c..a7057a7d 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli 9842 2007-05-20 17:44:23Z herbelin $ i*) +(*i $Id: proof_type.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Environ @@ -28,8 +28,7 @@ open Pattern type prim_rule = | Intro of identifier - | Intro_replacing of identifier - | Cut of bool * identifier * types + | Cut of bool * bool * identifier * types | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr @@ -37,7 +36,7 @@ type prim_rule = | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list - | Move of bool * identifier * identifier + | Move of bool * identifier * identifier move_location | Rename of identifier * identifier | Change_evars @@ -128,3 +127,17 @@ and tactic_arg = Tacexpr.gen_tactic_arg type hyp_location = identifier Tacexpr.raw_hyp_location + +type ltac_call_kind = + | LtacNotationCall of string + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref + | LtacVarCall of identifier * glob_tactic_expr + | LtacConstrInterp of rawconstr * + ((identifier * constr) list * (identifier * identifier option) list) + +type ltac_trace = (loc * ltac_call_kind) list + +exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn + +val abstract_tactic_box : atomic_tactic_expr option ref ref diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 172a7d70..6e08e741 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 11021 2008-05-29 16:48:18Z barras $ *) +(* $Id: refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -189,7 +189,6 @@ let leaf g = let check_subproof_connection gl spfl = list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl - let abstract_operation syntax semantics gls = let (sgl_sigma,validation) = semantics gls in let hidden_proof = validation (List.map leaf sgl_sigma.it) in @@ -204,6 +203,7 @@ let abstract_tactic_expr ?(dflt=false) te tacfun gls = abstract_operation (Tactic(te,dflt)) tacfun gls let abstract_tactic ?(dflt=false) te = + !abstract_tactic_box := Some te; abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) let abstract_extended_tactic ?(dflt=false) s args = @@ -491,13 +491,18 @@ let tclNOTSAMEGOAL (tac : tactic) goal = (str"Tactic generated a subgoal identical to the original goal.") else rslt -let catch_failerror = function - | e when catchable_exception e -> check_for_interrupt () - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> +let catch_failerror e = + if catchable_exception e then check_for_interrupt () + else match e with + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) + | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise + (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -548,14 +553,8 @@ let ite_gen tcal tac_if continue tac_else gl= try tcal tac_if0 continue gl with (* Breakpoint *) - | e when catchable_exception e -> - check_for_interrupt (); tac_else0 e gl - | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e -> - check_for_interrupt (); tac_else0 e gl - | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) - + | e -> catch_failerror e; tac_else0 e gl + (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) @@ -754,9 +753,7 @@ let extract_open_pftreestate pts = let extract_pftreestate pts = if pts.tstack <> [] then - errorlabstrm "extract_pftreestate" - (str"Cannot extract from a proof-tree in which we have descended;" ++ - spc () ++ str"Please ascend to the root"); + errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed"); let pfterm,subgoals = extract_open_pftreestate pts in let exl = Evarutil.non_instantiated pts.tpfsigma in if subgoals <> [] or exl <> [] then diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d0789980..8e51171f 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml 11100 2008-06-11 11:10:31Z herbelin $ i*) +(*i $Id: tacexpr.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) open Names open Topconstr @@ -65,6 +65,20 @@ type hyp_location_flag = (* To distinguish body and type of local defs *) type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveToEnd of bool + +let no_move = MoveToEnd true + +open Pp + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top") + type 'a induction_arg = | ElimOnConstr of 'a | ElimOnIdent of identifier located @@ -76,8 +90,10 @@ type inversion_kind = | FullInversionClear type ('c,'id) inversion_strength = - | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr - | DepInversion of inversion_kind * 'c option * intro_pattern_expr + | NonDepInversion of + inversion_kind * 'id list * intro_pattern_expr located option + | DepInversion of + inversion_kind * 'c option * intro_pattern_expr located option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -106,6 +122,11 @@ let simple_clause_of = function | _ -> error "not a simple clause (one hypothesis or conclusion)" +type ('constr,'id) induction_clause = + ('constr with_bindings induction_arg list * 'constr with_bindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + 'id gclause option) + type multi = | Precisely of int | UpTo of int @@ -130,14 +151,14 @@ type ('a,'t) match_rule = type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Basic tactics *) - | TacIntroPattern of intro_pattern_expr list + | TacIntroPattern of intro_pattern_expr located list | TacIntrosUntil of quantified_hypothesis - | TacIntroMove of identifier option * identifier located option + | TacIntroMove of identifier option * 'id move_location | TacAssumption | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr - | TacApply of advanced_flag * evars_flag * 'constr with_bindings + | TacApply of advanced_flag * evars_flag * 'constr with_bindings list | TacElim of evars_flag * 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr @@ -149,19 +170,14 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacCofix of identifier option | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list | TacCut of 'constr - | TacAssert of 'tac option * intro_pattern_expr * 'constr + | TacAssert of 'tac option * intro_pattern_expr located * 'constr | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause * letin_flag (* Derived basic tactics *) - | TacSimpleInduction of quantified_hypothesis - | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * - 'constr with_bindings option * intro_pattern_expr * 'id gclause option - | TacSimpleDestruct of quantified_hypothesis - | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list * - 'constr with_bindings option * intro_pattern_expr * 'id gclause option - + | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis + | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause list | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr | TacDecomposeOr of 'constr @@ -181,7 +197,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Context management *) | TacClear of bool * 'id list | TacClearBody of 'id list - | TacMove of bool * 'id * 'id + | TacMove of bool * 'id * 'id move_location | TacRename of ('id *'id) list | TacRevert of 'id list @@ -236,7 +252,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list - | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg @@ -249,7 +265,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | TacVoid | MetaIdArg of loc * bool * string | ConstrMayEval of ('constr,'cst) may_eval - | IntroPattern of intro_pattern_expr + | IntroPattern of intro_pattern_expr located | Reference of 'ref | Integer of int | TacCall of loc * diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 213cc13f..6bbaff08 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml 10544 2008-02-09 11:31:35Z herbelin $ *) +(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +open Pp open Util open Names open Nameops @@ -58,7 +59,7 @@ let pf_get_hyp gls id = try Sign.lookup_named id (pf_hyps gls) with Not_found -> - error ("No such hypothesis : " ^ (string_of_id id)) + error ("No such hypothesis: " ^ (string_of_id id)) let pf_get_hyp_typ gls id = let (_,_,ty)= (pf_get_hyp gls id) in @@ -175,15 +176,11 @@ let refiner = refiner let introduction_no_check id = refiner (Prim (Intro id)) -(* This does not check that the dependencies are correct *) -let intro_replacing_no_check whereid gl = - refiner (Prim (Intro_replacing whereid)) gl - -let internal_cut_no_check id t gl = - refiner (Prim (Cut (true,id,t))) gl +let internal_cut_no_check replace id t gl = + refiner (Prim (Cut (true,replace,id,t))) gl -let internal_cut_rev_no_check id t gl = - refiner (Prim (Cut (false,id,t))) gl +let internal_cut_rev_no_check replace id t gl = + refiner (Prim (Cut (false,replace,id,t))) gl let refine_no_check c gl = refiner (Prim (Refine c)) gl @@ -220,13 +217,12 @@ let mutual_cofix f others gl = (* Versions with consistency checks *) let introduction id = with_check (introduction_no_check id) -let intro_replacing id = with_check (intro_replacing_no_check id) -let internal_cut d t = with_check (internal_cut_no_check d t) -let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t) +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) let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) -let thin l = with_check (thin_no_check l) +let thin c = with_check (thin_no_check c) let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') let rename_hyp l = with_check (rename_hyp_no_check l) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 8b0053a4..2fc66e71 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacmach.mli 11094 2008-06-10 19:35:23Z herbelin $ i*) +(*i $Id: tacmach.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names @@ -123,15 +123,15 @@ val change_constraints_pftreestate : val refiner : rule -> tactic val introduction_no_check : identifier -> tactic -val intro_replacing_no_check : identifier -> tactic -val internal_cut_no_check : identifier -> types -> tactic -val internal_cut_rev_no_check : identifier -> types -> tactic +val internal_cut_no_check : bool -> identifier -> types -> tactic +val internal_cut_rev_no_check : bool -> identifier -> types -> tactic val refine_no_check : constr -> tactic val convert_concl_no_check : types -> cast_kind -> tactic val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : identifier list -> tactic val thin_body_no_check : identifier list -> tactic -val move_hyp_no_check : bool -> identifier -> identifier -> tactic +val move_hyp_no_check : + bool -> identifier -> identifier move_location -> tactic val rename_hyp_no_check : (identifier*identifier) list -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic @@ -140,15 +140,14 @@ val mutual_cofix : identifier -> (identifier * constr) list -> tactic (*s The most primitive tactics with consistency and type checking *) val introduction : identifier -> tactic -val intro_replacing : identifier -> tactic -val internal_cut : identifier -> types -> tactic -val internal_cut_rev : identifier -> types -> tactic +val internal_cut : bool -> identifier -> types -> tactic +val internal_cut_rev : bool -> identifier -> types -> tactic val refine : constr -> tactic val convert_concl : types -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val thin_body : identifier list -> tactic -val move_hyp : bool -> identifier -> identifier -> tactic +val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier*identifier) list -> tactic (*s Tactics handling a list of goals. *) -- cgit v1.2.3