From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 20 Sep 2012 09:41:14 +0200 Subject: Imported Upstream version 0.3 --- AAC_rewrite.ml | 524 --------------------------------------------------------- 1 file changed, 524 deletions(-) delete mode 100644 AAC_rewrite.ml (limited to 'AAC_rewrite.ml') diff --git a/AAC_rewrite.ml b/AAC_rewrite.ml deleted file mode 100644 index be286f9..0000000 --- a/AAC_rewrite.ml +++ /dev/null @@ -1,524 +0,0 @@ -(***************************************************************************) -(* 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 *) - - -module Control = struct - let debug = false - let printing = false - let time = false -end - -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 -> - pr_constr "last goal" (Tacmach.pf_concl gl); - exn msg e - -(* 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 - | _ -> AAC_coq.anomaly msg - -module M = AAC_matcher - -open Term -open Names -open Coqlib -open Proof_type - -(** The various kind of relation we can encounter, as a hierarchy *) -type rew_relation = - | Bare of AAC_coq.Relation.t - | Transitive of AAC_coq.Transitive.t - | 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 - (fun e -> k (Equivalence e)) - with - | Not_found -> - begin - try AAC_coq.Transitive.cps_from_relation rlt - (fun trans -> k (Transitive trans)) - with - |Not_found -> k (Bare rlt) - end - - -(* - Various situations: - 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 -*) - -(** aac_lift : the ideal type beyond AAC.v/AAC_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 : AAC_coq.Relation.t; - e : AAC_coq.Equivalence.t; - 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; - morph_rlt : AAC_coq.Relation.t; (** the relation we look for in morphism *) - eqt : AAC_coq.Equivalence.t; (** the equivalence we use as workbase *) - rlt : AAC_coq.Relation.t; (** the relation in the goal *) - lifting: aac_lift - } - -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, - [| - rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - e - |] - ) 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 - let lift = - { - r = rlt; - e = AAC_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.AAC_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.AAC_coq.Rewrite.left else hypinfo.AAC_coq.Rewrite.right; - subject = if in_left then left else right; - morph_rlt = AAC_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 : 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) -> - (* 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 - (* 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' -> - 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 : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) : Proof_type.tactic = - handle eqt zero envs t t' - (fun maps eval t t' -> - 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; - 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 *) - 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 - (Tacticals.tclTHENLIST - [ - convert ; - tac_or_exn apply_tac AAC_coq.user_error "unification failure"; - tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) AAC_coq.anomaly "vm_compute failure"; - Tacticals.tclORELSE 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) = 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; - 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 *) - let convert_to = mkApp (rlt.AAC_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 - (Tacticals.tclTHENLIST - [ - convert ; - apply_tac; - ]) - - ) - -(** 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 (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 - (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 - Tacticals.tclTHEN - (Refiner.tclEVARS evar_map) - (k left lift ir tleft tright) - goal - )goal - with - | Not_found -> AAC_coq.user_error "No lifting from the goal's relation to an equivalence" - -open Libnames -open Tacinterp - -let aac_normalise = fun goal -> - let ids = Tacmach.pf_ids_of_hyps goal in - Tacticals.tclTHENLIST - [ - aac_conclude by_aac_normalise; - Tacinterp.interp ( - <:tactic< - intro x; - intro y; - vm_compute in x; - vm_compute in y; - unfold x; - unfold y; - compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl - >> - ); - 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" - r_reflexive - (fun reflexive -> - let lift_reflexivity = - mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), - [| - x; - r; - lift.e.AAC_coq.Equivalence.eq; - lift.lift; - reflexive - |]) - in - Tacticals.tclTHEN - (Tactics.apply lift_reflexivity) - (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 = - 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 - | Some x -> x - | None -> AAC_coq.user_error "The goal is not an equation" - 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; - preorder.AAC_coq.Relation.r; - using_eq.AAC_coq.Equivalence.eq; - lifting; - step; - left; - right; - |]) - in - Tacticals.tclTHENLIST - [ - Tactics.apply lift_transitivity - ] goal - - -(** The core tactic for aac_rewrite *) -let core_aac_rewrite ?abort - 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; - 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 -> - Tacticals.tclTHENSV - (tac_or_exn (tran_tac) AAC_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 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 - | 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 - None -> - List.nth ( (AAC_search_monad.to_list envm)) 0 - | Some x -> List.nth ( (AAC_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 ?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 (_,_,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 - in - 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 - | 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 - (* We sort the monad in increasing size of contet *) - 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) - - 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 - - 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")) - ) - ) goal - - -open Rewrite -open Tacmach -open Tacticals -open Tacexpr -open Tacinterp -open Extraargs -open Genarg - -let rec add k x = function - | [] -> [k,x] - | k',_ as ky::q -> - if k'=k then AAC_coq.user_error ("redondant argument ("^k^")") - else ky::add k x q - -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 = - 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 - (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 ) -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 ] -| [ "in_right" aac_args(q) ] -> [ add "in_right" 0 q ] -| [ ] -> [ [] ] -END - -let pr_constro _ _ _ = fun b -> - match b with - | None -> Pp.str "" - | Some o -> Pp.str "" - -ARGUMENT EXTEND constro -TYPED AS (constr option) -PRINTED BY pr_constro -| [ "[" constr(c) "]" ] -> [ Some c ] -| [ ] -> [ None ] -END - -TACTIC EXTEND _aac_reflexivity_ -| [ "aac_reflexivity" ] -> [ aac_reflexivity ] -END - -TACTIC EXTEND _aac_normalise_ -| [ "aac_normalise" ] -> [ 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 ] -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 ] -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 ] -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 ] -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 ] -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 -- cgit v1.2.3