From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 20 Sep 2012 09:41:14 +0200 Subject: Imported Upstream version 0.3 --- AAC_theory.mli | 197 --------------------------------------------------------- 1 file changed, 197 deletions(-) delete mode 100644 AAC_theory.mli (limited to 'AAC_theory.mli') diff --git a/AAC_theory.mli b/AAC_theory.mli deleted file mode 100644 index 2f57446..0000000 --- a/AAC_theory.mli +++ /dev/null @@ -1,197 +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. *) -(***************************************************************************) - -(** 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 {!AAC_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: AAC_coq.Relation.t -> pack -> Term.constr - - (** [null] builds a dummy (identity) symbol, given an {!AAC_coq.Relation.t} *) - val null: AAC_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 {!AAC_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 - {!AAC_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 {!AAC_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 : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> (Term.constr * Term.constr) -> AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma - - (** [add_symbol] adds a given binary symbol to the environment of - known stuff. *) - val add_symbol : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_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 : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> AAC_coq.goal_sigma * ir - val ir_to_units : ir -> AAC_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 -> AAC_coq.Relation.t -> (Term.rel_context) ->AAC_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 : AAC_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 -> AAC_matcher.Terms.t -> Term.constr - -end -- cgit v1.2.3