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
|
(***************************************************************************)
(* 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 where we import several definitions from Coq's
standard library.
This general purpose library could be reused by other plugins.
Some salient points:
- we use Caml's module system to mimic Coq's one, and avoid cluttering
the namespace;
- we also provide several handlers for standard coq tactics, in
order to provide a unified setting (we replace functions that
modify the evar_map by functions that operate on the whole
goal, and repack the modified evar_map with it).
*)
(** {2 Getting Coq terms from the environment} *)
val init_constant : string list -> string -> Term.constr
(** {2 General purpose functions} *)
type goal_sigma = Proof_type.goal Tacmach.sigma
val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma
val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma
val nf_evar : goal_sigma -> Term.constr -> Term.constr
val evar_unit :goal_sigma ->Term.constr*Term.constr-> Term.constr* goal_sigma
val evar_binary: goal_sigma -> Term.constr*Term.constr -> Term.constr* goal_sigma
(** [mk_letin name v] binds the constr [v] using a letin tactic *)
val mk_letin : string ->Term.constr ->Term.constr * Proof_type.tactic
(** [mk_letin' name v] is a drop-in replacement for [mk_letin' name v]
that does not make a binding (useful to test whether using lets is
efficient) *)
val mk_letin' : string ->Term.constr ->Term.constr * Proof_type.tactic
(* decomp_term : constr -> (constr, types) kind_of_term *)
val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term
(** {2 Bindings with Coq' Standard Library} *)
(** Coq lists *)
module List:
sig
(** [of_list ty l] *)
val of_list:Term.constr ->Term.constr list ->Term.constr
(** [type_of_list ty] *)
val type_of_list:Term.constr ->Term.constr
end
(** Coq pairs *)
module Pair:
sig
val typ:Term.constr lazy_t
val pair:Term.constr lazy_t
end
(** Coq positive numbers (pos) *)
module Pos:
sig
val typ:Term.constr lazy_t
val of_int: int ->Term.constr
end
(** Coq unary numbers (peano) *)
module Nat:
sig
val typ:Term.constr lazy_t
val of_int: int ->Term.constr
end
(** Coq typeclasses *)
module Classes:
sig
val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr
val mk_equivalence: Term.constr -> Term.constr -> Term.constr
end
(** 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
(** pairs [(x,r)] such that [r: Relation x] *)
type reltype = Term.constr * Term.constr
(** triples [((x,r),e)] such that [e : @Equivalence x r]*)
type eqtype = reltype * Term.constr
(** {2 Some tacticials} *)
(** time the execution of a tactic *)
val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
(** emit debug messages to see which tactics are failing *)
val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
(** print the current goal *)
val tclPRINT : Proof_type.tactic -> Proof_type.tactic
|
