1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 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 20092010: 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=n2] 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 datastructure 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 > (Context.Rel.t) >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
