author | blanchet |
Wed, 19 Feb 2014 08:34:33 +0100 | |
changeset 55575 | a5e33e18fb5c |
parent 55567 | 260e18aa306f |
child 55701 | 38f75365fc2a |
permissions | -rw-r--r-- |
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 co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec 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 co-rec repository
blanchet
parents:
diff
changeset
|
6 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
signature BNF_FP_N2M_SUGAR = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
55343 | 10 |
val unfold_lets_splits: term -> term |
54243 | 11 |
val dest_map: Proof.context -> string -> term -> term * term list |
12 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55567
diff
changeset
|
13 |
val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> |
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
|
14 |
term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory -> |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
15 |
(BNF_FP_Def_Sugar.fp_sugar list |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
16 |
* (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
|
17 |
* local_theory |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55567
diff
changeset
|
18 |
val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> |
54009 | 19 |
(term * term list list) list list -> local_theory -> |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
20 |
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
21 |
* (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
|
22 |
* local_theory |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
|
54006 | 28 |
open Ctr_Sugar |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
open BNF_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
open BNF_Def |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
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
|
33 |
open BNF_FP_N2M |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
val n2mN = "n2m_" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
|
54256 | 37 |
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option); |
38 |
||
39 |
structure Data = Generic_Data |
|
40 |
( |
|
41 |
type T = n2m_sugar Typtab.table; |
|
42 |
val empty = Typtab.empty; |
|
43 |
val extend = I; |
|
55394
d5ebe055b599
more liberal merging of BNFs and constructor sugar
blanchet
parents:
55343
diff
changeset
|
44 |
fun merge data : T = Typtab.merge (K true) data; |
54256 | 45 |
); |
46 |
||
47 |
fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) = |
|
48 |
(map (morph_fp_sugar phi) fp_sugars, |
|
49 |
(Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt, |
|
50 |
Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt)); |
|
51 |
||
52 |
val transfer_n2m_sugar = |
|
54740 | 53 |
morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; |
54256 | 54 |
|
55 |
fun n2m_sugar_of ctxt = |
|
56 |
Typtab.lookup (Data.get (Context.Proof ctxt)) |
|
57 |
#> Option.map (transfer_n2m_sugar ctxt); |
|
58 |
||
59 |
fun register_n2m_sugar key n2m_sugar = |
|
60 |
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
|
61 |
(fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar))); |
54256 | 62 |
|
55343 | 63 |
fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) = |
64 |
unfold_lets_splits (betapply (arg2, arg1)) |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55409
diff
changeset
|
65 |
| unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) = |
55343 | 66 |
(case unfold_lets_splits u of |
55336 | 67 |
u' as Abs (s1, T1, Abs (s2, T2, _)) => |
68 |
let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in |
|
69 |
lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) |
|
54243 | 70 |
end |
71 |
| _ => t) |
|
55343 | 72 |
| unfold_lets_splits (t $ u) = betapply (pairself unfold_lets_splits (t, u)) |
73 |
| unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t) |
|
74 |
| unfold_lets_splits t = t; |
|
54243 | 75 |
|
76 |
fun mk_map_pattern ctxt s = |
|
77 |
let |
|
78 |
val bnf = the (bnf_of ctxt s); |
|
79 |
val mapx = map_of_bnf bnf; |
|
80 |
val live = live_of_bnf bnf; |
|
81 |
val (f_Ts, _) = strip_typeN live (fastype_of mapx); |
|
54265
3e1d230f1c00
make local theory operations non-pervasive (makes more intuitive sense)
blanchet
parents:
54256
diff
changeset
|
82 |
val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts; |
54243 | 83 |
in |
84 |
(mapx, betapplys (mapx, fs)) |
|
85 |
end; |
|
86 |
||
87 |
fun dest_map ctxt s call = |
|
88 |
let |
|
89 |
val (map0, pat) = mk_map_pattern ctxt s; |
|
90 |
val (_, tenv) = fo_match ctxt call pat; |
|
91 |
in |
|
92 |
(map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv []) |
|
93 |
end; |
|
94 |
||
54276 | 95 |
fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t]) |
96 |
| dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1; |
|
54239 | 97 |
|
54245 | 98 |
fun map_partition f xs = |
99 |
fold_rev (fn x => fn (ys, (good, bad)) => |
|
100 |
case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad))) |
|
101 |
xs ([], ([], [])); |
|
102 |
||
54256 | 103 |
fun key_of_fp_eqs fp fpTs fp_eqs = |
54267 | 104 |
Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs); |
54256 | 105 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
106 |
(* TODO: test with sort constraints on 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
|
107 |
fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 = |
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
|
108 |
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
|
109 |
val thy = Proof_Context.theory_of no_defs_lthy0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
110 |
|
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
|
111 |
val qsotm = quote o Syntax.string_of_term no_defs_lthy0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
112 |
|
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
|
113 |
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
|
114 |
error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts)); |
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
115 |
fun nested_self_call t = |
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
116 |
error ("Unsupported nested self-call " ^ qsotm t); |
54245 | 117 |
|
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
|
118 |
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
|
119 |
val fp_b_names = map base_name_of_typ fpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
120 |
|
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 |
val nn = length fpTs; |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
122 |
val kks = 0 upto nn - 1; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
123 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
124 |
fun target_ctr_sugar_of_fp_sugar fpT ({T, 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
|
125 |
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
|
126 |
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; |
54740 | 127 |
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
|
128 |
in |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
129 |
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
|
130 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
131 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
132 |
val ctr_defss = map #ctr_defs fp_sugars0; |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
133 |
val mapss = map #maps fp_sugars0; |
54302 | 134 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
135 |
|
54302 | 136 |
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
|
137 |
val ctr_Tss = map (map fastype_of) ctrss; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
138 |
|
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
|
139 |
val As' = fold (fold Term.add_tfreesT) ctr_Tss []; |
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 |
val As = map TFree As'; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
141 |
|
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
|
142 |
val ((Cs, Xs), 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
|
143 |
no_defs_lthy0 |
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
|
144 |
|> 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
|
145 |
|> 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
|
146 |
||>> variant_tfrees fp_b_names; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
147 |
|
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
|
148 |
fun check_call_dead live_call call = |
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
|
149 |
if null (get_indices call) then () else incompatible_calls [live_call, call]; |
54245 | 150 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
151 |
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
|
152 |
(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
|
153 |
[(kk, _)] => nth Xs kk |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
154 |
| _ => 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
|
155 |
| 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
|
156 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
157 |
fun freeze_fpTs_mutual_call calls T = |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
158 |
(case fold (union (op =)) (map get_indices calls) [] of |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
159 |
[] => freeze_fpTs_type_based_default T |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
160 |
| [kk] => nth Xs kk |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
161 |
| _ => incompatible_calls calls); |
54253 | 162 |
|
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
163 |
fun freeze_fpTs_map (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
|
164 |
(Type (s, Ts)) = |
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
165 |
if Ts' = Ts then |
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
166 |
nested_self_call live_call |
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
167 |
else |
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
168 |
(List.app (check_call_dead 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
|
169 |
Type (s, map2 (freeze_fpTs_call fpT) |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
170 |
(flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts)) |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
171 |
and freeze_fpTs_call 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
|
172 |
(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
|
173 |
([], _) => |
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
|
174 |
(case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of |
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
175 |
([], _) => freeze_fpTs_mutual_call calls T |
54301
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
176 |
| callsp => freeze_fpTs_map fpT callsp T) |
e0943a2ee400
added check to avoid odd situations the N2M code cannot handle
blanchet
parents:
54300
diff
changeset
|
177 |
| callsp => freeze_fpTs_map fpT callsp T) |
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
178 |
| freeze_fpTs_call _ _ T = T; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
179 |
|
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
|
180 |
val ctr_Tsss = map (map binder_types) ctr_Tss; |
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
181 |
val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs_call) fpTs callssss ctr_Tsss; |
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
|
182 |
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
183 |
|
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
|
184 |
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
|
185 |
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
|
186 |
val mss = map (map length) ctr_Tsss; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
187 |
|
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
|
188 |
val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts; |
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
|
189 |
val key = key_of_fp_eqs fp fpTs fp_eqs; |
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
|
190 |
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
|
191 |
(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
|
192 |
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
|
193 |
| 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
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
b_names base_fp_names; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
199 |
|
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
|
200 |
val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_injects, |
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 |
dtor_ctors, xtor_co_iter_thmss, ...}, 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
|
202 |
fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
203 |
|
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
|
204 |
val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss 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
|
205 |
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec 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 ((xtor_co_iterss, iters_args_types, coiters_args_types), _) = |
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
|
208 |
mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy; |
54256 | 209 |
|
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
|
210 |
fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
211 |
|
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
|
212 |
val ((co_iterss, co_iter_defss), 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
|
213 |
fold_map2 (fn b => |
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
|
214 |
(if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types) |
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
|
215 |
else define_coiters [unfoldN, corecN] (the coiters_args_types)) |
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
|
216 |
(mk_binding b) fpTs Cs) fp_bs xtor_co_iterss 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
|
217 |
|>> split_list; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
218 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
219 |
val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, |
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55394
diff
changeset
|
220 |
disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), 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
|
221 |
if fp = Least_FP then |
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 |
derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct |
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 |
xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss |
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 |
co_iterss co_iter_defss lthy |
55409
b74248961819
made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet
parents:
55394
diff
changeset
|
225 |
|> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) => |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
226 |
([induct], [inducts], fold_thmss, rec_thmss, replicate nn [], |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
227 |
replicate nn [], replicate nn [], replicate nn [])) |
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
|
228 |
||> (fn info => (SOME info, 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
|
229 |
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:
54284
diff
changeset
|
230 |
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct |
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
|
231 |
dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss |
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
|
232 |
ns ctr_defss ctr_sugars co_iterss co_iter_defss |
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
|
233 |
(Proof_Context.export lthy no_defs_lthy) 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
|
234 |
|> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), |
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
|
235 |
(disc_unfold_thmss, disc_corec_thmss, _), _, |
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
|
236 |
(sel_unfold_thmsss, sel_corec_thmsss, _)) => |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
237 |
(map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
238 |
corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
239 |
sel_corec_thmsss)) |
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
|
240 |
||> (fn info => (NONE, SOME info)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
241 |
|
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
|
242 |
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; |
54256 | 243 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
244 |
fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
245 |
co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss = |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
246 |
{T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
247 |
nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
248 |
ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
249 |
common_co_inducts = common_co_inducts, co_inducts = co_inducts, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
250 |
co_iter_thmss = [un_fold_thms, co_rec_thms], |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
251 |
disc_co_iterss = [disc_unfold_thms, disc_corec_thms], |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
252 |
sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]} |
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
|
253 |
|> morph_fp_sugar phi; |
54256 | 254 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
255 |
val target_fp_sugars = |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
256 |
map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
257 |
(transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
258 |
sel_unfold_thmsss sel_corec_thmsss; |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
259 |
|
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55486
diff
changeset
|
260 |
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
|
261 |
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
|
262 |
(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
|
263 |
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
|
264 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
265 |
|
55567 | 266 |
fun indexify_callsss ctrs callsss = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
267 |
let |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
268 |
fun indexify_ctr ctr = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
269 |
(case AList.lookup Term.aconv_untyped callsss ctr of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
270 |
NONE => replicate (num_binder_types (fastype_of ctr)) [] |
55343 | 271 |
| 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 co-rec repository
blanchet
parents:
diff
changeset
|
272 |
in |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
273 |
map indexify_ctr ctrs |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
274 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
275 |
|
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
276 |
fun retypargs tyargs (Type (s, _)) = Type (s, tyargs); |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
277 |
|
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
278 |
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
|
279 |
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
|
280 |
| fold_subtype_pairs f TU = f TU; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
281 |
|
54009 | 282 |
fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
283 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
284 |
val qsoty = quote o Syntax.string_of_typ lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
285 |
val qsotys = space_implode " or " o map qsoty; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
286 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
287 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
288 |
fun not_co_datatype (T as Type (s, _)) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
289 |
if fp = Least_FP andalso |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
290 |
is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
291 |
error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")") |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
292 |
else |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
293 |
not_co_datatype0 T |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
294 |
| not_co_datatype T = not_co_datatype0 T; |
54303
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents:
54302
diff
changeset
|
295 |
fun not_mutually_nested_rec Ts1 Ts2 = |
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents:
54302
diff
changeset
|
296 |
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
|
297 |
" nor nested recursive through " ^ |
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
298 |
(if Ts1 = Ts2 andalso can the_single Ts1 then "itself" else qsotys Ts2)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
299 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
300 |
val sorted_actual_Ts = |
54266
4e0738356ac9
stronger normalization, to increase n2m cache effectiveness
blanchet
parents:
54265
diff
changeset
|
301 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
302 |
|
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
303 |
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
|
304 |
|
54282 | 305 |
fun the_fp_sugar_of (T as Type (T_name, _)) = |
306 |
(case fp_sugar_of lthy T_name of |
|
307 |
SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T |
|
308 |
| NONE => not_co_datatype T); |
|
309 |
||
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
310 |
fun gen_rhss_in gen_Ts rho subTs = |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
311 |
let |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
312 |
fun maybe_insert (T, Type (_, gen_tyargs)) = |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
313 |
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
|
314 |
| maybe_insert _ = I; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
315 |
|
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
316 |
val ctrs = maps the_ctrs_of gen_Ts; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
317 |
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
|
318 |
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
|
319 |
in |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
320 |
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
|
321 |
end; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
322 |
|
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
|
323 |
fun gather_types _ _ num_groups seen gen_seen [] = (num_groups, seen, gen_seen) |
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
|
324 |
| gather_types lthy rho num_groups seen gen_seen ((T as Type (_, tyargs)) :: Ts) = |
54282 | 325 |
let |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
326 |
val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
327 |
val mutual_Ts = map (retypargs tyargs) mutual_Ts0; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
328 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
329 |
val _ = seen = [] orelse exists (exists_strict_subtype_in seen) mutual_Ts orelse |
54303
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents:
54302
diff
changeset
|
330 |
not_mutually_nested_rec mutual_Ts seen; |
4f55054d197c
reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents:
54302
diff
changeset
|
331 |
|
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
332 |
fun fresh_tyargs () = |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
333 |
let |
55567 | 334 |
(* The name "'zy" is unlikely to clash with the context, yielding more cache hits. *) |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
335 |
val (gen_tyargs, lthy') = |
55567 | 336 |
variant_tfrees (replicate (length tyargs) "zy") lthy |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
337 |
|>> map Logic.varifyT_global; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
338 |
val rho' = (gen_tyargs ~~ tyargs) @ rho; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
339 |
in |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
340 |
(rho', gen_tyargs, gen_seen, lthy') |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
341 |
end; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
342 |
|
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
343 |
val (rho', gen_tyargs, gen_seen', lthy') = |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
344 |
if exists (exists_subtype_in seen) mutual_Ts then |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
345 |
(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
|
346 |
[] => fresh_tyargs () |
54899
7a01387c47d5
added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents:
54740
diff
changeset
|
347 |
| gen_tyargs :: gen_tyargss_tl => |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
348 |
let |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
349 |
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
|
350 |
val mgu = Type.raw_unifys unify_pairs Vartab.empty; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
351 |
val gen_tyargs' = map (Envir.subst_type mgu) gen_tyargs; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
352 |
val gen_seen' = map (Envir.subst_type mgu) gen_seen; |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
353 |
in |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
354 |
(rho, gen_tyargs', gen_seen', lthy) |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
355 |
end) |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
356 |
else |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
357 |
fresh_tyargs (); |
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
358 |
|
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
359 |
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
|
360 |
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
|
361 |
val Ts' = fold (remove1 (op =)) other_mutual_Ts Ts; |
54282 | 362 |
in |
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
|
363 |
gather_types lthy' rho' (num_groups + 1) (seen @ mutual_Ts) (gen_seen' @ gen_mutual_Ts) |
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
|
364 |
Ts' |
54282 | 365 |
end |
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
|
366 |
| gather_types _ _ _ _ _ (T :: _) = not_co_datatype T; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
367 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
368 |
val (num_groups, perm_Ts, perm_gen_Ts) = gather_types lthy [] 0 [] [] sorted_actual_Ts; |
54283
6f0a49ed1bb1
fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents:
54282
diff
changeset
|
369 |
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
|
370 |
|
55480
59cc4a8bc28a
allow different functions to recurse on the same type, like in the old package
blanchet
parents:
55479
diff
changeset
|
371 |
val missing_Ts = subtract (op =) actual_Ts perm_Ts; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
372 |
val Ts = actual_Ts @ missing_Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
373 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
374 |
val nn = length Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
375 |
val kks = 0 upto nn - 1; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
376 |
|
54267 | 377 |
val callssss0 = pad_list [] nn actual_callssss0; |
378 |
||
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
379 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
380 |
val bs = pad_list (Binding.name common_name) nn actual_bs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
381 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
382 |
fun permute xs = permute_like (op =) Ts perm_Ts xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
383 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
384 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
385 |
val perm_bs = permute bs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
386 |
val perm_kks = permute kks; |
54267 | 387 |
val perm_callssss0 = permute callssss0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
388 |
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 co-rec repository
blanchet
parents:
diff
changeset
|
389 |
|
55567 | 390 |
val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
391 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
392 |
val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
393 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
394 |
val ((perm_fp_sugars, fp_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:
54284
diff
changeset
|
395 |
if num_groups > 1 then |
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
|
396 |
mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss |
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
|
397 |
perm_fp_sugars0 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
|
398 |
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:
54284
diff
changeset
|
399 |
((perm_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
|
400 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
401 |
val fp_sugars = unpermute perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
402 |
in |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53678
diff
changeset
|
403 |
((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
404 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
405 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
406 |
end; |