blob: 3d1e8f462d270904056f78643e82cc51ba2886d6 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Ltac2.Init.
(** ML-facing types *)
Ltac2 Type hypothesis := [ AnonHyp (int) | NamedHyp (ident) ].
Ltac2 Type bindings := [
| NoBindings
| ImplicitBindings (constr list)
| ExplicitBindings ((hypothesis * constr) list)
].
Ltac2 Type constr_with_bindings := constr * bindings.
Ltac2 Type occurrences := [
| AllOccurrences
| AllOccurrencesBut (int list)
| NoOccurrences
| OnlyOccurrences (int list)
].
Ltac2 Type hyp_location_flag := [ InHyp | InHypTypeOnly | InHypValueOnly ].
Ltac2 Type clause := {
on_hyps : (ident * occurrences * hyp_location_flag) list option;
on_concl : occurrences;
}.
Ltac2 Type evaluable_reference := [
| EvalVarRef (ident)
| EvalConstRef (constant)
].
Ltac2 Type red_flags := {
rBeta : bool;
rMatch : bool;
rFix : bool;
rCofix : bool;
rZeta : bool;
rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
rConst : evaluable_reference list
}.
Ltac2 Type 'a not_implemented.
Ltac2 Type rec intro_pattern := [
| IntroForthcoming (bool)
| IntroNaming (intro_pattern_naming)
| IntroAction (intro_pattern_action)
]
with intro_pattern_naming := [
| IntroIdentifier (ident)
| IntroFresh (ident)
| IntroAnonymous
]
with intro_pattern_action := [
| IntroWildcard
| IntroOrAndPattern (or_and_intro_pattern)
| IntroInjection (intro_pattern list)
| IntroApplyOn ((constr * intro_pattern) not_implemented) (* Not Implemented yet *)
| IntroRewrite (bool)
]
with or_and_intro_pattern := [
| IntroOrPattern (intro_pattern list list)
| IntroAndPattern (intro_pattern list)
].
Ltac2 Type evar_flag := bool.
Ltac2 Type advanced_flag := bool.
(** Standard, built-in tactics. See Ltac1 for documentation. *)
Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "ltac2" "tac_intros".
Ltac2 @ external apply : advanced_flag -> evar_flag ->
(unit -> constr_with_bindings) list -> (ident * (intro_pattern option)) option -> unit := "ltac2" "tac_apply".
Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "tac_case".
Ltac2 @ external generalize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_generalize".
Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_assert".
Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough".
Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
Ltac2 @ external red : clause -> unit := "ltac2" "tac_red".
Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf".
Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv".
Ltac2 @ external cbn : red_flags -> clause -> unit := "ltac2" "tac_cbn".
Ltac2 @ external lazy : red_flags -> clause -> unit := "ltac2" "tac_lazy".
Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".
Ltac2 @ external transitivity : constr -> unit := "ltac2" "tac_transitivity".
Ltac2 @ external etransitivity : unit -> unit := "ltac2" "tac_etransitivity".
Ltac2 @ external cut : constr -> unit := "ltac2" "tac_cut".
Ltac2 @ external left : evar_flag -> bindings -> unit := "ltac2" "tac_left".
Ltac2 @ external right : evar_flag -> bindings -> unit := "ltac2" "tac_right".
Ltac2 @ external constructor : evar_flag -> unit := "ltac2" "tac_constructor".
Ltac2 @ external split : evar_flag -> bindings -> unit := "ltac2" "tac_split".
Ltac2 @ external constructor_n : evar_flag -> int -> bindings -> unit := "ltac2" "tac_constructorn".
Ltac2 @ external intros_until : hypothesis -> unit := "ltac2" "tac_introsuntil".
Ltac2 @ external symmetry : clause -> unit := "ltac2" "tac_symmetry".
Ltac2 @ external rename : (ident * ident) list -> unit := "ltac2" "tac_rename".
Ltac2 @ external revert : ident list -> unit := "ltac2" "tac_revert".
Ltac2 @ external admit : unit -> unit := "ltac2" "tac_admit".
Ltac2 @ external fix_ : ident option -> int -> unit := "ltac2" "tac_fix".
Ltac2 @ external cofix_ : ident option -> unit := "ltac2" "tac_cofix".
Ltac2 @ external clear : ident list -> unit := "ltac2" "tac_clear".
Ltac2 @ external keep : ident list -> unit := "ltac2" "tac_keep".
Ltac2 @ external clearbody : ident list -> unit := "ltac2" "tac_clearbody".
Ltac2 @ external exact_no_check : constr -> unit := "ltac2" "tac_exactnocheck".
Ltac2 @ external vm_cast_no_check : constr -> unit := "ltac2" "tac_vmcastnocheck".
Ltac2 @ external native_cast_no_check : constr -> unit := "ltac2" "tac_nativecastnocheck".
Ltac2 @ external absurd : constr -> unit := "ltac2" "tac_absurd".
Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst".
Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".
|
