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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Ltac2.Init.
Ltac2 @ external type : constr -> constr := "ltac2" "constr_type".
(** Return the type of a term *)
Ltac2 @ external equal : constr -> constr -> bool := "ltac2" "constr_equal".
(** Strict syntactic equality: only up to α-conversion and evar expansion *)
Module Unsafe.
(** Low-level access to kernel terms. Use with care! *)
Ltac2 Type case.
Ltac2 Type case_invert := [
| NoInvert
| CaseInvert (constr array)
].
Ltac2 Type kind := [
| Rel (int)
| Var (ident)
| Meta (meta)
| Evar (evar, constr array)
| Sort (sort)
| Cast (constr, cast, constr)
| Prod (binder, constr)
| Lambda (binder, constr)
| LetIn (binder, constr, constr)
| App (constr, constr array)
| Constant (constant, instance)
| Ind (inductive, instance)
| Constructor (constructor, instance)
| Case (case, constr, case_invert, constr, constr array)
| Fix (int array, int, binder array, constr array)
| CoFix (int, binder array, constr array)
| Proj (projection, constr)
| Uint63 (uint63)
| Float (float)
| Array (instance, constr array, constr, constr)
].
Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
Ltac2 @ external make : kind -> constr := "ltac2" "constr_make".
Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check".
(** Checks that a constr generated by unsafe means is indeed safe in the
current environment, and returns it, or the error otherwise. Panics if
not focused. *)
Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl".
(** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with
[r₁;...;rₙ] in [c]. *)
Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "constr_closenl".
(** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
[Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
Ltac2 @ external case : inductive -> case := "ltac2" "constr_case".
(** Generate the case information for a given inductive type. *)
Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "constr_constructor".
(** Generate the i-th constructor for a given inductive type. Indexing starts
at 0. Panics if there is no such constructor. *)
End Unsafe.
Module Binder.
Ltac2 @ external make : ident option -> constr -> binder := "ltac2" "constr_binder_make".
(** Create a binder given the name and the type of the bound variable. *)
Ltac2 @ external name : binder -> ident option := "ltac2" "constr_binder_name".
(** Retrieve the name of a binder. *)
Ltac2 @ external type : binder -> constr := "ltac2" "constr_binder_type".
(** Retrieve the type of a binder. *)
End Binder.
Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
(** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
the proof built by the tactic. *)
Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype".
(** Pretype the provided preterm. Assumes the goal to be focussed. *)
Ltac2 is_evar(c: constr) :=
match Unsafe.kind c with
| Unsafe.Evar _ _ => true
| _ => false
end.
Ltac2 @ external has_evar : constr -> bool := "ltac2" "constr_has_evar".
Ltac2 is_var(c: constr) :=
match Unsafe.kind c with
| Unsafe.Var _ => true
| _ => false
end.
Ltac2 is_fix(c: constr) :=
match Unsafe.kind c with
| Unsafe.Fix _ _ _ _ => true
| _ => false
end.
Ltac2 is_cofix(c: constr) :=
match Unsafe.kind c with
| Unsafe.CoFix _ _ _ => true
| _ => false
end.
Ltac2 is_ind(c: constr) :=
match Unsafe.kind c with
| Unsafe.Ind _ _ => true
| _ => false
end.
Ltac2 is_constructor(c: constr) :=
match Unsafe.kind c with
| Unsafe.Constructor _ _ => true
| _ => false
end.
Ltac2 is_proj(c: constr) :=
match Unsafe.kind c with
| Unsafe.Proj _ _ => true
| _ => false
end.
Ltac2 is_const(c: constr) :=
match Unsafe.kind c with
| Unsafe.Constant _ _ => true
| _ => false
end.
|
