author  wenzelm 
Sat, 08 Nov 2014 16:55:41 +0100  
changeset 58948  f6ecc0fb2066 
parent 58734  20235f0512e2 
child 59040  ac836bcddb3b 
permissions  rwrr 
55061  1 
(* Title: HOL/Tools/BNF/bnf_fp_n2m_sugar.ML 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

3 
Copyright 2013 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

4 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

5 
Suggared flattening of nested to mutual (co)recursion. 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

6 
*) 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

7 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

8 
signature BNF_FP_N2M_SUGAR = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

9 
sig 
55343  10 
val unfold_lets_splits: term > term 
57895  11 
val unfold_splits_lets: term > term 
54243  12 
val dest_map: Proof.context > string > term > term * term list 
13 

58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

14 
val mutualize_fp_sugars: (string > bool) > BNF_Util.fp_kind > int list > binding list > 
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

15 
typ list > term list > term list list list list > BNF_FP_Def_Sugar.fp_sugar list > 
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

16 
local_theory > 
58180  17 
(BNF_FP_Def_Sugar.fp_sugar list 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

18 
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

19 
* local_theory 
58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

20 
val nested_to_mutual_fps: (string > bool) > BNF_Util.fp_kind > binding list > typ list > 
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

21 
term list > (term * term list list) list list > local_theory > 
58180  22 
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

23 
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) 
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

24 
* local_theory 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

25 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

26 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

27 
structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

28 
struct 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

29 

54006  30 
open Ctr_Sugar 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

31 
open BNF_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

32 
open BNF_Def 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

33 
open BNF_FP_Util 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

34 
open BNF_FP_Def_Sugar 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

35 
open BNF_FP_N2M 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

36 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

37 
val n2mN = "n2m_" 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

38 

54256  39 
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option); 
40 

41 
structure Data = Generic_Data 

42 
( 

43 
type T = n2m_sugar Typtab.table; 

44 
val empty = Typtab.empty; 

45 
val extend = I; 

55394
d5ebe055b599
more liberal merging of BNFs and constructor sugar
blanchet
parents:
55343
diff
changeset

46 
fun merge data : T = Typtab.merge (K true) data; 
54256  47 
); 
48 

49 
fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) = 

50 
(map (morph_fp_sugar phi) fp_sugars, 

51 
(Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt, 

52 
Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt)); 

53 

58115  54 
val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism; 
54256  55 

56 
fun n2m_sugar_of ctxt = 

57 
Typtab.lookup (Data.get (Context.Proof ctxt)) 

58115  58 
#> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt)); 
54256  59 

60 
fun register_n2m_sugar key n2m_sugar = 

61 
Local_Theory.declaration {syntax = false, pervasive = false} 

55444
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga  'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
55414
diff
changeset

62 
(fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar))); 
54256  63 

57895  64 
fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) = 
57897  65 
unfold_lets_splits (betapply (unfold_splits_lets u, t)) 
57895  66 
 unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u) 
67 
 unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t) 

68 
 unfold_lets_splits t = t 

57897  69 
and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) = 
57895  70 
(case unfold_splits_lets u of 
55336  71 
u' as Abs (s1, T1, Abs (s2, T2, _)) => 
72 
let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in 

73 
lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) 

54243  74 
end 
57897  75 
 _ => t $ unfold_lets_splits u) 
76 
 unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t 

77 
 unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u) 

57895  78 
 unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t) 
79 
 unfold_splits_lets t = unfold_lets_splits t; 

54243  80 

81 
fun mk_map_pattern ctxt s = 

82 
let 

83 
val bnf = the (bnf_of ctxt s); 

84 
val mapx = map_of_bnf bnf; 

85 
val live = live_of_bnf bnf; 

86 
val (f_Ts, _) = strip_typeN live (fastype_of mapx); 

54265
3e1d230f1c00
make local theory operations nonpervasive (makes more intuitive sense)
blanchet
parents:
54256
diff
changeset

87 
val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts; 
54243  88 
in 
89 
(mapx, betapplys (mapx, fs)) 

90 
end; 

91 

92 
fun dest_map ctxt s call = 

93 
let 

94 
val (map0, pat) = mk_map_pattern ctxt s; 

95 
val (_, tenv) = fo_match ctxt call pat; 

96 
in 

97 
(map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv []) 

98 
end; 

99 

54276  100 
fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t]) 
101 
 dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1; 

54239  102 

54245  103 
fun map_partition f xs = 
104 
fold_rev (fn x => fn (ys, (good, bad)) => 

105 
case f x of SOME y => (y :: ys, (x :: good, bad))  NONE => (ys, (good, x :: bad))) 

106 
xs ([], ([], [])); 

107 

58222  108 
fun key_of_fp_eqs fp As fpTs fp_eqs = 
109 
Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs) 

110 
> Term.map_atyps (fn T as TFree (_, S) => 

111 
(case find_index (curry (op =) T) As of 

112 
~1 => T 

113 
 j => TFree ("'" ^ string_of_int j, S))); 

54256  114 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

115 
fun get_indices callers t = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

116 
callers 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

117 
> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

118 
> map_filter I; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

119 

58340  120 
fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_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:
54284
diff
changeset

121 
let 
58280
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

122 
val thy = Proof_Context.theory_of no_defs_lthy; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

123 

58280
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

124 
val qsotm = quote o Syntax.string_of_term no_defs_lthy; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

125 

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:
55444
diff
changeset

126 
fun incompatible_calls ts = 
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:
55444
diff
changeset

127 
error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts)); 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

128 
fun mutual_self_call caller t = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

129 
error ("Unsupported mutual selfcall " ^ qsotm t ^ " from " ^ qsotm caller); 
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

130 
fun nested_self_call t = 
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

131 
error ("Unsupported nested selfcall " ^ qsotm t); 
54245  132 

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:
54284
diff
changeset

133 
val b_names = map Binding.name_of bs; 
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:
54284
diff
changeset

134 
val fp_b_names = map base_name_of_typ fpTs; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

135 

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:
54284
diff
changeset

136 
val nn = length fpTs; 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset

137 
val kks = 0 upto nn  1; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

138 

58460  139 
fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) = 
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:
54284
diff
changeset

140 
let 
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:
54284
diff
changeset

141 
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; 
54740  142 
val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho); 
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:
54284
diff
changeset

143 
in 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset

144 
morph_ctr_sugar phi ctr_sugar 
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:
54284
diff
changeset

145 
end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

146 

58460  147 
val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0; 
58462  148 
val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0; 
54302  149 
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

150 

54302  151 
val ctrss = map #ctrs ctr_sugars; 
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:
54284
diff
changeset

152 
val ctr_Tss = map (map fastype_of) ctrss; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

153 

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:
54284
diff
changeset

154 
val As' = fold (fold Term.add_tfreesT) ctr_Tss []; 
58236  155 
val unsorted_As' = map (apsnd (K @{sort type})) As'; 
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:
54284
diff
changeset

156 
val As = map TFree As'; 
58236  157 
val unsorted_As = map TFree unsorted_As'; 
158 

159 
val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As); 

160 
val unsorted_fpTs = map unsortAT fpTs; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

161 

58280
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

162 
val ((Cs, Xs), names_lthy) = 
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

163 
no_defs_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:
54284
diff
changeset

164 
> fold Variable.declare_typ As 
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:
54284
diff
changeset

165 
> mk_TFrees nn 
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:
54284
diff
changeset

166 
>> variant_tfrees fp_b_names; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

167 

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:
54284
diff
changeset

168 
fun check_call_dead live_call call = 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

169 
if null (get_indices callers call) then () else incompatible_calls [live_call, call]; 
54245  170 

55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

171 
fun freeze_fpTs_type_based_default (T as Type (s, Ts)) = 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

172 
(case filter (curry (op =) T o snd) (map_index I fpTs) of 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

173 
[(kk, _)] => nth Xs kk 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

174 
 _ => Type (s, map freeze_fpTs_type_based_default Ts)) 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

175 
 freeze_fpTs_type_based_default T = T; 
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:
55444
diff
changeset

176 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

177 
fun freeze_fpTs_mutual_call kk fpT calls T = 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

178 
(case fold (union (op =)) (map (get_indices callers) calls) [] of 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

179 
[] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

180 
 [kk'] => 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

181 
if T = fpT andalso kk' <> kk then 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

182 
mutual_self_call (nth callers kk) 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

183 
(the (find_first (not o null o get_indices callers) calls)) 
58290
14e186d2dd3a
proper checks  the calls data structure may contain spurious entries
blanchet
parents:
58280
diff
changeset

184 
else if T = nth fpTs kk' then 
14e186d2dd3a
proper checks  the calls data structure may contain spurious entries
blanchet
parents:
58280
diff
changeset

185 
nth Xs kk' 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

186 
else 
58290
14e186d2dd3a
proper checks  the calls data structure may contain spurious entries
blanchet
parents:
58280
diff
changeset

187 
freeze_fpTs_type_based_default T 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

188 
 _ => incompatible_calls calls); 
54253  189 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

190 
fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls)) 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

191 
(Type (s, Ts)) = 
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

192 
if Ts' = Ts then 
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

193 
nested_self_call live_call 
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

194 
else 
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset

195 
(List.app (check_call_dead live_call) dead_calls; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

196 
Type (s, map2 (freeze_fpTs_call kk fpT) 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

197 
(flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts)) 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

198 
and freeze_fpTs_call kk fpT calls (T as Type (s, _)) = 
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:
54284
diff
changeset

199 
(case map_partition (try (snd o dest_map no_defs_lthy s)) calls of 
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:
54284
diff
changeset

200 
([], _) => 
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:
54284
diff
changeset

201 
(case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

202 
([], _) => freeze_fpTs_mutual_call kk fpT calls T 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

203 
 callsp => freeze_fpTs_map kk fpT callsp T) 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

204 
 callsp => freeze_fpTs_map kk fpT callsp T) 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

205 
 freeze_fpTs_call _ _ _ T = T; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

206 

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:
54284
diff
changeset

207 
val ctr_Tsss = map (map binder_types) ctr_Tss; 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58577
diff
changeset

208 
val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; 
55966  209 
val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

210 

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:
54284
diff
changeset

211 
val ns = map length ctr_Tsss; 
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:
54284
diff
changeset

212 
val kss = map (fn n => 1 upto n) ns; 
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:
54284
diff
changeset

213 
val mss = map (map length) ctr_Tsss; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

214 

58236  215 
val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs; 
216 
val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs; 

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:
54284
diff
changeset

217 
in 
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:
54284
diff
changeset

218 
(case n2m_sugar_of no_defs_lthy key of 
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:
54284
diff
changeset

219 
SOME n2m_sugar => (n2m_sugar, no_defs_lthy) 
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:
54284
diff
changeset

220 
 NONE => 
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:
54284
diff
changeset

221 
let 
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:
54284
diff
changeset

222 
val base_fp_names = Name.variant_list [] fp_b_names; 
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:
54284
diff
changeset

223 
val fp_bs = map2 (fn b_name => fn base_fp_name => 
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:
54284
diff
changeset

224 
Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name))) 
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:
54284
diff
changeset

225 
b_names base_fp_names; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

226 

55702
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

227 
val Type (s, Us) :: _ = fpTs; 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

228 
val killed_As' = 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

229 
(case bnf_of no_defs_lthy s of 
58236  230 
NONE => unsorted_As' 
55702
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

231 
 SOME bnf => 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

232 
let 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

233 
val Type (_, Ts) = T_of_bnf bnf; 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

234 
val deads = deads_of_bnf bnf; 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

235 
val dead_Us = 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

236 
map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us); 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

237 
in fold Term.add_tfreesT dead_Us [] end); 
63c80031d8dd
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents:
55701
diff
changeset

238 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

239 
val fp_absT_infos = map #absT_info fp_sugars0; 
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

240 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

241 
val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

242 
dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = 
58340  243 
fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs 
244 
unsorted_As' killed_As' fp_eqs no_defs_lthy; 

55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

245 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

246 
val fp_abs_inverses = map #abs_inverse fp_absT_infos; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

247 
val fp_type_definitions = map #type_definition fp_absT_infos; 
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fpoperations
traytel
parents:
55772
diff
changeset

248 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

249 
val abss = map #abs absT_infos; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

250 
val reps = map #rep absT_infos; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

251 
val absTs = map #absT absT_infos; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

252 
val repTs = map #repT absT_infos; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

253 
val abs_inverses = map #abs_inverse absT_infos; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

254 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

255 
val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

256 
val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

257 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

258 
val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

259 
mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; 
54256  260 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

261 
fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

262 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

263 
val ((co_recs, co_rec_defs), lthy) = 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58577
diff
changeset

264 
@{fold_map 2} (fn b => 
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

265 
if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

266 
else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

267 
fp_bs xtor_co_recs lthy 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

268 
>> split_list; 
58131
1abeda3c3bc2
drop hopeless feature  unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58117
diff
changeset

269 

58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

270 
val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss), 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

271 
fp_sugar_thms) = 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

272 
if fp = Least_FP then 
58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

273 
derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct 
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

274 
xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

275 
fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

276 
lthy 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

277 
> `(fn ((inducts, induct, _), (rec_thmss, _)) => 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

278 
([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

279 
> (fn info => (SOME info, NONE)) 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

280 
else 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

281 
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

282 
xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

283 
ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

284 
(fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

285 
(Proof_Context.export lthy no_defs_lthy) lthy 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

286 
> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _, 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

287 
(corec_sel_thmsss, _)) => 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

288 
(map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

289 
corec_disc_thmss, corec_sel_thmsss)) 
c1f3fa32d322
extended 'datatype_compat' to generate the expected, oldstyle recursor in the presence of recursion through functions
blanchet
parents:
58180
diff
changeset

290 
> (fn info => (NONE, SOME info)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

291 

58280
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

292 
val phi = Proof_Context.export_morphism names_lthy no_defs_lthy; 
54256  293 

56648
2ffa440b3074
manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents:
56641
diff
changeset

294 
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec 
58462  295 
co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss 
58676  296 
({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...}, 
58672
3f0d612ebd8e
preserve the structure of 'map_sel' theorem in ML
desharna
parents:
58671
diff
changeset

297 
fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, 
58673
add1a78da098
preserve the structure of 'set_intros' theorem in ML
desharna
parents:
58672
diff
changeset

298 
rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, 
58574  299 
fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, 
58734  300 
co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, 
58732  301 
set_inducts, ...}, 
58568  302 
...} : fp_sugar) = 
58117
9608028d8f43
more compatibility between old and newstyle datatypes
blanchet
parents:
58115
diff
changeset

303 
{T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, 
58674  304 
pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info, 
305 
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, 

58460  306 
fp_ctr_sugar = 
307 
{ctrXs_Tss = ctrXs_Tss, 

308 
ctr_defs = ctr_defs, 

58569  309 
ctr_sugar = ctr_sugar, 
58570  310 
ctr_transfers = ctr_transfers, 
58571  311 
case_transfers = case_transfers, 
58676  312 
disc_transfers = disc_transfers, 
313 
sel_transfers = sel_transfers}, 

58459  314 
fp_bnf_sugar = 
58462  315 
{map_thms = map_thms, 
58560  316 
map_disc_iffs = map_disc_iffs, 
58672
3f0d612ebd8e
preserve the structure of 'map_sel' theorem in ML
desharna
parents:
58671
diff
changeset

317 
map_selss = map_selss, 
58462  318 
rel_injects = rel_injects, 
58562  319 
rel_distincts = rel_distincts, 
58563  320 
rel_sels = rel_sels, 
58564  321 
rel_intros = rel_intros, 
58565  322 
rel_cases = rel_cases, 
58566  323 
set_thms = set_thms, 
58671
4cc24f1e52d5
preserve the structure of 'set_sel' theorem in ML
desharna
parents:
58634
diff
changeset

324 
set_selssss = set_selssss, 
58673
add1a78da098
preserve the structure of 'set_intros' theorem in ML
desharna
parents:
58672
diff
changeset

325 
set_introssss = set_introssss, 
58568  326 
set_cases = set_cases}, 
58459  327 
fp_co_induct_sugar = 
58461  328 
{co_rec = co_rec, 
329 
common_co_inducts = common_co_inducts, 

330 
co_inducts = co_inducts, 

58674  331 
co_rec_def = co_rec_def, 
58459  332 
co_rec_thms = co_rec_thms, 
333 
co_rec_discs = co_rec_disc_thms, 

58572  334 
co_rec_disc_iffs = co_rec_disc_iffs, 
58573  335 
co_rec_selss = co_rec_sel_thmss, 
336 
co_rec_codes = co_rec_codes, 

58574  337 
co_rec_transfers = co_rec_transfers, 
58734  338 
co_rec_o_maps = co_rec_o_maps, 
58575  339 
common_rel_co_inducts = common_rel_co_inducts, 
58576  340 
rel_co_inducts = rel_co_inducts, 
58577  341 
common_set_inducts = common_set_inducts, 
342 
set_inducts = set_inducts}} 

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:
54284
diff
changeset

343 
> morph_fp_sugar phi; 
54256  344 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset

345 
val target_fp_sugars = 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58577
diff
changeset

346 
@{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss 
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58577
diff
changeset

347 
ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss 
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58577
diff
changeset

348 
co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0; 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset

349 

0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset

350 
val n2m_sugar = (target_fp_sugars, fp_sugar_thms); 
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:
54284
diff
changeset

351 
in 
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:
54284
diff
changeset

352 
(n2m_sugar, lthy > register_n2m_sugar key n2m_sugar) 
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:
54284
diff
changeset

353 
end) 
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:
54284
diff
changeset

354 
end; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

355 

55543  356 
fun indexify_callsss ctrs callsss = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

357 
let 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

358 
fun indexify_ctr ctr = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

359 
(case AList.lookup Term.aconv_untyped callsss ctr of 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

360 
NONE => replicate (num_binder_types (fastype_of ctr)) [] 
55343  361 
 SOME callss => map (map (Envir.beta_eta_contract o unfold_lets_splits)) callss); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

362 
in 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

363 
map indexify_ctr ctrs 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

364 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

365 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

366 
fun retypargs tyargs (Type (s, _)) = Type (s, tyargs); 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

367 

6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

368 
fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) = 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

369 
f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I) 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

370 
 fold_subtype_pairs f TU = f TU; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

371 

55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

372 
val impossible_caller = Bound ~1; 
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

373 

58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

374 
fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy = 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

375 
let 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

376 
val qsoty = quote o Syntax.string_of_typ lthy; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

377 
val qsotys = space_implode " or " o map qsoty; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

378 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

379 
fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype"); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

380 
fun not_co_datatype (T as Type (s, _)) = 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

381 
if fp = Least_FP andalso 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57983
diff
changeset

382 
is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then 
58315  383 
error (qsoty T ^ " is an oldstyle datatype") 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

384 
else 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

385 
not_co_datatype0 T 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

386 
 not_co_datatype T = not_co_datatype0 T; 
54303
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hardtosolve issues outside the N2M code
blanchet
parents:
54302
diff
changeset

387 
fun not_mutually_nested_rec Ts1 Ts2 = 
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hardtosolve issues outside the N2M code
blanchet
parents:
54302
diff
changeset

388 
error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^ 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

389 
" nor nested recursive through " ^ 
58117
9608028d8f43
more compatibility between old and newstyle datatypes
blanchet
parents:
58115
diff
changeset

390 
(if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2)); 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

391 

55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

392 
val sorted_actual_Ts = 
54266
4e0738356ac9
stronger normalization, to increase n2m cache effectiveness
blanchet
parents:
54265
diff
changeset

393 
sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

394 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

395 
fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s))); 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

396 

54282  397 
fun the_fp_sugar_of (T as Type (T_name, _)) = 
398 
(case fp_sugar_of lthy T_name of 

399 
SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T 

400 
 NONE => not_co_datatype T); 

401 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

402 
fun gen_rhss_in gen_Ts rho subTs = 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

403 
let 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

404 
fun maybe_insert (T, Type (_, gen_tyargs)) = 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

405 
if member (op =) subTs T then insert (op =) gen_tyargs else I 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

406 
 maybe_insert _ = I; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

407 

6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

408 
val ctrs = maps the_ctrs_of gen_Ts; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

409 
val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

410 
val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

411 
in 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

412 
fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) [] 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

413 
end; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

414 

56485  415 
fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen) 
416 
 gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) = 

54282  417 
let 
58234  418 
val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T; 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

419 
val mutual_Ts = map (retypargs tyargs) mutual_Ts0; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

420 

56485  421 
val rev_seen = flat rev_seens; 
422 
val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse 

423 
not_mutually_nested_rec mutual_Ts rev_seen; 

54303
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hardtosolve issues outside the N2M code
blanchet
parents:
54302
diff
changeset

424 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

425 
fun fresh_tyargs () = 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

426 
let 
58234  427 
val (unsorted_gen_tyargs, lthy') = 
58280
2ec3e2de34c3
more canonical (and correct) local theory threading
blanchet
parents:
58236
diff
changeset

428 
variant_tfrees (replicate (length tyargs) "z") lthy 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

429 
>> map Logic.varifyT_global; 
58234  430 
val gen_tyargs = 
431 
map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) tyargs0 unsorted_gen_tyargs; 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

432 
val rho' = (gen_tyargs ~~ tyargs) @ rho; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

433 
in 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

434 
(rho', gen_tyargs, gen_seen, lthy') 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

435 
end; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

436 

6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

437 
val (rho', gen_tyargs, gen_seen', lthy') = 
56485  438 
if exists (exists_subtype_in rev_seen) mutual_Ts then 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

439 
(case gen_rhss_in gen_seen rho mutual_Ts of 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

440 
[] => fresh_tyargs () 
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54740
diff
changeset

441 
 gen_tyargs :: gen_tyargss_tl => 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

442 
let 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

443 
val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl); 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

444 
val mgu = Type.raw_unifys unify_pairs Vartab.empty; 
58948
f6ecc0fb2066
proper Envir.norm_type for result of Type.raw_unifys;
wenzelm
parents:
58734
diff
changeset

445 
val gen_tyargs' = map (Envir.norm_type mgu) gen_tyargs; 
f6ecc0fb2066
proper Envir.norm_type for result of Type.raw_unifys;
wenzelm
parents:
58734
diff
changeset

446 
val gen_seen' = map (Envir.norm_type mgu) gen_seen; 
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

447 
in 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

448 
(rho, gen_tyargs', gen_seen', lthy) 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

449 
end) 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

450 
else 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

451 
fresh_tyargs (); 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

452 

6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

453 
val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0; 
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

454 
val other_mutual_Ts = remove1 (op =) T mutual_Ts; 
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset

455 
val Ts' = fold (remove1 (op =)) other_mutual_Ts Ts; 
54282  456 
in 
56485  457 
gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts' 
54282  458 
end 
56485  459 
 gather_types _ _ _ _ (T :: _) = not_co_datatype T; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

460 

56485  461 
val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts; 
58340  462 
val (perm_mutual_cliques, perm_Ts) = 
56485  463 
split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss)); 
464 

54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

465 
val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts; 
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset

466 

56484  467 
val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

468 
val Ts = actual_Ts @ missing_Ts; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

469 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

470 
val nn = length Ts; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

471 
val kks = 0 upto nn  1; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

472 

54267  473 
val callssss0 = pad_list [] nn actual_callssss0; 
474 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

475 
val common_name = mk_common_name (map Binding.name_of actual_bs); 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

476 
val bs = pad_list (Binding.name common_name) nn actual_bs; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

477 
val callers = pad_list impossible_caller nn actual_callers; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

478 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

479 
fun permute xs = permute_like (op =) Ts perm_Ts xs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

480 
fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

481 

58340  482 
(* The assignment of callers to mutual cliques is incorrect in general. This code would need to 
483 
inspect the actual calls to discover the correct cliques in the presence of type duplicates. 

484 
However, the naive scheme implemented here supports "prim(co)rec" specifications following 

485 
reasonable ordering of the duplicates (e.g., keeping the cliques together). *) 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

486 
val perm_bs = permute bs; 
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55702
diff
changeset

487 
val perm_callers = permute callers; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

488 
val perm_kks = permute kks; 
54267  489 
val perm_callssss0 = permute callssss0; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

490 
val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

491 

58460  492 
val perm_callssss = 
493 
map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0; 

53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

494 

53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

495 
val ((perm_fp_sugars, fp_sugar_thms), lthy) = 
58117
9608028d8f43
more compatibility between old and newstyle datatypes
blanchet
parents:
58115
diff
changeset

496 
if length perm_Tss = 1 then 
56485  497 
((perm_fp_sugars0, (NONE, NONE)), lthy) 
498 
else 

58340  499 
mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers 
58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset

500 
perm_callssss perm_fp_sugars0 lthy; 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

501 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

502 
val fp_sugars = unpermute perm_fp_sugars; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

503 
in 
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset

504 
((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) 
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

505 
end; 
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

506 

ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket corec repository
blanchet
parents:
diff
changeset

507 
end; 