1(* non-interactive mode
2*)
3structure ho_basicTools :> ho_basicTools =
4struct
5open HolKernel Parse boolLib;
6
7(* interactive mode
8val () = loadPath := union ["..", "../finished"] (!loadPath);
9val () = app load
10  ["bossLib",
11   "realLib",
12   "rich_listTheory",
13   "arithmeticTheory",
14   "numTheory",
15   "pred_setTheory",
16   "pairTheory",
17   "combinTheory",
18   "listTheory",
19   "dividesTheory",
20   "primeTheory",
21   "gcdTheory",
22   "probLib",
23   "hoTools"];
24val () = show_assums := true;
25
26*)
27
28open hurdUtils;
29
30infixr 0 ##
31
32(* ------------------------------------------------------------------------- *)
33(* Debugging.                                                                *)
34(* ------------------------------------------------------------------------- *)
35
36val trace_level = ref 0;
37val _ = Feedback.register_trace ("ho_basicTools", trace_level, 10);
38fun trace l s = if l > !trace_level then () else say (s ^ "\n");
39fun trace_x l s f x =
40  if l > !trace_level then () else say (s ^ ":\n" ^ f x ^ "\n");
41fun trace_CONV l s tm = (trace_x l s term_to_string tm; QCONV ALL_CONV tm);
42
43(* ------------------------------------------------------------------------- *)
44(* Type/term substitutions                                                   *)
45(* ------------------------------------------------------------------------- *)
46
47val empty_raw_subst : raw_substitution = (([], empty_tmset), ([], []));
48
49fun raw_match' tm1 tm2 ((tmS, tmIds), (tyS, tyIds)) =
50  raw_match tyIds tmIds tm1 tm2 (tmS, tyS);
51
52fun type_raw_match ty1 ty2 (sub : raw_substitution) =
53  let
54    val tm1 = mk_const ("NIL", mk_type ("list", [ty1]))
55    val tm2 = mk_const ("NIL", mk_type ("list", [ty2]))
56  in
57    raw_match' tm1 tm2 sub
58  end;
59
60val finalize_subst : raw_substitution -> substitution = norm_subst;
61
62(* ------------------------------------------------------------------------- *)
63(* Higher-order matching.                                                    *)
64(* ------------------------------------------------------------------------- *)
65
66fun dest_ho_pat bvs tm =
67  if is_var tm andalso not (is_bv bvs tm) then
68    (tm, [])
69  else
70    let
71      val (a, b) = dest_comb tm
72      val bi = dest_bv bvs b
73    in
74      (I ## cons bi) (dest_ho_pat bvs a)
75    end;
76fun is_ho_pat bvs = can (dest_ho_pat bvs);
77fun mk_ho_pat bvs (var, []) = var
78  | mk_ho_pat bvs (var, b::bs) =
79  mk_comb (mk_ho_pat bvs (var, bs), mk_bv bvs b);
80
81local
82  fun beta [] tm = (tm, fn () => REFL tm)
83    | beta (v::vs) tm =
84    let
85      val tm_abs = mk_abs (v, tm)
86      val (match_tm, th1) = beta vs tm_abs
87    in
88      (match_tm,
89       fn () =>
90       TRANS (MK_COMB (th1 (), REFL v)) (QCONV BETA_CONV (mk_comb (tm_abs, v))))
91    end
92
93  fun eta_beta [] tm = (tm, fn () => REFL tm)
94    | eta_beta (v::vs) tm =
95    let
96      val body = eta_conv (mk_abs (v, tm))
97      val (match_tm, th) = eta_beta vs body
98    in
99      (match_tm, fn () => MK_COMB (th (), REFL v))
100    end
101    handle HOL_ERR _ => beta (v::vs) tm
102in
103  fun ho_pat_match bvs pat_bvs tm =
104    let
105      val tm_bvs = filter (is_bv bvs) (free_vars tm)
106      val _ = assert (forall (is_bv pat_bvs) tm_bvs)
107        (ERR "ho_pat_match" "var pattern doesn't have all bound vars used")
108    in
109      eta_beta pat_bvs tm
110    end
111
112  fun ho_raw_match (var, bs) (bvs, tm) sub =
113    let
114      val var_bvs = map (mk_bv bvs) bs
115    in
116      (C (raw_match' var) sub ## I) (ho_pat_match bvs var_bvs tm)
117    end
118end;
119
120local
121  fun check_off_bvs _ tm [] = tm
122    | check_off_bvs bvs tm (b :: bs) =
123    let
124      val (a, v) = dest_comb tm
125      val _ = assert (dest_bv bvs v = b) (ERR "fo_pat_match" "wrong bound vars")
126    in
127      check_off_bvs bvs a bs
128    end
129in
130  fun fo_raw_match (var, bs) (bvs, tm) sub =
131    let
132      val body = check_off_bvs bvs tm bs
133      val bvfvs = listset bvs Isct FVs body
134      val _ = assert (HOLset.isEmpty bvfvs)
135        (ERR "fo_pat_match" "term to be matched contains bound vars")
136    in
137      raw_match' var body sub
138    end;
139end;
140
141local
142  fun match (bvs, tm) (bvs', tm') sub =
143    if is_bv bvs tm then
144      let
145        val _ = assert (dest_bv bvs tm = dest_bv bvs' tm')
146          (ERR "ho_match" "bound var in pattern does not match")
147      in
148        (sub, fn () => REFL tm')
149      end
150    else if is_ho_pat bvs tm then
151      ho_raw_match (dest_ho_pat bvs tm) (bvs', tm') sub
152    else
153      (case Df dest_term (tm, tm') of
154         (COMB (Rator, Rand), COMB (Rator', Rand')) =>
155         let
156           val (sub', rator_th) = match (bvs, Rator) (bvs', Rator') sub
157           val (sub'', rand_th) = match (bvs, Rand) (bvs', Rand') sub'
158         in
159           (sub'', fn () => MK_COMB (rator_th (), rand_th ()))
160         end
161       | (LAMB (Bvar, Body), LAMB (Bvar', Body')) =>
162         let
163           val sub' = type_raw_match (type_of Bvar) (type_of Bvar') sub
164           val (sub'', thk) = match (Bvar::bvs, Body) (Bvar'::bvs', Body') sub'
165         in
166           (sub'', fn () => MK_ABS (GEN Bvar' (thk ())))
167         end
168       | (CONST _, CONST _)
169         => (raw_match' tm tm' sub, fn () => REFL tm')
170       | (VAR _, _)
171         => raise BUG "ho_match" "var in pattern shouldn't be possible"
172       | _ => raise ERR "ho_match" "fundamentally different terms")
173in
174  fun ho_match_bvs (bvs, tm) (bvs', tm') : ho_substitution =
175    (finalize_subst ## (fn thk => fn () => SYM (thk ())))
176    (match (bvs, tm) (bvs', tm') empty_raw_subst)
177
178  fun ho_match tm tm' : ho_substitution = ho_match_bvs ([], tm) ([], tm')
179end;
180
181fun var_ho_match_bvs vars (bvs, tm) (bvs', tm') =
182  let
183    val ho_sub as (sub, _) = ho_match_bvs (bvs, tm) (bvs', tm')
184    val _ = assert (subst_vars_in_set sub vars)
185      (ERR "var_ho_match_bvs" "subst vars not contained in set")
186  in
187    ho_sub
188  end;
189
190fun var_ho_match vars tm tm' = var_ho_match_bvs vars ([], tm) ([], tm');
191
192(*
193val tm = ``\(x : num). f``;
194val tm' = ``\(n : num). T``;
195val (sub, th) = try (ho_match tm) tm';
196
197val tm = ``!x y. f x y``;
198val tm' = ``!a b. f a a b``;
199val (sub, th) = try (ho_match tm) tm';
200pinst sub tm;
201REWR_CONV (th ()) tm';
202
203val tm = ``!x y z. f x z``;
204val tm' = ``!a b c. P (f a c) (g a)``;
205val (sub, th) = try (ho_match tm) tm';
206pinst sub tm;
207REWR_CONV (th ()) tm';
208
209val tm = ``\ (v : 'a). a v (b v)``;
210val tm' = ``\ (y : 'a). f y``;
211val (sub, th) = try (ho_match tm) tm';
212pinst sub tm;
213REWR_CONV (th ()) tm';
214
215val tm = ``\ (v : 'a). v``;
216val tm' = ``\ (y : 'b). y``;
217val (sub, th) = try (ho_match tm) tm';
218pinst sub tm;
219REWR_CONV (th ()) tm';
220*)
221
222(* ------------------------------------------------------------------------- *)
223(* Higher-order rewriting.                                                   *)
224(* ------------------------------------------------------------------------- *)
225
226(* Normal rewriting *)
227
228fun ho_subst_REWR th (sub, thk) = TRANS (thk ()) (PINST sub th);
229
230fun ho_REWR_CONV th =
231  let
232    val (vars, th') = thm_to_vthm th
233    val pat = LHS th'
234  in
235    ho_subst_REWR th' o var_ho_match vars pat
236  end;
237
238fun ho_REWRITE_CONV ths = QCONV (TOP_DEPTH_CONV (FIRSTC (map ho_REWR_CONV ths)));
239
240fun ho_REWRITE_TAC ths = CONV_TAC (ho_REWRITE_CONV ths);
241
242(* Conditional rewriting, pass in a prover *)
243
244fun ho_subst_COND_REWR th =
245  let
246    val (cond, _) = (dest_imp o concl) th
247  in
248    fn prover => fn (sub, thk) =>
249    let
250      val goal = pinst sub cond
251      val _ = trace_x 2 "ho_subst_COND_REWR: goal" term_to_string goal
252      val proved_cond = prover goal
253    in
254      TRANS (thk ()) (MP (PINST sub th) proved_cond)
255      handle h as HOL_ERR _ => raise err_BUG
256        ("ho_subst_COND_REWR: using crw\n" ^ thm_to_string th ^
257         "\nand proved_cond\n" ^ thm_to_string proved_cond) h
258    end
259  end;
260
261fun ho_COND_REWR_CONV th =
262  let
263    val (vars, th') = thm_to_vthm th
264    val pat = (lhs o snd o dest_imp o concl) th'
265    val f = ho_subst_COND_REWR th'
266  in
267    fn prover => f prover o var_ho_match vars pat
268  end;
269
270(* non-interactive mode
271*)
272end;
273