diff options
Diffstat (limited to 'proofs/decl_mode.ml')
-rw-r--r-- | proofs/decl_mode.ml | 121 |
1 files changed, 121 insertions, 0 deletions
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" |