From 17564e4922acda6b72bf39de7a8c23ed0c0178f6 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:21:44 -0400 Subject: Imported Upstream version 8.5.1 --- rewrite.ml4 | 95 ++++++++++++++++++------------------------------------------- 1 file changed, 27 insertions(+), 68 deletions(-) (limited to 'rewrite.ml4') diff --git a/rewrite.ml4 b/rewrite.ml4 index 383d706..b3e52e0 100644 --- a/rewrite.ml4 +++ b/rewrite.ml4 @@ -8,6 +8,7 @@ (** aac_rewrite -- rewriting modulo *) +DECLARE PLUGIN "aac" module Control = struct let debug = false @@ -26,16 +27,15 @@ let tac_or_exn tac exn msg = fun gl -> pr_constr "last goal" (Tacmach.pf_concl gl); exn msg e + +let retype = Coq.retype + (* helper to be used with the previous function: raise a new anomaly except if a another one was previously raised *) let push_anomaly msg = function - | Util.Anomaly _ as e -> raise e + | e when Errors.is_anomaly e -> raise e | _ -> Coq.anomaly msg - - - - module M = Matcher open Term @@ -184,14 +184,14 @@ let by_aac_reflexivity zero (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply decision_thm in + let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in + let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in (Tacticals.tclTHENLIST - [ + [ retype decision_thm; retype convert_to; convert ; tac_or_exn apply_tac Coq.user_error "unification failure"; tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure"; - Tacticals.tclORELSE Tactics.reflexivity + Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity) (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) ]) ) @@ -215,10 +215,10 @@ let by_aac_normalise zero lift ir t t' = (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply normalise_thm in + let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in + let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in (Tacticals.tclTHENLIST - [ + [ retype normalise_thm; retype convert_to; convert ; apply_tac; ]) @@ -260,6 +260,7 @@ let aac_normalise = fun goal -> Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; + Proofview.V82.of_tactic begin Tacinterp.interp ( <:tactic< intro x; @@ -270,8 +271,8 @@ let aac_normalise = fun goal -> unfold y; compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl >> - ); - Tactics.keep ids + )end; + Proofview.V82.of_tactic (Tactics.keep ids) ] goal let aac_reflexivity = fun goal -> @@ -293,7 +294,8 @@ let aac_reflexivity = fun goal -> |]) in Tacticals.tclTHEN - (Tactics.apply lift_reflexivity) + + (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity))) (fun goal -> let concl = Tacmach.pf_concl goal in let _ = pr_constr "concl "concl in @@ -330,8 +332,8 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ |]) in Tacticals.tclTHENLIST - [ - Tactics.apply lift_transitivity + [ retype lift_transitivity; + Proofview.V82.of_tactic (Tactics.apply lift_transitivity) ] goal @@ -439,41 +441,6 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ) goal -(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against - the pattern, and introduces an hypothesis H of type p = t. (Note - that we have performed the substitution in p). -*) - -let aac_match ~eq pattern term h = fun gl -> - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let carrier = Typing.type_of env evar_map term in - let rel = Coq.Relation.make carrier eq in - let equiv,gl = Coq.Equivalence.from_relation gl rel in - (* first, we decompose the pattern as an arity. *) - let x_args, pat = Term.decompose_lam pattern in - (* then, we reify the pattern and the term, using the provided equality *) - let envs = Theory.Trans.empty_envs () in - let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in - let gl,ir = Theory.Trans.ir_of_envs gl rel envs in - let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in - (* then, we pick the first solution to the matching problem *) - let sigma = match Search_monad.choose solutions with - | None -> Coq.user_error "no solution to the matching problem" - | Some sigma -> sigma - in - let p_sigma = Matcher.Subst.instantiate sigma left in - let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in - (* Then, we have to assert the fact that p_sigma is equal to term *) - let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in - let evar_map = Tacmach.project gl in - Tacticals.tclTHENLIST - [ - Refiner.tclEVARS evar_map; - Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right); - ] gl - - open Coq.Rewrite open Tacmach open Tacticals @@ -525,47 +492,39 @@ PRINTED BY pr_constro END TACTIC EXTEND _aac_reflexivity_ -| [ "aac_reflexivity" ] -> [ aac_reflexivity ] +| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ] END TACTIC EXTEND _aac_normalise_ -| [ "aac_normalise" ] -> [ aac_normalise ] +| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ] END TACTIC EXTEND _aac_rewrite_ | [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl) ] END TACTIC EXTEND _aac_pattern_ | [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl) ] END TACTIC EXTEND _aac_instances_ | [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl) ] END TACTIC EXTEND _aacu_rewrite_ | [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl) ] END TACTIC EXTEND _aacu_pattern_ | [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl) ] END TACTIC EXTEND _aacu_instances_ | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ] -END - -TACTIC EXTEND _aac_match_ -| [ "aac_match" constr(p) constr(t) ident(h)] -> - [ fun gl -> - let ty = Tacmach.pf_type_of gl t in - let eq = Coq.Leibniz.eq ty in - aac_match ~eq p t (Names.Name h) gl] + [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ] END -- cgit v1.2.3