304 |
304 |
305 fun dest_plain_fun t = |
305 fun dest_plain_fun t = |
306 case try dest_fun_upd t of |
306 case try dest_fun_upd t of |
307 NONE => |
307 NONE => |
308 (case t of |
308 (case t of |
309 (Abs (_, _, Const (@{const_name HOL.undefined}, _))) => [] |
309 Abs (_, _, _) => ([], t) |
310 | _ => raise TERM ("dest_plain_fun", [t])) |
310 | _ => raise TERM ("dest_plain_fun", [t])) |
311 | SOME (t0, (t1, t2)) => (t1, t2) :: dest_plain_fun t0 |
311 | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_plain_fun t0) |
312 |
312 |
313 fun make_plain_fun T1 T2 tps = |
313 fun make_plain_fun T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t |
314 fold_rev (mk_fun_upd T1 T2) tps (absdummy (T1, Const ("_", T2))) |
|
315 |
314 |
316 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) |
315 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) |
317 | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps |
316 | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps |
318 | make_set T1 ((t1, @{const True}) :: tps) = |
317 | make_set T1 ((t1, @{const True}) :: tps) = |
319 Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) |
318 Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) |
320 $ t1 $ (make_set T1 tps) |
319 $ t1 $ (make_set T1 tps) |
321 | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) |
320 | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) |
322 |
321 |
|
322 fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) |
|
323 | make_coset T tps = |
|
324 let |
|
325 val U = T --> @{typ bool} |
|
326 fun invert @{const False} = @{const True} |
|
327 | invert @{const True} = @{const False} |
|
328 in |
|
329 Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) |
|
330 $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) |
|
331 end |
|
332 |
323 fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
333 fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
324 | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps |
334 | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps |
325 | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) |
335 | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) |
326 |
336 |
327 fun post_process_term t = |
337 fun post_process_term t = |
328 case fastype_of t of |
338 let |
329 Type (@{type_name fun}, [T1, T2]) => |
339 (*val _ = tracing ("post_process:" ^ Syntax.string_of_term ctxt t)*) |
330 (case try dest_plain_fun t of |
340 fun map_Abs f t = |
331 SOME tps => |
341 case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) |
332 tps |
342 fun process_args t = case strip_comb t of |
333 |> map (pairself post_process_term) |
343 (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) |
334 |> (case T2 of |
344 in |
335 @{typ bool} => rev #> make_set T1 |
345 case fastype_of t of |
336 | Type (@{type_name option}, _) => make_map T1 T2 |
346 Type (@{type_name fun}, [T1, T2]) => |
337 | _ => make_plain_fun T1 T2) |
347 (case try dest_plain_fun t of |
338 | NONE => t) |
348 SOME (tps, t) => |
339 | _ => t |
349 (map (pairself post_process_term) tps, map_Abs post_process_term t) |
|
350 |> (case T2 of |
|
351 @{typ bool} => |
|
352 (case t of |
|
353 Abs(_, _, @{const True}) => fst #> rev #> make_set T1 |
|
354 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1 |
|
355 | _ => raise TERM ("post_process_term", [t])) |
|
356 | Type (@{type_name option}, _) => |
|
357 (case t of |
|
358 Abs(_, _, Const(@{const_name None}, _)) => fst #> (make_map T1 T2) |
|
359 | _ => make_plain_fun T1 T2) |
|
360 | _ => make_plain_fun T1 T2) |
|
361 | NONE => raise TERM ("post_process_term", [t])) |
|
362 | _ => process_args t |
|
363 end |
340 |
364 |
341 (** generator compiliation **) |
365 (** generator compiliation **) |
342 |
366 |
343 fun compile_generator_expr ctxt t = |
367 fun compile_generator_expr ctxt t = |
344 let |
368 let |