forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cfTacticsBaseLib.sig
146 lines (106 loc) · 4.97 KB
/
cfTacticsBaseLib.sig
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
signature cfTacticsBaseLib =
sig
include Abbrev
val progress_then : thm_tactic -> thm -> tactic
val try_progress_then : thm_tactic -> thm -> tactic
val progress : thm -> tactic
val progress_with_then : thm_tactic -> thm -> thm -> tactic
val progress_with : thm -> thm -> tactic
val instantiate : tactic
val instantiate1 : tactic
val try_finally : tactic -> tactic
val sing : 'a -> 'a list
val EVAL_PAT : term -> conv
val eval_pat_tac : term -> tactic
val qeval_pat_tac : term quotation -> tactic
val compute_pat : computeLib.compset -> term -> conv
val compute_pat_tac : computeLib.compset -> term -> tactic
val qcompute_pat_tac : computeLib.compset -> term quotation -> tactic
val hnf_conv : conv
val hnf : tactic
val cbv : tactic
val rewr_head_conv : thm -> conv
val parse : term -> term -> string quotation -> term
val parse_exp : string quotation -> term
val parse_decl : string quotation -> term
val parse_topdecs : string quotation -> term
val fetch_v : string -> ml_progLib.ml_prog_state -> term
val fetch_def : string -> ml_progLib.ml_prog_state -> thm
(*----------------------------------------------------------------*)
type conseq_conv = ConseqConv.conseq_conv
type directed_conseq_conv = ConseqConv.directed_conseq_conv
val find_map : ('a -> 'b option) -> 'a list -> 'b option
val NCONV : int -> conv -> conv
val UNCHANGED_CONV : conv -> conv
val CUSTOM_THEN_CONSEQ_CONV :
(exn -> bool) -> (exn -> bool) ->
conseq_conv -> conseq_conv -> conseq_conv
val handle_none : exn -> bool
val handle_UNCHANGED : exn -> bool
(* This has different semantics than [ConseqConv.THEN_CONSEQ_CONV], but I
believe these are the right ones.
Just like [Conv.THENC], it fails if either the first or the second
conversion fails, while [ConseqConv.THEN_CONSEQ_CONV] handles a failure
just like raising [UNCHANGED], which makes it impossible to make the first
conversion abort a THEN_CONSEQ_CONV.
*)
val THEN_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv
(* Similarly, this one has different semantics than
[ConseqConv.ORELSE_CONSEQ_CONV], and instead matches the semantics of
[Conv.ORELSEC]
*)
val ORELSE_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv
val EVERY_CONSEQ_CONV : conseq_conv list -> conseq_conv
val FIRST_CONSEQ_CONV : conseq_conv list -> conseq_conv
val CUSTOM_THEN_DCC :
(conseq_conv -> conseq_conv -> conseq_conv) ->
directed_conseq_conv -> directed_conseq_conv -> directed_conseq_conv
(* Has the same semantics as THEN_CONSEQ_CONV *)
val THEN_DCC :
directed_conseq_conv * directed_conseq_conv -> directed_conseq_conv
(* Has the same semantics as ORELSE_CONSEQ_CONV *)
val ORELSE_DCC :
directed_conseq_conv * directed_conseq_conv -> directed_conseq_conv
val EVERY_DCC : directed_conseq_conv list -> directed_conseq_conv
val CHANGED_DCC : directed_conseq_conv -> directed_conseq_conv
val QCHANGED_DCC : directed_conseq_conv -> directed_conseq_conv
val CONV_DCC : conv -> directed_conseq_conv
val STRENGTHEN_CONSEQ_CONV : conseq_conv -> directed_conseq_conv
val WEAKEN_CONSEQ_CONV : conseq_conv -> directed_conseq_conv
val TOP_REDEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
val CONJ_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv
val CONJ1_CONSEQ_CONV : conseq_conv -> conseq_conv
val CONJ2_CONSEQ_CONV : conseq_conv -> conseq_conv
val CONJ_LIST_CONSEQ_CONV : conseq_conv list -> conseq_conv
val DISJ_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv
val DISJ1_CONSEQ_CONV : conseq_conv -> conseq_conv
val DISJ2_CONSEQ_CONV : conseq_conv -> conseq_conv
val DISJ_LIST_CONSEQ_CONV : conseq_conv list -> conseq_conv
val IMP_CONSEQ_CONV : conseq_conv -> conseq_conv -> conseq_conv
val IMP_ASSUM_CONSEQ_CONV : conseq_conv -> conseq_conv
val IMP_CONCL_CONSEQ_CONV : conseq_conv -> conseq_conv
val IMP_LIST_CONSEQ_CONV : conseq_conv list -> conseq_conv
val STRIP_FORALL_CONSEQ_CONV : conseq_conv -> conseq_conv
val STRIP_EXISTS_CONSEQ_CONV : conseq_conv -> conseq_conv
val print_cc : conseq_conv
val print_dcc : directed_conseq_conv
(* -- *)
val MATCH_IMP_STRENGTHEN_CONSEQ_CONV : thm -> conseq_conv
(** Tactics to deal with goals of the form [?x1..xn. A1 /\ ... /\ Am], where
the [Ai]s are not themselves of the form [_ /\ _], and shouldn't start
with existential quantifications. The focus is on A1 (the "head"), where
most of the work is usually done.
*)
type econj = {evars: term list, head_conj: term, rest: term list}
val dest_econj : term -> econj
val mk_econj : econj -> term
val is_econj : term -> bool
val normalize_to_econj_conv : conv
val econj_head_conseq_conv : conseq_conv -> conseq_conv
val econj_nth_irule_conseq_conv : int -> thm -> conseq_conv
val econj_head_irule_conseq_conv : thm -> conseq_conv
(* Tactics *)
val normalize_to_econj : tactic
val econj_nth_irule : int -> thm -> tactic
val econj_head_irule : thm -> tactic
end