diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /proofs | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/decl_expr.mli | 108 | ||||
-rw-r--r-- | proofs/decl_mode.ml | 121 | ||||
-rw-r--r-- | proofs/decl_mode.mli | 73 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 6 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 4 | ||||
-rw-r--r-- | proofs/logic.ml | 63 | ||||
-rw-r--r-- | proofs/pfedit.ml | 24 | ||||
-rw-r--r-- | proofs/pfedit.mli | 6 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 27 | ||||
-rw-r--r-- | proofs/proof_trees.mli | 6 | ||||
-rw-r--r-- | proofs/proof_type.ml | 17 | ||||
-rw-r--r-- | proofs/proof_type.mli | 16 | ||||
-rw-r--r-- | proofs/redexpr.ml | 4 | ||||
-rw-r--r-- | proofs/refiner.ml | 226 | ||||
-rw-r--r-- | proofs/refiner.mli | 32 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 4 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.mli | 8 |
18 files changed, 582 insertions, 165 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli new file mode 100644 index 00000000..24af3842 --- /dev/null +++ b/proofs/decl_expr.mli @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Util +open Tacexpr + +type ('constr,'tac) justification = + By_tactic of 'tac +| Automated of 'constr list + +type 'it statement = + {st_label:name; + st_it:'it} + +type thesis_kind = + Plain + | Sub of int + | For of identifier + +type 'this or_thesis = + This of 'this + | Thesis of thesis_kind + +type side = Lhs | Rhs + +type elim_type = + ET_Case_analysis + | ET_Induction + +type block_type = + B_proof + | B_claim + | B_focus + | B_elim of elim_type + +type ('it,'constr,'tac) cut = + {cut_stat: 'it statement; + cut_by: ('constr,'tac) justification} + +type ('var,'constr) hyp = + Hvar of 'var + | Hprop of 'constr statement + +type ('constr,'tac) casee = + Real of 'constr + | Virtual of ('constr,'constr,'tac) cut + +type ('hyp,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pcut of ('constr or_thesis,'constr,'tac) cut + | Prew of side * ('constr,'constr,'tac) cut + | Passume of ('hyp,'constr) hyp list + | Plet of ('hyp,'constr) hyp list + | Pgiven of ('hyp,'constr) hyp list + | Pconsider of 'constr*('hyp,'constr) hyp list + | Pclaim of 'constr statement + | 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 + | Pper of elim_type * ('constr,'tac) casee + | Pend of block_type + | Pescape + +type emphasis = int + +type ('hyp,'constr,'pat,'tac) gen_proof_instr= + {emph: emphasis; + instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + + +type raw_proof_instr = + ((identifier*(Topconstr.constr_expr option)) located, + Topconstr.constr_expr, + Topconstr.cases_pattern_expr, + raw_tactic_expr) gen_proof_instr + +type glob_proof_instr = + ((identifier*(Genarg.rawconstr_and_expr option)) located, + Genarg.rawconstr_and_expr, + Topconstr.cases_pattern_expr, + Tacexpr.glob_tactic_expr) gen_proof_instr + +type proof_pattern = + {pat_vars: Term.types statement list; + pat_aliases: (Term.constr*Term.types) statement list; + pat_constr: Term.constr; + pat_typ: Term.types; + pat_pat: Rawterm.cases_pattern; + pat_expr: Topconstr.cases_pattern_expr} + +type proof_instr = + (Term.constr statement, + Term.constr, + proof_pattern, + Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml new file mode 100644 index 00000000..094c5625 --- /dev/null +++ b/proofs/decl_mode.ml @@ -0,0 +1,121 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Term +open Evd +open Util + +let daimon_flag = ref false + +let set_daimon_flag () = daimon_flag:=true +let clear_daimon_flag () = daimon_flag:=false +let get_daimon_flag () = !daimon_flag + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +let mode_of_pftreestate pts = + let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in + if goal.evar_extra = None then + Mode_tactic + else + Mode_proof + +let get_current_mode () = + try + mode_of_pftreestate (Pfedit.get_pftreestate ()) + with _ -> Mode_none + +let check_not_proof_mode str = + if get_current_mode () = Mode_proof then + error str + +type split_tree= + Push of (Idset.t * split_tree) + | Split of (Idset.t * inductive * (Idset.t * split_tree) option array) + | Pop of split_tree + | End_of_branch of (identifier * int) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + { pm_last: Names.name (* anonymous if none *); + pm_hyps: Idset.t; + pm_partial_goal : constr ; (* partial goal construction *) + pm_subgoals : (metavariable*constr) list; + pm_stack : stack_info list } + +let pm_in,pm_out = Dyn.create "pm_info" + +let get_info gl= + match gl.evar_extra with + None -> invalid_arg "get_info" + | Some extra -> + try pm_out extra with _ -> invalid_arg "get_info" + +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 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 + Mode_proof -> + Some + begin + match get_top_stack pts with + [] -> "\"end proof\"" + | Claim::_ -> "\"end claim\"" + | Focus_claim::_-> "\"end focus\"" + | (Suppose_case :: Per (et,_,_,_) :: _ + | Per (et,_,_,_) :: _ ) -> + begin + match et with + Decl_expr.ET_Case_analysis -> + "\"end cases\" or start a new case" + | Decl_expr.ET_Induction -> + "\"end induction\" or start a new case" + end + | _ -> anomaly "lonely suppose" + end + | Mode_tactic -> + begin + try + ignore + (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts); + Some "\"return\"" + with Not_found -> None + end + | Mode_none -> + error "no proof in progress" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli new file mode 100644 index 00000000..0dd1cb33 --- /dev/null +++ b/proofs/decl_mode.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Term +open Evd +open Tacmach + +val set_daimon_flag : unit -> unit +val clear_daimon_flag : unit -> unit +val get_daimon_flag : unit -> bool + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +val mode_of_pftreestate : pftreestate -> command_mode + +val get_current_mode : unit -> command_mode + +val check_not_proof_mode : string -> unit + +type split_tree= + Push of (Idset.t * split_tree) + | Split of (Idset.t * inductive * (Idset.t*split_tree) option array) + | Pop of split_tree + | End_of_branch of (identifier * int) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + { pm_last: Names.name (* anonymous if none *); + pm_hyps: Idset.t; + pm_partial_goal : constr ; (* partial goal construction *) + pm_subgoals : (metavariable*constr) list; + pm_stack : stack_info list } + +val pm_in : pm_info -> Dyn.t + +val get_info : Proof_type.goal -> pm_info + +val get_end_command : pftreestate -> string option + +val get_stack : pftreestate -> stack_info list + +val get_top_stack : pftreestate -> stack_info list diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 7a23d052..79f01ba1 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: evar_refiner.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Util open Names @@ -22,7 +22,7 @@ open Refiner (* w_tactic pour instantiate *) -let w_refine env ev rawc evd = +let w_refine ev rawc evd = if Evd.is_defined (evars_of evd) ev then error "Instantiate called on already-defined evar"; let e_info = Evd.find (evars_of evd) ev in @@ -45,5 +45,5 @@ let instantiate_pf_com n com pfts = let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in let evd = create_evar_defs sigma in - let evd' = w_refine env sp rawc evd in + let evd' = w_refine sp rawc evd in change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 9880f2f0..baa6b19a 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 6616 2005-01-21 17:18:23Z herbelin $ i*) +(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Names @@ -18,7 +18,7 @@ open Refiner (* Refinement of existential variables. *) -val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs +val w_refine : evar -> Rawterm.rawconstr -> evar_defs -> evar_defs val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/logic.ml b/proofs/logic.ml index ffbc0d56..e40d1232 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *) open Pp open Util @@ -80,15 +80,15 @@ let clear_hyps ids gl = error (string_of_id id'^ " is used in hypothesis "^string_of_id id)) (global_vars_set_of_decl env d) in - clear_hyps ids fcheck gl.evar_hyps in + clear_hyps ids fcheck gl.evar_hyps in let ncl = gl.evar_concl in - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^" is used in conclusion")) - (global_vars_set env ncl); - mk_goal nhyps ncl + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^" is used in conclusion")) + (global_vars_set_drop_evar env ncl); + mk_goal nhyps ncl gl.evar_extra (* The ClearBody tactic *) @@ -155,7 +155,7 @@ let split_sign hfrom hto l = else splitrec (d::left) (toleft or (hyp = hto)) right in - splitrec [] false l + splitrec [] false l let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = let env = Global.env() in @@ -214,19 +214,25 @@ let check_forward_dependencies id tail = ^ (string_of_id id'))) tail +let check_goal_dependency id cl = + let env = Global.env() in + if Idset.mem id (global_vars_set_drop_evar env cl) then + error (string_of_id id^" is used in conclusion") let rename_hyp id1 id2 sign = apply_to_hyp_and_dependent_on sign id1 (fun (_,b,t) _ -> (id2,b,t)) (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) -let replace_hyp sign id d = +let replace_hyp sign id d cl = + if !check then + check_goal_dependency id cl; apply_to_hyp sign id (fun sign _ tail -> - if !check then - (check_backward_dependencies sign d; - check_forward_dependencies id tail); - d) + if !check then + (check_backward_dependencies sign d; + check_forward_dependencies id tail); + d) (* why we dont check that id does not appear in tail ??? *) let insert_after_hyp sign id d = @@ -264,6 +270,7 @@ let goal_type_of env sigma c = let rec mk_refgoals sigma goal goalacc conclty trm = let env = evar_env goal in let hyps = goal.evar_hyps in + 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 @@ -284,9 +291,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = - if isInd f & not (array_exists occur_meta l) (* we could be finer *) - then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l) - else mk_hdgoals sigma goal goalacc f + match kind_of_term f with + | (Ind _ (* needed if defs in Type are polymorphic: | Const _*)) + when not (array_exists occur_meta l) (* we could be finer *) -> + (* Sort-polymorphism of definition and inductive types *) + goalacc, + type_of_global_reference_knowing_parameters env sigma f l + | _ -> + mk_hdgoals sigma goal goalacc f in let (acc'',conclty') = mk_arggoals sigma goal acc' hdty (Array.to_list l) in @@ -315,6 +327,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = and mk_hdgoals sigma goal goalacc trm = let env = evar_env goal in let hyps = goal.evar_hyps in + let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; @@ -326,8 +339,10 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty) = - if isInd f & not (array_exists occur_meta l) (* we could be finer *) - then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l) + 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) else mk_hdgoals sigma goal goalacc f in mk_arggoals sigma goal acc' hdty (Array.to_list l) @@ -392,6 +407,7 @@ let prim_refiner r sigma goal = let env = evar_env goal in let sign = goal.evar_hyps in let cl = goal.evar_concl in + let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in match r with (* Logical rules *) | Intro id -> @@ -416,12 +432,12 @@ let prim_refiner r sigma goal = (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); - let sign' = replace_hyp sign id (id,None,c1) in + let sign' = replace_hyp sign id (id,None,c1) cl in let sg = mk_goal sign' (subst1 (mkVar id) b) in [sg] | LetIn (_,c1,t1,b) -> if occur_meta c1 then error_use_instantiate(); - let sign' = replace_hyp sign id (id,Some c1,t1) in + let sign' = replace_hyp sign id (id,Some c1,t1) cl in let sg = mk_goal sign' (subst1 (mkVar id) b) in [sg] | _ -> @@ -474,7 +490,8 @@ let prim_refiner r sigma goal = let _ = find_coinductive env sigma b in () with Not_found -> error ("All methods must construct elements " ^ - "in coinductive types") + "in coinductiv-> goal +e types") in let all = (f,cl)::others in List.iter (fun (_,c) -> check_is_coind env c) all; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index fa6f8c37..565c9547 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *) +(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -150,6 +150,14 @@ let subtree_solved () = is_complete_proof (proof_of_pftreestate pts) & not (is_top_pftreestate pts) +let tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate pts) + +let top_tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate (top_of_tree pts)) + (*********************************************************************) (* Undo functions *) (*********************************************************************) @@ -243,7 +251,7 @@ let set_end_tac tac = (*********************************************************************) let start_proof na str sign concl hook = - let top_goal = mk_goal sign concl in + let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; top_goal = top_goal; @@ -253,7 +261,6 @@ let start_proof na str sign concl hook = start(na,ts); set_current_proof na - let solve_nth k tac = let pft = get_pftreestate () in if not (List.mem (-1) (cursor_of_pftreestate pft)) then @@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven let traverse_next_unproven () = mutate next_unproven - (* The goal focused on *) let focus_n = ref 0 let make_focus n = focus_n := n @@ -317,5 +323,11 @@ 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 pts = get_pftreestate () in - if not (is_top_pftreestate pts) then mutate top_of_tree + mutate top_of_tree + +let reset_top_of_script () = + mutate (fun pts -> + try + up_until_matching_rule is_proof_instr pts + with Not_found -> top_of_tree pts) + diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index ca379d2e..8c0c7f55 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 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Util @@ -172,8 +172,12 @@ val make_focus : int -> unit val focus : unit -> int val focused_goal : unit -> int val subtree_solved : unit -> bool +val tree_solved : unit -> bool +val top_tree_solved : unit -> bool val reset_top_of_tree : unit -> unit +val reset_top_of_script : unit -> unit + val traverse : int -> unit val traverse_nth_goal : int -> unit val traverse_next_unproven : unit -> unit diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 7e299b89..9d70d012 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 6113 2004-09-17 20:28:19Z barras $ *) +(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Closure open Util @@ -18,6 +18,7 @@ open Sign open Evd open Environ open Evarutil +open Decl_expr open Proof_type open Tacred open Typing @@ -32,9 +33,9 @@ let is_bind = function (* Functions on goals *) -let mk_goal hyps cl = +let mk_goal hyps cl extra = { evar_hyps = hyps; evar_concl = cl; - evar_body = Evar_empty} + evar_body = Evar_empty; evar_extra = extra } (* Functions on proof trees *) @@ -52,7 +53,7 @@ let children_of_proof pf = let goal_of_proof pf = pf.goal let subproof_of_proof pf = match pf.ref with - | Some (Tactic (_,pf), _) -> pf + | Some (Nested (_,pf), _) -> pf | _ -> failwith "subproof_of_proof" let status_of_proof pf = pf.open_subgoals @@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0 let is_leaf_proof pf = (pf.ref = None) let is_tactic_proof pf = match pf.ref with - | Some (Tactic _, _) -> true + | Some (Nested (Tactic _,_),_) -> true | _ -> false @@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed 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) *) + +let is_dem_rule = function + Decl_proof _ -> true + | _ -> false + +let is_proof_instr = function + Nested(Proof_instr (_,_),_) -> true + | _ -> false + +let is_focussing_command = function + Decl_proof b -> b + | Nested (Proof_instr (b,_),_) -> b + | _ -> false + + (*********************************************************************) (* Pretty printing functions *) (*********************************************************************) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index cbf91c8a..f9b64f41 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 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: proof_trees.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Util @@ -21,7 +21,7 @@ open Proof_type (* This module declares readable constraints, and a few utilities on constraints and proof trees *) -val mk_goal : named_context_val -> constr -> goal +val mk_goal : named_context_val -> constr -> Dyn.t option -> goal val rule_of_proof : proof_tree -> rule val ref_of_proof : proof_tree -> (rule * proof_tree list) @@ -36,6 +36,8 @@ val is_tactic_proof : proof_tree -> bool val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option val pf_lookup_index_as_renamed : env -> constr -> int -> int option +val is_proof_instr : rule -> bool +val is_focussing_command : rule -> bool (*s Pretty printing functions. *) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 009e9d5b..abe31624 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 7639 2005-12-02 10:01:15Z gregoire $ *) +(*i $Id: proof_type.ml 9244 2006-10-16 17:11:44Z barras $ *) (*i*) open Environ @@ -16,6 +16,7 @@ open Libnames open Term open Util open Tacexpr +open Decl_expr open Rawterm open Genarg open Nametab @@ -39,12 +40,6 @@ type prim_rule = | Move of bool * identifier * identifier | Rename of identifier * identifier -(*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(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; goal : goal; @@ -52,9 +47,15 @@ type proof_tree = { and rule = | Prim of prim_rule - | Tactic of tactic_expr * proof_tree + | Nested of compound_rule * proof_tree + | Decl_proof of bool + | Daimon | Change_evars +and compound_rule= + | Tactic of tactic_expr * bool + | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *) + and goal = evar_info and tactic = goal sigma -> (goal list sigma * validation) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 0e42dcba..d87c1298 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 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: proof_type.mli 9244 2006-10-16 17:11:44Z barras $ i*) (*i*) open Environ @@ -16,6 +16,7 @@ open Libnames open Term open Util open Tacexpr +open Decl_expr open Rawterm open Genarg open Nametab @@ -46,7 +47,7 @@ type prim_rule = evar_body = Evar_Empty; evar_info = { pgm : [The Realizer pgm if any] lc : [Set of evar num occurring in subgoal] }} - sigma = { stamp = [an int characterizing the ed field, for quick compare] + sigma = { stamp = [an int chardacterizing the ed field, for quick compare] ed : [A set of existential variables depending in the subgoal] number of first evar, it = { evar_concl = [the type of first evar] @@ -71,7 +72,7 @@ type prim_rule = [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(Tactic (t,p),l))] then [p] is the proof + 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; @@ -80,9 +81,16 @@ type proof_tree = { and rule = | Prim of prim_rule - | Tactic of tactic_expr * proof_tree + | Nested of compound_rule * proof_tree + | Decl_proof of bool + | Daimon | Change_evars +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 + and goal = evar_info and tactic = goal sigma -> (goal list sigma * validation) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index eb47fc2e..ad277caa 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: redexpr.ml 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *) open Pp open Util @@ -24,7 +24,7 @@ open RedFlags (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in - Vconv.cbv_vm env c ctyp + Vnorm.cbv_vm env c ctyp let set_opaque_const sp = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 067ae471..70a0e3db 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: refiner.ml 9261 2006-10-23 10:01:40Z barras $ *) open Pp open Util @@ -43,6 +43,31 @@ let and_status = List.fold_left (+) 0 let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps + +let descend n p = + match p.ref with + | None -> error "It is a leaf." + | Some(r,pfl) -> + if List.length pfl >= n then + (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")) + | _ -> assert false) + else + error "Too few subproofs" + (* Normalizing evars in a goal. Called by tactic Local_constraints (i.e. when the sigma of the proof tree changes). Detect if the goal is unchanged *) @@ -50,10 +75,10 @@ let norm_goal sigma gl = let red_fun = Evarutil.nf_evar sigma in let ncl = red_fun gl.evar_concl in let ngl = - { evar_concl = ncl; - evar_hyps = map_named_val red_fun gl.evar_hyps; - evar_body = gl.evar_body} in - if Evd.eq_evar_info ngl gl then None else Some ngl + { 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 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] @@ -91,9 +116,9 @@ let rec frontier p = (List.flatten gll, (fun retpfl -> let pfl' = mapshape (List.map List.length gll) vl retpfl in - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')})) + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')})) let rec frontier_map_rec f n p = @@ -111,9 +136,9 @@ let rec frontier_map_rec f n p = (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc)) (n,[]) pfl in let pfl' = List.rev rpfl' in - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')} + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')} let frontier_map f n p = let nmax = p.open_subgoals in @@ -137,9 +162,9 @@ 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 - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')} + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')} let frontier_mapi f p = frontier_mapi_rec f 1 p @@ -152,50 +177,35 @@ let rec nb_unsolved_goals pf = pf.open_subgoals (* leaf g is the canonical incomplete proof of a goal g *) -let leaf g = { - open_subgoals = 1; - goal = g; - ref = None } - -(* Tactics table. *) - -let tac_tab = Hashtbl.create 17 - -let add_tactic s t = - if Hashtbl.mem tac_tab s then - errorlabstrm ("Refiner.add_tactic: ") - (str ("Cannot redeclare tactic "^s)); - Hashtbl.add tac_tab s t - -let overwriting_add_tactic s t = - if Hashtbl.mem tac_tab s then begin - Hashtbl.remove tac_tab s; - warning ("Overwriting definition of tactic "^s) - end; - Hashtbl.add tac_tab s t - -let lookup_tactic s = - try - Hashtbl.find tac_tab s - with Not_found -> - errorlabstrm "Refiner.lookup_tactic" - (str"The tactic " ++ str s ++ str" is not installed") - +let leaf g = + { open_subgoals = 1; + goal = g; + ref = None } (* refiner r is a tactic applying the rule r *) let check_subproof_connection gl spfl = list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl -let abstract_tactic_expr te tacfun gls = - let (sgl_sigma,v) = tacfun gls in - let hidden_proof = v (List.map leaf sgl_sigma.it) in + +let abstract_operation syntax semantics gls = + let (sgl_sigma,validation) = semantics gls in + let hidden_proof = validation (List.map leaf sgl_sigma.it) in (sgl_sigma, fun spfl -> assert (check_subproof_connection sgl_sigma.it spfl); { open_subgoals = and_status (List.map pf_status spfl); goal = gls.it; - ref = Some(Tactic(te,hidden_proof),spfl) }) + ref = Some(Nested(syntax,hidden_proof),spfl)}) + +let abstract_tactic_expr ?(dflt=false) te tacfun gls = + abstract_operation (Tactic(te,dflt)) tacfun gls + +let abstract_tactic ?(dflt=false) te = + abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) + +let abstract_extended_tactic ?(dflt=false) s args = + abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args)) let refiner = function | Prim pr as r -> @@ -209,8 +219,21 @@ let refiner = function goal = goal_sigma.it; ref = Some(r,spfl) }))) - | Tactic _ -> failwith "Refiner: should not occur" + + | Nested (_,_) | Decl_proof _ -> + failwith "Refiner: should not occur" + (* Daimon is a canonical unfinished proof *) + + | Daimon -> + fun gls -> + ({it=[];sigma=gls.sigma}, + fun spfl -> + assert (spfl=[]); + { open_subgoals = 0; + goal = gls.it; + ref = Some(Daimon,[])}) + (* [Local_constraints lc] makes the local constraints be [lc] and normalizes evars *) @@ -237,19 +260,11 @@ let local_Constraints gl = refiner Change_evars gl let norm_evar_tac = local_Constraints -(* -let vernac_tactic (s,args) = - let tacfun = lookup_tactic s args in - abstract_extra_tactic s args tacfun -*) -let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te)) - -let abstract_extended_tactic s args = - abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args)) - -let vernac_tactic (s,args) = - let tacfun = lookup_tactic s args in - abstract_extended_tactic s args tacfun +let norm_evar_proof sigma pf = + let nf_subgoal i sgl = + let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in + v (List.map leaf gll.it) in + frontier_mapi nf_subgoal pf (* [extract_open_proof : proof_tree -> constr * (int * constr) list] takes a (not necessarly complete) proof and gives a pair (pfterm,obl) @@ -271,14 +286,16 @@ let extract_open_proof sigma pf = let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf - | {ref=Some(Tactic (_,hidden_proof),spfl)} -> + | {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(Change_evars,[pf])} -> (proof_extractor vl) pf + + | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf - | {ref=None;goal=goal} -> + | {ref=(None|Some(Daimon,[]));goal=goal} -> let visible_rels = map_succeed (fun id -> @@ -555,6 +572,8 @@ let tclIFTHENSELSE=ite_gen tclTHENS let tclIFTHENSVELSE=ite_gen tclTHENSV +let tclIFTHENTRYELSEMUST tac1 tac2 gl = + tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") @@ -633,7 +652,6 @@ let tactic_list_tactic tac gls = - (* 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 @@ -665,41 +683,19 @@ 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 descend n p = - match p.ref with - | None -> error "It is a leaf." - | Some(r,pfl) -> - if List.length pfl >= n then - (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 - { open_subgoals = newstatus; - goal = p.goal; - ref = Some(r,spfl) } - else - error "descend: validation")) - | _ -> assert false) - else - error "Too few subproofs" - let traverse n pts = match n with | 0 -> (* go to the parent *) (match pts.tstack with | [] -> error "traverse: no ancestors" | (_,v)::tl -> - { tpf = v [pts.tpf]; + let pf = v [pts.tpf] in + let pf = norm_evar_proof pts.tpfsigma pf in + { tpf = pf; tstack = tl; tpfsigma = pts.tpfsigma }) | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) (match pts.tpf.ref with - | Some (Tactic (_,spf),_) -> + | Some (Nested (_,spf),_) -> let v = (fun pfl -> pts.tpf) in { tpf = spf; tstack = (-1,v)::pts.tstack; @@ -718,17 +714,23 @@ let app_tac sigr tac p = sigr := gll.sigma; v (List.map leaf gll.it) -(* solve the nth subgoal with tactic tac *) -let solve_nth_pftreestate n tac pts = +(* modify proof state at current position *) + +let map_pftreestate f pts = let sigr = ref pts.tpfsigma in - let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in + let tpf' = f sigr pts.tpf in let tpf'' = - if !sigr == pts.tpfsigma then tpf' - else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in + if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in { tpf = tpf''; tpfsigma = !sigr; tstack = pts.tstack } +(* solve the nth subgoal with tactic tac *) + +let solve_nth_pftreestate n tac = + 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. @@ -880,6 +882,38 @@ let prev_unproven pts = let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +let change_rule f pts = + let mark_top _ pt = + match pt.ref with + Some (oldrule,l) -> + {pt with ref=Some (f oldrule,l)} + | _ -> invalid_arg "change_rule" in + map_pftreestate mark_top pts + +let match_rule p pts = + match (proof_of_pftreestate pts).ref with + Some (r,_) -> p r + | None -> false + +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 + pts + else + up_until_matching_rule p one_up + +let rec up_to_matching_rule p pts = + if match_rule p pts then + pts + else + if is_top_pftreestate pts then + raise Not_found + else + let one_up = traverse 0 pts in + up_to_matching_rule p one_up (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 417ddbcd..d8b13dba 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 7911 2006-01-21 11:18:36Z herbelin $ i*) +(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*) (*i*) open Term @@ -32,20 +32,17 @@ val apply_sig_tac : type transformation_tactic = proof_tree -> (goal list * validation) -val add_tactic : string -> (closed_generic_argument list -> tactic) -> unit -val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit -val lookup_tactic : string -> (closed_generic_argument list) -> tactic - (*s Hiding the implementation of tactics. *) (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under - a single proof node *) -val abstract_tactic : atomic_tactic_expr -> tactic -> tactic -val abstract_tactic_expr : tactic_expr -> tactic -> tactic -val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic + a single proof node. The boolean tells if the default tactic is used. *) +val abstract_operation : compound_rule -> tactic -> tactic +val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic +val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic +val abstract_extended_tactic : + ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic val refiner : rule -> tactic -val vernac_tactic : string * closed_generic_argument list -> tactic val frontier : transformation_tactic val list_pf : proof_tree -> goal list val unTAC : tactic -> goal sigma -> proof_tree sigma @@ -148,6 +145,12 @@ 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. + Equivalent to [(tac1;try tac2)||tac2] *) + +val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic + (*s Tactics handling a list of goals. *) type validation_list = proof_tree list -> proof_tree list @@ -170,11 +173,14 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool +val match_rule : (rule -> bool) -> pftreestate -> bool val evc_of_pftreestate : pftreestate -> evar_map 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 : + (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate val solve_pftreestate : tactic -> pftreestate -> pftreestate @@ -193,6 +199,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate 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) -> + pftreestate -> pftreestate +val up_to_matching_rule : (rule -> bool) -> + pftreestate -> pftreestate +val change_rule : (rule -> rule) -> pftreestate -> pftreestate val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b721dacd..0fe21552 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 8917 2006-06-07 16:59:05Z herbelin $ i*) +(*i $Id: tacexpr.ml 9267 2006-10-24 12:55:46Z herbelin $ i*) open Names open Topconstr @@ -234,7 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = '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 - | TacFreshId of string option + | TacFreshId of string or_var list | Tacexp of 'tac (* Globalized tactics *) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 889e06a8..96df8f64 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -31,6 +31,8 @@ type debug_info = (* An exception handler *) let explain_logic_error = ref (fun e -> mt()) +let explain_logic_error_no_anomaly = ref (fun e -> mt()) + (* Prints the goal *) let db_pr_goal g = msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g)) diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index fc1b6120..6de8244d 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 7911 2006-01-21 11:18:36Z herbelin $ i*) +(*i $Id: tactic_debug.mli 9092 2006-08-28 11:42:14Z bertot $ i*) open Environ open Pattern @@ -66,5 +66,11 @@ val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit (* An exception handler *) val explain_logic_error: (exn -> Pp.std_ppcmds) ref +(* For use in the Ltac debugger: some exception that are usually + consider anomalies are acceptable because they are caught later in + the process that is being debugged. One should not require + from users that they report these anomalies. *) +val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref + (* Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit |