9 signature CODEGEN_NAMES = |
9 signature CODEGEN_NAMES = |
10 sig |
10 sig |
11 type tyco = string |
11 type tyco = string |
12 type const = string |
12 type const = string |
13 val class: theory -> class -> class |
13 val class: theory -> class -> class |
14 val class_rev: theory -> class -> class |
14 val class_rev: theory -> class -> class option |
15 val tyco: theory -> tyco -> tyco |
15 val tyco: theory -> tyco -> tyco |
16 val tyco_rev: theory -> tyco -> tyco |
16 val tyco_rev: theory -> tyco -> tyco option |
17 val tyco_force: tyco * string -> theory -> theory |
17 val tyco_force: tyco * string -> theory -> theory |
18 val instance: theory -> class * tyco -> string |
18 val instance: theory -> class * tyco -> string |
19 val instance_rev: theory -> string -> class * tyco |
19 val instance_rev: theory -> string -> (class * tyco) option |
|
20 val instance_force: (class * tyco) * string -> theory -> theory |
20 val const: theory -> CodegenConsts.const -> const |
21 val const: theory -> CodegenConsts.const -> const |
21 val const_rev: theory -> const -> CodegenConsts.const |
22 val const_rev: theory -> const -> CodegenConsts.const option |
22 val const_force: CodegenConsts.const * const -> theory -> theory |
23 val const_force: CodegenConsts.const * const -> theory -> theory |
23 val purify_var: string -> string |
24 val purify_var: string -> string |
|
25 val has_nsp: string -> string -> bool |
|
26 val nsp_module: string |
|
27 val nsp_class: string |
|
28 val nsp_tyco: string |
|
29 val nsp_inst: string |
|
30 val nsp_fun: string |
|
31 val nsp_classop: string |
|
32 val nsp_dtco: string |
|
33 val nsp_eval: string |
24 end; |
34 end; |
25 |
35 |
26 structure CodegenNames: CODEGEN_NAMES = |
36 structure CodegenNames: CODEGEN_NAMES = |
27 struct |
37 struct |
28 |
38 |
276 Symtab.update_new (name, c_tys) constrev)) (Names names); |
286 Symtab.update_new (name, c_tys) constrev)) (Names names); |
277 in |
287 in |
278 thy |
288 thy |
279 end; |
289 end; |
280 |
290 |
|
291 fun instance_force (instance, name) thy = |
|
292 let |
|
293 val names = NameSpace.unpack name; |
|
294 val (prefix, base) = split_last (NameSpace.unpack name); |
|
295 val prefix' = purify_prefix prefix; |
|
296 val base' = purify_base base; |
|
297 val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix) |
|
298 then () |
|
299 else |
|
300 error ("Name violates naming conventions: " ^ quote name |
|
301 ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base']))) |
|
302 val names_ref = CodeName.get thy; |
|
303 val (Names names) = ! names_ref; |
|
304 val (inst, instrev) = #instance names; |
|
305 val _ = if Insttab.defined inst instance |
|
306 then error ("Instance already named: " ^ quote (fst instance) ^ ", " ^ quote (snd instance)) |
|
307 else (); |
|
308 val _ = if Symtab.defined instrev name |
|
309 then error ("Name already given to instance: " ^ quote name) |
|
310 else (); |
|
311 val _ = names_ref := map_inst (K (Insttab.update_new (instance, name) inst, |
|
312 Symtab.update_new (name, instance) instrev)) (Names names); |
|
313 in |
|
314 thy |
|
315 end; |
|
316 |
281 |
317 |
282 (* naming policies *) |
318 (* naming policies *) |
283 |
319 |
284 fun policy thy get_basename get_thyname name = |
320 fun policy thy get_basename get_thyname name = |
285 let |
321 let |
309 val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys; |
345 val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys; |
310 val base = map (purify_base o NameSpace.base) (c :: tycos); |
346 val base = map (purify_base o NameSpace.base) (c :: tycos); |
311 in NameSpace.pack (prefix @ [space_implode "_" base]) end; |
347 in NameSpace.pack (prefix @ [space_implode "_" base]) end; |
312 |
348 |
313 |
349 |
|
350 (* shallow name spaces *) |
|
351 |
|
352 val nsp_module = ""; (*a dummy by convention*) |
|
353 val nsp_class = "class"; |
|
354 val nsp_tyco = "tyco"; |
|
355 val nsp_inst = "inst"; |
|
356 val nsp_fun = "fun"; |
|
357 val nsp_classop = "classop"; |
|
358 val nsp_dtco = "dtco"; |
|
359 val nsp_eval = "EVAL"; (*only for evaluation*) |
|
360 |
|
361 fun add_nsp shallow name = |
|
362 name |
|
363 |> NameSpace.unpack |
|
364 |> split_last |
|
365 |> apsnd (single #> cons shallow) |
|
366 |> (op @) |
|
367 |> NameSpace.pack; |
|
368 |
|
369 fun dest_nsp nsp nspname = |
|
370 let |
|
371 val xs = NameSpace.unpack nspname; |
|
372 val (ys, base) = split_last xs; |
|
373 val (module, shallow) = split_last ys; |
|
374 in |
|
375 if nsp = shallow |
|
376 then (SOME o NameSpace.pack) (module @ [base]) |
|
377 else NONE |
|
378 end; |
|
379 |
|
380 val has_nsp = is_some oo dest_nsp; |
|
381 |
|
382 fun if_nsp nsp f idf = |
|
383 Option.map f (dest_nsp nsp idf); |
|
384 |
|
385 |
314 (* external interfaces *) |
386 (* external interfaces *) |
315 |
387 |
316 fun class thy = |
388 fun class thy = |
317 get thy #class Symtab.lookup map_class Symtab.update class_policy; |
389 get thy #class Symtab.lookup map_class Symtab.update class_policy |
|
390 #> add_nsp nsp_class; |
318 fun tyco thy = |
391 fun tyco thy = |
319 get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy; |
392 get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy |
|
393 #> add_nsp nsp_tyco; |
320 fun instance thy = |
394 fun instance thy = |
321 get thy #instance Insttab.lookup map_inst Insttab.update instance_policy; |
395 get thy #instance Insttab.lookup map_inst Insttab.update instance_policy |
322 fun const thy = |
396 #> add_nsp nsp_inst; |
323 get thy #const Consttab.lookup map_const Consttab.update const_policy |
397 fun const thy c_ty = case CodegenConsts.norm thy c_ty |
324 o CodegenConsts.norm thy; |
398 of (c_tys as (c, tys)) => add_nsp (if (is_some o CodegenData.get_datatype_of_constr thy) c_tys |
325 |
399 then nsp_dtco |
326 fun class_rev thy = rev thy #class "class"; |
400 else if (is_some o AxClass.class_of_param thy) c andalso |
327 fun tyco_rev thy = rev thy #tyco "type constructor"; |
401 case tys of [TFree _] => true | [TVar _] => true | _ => false |
328 fun instance_rev thy = rev thy #instance "instance"; |
402 then nsp_classop |
329 fun const_rev thy = rev thy #const "constant"; |
403 else nsp_fun) |
|
404 (get thy #const Consttab.lookup map_const Consttab.update const_policy c_tys); |
|
405 |
|
406 fun class_rev thy = |
|
407 dest_nsp nsp_class |
|
408 #> Option.map (rev thy #class "class"); |
|
409 fun tyco_rev thy = |
|
410 dest_nsp nsp_tyco |
|
411 #> Option.map (rev thy #tyco "type constructor"); |
|
412 fun instance_rev thy = |
|
413 dest_nsp nsp_inst |
|
414 #> Option.map (rev thy #instance "instance"); |
|
415 fun const_rev thy nspname = |
|
416 (case dest_nsp nsp_fun nspname |
|
417 of name as SOME _ => name |
|
418 | _ => (case dest_nsp nsp_dtco nspname |
|
419 of name as SOME _ => name |
|
420 | _ => (case dest_nsp nsp_classop nspname |
|
421 of name as SOME _ => name |
|
422 | _ => NONE))) |
|
423 |> Option.map (rev thy #const "constant"); |
330 |
424 |
331 |
425 |
332 (* outer syntax *) |
426 (* outer syntax *) |
333 |
427 |
334 local |
428 local |
340 const_force (CodegenConsts.read_const thy raw_c, name) thy; |
434 const_force (CodegenConsts.read_const thy raw_c, name) thy; |
341 |
435 |
342 fun tyco_force_e (raw_tyco, name) thy = |
436 fun tyco_force_e (raw_tyco, name) thy = |
343 tyco_force (Sign.intern_type thy raw_tyco, name) thy; |
437 tyco_force (Sign.intern_type thy raw_tyco, name) thy; |
344 |
438 |
345 val (constnameK, typenameK) = ("code_constname", "code_typename"); |
439 fun instance_force_e ((raw_tyco, raw_class), name) thy = |
|
440 instance_force ((Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco), name) thy; |
|
441 |
|
442 val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname"); |
346 |
443 |
347 val constnameP = |
444 val constnameP = |
348 OuterSyntax.command constnameK "declare code name for constant" K.thy_decl ( |
445 OuterSyntax.command constnameK "declare code name for constant" K.thy_decl ( |
349 Scan.repeat1 (P.term -- P.name) |
446 Scan.repeat1 (P.term -- P.name) |
350 >> (fn aliasses => |
447 >> (fn aliasses => |
351 Toplevel.theory (fold const_force_e aliasses)) |
448 Toplevel.theory (fold const_force_e aliasses)) |
352 ); |
449 ); |
353 |
450 |
354 val typenameP = |
451 val typenameP = |
355 OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl ( |
452 OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl ( |
356 Scan.repeat1 (P.name -- P.name) |
453 Scan.repeat1 (P.xname -- P.name) |
357 >> (fn aliasses => |
454 >> (fn aliasses => |
358 Toplevel.theory (fold tyco_force_e aliasses)) |
455 Toplevel.theory (fold tyco_force_e aliasses)) |
359 ); |
456 ); |
360 |
457 |
|
458 val instnameP = |
|
459 OuterSyntax.command instnameK "declare code name for instance relation" K.thy_decl ( |
|
460 Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name) |
|
461 >> (fn aliasses => |
|
462 Toplevel.theory (fold instance_force_e aliasses)) |
|
463 ); |
|
464 |
361 in |
465 in |
362 |
466 |
363 val _ = OuterSyntax.add_parsers [constnameP, typenameP]; |
467 val _ = OuterSyntax.add_parsers [constnameP, typenameP, instnameP]; |
364 |
468 |
365 |
469 |
366 end; (*local*) |
470 end; (*local*) |
367 |
471 |
368 end; |
472 end; |