From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- proofs/tacmach.mli | 183 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 proofs/tacmach.mli (limited to 'proofs/tacmach.mli') 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 *) +(* '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 -- cgit v1.2.3