summaryrefslogtreecommitdiff
path: root/aac_rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'aac_rewrite.ml')
-rw-r--r--aac_rewrite.ml308
1 files changed, 308 insertions, 0 deletions
diff --git a/aac_rewrite.ml b/aac_rewrite.ml
new file mode 100644
index 0000000..c4c88e0
--- /dev/null
+++ b/aac_rewrite.ml
@@ -0,0 +1,308 @@
+(***************************************************************************)
+(* 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 *)
+
+(* functions to handle the failures of our tactic. Some should be
+ reported [anomaly], some are on behalf of the user [user_error]*)
+let anomaly msg =
+ Util.anomaly ("aac_tactics: " ^ msg)
+
+let user_error msg =
+ Util.error ("aac_tactics: " ^ msg)
+
+(* debug and timing functions *)
+let debug = false
+let printing = false
+let time = false
+
+let debug x =
+ if debug then
+ Printf.printf "%s\n%!" x
+
+let pr_constr msg constr =
+ if printing then
+ ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg));
+ Pp.msgnl (Printer.pr_constr constr);
+ )
+
+let time msg tac =
+ if time then Coq.tclTIME msg tac
+ else tac
+
+let tac_or_exn tac exn msg =
+ fun gl -> try tac gl with e -> 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
+ | _ -> anomaly msg
+
+module M = Matcher
+
+open Term
+open Names
+open Coqlib
+open Proof_type
+
+
+(** [find_applied_equivalence goal eq] try to ensure that the goal is
+ an applied equivalence relation, with two operands of the same type.
+
+ This function is transitionnal, as we plan to integrate with the
+ new rewrite features of Coq 8.3, that seems to handle this kind of
+ things.
+*)
+let find_applied_equivalence goal : Term.constr -> Coq.eqtype *Term.constr *Term.constr* Coq.goal_sigma = fun equation ->
+ let env = Tacmach.pf_env goal in
+ let evar_map = Tacmach.project goal in
+ match Coq.decomp_term equation with
+ | App(c,ca) when Array.length ca >= 2 ->
+ let n = Array.length ca in
+ let left = ca.(n-2) in
+ let right = ca.(n-1) in
+ let left_type = Tacmach.pf_type_of goal left in
+ (* let right_type = Tacmach.pf_type_of goal right in *)
+ let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in
+ let eq_type = Coq.Classes.mk_equivalence left_type partial_app in
+ begin
+ try
+ let evar_map, equivalence = Typeclasses.resolve_one_typeclass env evar_map eq_type in
+ let goal = Coq.goal_update goal evar_map in
+ ((left_type, partial_app), equivalence),left, right, goal
+ with
+ | Not_found -> user_error "The goal is not an applied equivalence"
+ end
+ | _ -> user_error "The goal is not an equation"
+
+
+(* [find_applied_equivalence_force] brutally decomposes the given
+ equation, and fail if we find a relation that is not the same as
+ the one we look for [r] *)
+let find_applied_equivalence_force rlt goal : Term.constr -> Term.constr *Term.constr* Coq.goal_sigma = fun equation ->
+ match Coq.decomp_term equation with
+ | App(c,ca) when Array.length ca >= 2 ->
+ let n = Array.length ca in
+ let left = ca.(n-2) in
+ let right = ca.(n-1) in
+ let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in
+ let _ = if snd rlt = partial_app then () else user_error "The goal and the hypothesis have different top-level relations" in
+
+ left, right, goal
+ | _ -> user_error "The hypothesis is not an equation"
+
+
+
+(** Build a couple of [t] from an hypothesis (variable names are not
+ relevant) *)
+let rec t_of_hyp goal rlt envs e = match Coq.decomp_term e with
+ | Prod (name,ty,c) -> let x, y = t_of_hyp goal rlt envs c
+ in x,y+1
+ | _ ->
+ let l,r ,goal = find_applied_equivalence_force rlt goal e in
+ let l,goal = Theory.Trans.t_of_constr goal rlt envs l in
+ let r,goal = Theory.Trans.t_of_constr goal rlt envs r in
+ (l,r),0
+
+(** @deprecated: [option_rip] will be removed as soon as a proper interface is
+ given to the user *)
+let option_rip = function | Some x -> x | None -> raise Not_found
+
+let mk_hyp_app conv c env =
+ let l = Matcher.Subst.to_list env in
+ let l = List.sort (fun (x,_) (y,_) -> compare y x) l in
+ let l = List.map (fun x -> conv (snd x)) l in
+ let v = Array.of_list l in
+ mkApp (c,v)
+
+
+
+(** {1 Tactics} *)
+
+(** [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 eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = fun goal ->
+ let maps, reifier,reif_letins = Theory.Trans.mk_reifier eqt envs goal in
+ let ((x,r),e) = eqt in
+
+ (* 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, eval_letin = Coq.mk_letin' "eval_name" (mkApp (Lazy.force Theory.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum|])) in
+ let _ = pr_constr "left" t in
+ let _ = pr_constr "right" t' in
+ let t , t_letin = Coq.mk_letin "left" t in
+ let t', t_letin'= Coq.mk_letin "right" t' in
+ let apply_tac = Tactics.apply (
+ mkApp (Lazy.force Theory.decide_thm, [|x;r;e; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum;t;t'|]))
+ in
+ Tactics.tclABSTRACT None
+ (Tacticals.tclTHENLIST
+ [
+ tac_or_exn reif_letins anomaly "invalid letin (1)";
+ tac_or_exn eval_letin anomaly "invalid letin (2)";
+ tac_or_exn t_letin anomaly "invalid letin (3)";
+ tac_or_exn t_letin' anomaly "invalid letin (4)";
+ tac_or_exn apply_tac anomaly "could not apply the decision theorem";
+ tac_or_exn (time "vm_norm" (Tactics.normalise_vm_in_concl)) anomaly "vm_compute failure";
+ Tacticals.tclORELSE Tactics.reflexivity
+ (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
+ ])
+ goal
+
+
+(** The core tactic for aac_rewrite *)
+let core_aac_rewrite ?(l2r = true) envs eqt rew p subst left = fun goal ->
+ let rlt = fst eqt in
+ let t = Matcher.Subst.instantiate subst p in
+ let tr = Theory.Trans.raw_constr_of_t envs rlt t in
+ let tac_rew_l2r =
+ if l2r then Equality.rewriteLR rew else Equality.rewriteRL rew
+ in
+ pr_constr "transitivity through" tr;
+ Tacticals.tclTHENSV
+ (tac_or_exn (Tactics.transitivity tr) anomaly "Unable to make the transitivity step")
+ [|
+ (* si by_aac_reflexivity foire (pas un theoreme), il fait tclFAIL, et on rattrape ici *)
+ tac_or_exn (time "by_aac_refl" (by_aac_reflexivity eqt envs left t)) push_anomaly "Invalid transitivity step";
+ tac_or_exn (tac_rew_l2r) anomaly "Unable to rewrite";
+ |] goal
+
+exception NoSolutions
+
+(** Choose a substitution from a
+ [(int * Terms.t * Env.env Search.m) Search.m ] *)
+let choose_subst subterm sol m=
+ try
+ let (depth,pat,envm) = match subterm with
+ | None -> (* first solution *)
+ option_rip (Matcher.Search.choose m)
+ | Some x ->
+ List.nth (List.rev (Matcher.Search.to_list m)) x
+ in
+ let env = match sol with
+ None -> option_rip (Matcher.Search.choose envm)
+ | Some x -> List.nth (List.rev (Matcher.Search.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 rew ?(l2r=true) ?(show = false) ?strict ?occ_subterm ?occ_sol : Proof_type.tactic = fun goal ->
+ let envs = Theory.Trans.empty_envs () in
+ let rew_type = Tacmach.pf_type_of goal rew in
+ let (gl : Term.types) = Tacmach.pf_concl goal in
+ let _ = pr_constr "h" rew_type in
+ let _ = pr_constr "gl" gl in
+ let eqt, left, right, goal = find_applied_equivalence goal gl in
+ let rlt = fst eqt in
+ let left,goal = Theory.Trans.t_of_constr goal rlt envs left in
+ let right,goal = Theory.Trans.t_of_constr goal rlt envs right in
+ let (hleft,hright),hn = t_of_hyp goal rlt envs rew_type in
+ let pattern = if l2r then hleft else hright in
+ let m = Matcher.subterm ?strict pattern left in
+
+ let m = Matcher.Search.sort (fun (x,_,_) (y,_,_) -> x - y) m in
+ if show
+ then
+ let _ = Pp.msgnl (Pp.str "All solutions:") in
+ let _ = Pp.msgnl (Matcher.pp_all (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t envs rlt t) ) m) in
+ Tacticals.tclIDTAC goal
+ else
+ try
+ let pat,env = choose_subst occ_subterm occ_sol m in
+ let rew = mk_hyp_app (Theory.Trans.raw_constr_of_t envs rlt )rew env in
+ core_aac_rewrite ~l2r envs eqt rew pat env left goal
+ with
+ | NoSolutions -> Tacticals.tclFAIL 0
+ (Pp.str (if occ_subterm = None && occ_sol = None
+ then "No matching subterm found"
+ else "No such solution")) goal
+
+
+let aac_reflexivity : Proof_type.tactic = fun goal ->
+ let (gl : Term.types) = Tacmach.pf_concl goal in
+ let envs = Theory.Trans.empty_envs() in
+ let eqt, left, right, evar_map = find_applied_equivalence goal gl in
+ let rlt = fst eqt in
+ let left,goal = Theory.Trans.t_of_constr goal rlt envs left in
+ let right,goal = Theory.Trans.t_of_constr goal rlt envs right in
+ by_aac_reflexivity eqt envs left right goal
+
+
+open Tacmach
+open Tacticals
+open Tacexpr
+open Tacinterp
+open Extraargs
+
+ (* Adding entries to the grammar of tactics *)
+TACTIC EXTEND _aac1_
+| [ "aac_reflexivity" ] -> [ aac_reflexivity ]
+END
+
+
+TACTIC EXTEND _aac2_
+| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:j c gl ]
+END
+
+TACTIC EXTEND _aac3_
+| [ "aac_rewrite" orient(o) constr(c) "subst" integer(j)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:0 ~occ_sol:j c gl ]
+END
+
+TACTIC EXTEND _aac4_
+| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:0 c gl ]
+END
+
+TACTIC EXTEND _aac5_
+| [ "aac_rewrite" orient(o) constr(c) ] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~strict:true c gl ]
+END
+
+TACTIC EXTEND _aac6_
+| [ "aac_instances" orient(o) constr(c)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~show:true c gl ]
+END
+
+
+
+
+TACTIC EXTEND _aacu2_
+| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:j c gl ]
+END
+
+TACTIC EXTEND _aacu3_
+| [ "aacu_rewrite" orient(o) constr(c) "subst" integer(j)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:0 ~occ_sol:j c gl ]
+END
+
+TACTIC EXTEND _aacu4_
+| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:0 c gl ]
+END
+
+TACTIC EXTEND _aacu5_
+| [ "aacu_rewrite" orient(o) constr(c) ] ->
+ [ fun gl -> aac_rewrite ~l2r:o c gl ]
+END
+
+TACTIC EXTEND _aacu6_
+| [ "aacu_instances" orient(o) constr(c)] ->
+ [ fun gl -> aac_rewrite ~l2r:o ~show:true c gl ]
+END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 13:23:51 +0000