author | blanchet |
Tue, 08 Apr 2014 13:47:27 +0200 | |
changeset 56452 | 0c98c9118407 |
parent 56002 | 2028467b4df4 |
child 56453 | 00548d372f02 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_compat.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
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 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
5 |
Compatibility layer with the old datatype package ("datatype_compat"). |
53303
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_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
10 |
val datatype_compat_cmd : string list -> local_theory -> local_theory |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
11 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
12 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
13 |
structure BNF_LFP_Compat : BNF_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
14 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
|
54006 | 16 |
open Ctr_Sugar |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
17 |
open BNF_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
19 |
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
|
20 |
open BNF_FP_N2M_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
val compatN = "compat_"; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
|
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
24 |
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
25 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *) |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
27 |
fun datatype_compat_cmd raw_fpT_names lthy = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
val thy = Proof_Context.theory_of lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
fun not_datatype s = error (quote s ^ " is not a new-style datatype"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
fun not_mutually_recursive ss = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
35 |
val fpT_names = |
56002 | 36 |
map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy) |
55951
c07d184aebe9
tuned signature -- more uniform check_type_name/read_type_name;
wenzelm
parents:
55863
diff
changeset
|
37 |
raw_fpT_names; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
38 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
fun lfp_sugar_of s = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
(case fp_sugar_of lthy s of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
| _ => not_datatype s); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
44 |
val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names; |
55485 | 45 |
val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
val fpT_names' = map (fst o dest_Type) fpTs0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
48 |
val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
|
56452
0c98c9118407
preserve user type variable names to avoid mismatches/confusion
blanchet
parents:
56002
diff
changeset
|
50 |
val (As_names, _) = lthy |> Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As); |
0c98c9118407
preserve user type variable names to avoid mismatches/confusion
blanchet
parents:
56002
diff
changeset
|
51 |
val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
52 |
val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
54 |
fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk = |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
55 |
(case try lfp_sugar_of s of |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
56 |
SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) => |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
57 |
let |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
58 |
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) []; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
59 |
val substT = Term.typ_subst_TVars rho; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
60 |
val mutual_Ts = map substT mutual_Ts0; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
61 |
val mutual_nn = length mutual_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:
55409
diff
changeset
|
62 |
val mutual_kks = kk upto kk + mutual_nn - 1; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
63 |
val mutual_Tkks = mutual_Ts ~~ mutual_kks; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
65 |
fun indices_of_ctr_arg parent_Tkks (U as Type (s, Us)) (accum as (Tparents_ksss, kk')) = |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
66 |
if s = @{type_name fun} then |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
67 |
if exists_subtype_in mutual_Ts U then |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
68 |
(warning "Incomplete support for recursion through functions -- \ |
55485 | 69 |
\the old 'primrec' will fail"; |
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
70 |
indices_of_ctr_arg parent_Tkks (range_type U) accum) |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
71 |
else |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
72 |
([], accum) |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
73 |
else |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
74 |
(case AList.lookup (op =) (parent_Tkks @ mutual_Tkks) U of |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
75 |
SOME kk => ([kk], accum) |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
76 |
| NONE => |
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
77 |
if exists (exists_strict_subtype_in mutual_Ts) Us then |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
78 |
error "Deeply nested recursion not supported" |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
79 |
else if exists (member (op =) mutual_Ts) Us then |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
80 |
([kk'], |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
81 |
nested_Tparentss_indicessss_of parent_Tkks U kk' |>> append Tparents_ksss) |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
82 |
else |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
83 |
([], accum)) |
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
84 |
| indices_of_ctr_arg _ _ accum = ([], accum); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
85 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
86 |
fun Tparents_indicesss_of_mutual_type T kk ctr_Tss = |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
87 |
let val parent_Tkks' = (T, kk) :: parent_Tkks in |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
88 |
fold_map (fold_map (indices_of_ctr_arg parent_Tkks')) ctr_Tss |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
89 |
#>> pair parent_Tkks' |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
90 |
end; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
91 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
92 |
val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts; |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
93 |
val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss; |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
94 |
in |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
95 |
([], kk + mutual_nn) |
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
96 |
|> fold_map3 Tparents_indicesss_of_mutual_type mutual_Ts mutual_kks ctr_Tsss |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
97 |
|> (fn (Tparentss_kkssss, (Tparentss_kkssss', kk)) => |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
98 |
(Tparentss_kkssss @ Tparentss_kkssss', kk)) |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
99 |
end |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
100 |
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^ |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
101 |
" not corresponding to new-style datatype (cf. \"datatype_new\")")); |
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
102 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
103 |
val (Tparentss_kkssss, _) = nested_Tparentss_indicessss_of [] fpT1 0; |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
104 |
val Tparentss = map fst Tparentss_kkssss; |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
105 |
val Ts = map (fst o hd) Tparentss; |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
106 |
val kkssss = map snd Tparentss_kkssss; |
55485 | 107 |
|
108 |
val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
109 |
val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0; |
55485 | 110 |
val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0; |
111 |
||
55481 | 112 |
val b_names = Name.variant_list [] (map base_name_of_typ Ts); |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
113 |
val compat_b_names = map (prefix compatN) b_names; |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
114 |
val compat_bs = map Binding.name compat_b_names; |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
115 |
val common_name = compatN ^ mk_common_name b_names; |
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
116 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
117 |
val nn_fp = length fpTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
118 |
val nn = length Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
119 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
120 |
val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
121 |
|
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
122 |
fun apply_comps n kk = |
55966 | 123 |
mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
124 |
|
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
125 |
val callssss = |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
126 |
map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks))) |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
127 |
kkssss ctr_Tsss0; |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
128 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
129 |
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
54286
22616f65d4ea
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents:
54267
diff
changeset
|
130 |
if nn > nn_fp then |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55571
diff
changeset
|
131 |
mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy |
54286
22616f65d4ea
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents:
54267
diff
changeset
|
132 |
else |
22616f65d4ea
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents:
54267
diff
changeset
|
133 |
((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
|
134 |
|
55540
892a425c5eaa
follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
blanchet
parents:
55539
diff
changeset
|
135 |
val {common_co_inducts = [induct], ...} :: _ = fp_sugars; |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
136 |
val inducts = map (the_single o #co_inducts) fp_sugars; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
137 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
138 |
fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
139 |
| mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts) |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
140 |
| mk_dtyp [kk] (Type (@{type_name fun}, [T, T'])) = |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
141 |
Datatype_Aux.DtType (@{type_name fun}, [mk_dtyp [] T, mk_dtyp [kk] T']) |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
142 |
| mk_dtyp [kk] T = if nth Ts kk = T then Datatype_Aux.DtRec kk else mk_dtyp [] T; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
143 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
144 |
fun mk_ctr_descr Ts kkss ctr0 = |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
145 |
mk_ctr Ts ctr0 |> (fn Const (s, T) => (s, map2 mk_dtyp kkss (binder_types T))); |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
146 |
fun mk_typ_descr kksss ((Type (T_name, Ts), kk) :: parents) ctrs0 = |
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
147 |
(kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
148 |
|
55486
8609527278f2
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
blanchet
parents:
55485
diff
changeset
|
149 |
val descr = map3 mk_typ_descr kkssss Tparentss ctrss0; |
55863 | 150 |
val recs = map (fst o dest_Const o #co_rec) fp_sugars; |
151 |
val rec_thms = maps #co_rec_thms fp_sugars; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
152 |
|
55567 | 153 |
fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, |
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
154 |
distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) = |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
155 |
(T_name0, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
156 |
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
157 |
inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
158 |
rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
159 |
case_cong = case_cong, weak_case_cong = weak_case_cong, split = split, |
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
160 |
split_asm = split_asm}); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
161 |
|
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55531
diff
changeset
|
162 |
val infos = map_index mk_info (take nn_fp fp_sugars); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
163 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
164 |
val all_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
165 |
(case lfp_sugar_thms of |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
166 |
NONE => [] |
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
167 |
| SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) => |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
168 |
let |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
169 |
val common_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
170 |
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
171 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
172 |
|> map (fn (thmN, thms, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
173 |
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
174 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
175 |
val notes = |
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
176 |
[(inductN, map single induct_thms, induct_attrs), |
55479
ece4910c3ea0
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents:
55409
diff
changeset
|
177 |
(recN, rec_thmss, code_nitpicksimp_simp_attrs)] |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
178 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
179 |
|> maps (fn (thmN, thmss, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
180 |
if forall null thmss then |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
181 |
[] |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
182 |
else |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
183 |
map2 (fn b_name => fn thms => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
184 |
((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])])) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
185 |
compat_b_names thmss); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
186 |
in |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
187 |
common_notes @ notes |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
188 |
end); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
189 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
190 |
val register_interpret = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
191 |
Datatype_Data.register infos |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
192 |
#> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
193 |
in |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
194 |
lthy |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
195 |
|> Local_Theory.raw_theory register_interpret |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
196 |
|> Local_Theory.notes all_notes |> snd |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
197 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
198 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
199 |
val _ = |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
200 |
Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
54025 | 201 |
"register new-style datatypes as old-style datatypes" |
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55486
diff
changeset
|
202 |
(Scan.repeat1 Parse.type_const >> datatype_compat_cmd); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
203 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
204 |
end; |