16 ML {* open Nominal_Dt_Alpha *} |
16 ML {* open Nominal_Dt_Alpha *} |
17 |
17 |
18 use "nominal_dt_quot.ML" |
18 use "nominal_dt_quot.ML" |
19 ML {* open Nominal_Dt_Quot *} |
19 ML {* open Nominal_Dt_Quot *} |
20 |
20 |
21 |
|
22 |
|
23 (*****************************************) |
21 (*****************************************) |
24 (* setup for induction principles method *) |
22 (* setup for induction principles method *) |
25 use "nominal_induct.ML" |
23 use "nominal_induct.ML" |
26 method_setup nominal_induct = |
24 method_setup nominal_induct = |
27 {* NominalInduct.nominal_induct_method *} |
25 {* NominalInduct.nominal_induct_method *} |
73 fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) |
71 fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) |
74 | replace_typ ty_ss T = T |
72 | replace_typ ty_ss T = T |
75 |
73 |
76 fun raw_dts ty_ss dts = |
74 fun raw_dts ty_ss dts = |
77 let |
75 let |
78 fun raw_dts_aux1 (bind, tys, mx) = |
76 fun raw_dts_aux1 (bind, tys, _) = |
79 (raw_bind bind, map (replace_typ ty_ss) tys, mx) |
77 (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn) |
80 |
78 |
81 fun raw_dts_aux2 (ty_args, bind, mx, constrs) = |
79 fun raw_dts_aux2 (ty_args, bind, _, constrs) = |
82 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
80 (ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs) |
83 in |
81 in |
84 map raw_dts_aux2 dts |
82 map raw_dts_aux2 dts |
85 end |
83 end |
86 |
84 |
87 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
85 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
103 *} |
101 *} |
104 |
102 |
105 ML {* |
103 ML {* |
106 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
104 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
107 let |
105 let |
108 val bn_funs' = map (fn (bn, ty, mx) => |
106 val bn_funs' = map (fn (bn, ty, _) => |
109 (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs |
107 (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs |
110 |
108 |
111 val bn_eqs' = map (fn (attr, trm) => |
109 val bn_eqs' = map (fn (attr, trm) => |
112 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
110 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
113 in |
111 in |
114 (bn_funs', bn_eqs') |
112 (bn_funs', bn_eqs') |
153 (bn_fun_strs ~~ bn_fun_strs') |
151 (bn_fun_strs ~~ bn_fun_strs') |
154 |
152 |
155 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
153 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
156 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
154 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
157 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
155 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
|
156 |
|
157 val _ = tracing ("raw_dt info:\n" ^ @{make_string} raw_dts) |
158 |
158 |
159 val (raw_dt_full_names, thy1) = |
159 val (raw_dt_full_names, thy1) = |
160 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy |
160 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy |
161 |
161 |
162 val lthy1 = Named_Target.theory_init thy1 |
162 val lthy1 = Named_Target.theory_init thy1 |