src/Tools/code/code_name.ML
author haftmann
Mon Dec 10 11:24:15 2007 +0100 (2007-12-10 ago)
changeset 25597 34860182b250
parent 25485 33840a854e63
child 25999 f8bcd311d501
permissions -rw-r--r--
moved instance parameter management from class.ML to axclass.ML
     1 (*  Title:      Tools/code/code_name.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Naming policies for code generation: prefixing any name by corresponding
     6 theory name, conversion to alphanumeric representation.
     7 Mappings are incrementally cached.  Assumes non-concurrent processing
     8 inside a single theory.
     9 *)
    10 
    11 signature CODE_NAME =
    12 sig
    13   val purify_var: string -> string
    14   val purify_tvar: string -> string
    15   val purify_sym: string -> string
    16   val check_modulename: string -> string
    17   type var_ctxt;
    18   val make_vars: string list -> var_ctxt;
    19   val intro_vars: string list -> var_ctxt -> var_ctxt;
    20   val lookup_var: var_ctxt -> string -> string;
    21 
    22   val class: theory -> class -> class
    23   val class_rev: theory -> class -> class option
    24   val classrel: theory -> class * class -> string
    25   val classrel_rev: theory -> string -> (class * class) option
    26   val tyco: theory -> string -> string
    27   val tyco_rev: theory -> string -> string option
    28   val instance: theory -> class * string -> string
    29   val instance_rev: theory -> string -> (class * string) option
    30   val const: theory -> string -> string
    31   val const_rev: theory -> string -> string option
    32   val value_name: string
    33   val labelled_name: theory -> string -> string
    34 
    35   val setup: theory -> theory
    36 end;
    37 
    38 structure CodeName: CODE_NAME =
    39 struct
    40 
    41 (** purification **)
    42 
    43 fun purify_name upper lower =
    44   let
    45     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
    46     val is_junk = not o is_valid andf Symbol.is_regular;
    47     val junk = Scan.many is_junk;
    48     val scan_valids = Symbol.scanner "Malformed input"
    49       ((junk |--
    50         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
    51         --| junk))
    52       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
    53     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
    54       else if lower then (if forall Symbol.is_ascii_upper cs
    55         then map else nth_map 0) Symbol.to_ascii_lower cs
    56       else cs;
    57   in
    58     explode
    59     #> scan_valids
    60     #> space_implode "_"
    61     #> explode
    62     #> upper_lower
    63     #> implode
    64   end;
    65 
    66 fun purify_var "" = "x"
    67   | purify_var v = purify_name false true v;
    68 
    69 fun purify_tvar "" = "'a"
    70   | purify_tvar v =
    71       (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
    72 
    73 fun check_modulename mn =
    74   let
    75     val mns = NameSpace.explode mn;
    76     val mns' = map (purify_name true false) mns;
    77   in
    78     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
    79       ^ "perhaps try " ^ quote (NameSpace.implode mns'))
    80   end;
    81 
    82 
    83 (** variable name contexts **)
    84 
    85 type var_ctxt = string Symtab.table * Name.context;
    86 
    87 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
    88   Name.make_context names);
    89 
    90 fun intro_vars names (namemap, namectxt) =
    91   let
    92     val (names', namectxt') = Name.variants names namectxt;
    93     val namemap' = fold2 (curry Symtab.update) names names' namemap;
    94   in (namemap', namectxt') end;
    95 
    96 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
    97  of SOME name' => name'
    98   | NONE => error ("Invalid name in context: " ^ quote name);
    99 
   100 
   101 
   102 (** global names (identifiers) **)
   103 
   104 (* identifier categories *)
   105 
   106 val suffix_class = "class";
   107 val suffix_classrel = "classrel"
   108 val suffix_tyco = "tyco";
   109 val suffix_instance = "inst";
   110 val suffix_const = "const";
   111 
   112 fun string_of_classrel (class, superclass) = class ^ " < " ^ superclass;
   113 fun string_of_instance (class, tyco) = tyco ^ " :: " ^ class;
   114 
   115 fun add_suffix nsp name =
   116   NameSpace.append name nsp;
   117 
   118 fun dest_suffix nsp name =
   119   if NameSpace.base name = nsp
   120   then SOME (NameSpace.qualifier name)
   121   else NONE;
   122 
   123 local
   124 
   125 val name_mapping  = [
   126   (suffix_class,       "class"),
   127   (suffix_classrel,    "subclass relation"),
   128   (suffix_tyco,        "type constructor"),
   129   (suffix_instance,    "instance"),
   130   (suffix_const,       "constant")
   131 ]
   132 
   133 in
   134 
   135 val category_of = the o AList.lookup (op =) name_mapping o NameSpace.base;
   136 
   137 end;
   138 
   139 
   140 (* theory name lookup *)
   141 
   142 fun thyname_of thy f errmsg x =
   143   let
   144     fun thy_of thy =
   145       if f thy x then case get_first thy_of (Theory.parents_of thy)
   146         of NONE => SOME thy
   147          | thy => thy
   148       else NONE;
   149   in case thy_of thy
   150    of SOME thy => Context.theory_name thy
   151     | NONE => error (errmsg x) end;
   152 
   153 fun thyname_of_class thy =
   154   thyname_of thy (fn thy => member (op =) (Sign.all_classes thy))
   155     (fn class => "thyname_of_class: no such class: " ^ quote class);
   156 
   157 fun thyname_of_tyco thy =
   158   thyname_of thy Sign.declared_tyname
   159     (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
   160 
   161 fun thyname_of_instance thy =
   162   let
   163     fun test_instance thy (class, tyco) =
   164       can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
   165   in thyname_of thy test_instance
   166     (fn (class, tyco) => "thyname_of_instance: no such instance: "
   167       ^ (quote o string_of_instance) (class, tyco))
   168   end;
   169 
   170 fun thyname_of_const thy =
   171   thyname_of thy Sign.declared_const
   172     (fn c => "thyname_of_const: no such constant: " ^ quote c);
   173 
   174 
   175 (* naming policies *)
   176 
   177 val purify_prefix =
   178   explode
   179   (*should disappear as soon as hierarchical theory name spaces are available*)
   180   #> Symbol.scanner "Malformed name"
   181       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   182   #> implode
   183   #> NameSpace.explode
   184   #> map (purify_name true false);
   185 
   186 fun purify_base _ "op &" = "and"
   187   | purify_base _ "op |" = "or"
   188   | purify_base _ "op -->" = "implies"
   189   | purify_base _ "{}" = "empty"
   190   | purify_base _ "op :" = "member"
   191   | purify_base _ "op Int" = "intersect"
   192   | purify_base _ "op Un" = "union"
   193   | purify_base _ "*" = "product"
   194   | purify_base _ "+" = "sum"
   195   | purify_base lower s = if String.isPrefix "op =" s
   196       then "eq" ^ purify_name false lower s
   197       else purify_name false lower s;
   198 
   199 val purify_sym = purify_base false;
   200 
   201 fun default_policy thy get_basename get_thyname name =
   202   let
   203     val prefix = (purify_prefix o get_thyname thy) name;
   204     val base = (purify_base true o get_basename) name;
   205   in NameSpace.implode (prefix @ [base]) end;
   206 
   207 fun class_policy thy = default_policy thy NameSpace.base thyname_of_class;
   208 fun classrel_policy thy = default_policy thy (fn (class1, class2) => 
   209   NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
   210   (*order fits nicely with composed projections*)
   211 fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco;
   212 fun instance_policy thy = default_policy thy (fn (class, tyco) => 
   213   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   214 
   215 fun force_thyname thy c = case Code.get_datatype_of_constr thy c
   216  of SOME dtco => SOME (thyname_of_tyco thy dtco)
   217   | NONE => (case AxClass.class_of_param thy c
   218      of SOME class => SOME (thyname_of_class thy class)
   219       | NONE => (case AxClass.inst_of_param thy c
   220          of SOME (c, tyco) => SOME (thyname_of_instance thy
   221               ((the o AxClass.class_of_param thy) c, tyco))
   222           | NONE => NONE));
   223 
   224 fun const_policy thy c =
   225   case force_thyname thy c
   226    of NONE => default_policy thy NameSpace.base thyname_of_const c
   227     | SOME thyname => let
   228         val prefix = purify_prefix thyname;
   229         val base = (purify_base true o NameSpace.base) c;
   230       in NameSpace.implode (prefix @ [base]) end;
   231 
   232 
   233 (* theory and code data *)
   234 
   235 type tyco = string;
   236 type const = string;
   237 
   238 structure StringPairTab =
   239   TableFun(
   240     type key = string * string;
   241     val ord = prod_ord fast_string_ord fast_string_ord;
   242   );
   243 
   244 datatype names = Names of {
   245   class: class Symtab.table * class Symtab.table,
   246   classrel: string StringPairTab.table * (class * class) Symtab.table,
   247   tyco: tyco Symtab.table * tyco Symtab.table,
   248   instance: string StringPairTab.table * (class * tyco) Symtab.table
   249 }
   250 
   251 val empty_names = Names {
   252   class = (Symtab.empty, Symtab.empty),
   253   classrel = (StringPairTab.empty, Symtab.empty),
   254   tyco = (Symtab.empty, Symtab.empty),
   255   instance = (StringPairTab.empty, Symtab.empty)
   256 };
   257 
   258 local
   259   fun mk_names (class, classrel, tyco, instance) =
   260     Names { class = class, classrel = classrel, tyco = tyco, instance = instance };
   261   fun map_names f (Names { class, classrel, tyco, instance }) =
   262     mk_names (f (class, classrel, tyco, instance));
   263 in
   264   fun merge_names (Names { class = (class1, classrev1),
   265       classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
   266       instance = (instance1, instancerev1) },
   267     Names { class = (class2, classrev2),
   268       classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
   269       instance = (instance2, instancerev2) }) =
   270     mk_names ((Symtab.merge (op =) (class1, class2), Symtab.merge (op =) (classrev1, classrev2)),
   271       (StringPairTab.merge (op =) (classrel1, classrel2), Symtab.merge (op =) (classrelrev1, classrelrev2)),
   272       (Symtab.merge (op =) (tyco1, tyco2), Symtab.merge (op =) (tycorev1, tycorev2)),
   273       (StringPairTab.merge (op =) (instance1, instance2), Symtab.merge (op =) (instancerev1, instancerev2)));
   274   fun map_class f = map_names
   275     (fn (class, classrel, tyco, inst) => (f class, classrel, tyco, inst));
   276   fun map_classrel f = map_names
   277     (fn (class, classrel, tyco, inst) => (class, f classrel, tyco, inst));
   278   fun map_tyco f = map_names
   279     (fn (class, classrel, tyco, inst) => (class, classrel, f tyco, inst));
   280   fun map_instance f = map_names
   281     (fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst));
   282 end; (*local*)
   283 
   284 structure CodeName = TheoryDataFun
   285 (
   286   type T = names ref;
   287   val empty = ref empty_names;
   288   fun copy (ref names) = ref names;
   289   val extend = copy;
   290   fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
   291 );
   292 
   293 structure ConstName = CodeDataFun
   294 (
   295   type T = const Symtab.table * string Symtab.table;
   296   val empty = (Symtab.empty, Symtab.empty);
   297   fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
   298     (Symtab.merge (op =) (const1, const2),
   299       Symtab.merge (op =) (constrev1, constrev2));
   300   fun purge _ NONE _ = empty
   301     | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
   302         fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
   303 );
   304 
   305 val setup = CodeName.init;
   306 
   307 
   308 (* forward lookup with cache update *)
   309 
   310 fun get thy get_tabs get upd_names upd policy x =
   311   let
   312     val names_ref = CodeName.get thy;
   313     val (Names names) = ! names_ref;
   314     val tabs = get_tabs names;
   315     fun declare name =
   316       let
   317         val names' = upd_names (K (upd (x, name) (fst tabs),
   318           Symtab.update_new (name, x) (snd tabs))) (Names names)
   319       in (names_ref := names'; name) end;
   320   in case get (fst tabs) x
   321    of SOME name => name
   322     | NONE => 
   323         x
   324         |> policy thy
   325         |> Name.variant (Symtab.keys (snd tabs))
   326         |> declare
   327   end;
   328 
   329 fun get_const thy const =
   330   let
   331     val tabs = ConstName.get thy;
   332     fun declare name =
   333       let
   334         val names' = (Symtab.update (const, name) (fst tabs),
   335           Symtab.update_new (name, const) (snd tabs))
   336       in (ConstName.change thy (K names'); name) end;
   337   in case Symtab.lookup (fst tabs) const
   338    of SOME name => name
   339     | NONE => 
   340         const
   341         |> const_policy thy
   342         |> Name.variant (Symtab.keys (snd tabs))
   343         |> declare
   344   end;
   345 
   346 
   347 (* backward lookup *)
   348 
   349 fun rev thy get_tabs name =
   350   let
   351     val names_ref = CodeName.get thy
   352     val (Names names) = ! names_ref;
   353     val tab = (snd o get_tabs) names;
   354   in case Symtab.lookup tab name
   355    of SOME x => x
   356     | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
   357   end;
   358 
   359 fun rev_const thy name =
   360   let
   361     val tab = snd (ConstName.get thy);
   362   in case Symtab.lookup tab name
   363    of SOME const => const
   364     | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
   365   end;
   366 
   367 
   368 (* external interfaces *)
   369 
   370 fun class thy =
   371   get thy #class Symtab.lookup map_class Symtab.update class_policy
   372   #> add_suffix suffix_class;
   373 fun classrel thy =
   374   get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
   375   #> add_suffix suffix_classrel;
   376 fun tyco thy =
   377   get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   378   #> add_suffix suffix_tyco;
   379 fun instance thy =
   380   get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
   381   #> add_suffix suffix_instance;
   382 fun const thy =
   383   get_const thy
   384   #> add_suffix suffix_const;
   385 
   386 fun class_rev thy =
   387   dest_suffix suffix_class
   388   #> Option.map (rev thy #class);
   389 fun classrel_rev thy =
   390   dest_suffix suffix_classrel
   391   #> Option.map (rev thy #classrel);
   392 fun tyco_rev thy =
   393   dest_suffix suffix_tyco
   394   #> Option.map (rev thy #tyco);
   395 fun instance_rev thy =
   396   dest_suffix suffix_instance
   397   #> Option.map (rev thy #instance);
   398 fun const_rev thy =
   399   dest_suffix suffix_const
   400   #> Option.map (rev_const thy);
   401 
   402 local
   403 
   404 val f_mapping = [
   405   (suffix_class,       class_rev),
   406   (suffix_classrel,    Option.map string_of_classrel oo classrel_rev),
   407   (suffix_tyco,        tyco_rev),
   408   (suffix_instance,    Option.map string_of_instance oo instance_rev),
   409   (suffix_const,       fn thy => Option.map (CodeUnit.string_of_const thy) o const_rev thy)
   410 ];
   411 
   412 in
   413 
   414 val value_name = "Isabelle_Eval.EVAL.EVAL"
   415 
   416 fun labelled_name thy suffix_name = if suffix_name = value_name then "<term>" else
   417   let
   418     val category = category_of suffix_name;
   419     val name = NameSpace.qualifier suffix_name;
   420     val suffix = NameSpace.base suffix_name
   421   in case (the o AList.lookup (op =) f_mapping) suffix thy suffix_name
   422    of SOME thing => category ^ " " ^ quote thing
   423     | NONE => error ("Unknown name: " ^ quote name)
   424   end;
   425 
   426 end;
   427 
   428 end;