Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 183 insertions, 0 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
new file mode 100644
index 00000000..59b48da2
--- /dev/null
+++ b/proofs/tacmach.mli
@@ -0,0 +1,183 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: tacmach.mli,v 1.50.2.1 2004/07/16 19:30:50 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+open Reduction
+open Proof_trees
+open Proof_type
+open Refiner
+open Tacred
+open Tacexpr
+open Rawterm
+(*i*)
+
+(* Operations for handling terms under a local typing context. *)
+
+type 'a sigma   = 'a Proof_type.sigma;;
+type validation = Proof_type.validation;;
+type tactic     = Proof_type.tactic;;
+
+val sig_it  : 'a sigma   -> 'a
+val project : goal sigma -> evar_map
+
+val re_sig : 'a -> evar_map -> 'a sigma
+
+val unpackage : 'a sigma -> evar_map ref * 'a
+val repackage : evar_map ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+val pf_concl              : goal sigma -> types
+val pf_env                : goal sigma -> env
+val pf_hyps               : goal sigma -> named_context
+(*i val pf_untyped_hyps       : goal sigma -> (identifier * constr) list i*)
+val pf_hyps_types         : goal sigma -> (identifier * types) list
+val pf_nth_hyp_id         : goal sigma -> int -> identifier
+val pf_last_hyp           : goal sigma -> named_declaration
+val pf_ids_of_hyps        : goal sigma -> identifier list
+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 pf_execute            : goal sigma -> constr -> unsafe_judgment
+val 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
+
+val pf_get_hyp            : goal sigma -> identifier -> named_declaration
+val pf_get_hyp_typ        : goal sigma -> identifier -> types
+
+val pf_get_new_id  : identifier      -> goal sigma -> identifier
+val pf_get_new_ids : identifier list -> goal sigma -> identifier list
+
+val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
+
+
+val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
+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_hnf_constr              : goal sigma -> constr -> constr
+val pf_red_product             : goal sigma -> constr -> constr
+val pf_nf                      : goal sigma -> constr -> constr
+val pf_nf_betaiota             : goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
+val pf_compute                 : goal sigma -> constr -> constr
+val pf_unfoldn    : (int list * evaluable_global_reference) list
+        -> goal sigma -> constr -> constr
+
+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
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val frontier : transformation_tactic
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate = Refiner.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 -> 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 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_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 :
+  evar_map -> pftreestate -> pftreestate
+
+(*
+val vernac_tactic : string * tactic_arg list -> tactic
+*)
+(*s The most primitive tactics. *)
+
+val refiner                   : rule -> tactic
+val introduction_no_check     : identifier -> tactic
+val intro_replacing_no_check  : identifier -> tactic
+val internal_cut_no_check     : identifier -> types -> tactic
+val internal_cut_rev_no_check : identifier -> types -> tactic
+val refine_no_check           : constr -> tactic
+val convert_concl_no_check    : types -> tactic
+val convert_hyp_no_check      : named_declaration -> tactic
+val thin_no_check             : identifier list -> tactic
+val thin_body_no_check        : identifier list -> tactic
+val move_hyp_no_check         : bool -> identifier -> identifier -> tactic
+val rename_hyp_no_check       : identifier -> identifier -> tactic
+val mutual_fix      :
+  identifier -> int -> (identifier * int * constr) list -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val rename_bound_var_goal : tactic
+
+(*s The most primitive tactics with consistency and type checking *)
+
+val introduction     : identifier -> tactic
+val intro_replacing  : identifier -> tactic
+val internal_cut     : identifier -> types -> tactic
+val internal_cut_rev : identifier -> types -> tactic
+val refine           : constr -> tactic
+val convert_concl    : constr -> tactic
+val convert_hyp      : named_declaration -> tactic
+val thin             : identifier list -> tactic
+val convert_concl    : types -> tactic
+val convert_hyp      : named_declaration -> tactic
+val thin             : identifier list -> tactic
+val thin_body        : identifier list -> tactic
+val move_hyp         : bool -> identifier -> identifier -> tactic
+val rename_hyp       : identifier -> identifier -> 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 Pretty-printing functions. *)
+
+(*i*)
+open Pp
+(*i*)
+
+val pr_gls    : goal sigma -> std_ppcmds
+val pr_glls   : goal list sigma -> std_ppcmds