diff options
author | Stephane Glondu <steph@glondu.net> | 2010-12-01 11:53:25 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-12-01 11:53:25 +0100 |
commit | 9e28c50232e56e35437afb468c6d273abcf5eab5 (patch) | |
tree | 5683a9003d284a2b346491ebf276f67c3ec733fa /aac_rewrite.ml | |
parent | 1aa8b6f6a876af22f538c869f022bc4ca5986b40 (diff) |
Imported Upstream version 0.2upstream/0.2
Diffstat (limited to 'aac_rewrite.ml')
-rw-r--r-- | aac_rewrite.ml | 308 |
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 |