diff options
Diffstat (limited to 'theory.mli')
| -rw-r--r-- | theory.mli | 219 |
1 files changed, 219 insertions, 0 deletions
diff --git a/theory.mli b/theory.mli new file mode 100644 index 0000000..85ad24b --- /dev/null +++ b/theory.mli @@ -0,0 +1,219 @@ +(***************************************************************************) +(* 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}). +*) + + + + +(** 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 + +(** The constr associated with our typeclasses for AC or A operators *) +val op_ac:Term.constr lazy_t +val op_a: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 + +(** {2 Packaging modules} *) + +(** 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_typeof rlt int] *) + val mk_typeof: Coq.reltype ->int ->Term.constr + + (** [mk_typeof rlt int] *) + val mk_relof: Coq.reltype ->int ->Term.constr + + (** [mk_pack rlt (ar,value,morph)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [null] builds a dummy symbol, given an {!Coq.eqtype} and a + constant *) + val null: Coq.eqtype -> Term.constr -> Term.constr + +end + +(** Dynamically typed AC operations *) +module Sum: +sig + + (** mimics the Coq record [Sum.pack] *) + type pack = {plus : Term.constr; zero: Term.constr ; opac: Term.constr} + + val typ: Term.constr lazy_t + + (** [mk_pack rlt (plus,zero,opac)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [zero rlt pack]*) + val zero: Coq.reltype -> Term.constr -> Term.constr + + (** [plus rlt pack]*) + val plus: Coq.reltype -> Term.constr -> Term.constr + +end + + +(** Dynamically typed A operations *) +module Prd: +sig + + (** mimics the Coq record [Prd.pack] *) + type pack = {dot: Term.constr; one: Term.constr ; opa: Term.constr} + + val typ: Term.constr lazy_t + + (** [mk_pack rlt (dot,one,opa)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [one rlt pack]*) + val one: Coq.reltype -> Term.constr -> Term.constr + + (** [dot rlt pack]*) + val dot: Coq.reltype -> Term.constr -> Term.constr + +end + + +(** [mk_equal rlt l r] builds the term [l == r] *) +val mk_equal : Coq.reltype -> Term.constr -> Term.constr -> Term.constr + + +(** {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; the + behaviour in this case is almost unspecified: we simply give + priority to AC 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 + + (** {1 Reification: from Coq terms to AST {!Matcher.Terms.t} } *) + + (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree + of the term [cstr]. 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 creates fresh evars; this is + why we give back the [goal], accordingly updated. *) + val t_of_constr : Coq.goal_sigma -> Coq.reltype -> envs -> Term.constr -> Matcher.Terms.t * Coq.goal_sigma + + (** {1 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. *) + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t] rebuilds a term in the raw representation *) + val raw_constr_of_t : envs -> Coq.reltype -> Matcher.Terms.t -> Term.constr + + (** {2 Building reified terms} *) + + (** The reification environments, as Coq constrs *) + type sigmas = { + env_sym : Term.constr; + env_sum : Term.constr; + env_prd : Term.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.eqtype -> envs -> Coq.goal_sigma -> sigmas * reifier * 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 |