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