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 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
|
