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