author | blanchet |
Fri, 05 Sep 2014 00:41:01 +0200 | |
changeset 58189 | 9d714be4f028 |
parent 58186 | a6c3962ea907 |
child 58211 | c1f3fa32d322 |
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 |
58125 | 13 |
datatype nesting_preference = Keep_Nesting | Unfold_Nesting |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
14 |
|
58125 | 15 |
val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table |
16 |
val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option |
|
17 |
val the_info: theory -> nesting_preference -> 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 |
58125 | 19 |
val the_descr: theory -> nesting_preference -> 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 |
58186 | 23 |
val interpretation: string -> nesting_preference -> |
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 |
58125 | 28 |
val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory -> |
29 |
string list * theory |
|
58126 | 30 |
val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> |
31 |
local_theory -> (term list * thm list) * local_theory |
|
58147 | 32 |
val add_primrec_global: (binding * typ option * mixfix) list -> |
33 |
(Attrib.binding * term) list -> theory -> (term list * thm list) * theory |
|
34 |
val add_primrec_overloaded: (string * (string * typ) * bool) list -> |
|
35 |
(binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> |
|
36 |
(term list * thm list) * theory |
|
37 |
val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> |
|
38 |
local_theory -> (string list * (term list * (int 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
|
39 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
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
|
42 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
|
54006 | 44 |
open Ctr_Sugar |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
45 |
open BNF_Util |
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 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
51 |
val compatN = "compat_"; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
52 |
|
58125 | 53 |
datatype nesting_preference = Keep_Nesting | Unfold_Nesting; |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
54 |
|
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
55 |
fun reindex_desc desc = |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
56 |
let |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
57 |
val kks = map fst desc; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
58 |
val perm_kks = sort int_ord kks; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
59 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
60 |
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
|
61 |
| 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
|
62 |
Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks) |
58113 | 63 |
| perm_dtyp D = D; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
64 |
in |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
65 |
if perm_kks = kks then |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
66 |
desc |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
67 |
else |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
68 |
perm_kks ~~ |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
69 |
map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc |
58113 | 70 |
end; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
71 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
72 |
fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref 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
|
73 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
74 |
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
|
75 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
76 |
fun not_datatype s = error (quote s ^ " is not a new-style datatype"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
77 |
fun not_mutually_recursive ss = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
78 |
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
79 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
fun lfp_sugar_of s = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
81 |
(case fp_sugar_of lthy s of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
82 |
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
| _ => not_datatype s); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
84 |
|
56455
1ff66e72628b
allow arguments to 'datatype_compat' in disorder
blanchet
parents:
56453
diff
changeset
|
85 |
val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0))); |
1ff66e72628b
allow arguments to 'datatype_compat' in disorder
blanchet
parents:
56453
diff
changeset
|
86 |
val fpT_names = 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
|
87 |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
88 |
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
|
89 |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
val fpTs = map (fn s => Type (s, As)) fpT_names; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
93 |
|
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
94 |
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
|
95 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
96 |
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
|
97 |
|
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
(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
|
101 |
|
56455
1ff66e72628b
allow arguments to 'datatype_compat' in disorder
blanchet
parents:
56453
diff
changeset
|
102 |
val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
103 |
val orig_descr = map3 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
|
104 |
val all_infos = Old_Datatype_Data.get_all thy; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
105 |
val (orig_descr' :: nested_descrs) = |
58125 | 106 |
if nesting_pref = Keep_Nesting then [orig_descr] |
107 |
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
|
108 |
|
57798 | 109 |
fun cliquify_descr [] = [] |
110 |
| cliquify_descr [entry] = [[entry]] |
|
111 |
| cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) = |
|
112 |
let |
|
113 |
val nn = |
|
114 |
if member (op =) fpT_names T_name1 then |
|
115 |
nn_fp |
|
116 |
else |
|
117 |
(case Symtab.lookup all_infos T_name1 of |
|
118 |
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
|
119 |
length (filter_out (exists Old_Datatype_Aux.is_rec_type o #2 o snd) descr) |
57798 | 120 |
| NONE => raise Fail "unknown old-style datatype"); |
121 |
in |
|
122 |
chop nn full_descr ||> cliquify_descr |> op :: |
|
123 |
end; |
|
124 |
||
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
125 |
(* put nested types before the types that nest them, as needed for N2M *) |
56484 | 126 |
val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs); |
127 |
val (cliques, descr) = |
|
57798 | 128 |
split_list (flat (map_index (fn (i, descr) => map (pair i) descr) |
129 |
(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
|
130 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
131 |
val dest_dtyp = Old_Datatype_Aux.typ_of_dtyp descr; |
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
|
132 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
133 |
val Ts = Old_Datatype_Aux.get_rec_types descr; |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
134 |
val nn = length Ts; |
55485 | 135 |
|
136 |
val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; |
|
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
137 |
val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
138 |
val kkssss = |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset
|
139 |
map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) 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
|
140 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
141 |
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
|
142 |
|
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
143 |
fun apply_comps n kk = |
55966 | 144 |
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
|
145 |
|
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
146 |
val callssss = |
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
147 |
map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
148 |
|
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
149 |
val b_names = Name.variant_list [] (map base_name_of_typ Ts); |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
150 |
val compat_b_names = map (prefix compatN) b_names; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
151 |
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
|
152 |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
153 |
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
|
154 |
if nn > nn_fp then |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
155 |
mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 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
|
156 |
else |
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
|
157 |
((fp_sugars0, (NONE, NONE)), lthy); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
158 |
|
56453
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
159 |
val recs = map (fst o dest_Const o #co_rec) fp_sugars; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
160 |
val rec_thms = maps #co_rec_thms fp_sugars; |
00548d372f02
support deeply nested datatypes in 'datatype_compat'
blanchet
parents:
56452
diff
changeset
|
161 |
|
55540
892a425c5eaa
follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
blanchet
parents:
55539
diff
changeset
|
162 |
val {common_co_inducts = [induct], ...} :: _ = fp_sugars; |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
163 |
val inducts = map (the_single o #co_inducts) fp_sugars; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
164 |
|
55567 | 165 |
fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57807
diff
changeset
|
166 |
distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) = |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
167 |
(T_name0, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
168 |
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, |
57794 | 169 |
inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, |
170 |
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
|
171 |
case_cong = case_cong, case_cong_weak = case_cong_weak, split = split, |
57794 | 172 |
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
|
173 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
174 |
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
|
175 |
in |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
176 |
(nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
177 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
178 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
179 |
fun infos_of_new_datatype_mutual_cluster lthy fpT_name = |
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
180 |
#5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy) |
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
181 |
handle ERROR _ => []; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
182 |
|
58125 | 183 |
fun get_all thy nesting_pref = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
184 |
let |
58133 | 185 |
val lthy = Proof_Context.init_global thy; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
186 |
val old_info_tab = Old_Datatype_Data.get_all thy; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
187 |
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
|
188 |
|> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s)); |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
189 |
val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
190 |
in |
58125 | 191 |
fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
192 |
old_info_tab |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
193 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
194 |
|
58125 | 195 |
fun get_one get_old get_new thy nesting_pref x = |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
196 |
let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
197 |
(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
|
198 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
199 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
200 |
fun get_info_of_new_datatype thy T_name = |
58130 | 201 |
let val lthy = Proof_Context.init_global thy in |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
202 |
AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
203 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
204 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
205 |
val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
206 |
|
58125 | 207 |
fun the_info thy nesting_pref T_name = |
208 |
(case get_info thy nesting_pref T_name of |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
209 |
SOME info => info |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
210 |
| NONE => error ("Unknown datatype " ^ quote T_name)); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
211 |
|
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
212 |
fun the_spec thy T_name = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
213 |
let |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
214 |
val {descr, index, ...} = the_info thy Keep_Nesting T_name; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
215 |
val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index); |
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
216 |
val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
217 |
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
|
218 |
in (tfrees, ctrs) end; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
219 |
|
58125 | 220 |
fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
221 |
let |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
222 |
fun not_mutually_recursive ss = |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
223 |
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
|
224 |
|
58125 | 225 |
val info = the_info thy nesting_pref T_name01; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
226 |
val descr = #descr info; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
227 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
228 |
val (_, Ds, _) = the (AList.lookup (op =) descr (#index info)); |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
229 |
val vs = map Old_Datatype_Aux.dest_DtTFree Ds; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
230 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
231 |
fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
232 |
| is_DtTFree _ = false; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
233 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
234 |
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
|
235 |
val protoTs as (dataTs, _) = chop k descr |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
236 |
|> (pairself o map) |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
237 |
(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
|
238 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
239 |
val T_names = map fst dataTs; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
240 |
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
|
241 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
242 |
val (Ts, Us) = (pairself o map) Type protoTs; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
243 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
244 |
val names = map Long_Name.base_name T_names; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
245 |
val (auxnames, _) = Name.make_context names |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
246 |
|> 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
|
247 |
val prefix = space_implode "_" names; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
248 |
in |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
249 |
(descr, vs, T_names, prefix, (names, auxnames), (Ts, Us)) |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
250 |
end; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
251 |
|
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
252 |
fun get_constrs thy T_name = |
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58126
diff
changeset
|
253 |
try (the_spec thy) T_name |
58119 | 254 |
|> Option.map (fn (tfrees, ctrs) => |
255 |
let |
|
256 |
fun varify_tfree (s, S) = TVar ((s, 0), S); |
|
257 |
fun varify_typ (TFree x) = varify_tfree x |
|
258 |
| varify_typ T = T; |
|
259 |
||
260 |
val dataT = Type (T_name, map varify_tfree tfrees); |
|
261 |
||
262 |
fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT; |
|
263 |
in |
|
264 |
map (apsnd mk_ctr_typ) ctrs |
|
265 |
end); |
|
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
266 |
|
58125 | 267 |
fun old_interpretation_of nesting_pref f config T_names thy = |
268 |
if nesting_pref = Unfold_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then |
|
58122 | 269 |
f config T_names thy |
270 |
else |
|
271 |
thy; |
|
272 |
||
58137 | 273 |
fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy = |
58122 | 274 |
let val T_names = map (fst o dest_Type o #T) fp_sugars in |
58146 | 275 |
if forall (curry (op =) Least_FP o #fp) fp_sugars andalso |
276 |
(nesting_pref = Keep_Nesting orelse |
|
277 |
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
|
278 |
f Old_Datatype_Aux.default_config T_names thy |
58122 | 279 |
else |
280 |
thy |
|
281 |
end; |
|
282 |
||
58186 | 283 |
fun interpretation name nesting_pref f = |
58177
166131276380
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
blanchet
parents:
58147
diff
changeset
|
284 |
let val new_f = new_interpretation_of nesting_pref f in |
166131276380
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
blanchet
parents:
58147
diff
changeset
|
285 |
Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f) |
58186 | 286 |
#> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f) |
58177
166131276380
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
blanchet
parents:
58147
diff
changeset
|
287 |
end; |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
288 |
|
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
289 |
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
290 |
|
58125 | 291 |
fun datatype_compat fpT_names lthy = |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
292 |
let |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
293 |
val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') = |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58130
diff
changeset
|
294 |
mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting 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
|
295 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
296 |
val all_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
297 |
(case lfp_sugar_thms of |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
298 |
NONE => [] |
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
299 |
| SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) => |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
300 |
let |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
301 |
val common_name = compatN ^ mk_common_name b_names; |
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
302 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
303 |
val common_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
304 |
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
305 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
306 |
|> map (fn (thmN, thms, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
307 |
((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
|
308 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
309 |
val notes = |
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
310 |
[(inductN, map single induct_thms, 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
|
311 |
(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
|
312 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
313 |
|> maps (fn (thmN, thmss, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
314 |
if forall null thmss then |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
315 |
[] |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
316 |
else |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
317 |
map2 (fn b_name => fn thms => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
318 |
((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
|
319 |
compat_b_names thmss); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
320 |
in |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
321 |
common_notes @ notes |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
322 |
end); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
323 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
324 |
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
|
325 |
Old_Datatype_Data.register infos |
58113 | 326 |
#> 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
|
327 |
in |
58117
9608028d8f43
more compatibility between old- and new-style datatypes
blanchet
parents:
58113
diff
changeset
|
328 |
lthy' |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
329 |
|> Local_Theory.raw_theory register_interpret |
57633 | 330 |
|> Local_Theory.notes all_notes |
331 |
|> snd |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
332 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
333 |
|
58179 | 334 |
val datatype_compat_global = map_local_theory o datatype_compat; |
58125 | 335 |
|
336 |
fun datatype_compat_cmd raw_fpT_names lthy = |
|
337 |
let |
|
338 |
val fpT_names = |
|
339 |
map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy) |
|
340 |
raw_fpT_names; |
|
341 |
in |
|
342 |
datatype_compat fpT_names lthy |
|
343 |
end; |
|
344 |
||
345 |
fun add_datatype nesting_pref old_specs thy = |
|
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
346 |
let |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
347 |
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
|
348 |
|
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
349 |
fun new_type_args_of (s, S) = (SOME Binding.empty, (TFree (s, @{sort type}), S)); |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
350 |
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
|
351 |
|
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
352 |
fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) = |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
353 |
(((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs), |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
354 |
(Binding.empty, Binding.empty)), []); |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
355 |
|
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
356 |
val new_specs = map new_spec_of old_specs; |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
357 |
in |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
358 |
(fpT_names, |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
359 |
thy |
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58186
diff
changeset
|
360 |
|> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs)) |
58125 | 361 |
|> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names))) |
58123
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
362 |
end; |
62765d39539f
implemented compatibility definition of datatype
blanchet
parents:
58122
diff
changeset
|
363 |
|
58126 | 364 |
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec; |
58147 | 365 |
val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global; |
366 |
val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded; |
|
367 |
val add_primrec_simple = apfst (apsnd (apsnd (apsnd flat o apfst flat))) ooo |
|
368 |
BNF_LFP_Rec_Sugar.add_primrec_simple; |
|
58126 | 369 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
370 |
val _ = |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
371 |
Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
54025 | 372 |
"register new-style datatypes as old-style datatypes" |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
373 |
(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
|
374 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
375 |
end; |