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