diff options
Diffstat (limited to 'src/aac_rewrite.ml')
| -rw-r--r-- | src/aac_rewrite.ml | 425 |
1 files changed, 425 insertions, 0 deletions
diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml new file mode 100644 index 0000000..697c15c --- /dev/null +++ b/src/aac_rewrite.ml @@ -0,0 +1,425 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** aac_rewrite -- rewriting modulo A or AC*) + +open Ltac_plugin + +module Control = struct + let debug = false + let printing = false + let time = false +end + +module Debug = Helper.Debug (Control) +open Debug + +let time_tac msg tac = + if Control.time then Coq.tclTIME msg tac else tac + +let tac_or_exn tac exn msg = fun gl -> + try tac gl with e -> + let env = Tacmach.pf_env gl in + let sigma = Tacmach.project gl in + pr_constr env sigma "last goal" (Tacmach.pf_concl gl); + exn msg e + + +let retype = Coq.retype + +open EConstr +open Names +open Proof_type + + +(** aac_lift : the ideal type beyond AAC_rewrite.v/Lift + + A base relation r, together with an equivalence relation, and the + proof that the former lifts to the later. Howver, we have to + ensure manually the invariant : r.carrier == e.carrier, and that + lift connects the two things *) +type aac_lift = + { + r : Coq.Relation.t; + e : Coq.Equivalence.t; + lift : constr + } + +type rewinfo = + { + hypinfo : Coq.Rewrite.hypinfo; + + in_left : bool; (** are we rewriting in the left hand-sie of the goal *) + pattern : constr; + subject : constr; + morph_rlt : Coq.Relation.t; (** the relation we look for in morphism *) + eqt : Coq.Equivalence.t; (** the equivalence we use as workbase *) + rlt : Coq.Relation.t; (** the relation in the goal *) + lifting: aac_lift + } + +let infer_lifting (rlt: Coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = + Coq.cps_evar_relation rlt.Coq.Relation.carrier (fun e -> + let lift_ty = + mkApp (Lazy.force Theory.Stubs.lift, + [| + rlt.Coq.Relation.carrier; + rlt.Coq.Relation.r; + e + |] + ) in + Coq.cps_resolve_one_typeclass ~error:(Pp.strbrk "Cannot infer a lifting") + lift_ty (fun lift goal -> + let x = rlt.Coq.Relation.carrier in + let r = rlt.Coq.Relation.r in + let eq = (Coq.nf_evar goal e) in + let equiv = Coq.lapp Theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in + let lift = + { + r = rlt; + e = Coq.Equivalence.make x eq equiv; + lift = lift; + } + in + k ~lift:lift goal + )) + +(** Builds a rewinfo, once and for all *) +let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= + let l2r = hypinfo.Coq.Rewrite.l2r in + infer_lifting rlt + (fun ~lift -> + let eq = lift.e in + k { + hypinfo = hypinfo; + in_left = in_left; + pattern = if l2r then hypinfo.Coq.Rewrite.left else hypinfo.Coq.Rewrite.right; + subject = if in_left then left else right; + morph_rlt = Coq.Equivalence.to_relation eq; + eqt = eq; + lifting = lift; + rlt = rlt + } + ) + + + +(** {1 Tactics} *) + + +(** Build the reifiers, the reified terms, and the evaluation fonction *) +let handle eqt zero envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) k = + + let (x,r,_) = Coq.Equivalence.split eqt in + Theory.Trans.mk_reifier (Coq.Equivalence.to_relation eqt) zero envs + (fun (maps, reifier) -> + (* fold through a term and reify *) + let t = Theory.Trans.reif_constr_of_t reifier t in + let t' = Theory.Trans.reif_constr_of_t reifier t' in + (* Some letins *) + let eval = (mkApp (Lazy.force Theory.Stubs.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units|])) in + + Coq.cps_mk_letin "eval" eval (fun eval -> + Coq.cps_mk_letin "left" t (fun t -> + Coq.cps_mk_letin "right" t' (fun t' -> + k maps eval t t')))) + +(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that + is merely a proof of equality of two terms modulo AAC *) +let by_aac_reflexivity zero + eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = + handle eqt zero envs t t' + (fun maps eval t t' -> + let (x,r,e) = Coq.Equivalence.split eqt in + let decision_thm = Coq.lapp Theory.Stubs.decide_thm + [|x;r;e; + maps.Theory.Trans.env_sym; + maps.Theory.Trans.env_bin; + maps.Theory.Trans.env_units; + t;t'; + |] + in + (* 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 = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.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 (Pp.strbrk "unification failure"); + tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic (Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure"; + Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity) + (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) + ]) + ) + +let by_aac_normalise zero lift ir t t' = + let eqt = lift.e in + let rlt = lift.r in + handle eqt zero ir t t' + (fun maps eval t t' -> + let (x,r,e) = Coq.Equivalence.split eqt in + let normalise_thm = Coq.lapp Theory.Stubs.lift_normalise_thm + [|x;r;e; + maps.Theory.Trans.env_sym; + maps.Theory.Trans.env_bin; + maps.Theory.Trans.env_units; + rlt.Coq.Relation.r; + lift.lift; + t;t'; + |] + in + (* 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 = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.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; + ]) + + ) + +(** A handler tactic, that reifies the goal, and infer the liftings, + and then call its continuation *) +let aac_conclude + (k : constr -> aac_lift -> Theory.Trans.ir -> Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) = fun goal -> + + let (equation : types) = Tacmach.pf_concl goal in + let envs = Theory.Trans.empty_envs () in + let left, right,r = + match Coq.match_as_equation goal equation with + | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation" + | Some x -> x in + try infer_lifting r + (fun ~lift goal -> + let eq = Coq.Equivalence.to_relation lift.e in + let tleft,tright, goal = Theory.Trans.t_of_constr goal eq envs (left,right) in + let goal, ir = Theory.Trans.ir_of_envs goal eq envs in + let concl = Tacmach.pf_concl goal in + let env = Tacmach.pf_env goal in + let sigma = Tacmach.project goal in + let _ = pr_constr env sigma "concl "concl in + let evar_map = Tacmach.project goal in + Tacticals.tclTHEN + (Refiner.tclEVARS evar_map) + (k left lift ir tleft tright) + goal + )goal + with + | Not_found -> Coq.user_error @@ Pp.strbrk "No lifting from the goal's relation to an equivalence" + +open Tacexpr + +let aac_normalise = fun goal -> + let ids = Tacmach.pf_ids_of_hyps goal in + let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in + let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in + let norm_tac = Locus.ArgArg (None, norm_tac) in + Tacticals.tclTHENLIST + [ + aac_conclude by_aac_normalise; + Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (None, TacCall (None, (norm_tac, []))))); + Proofview.V82.of_tactic (Tactics.keep ids) + ] goal + +let aac_reflexivity = fun goal -> + aac_conclude + (fun zero lift ir t t' -> + let x,r = Coq.Relation.split (lift.r) in + let r_reflexive = (Coq.Classes.mk_reflexive x r) in + Coq.cps_resolve_one_typeclass ~error:(Pp.strbrk "The goal's relation is not reflexive") + r_reflexive + (fun reflexive -> + let lift_reflexivity = + mkApp (Lazy.force (Theory.Stubs.lift_reflexivity), + [| + x; + r; + lift.e.Coq.Equivalence.eq; + lift.lift; + reflexive + |]) + in + Tacticals.tclTHEN + + (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity))) + (fun goal -> + let concl = Tacmach.pf_concl goal in + let env = Tacmach.pf_env goal in + let sigma = Tacmach.project goal in + let _ = pr_constr env sigma "concl "concl in + by_aac_reflexivity zero lift.e ir t t' goal) + ) + ) goal + +(** A sub-tactic to lift the rewriting using Lift *) +let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): tactic = + fun goal -> + (* catch the equation and the two members*) + let concl = Tacmach.pf_concl goal in + let (left, right, _ ) = match Coq.match_as_equation goal concl with + | Some x -> x + | None -> Coq.user_error @@ Pp.strbrk "The goal is not an equation" + in + let lift_transitivity = + let thm = + if in_left + then + Lazy.force Theory.Stubs.lift_transitivity_left + else + Lazy.force Theory.Stubs.lift_transitivity_right + in + mkApp (thm, + [| + preorder.Coq.Relation.carrier; + preorder.Coq.Relation.r; + using_eq.Coq.Equivalence.eq; + lifting; + step; + left; + right; + |]) + in + Tacticals.tclTHENLIST + [ retype lift_transitivity; + Proofview.V82.of_tactic (Tactics.apply lift_transitivity) + ] goal + + +(** The core tactic for aac_rewrite. Env and sigma are for the constr *) +let core_aac_rewrite ?abort + rewinfo + subst + (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) + env sigma (tr : constr) t left : tactic = + pr_constr env sigma "transitivity through" tr; + let tran_tac = + lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt + in + Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> + Tacticals.tclTHENSV + (tac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step") + ( + if rewinfo.in_left + then [| by_aac_reflexivity left t ; rew |] + else [| by_aac_reflexivity t left ; rew |] + ) + ) + +exception NoSolutions + + +(** Choose a substitution from a + [(int * Terms.t * Env.env Search_monad.m) Search_monad.m ] *) +(* WARNING: Beware, since the printing function can change the order of the + printed monad, this function has to be updated accordingly *) +let choose_subst subterm sol m= + try + let (depth,pat,envm) = match subterm with + | None -> (* first solution *) + List.nth ( List.rev (Search_monad.to_list m)) 0 + | Some x -> + List.nth ( List.rev (Search_monad.to_list m)) x + in + let env = match sol with + None -> + List.nth ( (Search_monad.to_list envm)) 0 + | Some x -> List.nth ( (Search_monad.to_list envm)) x + in + pat, env + with + | _ -> raise NoSolutions + +(** rewrite the constr modulo AC from left to right in the left member + of the goal *) +let aac_rewrite_wrap ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> + let envs = Theory.Trans.empty_envs () in + let (concl : types) = Tacmach.pf_concl goal in + let (_,_,rlt) as concl = + match Coq.match_as_equation goal concl with + | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation" + | Some (left, right, rlt) -> left,right,rlt + in + let check_type x = + Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier + in + Coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type) + (fun hypinfo -> + dispatch in_left concl hypinfo + ( + fun rewinfo -> + let goal = + match extra with + | Some t -> Theory.Trans.add_symbol goal rewinfo.morph_rlt envs (EConstr.to_constr (Tacmach.project goal) t) + | None -> goal + in + let pattern, subject, goal = + Theory.Trans.t_of_constr goal rewinfo.morph_rlt envs + (rewinfo.pattern , rewinfo.subject) + in + let goal, ir = Theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in + + let units = Theory.Trans.ir_to_units ir in + let m = Matcher.subterm ?strict units pattern subject in + (* We sort the monad in increasing size of contet *) + let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + + if show + then + Print.print rewinfo.morph_rlt ir m (hypinfo.Coq.Rewrite.context) + + else + try + let pat,subst = choose_subst occ_subterm occ_sol m in + let tr_step = Matcher.Subst.instantiate subst pat in + let tr_step_raw = Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in + + let conv = (Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.Coq.Rewrite.context)) in + let subst = Matcher.Subst.to_list subst in + let subst = List.map (fun (x,y) -> x, conv y) subst in + let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in + let env = Tacmach.pf_env goal in + let sigma = Tacmach.project goal in + (* I'm not sure whether this is the right env/sigma for printing tr_step_raw *) + core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity env sigma tr_step_raw tr_step subject + + with + | NoSolutions -> + Tacticals.tclFAIL 0 + (Pp.str (if occ_subterm = None && occ_sol = None + then "No matching occurrence modulo AC found" + else "No such solution")) + ) + ) goal + +let get k l = try Some (List.assoc k l) with Not_found -> None + +let get_lhs l = try ignore (List.assoc "in_right" l); false with Not_found -> true + +let aac_rewrite ~args = + aac_rewrite_wrap ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) + + + +let rec add k x = function + | [] -> [k,x] + | k',_ as ky::q -> + if k'=k then Coq.user_error @@ Pp.strbrk ("redondant argument ("^k^")") + else ky::add k x q + +let pr_aac_args _ _ _ l = + List.fold_left + (fun acc -> function + | ("in_right" as s,_) -> Pp.(++) (Pp.str s) acc + | (k,i) -> Pp.(++) (Pp.(++) (Pp.str k) (Pp.int i)) acc + ) (Pp.str "") l + |