src/Pure/Tools/codegen_names.ML
changeset 21927 9677abe5d374
parent 21915 4e63c55f4cb4
child 21931 314f9e2a442c
equal deleted inserted replaced
21926:1091904ddb19 21927:9677abe5d374
    11 sig
    11 sig
    12   type tyco = string
    12   type tyco = string
    13   type const = string
    13   type const = string
    14   val class: theory -> class -> class
    14   val class: theory -> class -> class
    15   val class_rev: theory -> class -> class option
    15   val class_rev: theory -> class -> class option
       
    16   val classrel: theory -> class * class -> string
       
    17   val classrel_rev: theory -> string -> (class * class) option
    16   val tyco: theory -> tyco -> tyco
    18   val tyco: theory -> tyco -> tyco
    17   val tyco_rev: theory -> tyco -> tyco option
    19   val tyco_rev: theory -> tyco -> tyco option
    18   val instance: theory -> class * tyco -> string
    20   val instance: theory -> class * tyco -> string
    19   val instance_rev: theory -> string -> (class * tyco) option
    21   val instance_rev: theory -> string -> (class * tyco) option
    20   val const: theory -> CodegenConsts.const -> const
    22   val const: theory -> CodegenConsts.const -> const
    30 
    32 
    31 (* theory data *)
    33 (* theory data *)
    32 
    34 
    33 type tyco = string;
    35 type tyco = string;
    34 type const = string;
    36 type const = string;
    35 val inst_ord = prod_ord fast_string_ord fast_string_ord;
    37 val string_pair_ord = prod_ord fast_string_ord fast_string_ord;
    36 val eq_inst = is_equal o inst_ord;
    38 val eq_string_pair = is_equal o string_pair_ord;
    37 structure Consttab = CodegenConsts.Consttab;
    39 structure Consttab = CodegenConsts.Consttab;
    38 
    40 
    39 structure Insttab =
    41 structure StringPairTab =
    40   TableFun(
    42   TableFun(
    41     type key = class * tyco;
    43     type key = string * string;
    42     val ord = inst_ord;
    44     val ord = string_pair_ord;
    43   );
    45   );
    44 
    46 
    45 datatype names = Names of {
    47 datatype names = Names of {
    46   class: class Symtab.table * class Symtab.table,
    48   class: class Symtab.table * class Symtab.table,
       
    49   classrel: string StringPairTab.table * (class * class) Symtab.table,
    47   tyco: tyco Symtab.table * tyco Symtab.table,
    50   tyco: tyco Symtab.table * tyco Symtab.table,
    48   instance: string Insttab.table * (class * tyco) Symtab.table,
    51   instance: string StringPairTab.table * (class * tyco) Symtab.table,
    49   const: const Consttab.table * (string * typ list) Symtab.table
    52   const: const Consttab.table * (string * typ list) Symtab.table
    50 }
    53 }
    51 
    54 
    52 val empty_names = Names {
    55 val empty_names = Names {
    53   class = (Symtab.empty, Symtab.empty),
    56   class = (Symtab.empty, Symtab.empty),
       
    57   classrel = (StringPairTab.empty, Symtab.empty),
    54   tyco = (Symtab.empty, Symtab.empty),
    58   tyco = (Symtab.empty, Symtab.empty),
    55   instance = (Insttab.empty, Symtab.empty),
    59   instance = (StringPairTab.empty, Symtab.empty),
    56   const = (Consttab.empty, Symtab.empty)
    60   const = (Consttab.empty, Symtab.empty)
    57 };
    61 };
    58 
    62 
    59 local
    63 local
    60   fun mk_names (class, tyco, instance, const) =
    64   fun mk_names (class, classrel, tyco, instance, const) =
    61     Names { class = class, tyco = tyco, instance = instance, const = const};
    65     Names { class = class, classrel = classrel, tyco = tyco, instance = instance, const = const};
    62   fun map_names f (Names { class, tyco, instance, const }) =
    66   fun map_names f (Names { class, classrel, tyco, instance, const }) =
    63     mk_names (f (class, tyco, instance, const));
    67     mk_names (f (class, classrel, tyco, instance, const));
    64   val eq_string = op = : string * string -> bool;
    68   val eq_string = op = : string * string -> bool;
    65 in
    69 in
    66   fun merge_names (Names { class = (class1, classrev1), tyco = (tyco1, tycorev1),
    70   fun merge_names (Names { class = (class1, classrev1),
       
    71       classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
    67       instance = (instance1, instancerev1), const = (const1, constrev1) },
    72       instance = (instance1, instancerev1), const = (const1, constrev1) },
    68     Names { class = (class2, classrev2), tyco = (tyco2, tycorev2),
    73     Names { class = (class2, classrev2),
       
    74       classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
    69       instance = (instance2, instancerev2), const = (const2, constrev2) }) =
    75       instance = (instance2, instancerev2), const = (const2, constrev2) }) =
    70     mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
    76     mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
       
    77       (StringPairTab.merge eq_string (classrel1, classrel2), Symtab.merge eq_string_pair (classrelrev1, classrelrev2)),
    71       (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
    78       (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
    72       (Insttab.merge eq_string (instance1, instance2), Symtab.merge eq_inst (instancerev1, instancerev2)),
    79       (StringPairTab.merge eq_string (instance1, instance2), Symtab.merge eq_string_pair (instancerev1, instancerev2)),
    73       (Consttab.merge eq_string (const1, const2), Symtab.merge CodegenConsts.eq_const (constrev1, constrev2)));
    80       (Consttab.merge eq_string (const1, const2), Symtab.merge CodegenConsts.eq_const (constrev1, constrev2)));
    74   fun map_class f = map_names
    81   fun map_class f = map_names
    75     (fn (class, tyco, inst, const) => (f class, tyco, inst, const));
    82     (fn (class, classrel, tyco, inst, const) => (f class, classrel, tyco, inst, const));
       
    83   fun map_classrel f = map_names
       
    84     (fn (class, classrel, tyco, inst, const) => (class, f classrel, tyco, inst, const));
    76   fun map_tyco f = map_names
    85   fun map_tyco f = map_names
    77     (fn (class, tyco, inst, const) => (class, f tyco, inst, const));
    86     (fn (class, classrel, tyco, inst, const) => (class, classrel, f tyco, inst, const));
    78   fun map_inst f = map_names
    87   fun map_inst f = map_names
    79     (fn (class, tyco, inst, const) => (class, tyco, f inst, const));
    88     (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, f inst, const));
    80   fun map_const f = map_names
    89   fun map_const f = map_names
    81     (fn (class, tyco, inst, const) => (class, tyco, inst, f const));
    90     (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, inst, f const));
    82 
    91 
    83 end; (*local*)
    92 end; (*local*)
    84 
    93 
    85 structure CodeName = TheoryDataFun
    94 structure CodeName = TheoryDataFun
    86 (struct
    95 (struct
   140         of NONE => SOME thy
   149         of NONE => SOME thy
   141          | thy => thy
   150          | thy => thy
   142       else NONE;
   151       else NONE;
   143   in case thy_of thy
   152   in case thy_of thy
   144    of SOME thy => Context.theory_name thy
   153    of SOME thy => Context.theory_name thy
   145         |> explode
       
   146         (*should disappear as soon as hierarchical theory name spaces are available*)
       
   147         |> Symbol.scanner "Malformed name"
       
   148              (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
       
   149         |> implode
       
   150     | NONE => error (errmsg x) end;
   154     | NONE => error (errmsg x) end;
   151 
   155 
   152 fun thyname_of_class thy =
   156 fun thyname_of_class thy =
   153   thyname_of thy (fn thy => member (op =) (Sign.classes thy))
   157   thyname_of thy (fn thy => member (op =) (Sign.classes thy))
   154     (fn class => "thyname_of_class: no such class: " ^ quote class);
   158     (fn class => "thyname_of_class: no such class: " ^ quote class);
       
   159 
       
   160 fun thyname_of_classrel thy =
       
   161   thyname_of thy (fn thy => fn (class1, class2) => Sign.subsort thy ([class1], [class2]))
       
   162     (fn (class1, class2) => "thyname_of_classrel: no such classrel: " ^ quote class1 ^ " in " ^ quote class2);
   155 
   163 
   156 fun thyname_of_tyco thy =
   164 fun thyname_of_tyco thy =
   157   thyname_of thy Sign.declared_tyname
   165   thyname_of thy Sign.declared_tyname
   158     (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
   166     (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
   159 
   167 
   228 
   236 
   229 val purify_idf = purify_op #> purify_name;
   237 val purify_idf = purify_op #> purify_name;
   230 val purify_prefix = map (purify_idf #> purify_upper);
   238 val purify_prefix = map (purify_idf #> purify_upper);
   231 val purify_base = purify_idf #> purify_lower;
   239 val purify_base = purify_idf #> purify_lower;
   232 
   240 
       
   241 val dotify =
       
   242   explode
       
   243   (*should disappear as soon as hierarchical theory name spaces are available*)
       
   244   #> Symbol.scanner "Malformed name"
       
   245       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
       
   246   #> implode;
       
   247 
   233 
   248 
   234 (* naming policies *)
   249 (* naming policies *)
   235 
   250 
   236 fun policy thy get_basename get_thyname name =
   251 fun policy thy get_basename get_thyname name =
   237   let
   252   let
   238     val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
   253     val prefix = (purify_prefix o NameSpace.explode o dotify o get_thyname thy) name;
   239     val base = (purify_base o get_basename) name;
   254     val base = (purify_base o get_basename) name;
   240   in NameSpace.implode (prefix @ [base]) end;
   255   in NameSpace.implode (prefix @ [base]) end;
   241 
   256 
   242 fun class_policy thy = policy thy NameSpace.base thyname_of_class;
   257 fun class_policy thy = policy thy NameSpace.base thyname_of_class;
       
   258 fun classrel_policy thy = policy thy (fn (class1, class2) => 
       
   259   NameSpace.base class2 ^ "_" ^ NameSpace.base class1) thyname_of_classrel;
   243 fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
   260 fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
   244 fun instance_policy thy = policy thy (fn (class, tyco) => 
   261 fun instance_policy thy = policy thy (fn (class, tyco) => 
   245   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   262   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   246 
   263 
   247 fun force_thyname thy (const as (c, tys)) =
   264 fun force_thyname thy (const as (c, tys)) =
   257 
   274 
   258 fun const_policy thy (c, tys) =
   275 fun const_policy thy (c, tys) =
   259   case force_thyname thy (c, tys)
   276   case force_thyname thy (c, tys)
   260    of NONE => policy thy NameSpace.base thyname_of_const c
   277    of NONE => policy thy NameSpace.base thyname_of_const c
   261     | SOME thyname => let
   278     | SOME thyname => let
   262         val prefix = (purify_prefix o NameSpace.explode) thyname;
   279         val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
   263         val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
   280         val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
   264         val base = map (purify_base o NameSpace.base) (c :: tycos);
   281         val base = map (purify_base o NameSpace.base) (c :: tycos);
   265       in NameSpace.implode (prefix @ [space_implode "_" base]) end;
   282       in NameSpace.implode (prefix @ [space_implode "_" base]) end;
   266 
   283 
   267 
   284 
   268 (* shallow name spaces *)
   285 (* shallow name spaces *)
   269 
   286 
   270 val nsp_class = "class";
   287 val nsp_class = "class";
       
   288 val nsp_classrel = "clsrel"
   271 val nsp_tyco = "tyco";
   289 val nsp_tyco = "tyco";
   272 val nsp_inst = "inst";
   290 val nsp_inst = "inst";
   273 val nsp_const = "const";
   291 val nsp_const = "const";
   274 
   292 
   275 fun add_nsp nsp name =
   293 fun add_nsp nsp name =
   284 (* external interfaces *)
   302 (* external interfaces *)
   285 
   303 
   286 fun class thy =
   304 fun class thy =
   287   get thy #class Symtab.lookup map_class Symtab.update class_policy
   305   get thy #class Symtab.lookup map_class Symtab.update class_policy
   288   #> add_nsp nsp_class;
   306   #> add_nsp nsp_class;
       
   307 fun classrel thy =
       
   308   get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
       
   309   #> add_nsp nsp_classrel;
   289 fun tyco thy =
   310 fun tyco thy =
   290   get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   311   get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   291   #> add_nsp nsp_tyco;
   312   #> add_nsp nsp_tyco;
   292 fun instance thy =
   313 fun instance thy =
   293   get thy #instance Insttab.lookup map_inst Insttab.update instance_policy
   314   get thy #instance StringPairTab.lookup map_inst StringPairTab.update instance_policy
   294   #> add_nsp nsp_inst;
   315   #> add_nsp nsp_inst;
   295 fun const thy =
   316 fun const thy =
   296   CodegenConsts.norm thy
   317   CodegenConsts.norm thy
   297   #> get thy #const Consttab.lookup map_const Consttab.update const_policy 
   318   #> get thy #const Consttab.lookup map_const Consttab.update const_policy 
   298   #> add_nsp nsp_const;
   319   #> add_nsp nsp_const;
   299 
   320 
   300 fun class_rev thy =
   321 fun class_rev thy =
   301   dest_nsp nsp_class
   322   dest_nsp nsp_class
   302   #> Option.map (rev thy #class "class");
   323   #> Option.map (rev thy #class "class");
       
   324 fun classrel_rev thy =
       
   325   dest_nsp nsp_classrel
       
   326   #> Option.map (rev thy #classrel "class relation");
   303 fun tyco_rev thy =
   327 fun tyco_rev thy =
   304   dest_nsp nsp_tyco
   328   dest_nsp nsp_tyco
   305   #> Option.map (rev thy #tyco "type constructor");
   329   #> Option.map (rev thy #tyco "type constructor");
   306 fun instance_rev thy =
   330 fun instance_rev thy =
   307   dest_nsp nsp_inst
   331   dest_nsp nsp_inst