author | blanchet |
Wed, 28 Dec 2016 17:22:16 +0100 | |
changeset 64674 | ef0a5fd30f3b |
parent 63859 | dca6fabd8060 |
child 64705 | 7596b0736ab9 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_compat.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
3 |
Copyright 2013, 2014 |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
58147 | 5 |
Compatibility layer with the old datatype package. Partly based on |
58119 | 6 |
|
7 |
Title: HOL/Tools/Old_Datatype/old_datatype_data.ML |
|
8 |
Author: Stefan Berghofer, TU Muenchen |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
10 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
11 |
signature BNF_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
12 |
sig |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
13 |
datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
14 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
15 |
val get_all: theory -> preference list -> Old_Datatype_Aux.info Symtab.table |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
16 |
val get_info: theory -> preference list -> string -> Old_Datatype_Aux.info option |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
17 |
val the_info: theory -> preference list -> string -> Old_Datatype_Aux.info |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
18 |
val the_spec: theory -> string -> (string * sort) list * (string * typ list) list |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
19 |
val the_descr: theory -> preference list -> string list -> |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
20 |
Old_Datatype_Aux.descr * (string * sort) list * string list * string |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
21 |
* (string list * string list) * (typ list * typ list) |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
22 |
val get_constrs: theory -> string -> (string * typ) list option |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
23 |
val interpretation: string -> preference list -> |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
24 |
(Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory |
58125 | 25 |
val datatype_compat: string list -> local_theory -> local_theory |
26 |
val datatype_compat_global: string list -> theory -> theory |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
27 |
val datatype_compat_cmd: string list -> local_theory -> local_theory |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
28 |
val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory |
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63047
diff
changeset
|
29 |
val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs -> |
58684 | 30 |
local_theory -> (term list * thm list) * local_theory |
60003 | 31 |
val primrec_global: (binding * typ option * mixfix) list -> |
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63047
diff
changeset
|
32 |
Specification.multi_specs -> theory -> (term list * thm list) * theory |
60003 | 33 |
val primrec_overloaded: (string * (string * typ) * bool) list -> |
63064
2f18172214c8
support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents:
63047
diff
changeset
|
34 |
(binding * typ option * mixfix) list -> Specification.multi_specs -> theory -> |
58147 | 35 |
(term list * thm list) * theory |
60003 | 36 |
val primrec_simple: ((binding * typ) * mixfix) list -> term list -> |
58220 | 37 |
local_theory -> (string list * (term list * thm list)) * local_theory |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
38 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
structure BNF_LFP_Compat : BNF_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
|
54006 | 43 |
open Ctr_Sugar |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
open BNF_Util |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
45 |
open BNF_Tactics |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
open BNF_FP_Def_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
48 |
open BNF_FP_N2M_Sugar |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
49 |
open BNF_LFP |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
50 |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
51 |
val compat_N = "compat_"; |
58213 | 52 |
val rec_split_N = "rec_split_"; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
54 |
datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args; |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
55 |
|
58213 | 56 |
fun mk_split_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
57 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
58 |
fun repair_rec_arg_args [] [] = [] |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
59 |
| repair_rec_arg_args ((g_T as Type (@{type_name fun}, _)) :: g_Ts) (g :: gs) = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
60 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
61 |
val (x_Ts, body_T) = strip_type g_T; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
62 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
63 |
(case try HOLogic.dest_prodT body_T of |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
64 |
NONE => [g] |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
65 |
| SOME (fst_T, _) => |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
66 |
if member (op =) fpTs fst_T then |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
67 |
let val (xs, _) = mk_Frees "x" x_Ts ctxt in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
68 |
map (fn mk_proj => fold_rev Term.lambda xs (mk_proj (Term.list_comb (g, xs)))) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
69 |
[HOLogic.mk_fst, HOLogic.mk_snd] |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
70 |
end |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
71 |
else |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
72 |
[g]) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
73 |
:: repair_rec_arg_args g_Ts gs |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
74 |
end |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
75 |
| repair_rec_arg_args (g_T :: g_Ts) (g :: gs) = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
76 |
if member (op =) fpTs g_T then |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
77 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
78 |
val j = find_index (member (op =) Cs) g_Ts; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
79 |
val h = nth gs j; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
80 |
val g_Ts' = nth_drop j g_Ts; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
81 |
val gs' = nth_drop j gs; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
82 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
83 |
[g, h] :: repair_rec_arg_args g_Ts' gs' |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
84 |
end |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
85 |
else |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
86 |
[g] :: repair_rec_arg_args g_Ts gs; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
87 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
88 |
fun repair_back_rec_arg f_T f' = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
89 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
90 |
val g_Ts = Term.binder_types f_T; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
91 |
val (gs, _) = mk_Frees "g" g_Ts ctxt; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
92 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
93 |
fold_rev Term.lambda gs (Term.list_comb (f', |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
94 |
flat_rec_arg_args (repair_rec_arg_args g_Ts gs))) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
95 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
96 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
97 |
val f_Ts = binder_fun_types (fastype_of rec1); |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
98 |
val (fs', _) = mk_Frees "f" (replicate (length f_Ts) Term.dummyT) ctxt; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
99 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
100 |
fun mk_rec' recx = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
101 |
fold_rev Term.lambda fs' (Term.list_comb (recx, map2 repair_back_rec_arg f_Ts fs')) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
102 |
|> Syntax.check_term ctxt; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
103 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
104 |
map mk_rec' recs |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
105 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
106 |
|
58213 | 107 |
fun define_split_recs fpTs Cs recs lthy = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
108 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
109 |
val b_names = Name.variant_list [] (map base_name_of_typ fpTs); |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
110 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
111 |
fun mk_binding b_name = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
112 |
Binding.qualify true (compat_N ^ b_name) |
58213 | 113 |
(Binding.prefix_name rec_split_N (Binding.name b_name)); |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
114 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
115 |
val bs = map mk_binding b_names; |
58213 | 116 |
val rhss = mk_split_rec_rhs lthy fpTs Cs recs; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
117 |
in |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
118 |
@{fold_map 3} (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
119 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
120 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
121 |
fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
122 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
123 |
val f_Ts = binder_fun_types (fastype_of rec1); |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
124 |
val (fs, _) = mk_Frees "f" f_Ts ctxt; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
125 |
val frecs = map (fn recx => Term.list_comb (recx, fs)) recs; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
126 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
127 |
val Xs_frecs = Xs ~~ frecs; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
128 |
val fss = unflat ctrss fs; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
129 |
|
63047
2146553e96c6
generalize code to avoid making assumptions about type variable names
blanchet
parents:
62497
diff
changeset
|
130 |
fun mk_rec_call g n (Type (@{type_name fun}, [_, ran_T])) = |
2146553e96c6
generalize code to avoid making assumptions about type variable names
blanchet
parents:
62497
diff
changeset
|
131 |
Abs (Name.uu, Term.dummyT, mk_rec_call g (n + 1) ran_T) |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
132 |
| mk_rec_call g n X = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
133 |
let |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
134 |
val frec = the (AList.lookup (op =) Xs_frecs X); |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
135 |
val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
136 |
in frec $ xg end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
137 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
138 |
fun mk_rec_arg_arg ctrXs_T g = |
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
139 |
g :: (if member (op =) Xs (body_type ctrXs_T) then [mk_rec_call g 0 ctrXs_T] else []); |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
140 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
141 |
fun mk_goal frec ctrXs_Ts ctr f = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
142 |
let |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
143 |
val ctr_Ts = binder_types (fastype_of ctr); |
58217 | 144 |
val (gs, _) = mk_Frees "g" ctr_Ts ctxt; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
145 |
val gctr = Term.list_comb (ctr, gs); |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
146 |
val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg ctrXs_Ts gs); |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
147 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
148 |
fold_rev (fold_rev Logic.all) [fs, gs] |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
149 |
(mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) |
63047
2146553e96c6
generalize code to avoid making assumptions about type variable names
blanchet
parents:
62497
diff
changeset
|
150 |
|> Syntax.check_term ctxt |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
151 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
152 |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
153 |
val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
154 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
155 |
fun tac ctxt = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
156 |
unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN |
60728 | 157 |
HEADGOAL (rtac ctxt refl); |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
158 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
159 |
fun prove goal = |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
160 |
Goal.prove_sorry ctxt [] [] goal (tac o #context) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
161 |
|> Thm.close_derivation; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
162 |
in |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
163 |
map (map prove) goalss |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
164 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
165 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
166 |
fun define_split_rec_derive_induct_rec_thms Xs fpTs ctrXs_Tsss ctrss inducts induct recs0 rec_thmss |
58217 | 167 |
lthy = |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
168 |
let |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
169 |
val thy = Proof_Context.theory_of lthy; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
170 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
171 |
(* imperfect: will not yield the expected theorem for functions taking a large number of |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
172 |
arguments *) |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
173 |
val repair_induct = unfold_thms lthy @{thms all_mem_range}; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
174 |
|
58214 | 175 |
val inducts' = map repair_induct inducts; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
176 |
val induct' = repair_induct induct; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
177 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
178 |
val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
179 |
val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; |
58213 | 180 |
val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
181 |
val rec'_thmss = mk_split_rec_thmss lthy' Xs ctrXs_Tsss ctrss rec_thmss recs' rec'_defs; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
182 |
in |
58214 | 183 |
((inducts', induct', recs', rec'_thmss), lthy') |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
184 |
end; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
185 |
|
58219
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
186 |
fun body_rec_indices (Old_Datatype_Aux.DtRec kk) = [kk] |
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
187 |
| body_rec_indices (Old_Datatype_Aux.DtType (@{type_name fun}, [_, D])) = body_rec_indices D |
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
188 |
| body_rec_indices _ = []; |
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
189 |
|
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
190 |
fun reindex_desc desc = |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
191 |
let |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
192 |
val kks = map fst desc; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
193 |
val perm_kks = sort int_ord kks; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
194 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
195 |
fun perm_dtyp (Old_Datatype_Aux.DtType (s, Ds)) = Old_Datatype_Aux.DtType (s, map perm_dtyp Ds) |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
196 |
| perm_dtyp (Old_Datatype_Aux.DtRec kk) = |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
197 |
Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks) |
58113 | 198 |
| perm_dtyp D = D; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
199 |
in |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
200 |
if perm_kks = kks then |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
201 |
desc |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
202 |
else |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
203 |
perm_kks ~~ |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
204 |
map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc |
58113 | 205 |
end; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
206 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
207 |
fun mk_infos_of_mutually_recursive_new_datatypes prefs check_names fpT_names0 lthy = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
208 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
209 |
val thy = Proof_Context.theory_of lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
210 |
|
58315 | 211 |
fun not_datatype s = error (quote s ^ " is not a datatype"); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
212 |
fun not_mutually_recursive ss = |
58315 | 213 |
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
214 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
215 |
fun checked_fp_sugar_of s = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
216 |
(case fp_sugar_of lthy s of |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
217 |
SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) => |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
218 |
if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
219 |
| _ => not_datatype s); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
220 |
|
58229 | 221 |
val fpTs0 as Type (_, var_As) :: _ = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
222 |
map (#T o checked_fp_sugar_of o fst o dest_Type) |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
223 |
(#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0)))); |
63732 | 224 |
val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
225 |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
226 |
val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
227 |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
228 |
val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy; |
56452
0c98c9118407
preserve user type variable names to avoid mismatches/confusion
blanchet
parents:
56002
diff
changeset
|
229 |
val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As; |
56455
1ff66e72628b
allow arguments to 'datatype_compat' in disorder
blanchet
parents:
56453
diff
changeset
|
230 |
val fpTs = map (fn s => Type (s, As)) fpT_names; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
231 |
|
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
232 |
val nn_fp = length fpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
233 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
234 |
val mk_dtyp = Old_Datatype_Aux.dtyp_of_typ (map (apsnd (map Term.dest_TFree) o dest_Type) fpTs); |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
235 |
|
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
236 |
fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp); |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
237 |
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) = |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
238 |
(index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
239 |
|
63732 | 240 |
val fp_sugars as {fp, ...} :: _ = map checked_fp_sugar_of fpT_names; |
241 |
val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
242 |
val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
243 |
val all_infos = Old_Datatype_Data.get_all thy; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
244 |
val (orig_descr' :: nested_descrs) = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
245 |
if member (op =) prefs Keep_Nesting then [orig_descr] |
58125 | 246 |
else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
247 |
|
57798 | 248 |
fun cliquify_descr [] = [] |
249 |
| cliquify_descr [entry] = [[entry]] |
|
250 |
| cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) = |
|
251 |
let |
|
252 |
val nn = |
|
253 |
if member (op =) fpT_names T_name1 then |
|
254 |
nn_fp |
|
255 |
else |
|
256 |
(case Symtab.lookup all_infos T_name1 of |
|
257 |
SOME {descr, ...} => |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
258 |
length (filter_out (exists Old_Datatype_Aux.is_rec_type o #2 o snd) descr) |
57798 | 259 |
| NONE => raise Fail "unknown old-style datatype"); |
260 |
in |
|
261 |
chop nn full_descr ||> cliquify_descr |> op :: |
|
262 |
end; |
|
263 |
||
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
264 |
(* put nested types before the types that nest them, as needed for N2M *) |
56484 | 265 |
val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs); |
58340 | 266 |
val (mutual_cliques, descr) = |
57798 | 267 |
split_list (flat (map_index (fn (i, descr) => map (pair i) descr) |
268 |
(maps cliquify_descr descrs))); |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
269 |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
270 |
val fpTs' = Old_Datatype_Aux.get_rec_types descr; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
271 |
val nn = length fpTs'; |
55485 | 272 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
273 |
val fp_sugars = map (checked_fp_sugar_of o fst o dest_Type) fpTs'; |
58219
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
274 |
val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr; |
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
275 |
val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
276 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
277 |
val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
278 |
|
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
279 |
fun apply_comps n kk = |
55966 | 280 |
mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
281 |
|
58219
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
58218
diff
changeset
|
282 |
val callssss = map2 (map2 (map2 (map o apply_comps o num_binder_types))) ctr_Tsss kkssss; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
283 |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
284 |
val b_names = Name.variant_list [] (map base_name_of_typ fpTs'); |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
285 |
val compat_b_names = map (prefix compat_N) b_names; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
286 |
val compat_bs = map Binding.name compat_b_names; |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
287 |
|
58217 | 288 |
val ((fp_sugars', (lfp_sugar_thms', _)), lthy') = |
54286
22616f65d4ea
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents:
54267
diff
changeset
|
289 |
if nn > nn_fp then |
58340 | 290 |
mutualize_fp_sugars (K true) Least_FP mutual_cliques compat_bs fpTs' callers callssss |
291 |
fp_sugars lthy |
|
54286
22616f65d4ea
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents:
54267
diff
changeset
|
292 |
else |
58217 | 293 |
((fp_sugars, (NONE, NONE)), lthy); |
294 |
||
58460 | 295 |
fun mk_ctr_of ({fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} : fp_sugar) (Type (_, Ts)) = |
296 |
map (mk_ctr Ts) ctrs; |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
297 |
val substAT = Term.typ_subst_atomic (var_As ~~ As); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
298 |
|
58217 | 299 |
val Xs' = map #X fp_sugars'; |
58460 | 300 |
val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars'; |
58217 | 301 |
val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
302 |
val {fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars'; |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
303 |
val inducts = map (hd o #co_inducts o the o #fp_co_induct_sugar) fp_sugars'; |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
304 |
val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars'; |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63732
diff
changeset
|
305 |
val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars'; |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
306 |
|
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
307 |
fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T) |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
308 |
| is_nested_rec_type _ = false; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
309 |
|
58217 | 310 |
val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
311 |
if member (op =) prefs Keep_Nesting orelse |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
312 |
not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
313 |
((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy') |
63732 | 314 |
else if fp = Least_FP then |
58218
a92acec845a7
no type-based lookup -- these fail in the general, ambiguous case
blanchet
parents:
58217
diff
changeset
|
315 |
define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs |
58217 | 316 |
rec_thmss lthy' |
58214 | 317 |
|>> `(fn (inducts', induct', _, rec'_thmss) => |
63732 | 318 |
SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) |
319 |
else |
|
320 |
not_datatype fpT_name1; |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
321 |
|
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
322 |
val rec'_names = map (fst o dest_Const) recs'; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
323 |
val rec'_thms = flat rec'_thmss; |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
324 |
|
58460 | 325 |
fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy, |
326 |
injects, distincts, case_thms, case_cong, case_cong_weak, split, |
|
327 |
split_asm, ...}, ...}, ...} : fp_sugar) = |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
328 |
(T_name0, |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
329 |
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct', |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
330 |
inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names, |
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
331 |
rec_rewrites = rec'_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57807
diff
changeset
|
332 |
case_cong = case_cong, case_cong_weak = case_cong_weak, split = split, |
57794 | 333 |
split_asm = split_asm}); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
334 |
|
58217 | 335 |
val infos = map_index mk_info (take nn_fp fp_sugars'); |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
336 |
in |
58217 | 337 |
(nn, b_names, compat_b_names, lfp_sugar_thms'', infos, lthy'') |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
338 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
339 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
340 |
fun infos_of_new_datatype_mutual_cluster lthy prefs fpT_name = |
58358 | 341 |
let |
342 |
fun get prefs = |
|
343 |
#5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy) |
|
344 |
handle ERROR _ => []; |
|
345 |
in |
|
346 |
(case get prefs of |
|
347 |
[] => if member (op =) prefs Keep_Nesting then [] else get (Keep_Nesting :: prefs) |
|
348 |
| infos => infos) |
|
349 |
end; |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
350 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
351 |
fun get_all thy prefs = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
352 |
let |
59644 | 353 |
val ctxt = Proof_Context.init_global thy; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
354 |
val old_info_tab = Old_Datatype_Data.get_all thy; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
355 |
val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
356 |
|> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s)); |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
357 |
val new_infos = |
59644 | 358 |
maps (infos_of_new_datatype_mutual_cluster ctxt (insert (op =) Keep_Nesting prefs)) |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
359 |
new_T_names; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
360 |
in |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
361 |
fold (if member (op =) prefs Keep_Nesting then Symtab.update else Symtab.default) new_infos |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
362 |
old_info_tab |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
363 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
364 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
365 |
fun get_one get_old get_new thy prefs x = |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
366 |
let |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
367 |
val (get_fst, get_snd) = (get_old thy, get_new thy) |> member (op =) prefs Keep_Nesting ? swap; |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
368 |
in |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
369 |
(case get_fst x of NONE => get_snd x | res => res) |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
370 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
371 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
372 |
fun get_info_of_new_datatype prefs thy T_name = |
59644 | 373 |
let val ctxt = Proof_Context.init_global thy in |
374 |
AList.lookup (op =) (infos_of_new_datatype_mutual_cluster ctxt prefs T_name) T_name |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
375 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
376 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
377 |
fun get_info thy prefs = |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
378 |
get_one Old_Datatype_Data.get_info (get_info_of_new_datatype prefs) thy prefs; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
379 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
380 |
fun the_info thy prefs T_name = |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
381 |
(case get_info thy prefs T_name of |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
382 |
SOME info => info |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
383 |
| NONE => error ("Unknown datatype " ^ quote T_name)); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
384 |
|
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
385 |
fun the_spec thy T_name = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
386 |
let |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
387 |
val {descr, index, ...} = the_info thy [Keep_Nesting, Include_GFPs] T_name; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
388 |
val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index); |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
389 |
val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
390 |
val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0; |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
391 |
in (tfrees, ctrs) end; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
392 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
393 |
fun the_descr thy prefs (T_names0 as T_name01 :: _) = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
394 |
let |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
395 |
fun not_mutually_recursive ss = |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
396 |
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
397 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
398 |
val info = the_info thy prefs T_name01; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
399 |
val descr = #descr info; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
400 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
401 |
val (_, Ds, _) = the (AList.lookup (op =) descr (#index info)); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
402 |
val vs = map Old_Datatype_Aux.dest_DtTFree Ds; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
403 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
404 |
fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
405 |
| is_DtTFree _ = false; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
406 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
407 |
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
408 |
val protoTs as (dataTs, _) = chop k descr |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58684
diff
changeset
|
409 |
|> (apply2 o map) |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
410 |
(fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds)); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
411 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
412 |
val T_names = map fst dataTs; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
413 |
val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0 |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
414 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58684
diff
changeset
|
415 |
val (Ts, Us) = apply2 (map Type) protoTs; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
416 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
417 |
val names = map Long_Name.base_name T_names; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
418 |
val (auxnames, _) = Name.make_context names |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
419 |
|> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
420 |
val prefix = space_implode "_" names; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
421 |
in |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
422 |
(descr, vs, T_names, prefix, (names, auxnames), (Ts, Us)) |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
423 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
424 |
|
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
425 |
fun get_constrs thy T_name = |
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
426 |
try (the_spec thy) T_name |
58119 | 427 |
|> Option.map (fn (tfrees, ctrs) => |
428 |
let |
|
429 |
fun varify_tfree (s, S) = TVar ((s, 0), S); |
|
430 |
fun varify_typ (TFree x) = varify_tfree x |
|
431 |
| varify_typ T = T; |
|
432 |
||
433 |
val dataT = Type (T_name, map varify_tfree tfrees); |
|
434 |
||
435 |
fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT; |
|
436 |
in |
|
437 |
map (apsnd mk_ctr_typ) ctrs |
|
438 |
end); |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
439 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
440 |
fun old_interpretation_of prefs f config T_names thy = |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
441 |
if not (member (op =) prefs Keep_Nesting) orelse |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
442 |
exists (is_none o fp_sugar_of_global thy) T_names then |
58122 | 443 |
f config T_names thy |
444 |
else |
|
445 |
thy; |
|
446 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
447 |
fun new_interpretation_of prefs f (fp_sugars : fp_sugar list) thy = |
58122 | 448 |
let val T_names = map (fst o dest_Type o #T) fp_sugars in |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
449 |
if (member (op =) prefs Include_GFPs orelse forall (curry (op =) Least_FP o #fp) fp_sugars) |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
450 |
andalso (member (op =) prefs Keep_Nesting orelse |
58146 | 451 |
exists (is_none o Old_Datatype_Data.get_info thy) T_names) then |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
452 |
f Old_Datatype_Aux.default_config T_names thy |
58122 | 453 |
else |
454 |
thy |
|
455 |
end; |
|
456 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
457 |
fun interpretation name prefs f = |
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
458 |
Old_Datatype_Data.interpretation (old_interpretation_of prefs f) |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
459 |
#> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f); |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
460 |
|
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
63064
diff
changeset
|
461 |
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]}; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
462 |
|
58125 | 463 |
fun datatype_compat fpT_names lthy = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
464 |
let |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
465 |
val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
466 |
mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
467 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
468 |
val all_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
469 |
(case lfp_sugar_thms of |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
470 |
NONE => [] |
58214 | 471 |
| SOME ((inducts, induct, induct_attrs), (rec_thmss, _)) => |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
472 |
let |
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
58189
diff
changeset
|
473 |
val common_name = compat_N ^ mk_common_name b_names; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
474 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
475 |
val common_notes = |
58214 | 476 |
(if nn > 1 then [(inductN, [induct], induct_attrs)] else []) |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
477 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
478 |
|> map (fn (thmN, thms, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
479 |
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
480 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
481 |
val notes = |
58214 | 482 |
[(inductN, map single inducts, induct_attrs), |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
483 |
(recN, rec_thmss, code_nitpicksimp_simp_attrs)] |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
484 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
485 |
|> maps (fn (thmN, thmss, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
486 |
if forall null thmss then |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
487 |
[] |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
488 |
else |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
489 |
map2 (fn b_name => fn thms => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
490 |
((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])])) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
491 |
compat_b_names thmss); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
492 |
in |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
493 |
common_notes @ notes |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
494 |
end); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
495 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
496 |
val register_interpret = |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
497 |
Old_Datatype_Data.register infos |
58113 | 498 |
#> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
499 |
in |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
500 |
lthy' |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
501 |
|> Local_Theory.raw_theory register_interpret |
57633 | 502 |
|> Local_Theory.notes all_notes |
503 |
|> snd |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
504 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
505 |
|
58665 | 506 |
val datatype_compat_global = Named_Target.theory_map o datatype_compat; |
58125 | 507 |
|
508 |
fun datatype_compat_cmd raw_fpT_names lthy = |
|
509 |
let |
|
510 |
val fpT_names = |
|
511 |
map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy) |
|
512 |
raw_fpT_names; |
|
513 |
in |
|
514 |
datatype_compat fpT_names lthy |
|
515 |
end; |
|
516 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
517 |
fun add_datatype prefs old_specs thy = |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
518 |
let |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
519 |
val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs; |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
520 |
|
58300 | 521 |
fun new_type_args_of (s, S) = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
522 |
(if member (op =) prefs Kill_Type_Args then NONE else SOME Binding.empty, |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
523 |
(TFree (s, @{sort type}), S)); |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
524 |
fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx); |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
525 |
|
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
526 |
fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) = |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
527 |
(((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs), |
62324 | 528 |
(Binding.empty, Binding.empty, Binding.empty)), []); |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
529 |
|
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
530 |
val new_specs = map new_spec_of old_specs; |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
531 |
in |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
532 |
(fpT_names, |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
533 |
thy |
58665 | 534 |
|> Named_Target.theory_map |
535 |
(co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs)) |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58340
diff
changeset
|
536 |
|> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names))) |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
537 |
end; |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
538 |
|
60004 | 539 |
fun old_of_new f (ts, _, simpss) = (ts, f simpss); |
540 |
||
64674
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
63859
diff
changeset
|
541 |
val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec false []; |
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
63859
diff
changeset
|
542 |
val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global false []; |
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
63859
diff
changeset
|
543 |
val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded false []; |
62497
5b5b704f4811
respect qualification when noting theorems in prim(co)rec
traytel
parents:
62324
diff
changeset
|
544 |
val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo |
64674
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
63859
diff
changeset
|
545 |
BNF_LFP_Rec_Sugar.primrec_simple false; |
58126 | 546 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
547 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59644
diff
changeset
|
548 |
Outer_Syntax.local_theory @{command_keyword datatype_compat} |
58315 | 549 |
"register datatypes as old-style datatypes and derive old-style properties" |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
550 |
(Scan.repeat1 Parse.type_const >> datatype_compat_cmd); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
551 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
552 |
end; |