equal
deleted
inserted
replaced
95 ML {* |
95 ML {* |
96 fun print_constr (((name, anno_tys), bds), syn) = |
96 fun print_constr (((name, anno_tys), bds), syn) = |
97 (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ " " |
97 (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
|
100 *} |
|
101 |
|
102 ML Local_Theory.exit_global |
|
103 |
|
104 ML {* |
|
105 fun fv_constr prefix (((name, anno_tys), bds), syn) = |
|
106 prefix ^ " (" ^ (Binding.name_of name) ^ ") = " |
100 *} |
107 *} |
101 |
108 |
102 ML {* |
109 ML {* |
103 fun single_dt (((s2, s3), syn), constrs) = |
110 fun single_dt (((s2, s3), syn), constrs) = |
104 ["constructor declaration"] |
111 ["constructor declaration"] |
108 @ ["constructors: "] @ (map print_constr constrs) |
115 @ ["constructors: "] @ (map print_constr constrs) |
109 |> separate "\n" |
116 |> separate "\n" |
110 |> implode |
117 |> implode |
111 *} |
118 *} |
112 |
119 |
|
120 ML {* |
|
121 fun fv_dt (((s2, s3), syn), constrs) = |
|
122 map (fv_constr ("fv_" ^ Binding.name_of s3)) constrs |
|
123 |> separate "\n" |
|
124 |> implode |
|
125 *} |
|
126 |
113 ML {* fun single_fun_eq (at, s) = |
127 ML {* fun single_fun_eq (at, s) = |
114 ["function equations: ", s] |
128 ["function equations: ", s] |
115 |> separate "\n" |
129 |> separate "\n" |
116 |> implode |
130 |> implode |
117 *} |
131 *} |
121 |> separate "\n" |
135 |> separate "\n" |
122 |> implode |
136 |> implode |
123 *} |
137 *} |
124 |
138 |
125 ML {* |
139 ML {* |
126 fun print_dts (dts, (funs, feqs)) = |
140 fun print_dts (dts, (funs, feqs)) lthy = |
127 let |
141 let |
128 val _ = warning (implode (separate "\n" (map single_dt dts))) |
142 val _ = warning (implode (separate "\n" (map single_dt dts))) |
129 val _ = warning (implode (separate "\n" (map single_fun_fix funs))) |
143 val _ = warning (implode (separate "\n" (map single_fun_fix funs))) |
130 val _ = warning (implode (separate "\n" (map single_fun_eq feqs))) |
144 val _ = warning (implode (separate "\n" (map single_fun_eq feqs))) |
|
145 val _ = warning (implode (separate "\n" (map fv_dt dts))) |
131 in |
146 in |
132 () |
147 () |
133 end |
148 end |
134 *} |
149 *} |
135 |
150 |
161 ML {* |
176 ML {* |
162 fun fn_defn [] [] thy = thy |
177 fun fn_defn [] [] thy = thy |
163 | fn_defn funs feqs thy = |
178 | fn_defn funs feqs thy = |
164 let |
179 let |
165 val lthy = Theory_Target.init NONE thy |
180 val lthy = Theory_Target.init NONE thy |
166 val ctxt = Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
181 val lthy = Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
167 val thy' = ProofContext.theory_of ctxt |
182 val thy' = Local_Theory.exit_global ctxt |
168 in |
183 in |
169 thy' |
184 thy' |
170 end |
185 end |
171 *} |
186 *} |
172 |
187 |
173 |
188 |
174 ML {* |
189 ML {* |
175 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
190 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
176 let |
191 dt_defn (map transp_dt dts) thy |
177 val thy1 = dt_defn (map transp_dt dts) thy |
192 |> fn_defn funs feqs |
178 val thy2 = fn_defn funs feqs thy1 |
193 |> Theory_Target.init NONE |
179 val _ = print_dts (dts, (funs, feqs)) |
194 |> print_dts (dts, (funs, feqs)) |
180 in |
195 |> Local_Theory.exit_global |
181 thy2 |
196 *} |
182 end *} |
|
183 |
197 |
184 (* Command Keyword *) |
198 (* Command Keyword *) |
185 ML {* |
199 ML {* |
186 let |
200 let |
187 val kind = OuterKeyword.thy_decl |
201 val kind = OuterKeyword.thy_decl |