diff options
Diffstat (limited to 'AAC_theory.mli')
| -rw-r--r-- | AAC_theory.mli | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/AAC_theory.mli b/AAC_theory.mli index 128e88b..2f57446 100644 --- a/AAC_theory.mli +++ b/AAC_theory.mli @@ -7,8 +7,8 @@ (***************************************************************************) (** Bindings for Coq constants that are specific to the plugin; - reification and translation functions. - + reification and translation functions. + Note: this module is highly correlated with the definitions of {i AAC.v}. @@ -35,7 +35,7 @@ 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 @@ -58,10 +58,10 @@ sig (** [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 @@ -76,27 +76,27 @@ module Stubs : sig (** 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 + + (** 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 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}. + {!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 @@ -105,25 +105,25 @@ module Trans : sig 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: + 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 + - 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 + + type envs val empty_envs : unit -> envs - + (** {2 Reification: from Coq terms to AST {!AAC_matcher.Terms.t} } *) @@ -135,15 +135,15 @@ module Trans : sig 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 + 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 @@ -155,7 +155,7 @@ module Trans : sig 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) @@ -163,7 +163,7 @@ module Trans : sig 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 = { @@ -171,18 +171,18 @@ module Trans : sig 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. + 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.*) |