23 -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a |
23 -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a |
24 val static_value_exn: 'a cookie -> theory -> string option |
24 val static_value_exn: 'a cookie -> theory -> string option |
25 -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result |
25 -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result |
26 val dynamic_holds_conv: conv |
26 val dynamic_holds_conv: conv |
27 val static_holds_conv: theory -> string list -> conv |
27 val static_holds_conv: theory -> string list -> conv |
28 val code_reflect: (string * string list) list -> string list -> string -> string option |
28 val code_reflect: (string * string list option) list -> string list -> string |
29 -> theory -> theory |
29 -> string option -> theory -> theory |
30 datatype truth = Holds |
30 datatype truth = Holds |
31 val put_truth: (unit -> truth) -> Proof.context -> Proof.context |
31 val put_truth: (unit -> truth) -> Proof.context -> Proof.context |
32 val trace: bool Unsynchronized.ref |
32 val trace: bool Unsynchronized.ref |
33 val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory |
33 val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory |
34 end; |
34 end; |
211 local |
211 local |
212 |
212 |
213 structure Code_Antiq_Data = Proof_Data |
213 structure Code_Antiq_Data = Proof_Data |
214 ( |
214 ( |
215 type T = (string list * string list) * (bool |
215 type T = (string list * string list) * (bool |
216 * (string * ((string * string) list * (string * string) list)) lazy); |
216 * (string * (string * string) list) lazy); |
217 fun init _ = (([], []), (true, (Lazy.value ("", ([], []))))); |
217 fun init _ = (([], []), (true, (Lazy.value ("", [])))); |
218 ); |
218 ); |
219 |
219 |
220 val is_first_occ = fst o snd o Code_Antiq_Data.get; |
220 val is_first_occ = fst o snd o Code_Antiq_Data.get; |
221 |
221 |
222 fun register_code new_tycos new_consts ctxt = |
222 fun register_code new_tycos new_consts ctxt = |
223 let |
223 let |
224 val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; |
224 val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; |
225 val tycos' = fold (insert (op =)) new_tycos tycos; |
225 val tycos' = fold (insert (op =)) new_tycos tycos; |
226 val consts' = fold (insert (op =)) new_consts consts; |
226 val consts' = fold (insert (op =)) new_consts consts; |
227 val acc_code = Lazy.lazy (fn () => |
227 val acc_code = Lazy.lazy (fn () => |
228 evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'); |
228 evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts' |
|
229 |> apsnd fst); |
229 in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; |
230 in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; |
230 |
231 |
231 fun register_const const = register_code [] [const]; |
232 fun register_const const = register_code [] [const]; |
232 |
233 |
233 fun register_datatype tyco constrs = register_code [tyco] constrs; |
234 fun print_const const all_struct_name consts_map = |
234 |
|
235 fun print_const const all_struct_name tycos_map consts_map = |
|
236 (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const; |
235 (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const; |
237 |
236 |
238 fun print_code is_first print_it ctxt = |
237 fun print_code is_first const ctxt = |
239 let |
238 let |
240 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
239 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
241 val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code; |
240 val (ml_code, consts_map) = Lazy.force acc_code; |
242 val ml_code = if is_first then ml_code |
241 val ml_code = if is_first then ml_code |
243 else ""; |
242 else ""; |
244 val all_struct_name = "Isabelle"; |
243 val all_struct_name = "Isabelle"; |
245 in (ml_code, print_it all_struct_name tycos_map consts_map) end; |
244 in (ml_code, print_const const all_struct_name consts_map) end; |
246 |
245 |
247 in |
246 in |
248 |
247 |
249 fun ml_code_antiq raw_const background = |
248 fun ml_code_antiq raw_const background = |
250 let |
249 let |
251 val const = Code.check_const (ProofContext.theory_of background) raw_const; |
250 val const = Code.check_const (ProofContext.theory_of background) raw_const; |
252 val is_first = is_first_occ background; |
251 val is_first = is_first_occ background; |
253 val background' = register_const const background; |
252 val background' = register_const const background; |
254 in (print_code is_first (print_const const), background') end; |
253 in (print_code is_first const, background') end; |
255 |
254 |
256 end; (*local*) |
255 end; (*local*) |
257 |
256 |
258 |
257 |
259 (* reflection support *) |
258 (* reflection support *) |
260 |
259 |
261 fun check_datatype thy tyco consts = |
260 fun check_datatype thy tyco some_consts = |
262 let |
261 let |
263 val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco; |
262 val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco; |
264 val missing_constrs = subtract (op =) consts constrs; |
263 val _ = case some_consts |
265 val _ = if null missing_constrs then [] |
264 of SOME consts => |
266 else error ("Missing constructor(s) " ^ commas (map quote missing_constrs) |
265 let |
267 ^ " for datatype " ^ quote tyco); |
266 val missing_constrs = subtract (op =) consts constrs; |
268 val false_constrs = subtract (op =) constrs consts; |
267 val _ = if null missing_constrs then [] |
269 val _ = if null false_constrs then [] |
268 else error ("Missing constructor(s) " ^ commas (map quote missing_constrs) |
270 else error ("Non-constructor(s) " ^ commas (map quote false_constrs) |
269 ^ " for datatype " ^ quote tyco); |
271 ^ " for datatype " ^ quote tyco); |
270 val false_constrs = subtract (op =) constrs consts; |
272 in () end; |
271 val _ = if null false_constrs then [] |
|
272 else error ("Non-constructor(s) " ^ commas (map quote false_constrs) |
|
273 ^ " for datatype " ^ quote tyco) |
|
274 in () end |
|
275 | NONE => (); |
|
276 in (tyco, constrs) end; |
273 |
277 |
274 fun add_eval_tyco (tyco, tyco') thy = |
278 fun add_eval_tyco (tyco, tyco') thy = |
275 let |
279 let |
276 val k = Sign.arity_number thy tyco; |
280 val k = Sign.arity_number thy tyco; |
277 fun pr pr' fxy [] = tyco' |
281 fun pr pr' _ [] = tyco' |
278 | pr pr' fxy [ty] = |
282 | pr pr' _ [ty] = |
279 Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] |
283 Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] |
280 | pr pr' fxy tys = |
284 | pr pr' _ tys = |
281 Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] |
285 Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] |
282 in |
286 in |
283 thy |
287 thy |
284 |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr)) |
288 |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr)) |
285 end; |
289 end; |