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, 0 insertions, 308 deletions
diff --git a/aac_rewrite.ml b/aac_rewrite.ml
deleted file mode 100644
index c4c88e0..0000000
--- a/aac_rewrite.ml
+++ /dev/null
@@ -1,308 +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 *)
-
-(* 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-20 13:31:14 +0000