diff options
Diffstat (limited to 'aac_rewrite.mli')
-rw-r--r-- | aac_rewrite.mli | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/aac_rewrite.mli b/aac_rewrite.mli new file mode 100644 index 0000000..81818b6 --- /dev/null +++ b/aac_rewrite.mli @@ -0,0 +1,59 @@ +(***************************************************************************) +(* 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. *) +(***************************************************************************) + +(** Main module for the Coq plug-in ; provides the [aac_rewrite] and + [aac_reflexivity] tactics. + + This file defines the entry point for the tactic aac_rewrite. It + does Joe-the-plumbing, given a goal, reifies the interesting + subterms (rewrited hypothesis, goal) into abstract syntax tree + {!Matcher.Terms} (see {!Theory.Trans.t_of_constr}). Then, we use the + results from the matcher to rebuild terms and make a transitivity + step toward a term in which the hypothesis can be rewritten using + the standard rewrite. + + Doing so, we generate a sub-goal which we solve using a reflexive + decision procedure for the equality of terms modulo + AAC. Therefore, we also need to reflect the goal into a concrete + data-structure. See {i AAC.v} for more informations, + especially the data-type {b T} and the {b decide} theorem. + +*) + +(** {2 Transitional functions} + + We define some plumbing functions that will be removed when we + integrate the new rewrite features of Coq 8.3 +*) + +(** [find_applied_equivalence goal eq] checks that the goal is + an applied equivalence relation, with two operands of the same + type. + +*) +val find_applied_equivalence : Proof_type.goal Tacmach.sigma -> Term.constr -> Coq.eqtype * Term.constr * Term.constr * Proof_type.goal Tacmach.sigma + +(** Build a couple of [t] from an hypothesis (variable names are not + relevant) *) +val t_of_hyp : Proof_type.goal Tacmach.sigma -> Coq.reltype -> Theory.Trans.envs -> Term.types -> (Matcher.Terms.t * Matcher.Terms.t) * int + +(** {2 Tactics} *) + +(** the [aac_reflexivity] tactic solves equalities modulo AAC, by + reflection: it reifies the goal to apply theorem [decide], from + file {i AAC.v}, and then concludes using [vm_compute] + and [reflexivity] +*) +val aac_reflexivity : Proof_type.tactic + +(** [aac_rewrite] is the tactic for in-depth reqwriting modulo AAC +with some options to choose the orientation of the rewriting and a +solution (first the subterm, then the solution)*) + +val aac_rewrite : Term.constr -> ?l2r:bool -> ?show:bool -> ?strict: bool -> ?occ_subterm:int -> ?occ_sol:int -> Proof_type.tactic + |