diff options
Diffstat (limited to 'aac_rewrite.mli')
| -rw-r--r-- | aac_rewrite.mli | 59 |
1 files changed, 0 insertions, 59 deletions
diff --git a/aac_rewrite.mli b/aac_rewrite.mli deleted file mode 100644 index 81818b6..0000000 --- a/aac_rewrite.mli +++ /dev/null @@ -1,59 +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. *) -(***************************************************************************) - -(** 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 - |