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
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
(***************************************************************************)
(* 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. *)
(***************************************************************************)
(** Interface with Coq *)
type constr = Term.constr
open Term
open Names
open Coqlib
(* The contrib name is used to locate errors when loading constrs *)
let contrib_name = "aac_tactics"
(* Getting constrs (primitive Coq terms) from exisiting Coq
libraries. *)
let find_constant contrib dir s =
Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
let init_constant dir s = find_constant contrib_name dir s
(* A clause specifying that the [let] should not try to fold anything
in the goal *)
let nowhere =
{ Tacexpr.onhyps = Some [];
Tacexpr.concl_occs = Rawterm.no_occurrences_expr
}
let mk_letin (name: string) (constr: constr) : constr * Proof_type.tactic =
let name = (Names.id_of_string name) in
let letin =
(Tactics.letin_tac
None
(Name name)
constr
None (* or Some ty *)
nowhere
) in
mkVar name, letin
let mk_letin' (name: string) (constr: constr) : constr * Proof_type.tactic
=
constr, Tacticals.tclIDTAC
(** {2 General functions} *)
type goal_sigma = Proof_type.goal Tacmach.sigma
let goal_update (goal : goal_sigma) evar_map : goal_sigma=
let it = Tacmach.sig_it goal in
Tacmach.re_sig it evar_map
let resolve_one_typeclass goal ty : constr*goal_sigma=
let env = Tacmach.pf_env goal in
let evar_map = Tacmach.project goal in
let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in
c, (goal_update goal em)
let nf_evar goal c : Term.constr=
let evar_map = Tacmach.project goal in
Evarutil.nf_evar evar_map c
let evar_unit (gl : goal_sigma) (rlt : constr * constr) : constr * goal_sigma =
let env = Tacmach.pf_env gl in
let evar_map = Tacmach.project gl in
let (em,x) = Evarutil.new_evar evar_map env (fst rlt) in
x,(goal_update gl em)
let evar_binary (gl: goal_sigma) (rlt: constr * constr) =
let env = Tacmach.pf_env gl in
let evar_map = Tacmach.project gl in
let x = fst rlt in
let ty = mkArrow x (mkArrow x x) in
let (em,x) = Evarutil.new_evar evar_map env ty in
x,( goal_update gl em)
(* decomp_term : constr -> (constr, types) kind_of_term *)
let decomp_term c = kind_of_term (strip_outer_cast c)
(** {2 Bindings with Coq' Standard Library} *)
module Pair = struct
let path = ["Coq"; "Init"; "Datatypes"]
let typ = lazy (init_constant path "prod")
let pair = lazy (init_constant path "pair")
end
module Pos = struct
let path = ["Coq" ; "NArith"; "BinPos"]
let typ = lazy (init_constant path "positive")
let xI = lazy (init_constant path "xI")
let xO = lazy (init_constant path "xO")
let xH = lazy (init_constant path "xH")
(* A coq positive from an int *)
let of_int n =
let rec aux n =
begin match n with
| n when n < 1 -> assert false
| 1 -> Lazy.force xH
| n -> mkApp
(
(if n mod 2 = 0
then Lazy.force xO
else Lazy.force xI
), [| aux (n/2)|]
)
end
in
aux n
end
module Nat = struct
let path = ["Coq" ; "Init"; "Datatypes"]
let typ = lazy (init_constant path "nat")
let _S = lazy (init_constant path "S")
let _O = lazy (init_constant path "O")
(* A coq nat from an int *)
let of_int n =
let rec aux n =
begin match n with
| n when n < 0 -> assert false
| 0 -> Lazy.force _O
| n -> mkApp
(
(Lazy.force _S
), [| aux (n-1)|]
)
end
in
aux n
end
(** Lists from the standard library*)
module List = struct
let path = ["Coq"; "Lists"; "List"]
let typ = lazy (init_constant path "list")
let nil = lazy (init_constant path "nil")
let cons = lazy (init_constant path "cons")
let cons ty h t =
mkApp (Lazy.force cons, [| ty; h ; t |])
let nil ty =
(mkApp (Lazy.force nil, [| ty |]))
let rec of_list ty = function
| [] -> nil ty
| t::q -> cons ty t (of_list ty q)
let type_of_list ty =
mkApp (Lazy.force typ, [|ty|])
end
(** Morphisms *)
module Classes =
struct
let classes_path = ["Coq";"Classes"; ]
let morphism = lazy (init_constant (classes_path@["Morphisms"]) "Proper")
(** build the constr [Proper rel t] *)
let mk_morphism ty rel t =
mkApp (Lazy.force morphism, [| ty; rel; t|])
let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence")
(** build the constr [Equivalence ty rel] *)
let mk_equivalence ty rel =
mkApp (Lazy.force equivalence, [| ty; rel|])
end
(** a [mset] is a ('a * pos) list *)
let mk_mset ty (l : (constr * int) list) =
let pos = Lazy.force Pos.typ in
let pair_ty = mkApp (Lazy.force Pair.typ , [| ty; pos|]) in
let pair (x : constr) (ar : int) =
mkApp (Lazy.force Pair.pair, [| ty ; pos ; x ; Pos.of_int ar|]) in
let rec aux = function
| [] -> List.nil pair_ty
| (t,ar)::q -> List.cons pair_ty (pair t ar) (aux q)
in
aux l
(** x r *)
type reltype = Term.constr * Term.constr
(** x r e *)
type eqtype = reltype * Term.constr
(** {1 Tacticals} *)
let tclTIME msg tac = fun gl ->
let u = Sys.time () in
let r = tac gl in
let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in
r
let tclDEBUG msg tac = fun gl ->
let _ = Pp.msgnl (Pp.str msg) in
tac gl
let tclPRINT tac = fun gl ->
let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in
tac gl
|
