author | blanchet |
Wed, 19 Feb 2014 08:33:59 +0100 | |
changeset 55573 | 6a1cbddebf86 |
parent 55571 | a6153343c44f |
child 55575 | a5e33e18fb5c |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Lorenz Panny, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
Library for recursor and corecursor sugar. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
signature BNF_FP_REC_SUGAR_UTIL = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
10 |
sig |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
11 |
val indexed: 'a list -> int -> int list * int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
12 |
val indexedd: 'a list list -> int -> int list list * int |
54299 | 13 |
val indexeddd: 'a list list list -> int -> int list list list * int |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
14 |
val indexedddd: 'a list list list list -> int -> int list list list list * int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
15 |
val find_index_eq: ''a list -> ''a -> int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
16 |
val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
17 |
|
55571 | 18 |
val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list |
19 |
||
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54614
diff
changeset
|
20 |
val drop_all: term -> term |
54202
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
21 |
|
55571 | 22 |
val get_free_indices: ((binding * typ) * 'a) list -> term -> int list |
23 |
||
55573 | 24 |
(* needed here for bootstrapping; would be more at home in "bnf_fp_def_sugar.ML" (FIXME) *) |
55571 | 25 |
val unzip_recT: typ -> typ -> typ list |
55573 | 26 |
val mk_iter_fun_arg_types: int -> int list -> typ -> typ list list |
55571 | 27 |
val flat_rec_arg_args: 'a list list -> 'a list |
28 |
val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
|
55571 | 34 |
open BNF_Util |
35 |
open BNF_FP_Util |
|
36 |
||
54614 | 37 |
fun indexe _ h = (h, h + 1); |
38 |
fun indexed xs = fold_map indexe xs; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
fun indexedd xss = fold_map indexed xss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
fun indexeddd xsss = fold_map indexedd xsss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
fun indexedddd xssss = fold_map indexeddd xssss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
fun find_index_eq hs h = find_index (curry (op =) h) hs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
|
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
45 |
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
|
55571 | 47 |
fun tvar_subst thy Ts Us = |
48 |
Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; |
|
49 |
||
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54614
diff
changeset
|
50 |
fun drop_all t = |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
51 |
subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev, |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
52 |
strip_qnt_body @{const_name all} t); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
|
55571 | 54 |
fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
55 |
|> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
56 |
|> map_filter I; |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
57 |
|
55571 | 58 |
fun unzip_recT (Type (@{type_name prod}, _)) T = [T] |
59 |
| unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts |
|
60 |
| unzip_recT _ T = [T]; |
|
61 |
||
55573 | 62 |
fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; |
55571 | 63 |
|
64 |
fun flat_rec_arg_args xss = |
|
65 |
(* FIXME (once the old datatype package is phased out): The first line below gives the preferred |
|
66 |
order. The second line is for compatibility with the old datatype package. *) |
|
67 |
(* flat xss *) |
|
68 |
map hd xss @ maps tl xss; |
|
69 |
||
70 |
fun mk_co_iter thy fp fpT Cs t = |
|
71 |
let |
|
72 |
val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t); |
|
73 |
val fpT0 = fp_case fp prebody body; |
|
74 |
val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs); |
|
75 |
val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); |
|
76 |
in |
|
77 |
Term.subst_TVars rho t |
|
78 |
end; |
|
79 |
||
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
end; |