From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/tacmach.ml | 185 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 104 insertions(+), 81 deletions(-) (limited to 'proofs/tacmach.ml') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8346e4c2..fa0d0362 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -1,17 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - error ("No such hypothesis: " ^ (string_of_id id)) + raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = let (_,_,ty)= (pf_get_hyp gls id) in @@ -74,18 +69,17 @@ let pf_get_new_ids ids gls = 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_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c + (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) +let pf_eapply f gls x = + on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply +let pf_e_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 simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute @@ -93,38 +87,17 @@ let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_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_conv_x gl = pf_reduce test_conversion gl Reduction.CONV +let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL +let pf_const_value = pf_reduce (fun env _ -> constant_value_in 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 pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) -let pf_check_type gls c1 c2 = - ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) - -let pf_is_matching = pf_apply Matching.is_matching_conv -let pf_matches = pf_apply Matching.matches_conv - -(************************************) -(* Tactics handling a list of goals *) -(************************************) - -type transformation_tactic = proof_tree -> goal list - -type validation_list = proof_tree list -> proof_tree list - -type tactic_list = Refiner.tactic_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 - +let pf_is_matching = pf_apply Constr_matching.is_matching_conv +let pf_matches = pf_apply Constr_matching.matches_conv (********************************************) (* Definition of the most primitive tactics *) @@ -132,69 +105,39 @@ let tclIDTAC_list = tclIDTAC_list let refiner = refiner -(* This does not check that the variable name is not here *) -let introduction_no_check id = - refiner (Prim (Intro id)) - let internal_cut_no_check replace id t gl = - refiner (Prim (Cut (true,replace,id,t))) gl + refiner (Cut (true,replace,id,t)) gl let internal_cut_rev_no_check replace id t gl = - refiner (Prim (Cut (false,replace,id,t))) gl + refiner (Cut (false,replace,id,t)) gl let refine_no_check c gl = - refiner (Prim (Refine c)) gl - -let convert_concl_no_check c sty gl = - refiner (Prim (Convert_concl (c,sty))) gl - -let convert_hyp_no_check d gl = - refiner (Prim (Convert_hyp d)) gl + refiner (Refine c) 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 + if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl -let move_hyp_no_check with_dep id1 id2 gl = - refiner (Prim (Move (with_dep,id1,id2))) gl - -let order_hyps idl gl = - refiner (Prim (Order idl)) gl - -let rec rename_hyp_no_check l gl = match l with - | [] -> tclIDTAC gl - | (id1,id2)::l -> - tclTHEN (refiner (Prim (Rename (id1,id2)))) - (rename_hyp_no_check l) gl +let move_hyp_no_check id1 id2 gl = + refiner (Move (id1,id2)) gl let mutual_fix f n others j gl = - with_check (refiner (Prim (FixRule (f,n,others,j)))) gl + with_check (refiner (FixRule (f,n,others,j))) gl let mutual_cofix f others j gl = - with_check (refiner (Prim (Cofix (f,others,j)))) gl + with_check (refiner (Cofix (f,others,j))) gl (* Versions with consistency checks *) -let introduction id = with_check (introduction_no_check id) let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) -let convert_concl d sty = with_check (convert_concl_no_check d sty) -let convert_hyp d = with_check (convert_hyp_no_check d) let thin c = with_check (thin_no_check c) -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 l = with_check (rename_hyp_no_check l) +let move_hyp id id' = with_check (move_hyp_no_check id id') (* Pretty-printers *) open Pp -open Tacexpr -open Glob_term let db_pr_goal sigma g = let env = Goal.V82.env sigma g in @@ -209,5 +152,85 @@ let pr_gls gls = let pr_glls glls = hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls)) + prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) + +(* Variants of [Tacmach] functions built with the new proof engine *) +module New = struct + + let pf_apply f gl = + f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + + let of_old f gl = + f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl } + + let pf_global id gl = + (** We only check for the existence of an [id] in [hyps] *) + let gl = Proofview.Goal.assume gl in + let hyps = Proofview.Goal.hyps gl in + Constrintern.construct_reference hyps id + + let pf_env = Proofview.Goal.env + let pf_concl = Proofview.Goal.concl + + let pf_type_of gl t = + pf_apply type_of gl t + + let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 + + let pf_ids_of_hyps gl = + (** We only get the identifiers in [hyps] *) + let gl = Proofview.Goal.assume gl in + let hyps = Proofview.Goal.hyps gl in + ids_of_named_context hyps + + let pf_get_new_id id gl = + let ids = pf_ids_of_hyps gl in + next_ident_away id ids + + let pf_get_hyp id gl = + let hyps = Proofview.Goal.hyps gl in + let sign = + try Context.lookup_named id hyps + with Not_found -> raise (RefinerError (NoSuchHyp id)) + in + sign + + let pf_get_hyp_typ id gl = + let (_,_,ty) = pf_get_hyp id gl in + ty + + let pf_hyps_types gl = + let env = Proofview.Goal.env gl in + let sign = Environ.named_context env in + List.map (fun (id,_,x) -> (id, x)) sign + + let pf_last_hyp gl = + let hyps = Proofview.Goal.hyps gl in + List.hd hyps + + let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + (** We normalize the conclusion just after *) + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + nf_evar sigma concl + + let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + + let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t + + let pf_reduce_to_quantified_ind gl t = + pf_apply reduce_to_quantified_ind gl t + + let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_type_of gl t = + pf_whd_betadeltaiota gl (pf_get_type_of gl t) + + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t + + let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_compute gl t = pf_apply compute gl t + + let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t +end -- cgit v1.2.3