src/Tools/code/code_name.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 30161 c26e515f1c29
child 30648 17365ef082f3
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
     1 (*  Title:      Tools/code/code_name.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Some code generator infrastructure concerning names.
     5 *)
     6 
     7 signature CODE_NAME =
     8 sig
     9   structure StringPairTab: TABLE
    10   val first_upper: string -> string
    11   val first_lower: string -> string
    12   val dest_name: string -> string * string
    13 
    14   val purify_var: string -> string
    15   val purify_tvar: string -> string
    16   val purify_sym: string -> string
    17   val purify_base: bool -> 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 read_const_exprs: theory -> string list -> string list * string list
    26   val mk_name_module: Name.context -> string option -> (string -> string option)
    27     -> 'a Graph.T -> string -> string
    28 end;
    29 
    30 structure Code_Name: CODE_NAME =
    31 struct
    32 
    33 (** auxiliary **)
    34 
    35 structure StringPairTab =
    36   TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
    37 
    38 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    39 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    40 
    41 val dest_name =
    42   apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    43 
    44 
    45 (** purification **)
    46 
    47 fun purify_name upper lower =
    48   let
    49     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
    50     val is_junk = not o is_valid andf Symbol.is_regular;
    51     val junk = Scan.many is_junk;
    52     val scan_valids = Symbol.scanner "Malformed input"
    53       ((junk |--
    54         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
    55         --| junk))
    56       ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
    57     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
    58       else if lower then (if forall Symbol.is_ascii_upper cs
    59         then map else nth_map 0) Symbol.to_ascii_lower cs
    60       else cs;
    61   in
    62     explode
    63     #> scan_valids
    64     #> space_implode "_"
    65     #> explode
    66     #> upper_lower
    67     #> implode
    68   end;
    69 
    70 fun purify_var "" = "x"
    71   | purify_var v = purify_name false true v;
    72 
    73 fun purify_tvar "" = "'a"
    74   | purify_tvar v =
    75       (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
    76 
    77 val purify_prefix =
    78   explode
    79   (*FIMXE should disappear as soon as hierarchical theory name spaces are available*)
    80   #> Symbol.scanner "Malformed name"
    81       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
    82   #> implode
    83   #> Long_Name.explode
    84   #> map (purify_name true false);
    85 
    86 (*FIMXE non-canonical function treating non-canonical names*)
    87 fun purify_base _ "op &" = "and"
    88   | purify_base _ "op |" = "or"
    89   | purify_base _ "op -->" = "implies"
    90   | purify_base _ "{}" = "empty"
    91   | purify_base _ "op :" = "member"
    92   | purify_base _ "op Int" = "intersect"
    93   | purify_base _ "op Un" = "union"
    94   | purify_base _ "*" = "product"
    95   | purify_base _ "+" = "sum"
    96   | purify_base lower s = if String.isPrefix "op =" s
    97       then "eq" ^ purify_name false lower s
    98       else purify_name false lower s;
    99 
   100 val purify_sym = purify_base false;
   101 
   102 fun check_modulename mn =
   103   let
   104     val mns = Long_Name.explode mn;
   105     val mns' = map (purify_name true false) mns;
   106   in
   107     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
   108       ^ "perhaps try " ^ quote (Long_Name.implode mns'))
   109   end;
   110 
   111 
   112 (** variable name contexts **)
   113 
   114 type var_ctxt = string Symtab.table * Name.context;
   115 
   116 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
   117   Name.make_context names);
   118 
   119 fun intro_vars names (namemap, namectxt) =
   120   let
   121     val (names', namectxt') = Name.variants names namectxt;
   122     val namemap' = fold2 (curry Symtab.update) names names' namemap;
   123   in (namemap', namectxt') end;
   124 
   125 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
   126  of SOME name' => name'
   127   | NONE => error ("Invalid name in context: " ^ quote name);
   128 
   129 
   130 (** misc **)
   131 
   132 fun read_const_exprs thy =
   133   let
   134     fun consts_of some_thyname =
   135       let
   136         val thy' = case some_thyname
   137          of SOME thyname => ThyInfo.the_theory thyname thy
   138           | NONE => thy;
   139         val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   140           ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
   141         fun belongs_here c =
   142           not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
   143       in case some_thyname
   144        of NONE => cs
   145         | SOME thyname => filter belongs_here cs
   146       end;
   147     fun read_const_expr "*" = ([], consts_of NONE)
   148       | read_const_expr s = if String.isSuffix ".*" s
   149           then ([], consts_of (SOME (unsuffix ".*" s)))
   150           else ([Code_Unit.read_const thy s], []);
   151   in pairself flat o split_list o map read_const_expr end;
   152 
   153 fun mk_name_module reserved_names module_prefix module_alias program =
   154   let
   155     fun mk_alias name = case module_alias name
   156      of SOME name' => name'
   157       | NONE => name
   158           |> Long_Name.explode
   159           |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
   160           |> Long_Name.implode;
   161     fun mk_prefix name = case module_prefix
   162      of SOME module_prefix => Long_Name.append module_prefix name
   163       | NONE => name;
   164     val tab =
   165       Symtab.empty
   166       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
   167            o fst o dest_name o fst)
   168              program
   169   in the o Symtab.lookup tab end;
   170 
   171 end;