diff options
Diffstat (limited to 'aac_rewrite.ml')
-rw-r--r-- | aac_rewrite.ml | 308 |
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 |