From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- proofs/tacmach.ml | 61 +++++++++++++++++++++++++++---------------------------- 1 file changed, 30 insertions(+), 31 deletions(-) (limited to 'proofs/tacmach.ml') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b740baa8..9e35abfc 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *) +(* $Id$ *) open Pp open Util open Names -open Nameops +open Namegen open Sign open Term open Termops @@ -55,10 +55,10 @@ 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 +let pf_get_hyp gls id = + try Sign.lookup_named id (pf_hyps gls) - with Not_found -> + with Not_found -> error ("No such hypothesis: " ^ (string_of_id id)) let pf_get_hyp_typ gls id = @@ -67,7 +67,7 @@ let pf_get_hyp_typ gls id = let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) -let pf_get_new_id id gls = +let pf_get_new_id id gls = next_ident_away id (pf_ids_of_hyps gls) let pf_get_new_ids ids gls = @@ -77,19 +77,19 @@ let pf_get_new_ids ids gls = ids [] let pf_interp_constr gls c = - let evc = project gls in + let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c let pf_interp_type gls c = - let evc = project gls in + 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_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c +let pf_reduction_of_red_expr gls re c = + (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply @@ -98,7 +98,7 @@ 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 = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) @@ -111,11 +111,14 @@ 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_get_type_of gls) +let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) -let pf_check_type gls c1 c2 = +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 *) (************************************) @@ -176,16 +179,16 @@ let refiner = refiner let introduction_no_check id = refiner (Prim (Intro id)) -let internal_cut_no_check replace id t gl = +let internal_cut_no_check replace id t gl = refiner (Prim (Cut (true,replace,id,t))) gl -let internal_cut_rev_no_check replace id t gl = +let internal_cut_rev_no_check replace id t gl = refiner (Prim (Cut (false,replace,id,t))) gl -let refine_no_check c gl = +let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl_no_check c sty gl = +let convert_concl_no_check c sty gl = refiner (Prim (Convert_concl (c,sty))) gl let convert_hyp_no_check d gl = @@ -199,31 +202,27 @@ let thin_no_check ids gl = 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 = +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)))) +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 mutual_fix_with_index f n others j gl = +let mutual_fix f n others j gl = with_check (refiner (Prim (FixRule (f,n,others,j)))) gl -let mutual_fix f n others = mutual_fix_with_index f n others 0 - -let mutual_cofix_with_index f others j gl = +let mutual_cofix f others j gl = with_check (refiner (Prim (Cofix (f,others,j)))) gl -let mutual_cofix f others = mutual_cofix_with_index f others 0 - (* Versions with consistency checks *) -let introduction id = with_check (introduction_no_check id) +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) @@ -231,7 +230,7 @@ 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 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) (* Pretty-printers *) @@ -250,4 +249,4 @@ let pr_gls gls = let pr_glls glls = hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) - + -- cgit v1.2.3