module Trans:sig..end
Tranlations between Coq and OCaml
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:
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);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; 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
val empty_envs : unit -> envsMatcher.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 : Environ.env ->
Evd.evar_map ->
Coq.Relation.t ->
envs ->
EConstr.constr * EConstr.constr ->
Matcher.Terms.t * Matcher.Terms.t * Evd.evar_map
val add_symbol : Environ.env ->
Evd.evar_map ->
Coq.Relation.t -> envs -> Constr.t -> Evd.evar_mapadd_symbol adds a given binary symbol to the environment of
known stuff.
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
Theory.Trans.t_of_constr; second, reified Coq terms, that are required for
the reflexive decision procedure.
type
val ir_of_envs : Environ.env ->
Evd.evar_map ->
Coq.Relation.t -> envs -> Evd.evar_map * ir
val ir_to_units : ir -> Matcher.ext_unitsval raw_constr_of_t : ir ->
Coq.Relation.t -> EConstr.rel_context -> Matcher.Terms.t -> EConstr.constrraw_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.
The reification environments, as Coq constrs
type
|
env_sym : |
|
env_bin : |
|
env_units : |
}
type
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.
val mk_reifier : Coq.Relation.t ->
EConstr.constr ->
ir ->
(sigmas * reifier) Proofview.tactic
val reif_constr_of_t : reifier -> Matcher.Terms.t -> EConstr.constrreif_constr_of_t reifier t rebuilds the term t in the
reified form.