Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 260 insertions, 0 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
new file mode 100644
index 00000000..0e3a49b0
--- /dev/null
+++ b/proofs/tacmach.ml
@@ -0,0 +1,260 @@
+(************************************************************************)
+(*  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: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *)
+
+open Util
+open Names
+open Nameops
+open Sign
+open Term
+open Termops
+open Instantiate
+open Environ
+open Reductionops
+open Evd
+open Typing
+open Tacred
+open Proof_trees
+open Proof_type
+open Logic
+open Refiner
+open Tacexpr
+
+let re_sig it gc = { it = it; sigma = gc }
+
+(**************************************************************)
+(* 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;;
+
+let unpackage = Refiner.unpackage
+let repackage = Refiner.repackage
+let apply_sig_tac = Refiner.apply_sig_tac
+
+let sig_it     = Refiner.sig_it
+let project    = Refiner.sig_sig
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = (sig_it gls).evar_hyps
+
+let pf_concl gls = (sig_it gls).evar_concl
+let pf_hyps_types gls  =
+  let sign = Environ.named_context (pf_env gls) in
+  List.map (fun (id,_,x) -> (id, x)) sign
+
+let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
+
+let pf_last_hyp gl = List.hd (pf_hyps gl)
+
+let pf_get_hyp gls id = 
+  try 
+    Sign.lookup_named id (pf_hyps gls)
+  with Not_found -> 
+    error ("No such hypothesis : " ^ (string_of_id id))
+
+let pf_get_hyp_typ gls id =
+  let (_,_,ty)= (pf_get_hyp gls id) in
+  ty
+
+let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
+
+let pf_get_new_id id gls = 
+  next_ident_away id (pf_ids_of_hyps gls)
+
+let pf_get_new_ids ids gls =
+  let avoid = pf_ids_of_hyps gls in
+  List.fold_right
+    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
+    ids []
+
+let pf_interp_constr gls c =
+  let evc = project gls in 
+  Constrintern.interp_constr evc (pf_env gls) c
+
+let pf_interp_openconstr gls c =
+  let evc = project gls in 
+  Constrintern.interp_openconstr evc (pf_env gls) c
+
+let pf_interp_type gls c =
+  let evc = project gls in 
+  Constrintern.interp_type evc (pf_env gls) c
+
+let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+
+let pf_parse_const gls = compose (pf_global gls) id_of_string
+
+let pf_execute gls =
+  let evc = project gls in 
+  Typing.unsafe_machine (pf_env gls) evc
+
+let pf_reduction_of_redexp gls re c = 
+  reduction_of_redexp re (pf_env gls) (project gls) c 
+
+let pf_apply f gls = f (pf_env gls) (project gls)
+let pf_reduce = pf_apply
+
+let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
+let pf_hnf_constr                = pf_reduce hnf_constr
+let pf_red_product               = pf_reduce red_product
+let pf_nf                        = pf_reduce nf
+let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_compute                   = pf_reduce compute
+let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_type_of                   = pf_reduce type_of
+
+let pf_conv_x                   = pf_reduce is_conv
+let pf_conv_x_leq               = pf_reduce is_conv_leq
+let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
+let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
+let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
+
+let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
+
+let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2)))
+
+(************************************)
+(* Tactics handling a list of goals *)
+(************************************)
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+let first_goal         = first_goal
+let goal_goal_list     = goal_goal_list
+let apply_tac_list     = apply_tac_list
+let then_tactic_list   = then_tactic_list
+let tactic_list_tactic = tactic_list_tactic
+let tclFIRSTLIST       = tclFIRSTLIST
+let tclIDTAC_list      = tclIDTAC_list
+
+
+(********************************************************)
+(* Functions for handling the state of the proof editor *)
+(********************************************************)
+
+type pftreestate = Refiner.pftreestate
+
+let proof_of_pftreestate    = proof_of_pftreestate
+let cursor_of_pftreestate   = cursor_of_pftreestate
+let is_top_pftreestate      = is_top_pftreestate
+let evc_of_pftreestate      = evc_of_pftreestate
+let top_goal_of_pftreestate = top_goal_of_pftreestate
+let nth_goal_of_pftreestate = nth_goal_of_pftreestate
+let traverse                = traverse
+let solve_nth_pftreestate   = solve_nth_pftreestate
+let solve_pftreestate       = solve_pftreestate
+let weak_undo_pftreestate   = weak_undo_pftreestate
+let mk_pftreestate          = mk_pftreestate
+let extract_pftreestate     = extract_pftreestate
+let extract_open_pftreestate = extract_open_pftreestate
+let first_unproven          = first_unproven
+let last_unproven           = last_unproven
+let nth_unproven            = nth_unproven
+let node_prev_unproven      = node_prev_unproven
+let node_next_unproven      = node_next_unproven
+let next_unproven           = next_unproven
+let prev_unproven           = prev_unproven
+let top_of_tree             = top_of_tree
+let frontier                = frontier
+let change_constraints_pftreestate = change_constraints_pftreestate
+
+
+(********************************************)
+(* Definition of the most primitive tactics *)
+(********************************************)
+
+let refiner = refiner
+
+(* This does not check that the variable name is not here *)
+let introduction_no_check id =
+  refiner (Prim (Intro id))
+
+(* This does not check that the dependencies are correct *)
+let intro_replacing_no_check whereid gl = 
+  refiner (Prim (Intro_replacing whereid)) gl
+
+let internal_cut_no_check id t gl = 
+  refiner (Prim (Cut (true,id,t))) gl
+
+let internal_cut_rev_no_check id t gl = 
+  refiner (Prim (Cut (false,id,t))) gl
+
+let refine_no_check c gl = 
+  refiner (Prim (Refine c)) gl
+
+let convert_concl_no_check c gl = 
+  refiner (Prim (Convert_concl c)) gl
+
+let convert_hyp_no_check d gl =
+  refiner (Prim (Convert_hyp d)) gl
+
+(* This does not check dependencies *)
+let thin_no_check ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl
+
+(* This does not check dependencies *)
+let thin_body_no_check ids gl =
+  if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
+
+let move_hyp_no_check with_dep id1 id2 gl = 
+  refiner (Prim (Move (with_dep,id1,id2))) gl
+
+let rename_hyp_no_check id1 id2 gl = 
+  refiner (Prim (Rename (id1,id2))) gl
+
+let mutual_fix f n others gl = 
+  with_check (refiner (Prim (FixRule (f,n,others)))) gl
+
+let mutual_cofix f others gl = 
+  with_check (refiner (Prim (Cofix (f,others)))) gl
+    
+let rename_bound_var_goal gls =
+  let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in 
+  let ids = ids_of_named_context sign in
+  convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls
+
+
+(* Versions with consistency checks *)
+
+let introduction id    = with_check (introduction_no_check id) 
+let intro_replacing id = with_check (intro_replacing_no_check id)
+let internal_cut d t     = with_check (internal_cut_no_check d t)
+let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
+let refine c           = with_check (refine_no_check c)
+let convert_concl d    = with_check (convert_concl_no_check d)
+let convert_hyp d      = with_check (convert_hyp_no_check d)
+let thin l             = with_check (thin_no_check l)
+let thin_body c        = with_check (thin_body_no_check c)
+let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
+let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
+    
+(* Pretty-printers *)
+
+open Pp
+open Printer
+open Tacexpr
+open Rawterm
+
+let rec pr_list f = function
+  | []   -> mt ()
+  | a::l1 -> (f a) ++ pr_list f l1
+
+let pr_gls gls =
+  hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls))
+
+let pr_glls glls =
+  hov 0 (pr_decls (sig_sig glls) ++ fnl () ++
+         prlist_with_sep pr_fnl pr_seq (sig_it glls))
+