aboutsummaryrefslogtreecommitdiff
path: root/mltt/core/context_tactical.ML
blob: d0fed615a557fe68b4abb3827ddbb923bec72218 (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
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
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
(*  Title:      context_tactical.ML
    Author:     Joshua Chen

More context tactics, and context tactic combinators.

Contains code modified from
  ~~/Pure/search.ML
  ~~/Pure/tactical.ML
*)

infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
infix 0 CORELSE CAPPEND CORELSE' CAPPEND'

structure Context_Tactical:
sig

type context_tactic' = int -> context_tactic
val CONTEXT_TACTIC': (Proof.context -> int -> tactic) -> context_tactic'
val all_ctac: context_tactic
val no_ctac: context_tactic
val print_ctac: (Proof.context -> string) -> context_tactic
val CTHEN: context_tactic * context_tactic -> context_tactic
val CORELSE: context_tactic * context_tactic -> context_tactic
val CAPPEND: context_tactic * context_tactic -> context_tactic
val CTHEN': context_tactic' * context_tactic' -> context_tactic'
val CORELSE': context_tactic' * context_tactic' -> context_tactic'
val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
val CTRY: context_tactic -> context_tactic
val CREPEAT: context_tactic -> context_tactic
val CREPEAT1: context_tactic -> context_tactic
val CREPEAT_N: int -> context_tactic -> context_tactic
val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
val CCHANGED: context_tactic -> context_tactic
val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_IN_RANGE: int -> int -> context_tactic' -> context_tactic
val CREPEAT_ALL_NEW: context_tactic' -> context_tactic'
val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic'
val CHEADGOAL: context_tactic' -> context_tactic
val CALLGOALS: context_tactic' -> context_tactic
val CSOMEGOAL: context_tactic' -> context_tactic
val CRANGE: context_tactic' list -> context_tactic'
val CFIRST: context_tactic list -> context_tactic
val CFIRST': context_tactic' list -> context_tactic'
val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) ->
  (context_state -> int) -> context_tactic -> context_tactic
val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) ->
  context_tactic -> context_tactic
val CTHEN_ASTAR: context_tactic -> (context_state -> bool) ->
  (int -> context_state -> int) -> context_tactic -> context_tactic
val CASTAR: (context_state -> bool) -> (int -> context_state -> int) ->
  context_tactic -> context_tactic

end = struct

type context_tactic' = int -> context_tactic

fun CONTEXT_TACTIC' tac i (ctxt, st) = TACTIC_CONTEXT ctxt ((tac ctxt i) st)

val all_ctac = Seq.make_results o Seq.single
val no_ctac = K Seq.empty
fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st)

fun (ctac1 CTHEN ctac2) cst =  Seq.maps_results ctac2 (ctac1 cst)

fun (ctac1 CORELSE ctac2) cst =
  (case Seq.pull (ctac1 cst) of
    NONE => ctac2 cst
  | some => Seq.make (fn () => some))

fun (ctac1 CAPPEND ctac2) cst =
  Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst)))

fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x
fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x
fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x

fun CTRY ctac = ctac CORELSE all_ctac

fun CREPEAT ctac =
  let
    fun rep qs cst =
      (case Seq.pull (Seq.filter_results (ctac cst)) of
        NONE => SOME (cst, Seq.make (fn () => repq qs))
      | SOME (cst', q) => rep (q :: qs) cst')
    and repq [] = NONE
      | repq (q :: qs) =
          (case Seq.pull q of
            NONE => repq qs
          | SOME (cst, q) => rep (q :: qs) cst);
  in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end

fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac

fun CREPEAT_N 0 _ = no_ctac
  | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac

fun CFILTER pred ctac cst =
  ctac cst
  |> Seq.filter_results
  |> Seq.filter pred
  |> Seq.make_results

(*Only accept next states where the subgoals have changed*)
fun CCHANGED ctac (cst as (_, st)) =
  CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst

local
  fun op THEN (f, g) x = Seq.maps_results g (f x)

  fun INTERVAL f i j x =
    if i > j then Seq.make_results (Seq.single x)
    else op THEN (f j, INTERVAL f i (j - 1)) x

  (*By Peter Lammich: apply tactic to subgoals in interval in a forward manner,
    skipping over emerging subgoals*)
  fun INTERVAL_FWD ctac l u (cst as (_, st)) = cst |>
    (if l > u then all_ctac
    else (ctac l CTHEN (fn cst' as (_, st') =>
      let val ofs = Thm.nprems_of st' - Thm.nprems_of st in
        if ofs < ~1
        then raise THM (
          "INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st'])
        else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst'
      end)))
in

fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) =
  cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
    INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))

(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward
  manner*)
fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) =
  cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
    INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))

(*Repeatedly apply ctac to the i-th until the k-th-from-last subgoals
  (i.e. leave the last k subgoals alone), until no more changes appear in the
  goal state.*)
fun CREPEAT_IN_RANGE i k ctac =
  let fun interval_ctac (cst as (_, st)) =
    INTERVAL_FWD ctac i (Thm.nprems_of st - k) cst
  in CREPEAT (CCHANGED interval_ctac) end

end

fun CREPEAT_ALL_NEW ctac =
  ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i))

fun CREPEAT_ALL_NEW_FWD ctac =
  ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i))

fun CHEADGOAL ctac = ctac 1

fun CALLGOALS ctac (cst as (_, st)) =
  let
    fun doall 0 = all_ctac
      | doall n = ctac n CTHEN doall (n - 1);
  in doall (Thm.nprems_of st) cst end

fun CSOMEGOAL ctac (cst as (_, st)) =
  let
    fun find 0 = no_ctac
      | find n = ctac n CORELSE find (n - 1);
  in find (Thm.nprems_of st) cst end

fun CRANGE [] _ = all_ctac
  | CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i

fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac

(*FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i*)
fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac)


(** Search tacticals **)

(* Best-first search *)

structure Thm_Heap = Heap (
  type elem = int * thm;
  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of)
)

structure Context_State_Heap = Heap (
  type elem = int * context_state;
  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2))
)

fun some_of_list [] = NONE
  | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l))

(*Check for and delete duplicate proof states*)
fun delete_all_min (cst as (_, st)) heap =
  if Context_State_Heap.is_empty heap then heap
  else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap)))
  then delete_all_min cst (Context_State_Heap.delete_min heap)
  else heap

(*Best-first search for a state that satisfies satp (incl initial state)
  Function sizef estimates size of problem remaining (smaller means better).
  tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
fun CTHEN_BEST_FIRST ctac0 satp sizef ctac =
  let
    fun pairsize cst = (sizef cst, cst);
    fun bfs (news, nst_heap) =
      (case List.partition satp news of
        ([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap)
      | (sats, _)  => some_of_list sats)
    and next nst_heap =
      if Context_State_Heap.is_empty nst_heap then NONE
      else
        let
          val (n, cst) = Context_State_Heap.min nst_heap;
        in
          bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap))
        end;
    fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty)
  in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end

(*Ordinary best-first search, with no initial tactic*)
val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac


(* A*-like search *)

(*Insertion into priority queue of states, marked with level*)
fun insert_with_level (lnth: int * int * context_state) [] = [lnth]
  | insert_with_level (l, m, cst) ((l', n, cst') :: csts) =
      if  n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts
      else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts
      else (l, m, cst) :: (l', n, cst') :: csts;

fun CTHEN_ASTAR ctac0 satp costf ctac =
  let
    fun bfs (news, nst, level) =
      let fun cost cst = (level, costf level cst, cst) in
        (case List.partition satp news of
          ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst)
        | (sats, _) => some_of_list sats)
      end
    and next [] = NONE
      | next ((level, n, cst) :: nst) =
          bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1)
  in fn cst => Seq.make_results
    (Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0)))
  end

(*Ordinary ASTAR, with no initial tactic*)
val CASTAR = CTHEN_ASTAR all_ctac;


end

open Context_Tactical