modules Evar_refiner et Typing_ev

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 219 insertions, 0 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
new file mode 100644
index 000000000..1d03b5c93
--- /dev/null
+++ b/proofs/tacmach.mli
@@ -0,0 +1,219 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Reduction
+open Proof_trees
+open Refiner
+open Evar_refiner
+open Tacred
+(*i*)
+
+(* Operations for handling terms under a local typing context. *)
+
+type 'a sigma
+
+val sig_it  : 'a sigma   -> 'a
+val sig_sig : goal sigma -> global_constraints
+val project : goal sigma -> evar_declarations
+
+val re_sig : 'a -> global_constraints -> 'a sigma
+
+val unpackage : 'a sigma -> global_constraints ref * 'a
+val repackage : global_constraints ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+val pf_env                : goal sigma -> unsafe_env
+val pf_untyped_hyps       : goal sigma -> constr signature
+val pf_concl              : goal sigma -> constr
+val pf_nth_hyp            : goal sigma -> int -> identifier * constr
+val pf_ctxt               : goal sigma -> ctxtty
+val pf_global             : goal sigma -> identifier -> constr
+val pf_parse_const        : goal sigma -> string -> constr
+val pf_type_of            : goal sigma -> constr -> constr
+val pf_check_type         : goal sigma -> constr -> constr -> constr
+val pf_fexecute           : goal sigma -> constr -> unsafe_judgment
+val hnf_type_of           : goal sigma -> constr -> constr
+
+val pf_get_hyp             : goal sigma -> identifier -> constr
+
+val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
+
+val pf_reduce : (evar_declarations -> constr -> constr) 
+                -> goal sigma -> constr -> constr
+
+val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function
+val pf_hnf_constr              : goal sigma -> constr -> constr
+val pf_red_product             : goal sigma -> constr -> constr
+val pf_nf                      : goal sigma -> constr -> constr
+val pf_one_step_reduce         : goal sigma -> constr -> constr
+val pf_reduce_to_mind : goal sigma -> constr -> constr * constr * constr
+val pf_reduce_to_ind  : goal sigma  -> constr -> section_path * constr * constr
+val pf_compute        : goal sigma -> constr -> constr
+val pf_unfoldn        : (int list * section_path) list -> goal sigma 
+                        -> constr -> constr
+
+val pf_const_value : goal sigma -> constr -> constr
+val pf_conv_x      : goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
+
+type validation            = proof_tree list -> proof_tree
+type tactic                = goal sigma -> (goal list sigma * validation)
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val frontier : transformation_tactic
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate
+
+val proof_of_pftreestate    : pftreestate -> proof_tree
+val cursor_of_pftreestate   : pftreestate -> int list
+val is_top_pftreestate      : pftreestate -> bool
+val evc_of_pftreestate      : pftreestate -> global_constraints
+val top_goal_of_pftreestate : pftreestate -> goal sigma
+val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
+val traverse                : int -> pftreestate -> pftreestate
+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_pftreestate     : pftreestate -> constr
+val first_unproven          : pftreestate -> pftreestate
+val last_unproven           : pftreestate -> pftreestate
+val nth_unproven            : int -> pftreestate -> pftreestate
+val node_prev_unproven      : int -> pftreestate -> pftreestate
+val node_next_unproven      : int -> pftreestate -> pftreestate
+val next_unproven           : pftreestate -> pftreestate
+val prev_unproven           : pftreestate -> pftreestate
+val top_of_tree             : pftreestate -> pftreestate
+val change_constraints_pftreestate :
+  global_constraints -> pftreestate -> pftreestate
+
+
+(*s Tacticals re-exported from the Refiner module. *)
+
+val tclIDTAC         : tactic
+val tclORELSE        : tactic -> tactic -> tactic
+val tclTHEN          : tactic -> tactic -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENS         : tactic -> tactic list -> tactic
+val tclTHENSI        : tactic -> tactic list -> tactic
+val tclREPEAT        : tactic -> tactic
+val tclFIRST         : tactic list -> tactic
+val tclSOLVE         : tactic list -> tactic
+val tclTRY           : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+val tclCOMPLETE      : tactic -> tactic
+val tclAT_LEAST_ONCE : tactic -> tactic
+val tclFAIL          : tactic
+val tclDO            : int -> tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
+val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+val tclINFO          : tactic -> tactic
+
+val unTAC         : tactic -> goal sigma -> proof_tree sigma
+val vernac_tactic : tactic_expression -> tactic
+val context       : ctxtty -> tactic
+
+
+(*s The most primitive tactics. *)
+
+val refiner         : rule -> tactic
+val introduction    : identifier -> tactic
+val intro_replacing : identifier -> tactic
+val refine          : constr -> tactic
+val convert_concl   : constr -> tactic
+val convert_hyp     : identifier -> constr -> tactic
+val thin            : identifier list -> tactic
+val move_hyp        : bool -> identifier -> identifier -> tactic
+val mutual_fix      : identifier list -> int list -> constr list -> tactic
+val mutual_cofix    : identifier list -> constr list -> tactic
+val rename_bound_var_goal : tactic
+
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+val first_goal         : 'a list sigma -> 'a sigma
+val goal_goal_list     : 'a sigma -> 'a list sigma
+val apply_tac_list     : tactic -> tactic_list
+val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
+val tactic_list_tactic : tactic_list -> tactic
+val tclFIRSTLIST       : tactic_list list -> tactic_list
+val tclIDTAC_list      : tactic_list
+
+
+(*s Walking constraints re-exported. *)
+
+type walking_constraints = Evar_refiner.walking_constraints
+
+type 'a result_w_tactic  = walking_constraints -> walking_constraints * 'a
+type w_tactic            = walking_constraints -> walking_constraints
+
+val startWalk : 
+  goal sigma -> walking_constraints * (walking_constraints -> tactic)
+
+val walking_THEN        : 'a result_w_tactic -> ('a -> tactic) -> tactic
+val walking             : w_tactic -> tactic
+val w_Focusing_THEN     : section_path -> 'a result_w_tactic 
+                          -> ('a -> w_tactic) -> w_tactic
+val w_Declare           : section_path -> constr -> w_tactic
+val w_Declare_At        : section_path -> section_path -> constr -> w_tactic
+val w_Define            : section_path -> constr -> w_tactic
+val w_Underlying        : walking_constraints -> evar_declarations
+val w_hyps              : walking_constraints -> context
+val w_type_of           : walking_constraints -> constr -> constr
+val w_add_sign          : (identifier * typed_type) 
+                          -> walking_constraints -> walking_constraints
+val w_IDTAC             : w_tactic
+val w_ORELSE            : w_tactic -> w_tactic -> w_tactic
+val ctxt_type_of        : readable_constraints -> constr -> constr
+val w_whd_betadeltaiota : walking_constraints -> constr -> constr
+val w_hnf_constr        : walking_constraints -> constr -> constr
+val w_conv_x            : walking_constraints -> constr -> constr -> bool
+val w_const_value       : walking_constraints -> constr -> constr
+val w_defined_const     : walking_constraints -> constr -> bool
+
+
+(*s Tactic Registration. *)
+
+val add_tactic         : string -> (tactic_arg list -> tactic) -> unit
+val overwriting_tactic : string -> (tactic_arg list -> tactic) -> unit
+
+
+(*s Hiding the implementation of tactics. *)
+
+val hide_tactic  : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+val overwrite_hidden_tactic : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+
+type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
+
+val hide_atomic_tactic  : string -> tactic -> tactic
+val hide_constr_tactic  : constr hide_combinator
+val hide_constrl_tactic : (constr list) hide_combinator
+val hide_numarg_tactic  : int hide_combinator
+val hide_ident_tactic   : identifier hide_combinator
+val hide_identl_tactic  : (identifier list) hide_combinator
+val hide_string_tactic  : string hide_combinator
+val hide_bindl_tactic   : ((bindOcc * constr) list) hide_combinator
+val hide_cbindl_tactic  : (constr * (bindOcc * constr) list) hide_combinator
+val hide_cbindll_tactic : 
+  ((constr * (bindOcc * constr) list) list) hide_combinator
+