summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/evar_refiner.ml23
-rw-r--r--proofs/logic.ml200
-rw-r--r--proofs/proof_type.ml20
-rw-r--r--proofs/proof_type.mli21
-rw-r--r--proofs/refiner.ml33
-rw-r--r--proofs/tacexpr.ml50
-rw-r--r--proofs/tacmach.ml24
-rw-r--r--proofs/tacmach.mli17
8 files changed, 189 insertions, 199 deletions
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. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-15 21:21:54 +0000