diff options
Diffstat (limited to 'AAC_rewrite.ml')
| -rw-r--r-- | AAC_rewrite.ml | 315 |
1 files changed, 157 insertions, 158 deletions
diff --git a/AAC_rewrite.ml b/AAC_rewrite.ml index bdba9cb..be286f9 100644 --- a/AAC_rewrite.ml +++ b/AAC_rewrite.ml @@ -9,20 +9,20 @@ (** aac_rewrite -- rewriting modulo *) -module Control = struct +module Control = struct let debug = false let printing = false let time = false end -module Debug = AAC_helper.Debug (Control) +module Debug = AAC_helper.Debug (Control) open Debug let time_tac msg tac = if Control.time then AAC_coq.tclTIME msg tac else tac -let tac_or_exn tac exn msg = fun gl -> - try tac gl with e -> +let tac_or_exn tac exn msg = fun gl -> + try tac gl with e -> pr_constr "last goal" (Tacmach.pf_concl gl); exn msg e @@ -37,7 +37,7 @@ module M = AAC_matcher open Term open Names open Coqlib -open Proof_type +open Proof_type (** The various kind of relation we can encounter, as a hierarchy *) type rew_relation = @@ -46,12 +46,12 @@ type rew_relation = | Equivalence of AAC_coq.Equivalence.t (** {!promote try to go higher in the aforementionned hierarchy} *) -let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = - try AAC_coq.Equivalence.cps_from_relation rlt +let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = + try AAC_coq.Equivalence.cps_from_relation rlt (fun e -> k (Equivalence e)) with - | Not_found -> - begin + | Not_found -> + begin try AAC_coq.Transitive.cps_from_relation rlt (fun trans -> k (Transitive trans)) with @@ -61,13 +61,13 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = (* Various situations: - p == q |- left == right : rewrite <- -> - p <= q |- left <= right : rewrite -> + p == q |- left == right : rewrite <- -> + p <= q |- left <= right : rewrite -> p <= q |- left == right : failure p == q |- left <= right : rewrite <- -> - + Not handled - p <= q |- left >= right : failure + p <= q |- left >= right : failure *) (** aac_lift : the ideal type beyond AAC.v/AAC_lift @@ -78,15 +78,15 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = lift connects the two things *) type aac_lift = { - r : AAC_coq.Relation.t; + r : AAC_coq.Relation.t; e : AAC_coq.Equivalence.t; - lift : Term.constr + lift : Term.constr } - + type rewinfo = { hypinfo : AAC_coq.Rewrite.hypinfo; - + in_left : bool; (** are we rewriting in the left hand-sie of the goal *) pattern : constr; subject : constr; @@ -97,9 +97,9 @@ type rewinfo = } let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = - AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e -> - let lift_ty = - mkApp (Lazy.force AAC_theory.Stubs.lift, + AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e -> + let lift_ty = + mkApp (Lazy.force AAC_theory.Stubs.lift, [| rlt.AAC_coq.Relation.carrier; rlt.AAC_coq.Relation.r; @@ -107,11 +107,11 @@ let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tac |] ) in AAC_coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting" - lift_ty (fun lift goal -> - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in - let eq = (AAC_coq.nf_evar goal e) in - let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in + lift_ty (fun lift goal -> + let x = rlt.AAC_coq.Relation.carrier in + let r = rlt.AAC_coq.Relation.r in + let eq = (AAC_coq.nf_evar goal e) in + let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in let lift = { r = rlt; @@ -120,14 +120,14 @@ let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tac } 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 dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= let l2r = hypinfo.AAC_coq.Rewrite.l2r in - infer_lifting rlt + infer_lifting rlt (fun ~lift -> - let eq = lift.e in + let eq = lift.e in k { hypinfo = hypinfo; in_left = in_left; @@ -137,10 +137,10 @@ let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) eqt = eq; lifting = lift; rlt = rlt - } + } ) - - + + (** {1 Tactics} *) @@ -148,34 +148,34 @@ let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) (** Build the reifiers, the reified terms, and the evaluation fonction *) let handle eqt zero envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) k = - let (x,r,_) = AAC_coq.Equivalence.split eqt in - AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs - (fun (maps, reifier) -> + let (x,r,_) = AAC_coq.Equivalence.split eqt in + AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs + (fun (maps, reifier) -> (* fold through a term and reify *) - let t = AAC_theory.Trans.reif_constr_of_t reifier t in + let t = AAC_theory.Trans.reif_constr_of_t reifier t in let t' = AAC_theory.Trans.reif_constr_of_t reifier t' in (* Some letins *) let eval = (mkApp (Lazy.force AAC_theory.Stubs.eval, [|x;r; maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units|])) in - + AAC_coq.cps_mk_letin "eval" eval (fun eval -> - AAC_coq.cps_mk_letin "left" t (fun t -> - AAC_coq.cps_mk_letin "right" t' (fun t' -> + AAC_coq.cps_mk_letin "left" t (fun t -> + AAC_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 *) + is merely a proof of equality of two terms modulo AAC *) let by_aac_reflexivity zero eqt envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) : Proof_type.tactic = - handle eqt zero envs t t' + handle eqt zero envs t t' (fun maps eval t t' -> - let (x,r,e) = AAC_coq.Equivalence.split eqt in + let (x,r,e) = AAC_coq.Equivalence.split eqt in let decision_thm = AAC_coq.lapp AAC_theory.Stubs.decide_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; + [|x;r;e; + maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units; t;t'; - |] + |] in (* This convert is required to deal with evars in a proper way *) @@ -193,20 +193,20 @@ let by_aac_reflexivity zero ) 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) = AAC_coq.Equivalence.split eqt in + 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) = AAC_coq.Equivalence.split eqt in let normalise_thm = AAC_coq.lapp AAC_theory.Stubs.lift_normalise_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; + [|x;r;e; + maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units; rlt.AAC_coq.Relation.r; lift.lift; t;t'; - |] + |] in (* This convert is required to deal with evars in a proper way *) @@ -223,37 +223,36 @@ let by_aac_normalise zero lift ir t t' = (** A handler tactic, that reifies the goal, and infer the liftings, and then call its continuation *) -let aac_conclude - (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal -> +let aac_conclude + (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal -> - let (equation : Term.types) = Tacmach.pf_concl goal in - let envs = AAC_theory.Trans.empty_envs () in - let left, right,r = + let (equation : Term.types) = Tacmach.pf_concl goal in + let envs = AAC_theory.Trans.empty_envs () in + let left, right,r = match AAC_coq.match_as_equation goal equation with | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some x -> x in - try infer_lifting r + | Some x -> x in + try infer_lifting r (fun ~lift goal -> - let eq = AAC_coq.Equivalence.to_relation lift.e in - let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in - let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in - let evar_map = Tacmach.project goal in + let eq = AAC_coq.Equivalence.to_relation lift.e in + let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in + let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "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 + goal + )goal + with | Not_found -> AAC_coq.user_error "No lifting from the goal's relation to an equivalence" -open Libnames +open Libnames open Tacinterp -open Q_coqast -let aac_normalise = fun goal -> - let ids = Tacmach.pf_ids_of_hyps goal in +let aac_normalise = fun goal -> + let ids = Tacmach.pf_ids_of_hyps goal in Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; @@ -271,17 +270,17 @@ let aac_normalise = fun goal -> Tactics.keep ids ] goal -let aac_reflexivity = fun goal -> - aac_conclude - (fun zero lift ir t t' -> - let x,r = AAC_coq.Relation.split (lift.r) in - let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in - AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" +let aac_reflexivity = fun goal -> + aac_conclude + (fun zero lift ir t t' -> + let x,r = AAC_coq.Relation.split (lift.r) in + let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in + AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" r_reflexive (fun reflexive -> - let lift_reflexivity = - mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), - [| + let lift_reflexivity = + mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), + [| x; r; lift.e.AAC_coq.Equivalence.eq; @@ -291,33 +290,33 @@ let aac_reflexivity = fun goal -> in Tacticals.tclTHEN (Tactics.apply lift_reflexivity) - (fun goal -> - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in + (fun goal -> + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "concl "concl in by_aac_reflexivity zero lift.e ir t t' goal) ) ) goal (** A sub-tactic to lift the rewriting using AAC_lift *) -let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic = +let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic = fun goal -> (* catch the equation and the two members*) - let concl = Tacmach.pf_concl goal in - let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with + let concl = Tacmach.pf_concl goal in + let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with | Some x -> x | None -> AAC_coq.user_error "The goal is not an equation" - in - let lift_transitivity = - let thm = - if in_left + in + let lift_transitivity = + let thm = + if in_left then Lazy.force AAC_theory.Stubs.lift_transitivity_left else Lazy.force AAC_theory.Stubs.lift_transitivity_right in - mkApp (thm, - [| - preorder.AAC_coq.Relation.carrier; + mkApp (thm, + [| + preorder.AAC_coq.Relation.carrier; preorder.AAC_coq.Relation.r; using_eq.AAC_coq.Equivalence.eq; lifting; @@ -326,7 +325,7 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq right; |]) in - Tacticals.tclTHENLIST + Tacticals.tclTHENLIST [ Tactics.apply lift_transitivity ] goal @@ -334,19 +333,19 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq (** The core tactic for aac_rewrite *) let core_aac_rewrite ?abort - rewinfo + rewinfo subst (by_aac_reflexivity : AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) - (tr : constr) t left : tactic = - pr_constr "transitivity through" tr; + (tr : constr) t left : tactic = + pr_constr "transitivity through" tr; let tran_tac = lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt in - AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> + AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> Tacticals.tclTHENSV (tac_or_exn (tran_tac) AAC_coq.anomaly "Unable to make the transitivity step") ( - if rewinfo.in_left + if rewinfo.in_left then [| by_aac_reflexivity left t ; rew |] else [| by_aac_reflexivity t left ; rew |] ) @@ -355,23 +354,23 @@ let core_aac_rewrite ?abort exception NoSolutions -(** Choose a substitution from a +(** Choose a substitution from a [(int * Terms.t * Env.env AAC_search_monad.m) AAC_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 + try + let (depth,pat,envm) = match subterm with | None -> (* first solution *) - List.nth ( List.rev (AAC_search_monad.to_list m)) 0 - | Some x -> - List.nth ( List.rev (AAC_search_monad.to_list m)) x - in - let env = match sol with + List.nth ( List.rev (AAC_search_monad.to_list m)) 0 + | Some x -> + List.nth ( List.rev (AAC_search_monad.to_list m)) x + in + let env = match sol with None -> List.nth ( (AAC_search_monad.to_list envm)) 0 - | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x - in + | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x + in pat, env with | _ -> raise NoSolutions @@ -379,66 +378,66 @@ let choose_subst subterm sol m= (** rewrite the constr modulo AC from left to right in the left member of the goal *) let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> - let envs = AAC_theory.Trans.empty_envs () in - let (concl : Term.types) = Tacmach.pf_concl goal in + let envs = AAC_theory.Trans.empty_envs () in + let (concl : Term.types) = Tacmach.pf_concl goal in let (_,_,rlt) as concl = match AAC_coq.match_as_equation goal concl with | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some (left, right, rlt) -> left,right,rlt + | Some (left, right, rlt) -> left,right,rlt in - let check_type x = + let check_type x = Tacmach.pf_conv_x goal x rlt.AAC_coq.Relation.carrier in AAC_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 -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t + fun rewinfo -> + let goal = + match extra with + | Some t -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t | None -> goal in - let pattern, subject, goal = - AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs - (rewinfo.pattern , rewinfo.subject) - in - let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in - - let units = AAC_theory.Trans.ir_to_units ir in - let m = AAC_matcher.subterm ?strict units pattern subject in + let pattern, subject, goal = + AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs + (rewinfo.pattern , rewinfo.subject) + in + let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in + + let units = AAC_theory.Trans.ir_to_units ir in + let m = AAC_matcher.subterm ?strict units pattern subject in (* We sort the monad in increasing size of contet *) - let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - + let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + if show - then - AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context) + then + AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context) else - try - let pat,subst = choose_subst occ_subterm occ_sol m in - let tr_step = AAC_matcher.Subst.instantiate subst pat in - let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in + try + let pat,subst = choose_subst occ_subterm occ_sol m in + let tr_step = AAC_matcher.Subst.instantiate subst pat in + let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in - let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in + let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in let subst = AAC_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 - core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject - - with - | NoSolutions -> - Tacticals.tclFAIL 0 - (Pp.str (if occ_subterm = None && occ_sol = None - then "No matching occurence modulo AC found" - else "No such solution")) - ) + 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 + core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject + + with + | NoSolutions -> + Tacticals.tclFAIL 0 + (Pp.str (if occ_subterm = None && occ_sol = None + then "No matching occurence modulo AC found" + else "No such solution")) + ) ) goal open Rewrite open Tacmach -open Tacticals +open Tacticals open Tacexpr open Tacinterp open Extraargs @@ -454,19 +453,19 @@ let get k l = try Some (List.assoc k l) with Not_found -> None let get_lhs l = try List.assoc "in_right" l; false with Not_found -> true -let aac_rewrite ~args = +let aac_rewrite ~args = aac_rewrite ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) -let pr_aac_args _ _ _ l = - List.fold_left +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 -ARGUMENT EXTEND aac_args -TYPED AS ((string * int) list ) +ARGUMENT EXTEND aac_args +TYPED AS ((string * int) list ) PRINTED BY pr_aac_args | [ "at" integer(n) aac_args(q) ] -> [ add "at" n q ] | [ "subst" integer(n) aac_args(q) ] -> [ add "subst" n q ] @@ -475,12 +474,12 @@ PRINTED BY pr_aac_args END let pr_constro _ _ _ = fun b -> - match b with + match b with | None -> Pp.str "" | Some o -> Pp.str "<constr>" ARGUMENT EXTEND constro -TYPED AS (constr option) +TYPED AS (constr option) PRINTED BY pr_constro | [ "[" constr(c) "]" ] -> [ Some c ] | [ ] -> [ None ] @@ -498,7 +497,7 @@ 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 ] 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 ] @@ -513,7 +512,7 @@ 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 ] 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 ] |