summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml47
-rw-r--r--proofs/clenvtac.mli2
-rw-r--r--proofs/decl_expr.mli24
-rw-r--r--proofs/decl_mode.ml42
-rw-r--r--proofs/decl_mode.mli8
-rw-r--r--proofs/evar_refiner.ml53
-rw-r--r--proofs/evar_refiner.mli8
-rw-r--r--proofs/logic.ml187
-rw-r--r--proofs/logic.mli6
-rw-r--r--proofs/pfedit.ml108
-rw-r--r--proofs/pfedit.mli23
-rw-r--r--proofs/proof_trees.ml25
-rw-r--r--proofs/proof_trees.mli4
-rw-r--r--proofs/proof_type.ml31
-rw-r--r--proofs/proof_type.mli43
-rw-r--r--proofs/proofs.mllib12
-rw-r--r--proofs/redexpr.ml131
-rw-r--r--proofs/redexpr.mli15
-rw-r--r--proofs/refiner.ml312
-rw-r--r--proofs/refiner.mli30
-rw-r--r--proofs/tacexpr.ml149
-rw-r--r--proofs/tacmach.ml61
-rw-r--r--proofs/tacmach.mli20
-rw-r--r--proofs/tactic_debug.ml8
-rw-r--r--proofs/tactic_debug.mli6
25 files changed, 770 insertions, 585 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 769a9572..9bc818e8 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenvtac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -30,34 +30,34 @@ open Pattern
open Tacexpr
open Clenv
-
+
(* This function put casts around metavariables whose type could not be
* infered by the refiner, that is head of applications, predicates and
* subject of Cases.
* Does check that the casted type is closed. Anyway, the refiner would
* fail in this case... *)
-let clenv_cast_meta clenv =
+let clenv_cast_meta clenv =
let rec crec u =
match kind_of_term u with
| App _ | Case _ -> crec_hd u
| Cast (c,_,_) when isMeta c -> u
| _ -> map_constr crec u
-
+
and crec_hd u =
match kind_of_term (strip_outer_cast u) with
- | Meta mv ->
- (try
+ | Meta mv ->
+ (try
let b = Typing.meta_type clenv.evd mv in
- if occur_meta b then
- raise (RefinerError (MetaInType b));
- mkCast (mkMeta mv, DEFAULTcast, b)
+ assert (not (occur_meta b));
+ if occur_meta b then u
+ else mkCast (mkMeta mv, DEFAULTcast, b)
with Not_found -> u)
- | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
- | Case(ci,p,c,br) ->
- mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
- | _ -> u
- in
+ | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+ | Case(ci,p,c,br) ->
+ mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+ | _ -> u
+ in
crec
let clenv_value_cast_meta clenv =
@@ -70,16 +70,17 @@ let clenv_pose_dependent_evars with_evars clenv =
(RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
-
let clenv_refine with_evars ?(with_classes=true) clenv gls =
let clenv = clenv_pose_dependent_evars with_evars clenv in
- let evd' =
- if with_classes then
- Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd
+ let evd' =
+ if with_classes then
+ Typeclasses.resolve_typeclasses ~fail:(not with_evars)
+ clenv.env clenv.evd
else clenv.evd
in
+ let clenv = { clenv with evd = evd' } in
tclTHEN
- (tclEVARS (evars_of evd'))
+ (tclEVARS evd')
(refine (clenv_cast_meta clenv (clenv_value clenv)))
gls
@@ -104,17 +105,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
open Unification
let fail_quick_unif_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
+ modulo_conv_on_closed_terms = Some full_transparent_state;
use_metas_eagerly = false;
modulo_delta = empty_transparent_state;
+ resolve_evars = false;
+ use_evars_pattern_unification = false;
}
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
+let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
let env = pf_env gls in
let evd = create_goal_evar_defs (project gls) in
let evd' = w_unify false env CONV ~flags m n evd in
- tclIDTAC {it = gls.it; sigma = evars_of evd'}
+ tclIDTAC {it = gls.it; sigma = evd'}
let unify ?(flags=fail_quick_unif_flags) m gls =
let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 04a5eb57..96fb262a 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: clenvtac.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 22752eda..bf5fa2e9 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_expr.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id$ *)
open Names
open Util
open Tacexpr
-type 'it statement =
+type 'it statement =
{st_label:name;
st_it:'it}
@@ -41,12 +41,12 @@ type ('it,'constr,'tac) cut =
cut_by: 'constr list option;
cut_using: 'tac option}
-type ('var,'constr) hyp =
- Hvar of 'var
+type ('var,'constr) hyp =
+ Hvar of 'var
| Hprop of 'constr statement
-type ('constr,'tac) casee =
- Real of 'constr
+type ('constr,'tac) casee =
+ Real of 'constr
| Virtual of ('constr statement,'constr,'tac) cut
type ('hyp,'constr,'pat,'tac) bare_proof_instr =
@@ -64,9 +64,9 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
| Pfocus of 'constr statement
| Pdefine of identifier * 'hyp list * 'constr
| Pcast of identifier or_thesis * 'constr
- | Psuppose of ('hyp,'constr) hyp list
- | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
- | Ptake of 'constr list
+ | Psuppose of ('hyp,'constr) hyp list
+ | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+ | Ptake of 'constr list
| Pper of elim_type * ('constr,'tac) casee
| Pend of block_type
| Pescape
@@ -86,11 +86,11 @@ type raw_proof_instr =
type glob_proof_instr =
((identifier*(Genarg.rawconstr_and_expr option)) located,
- Genarg.rawconstr_and_expr,
+ Genarg.rawconstr_and_expr,
Topconstr.cases_pattern_expr,
Tacexpr.glob_tactic_expr) gen_proof_instr
-type proof_pattern =
+type proof_pattern =
{pat_vars: Term.types statement list;
pat_aliases: (Term.constr*Term.types) statement list;
pat_constr: Term.constr;
@@ -100,6 +100,6 @@ type proof_pattern =
type proof_instr =
(Term.constr statement,
- Term.constr,
+ Term.constr,
proof_pattern,
Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 134a4d8b..8be5f355 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
+(*i $Id$ i*)
open Names
open Term
@@ -15,9 +15,9 @@ open Util
let daimon_flag = ref false
-let set_daimon_flag () = daimon_flag:=true
+let set_daimon_flag () = daimon_flag:=true
let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag
+let get_daimon_flag () = !daimon_flag
type command_mode =
Mode_tactic
@@ -27,12 +27,12 @@ type command_mode =
let mode_of_pftreestate pts =
let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
if goal.evar_extra = None then
- Mode_tactic
+ Mode_tactic
else
Mode_proof
-
+
let get_current_mode () =
- try
+ try
mode_of_pftreestate (Pfedit.get_pftreestate ())
with _ -> Mode_none
@@ -42,7 +42,7 @@ let check_not_proof_mode str =
type split_tree=
Skip_patt of Idset.t * split_tree
- | Split_patt of Idset.t * inductive *
+ | Split_patt of Idset.t * inductive *
(bool array * (Idset.t * split_tree) option) array
| Close_patt of split_tree
| End_patt of (identifier * (int * int))
@@ -54,7 +54,7 @@ type elim_kind =
type recpath = int option*Declarations.wf_paths
-type per_info =
+type per_info =
{per_casee:constr;
per_ctype:types;
per_ind:inductive;
@@ -64,7 +64,7 @@ type per_info =
per_nparams:int;
per_wf:recpath}
-type stack_info =
+type stack_info =
Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
| Suppose_case
| Claim
@@ -73,7 +73,7 @@ type stack_info =
type pm_info =
{ pm_stack : stack_info list}
-let pm_in,pm_out = Dyn.create "pm_info"
+let pm_in,pm_out = Dyn.create "pm_info"
let get_info gl=
match gl.evar_extra with
@@ -81,30 +81,30 @@ let get_info gl=
| Some extra ->
try pm_out extra with _ -> invalid_arg "get_info"
-let get_stack pts =
+let get_stack pts =
let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
info.pm_stack
-let get_top_stack pts =
+let get_top_stack pts =
let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
info.pm_stack
let get_end_command pts =
- match mode_of_pftreestate pts with
+ match mode_of_pftreestate pts with
Mode_proof ->
- Some
+ Some
begin
match get_top_stack pts with
[] -> "\"end proof\""
| Claim::_ -> "\"end claim\""
| Focus_claim::_-> "\"end focus\""
- | (Suppose_case :: Per (et,_,_,_) :: _
- | Per (et,_,_,_) :: _ ) ->
+ | (Suppose_case :: Per (et,_,_,_) :: _
+ | Per (et,_,_,_) :: _ ) ->
begin
match et with
- Decl_expr.ET_Case_analysis ->
+ Decl_expr.ET_Case_analysis ->
"\"end cases\" or start a new case"
- | Decl_expr.ET_Induction ->
+ | Decl_expr.ET_Induction ->
"\"end induction\" or start a new case"
end
| _ -> anomaly "lonely suppose"
@@ -112,7 +112,7 @@ let get_end_command pts =
| Mode_tactic ->
begin
try
- ignore
+ ignore
(Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
Some "\"return\""
with Not_found -> None
@@ -120,8 +120,8 @@ let get_end_command pts =
| Mode_none ->
error "no proof in progress"
-let get_last env =
- try
+let get_last env =
+ try
let (id,_,_) = List.hd (Environ.named_context env) in id
with Invalid_argument _ -> error "no previous statement to use"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index bcfd6a96..1ecd4d3a 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_mode.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
+(* $Id$ *)
open Names
open Term
@@ -23,7 +23,7 @@ type command_mode =
| Mode_none
val mode_of_pftreestate : pftreestate -> command_mode
-
+
val get_current_mode : unit -> command_mode
val check_not_proof_mode : string -> unit
@@ -42,7 +42,7 @@ type elim_kind =
type recpath = int option*Declarations.wf_paths
-type per_info =
+type per_info =
{per_casee:constr;
per_ctype:types;
per_ind:inductive;
@@ -52,7 +52,7 @@ type per_info =
per_nparams:int;
per_wf:recpath}
-type stack_info =
+type stack_info =
Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
| Suppose_case
| Claim
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f4613f8d..e4fab3f2 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,45 +6,59 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id$ *)
open Util
open Names
open Term
open Evd
+open Evarutil
open Sign
open Proof_trees
open Refiner
-open Pretyping
(******************************************)
(* Instantiation of existential variables *)
(******************************************)
-(* w_tactic pour instantiate *)
+let depends_on_evar evk _ (pbty,_,t1,t2) =
+ try head_evar t1 = evk
+ with NoHeadEvar ->
+ try head_evar t2 = evk
+ with NoHeadEvar -> false
-let w_refine evk (ltac_vars,rawc) evd =
- if Evd.is_defined (evars_of evd) evk then
+let define_and_solve_constraints evk c evd =
+ try
+ let evd = define evk c evd in
+ let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+ fst (List.fold_left
+ (fun (evd,b as p) (pbty,env,t1,t2) ->
+ if b then Evarconv.evar_conv_x env evd pbty t1 t2 else p) (evd,true)
+ pbs)
+ with e when Pretype_errors.precatchable_exception e ->
+ error "Instance does not satisfy constraints."
+
+let w_refine (evk,evi) (ltac_var,rawc) sigma =
+ if Evd.is_defined sigma evk then
error "Instantiate called on already-defined evar";
- let e_info = Evd.find (evars_of evd) evk in
- let env = Evd.evar_env e_info in
- let evd',typed_c =
- try Pretyping.Default.understand_ltac
- (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
+ let env = Evd.evar_env evi in
+ let sigma',typed_c =
+ try Pretyping.Default.understand_ltac true sigma env ltac_var
+ (Pretyping.OfType (Some evi.evar_concl)) rawc
with _ ->
let loc = Rawterm.loc_of_rawconstr rawc in
- user_err_loc
+ user_err_loc
(loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
string_of_existential evk))
in
- evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
+ define_and_solve_constraints evk typed_c (evars_reset_evd sigma' sigma)
(* vernac command Existential *)
-let instantiate_pf_com n com pfts =
+let instantiate_pf_com n com pfts =
let gls = top_goal_of_pftreestate pfts in
- let sigma = gls.sigma in
- let (evk,evi) =
+ let sigma = gls.sigma in
+ let (evk,evi) =
let evl = Evarutil.non_instantiated sigma in
if (n <= 0) then
error "incorrect existential variable index"
@@ -52,9 +66,8 @@ let instantiate_pf_com n com pfts =
error "not so many uninstantiated existential variables"
else
List.nth evl (n-1)
- in
+ in
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 evk (([],[]),rawc) evd in
- change_constraints_pftreestate (evars_of evd') pfts
+ let rawc = Constrintern.intern_constr sigma env com in
+ let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
+ change_constraints_pftreestate sigma' pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a42b11a4..30e702a0 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evar_refiner.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -20,10 +20,10 @@ open Rawterm
(* Refinement of existential variables. *)
-val w_refine : evar -> (var_map * unbound_ltac_var_map) * rawconstr ->
- evar_defs -> evar_defs
+val w_refine : evar * evar_info ->
+ rawconstr_ltac_closure -> evar_map -> evar_map
val instantiate_pf_com :
int -> Topconstr.constr_expr -> pftreestate -> pftreestate
-(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c019d45f..9cab6a05 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -28,7 +28,7 @@ open Type_errors
open Retyping
open Evarutil
open Tacexpr
-
+
type refiner_error =
(* Errors raised by the refiner *)
@@ -50,15 +50,17 @@ open Pretype_errors
let rec catchable_exception = function
| Stdpp.Exc_located(_,e) -> catchable_exception e
| LtacLocated(_,e) -> catchable_exception e
- | Util.UserError _ | TypeError _
+ | Util.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+ (* reduction errors *)
+ | Tacred.ReductionTacticError _
(* unification errors *)
| PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
|CannotFindWellTypedAbstraction _
|UnsolvableImplicit _)) -> true
- | Typeclasses_errors.TypeClassError
+ | Typeclasses_errors.TypeClassError
(_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
| _ -> false
@@ -73,19 +75,19 @@ 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 sign id f =
- try apply_to_hyp sign id f
- with Hyp_not_found ->
+ try apply_to_hyp sign id f
+ with Hyp_not_found ->
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 ->
+ try apply_to_hyp_and_dependent_on sign id f g
+ with Hyp_not_found ->
if !check then error "No such assumption."
else sign
let check_typability env sigma c =
- if !check then let _ = type_of env sigma c in ()
+ if !check then let _ = type_of env sigma c in ()
(************************************************************************)
(************************************************************************)
@@ -99,7 +101,7 @@ let check_typability env sigma c =
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 sign cl ids in
- (hyps,concl,evars_of !evdref)
+ (hyps,concl, !evdref)
(* The ClearBody tactic *)
@@ -111,7 +113,7 @@ let recheck_typability (what,id) env sigma t =
| Some id -> "hypothesis "^(string_of_id id) in
error
("The correctness of "^s^" relies on the body of "^(string_of_id id))
-
+
let remove_hyp_body env sigma id =
let sign =
apply_to_hyp_and_dependent_on (named_context_val env) id
@@ -121,7 +123,7 @@ let remove_hyp_body env sigma id =
| Some c ->(id,None,t))
(fun (id',c,t as d) sign ->
(if !check then
- begin
+ begin
let env = reset_with_named_context sign env in
match c with
| None -> recheck_typability (Some id',id) env sigma t
@@ -130,7 +132,7 @@ let remove_hyp_body env sigma id =
recheck_typability (Some id',id) env sigma b'
end;d))
in
- reset_with_named_context sign env
+ reset_with_named_context sign env
(* Reordering of the context *)
@@ -138,7 +140,7 @@ let remove_hyp_body env sigma id =
(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
(* reculees par rapport aux autres (faire le contraire!) *)
-
+
let mt_q = (Idmap.empty,[])
let push_val y = function
(_,[] as q) -> q
@@ -211,8 +213,8 @@ let check_decl_position env sign (x,_,_ as d) =
(* Auxiliary functions for primitive MOVE tactic
*
* [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
+ * 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. *)
@@ -228,17 +230,17 @@ let split_sign hfrom hto l =
let rec splitrec left toleft = function
| [] -> error_no_such_hypothesis hfrom
| (hyp,c,typ) as d :: right ->
- if hyp = hfrom then
+ if hyp = hfrom then
(left,right,d, toleft or hto = MoveToEnd true)
else
- splitrec (d::left)
+ splitrec (d::left)
(toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
right
- in
+ in
splitrec [] false l
let hyp_of_move_location = function
- | MoveAfter id -> id
+ | MoveAfter id -> id
| MoveBefore id -> id
| _ -> assert false
@@ -258,12 +260,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
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 & hto <> MoveAfter hyp then
+ if List.exists (test_dep d) middle then
+ if with_dep & hto <> MoveAfter hyp then
(first, d::middle)
- else
- errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++
- pr_move_location pr_id hto ++
+ else
+ errorlabstrm "move_hyp" (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
@@ -271,16 +273,16 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
in
if hto = MoveAfter hyp then
List.rev first' @ List.rev middle' @ right
- else
+ else
moverec first' middle' right
in
- if toleft then
- let right =
+ if toleft then
+ let right =
List.fold_right push_named_context_val right empty_named_context_val in
List.fold_left (fun sign d -> push_named_context_val d sign)
- right (moverec [] [declfrom] left)
- else
- let right =
+ right (moverec [] [declfrom] left)
+ else
+ let right =
List.fold_right push_named_context_val
(moverec [] [declfrom] right) empty_named_context_val in
List.fold_left (fun sign d -> push_named_context_val d sign)
@@ -295,7 +297,7 @@ let rename_hyp id1 id2 sign =
(************************************************************************)
(* Implementation of the logical rules *)
-(* Will only be used on terms given to the Refine rule which have meta
+(* Will only be used on terms given to the Refine rule which have meta
variables only in Application and Case *)
let error_unsupported_deep_meta c =
@@ -303,7 +305,7 @@ let error_unsupported_deep_meta c =
strbrk "form contains metavariables deep inside the term is not " ++
strbrk "supported; try \"refine\" instead.")
-let collect_meta_variables c =
+let collect_meta_variables c =
let rec collrec deep acc c = match kind_of_term c with
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
@@ -312,16 +314,16 @@ let collect_meta_variables c =
in
List.rev (collrec false [] c)
-let check_meta_variables c =
+let check_meta_variables c =
if not (list_distinct (collect_meta_variables c)) then
raise (RefinerError (NonLinearProof c))
let check_conv_leq_goal env sigma arg ty conclty =
- if !check & not (is_conv_leq env sigma ty conclty) then
+ if !check & not (is_conv_leq env sigma ty conclty) then
raise (RefinerError (BadType (arg,ty,conclty)))
let goal_type_of env sigma c =
- (if !check then type_of else Retyping.get_type_of) env sigma c
+ (if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = evar_env goal in
@@ -329,7 +331,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
(*
if not (occur_meta trm) then
- let t'ty = (unsafe_machine env sigma trm).uj_type in
+ let t'ty = (unsafe_machine env sigma trm).uj_type in
let _ = conv_leq_goal env sigma trm t'ty conclty in
(goalacc,t'ty)
else
@@ -352,9 +354,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| Ind _ | Const _
when (isInd f or has_polymorphic_type (destConst f)) ->
(* Sort-polymorphism of definition and inductive types *)
- goalacc,
+ goalacc,
type_of_global_reference_knowing_conclusion env sigma f conclty
- | _ ->
+ | _ ->
mk_hdgoals sigma goal goalacc f
in
let (acc'',conclty') =
@@ -365,14 +367,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| Case (_,p,c,lf) ->
let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
check_conv_leq_goal env sigma trm conclty' conclty;
- let acc'' =
+ let acc'' =
array_fold_left2
(fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
- acc' lbrty lf
+ acc' lbrty lf
in
(acc'',conclty')
- | _ ->
+ | _ ->
if occur_meta trm then
anomaly "refiner called with a meta in non app/case subterm";
@@ -397,8 +399,8 @@ and mk_hdgoals sigma goal goalacc trm =
mk_refgoals sigma goal goalacc ty t
| App (f,l) ->
- let (acc',hdty) =
- if isInd f or isConst f
+ let (acc',hdty) =
+ if isInd f or isConst f
& not (array_exists occur_meta l) (* we could be finer *)
then
(goalacc,type_of_global_reference_knowing_parameters env sigma f l)
@@ -408,16 +410,16 @@ and mk_hdgoals sigma goal goalacc trm =
| Case (_,p,c,lf) ->
let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
- let acc'' =
+ let acc'' =
array_fold_left2
(fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
- acc' lbrty lf
+ acc' lbrty lf
in
(acc'',conclty')
| _ ->
if !check && occur_meta trm then
- anomaly "refined called with a dependent meta";
+ anomaly "refine called with a dependent meta";
goalacc, goal_type_of env sigma trm
and mk_arggoals sigma goal goalacc funty = function
@@ -434,14 +436,13 @@ and mk_arggoals sigma goal goalacc funty = function
and mk_casegoals sigma goal goalacc p c =
let env = evar_env goal in
- let (acc',ct) = mk_hdgoals sigma goal goalacc c in
+ let (acc',ct) = mk_hdgoals sigma goal goalacc c in
let (acc'',pt) = mk_hdgoals sigma goal acc' p in
- let pj = {uj_val=p; uj_type=pt} in
let indspec =
- try find_mrectype env sigma (nf_evar sigma ct)
+ try find_mrectype env sigma ct
with Not_found -> anomaly "mk_casegoals" in
let (lbrty,conclty) =
- type_case_branches_with_names env indspec pj c in
+ type_case_branches_with_names env indspec p c in
(acc'',lbrty,conclty)
@@ -467,7 +468,7 @@ let norm_goal sigma gl =
let red_fun = Evarutil.nf_evar sigma in
let ncl = red_fun gl.evar_concl in
let ngl =
- { gl with
+ { gl with
evar_concl = ncl;
evar_hyps = map_named_val red_fun gl.evar_hyps } in
if Evd.eq_evar_info ngl gl then None else Some ngl
@@ -487,7 +488,7 @@ let prim_refiner r sigma goal =
(* Logical rules *)
| Intro id ->
if !check && mem_named_context id (named_context_of_val sign) then
- error "New variable is already declared";
+ error ("Variable " ^ string_of_id id ^ " is already declared.");
(match kind_of_term (strip_outer_cast cl) with
| Prod (_,c1,b) ->
let sg = mk_goal (push_named_context_val (id,None,c1) sign)
@@ -500,7 +501,7 @@ let prim_refiner r sigma goal =
([sg], sigma)
| _ ->
raise (RefinerError IntroNeedsProduct))
-
+
| Cut (b,replace,id,t) ->
let sg1 = mk_goal sign (nf_betaiota sigma t) in
let sign,cl,sigma =
@@ -512,58 +513,58 @@ let prim_refiner r sigma goal =
cl,sigma
else
(if !check && mem_named_context id (named_context_of_val sign) then
- error "New variable is already declared";
+ error ("Variable " ^ string_of_id id ^ " is already declared.");
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,j) ->
- let rec check_ind env k cl =
- match kind_of_term (strip_outer_cast cl) with
- | Prod (na,c1,b) ->
- if k = 1 then
- try
+ let rec check_ind env k cl =
+ match kind_of_term (strip_outer_cast cl) with
+ | Prod (na,c1,b) ->
+ if k = 1 then
+ try
fst (find_inductive env sigma c1)
- with Not_found ->
+ with Not_found ->
error "Cannot do a fixpoint on a non inductive type."
- else
+ else
check_ind (push_rel (na,None,c1) env) (k-1) b
| _ -> error "Not enough products."
in
let (sp,_) = check_ind env n cl in
let firsts,lasts = list_chop j rest in
let all = firsts@(f,n,cl)::lasts in
- let rec mk_sign sign = function
+ let rec mk_sign sign = function
| (f,n,ar)::oth ->
- let (sp',_) = check_ind env n ar in
- if not (sp=sp') then
- error ("Fixpoints should be on the same " ^
+ let (sp',_) = check_ind env n ar in
+ if not (sp=sp') then
+ error ("Fixpoints should be on the same " ^
"mutual inductive declaration.");
if !check && mem_named_context f (named_context_of_val sign) then
error
("Name "^string_of_id f^" 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
- in
+ in
(mk_sign sign all, sigma)
-
+
| Cofix (f,others,j) ->
- let rec check_is_coind env cl =
+ let rec check_is_coind env cl =
let b = whd_betadeltaiota env sigma cl in
match kind_of_term b with
| Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
- | _ ->
- try
+ | _ ->
+ try
let _ = find_coinductive env sigma b in ()
- with Not_found ->
+ with Not_found ->
error ("All methods must construct elements " ^
"in coinductive types.")
in
let firsts,lasts = list_chop j others in
let all = firsts@(f,cl)::lasts in
List.iter (fun (_,c) -> check_is_coind env c) all;
- let rec mk_sign sign = function
+ let rec mk_sign sign = function
| (f,ar)::oth ->
(try
(let _ = lookup_named_val f sign in
@@ -572,7 +573,7 @@ let prim_refiner r sigma goal =
| Not_found ->
mk_sign (push_named_context_val (f,None,ar) sign) oth)
| [] -> List.map (fun (_,c) -> mk_goal sign c) all
- in
+ in
(mk_sign sign all, sigma)
| Refine c ->
@@ -587,17 +588,17 @@ let prim_refiner r sigma goal =
if (not !check) || is_conv_leq env sigma cl' cl then
let sg = mk_goal sign cl' in
([sg], sigma)
- else
+ else
error "convert-concl rule passed non-converting term"
| Convert_hyp (id,copt,ty) ->
([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
(* And now the structural rules *)
- | Thin ids ->
+ | Thin ids ->
let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
([mk_goal hyps concl], nsigma)
-
+
| ThinBody ids ->
let clear_aux env id =
let env' = remove_hyp_body env sigma id in
@@ -609,9 +610,9 @@ let prim_refiner r sigma goal =
([sg], sigma)
| Move (withdep, hfrom, hto) ->
- let (left,right,declfrom,toleft) =
+ let (left,right,declfrom,toleft) =
split_sign hfrom hto (named_context_of_val sign) in
- let hyps' =
+ let hyps' =
move_hyp withdep toleft (left,declfrom,right) hto in
([mk_goal hyps' cl], sigma)
@@ -642,7 +643,7 @@ type variable_proof_status = ProofVar | SectionVar of identifier
type proof_variable = name * variable_proof_status
-let subst_proof_vars =
+let subst_proof_vars =
let rec aux p vars =
let _,subst =
List.fold_left (fun (n,l) var ->
@@ -653,22 +654,22 @@ let subst_proof_vars =
(n+1,t)) (p,[]) vars
in replace_vars (List.rev subst)
in aux 1
-
+
let rec rebind id1 id2 = function
| [] -> [Name id2,SectionVar id1]
- | (na,k as x)::l ->
+ | (na,k as x)::l ->
if na = Name id1 then (Name id2,k)::l else
let l' = rebind id1 id2 l in
if na = Name id2 then (Anonymous,k)::l' else x::l'
let add_proof_var id vl = (Name id,ProofVar)::vl
-let proof_variable_index x =
+let proof_variable_index x =
let rec aux n = function
| (Name id,ProofVar)::l when x = id -> n
| _::l -> aux (n+1) l
| [] -> raise Not_found
- in
+ in
aux 1
let prim_extractor subfun vl pft =
@@ -684,7 +685,7 @@ let prim_extractor subfun vl pft =
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]) ->
let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
@@ -699,7 +700,7 @@ let prim_extractor subfun vl pft =
let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
(add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkFix ((vn,j),(names,lcty,lfix))
+ mkFix ((vn,j),(names,lcty,lfix))
| Some (Prim (Cofix (f,others,j)),spfl) ->
let firsts,lasts = list_chop j others in
@@ -707,14 +708,14 @@ let prim_extractor subfun vl pft =
let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
let names = Array.map (fun (f,_) -> Name f) all in
let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
- (add_proof_var f vl) others in
+ (add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
mkCoFix (j,(names,lcty,lfix))
-
+
| Some (Prim (Refine c),spfl) ->
let mvl = collect_meta_variables c in
let metamap = List.combine mvl (List.map (subfun vl) spfl) in
- let cc = subst_proof_vars vl c in
+ let cc = subst_proof_vars vl c in
plain_instance metamap cc
(* Structural and conversion rules do not produce any proof *)
@@ -727,10 +728,10 @@ let prim_extractor subfun vl pft =
| Some (Prim (Thin _),[pf]) ->
(* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
subfun vl pf
-
+
| Some (Prim (ThinBody _),[pf]) ->
subfun vl pf
-
+
| Some (Prim (Move _|Order _),[pf]) ->
subfun vl pf
@@ -743,4 +744,4 @@ let prim_extractor subfun vl pft =
| Some _ -> anomaly "prim_extractor"
| None-> error "prim_extractor handed incomplete proof"
-
+
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2f3a0d89..0d56da38 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: logic.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -26,9 +26,9 @@ val with_check : tactic -> tactic
[Intro]: no check that the name does not exist\\
[Intro_after]: no check that the name does not exist and that variables in
its type does not escape their scope\\
- [Intro_replacing]: no check that the name does not exist and that
+ [Intro_replacing]: no check that the name does not exist and that
variables in its type does not escape their scope\\
- [Convert_hyp]:
+ [Convert_hyp]:
no check that the name exist and that its type is convertible\\
*)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 0aba9f5f..f3658ad4 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pfedit.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -31,10 +31,12 @@ open Safe_typing
(* Mainly contributed by C. Murthy *)
(*********************************************************************)
+type lemma_possible_guards = int list list
+
type proof_topstate = {
mutable top_end_tac : tactic option;
top_init_tac : tactic option;
- top_compute_guard : bool;
+ top_compute_guard : lemma_possible_guards;
top_goal : goal;
top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
@@ -81,26 +83,26 @@ let get_current_goal_context () = get_goal_context 1
let set_current_proof = Edit.focus proof_edits
-let resume_proof (loc,id) =
- try
+let resume_proof (loc,id) =
+ try
Edit.focus proof_edits id
with Invalid_argument "Edit.focus" ->
user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
let suspend_proof () =
- try
+ try
Edit.unfocus proof_edits
with Invalid_argument "Edit.unfocus" ->
errorlabstrm "Pfedit.suspend_current_proof"
(str"No active proof" ++ (msg_proofs true))
-
+
let resume_last_proof () =
match (Edit.last_focused proof_edits) with
| None ->
errorlabstrm "resume_last" (str"No proof-editing in progress.")
- | Some p ->
+ | Some p ->
Edit.focus proof_edits p
-
+
let get_current_proof_name () =
match Edit.read proof_edits with
| None ->
@@ -114,14 +116,14 @@ let add_proof (na,pfs,ts) =
let delete_proof_gen = Edit.delete proof_edits
let delete_proof (loc,id) =
- try
+ try
delete_proof_gen id
with (UserError ("Edit.delete",_)) ->
user_err_loc
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
-
+
let mutate f =
- try
+ try
Edit.mutate proof_edits (fun _ pfs -> f pfs)
with Invalid_argument "Edit.mutate" ->
errorlabstrm "Pfedit.mutate"
@@ -131,31 +133,31 @@ let start (na,ts) =
let pfs = mk_pftreestate ts.top_goal in
let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
add_proof(na,pfs,ts)
-
+
let restart_proof () =
match Edit.read proof_edits with
- | None ->
+ | None ->
errorlabstrm "Pfedit.restart"
(str"No focused proof to restart" ++ msg_proofs true)
- | Some(na,_,ts) ->
+ | Some(na,_,ts) ->
delete_proof_gen na;
start (na,ts);
set_current_proof na
let proof_term () =
extract_pftreestate (get_pftreestate())
-
+
(* Detect is one has completed a subtree of the initial goal *)
-let subtree_solved () =
+let subtree_solved () =
let pts = get_pftreestate () in
- is_complete_proof (proof_of_pftreestate pts) &
+ is_complete_proof (proof_of_pftreestate pts) &
not (is_top_pftreestate pts)
-let tree_solved () =
+let tree_solved () =
let pts = get_pftreestate () in
is_complete_proof (proof_of_pftreestate pts)
-let top_tree_solved () =
+let top_tree_solved () =
let pts = get_pftreestate () in
is_complete_proof (proof_of_pftreestate (top_of_tree pts))
@@ -165,19 +167,19 @@ let top_tree_solved () =
let set_undo = function
| None -> undo_limit := undo_default
- | Some n ->
- if n>=0 then
+ | Some n ->
+ if n>=0 then
undo_limit := n
- else
+ else
error "Cannot set a negative undo limit"
let get_undo () = Some !undo_limit
let undo n =
- try
- Edit.undo proof_edits n;
- (* needed because the resolution of a subtree is done in 2 steps
- then a sequence of undo can lead to a focus on a completely solved
+ try
+ Edit.undo proof_edits n;
+ (* needed because the resolution of a subtree is done in 2 steps
+ then a sequence of undo can lead to a focus on a completely solved
subtree - this solution only works properly if undoing one step *)
if subtree_solved() then Edit.undo proof_edits 1
with (Invalid_argument "Edit.undo") ->
@@ -186,14 +188,14 @@ let undo n =
(* Undo current focused proof to reach depth [n]. This is used in
[vernac_backtrack]. *)
let undo_todepth n =
- try
+ try
Edit.undo_todepth proof_edits n
with (Invalid_argument "Edit.undo") ->
errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
(* Return the depth of the current focused proof stack, this is used
to put informations in coq prompt (in emacs mode). *)
-let current_proof_depth() =
+let current_proof_depth() =
try
Edit.depth proof_edits
with (Invalid_argument "Edit.depth") -> -1
@@ -206,7 +208,7 @@ let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f
let cook_proof k =
- let (pfs,ts) = get_state()
+ let (pfs,ts) = get_state()
and ident = get_current_proof_name () in
let {evar_concl=concl} = ts.top_goal
and strength = ts.top_strength in
@@ -220,19 +222,19 @@ let cook_proof k =
const_entry_boxed = false},
ts.top_compute_guard, strength, ts.top_hook))
-let current_proof_statement () =
+let current_proof_statement () =
let ts = get_topstate() in
- (get_current_proof_name (), ts.top_strength,
+ (get_current_proof_name (), ts.top_strength,
ts.top_goal.evar_concl, ts.top_hook)
(*********************************************************************)
(* Abort functions *)
(*********************************************************************)
-
+
let refining () = [] <> (Edit.dom proof_edits)
let check_no_pending_proofs () =
- if refining () then
+ if refining () then
errorlabstrm "check_no_pending_proofs"
(str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
str"Use \"Abort All\" first or complete proof(s).")
@@ -252,9 +254,9 @@ let set_end_tac tac =
(* Modifying the current prooftree *)
(*********************************************************************)
-let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook =
let top_goal = mk_goal sign concl None in
- let ts = {
+ let ts = {
top_end_tac = None;
top_init_tac = init_tac;
top_compute_guard = compute_guard;
@@ -269,7 +271,7 @@ let solve_nth k tac =
let pft = get_pftreestate () in
if not (List.mem (-1) (cursor_of_pftreestate pft)) then
mutate (solve_nth_pftreestate k tac)
- else
+ else
error "cannot apply a tactic when we are descended behind a tactic-node"
let by tac = mutate (solve_pftreestate tac)
@@ -278,7 +280,7 @@ let instantiate_nth_evar_com n c =
mutate (Evar_refiner.instantiate_pf_com n c)
let traverse n = mutate (traverse n)
-
+
(* [traverse_to path]
Traverses the current proof to get to the location specified by
@@ -296,7 +298,7 @@ let common_ancestor l1 l2 =
| _, _ -> List.rev l1, List.length l2
in
common_aux (List.rev l1) (List.rev l2)
-
+
let rec traverse_up = function
| 0 -> (function pf -> pf)
| n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf))
@@ -326,12 +328,34 @@ let make_focus n = focus_n := n
let focus () = !focus_n
let focused_goal () = let n = !focus_n in if n=0 then 1 else n
-let reset_top_of_tree () =
+let reset_top_of_tree () =
mutate top_of_tree
-
-let reset_top_of_script () =
- mutate (fun pts ->
+
+let reset_top_of_script () =
+ mutate (fun pts ->
try
up_until_matching_rule is_proof_instr pts
with Not_found -> top_of_tree pts)
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+open Decl_kinds
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let build_constant_by_tactic sign typ tac =
+ let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+ start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
+ try
+ by tac;
+ let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
+ delete_current_proof ();
+ const
+ with e ->
+ delete_current_proof ();
+ raise e
+
+let build_by_tactic typ tac =
+ let sign = Decls.clear_proofs (Global.named_context ()) in
+ (build_constant_by_tactic sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 464f6286..acb85247 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pfedit.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -78,9 +78,12 @@ val get_undo : unit -> int option
systematically apply at initialization time (e.g. to start the
proof of mutually dependent theorems) *)
-val start_proof :
+type lemma_possible_guards = int list list
+
+val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
- ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+ ?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
+ declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
@@ -107,8 +110,10 @@ val suspend_proof : unit -> unit
it fails if there is no current proof of if it is not completed;
it also tells if the guardness condition has to be inferred. *)
-val cook_proof : (Refiner.pftreestate -> unit) ->
- identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
+val cook_proof : (Refiner.pftreestate -> unit) ->
+ identifier *
+ (Entries.definition_entry * lemma_possible_guards * goal_kind *
+ declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
@@ -190,5 +195,13 @@ val traverse_prev_unproven : unit -> unit
(* These two functions make it possible to implement more elaborate
proof and goal management, as it is done, for instance in pcoq *)
+
val traverse_to : int list -> unit
val mutate : (pftreestate -> pftreestate) -> unit
+
+
+(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+
+val build_constant_by_tactic : named_context_val -> types -> tactic ->
+ Entries.definition_entry
+val build_by_tactic : types -> tactic -> constr
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 99a1e506..a5bd073a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *)
+(* $Id$ *)
open Closure
open Util
@@ -33,10 +33,11 @@ let is_bind = function
(* Functions on goals *)
-let mk_goal hyps cl extra =
- { evar_hyps = hyps; evar_concl = cl;
+let mk_goal hyps cl extra =
+ { evar_hyps = hyps; evar_concl = cl;
evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
- evar_body = Evar_empty; evar_extra = extra }
+ evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar);
+ evar_extra = extra }
(* Functions on proof trees *)
@@ -48,9 +49,9 @@ let ref_of_proof pf =
let rule_of_proof pf =
let (r,_) = ref_of_proof pf in r
-let children_of_proof pf =
+let children_of_proof pf =
let (_,cl) = ref_of_proof pf in cl
-
+
let goal_of_proof pf = pf.goal
let subproof_of_proof pf = match pf.ref with
@@ -68,13 +69,13 @@ let is_tactic_proof pf = match pf.ref with
| _ -> false
-let pf_lookup_name_as_renamed env ccl s =
- Detyping.lookup_name_as_renamed env ccl s
+let pf_lookup_name_as_displayed env ccl s =
+ Detyping.lookup_name_as_displayed env ccl s
let pf_lookup_index_as_renamed env ccl n =
Detyping.lookup_index_as_renamed env ccl n
-(* Functions on rules (Proof mode) *)
+(* Functions on rules (Proof mode) *)
let is_dem_rule = function
Decl_proof _ -> true
@@ -85,9 +86,9 @@ let is_proof_instr = function
| _ -> false
let is_focussing_command = function
- Decl_proof b -> b
- | Nested (Proof_instr (b,_),_) -> b
- | _ -> false
+ Decl_proof b -> b
+ | Nested (Proof_instr (b,_),_) -> b
+ | _ -> false
(*********************************************************************)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index f9b64f41..6d1fc143 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_trees.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -33,7 +33,7 @@ val is_complete_proof : proof_tree -> bool
val is_leaf_proof : proof_tree -> bool
val is_tactic_proof : proof_tree -> bool
-val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option
+val pf_lookup_name_as_displayed : env -> constr -> identifier -> int option
val pf_lookup_index_as_renamed : env -> constr -> int -> int option
val is_proof_instr : rule -> bool
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 150fb89f..1daddde9 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 12168 2009-06-06 21:34:37Z herbelin $ *)
+(*i $Id$ *)
(*i*)
open Environ
@@ -48,11 +48,11 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Nested of compound_rule * proof_tree
+ | Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
-and compound_rule=
+and compound_rule=
| Tactic of tactic_expr * bool
| Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
@@ -63,47 +63,48 @@ and tactic = goal sigma -> (goal list sigma * validation)
and validation = (proof_tree list -> proof_tree)
and tactic_expr =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_tactic_expr
and atomic_tactic_expr =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_atomic_tactic_expr
and tactic_arg =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_tactic_arg
-type hyp_location = identifier Tacexpr.raw_hyp_location
-
-type ltac_call_kind =
+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)
+ (extended_patvar_map * (identifier * identifier option) list)
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * 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 c80e126f..c4a48c3c 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 12168 2009-06-06 21:34:37Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Environ
@@ -32,7 +32,7 @@ type prim_rule =
| FixRule of identifier * int * (identifier * int * constr) list * int
| Cofix of identifier * (identifier * constr) list * int
| Refine of constr
- | Convert_concl of types * cast_kind
+ | Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
| Thin of identifier list
| ThinBody of identifier list
@@ -58,7 +58,7 @@ type prim_rule =
lc : [Set of evars occurring
in the type of evar] } };
...
- number of last evar,
+ number of last evar,
it = { evar_concl = [the type of evar]
evar_hyps = [the context of the evar]
evar_body = [the body of the Evar if any]
@@ -69,11 +69,11 @@ type prim_rule =
\end{verbatim}
*)
-(*s Proof trees.
- [ref] = [None] if the goal has still to be proved,
+(*s Proof trees.
+ [ref] = [None] if the goal has still to be proved,
and [Some (r,l)] if the rule [r] was applied to the goal
- and gave [l] as subproofs to be completed.
- if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
+ and gave [l] as subproofs to be completed.
+ if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
that the goal can be proven if the goals in [l] are solved. *)
type proof_tree = {
open_subgoals : int;
@@ -82,11 +82,11 @@ type proof_tree = {
and rule =
| Prim of prim_rule
- | Nested of compound_rule * proof_tree
+ | Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
-and compound_rule=
+and compound_rule=
(* the boolean of Tactic tells if the default tactic is used *)
| Tactic of tactic_expr * bool
| Proof_instr of bool * proof_instr
@@ -98,47 +98,48 @@ and tactic = goal sigma -> (goal list sigma * validation)
and validation = (proof_tree list -> proof_tree)
and tactic_expr =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_tactic_expr
and atomic_tactic_expr =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_atomic_tactic_expr
and tactic_arg =
- (open_constr,
+ (constr,
constr_pattern,
evaluable_global_reference,
inductive,
ltac_constant,
identifier,
- glob_tactic_expr)
+ glob_tactic_expr,
+ tlevel)
Tacexpr.gen_tactic_arg
-type hyp_location = identifier Tacexpr.raw_hyp_location
-
-type ltac_call_kind =
+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)
+ (extended_patvar_map * (identifier * identifier option) list)
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
val abstract_tactic_box : atomic_tactic_expr option ref ref
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
new file mode 100644
index 00000000..05b86b1a
--- /dev/null
+++ b/proofs/proofs.mllib
@@ -0,0 +1,12 @@
+Tacexpr
+Proof_type
+Redexpr
+Proof_trees
+Logic
+Refiner
+Evar_refiner
+Tacmach
+Pfedit
+Tactic_debug
+Clenvtac
+Decl_mode
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ad8ee3a2..b0a01caa 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -15,11 +15,13 @@ open Term
open Declarations
open Libnames
open Rawterm
+open Pattern
open Reductionops
open Tacred
open Closure
open RedFlags
open Libobject
+open Summary
(* call by value normalisation function using the virtual machine *)
let cbv_vm env _ c =
@@ -40,18 +42,18 @@ let set_strategy_one ref l =
let cb = Global.lookup_constant sp in
if cb.const_body <> None & cb.const_opaque then
errorlabstrm "set_transparent_const"
- (str "Cannot make" ++ spc () ++
+ (str "Cannot make" ++ spc () ++
Nametab.pr_global_env Idset.empty (ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
Csymtable.set_transparent_const sp
| _ -> ()
let cache_strategy (_,str) =
- List.iter
+ List.iter
(fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
str
-let subst_strategy (_,subs,(local,obj)) =
+let subst_strategy (subs,(local,obj)) =
local,
list_smartmap
(fun (k,ql as entry) ->
@@ -62,7 +64,7 @@ let subst_strategy (_,subs,(local,obj)) =
let map_strategy f l =
let l' = List.fold_right
- (fun (lev,ql) str ->
+ (fun (lev,ql) str ->
let ql' = List.fold_right
(fun q ql ->
match f q with
@@ -71,21 +73,15 @@ let map_strategy f l =
if ql'=[] then str else (lev,ql')::str) l [] in
if l'=[] then None else Some (false,l')
-let export_strategy (local,obj) =
- if local then None else
- map_strategy (function
- EvalVarRef _ -> None
- | EvalConstRef _ as q -> Some q) obj
-
-let classify_strategy (_,(local,_ as obj)) =
+let classify_strategy (local,_ as obj) =
if local then Dispose else Substitute obj
let disch_ref ref =
match ref with
- EvalConstRef c ->
+ EvalConstRef c ->
let c' = Lib.discharge_con c in
if c==c' then Some ref else Some (EvalConstRef c')
- | _ -> Some ref
+ | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref
let discharge_strategy (_,(local,obj)) =
if local then None else
@@ -97,26 +93,22 @@ let (inStrategy,outStrategy) =
load_function = (fun _ (_,obj) -> cache_strategy obj);
subst_function = subst_strategy;
discharge_function = discharge_strategy;
- classify_function = classify_strategy;
- export_function = export_strategy }
+ classify_function = classify_strategy }
let set_strategy local str =
Lib.add_anonymous_leaf (inStrategy (local,str))
-let _ =
- Summary.declare_summary "Transparent constants and variables"
- { Summary.freeze_function = Conv_oracle.freeze;
- Summary.unfreeze_function = Conv_oracle.unfreeze;
- Summary.init_function = Conv_oracle.init;
- Summary.survive_module = false;
- Summary.survive_section = false }
+let _ = declare_summary "Transparent constants and variables"
+ { freeze_function = Conv_oracle.freeze;
+ unfreeze_function = Conv_oracle.unfreeze;
+ init_function = Conv_oracle.init }
(* Generic reduction: reduction functions used in reduction tactics *)
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
-
+type red_expr =
+ (constr, evaluable_global_reference, constr_pattern) red_expr_gen
let make_flag_constant = function
| EvalVarRef id -> fVAR id
@@ -141,17 +133,34 @@ let make_flag f =
f.rConst red
in red
-let is_reference c =
- try let _ref = global_of_constr c in true with _ -> false
+let is_reference = function PRef _ | PVar _ -> true | _ -> false
+
+(* table of custom reductino fonctions, not synchronized,
+ filled via ML calls to [declare_reduction] *)
+let reduction_tab = ref Stringmap.empty
+(* table of custom reduction expressions, synchronized,
+ filled by command Declare Reduction *)
let red_expr_tab = ref Stringmap.empty
-let declare_red_expr s f =
- try
- let _ = Stringmap.find s !red_expr_tab in
- error ("There is already a reduction expression of name "^s)
- with Not_found ->
- red_expr_tab := Stringmap.add s f !red_expr_tab
+let declare_reduction s f =
+ if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+ then error ("There is already a reduction expression of name "^s)
+ else reduction_tab := Stringmap.add s f !reduction_tab
+
+let check_custom = function
+ | ExtraRedExpr s ->
+ if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab)
+ then error ("Reference to undefined reduction expression "^s)
+ |_ -> ()
+
+let decl_red_expr s e =
+ if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+ then error ("There is already a reduction expression of name "^s)
+ else begin
+ check_custom e;
+ red_expr_tab := Stringmap.add s e !red_expr_tab
+ end
let out_arg = function
| ArgVar _ -> anomaly "Unevaluated or_var variable"
@@ -160,13 +169,14 @@ let out_arg = function
let out_with_occurrences ((b,l),c) =
((b,List.map out_arg l), c)
-let reduction_of_red_expr = function
- | Red internal ->
- if internal then (try_red_product,DEFAULTcast)
+let rec reduction_of_red_expr = function
+ | Red internal ->
+ if internal then (try_red_product,DEFAULTcast)
else (red_product,DEFAULTcast)
| Hnf -> (hnf_constr,DEFAULTcast)
| Simpl (Some (_,c as lp)) ->
- (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
+ (contextually (is_reference c) (out_with_occurrences lp)
+ (fun _ -> simpl),DEFAULTcast)
| Simpl None -> (simpl,DEFAULTcast)
| Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
| Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
@@ -174,6 +184,49 @@ let reduction_of_red_expr = function
| Fold cl -> (fold_commands cl,DEFAULTcast)
| Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
| ExtraRedExpr s ->
- (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
- with Not_found -> error("unknown user-defined reduction \""^s^"\""))
+ (try (Stringmap.find s !reduction_tab,DEFAULTcast)
+ with Not_found ->
+ (try reduction_of_red_expr (Stringmap.find s !red_expr_tab)
+ with Not_found ->
+ error("unknown user-defined reduction \""^s^"\"")))
| CbvVm -> (cbv_vm ,VMcast)
+
+
+let subst_flags subs flags =
+ { flags with rConst = List.map subs flags.rConst }
+
+let subst_occs subs (occ,e) = (occ,subs e)
+
+let subst_gen_red_expr subs_a subs_b subs_c = function
+ | Fold l -> Fold (List.map subs_a l)
+ | Pattern occs_l -> Pattern (List.map (subst_occs subs_a) occs_l)
+ | Simpl occs_o -> Simpl (Option.map (subst_occs subs_c) occs_o)
+ | Unfold occs_l -> Unfold (List.map (subst_occs subs_b) occs_l)
+ | Cbv flags -> Cbv (subst_flags subs_b flags)
+ | Lazy flags -> Lazy (subst_flags subs_b flags)
+ | e -> e
+
+let subst_red_expr subs e =
+ subst_gen_red_expr
+ (Mod_subst.subst_mps subs)
+ (Mod_subst.subst_evaluable_reference subs)
+ (Pattern.subst_pattern subs)
+ e
+
+let (inReduction,_) =
+ declare_object
+ {(default_object "REDUCTION") with
+ cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
+ load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e);
+ subst_function =
+ (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
+ classify_function =
+ (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
+
+let declare_red_expr locality s expr =
+ Lib.add_anonymous_leaf (inReduction (locality,s,expr))
+
+let _ = declare_summary "Declare Reduction"
+ { freeze_function = (fun () -> !red_expr_tab);
+ unfreeze_function = ((:=) red_expr_tab);
+ init_function = (fun () -> red_expr_tab := Stringmap.empty) }
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d72ff182..03d97ce3 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,24 +6,31 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: redexpr.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id$ i*)
open Names
open Term
open Closure
+open Pattern
open Rawterm
open Reductionops
open Termops
-
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
+type red_expr =
+ (constr, evaluable_global_reference, constr_pattern) red_expr_gen
val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
(* [true] if we should use the vm to verify the reduction *)
-val declare_red_expr : string -> reduction_function -> unit
+(* Adding a custom reduction (function to be use at the ML level)
+ NB: the effect is permanent. *)
+val declare_reduction : string -> reduction_function -> unit
+
+(* Adding a custom reduction (function to be called a vernac command).
+ The boolean flag is the locality. *)
+val declare_red_expr : bool -> string -> red_expr -> unit
(* Opaque and Transparent commands. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7ce256bf..a320b67c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
open Pp
open Util
@@ -49,23 +49,20 @@ let descend n p =
| None -> error "It is a leaf."
| Some(r,pfl) ->
if List.length pfl >= n then
- (match list_chop (n-1) pfl with
+ (match list_chop (n-1) pfl with
| left,(wanted::right) ->
(wanted,
(fun pfl' ->
- if (List.length pfl' = 1)
- & (List.hd pfl').goal = wanted.goal
- then
- let pf' = List.hd pfl' in
- let spfl = left@(pf'::right) in
- let newstatus = and_status (List.map pf_status spfl) in
- { p with
- open_subgoals = newstatus;
- ref = Some(r,spfl) }
- else
- error "descend: validation"))
+ if false (* debug *) then assert
+ (List.length pfl'=1 & (List.hd pfl').goal = wanted.goal);
+ let pf' = List.hd pfl' in
+ let spfl = left@(pf'::right) in
+ let newstatus = and_status (List.map pf_status spfl) in
+ { p with
+ open_subgoals = newstatus;
+ ref = Some(r,spfl) }))
| _ -> assert false)
- else
+ else
error "Too few subproofs"
@@ -75,28 +72,28 @@ let descend n p =
(vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ]
*)
-let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
+let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
(l : proof_tree list) =
match nl with
| [] -> []
| h::t ->
- let m,l = list_chop h l in
+ let m,l = list_chop h l in
(List.hd fl m) :: (mapshape t (List.tl fl) l)
(* [frontier : proof_tree -> goal list * validation]
given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
- to be solved to complete the proof, and [v] is the corresponding
+ to be solved to complete the proof, and [v] is the corresponding
validation *)
-
+
let rec frontier p =
match p.ref with
- | None ->
+ | None ->
([p.goal],
- (fun lp' ->
+ (fun lp' ->
let p' = List.hd lp' in
- if Evd.eq_evar_info p'.goal p.goal then
+ if Evd.eq_evar_info p'.goal p.goal then
p'
- else
+ else
errorlabstrm "Refiner.frontier"
(str"frontier was handed back a ill-formed proof.")))
| Some(r,pfl) ->
@@ -118,14 +115,14 @@ let set_solve_hook = (:=) solve_hook
let rec frontier_map_rec f n p =
if n < 1 || n > p.open_subgoals then p else
match p.ref with
- | None ->
+ | None ->
let p' = f p in
if Evd.eq_evar_info p'.goal p.goal then
begin
!solve_hook p';
p'
end
- else
+ else
errorlabstrm "Refiner.frontier_map"
(str"frontier_map was handed back a ill-formed proof.")
| Some(r,pfl) ->
@@ -142,20 +139,20 @@ let frontier_map f n p =
let nmax = p.open_subgoals in
let n = if n < 0 then nmax + n + 1 else n in
if n < 1 || n > nmax then
- errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
+ errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
frontier_map_rec f n p
let rec frontier_mapi_rec f i p =
if p.open_subgoals = 0 then p else
match p.ref with
- | None ->
+ | None ->
let p' = f i p in
if Evd.eq_evar_info p'.goal p.goal then
begin
!solve_hook p';
p'
end
- else
+ else
errorlabstrm "Refiner.frontier_mapi"
(str"frontier_mapi was handed back a ill-formed proof.")
| Some(r,pfl) ->
@@ -164,7 +161,7 @@ let rec frontier_mapi_rec f i p =
(fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
(i,[]) pfl in
let pfl' = List.rev rpfl' in
- { p with
+ { p with
open_subgoals = and_status (List.map pf_status pfl');
ref = Some(r,pfl')}
@@ -179,7 +176,7 @@ let rec nb_unsolved_goals pf = pf.open_subgoals
(* leaf g is the canonical incomplete proof of a goal g *)
-let leaf g =
+let leaf g =
{ open_subgoals = 1;
goal = g;
ref = None }
@@ -200,20 +197,20 @@ let abstract_operation syntax semantics gls =
ref = Some(Nested(syntax,hidden_proof),spfl)})
let abstract_tactic_expr ?(dflt=false) te tacfun gls =
- abstract_operation (Tactic(te,dflt)) 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 =
+let abstract_extended_tactic ?(dflt=false) s args =
abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
let refiner = function
| Prim pr as r ->
let prim_fun = prim_refiner pr in
(fun goal_sigma ->
- let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
+ let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
({it=sgl; sigma = sigma'},
(fun spfl ->
assert (check_subproof_connection sgl spfl);
@@ -222,15 +219,15 @@ let refiner = function
ref = Some(r,spfl) })))
- | Nested (_,_) | Decl_proof _ ->
+ | Nested (_,_) | Decl_proof _ ->
failwith "Refiner: should not occur"
-
+
(* Daimon is a canonical unfinished proof *)
- | Daimon ->
- fun gls ->
- ({it=[];sigma=gls.sigma},
- fun spfl ->
+ | Daimon ->
+ fun gls ->
+ ({it=[];sigma=gls.sigma},
+ fun spfl ->
assert (spfl=[]);
{ open_subgoals = 0;
goal = gls.it;
@@ -253,10 +250,10 @@ let norm_evar_proof sigma pf =
Their proof should be completed in order to complete the initial proof *)
let extract_open_proof sigma pf =
- let next_meta =
+ let next_meta =
let meta_cnt = ref 0 in
let rec f () =
- incr meta_cnt;
+ incr meta_cnt;
if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
else !meta_cnt
in f
@@ -264,14 +261,14 @@ let extract_open_proof sigma pf =
let open_obligations = ref [] in
let rec proof_extractor vl = function
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
-
+
| {ref=Some(Nested(_,hidden_proof),spfl)} ->
let sgl,v = frontier hidden_proof in
let flat_proof = v spfl in
proof_extractor vl flat_proof
-
+
| {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
-
+
| {ref=(None|Some(Daimon,[]));goal=goal} ->
let visible_rels =
map_succeed
@@ -290,13 +287,13 @@ let extract_open_proof sigma pf =
let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
let meta = next_meta () in
open_obligations := (meta,abs_concl):: !open_obligations;
- applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
-
+ applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
+
| _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
in
let pfterm = proof_extractor [] pf in
(pfterm, List.rev !open_obligations)
-
+
(*********************)
(* Tacticals *)
(*********************)
@@ -304,7 +301,7 @@ let extract_open_proof sigma pf =
(* unTAC : tactic -> goal sigma -> proof sigma *)
let unTAC tac g =
- let (gl_sigma,v) = tac g in
+ let (gl_sigma,v) = tac g in
{ it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
let unpackage glsig = (ref (glsig.sigma)),glsig.it
@@ -312,8 +309,8 @@ let unpackage glsig = (ref (glsig.sigma)),glsig.it
let repackage r v = {it=v;sigma = !r}
let apply_sig_tac r tac g =
- check_for_interrupt (); (* Breakpoint *)
- let glsigma,v = tac (repackage r g) in
+ check_for_interrupt (); (* Breakpoint *)
+ let glsigma,v = tac (repackage r g) in
r := glsigma.sigma;
(glsigma.it,v)
@@ -331,17 +328,19 @@ let tclNORMEVAR = norm_evar_tac
let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
(* the message printing identity tactic *)
-let tclIDTAC_MESSAGE s gls =
+let tclIDTAC_MESSAGE s gls =
msg (hov 0 s); tclIDTAC gls
(* General failure tactic *)
let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds
+exception FailError of int * std_ppcmds Lazy.t
(* The Fail tactic *)
-let tclFAIL lvl s g = raise (FailError (lvl,s))
+let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
+
+let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
let start_tac gls =
let (sigr,g) = unpackage gls in
@@ -357,7 +356,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
let gll,pl =
List.split
- (list_map_i (fun i ->
+ (list_map_i (fun i ->
apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
0 gs) in
(sigr, List.flatten gll,
@@ -391,7 +390,7 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
thensf_tac
(Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
subgoals
- else non_existent_goal k
+ else non_existent_goal k
(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
@@ -448,21 +447,22 @@ let rec tclTHENLIST = function
[] -> tclIDTAC
| t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
-
-
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+let tclMAP tacfun l =
+ List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
(* various progress criterions *)
-let same_goal gl subgoal =
+let same_goal gl subgoal =
eq_constr (conclusion subgoal) (conclusion gl) &&
eq_named_context_val (hypotheses subgoal) (hypotheses gl)
let weak_progress gls ptree =
- (List.length gls.it <> 1) ||
+ (List.length gls.it <> 1) ||
(not (same_goal (List.hd gls.it) ptree.it))
let progress gls ptree =
- (not (eq_evar_map ptree.sigma gls.sigma)) ||
+ (progress_evar_map ptree.sigma gls.sigma) ||
(weak_progress gls ptree)
@@ -473,7 +473,7 @@ let tclPROGRESS tac ptree =
if progress (fst rslt) ptree then rslt
else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
-(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
+(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
if tac leaves the goal unchanged, possibly modifying sigma *)
let tclWEAK_PROGRESS tac ptree =
let rslt = tac ptree in
@@ -487,14 +487,14 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
let rslt = tac goal in
let gls = (fst rslt).it in
if List.exists (same_goal goal.it) gls
- then errorlabstrm "Refiner.tclNOTSAMEGOAL"
+ then errorlabstrm "Refiner.tclNOTSAMEGOAL"
(str"Tactic generated a subgoal identical to the original goal.")
else rslt
let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
- | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
+ | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
| Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
check_for_interrupt ()
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
@@ -507,18 +507,18 @@ let catch_failerror e =
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
let tclORELSE0 t1 t2 g =
- try
+ try
t1 g
with (* Breakpoint *)
| e -> catch_failerror e; t2 g
-(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
+(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
then applies t2 *)
let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
(* applies t1;t2then if t1 succeeds or t2else if t1 fails
t2* are called in terminal position (unless t1 produces more than
- 1 subgoal!) *)
+ 1 subgoal!) *)
let tclORELSE_THEN t1 t2then t2else gls =
match
try Some(tclPROGRESS t1 gls)
@@ -526,7 +526,7 @@ let tclORELSE_THEN t1 t2then t2else gls =
with
| None -> t2else gls
| Some (sgl,v) ->
- let (sigr,gl) = unpackage sgl in
+ let (sigr,gl) = unpackage sgl in
finish_tac (then_tac t2then (sigr,gl,v))
(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
@@ -546,16 +546,16 @@ let ite_gen tcal tac_if continue tac_else gl=
let result=tac_if gl in
success:=true;result in
let tac_else0 e gl=
- if !success then
- raise e
- else
+ if !success then
+ raise e
+ else
tac_else gl in
- try
+ try
tcal tac_if0 continue gl
with (* Breakpoint *)
| e -> catch_failerror e; tac_else0 e gl
-(* Try the first tactic and, if it succeeds, continue with
+(* Try the first tactic and, if it succeeds, continue with
the second one, and if it fails, use the third one *)
let tclIFTHENELSE=ite_gen tclTHEN
@@ -566,7 +566,7 @@ let tclIFTHENSELSE=ite_gen tclTHENS
let tclIFTHENSVELSE=ite_gen tclTHENSV
-let tclIFTHENTRYELSEMUST tac1 tac2 gl =
+let tclIFTHENTRYELSEMUST tac1 tac2 gl =
tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
(* Fails if a tactic did not solve the goal *)
@@ -575,17 +575,17 @@ let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
(* Try the first thats solves the current goal *)
let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
-
+
(* Iteration tacticals *)
-let tclDO n t =
- let rec dorec k =
+let tclDO n t =
+ let rec dorec k =
if k < 0 then errorlabstrm "Refiner.tclDO"
(str"Wrong argument : Do needs a positive integer.");
if k = 0 then tclIDTAC
else if k = 1 then t else (tclTHEN t (dorec (k-1)))
- in
- dorec n
+ in
+ dorec n
(* Beware: call by need of CAML, g is needed *)
@@ -612,52 +612,52 @@ let tclIDTAC_list gls = (gls, fun x -> x)
(* first_goal : goal list sigma -> goal sigma *)
-let first_goal gls =
- let gl = gls.it and sig_0 = gls.sigma in
- if gl = [] then error "first_goal";
+let first_goal gls =
+ let gl = gls.it and sig_0 = gls.sigma in
+ if gl = [] then error "first_goal";
{ it = List.hd gl; sigma = sig_0 }
(* goal_goal_list : goal sigma -> goal list sigma *)
-let goal_goal_list gls =
+let goal_goal_list gls =
let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
-let apply_tac_list tac glls =
+let apply_tac_list tac glls =
let (sigr,lg) = unpackage glls in
match lg with
| (g1::rest) ->
let (gl,p) = apply_sig_tac sigr tac g1 in
- let n = List.length gl in
- (repackage sigr (gl@rest),
+ let n = List.length gl in
+ (repackage sigr (gl@rest),
fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
| _ -> error "apply_tac_list"
-
-let then_tactic_list tacl1 tacl2 glls =
+
+let then_tactic_list tacl1 tacl2 glls =
let (glls1,pl1) = tacl1 glls in
let (glls2,pl2) = tacl2 glls1 in
(glls2, compose pl1 pl2)
(* Transform a tactic_list into a tactic *)
-let tactic_list_tactic tac gls =
+let tactic_list_tactic tac gls =
let (glres,vl) = tac (goal_goal_list gls) in
(glres, compose idtac_valid vl)
-(* The type of proof-trees state and a few utilities
+(* The type of proof-trees state and a few utilities
A proof-tree state is built from a proof-tree, a set of global
constraints, and a stack which allows to navigate inside the
proof-tree remembering how to rebuild the global proof-tree
possibly after modification of one of the focused children proof-tree.
- The number in the stack corresponds to
+ The number in the stack corresponds to
either the selected subtree and the validation is a function from a
proof-tree list consisting only of one proof-tree to the global
- proof-tree
+ proof-tree
or -1 when the move is done behind a registered tactic in which
- case the validation corresponds to a constant function giving back
+ case the validation corresponds to a constant function giving back
the original proof-tree. *)
type pftreestate = {
@@ -666,11 +666,11 @@ type pftreestate = {
tstack : (int * validation) list }
let proof_of_pftreestate pts = pts.tpf
-let is_top_pftreestate pts = pts.tstack = []
+let is_top_pftreestate pts = pts.tstack = []
let cursor_of_pftreestate pts = List.map fst pts.tstack
let evc_of_pftreestate pts = pts.tpfsigma
-let top_goal_of_pftreestate pts =
+let top_goal_of_pftreestate pts =
{ it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
let nth_goal_of_pftreestate n pts =
@@ -678,7 +678,7 @@ let nth_goal_of_pftreestate n pts =
try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
with Invalid_argument _ | Failure _ -> non_existent_goal n
-let traverse n pts = match n with
+let traverse n pts = match n with
| 0 -> (* go to the parent *)
(match pts.tstack with
| [] -> error "traverse: no ancestors"
@@ -691,13 +691,13 @@ let traverse n pts = match n with
| -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
(match pts.tpf.ref with
| Some (Nested (_,spf),_) ->
- let v = (fun pfl -> pts.tpf) in
+ let v = (fun pfl -> pts.tpf) in
{ tpf = spf;
tstack = (-1,v)::pts.tstack;
tpfsigma = pts.tpfsigma }
| _ -> error "traverse: not a tactic-node")
| n -> (* when n>0, go to the nth child *)
- let (npf,v) = descend n pts.tpf in
+ let (npf,v) = descend n pts.tpf in
{ tpf = npf;
tpfsigma = pts.tpfsigma;
tstack = (n,v):: pts.tstack }
@@ -723,9 +723,9 @@ let map_pftreestate f pts =
(* solve the nth subgoal with tactic tac *)
let solve_nth_pftreestate n tac =
- map_pftreestate
+ map_pftreestate
(fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
-
+
let solve_pftreestate = solve_nth_pftreestate 1
(* This function implements a poor man's undo at the current goal.
@@ -771,78 +771,78 @@ let extract_pftreestate pts =
(* Focus on the first leaf proof in a proof-tree state *)
let rec first_unproven pts =
- let pf = (proof_of_pftreestate pts) in
+ let pf = (proof_of_pftreestate pts) in
if is_complete_proof pf then
errorlabstrm "first_unproven" (str"No unproven subgoals");
if is_leaf_proof pf then
pts
else
let childnum =
- list_try_find_i
- (fun n pf ->
+ list_try_find_i
+ (fun n pf ->
if not(is_complete_proof pf) then n else failwith "caught")
1 (children_of_proof pf)
- in
+ in
first_unproven (traverse childnum pts)
(* Focus on the last leaf proof in a proof-tree state *)
let rec last_unproven pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
if is_complete_proof pf then
errorlabstrm "last_unproven" (str"No unproven subgoals");
if is_leaf_proof pf then
pts
- else
+ else
let children = (children_of_proof pf) in
let nchilds = List.length children in
let childnum =
- list_try_find_i
+ list_try_find_i
(fun n pf ->
if not(is_complete_proof pf) then n else failwith "caught")
1 (List.rev children)
- in
+ in
last_unproven (traverse (nchilds-childnum+1) pts)
-
+
let rec nth_unproven n pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
if is_complete_proof pf then
errorlabstrm "nth_unproven" (str"No unproven subgoals");
if is_leaf_proof pf then
- if n = 1 then
- pts
+ if n = 1 then
+ pts
else
errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
- else
+ else
let children = children_of_proof pf in
let rec process i k = function
- | [] ->
+ | [] ->
errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
- | pf1::rest ->
- let k1 = nb_unsolved_goals pf1 in
- if k1 < k then
+ | pf1::rest ->
+ let k1 = nb_unsolved_goals pf1 in
+ if k1 < k then
process (i+1) (k-k1) rest
- else
+ else
nth_unproven k (traverse i pts)
- in
+ in
process 1 n children
let rec node_prev_unproven loc pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
match cursor_of_pftreestate pts with
| [] -> last_unproven pts
| n::l ->
if is_complete_proof pf or loc = 1 then
node_prev_unproven n (traverse 0 pts)
- else
+ else
let child = List.nth (children_of_proof pf) (loc - 2) in
if is_complete_proof child then
node_prev_unproven (loc - 1) pts
- else
+ else
first_unproven (traverse (loc - 1) pts)
let rec node_next_unproven loc pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
match cursor_of_pftreestate pts with
| [] -> first_unproven pts
| n::l ->
@@ -851,35 +851,35 @@ let rec node_next_unproven loc pts =
node_next_unproven n (traverse 0 pts)
else if is_complete_proof (List.nth (children_of_proof pf) loc) then
node_next_unproven (loc + 1) pts
- else
+ else
last_unproven(traverse (loc + 1) pts)
let next_unproven pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
if is_leaf_proof pf then
match cursor_of_pftreestate pts with
| [] -> error "next_unproven"
| n::_ -> node_next_unproven n (traverse 0 pts)
- else
+ else
node_next_unproven (List.length (children_of_proof pf)) pts
let prev_unproven pts =
- let pf = proof_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
if is_leaf_proof pf then
match cursor_of_pftreestate pts with
| [] -> error "prev_unproven"
| n::_ -> node_prev_unproven n (traverse 0 pts)
- else
+ else
node_prev_unproven 1 pts
-let rec top_of_tree pts =
+let rec top_of_tree pts =
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
let change_rule f pts =
let mark_top _ pt =
match pt.ref with
- Some (oldrule,l) ->
+ Some (oldrule,l) ->
{pt with ref=Some (f oldrule,l)}
| _ -> invalid_arg "change_rule" in
map_pftreestate mark_top pts
@@ -889,21 +889,21 @@ let match_rule p pts =
Some (r,_) -> p r
| None -> false
-let rec up_until_matching_rule p pts =
- if is_top_pftreestate pts then
+let rec up_until_matching_rule p pts =
+ if is_top_pftreestate pts then
raise Not_found
else
let one_up = traverse 0 pts in
- if match_rule p one_up then
+ if match_rule p one_up then
pts
else
up_until_matching_rule p one_up
-let rec up_to_matching_rule p pts =
- if match_rule p pts then
+let rec up_to_matching_rule p pts =
+ if match_rule p pts then
pts
else
- if is_top_pftreestate pts then
+ if is_top_pftreestate pts then
raise Not_found
else
let one_up = traverse 0 pts in
@@ -917,14 +917,50 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
let pp_info = ref (fun _ _ _ -> assert false)
let set_info_printer f = pp_info := f
-let tclINFO (tac : tactic) gls =
- let (sgl,v) as res = tac gls in
- begin try
+let tclINFO (tac : tactic) gls =
+ let (sgl,v) as res = tac gls in
+ begin try
let pf = v (List.map leaf (sig_it sgl)) in
let sign = named_context_of_val (sig_it gls).evar_hyps in
msgnl (hov 0 (str" == " ++
!pp_info (project gls) sign pf))
- with e when catchable_exception e ->
+ with e when catchable_exception e ->
msgnl (hov 0 (str "Info failed to apply validation"))
end;
res
+
+let pp_proof = ref (fun _ _ _ -> assert false)
+let set_proof_printer f = pp_proof := f
+
+let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
+ (if stack = []
+ then str "Rooted proof tree is:"
+ else (str "Proof tree at occurrence [" ++
+ prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n)
+ (List.rev stack) ++ str "] is:")) ++ fnl() ++
+ !pp_proof sigma (Global.named_context()) pf ++
+ Evd.pr_evar_map sigma
+
+(* Check that holes in arguments have been resolved *)
+
+let check_evars env sigma evm gl =
+ let origsigma = gl.sigma in
+ let rest =
+ Evd.fold (fun ev evi acc ->
+ if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev)
+ then Evd.add acc ev evi else acc)
+ evm Evd.empty
+ in
+ if rest <> Evd.empty then
+ let (evk,evi) = List.hd (Evd.to_list rest) in
+ let (loc,k) = evar_source evk rest in
+ let evi = Evarutil.nf_evar_info sigma evi in
+ Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
+
+let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
+ if sigma == project gl then tac c gl
+ else
+ let res = tclTHEN (tclEVARS sigma) (tac c) gl in
+ if not accept_unresolved_holes then
+ check_evars (pf_env gl) (fst res).sigma sigma gl;
+ res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index a6ba3af5..e853c12b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: refiner.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Term
@@ -80,6 +80,9 @@ val tclTHEN : tactic -> tactic -> tactic
convenient than [tclTHEN] when [n] is large *)
val tclTHENLIST : tactic list -> tactic
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+val tclMAP : ('a -> tactic) -> 'a list -> tactic
+
(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
@@ -131,7 +134,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENFIRSTn : tactic -> tactic array -> tactic
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds
+exception FailError of int * Pp.std_ppcmds Lazy.t
(* Takes an exception and either raise it at the next
level or do nothing. *)
@@ -148,6 +151,7 @@ val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.std_ppcmds -> tactic
+val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
@@ -155,14 +159,14 @@ val tclNOTSAMEGOAL : tactic -> tactic
val tclINFO : tactic -> tactic
(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
- if it succeeds, applies [tac2] to the resulting subgoals,
+ if it succeeds, applies [tac2] to the resulting subgoals,
and if not applies [tac3] to the initial goal [gls] *)
val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
- has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
+ has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
Equivalent to [(tac1;try tac2)||tac2] *)
val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
@@ -181,6 +185,11 @@ val then_tactic_list : tactic_list -> tactic_list -> tactic_list
val tactic_list_tactic : tactic_list -> tactic
val goal_goal_list : 'a sigma -> 'a list sigma
+(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
+ may have unresolved holes; if [solve_holes] these holes must be
+ resolved after application of the tactic; [sigma] must be an
+ extension of the sigma of the goal *)
+val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
(*s Functions for handling the state of the proof editor. *)
@@ -195,7 +204,7 @@ val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
-val map_pftreestate :
+val map_pftreestate :
(evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
@@ -206,7 +215,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
@@ -217,12 +226,12 @@ val next_unproven : pftreestate -> pftreestate
val prev_unproven : pftreestate -> pftreestate
val top_of_tree : pftreestate -> pftreestate
val match_rule : (rule -> bool) -> pftreestate -> bool
-val up_until_matching_rule : (rule -> bool) ->
+val up_until_matching_rule : (rule -> bool) ->
pftreestate -> pftreestate
-val up_to_matching_rule : (rule -> bool) ->
+val up_to_matching_rule : (rule -> bool) ->
pftreestate -> pftreestate
val change_rule : (rule -> rule) -> pftreestate -> pftreestate
-val change_constraints_pftreestate
+val change_constraints_pftreestate
: evar_map -> pftreestate -> pftreestate
@@ -233,3 +242,6 @@ open Pp
(*i*)
val set_info_printer :
(evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
+val set_proof_printer :
+ (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
+val print_pftreestate : pftreestate -> Pp.std_ppcmds
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 66136afa..b56e5184 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 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id$ i*)
open Names
open Topconstr
@@ -51,12 +51,12 @@ let make_red_flag =
if red.rConst <> [] & not red.rDelta then
error
"Cannot set both constants to unfold and constants not to unfold";
- add_flag
+ add_flag
{ red with rConst = list_union red.rConst l; rDelta = true }
lf
in
add_flag
- {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
+ {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
@@ -85,7 +85,7 @@ type inversion_kind =
| FullInversionClear
type ('c,'id) inversion_strength =
- | NonDepInversion of
+ | NonDepInversion of
inversion_kind * 'id list * intro_pattern_expr located option
| DepInversion of
inversion_kind * 'c option * intro_pattern_expr located option
@@ -98,30 +98,31 @@ type 'id message_token =
| MsgInt of int
| MsgIdent of 'id
-type 'id gsimple_clause = ('id raw_hyp_location) option
(* onhyps:
[None] means *on every hypothesis*
[Some l] means on hypothesis belonging to l *)
type 'id gclause =
{ onhyps : 'id raw_hyp_location list option;
- concl_occs : bool * int or_var list }
+ concl_occs : occurrences_expr }
let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
-let simple_clause_of = function
+let goal_location_of = function
| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
Some scl
| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
None
| _ ->
- error "not a simple clause (one hypothesis or conclusion)"
+ error "Not a simple \"in\" clause (one hypothesis or the 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 'constr induction_clause =
+ ('constr with_bindings induction_arg list * 'constr with_bindings option *
+ (intro_pattern_expr located option * intro_pattern_expr located option))
-type multi =
+type ('constr,'id) induction_clause_list =
+ 'constr induction_clause list * 'id gclause option
+
+type multi =
| Precisely of int
| UpTo of int
| RepeatStar
@@ -142,7 +143,7 @@ type ('a,'t) match_rule =
| Pat of 'a match_context_hyps list * 'a match_pattern * 't
| All of 't
-type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
+type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of intro_pattern_expr located list
| TacIntrosUntil of quantified_hypothesis
@@ -151,15 +152,15 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacExact of 'constr
| TacExactNoCheck of 'constr
| TacVmCastNoCheck of 'constr
- | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
+ | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
('id * intro_pattern_expr located option) option
- | TacElim of evars_flag * 'constr with_bindings *
+ | TacElim of evars_flag * 'constr with_bindings *
'constr with_bindings option
| TacElimType of 'constr
| TacCase of evars_flag * 'constr with_bindings
| TacCaseType of 'constr
| TacFix of identifier option * int
- | TacMutualFix of hidden_flag * identifier * int * (identifier * int *
+ | TacMutualFix of hidden_flag * identifier * int * (identifier * int *
'constr) list
| TacCofix of identifier option
| TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
@@ -171,7 +172,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Derived basic tactics *)
| TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
- | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause list
+ | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause_list
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
| TacDecomposeAnd of 'constr
| TacDecomposeOr of 'constr
@@ -198,86 +199,87 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Constructors *)
| TacLeft of evars_flag * 'constr bindings
| TacRight of evars_flag * 'constr bindings
- | TacSplit of evars_flag * split_flag * 'constr bindings
+ | TacSplit of evars_flag * split_flag * 'constr bindings list
| TacAnyConstructor of evars_flag * 'tac option
| TacConstructor of evars_flag * int or_metaid * 'constr bindings
(* Conversion *)
- | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
- | TacChange of 'constr with_occurrences option * 'constr * 'id gclause
+ | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
+ | TacChange of 'pat option * 'constr * 'id gclause
(* Equivalence relations *)
| TacReflexivity
| TacSymmetry of 'id gclause
- | TacTransitivity of 'constr
+ | TacTransitivity of 'constr option
(* Equality and inversion *)
- | TacRewrite of
+ | TacRewrite of
evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
| TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
-
+
(* For ML extensions *)
- | TacExtend of loc * string * 'constr generic_argument list
+ | TacExtend of loc * string * 'lev generic_argument list
(* For syntax extensions *)
| TacAlias of loc * string *
- (identifier * 'constr generic_argument) list
+ (identifier * 'lev generic_argument) list
* (dir_path * glob_tactic_expr)
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
- | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
- | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
- ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array *
- ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
- ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array
- | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
- ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
- | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
- | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
- | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
+ | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr
+ | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array
+ | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
+ | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
+ | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list
+ | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option
| TacId of 'id message_token list
| TacFail of int or_var * 'id message_token list
- | 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
- | 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
+ | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
+ | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
+ | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast
+ | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
- identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast =
+ identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
(* These are the possible arguments of a tactic definition *)
-and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
| TacDynamic of loc * Dyn.t
| TacVoid
| MetaIdArg of loc * bool * string
- | ConstrMayEval of ('constr,'cst) may_eval
+ | ConstrMayEval of ('constr,'cst,'pat) may_eval
| IntroPattern of intro_pattern_expr located
| Reference of 'ref
| Integer of int
| TacCall of loc *
- 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
- | TacExternal of loc * string * string *
- ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+ 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
+ | TacExternal of loc * string * string *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list
| TacFreshId of string or_var list
| Tacexp of 'tac
(* Globalized tactics *)
and glob_tactic_expr =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
identifier located,
- glob_tactic_expr) gen_tactic_expr
+ glob_tactic_expr,
+ glevel) gen_tactic_expr
type raw_tactic_expr =
(constr_expr,
@@ -286,7 +288,8 @@ type raw_tactic_expr =
reference or_by_notation,
reference,
identifier located or_metaid,
- raw_tactic_expr) gen_tactic_expr
+ raw_tactic_expr,
+ rlevel) gen_tactic_expr
type raw_atomic_tactic_expr =
(constr_expr, (* constr *)
@@ -295,7 +298,8 @@ type raw_atomic_tactic_expr =
reference or_by_notation, (* inductive *)
reference, (* ltac reference *)
identifier located or_metaid, (* identifier *)
- raw_tactic_expr) gen_atomic_tactic_expr
+ raw_tactic_expr,
+ rlevel) gen_atomic_tactic_expr
type raw_tactic_arg =
(constr_expr,
@@ -304,36 +308,41 @@ type raw_tactic_arg =
reference or_by_notation,
reference,
identifier located or_metaid,
- raw_tactic_expr) gen_tactic_arg
+ raw_tactic_expr,
+ rlevel) gen_tactic_arg
-type raw_generic_argument = constr_expr generic_argument
+type raw_generic_argument = rlevel generic_argument
-type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
+type raw_red_expr =
+ (constr_expr, reference or_by_notation, constr_expr) red_expr_gen
type glob_atomic_tactic_expr =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
identifier located,
- glob_tactic_expr) gen_atomic_tactic_expr
+ glob_tactic_expr,
+ glevel) gen_atomic_tactic_expr
type glob_tactic_arg =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
identifier located,
- glob_tactic_expr) gen_tactic_arg
+ glob_tactic_expr,
+ glevel) gen_tactic_arg
-type glob_generic_argument = rawconstr_and_expr generic_argument
+type glob_generic_argument = glevel generic_argument
type glob_red_expr =
- (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
+ (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern)
+ red_expr_gen
-type typed_generic_argument = Evd.open_constr generic_argument
+type typed_generic_argument = tlevel generic_argument
type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b740baa8..9e35abfc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
open Names
-open Nameops
+open Namegen
open Sign
open Term
open Termops
@@ -55,10 +55,10 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
let pf_last_hyp gl = List.hd (pf_hyps gl)
-let pf_get_hyp gls id =
- try
+let pf_get_hyp gls id =
+ try
Sign.lookup_named id (pf_hyps gls)
- with Not_found ->
+ with Not_found ->
error ("No such hypothesis: " ^ (string_of_id id))
let pf_get_hyp_typ gls id =
@@ -67,7 +67,7 @@ let pf_get_hyp_typ gls id =
let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
-let pf_get_new_id id gls =
+let pf_get_new_id id gls =
next_ident_away id (pf_ids_of_hyps gls)
let pf_get_new_ids ids gls =
@@ -77,19 +77,19 @@ let pf_get_new_ids ids gls =
ids []
let pf_interp_constr gls c =
- let evc = project gls in
+ let evc = project gls in
Constrintern.interp_constr evc (pf_env gls) c
let pf_interp_type gls c =
- let evc = project gls in
+ let evc = project gls in
Constrintern.interp_type evc (pf_env gls) c
let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
let pf_parse_const gls = compose (pf_global gls) id_of_string
-let pf_reduction_of_red_expr gls re c =
- (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
+let pf_reduction_of_red_expr gls re c =
+ (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
let pf_apply f gls = f (pf_env gls) (project gls)
let pf_reduce = pf_apply
@@ -98,7 +98,7 @@ let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota
let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack
let pf_hnf_constr = pf_reduce hnf_constr
let pf_red_product = pf_reduce red_product
-let pf_nf = pf_reduce nf
+let pf_nf = pf_reduce simpl
let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota)
let pf_compute = pf_reduce compute
let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds)
@@ -111,11 +111,14 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value env)
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
+let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
-let pf_check_type gls c1 c2 =
+let pf_check_type gls c1 c2 =
ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
+let pf_is_matching = pf_apply Matching.is_matching_conv
+let pf_matches = pf_apply Matching.matches_conv
+
(************************************)
(* Tactics handling a list of goals *)
(************************************)
@@ -176,16 +179,16 @@ let refiner = refiner
let introduction_no_check id =
refiner (Prim (Intro id))
-let internal_cut_no_check replace 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 replace 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 =
+let refine_no_check c gl =
refiner (Prim (Refine c)) gl
-let convert_concl_no_check c sty gl =
+let convert_concl_no_check c sty gl =
refiner (Prim (Convert_concl (c,sty))) gl
let convert_hyp_no_check d gl =
@@ -199,31 +202,27 @@ let thin_no_check ids gl =
let thin_body_no_check ids gl =
if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
-let move_hyp_no_check with_dep id1 id2 gl =
+let move_hyp_no_check with_dep id1 id2 gl =
refiner (Prim (Move (with_dep,id1,id2))) gl
let order_hyps idl gl =
refiner (Prim (Order idl)) gl
-let rec rename_hyp_no_check l gl = match l with
- | [] -> tclIDTAC gl
- | (id1,id2)::l ->
- tclTHEN (refiner (Prim (Rename (id1,id2))))
+let rec rename_hyp_no_check l gl = match l with
+ | [] -> tclIDTAC gl
+ | (id1,id2)::l ->
+ tclTHEN (refiner (Prim (Rename (id1,id2))))
(rename_hyp_no_check l) gl
-let mutual_fix_with_index f n others j gl =
+let mutual_fix f n others j gl =
with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
-let mutual_fix f n others = mutual_fix_with_index f n others 0
-
-let mutual_cofix_with_index f others j gl =
+let mutual_cofix f others j gl =
with_check (refiner (Prim (Cofix (f,others,j)))) gl
-let mutual_cofix f others = mutual_cofix_with_index f others 0
-
(* Versions with consistency checks *)
-let introduction id = with_check (introduction_no_check id)
+let introduction id = with_check (introduction_no_check id)
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)
@@ -231,7 +230,7 @@ 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 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 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)
(* Pretty-printers *)
@@ -250,4 +249,4 @@ let pr_gls gls =
let pr_glls glls =
hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
-
+
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 37acf850..a808ca41 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 12168 2009-06-06 21:34:37Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -21,6 +21,7 @@ open Refiner
open Redexpr
open Tacexpr
open Rawterm
+open Pattern
(*i*)
(* Operations for handling terms under a local typing context. *)
@@ -51,7 +52,7 @@ val pf_global : goal sigma -> identifier -> constr
val pf_parse_const : goal sigma -> string -> constr
val pf_type_of : goal sigma -> constr -> types
val pf_check_type : goal sigma -> constr -> types -> unit
-val hnf_type_of : goal sigma -> constr -> types
+val pf_hnf_type_of : goal sigma -> constr -> types
val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr
val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types
@@ -66,12 +67,12 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
-val pf_reduce :
+val pf_reduce :
(env -> evar_map -> constr -> constr) ->
goal sigma -> constr -> constr
val pf_whd_betadeltaiota : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
+val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_red_product : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
@@ -86,6 +87,9 @@ val pf_const_value : goal sigma -> constant -> 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
+
type transformation_tactic = proof_tree -> (goal list * validation)
val frontier : transformation_tactic
@@ -106,7 +110,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
@@ -135,12 +139,8 @@ val move_hyp_no_check :
val rename_hyp_no_check : (identifier*identifier) list -> tactic
val order_hyps : identifier list -> tactic
val mutual_fix :
- identifier -> int -> (identifier * int * constr) list -> tactic
-val mutual_cofix : identifier -> (identifier * constr) list -> tactic
-val mutual_fix_with_index :
identifier -> int -> (identifier * int * constr) list -> int -> tactic
-val mutual_cofix_with_index :
- identifier -> (identifier * constr) list -> int -> tactic
+val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic
(*s The most primitive tactics with consistency and type checking *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 7aa57d9b..ea8ab5b6 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tactic_debug.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
open Names
open Constrextern
@@ -68,11 +68,11 @@ let skip = ref 0
(* Prints the run counter *)
let run ini =
- if not ini then
+ if not ini then
for i=1 to 2 do
print_char (Char.chr 8);print_char (Char.chr 13)
done;
- msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
+ msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
fnl() ++ fnl())
(* Prints the prompt *)
@@ -168,7 +168,7 @@ let db_matching_failure debug =
let db_eval_failure debug s =
if debug <> DebugOff & !skip = 0 then
let s = str "message \"" ++ s ++ str "\"" in
- msgnl
+ msgnl
(str "This rule has failed due to \"Fail\" tactic (" ++
s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 63c89547..0a5e6087 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tactic_debug.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
open Environ
open Pattern
@@ -24,7 +24,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
val set_match_pattern_printer :
(env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
val set_match_rule_printer :
- ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+ ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
unit
(* Debug information *)
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
(* Prints the pattern rule *)
val db_pattern_rule :
- debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
+ debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
(* Prints a matched hypothesis *)
val db_matched_hyp :
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 16:15:41 +0000