diff options
Diffstat (limited to 'theory.mli')
| -rw-r--r-- | theory.mli | 197 |
1 files changed, 197 insertions, 0 deletions
diff --git a/theory.mli b/theory.mli new file mode 100644 index 0000000..cc9a617 --- /dev/null +++ b/theory.mli @@ -0,0 +1,197 @@ +(***************************************************************************) +(* 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. *) +(***************************************************************************) + +(** Bindings for Coq constants that are specific to the plugin; + reification and translation functions. + + Note: this module is highly correlated with the definitions of {i + AAC.v}. + + This module interfaces with the above Coq module; it provides + facilities to interpret a term with arbitrary operators as an + abstract syntax tree, and to convert an AST into a Coq term + (either using the Coq "raw" terms, as written in the starting + goal, or using the reified Coq datatypes we define in {i + AAC.v}). +*) + +(** Both in OCaml and Coq, we represent finite multisets using + weighted lists ([('a*int) list]), see {!Matcher.mset}. + + [mk_mset ty l] constructs a Coq multiset from an OCaml multiset + [l] of Coq terms of type [ty] *) + +val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr + +(** {2 Packaging modules} *) + +(** Environments *) +module Sigma: +sig + (** [add ty n x map] adds the value [x] of type [ty] with key [n] in [map] *) + val add: Term.constr ->Term.constr ->Term.constr ->Term.constr ->Term.constr + + (** [empty ty] create an empty map of type [ty] *) + val empty: Term.constr ->Term.constr + + (** [of_list ty null l] translates an OCaml association list into a Coq one *) + val of_list: Term.constr -> Term.constr -> (int * Term.constr ) list -> Term.constr + + (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *) + val to_fun: Term.constr ->Term.constr ->Term.constr ->Term.constr +end + + +(** Dynamically typed morphisms *) +module Sym: +sig + (** mimics the Coq record [Sym.pack] *) + type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} + + val typ: Term.constr lazy_t + + + (** [mk_pack rlt (ar,value,morph)] *) + val mk_pack: Coq.Relation.t -> pack -> Term.constr + + (** [null] builds a dummy (identity) symbol, given an {!Coq.Relation.t} *) + val null: Coq.Relation.t -> Term.constr + +end + + +(** We need to export some Coq stubs out of this module. They are used + by the main tactic, see {!Rewrite} *) +module Stubs : sig + val lift : Term.constr Lazy.t + val lift_proj_equivalence : Term.constr Lazy.t + val lift_transitivity_left : Term.constr Lazy.t + val lift_transitivity_right : Term.constr Lazy.t + val lift_reflexivity : Term.constr Lazy.t + (** The evaluation fonction, used to convert a reified coq term to a + raw coq term *) + val eval: Term.constr lazy_t + + (** The main lemma of our theory, that is + [compare (norm u) (norm v) = Eq -> eval u == eval v] *) + val decide_thm:Term.constr lazy_t + + val lift_normalise_thm : Term.constr lazy_t +end + +(** {2 Building reified terms} + + We define a bundle of functions to build reified versions of the + terms (those that will be given to the reflexive decision + procedure). In particular, each field takes as first argument the + index of the symbol rather than the symbol itself. *) + +(** Tranlations between Coq and OCaml *) +module Trans : sig + + (** This module provides facilities to interpret a term with + arbitrary operators as an instance of an abstract syntax tree + {!Matcher.Terms.t}. + + For each Coq application [f x_1 ... x_n], this amounts to + deciding whether one of the partial applications [f x_1 + ... x_i], [i<=n] is a proper morphism, whether the partial + application with [i=n-2] yields an A or AC binary operator, and + whether the whole term is the unit for some A or AC operator. We + use typeclass resolution to test each of these possibilities. + + Note that there are ambiguous terms: + - a term like [f x y] might yield a unary morphism ([f x]) and a + binary one ([f]); we select the latter one (unless [f] is A or + AC, in which case we declare it accordingly); + - a term like [S O] can be considered as a morphism ([S]) + applied to a unit for [(+)], or as a unit for [( * )]; we + chose to give priority to units, so that the latter + interpretation is selected in this case; + - an element might be the unit for several operations + *) + + (** To achieve this reification, one need to record informations + about the collected operators (symbols, binary operators, + units). We use the following imperative internal data-structure to + this end. *) + + type envs + val empty_envs : unit -> envs + + + (** {2 Reification: from Coq terms to AST {!Matcher.Terms.t} } *) + + + (** [t_of_constr goal rlt envs (left,right)] builds the abstract + syntax tree of the terms [left] and [right]. We rely on the [goal] + to perform typeclasses resolutions to find morphisms compatible + with the relation [rlt]. Doing so, it modifies the reification + environment [envs]. Moreover, we need to create fresh + evars; this is why we give back the [goal], accordingly + updated. *) + + val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> (Term.constr * Term.constr) -> Matcher.Terms.t * Matcher.Terms.t * Coq.goal_sigma + + (** [add_symbol] adds a given binary symbol to the environment of + known stuff. *) + val add_symbol : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma + + (** {2 Reconstruction: from AST back to Coq terms } + + The next functions allow one to map OCaml abstract syntax trees + to Coq terms. We need two functions to rebuild different kind of + terms: first, raw terms, like the one encountered by + {!t_of_constr}; second, reified Coq terms, that are required for + the reflexive decision procedure. *) + + type ir + val ir_of_envs : Coq.goal_sigma -> Coq.Relation.t -> envs -> Coq.goal_sigma * ir + val ir_to_units : ir -> Matcher.ext_units + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t] rebuilds a term in the raw representation, and + reconstruct the named products on top of it. In particular, this + allow us to print the context put around the left (or right) + hand side of a pattern. *) + val raw_constr_of_t : ir -> Coq.Relation.t -> (Term.rel_context) ->Matcher.Terms.t -> Term.constr + + (** {2 Building reified terms} *) + + (** The reification environments, as Coq constrs *) + + type sigmas = { + env_sym : Term.constr; + env_bin : Term.constr; + env_units : Term.constr; (* the [idx -> X:constr] *) + } + + + + (** We need to reify two terms (left and right members of a goal) + that share the same reification envirnoment. Therefore, we need + to add letins to the proof context in order to ensure some + sharing in the proof terms we produce. + + Moreover, in order to have as much sharing as possible, we also + add letins for various partial applications that are used + throughout the terms. + + To achieve this, we decompose the reconstruction function into + two steps: first, we build the reification environment and then + reify each term successively.*) + type reifier + + val mk_reifier : Coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic + + (** [reif_constr_of_t reifier t] rebuilds the term [t] in the + reified form. *) + val reif_constr_of_t : reifier -> Matcher.Terms.t -> Term.constr + +end |