1 (* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML |
|
2 Author: Lorenz Panny, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2013 |
|
5 |
|
6 Library for recursor and corecursor sugar. |
|
7 *) |
|
8 |
|
9 signature BNF_FP_REC_SUGAR_UTIL = |
|
10 sig |
|
11 val indexed: 'a list -> int -> int list * int |
|
12 val indexedd: 'a list list -> int -> int list list * int |
|
13 val indexeddd: 'a list list list -> int -> int list list list * int |
|
14 val indexedddd: 'a list list list list -> int -> int list list list list * int |
|
15 val find_index_eq: ''a list -> ''a -> int |
|
16 val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list |
|
17 |
|
18 val drop_all: term -> term |
|
19 |
|
20 val mk_partial_compN: int -> typ -> term -> term |
|
21 val mk_partial_comp: typ -> typ -> term -> term |
|
22 val mk_compN: int -> typ list -> term * term -> term |
|
23 val mk_comp: typ list -> term * term -> term |
|
24 |
|
25 val get_indices: ((binding * typ) * 'a) list -> term -> int list |
|
26 end; |
|
27 |
|
28 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = |
|
29 struct |
|
30 |
|
31 fun indexe _ h = (h, h + 1); |
|
32 fun indexed xs = fold_map indexe xs; |
|
33 fun indexedd xss = fold_map indexed xss; |
|
34 fun indexeddd xsss = fold_map indexedd xsss; |
|
35 fun indexedddd xssss = fold_map indexeddd xssss; |
|
36 |
|
37 fun find_index_eq hs h = find_index (curry (op =) h) hs; |
|
38 |
|
39 fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x); |
|
40 |
|
41 fun drop_all t = |
|
42 subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev, |
|
43 strip_qnt_body @{const_name all} t); |
|
44 |
|
45 fun mk_partial_comp gT fT g = |
|
46 let val T = domain_type fT --> range_type gT in |
|
47 Const (@{const_name Fun.comp}, gT --> fT --> T) $ g |
|
48 end; |
|
49 |
|
50 fun mk_partial_compN 0 _ g = g |
|
51 | mk_partial_compN n fT g = |
|
52 let val g' = mk_partial_compN (n - 1) (range_type fT) g in |
|
53 mk_partial_comp (fastype_of g') fT g' |
|
54 end; |
|
55 |
|
56 fun mk_compN n bound_Ts (g, f) = |
|
57 let val typof = curry fastype_of1 bound_Ts in |
|
58 mk_partial_compN n (typof f) g $ f |
|
59 end; |
|
60 |
|
61 val mk_comp = mk_compN 1; |
|
62 |
|
63 fun get_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes |
|
64 |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) |
|
65 |> map_filter I; |
|
66 |
|
67 end; |
|