241 in map expand end |
239 in map expand end |
242 |
240 |
243 end |
241 end |
244 |
242 |
245 |
243 |
246 (** lambda-lifting **) |
|
247 |
|
248 local |
|
249 fun mk_def triggers Ts T lhs rhs = |
|
250 let |
|
251 val eq = HOLogic.eq_const T $ lhs $ rhs |
|
252 fun trigger () = |
|
253 [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]] |
|
254 |> map (HOLogic.mk_list @{typ SMT.pattern}) |
|
255 |> HOLogic.mk_list @{typ "SMT.pattern list"} |
|
256 fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t) |
|
257 in |
|
258 fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq |
|
259 else eq) |
|
260 end |
|
261 |
|
262 fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts |
|
263 |
|
264 fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t |
|
265 | dest_abs Ts t = (Ts, t) |
|
266 |
|
267 fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) = |
|
268 let |
|
269 val t1 = mk_abs Us t |
|
270 val bs = sort int_ord (Term.add_loose_bnos (t1, 0, [])) |
|
271 fun rep i k = if member (op =) bs i then (Bound k, k+1) else (Bound i, k) |
|
272 val (rs, _) = fold_map rep (0 upto length Ts - 1) 0 |
|
273 val t2 = Term.subst_bounds (rs, t1) |
|
274 val Ts' = map (nth Ts) bs |
|
275 val (_, t3) = dest_abs [] t2 |
|
276 val t4 = mk_abs Ts' t2 |
|
277 |
|
278 val T = Term.fastype_of1 (Us @ Ts, t) |
|
279 fun app f = Term.list_comb (f, map Bound (rev bs)) |
|
280 in |
|
281 (case Termtab.lookup defs t4 of |
|
282 SOME (f, _) => (app f, cx) |
|
283 | NONE => |
|
284 let |
|
285 val (n, ctxt') = |
|
286 yield_singleton Variable.variant_fixes Name.uu ctxt |
|
287 val (is, UTs) = split_list (map_index I (Us @ Ts')) |
|
288 val f = Free (n, rev UTs ---> T) |
|
289 val lhs = Term.list_comb (f, map Bound (rev is)) |
|
290 val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3 |
|
291 in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end) |
|
292 end |
|
293 |
|
294 fun traverse triggers Ts t = |
|
295 (case t of |
|
296 (q as Const (@{const_name All}, _)) $ Abs a => |
|
297 abs_traverse triggers Ts a #>> (fn a' => q $ Abs a') |
|
298 | (q as Const (@{const_name Ex}, _)) $ Abs a => |
|
299 abs_traverse triggers Ts a #>> (fn a' => q $ Abs a') |
|
300 | (l as Const (@{const_name Let}, _)) $ u $ Abs a => |
|
301 traverse triggers Ts u ##>> abs_traverse triggers Ts a #>> |
|
302 (fn (u', a') => l $ u' $ Abs a') |
|
303 | Abs _ => |
|
304 let val (Us, u) = dest_abs [] t |
|
305 in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end |
|
306 | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $) |
|
307 | _ => pair t) |
|
308 |
|
309 and abs_traverse triggers Ts (n, T, t) = |
|
310 traverse triggers (T::Ts) t #>> (fn t' => (n, T, t')) |
|
311 in |
|
312 |
|
313 fun lift_lambdas ctxt triggers ts = |
|
314 (Termtab.empty, ctxt) |
|
315 |> fold_map (traverse triggers []) ts |
|
316 |> (fn (us, (defs, ctxt')) => |
|
317 (ctxt', (Termtab.fold (cons o snd o snd) defs [], us))) |
|
318 |
|
319 end |
|
320 |
|
321 |
|
322 (** introduce explicit applications **) |
244 (** introduce explicit applications **) |
323 |
245 |
324 local |
246 local |
325 (* |
247 (* |
326 Make application explicit for functions with varying number of arguments. |
248 Make application explicit for functions with varying number of arguments. |
616 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
538 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
617 |
539 |
618 val (ctxt2, ts3) = |
540 val (ctxt2, ts3) = |
619 ts2 |
541 ts2 |
620 |> eta_expand ctxt1 is_fol funcs |
542 |> eta_expand ctxt1 is_fol funcs |
621 |> lift_lambdas ctxt1 true |
543 |> Lambda_Lifting.lift_lambdas ctxt1 true |
622 ||> (op @) |
544 ||> (op @) |
623 |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) |
545 |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) |
624 |
546 |
625 val ((rewrite_rules, extra_thms, builtin), ts4) = |
547 val ((rewrite_rules, extra_thms, builtin), ts4) = |
626 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |
548 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |