From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- proofs/clenvtac.ml | 47 ++++---- proofs/clenvtac.mli | 2 +- proofs/decl_expr.mli | 24 ++-- proofs/decl_mode.ml | 42 +++---- proofs/decl_mode.mli | 8 +- proofs/evar_refiner.ml | 53 ++++---- proofs/evar_refiner.mli | 8 +- proofs/logic.ml | 187 ++++++++++++++--------------- proofs/logic.mli | 6 +- proofs/pfedit.ml | 108 ++++++++++------- proofs/pfedit.mli | 23 +++- proofs/proof_trees.ml | 25 ++-- proofs/proof_trees.mli | 4 +- proofs/proof_type.ml | 31 ++--- proofs/proof_type.mli | 43 +++---- proofs/proofs.mllib | 12 ++ proofs/redexpr.ml | 131 ++++++++++++++------ proofs/redexpr.mli | 15 ++- proofs/refiner.ml | 312 +++++++++++++++++++++++++++--------------------- proofs/refiner.mli | 30 +++-- proofs/tacexpr.ml | 149 ++++++++++++----------- proofs/tacmach.ml | 61 +++++----- proofs/tacmach.mli | 20 ++-- proofs/tactic_debug.ml | 8 +- proofs/tactic_debug.mli | 6 +- 25 files changed, 770 insertions(+), 585 deletions(-) create mode 100644 proofs/proofs.mllib (limited to 'proofs') 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 + (list_map_i (fun i -> apply_sig_tac sigr (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 : -- cgit v1.2.3