1(*=====================================================================  *)
2(* FILE          : quantHeuristicsLibParameters.sml                      *)
3(* DESCRIPTION   : some code to find instantations for quantified        *)
4(*                 variables                                             *)
5(*                                                                       *)
6(* AUTHORS       : Thomas Tuerk                                          *)
7(* DATE          : December 2008                                         *)
8(* ===================================================================== *)
9
10
11structure quantHeuristicsLibParameters :> quantHeuristicsLibParameters =
12struct
13
14(*
15quietdec := true;
16loadPath :=
17            (concat [Globals.HOLDIR, "/src/quantHeuristics"])::
18            !loadPath;
19
20map load ["quantHeuristicsTheory"];
21load "ConseqConv"
22show_assums := true;
23quietdec := true;
24*)
25
26open HolKernel Parse boolLib Drule ConseqConv quantHeuristicsLibBase
27open rich_listTheory quantHeuristicsTheory
28
29(*
30quietdec := false;
31*)
32
33
34(* quantHeuristicsLib contains the core functionality to eliminate
35   quantifiers. However the heuristics contained in this lib are just
36   concerned with equations and basic boolean expressions. This
37   file contains heuristics for common construcs like lists, pairs,
38   option-types, etc.
39*)
40
41
42
43(*******************************************************************
44 * Pairs
45 *******************************************************************)
46
47
48(* val v = ``x:('a # 'b)``;
49   val fv = [``y:'a``]:term list;
50   val t = ``FST (x:('a # 'b)) = y``
51   fun P v (t:term) = SOME (enumerate_pair true v)
52   val given = ["aaaa"]
53 *)
54
55fun enumerate_pair do_rec v =
56if not ((can pairSyntax.dest_prod) (type_of v)) then v else
57let
58   val (vn,vt) = dest_var v
59   val tL = pairSyntax.spine_prod vt;
60
61   val ntL = enumerate 1 tL
62   val vars = map (fn (n, ty) => (mk_var (vn^"_"^(Int.toString n), ty))) ntL
63   val vars' = if do_rec then (map (enumerate_pair do_rec) vars) else vars
64   val p = (pairSyntax.list_mk_pair vars')
65in
66   p
67end;
68
69val GUESS_PAIR_THM = prove (
70``!P (i:'b -> 'a). (!v. ?x. v = i x) ==>
71  (GUESS_EXISTS_GAP i P /\ GUESS_FORALL_GAP i P)``,
72simpLib.SIMP_TAC numLib.std_ss [GUESS_REWRITES])
73
74
75fun QUANT_INSTANTIATE_HEURISTIC___SPLIT_PAIR_GEN PL (sys:quant_heuristic_base) v t =
76let
77   (*check whether something should be done*)
78   val _ = pairSyntax.dest_prod (type_of v) handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;
79
80   fun P v t = first_opt (fn x => fn p => (p v t)) PL
81   val vars = case (P v t) of NONE => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp
82                            | some => valOf some;
83   val fvL = rev (free_vars vars)
84
85   val ip = pairLib.mk_pabs (pairLib.list_mk_pair fvL, vars);
86   val ip' = rhs (concl ((pairTools.PABS_ELIM_CONV ip) handle UNCHANGED => REFL ip));
87
88   val gthm = ISPECL[mk_abs (v, t), ip'] GUESS_PAIR_THM
89   val pre = rand (rator (concl gthm))
90   val pre_thm = prove (pre,
91     simpLib.SIMP_TAC numLib.std_ss [
92       pairTheory.EXISTS_PROD, pairTheory.FORALL_PROD])
93   val gthmL = BODY_CONJUNCTS (MP gthm pre_thm)
94in
95  {rewrites     = [],
96   general      = [],
97   exists_point = [],
98   forall_point = [],
99   forall       = [],
100   exists       = [],
101   forall_gap   = [guess_thm (gty_forall_gap, vars, fvL, el 2 gthmL)],
102   exists_gap   = [guess_thm (gty_exists_gap, vars, fvL, el 1 gthmL)]}
103end;
104
105
106fun split_pair___FST_SND___pred depth_split v t =
107let
108   val t1 = pairSyntax.mk_fst v;
109   val t2 = pairSyntax.mk_snd v;
110
111   val do_split = not (null (find_terms (fn t' => (t' = t1) orelse (t' = t2)) t))
112in
113   if do_split then (SOME (enumerate_pair depth_split v)) else NONE
114end;
115
116
117(* val v = ``x:('a # 'b # 'c)``;
118   val t = ``(\ (a,b,c). P a b c) ^v``
119 *)
120local
121   fun is_var_pabs v t =
122   let
123      val (b,v') = dest_comb t;
124   in
125      (v = v') andalso (pairSyntax.is_pabs b)
126   end handle HOL_ERR _ => false;
127in
128
129fun split_pair___PABS___pred v t =
130let
131   val p = hd (find_terms (is_var_pabs v) t);
132   val vars = fst (pairSyntax.dest_pabs (fst (dest_comb p)))
133in
134   (SOME vars)
135end handle Empty => NONE
136         | HOL_ERR _ => NONE;
137end;
138
139
140fun split_pair___ALL___pred v = K (SOME (enumerate_pair true v));
141
142
143
144(* val v = ``x:('a # 'b # 'c)``
145   val fv = []:term list;
146   val t = ``(\ (a1, a2, a3). P a1 a2 a3) (x:('a # 'b # 'c))``
147 *)
148
149fun pair_qp pL = combine_qps
150    [rewrite_qp [PAIR_EQ_EXPAND, pairTheory.FST, pairTheory.SND],
151     heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___SPLIT_PAIR_GEN pL],
152     final_rewrite_qp [pairTheory.FST, pairTheory.SND, PAIR_EQ_SIMPLE_EXPAND]]
153
154val pair_default_qp = pair_qp [split_pair___PABS___pred,
155        split_pair___FST_SND___pred false]
156
157val pair_ty_filter = type_match_filter [``:('a # 'b)``]
158
159(*
160val PAIR_QUANT_INSTANTIATE_CONV = QUANT_INSTANTIATE_CONV [pair_default_qp]
161
162val t = ``?p. (x = FST p) /\ Q p``;
163val thm = PAIR_QUANT_INSTANTIATE_CONV t;
164
165val t = ``?p. (7 = (SND p)) /\ Q p``
166val thm = PAIR_QUANT_INSTANTIATE_CONV t;
167
168val t = ``?p1 p2. (p1 = 7) /\ Q (p1,p2)``
169val thm = PAIR_QUANT_INSTANTIATE_CONV t
170
171
172val t = ``?v. (v,X) = Z``
173val thm = PAIR_QUANT_INSTANTIATE_CONV t;
174
175val t = ``!x. a /\ (\ (a1, t3, a2). P a1 a2 t3) x /\ b x``
176val thm = PAIR_QUANT_INSTANTIATE_CONV t
177
178val t = ``?x. (x = 2) /\ P x``;
179val thm = PAIR_QUANT_INSTANTIATE_CONV t
180
181val t = ``!x. ((f t = x) /\ P x) ==> Q x``;
182val thm = PAIR_QUANT_INSTANTIATE_CONV t
183
184val t = ``?v. (v,X) = (a,9)``;
185val thm = PAIR_QUANT_INSTANTIATE_CONV t
186
187*)
188
189
190val stateful_qp = quantHeuristicsLibBase.stateful_qp;
191val pure_stateful_qp = quantHeuristicsLibBase.pure_stateful_qp;
192val TypeBase_qp = quantHeuristicsLibBase.TypeBase_qp;
193
194
195(*******************************************************************
196 * Option types
197 *******************************************************************)
198
199val option_qp = combine_qps [
200   distinct_qp [optionTheory.NOT_NONE_SOME],
201
202   cases_qp    [optionTheory.option_nchotomy],
203
204   rewrite_qp  [optionTheory.SOME_11, optionTheory.IS_NONE_EQ_NONE,
205                optionTheory.IS_NONE_EQ_NONE,
206                IS_SOME_EQ_NOT_NONE],
207
208   final_rewrite_qp [optionTheory.option_CLAUSES]
209  ]
210
211val option_ty_filter = type_match_filter [``:'a option``]
212
213
214(*******************************************************************
215 * Sum types
216 *******************************************************************)
217
218val sum_qp = combine_qps [
219  get_qp___for_types [``:('a + 'b)``],
220  cases_qp [sumTheory.ISL_OR_ISR],
221  rewrite_qp [ISL_exists, ISR_exists, sumTheory.NOT_ISR_ISL, sumTheory.NOT_ISL_ISR, INL_NEQ_ELIM, INR_NEQ_ELIM],
222
223  final_rewrite_qp [sumTheory.OUTR, sumTheory.OUTL, sumTheory.ISL, sumTheory.ISR, sumTheory.INR_INL_11]
224]
225
226val sum_ty_filter = type_match_filter [``:('a + 'b)``]
227
228
229(*******************************************************************
230 * Nums
231 *******************************************************************)
232
233val num_qp = combine_qps [
234   distinct_qp [prim_recTheory.SUC_ID],
235
236   cases_qp [arithmeticTheory.num_CASES],
237
238   rewrite_qp [prim_recTheory.INV_SUC_EQ,
239      arithmeticTheory.EQ_ADD_RCANCEL,arithmeticTheory.EQ_ADD_LCANCEL,
240      arithmeticTheory.ADD_CLAUSES],
241
242   final_rewrite_qp [numTheory.NOT_SUC, GSYM numTheory.NOT_SUC]
243]
244
245val num_ty_filter = type_filter [``:num``]
246
247
248(*******************************************************************
249 * Lists
250 *******************************************************************)
251
252
253val list_no_len_qp = combine_qps [
254   distinct_qp [rich_listTheory.NOT_CONS_NIL],
255
256   cases_qp [listTheory.list_CASES],
257
258   rewrite_qp  [listTheory.CONS_11,
259                listTheory.NULL_EQ,
260                listTheory.APPEND_11,
261                listTheory.APPEND_eq_NIL],
262
263   final_rewrite_qp [listTheory.NULL_DEF,
264                     listTheory.TL, listTheory.HD,
265                     rich_listTheory.NOT_CONS_NIL,
266                     GSYM rich_listTheory.NOT_CONS_NIL]
267]
268
269val list_qp = combine_qp (rewrite_qp  [LIST_LENGTH_COMPARE_SUC,
270                     LIST_LENGTH_1]) list_no_len_qp;
271
272val list_len_qp = combine_qp (rewrite_qp  [LIST_LENGTH_COMPARE_SUC,
273                     LIST_LENGTH_20]) list_no_len_qp;
274
275val list_ty_filter = type_match_filter [``:'a list``]
276
277
278(*******************************************************************
279 * Records
280 *******************************************************************)
281
282fun get_record_type_rewrites ty =
283let
284   fun type_rewrites ty =
285       let
286          val ty_info = valOf (TypeBase.fetch ty)
287          val (thyname,typename) = TypeBasePure.ty_name_of ty_info
288       in
289          if null (TypeBasePure.fields_of ty_info) then [] else
290          (map (fn s => (DB.fetch thyname (typename^"_"^(fst s))))
291             (TypeBasePure.fields_of ty_info)) @
292          (map (fn s => (DB.fetch thyname (typename^s))) [
293           "_fupdfupds_comp", "_accessors", "_fn_updates",
294            "_literal_11", "_component_equality",
295            "_accfupds"])@
296          ((valOf (TypeBasePure.one_one_of ty_info))::
297          ((TypeBasePure.case_def_of ty_info)::
298          ((TypeBasePure.accessors_of ty_info)@(TypeBasePure.updates_of ty_info))))
299       end;
300
301  val constructor = hd (TypeBase.constructors_of ty)
302  val (typ, types) = let
303    fun domtys acc ty = let
304      val (d1, rty) = dom_rng ty
305    in
306      domtys (d1::acc) rty
307    end handle HOL_ERR _ => (ty, List.rev acc)
308  in
309    domtys [] (type_of constructor)
310  end
311in
312  [combinTheory.K_THM, combinTheory.o_THM]@
313  (flatten (map type_rewrites (typ::types)))
314end;
315
316
317(*
318
319Hol_datatype `my_record = <| field1 : bool ;
320                             field2 : num  ;
321                             field3 : bool |>`
322
323val do_rewrites = false
324fun P v t = true
325
326val v = ``r1:my_record``
327val t = ``r1.field1``
328
329*)
330
331fun QUANT_INSTANTIATE_HEURISTIC___RECORDS do_rewrites P sys v t =
332let
333   (*check whether something should be done*)
334   val v_info = case TypeBase.fetch (type_of v) of NONE   => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp
335                                                 | SOME x => x
336   val _ = if null (TypeBasePure.fields_of v_info) orelse not (P v t) then
337              raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp else ()
338   val (thyname,typename) = TypeBasePure.ty_name_of v_info
339
340   val vars = let
341      val (v_name,_) = dest_var v
342      fun mk_new_var (s, ty) = mk_var (s, ty);
343      in
344         map mk_new_var (TypeBasePure.fields_of v_info)
345      end;
346
347   val thm0 =
348        let
349           val xthm0 = DB.fetch thyname (typename^"_literal_nchotomy")
350           val xthm1 =  CONV_RULE (RENAME_VARS_CONV (map (fst o dest_var) (v :: vars))) xthm0
351        in xthm1
352        end;
353   val gc = QUANT_INSTANTIATE_HEURISTIC___one_case thm0 sys v t
354in
355   if do_rewrites then
356        (guess_collection_append gc
357              (guess_list2collection (get_record_type_rewrites (type_of v), [])))
358   else gc
359end
360
361fun record_qp do_rewrites P = heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___RECORDS do_rewrites P];
362
363
364val record_default_qp = record_qp false (K (K true))
365
366(*******************************************************************
367 * Heuristic for implications that considers just the right hand side
368 * and conjunctions that just assume everything
369 *******************************************************************)
370
371(*
372  val v = ``x:num``
373  val t = ``Q x ==> (x = 2) /\ P x``
374  val sys = debug_sys
375*)
376fun QUANT_INSTANTIATE_HEURISTIC___DEST_HEU dest sys v t =
377let
378   val tL = dest t;
379
380   (* get guesses form right hand side *)
381   val gcL = map (fn t => SOME (sys v t) handle HOL_ERR _ => NONE
382                                              | QUANT_INSTANTIATE_HEURISTIC___no_guess_exp => NONE) tL
383   val gc = guess_collection_flatten gcL
384   val (rw_thms, gL) = guess_collection2list gc
385
386   (* just assume without justification that these are valid guesses for the full implication,
387      this might be wrong! *)
388   fun guess_lift g = let
389      val (i, fvL) = guess_extract g
390      val ty_opt = guess_extract_type g
391      val g' = mk_guess_opt ty_opt v t i fvL
392   in g' end
393   val gL' = map guess_lift gL
394in
395   guess_list2collection (rw_thms, gL')
396end handle HOL_ERR _ => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp
397
398fun dest_lift_qp dest = heuristics_qp [QUANT_INSTANTIATE_HEURISTIC___DEST_HEU dest]
399
400val implication_concl_qp = dest_lift_qp (fn t => [snd (dest_imp_only t)])
401val conj_lift_qp = dest_lift_qp (fn t => (let val (t1,t2) = dest_conj t in [t1, t2] end))
402
403
404(*******************************************************************
405 * Combinations
406 *******************************************************************)
407
408val std_qps = [num_qp, option_qp, pair_default_qp, list_qp, sum_qp, record_default_qp]
409
410val no_ctxt_std_qp     = combine_qps std_qps
411val direct_ctxt_std_qp = combine_qps (std_qps @ [direct_context_qp])
412val std_qp             = combine_qps (std_qps @ [context_qp])
413
414
415
416end
417