src/Pure/Tools/codegen_names.ML
author haftmann
Fri, 29 Dec 2006 12:11:04 +0100
changeset 21927 9677abe5d374
parent 21915 4e63c55f4cb4
child 21931 314f9e2a442c
permissions -rw-r--r--
added handling for explicit classrel witnesses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Tools/codegen_names.ML
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     2
    ID:         $Id$
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     4
21461
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
     5
Naming policies for code generation: prefixing any name by corresponding theory name,
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
     6
conversion to alphanumeric representation, name space identifier.
20855
9f60d493c8fe clarified header comments
haftmann
parents: 20835
diff changeset
     7
Mappings are incrementally cached.
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     8
*)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
     9
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    10
signature CODEGEN_NAMES =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    11
sig
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    12
  type tyco = string
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    13
  type const = string
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    14
  val class: theory -> class -> class
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
    15
  val class_rev: theory -> class -> class option
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    16
  val classrel: theory -> class * class -> string
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    17
  val classrel_rev: theory -> string -> (class * class) option
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    18
  val tyco: theory -> tyco -> tyco
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
    19
  val tyco_rev: theory -> tyco -> tyco option
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    20
  val instance: theory -> class * tyco -> string
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
    21
  val instance_rev: theory -> string -> (class * tyco) option
20585
3fe913d70177 cleanupdiff
haftmann
parents: 20456
diff changeset
    22
  val const: theory -> CodegenConsts.const -> const
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
    23
  val const_rev: theory -> const -> CodegenConsts.const option
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    24
  val purify_var: string -> string
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
    25
  val purify_tvar: string -> string
21014
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
    26
  val check_modulename: string -> string
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    27
end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    28
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    29
structure CodegenNames: CODEGEN_NAMES =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    30
struct
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    31
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    32
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    33
(* theory data *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    34
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    35
type tyco = string;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    36
type const = string;
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    37
val string_pair_ord = prod_ord fast_string_ord fast_string_ord;
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    38
val eq_string_pair = is_equal o string_pair_ord;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    39
structure Consttab = CodegenConsts.Consttab;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    40
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    41
structure StringPairTab =
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    42
  TableFun(
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    43
    type key = string * string;
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    44
    val ord = string_pair_ord;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    45
  );
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    46
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    47
datatype names = Names of {
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    48
  class: class Symtab.table * class Symtab.table,
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    49
  classrel: string StringPairTab.table * (class * class) Symtab.table,
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    50
  tyco: tyco Symtab.table * tyco Symtab.table,
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    51
  instance: string StringPairTab.table * (class * tyco) Symtab.table,
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    52
  const: const Consttab.table * (string * typ list) Symtab.table
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    53
}
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    54
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    55
val empty_names = Names {
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    56
  class = (Symtab.empty, Symtab.empty),
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    57
  classrel = (StringPairTab.empty, Symtab.empty),
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    58
  tyco = (Symtab.empty, Symtab.empty),
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    59
  instance = (StringPairTab.empty, Symtab.empty),
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    60
  const = (Consttab.empty, Symtab.empty)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    61
};
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    62
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    63
local
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    64
  fun mk_names (class, classrel, tyco, instance, const) =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    65
    Names { class = class, classrel = classrel, tyco = tyco, instance = instance, const = const};
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    66
  fun map_names f (Names { class, classrel, tyco, instance, const }) =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    67
    mk_names (f (class, classrel, tyco, instance, const));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    68
  val eq_string = op = : string * string -> bool;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    69
in
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    70
  fun merge_names (Names { class = (class1, classrev1),
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    71
      classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    72
      instance = (instance1, instancerev1), const = (const1, constrev1) },
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    73
    Names { class = (class2, classrev2),
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    74
      classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    75
      instance = (instance2, instancerev2), const = (const2, constrev2) }) =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    76
    mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    77
      (StringPairTab.merge eq_string (classrel1, classrel2), Symtab.merge eq_string_pair (classrelrev1, classrelrev2)),
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    78
      (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    79
      (StringPairTab.merge eq_string (instance1, instance2), Symtab.merge eq_string_pair (instancerev1, instancerev2)),
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
    80
      (Consttab.merge eq_string (const1, const2), Symtab.merge CodegenConsts.eq_const (constrev1, constrev2)));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    81
  fun map_class f = map_names
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    82
    (fn (class, classrel, tyco, inst, const) => (f class, classrel, tyco, inst, const));
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    83
  fun map_classrel f = map_names
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    84
    (fn (class, classrel, tyco, inst, const) => (class, f classrel, tyco, inst, const));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    85
  fun map_tyco f = map_names
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    86
    (fn (class, classrel, tyco, inst, const) => (class, classrel, f tyco, inst, const));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    87
  fun map_inst f = map_names
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    88
    (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, f inst, const));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    89
  fun map_const f = map_names
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
    90
    (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, inst, f const));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    91
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    92
end; (*local*)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    93
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20389
diff changeset
    94
structure CodeName = TheoryDataFun
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    95
(struct
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    96
  val name = "Pure/codegen_names";
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    97
  type T = names ref;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    98
  val empty = ref empty_names;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
    99
  fun copy (ref names) = ref names;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   100
  val extend = copy;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   101
  fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   102
  fun print _ _ = ();
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   103
end);
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   104
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20389
diff changeset
   105
val _ = Context.add_setup CodeName.init;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   106
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   107
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   108
(* forward lookup with cache update *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   109
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   110
fun get thy get_tabs get upd_names upd policy x =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   111
  let
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20389
diff changeset
   112
    val names_ref = CodeName.get thy
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   113
    val (Names names) = ! names_ref;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   114
    val tabs = get_tabs names;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   115
    fun declare name =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   116
      let
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   117
        val names' = upd_names (K (upd (x, name) (fst tabs),
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   118
          Symtab.update_new (name, x) (snd tabs))) (Names names)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   119
      in (names_ref := names'; name) end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   120
  in case get (fst tabs) x
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   121
   of SOME name => name
21338
56d55dd30311 cleaned up
haftmann
parents: 21191
diff changeset
   122
    | NONE => 
56d55dd30311 cleaned up
haftmann
parents: 21191
diff changeset
   123
        x
56d55dd30311 cleaned up
haftmann
parents: 21191
diff changeset
   124
        |> policy thy
56d55dd30311 cleaned up
haftmann
parents: 21191
diff changeset
   125
        |> Name.variant (Symtab.keys (snd tabs))
56d55dd30311 cleaned up
haftmann
parents: 21191
diff changeset
   126
        |> declare
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   127
  end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   128
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   129
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   130
(* backward lookup *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   131
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   132
fun rev thy get_tabs errname name =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   133
  let
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20389
diff changeset
   134
    val names_ref = CodeName.get thy
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   135
    val (Names names) = ! names_ref;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   136
    val tab = (snd o get_tabs) names;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   137
  in case Symtab.lookup tab name
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   138
   of SOME x => x
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   139
    | NONE => error ("No such " ^ errname ^ ": " ^ quote name)
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   140
  end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   141
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   142
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   143
(* theory name lookup *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   144
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   145
fun thyname_of thy f errmsg x =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   146
  let
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   147
    fun thy_of thy =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   148
      if f thy x then case get_first thy_of (Theory.parents_of thy)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   149
        of NONE => SOME thy
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   150
         | thy => thy
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   151
      else NONE;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   152
  in case thy_of thy
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   153
   of SOME thy => Context.theory_name thy
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   154
    | NONE => error (errmsg x) end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   155
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   156
fun thyname_of_class thy =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   157
  thyname_of thy (fn thy => member (op =) (Sign.classes thy))
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   158
    (fn class => "thyname_of_class: no such class: " ^ quote class);
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   159
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   160
fun thyname_of_classrel thy =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   161
  thyname_of thy (fn thy => fn (class1, class2) => Sign.subsort thy ([class1], [class2]))
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   162
    (fn (class1, class2) => "thyname_of_classrel: no such classrel: " ^ quote class1 ^ " in " ^ quote class2);
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   163
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   164
fun thyname_of_tyco thy =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   165
  thyname_of thy Sign.declared_tyname
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   166
    (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   167
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   168
fun thyname_of_instance thy =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   169
  let
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   170
    fun test_instance thy (class, tyco) =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   171
      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   172
  in thyname_of thy test_instance
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   173
    (fn (class, tyco) => "thyname_of_instance: no such instance: " ^ quote class ^ ", " ^ quote tyco)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   174
  end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   175
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   176
fun thyname_of_const thy =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   177
  thyname_of thy Sign.declared_const
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   178
    (fn c => "thyname_of_const: no such constant: " ^ quote c);
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   179
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   180
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   181
(* purification of identifiers *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   182
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   183
val purify_name =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   184
  let
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   185
    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   186
    val is_junk = not o is_valid andf Symbol.not_eof;
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   187
    val junk = Scan.many is_junk;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   188
    val scan_valids = Symbol.scanner "Malformed input"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   189
      ((junk |--
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   190
        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   191
        --| junk))
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   192
      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   193
  in explode #> scan_valids #> space_implode "_" end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   194
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   195
fun purify_op "0" = "zero"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   196
  | purify_op "1" = "one"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   197
  | purify_op s =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   198
      let
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   199
        fun rep_op "+" = SOME "sum"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   200
          | rep_op "-" = SOME "diff"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   201
          | rep_op "*" = SOME "prod"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   202
          | rep_op "/" = SOME "quotient"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   203
          | rep_op "&" = SOME "conj"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   204
          | rep_op "|" = SOME "disj"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   205
          | rep_op "=" = SOME "eq"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   206
          | rep_op "~" = SOME "inv"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   207
          | rep_op "@" = SOME "append"
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   208
          | rep_op s = NONE;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   209
        val scan_valids = Symbol.scanner "Malformed input"
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   210
           (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof));
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   211
      in (explode #> scan_valids #> implode) s end;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   212
21014
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   213
val purify_lower =
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   214
  explode
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   215
  #> (fn cs => (if forall Symbol.is_ascii_upper cs
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   216
        then map else nth_map 0) Symbol.to_ascii_lower cs)
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   217
  #> implode;
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   218
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   219
val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   220
21014
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   221
fun check_modulename mn =
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   222
  let
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   223
    val mns = NameSpace.explode mn;
21014
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   224
    val mns' = map purify_upper mns;
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   225
  in
21121
fae2187d6e2f refined
haftmann
parents: 21081
diff changeset
   226
    if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   227
      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
21014
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   228
  end
3b0c2641f740 refined
haftmann
parents: 20855
diff changeset
   229
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   230
fun purify_var "" = "x"
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   231
  | purify_var v = (purify_name #> purify_lower) v;
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   232
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   233
fun purify_tvar "" = "'a"
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   234
  | purify_tvar v =
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   235
      (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   236
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   237
val purify_idf = purify_op #> purify_name;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   238
val purify_prefix = map (purify_idf #> purify_upper);
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   239
val purify_base = purify_idf #> purify_lower;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   240
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   241
val dotify =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   242
  explode
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   243
  (*should disappear as soon as hierarchical theory name spaces are available*)
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   244
  #> Symbol.scanner "Malformed name"
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   245
      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   246
  #> implode;
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   247
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   248
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   249
(* naming policies *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   250
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   251
fun policy thy get_basename get_thyname name =
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   252
  let
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   253
    val prefix = (purify_prefix o NameSpace.explode o dotify o get_thyname thy) name;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   254
    val base = (purify_base o get_basename) name;
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   255
  in NameSpace.implode (prefix @ [base]) end;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   256
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   257
fun class_policy thy = policy thy NameSpace.base thyname_of_class;
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   258
fun classrel_policy thy = policy thy (fn (class1, class2) => 
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   259
  NameSpace.base class2 ^ "_" ^ NameSpace.base class1) thyname_of_classrel;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   260
fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   261
fun instance_policy thy = policy thy (fn (class, tyco) => 
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   262
  NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   263
21461
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   264
fun force_thyname thy (const as (c, tys)) =
20585
3fe913d70177 cleanupdiff
haftmann
parents: 20456
diff changeset
   265
  case AxClass.class_of_param thy c
3fe913d70177 cleanupdiff
haftmann
parents: 20456
diff changeset
   266
   of SOME class => (case tys
3fe913d70177 cleanupdiff
haftmann
parents: 20456
diff changeset
   267
       of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
21461
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   268
        | _ => SOME (thyname_of_class thy class))
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   269
    | NONE => (case CodegenData.get_datatype_of_constr thy const
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   270
   of SOME dtco => SOME (thyname_of_tyco thy dtco)
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   271
    | NONE => (case CodegenConsts.find_def thy const
20585
3fe913d70177 cleanupdiff
haftmann
parents: 20456
diff changeset
   272
   of SOME ((thyname, _), _) => SOME thyname
21461
51239d45247b forced name prefix for class operations
haftmann
parents: 21338
diff changeset
   273
    | NONE => NONE));
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   274
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   275
fun const_policy thy (c, tys) =
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   276
  case force_thyname thy (c, tys)
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   277
   of NONE => policy thy NameSpace.base thyname_of_const c
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   278
    | SOME thyname => let
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   279
        val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   280
        val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   281
        val base = map (purify_base o NameSpace.base) (c :: tycos);
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21461
diff changeset
   282
      in NameSpace.implode (prefix @ [space_implode "_" base]) end;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   283
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   284
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   285
(* shallow name spaces *)
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   286
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   287
val nsp_class = "class";
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   288
val nsp_classrel = "clsrel"
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   289
val nsp_tyco = "tyco";
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   290
val nsp_inst = "inst";
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   291
val nsp_const = "const";
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   292
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   293
fun add_nsp nsp name =
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   294
  NameSpace.append name nsp
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   295
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   296
fun dest_nsp nsp name =
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   297
  if NameSpace.base name = nsp
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   298
  then SOME (NameSpace.qualifier name)
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   299
  else NONE;
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   300
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   301
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   302
(* external interfaces *)
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   303
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   304
fun class thy =
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   305
  get thy #class Symtab.lookup map_class Symtab.update class_policy
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   306
  #> add_nsp nsp_class;
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   307
fun classrel thy =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   308
  get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   309
  #> add_nsp nsp_classrel;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   310
fun tyco thy =
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   311
  get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   312
  #> add_nsp nsp_tyco;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   313
fun instance thy =
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   314
  get thy #instance StringPairTab.lookup map_inst StringPairTab.update instance_policy
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   315
  #> add_nsp nsp_inst;
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   316
fun const thy =
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   317
  CodegenConsts.norm thy
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   318
  #> get thy #const Consttab.lookup map_const Consttab.update const_policy 
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   319
  #> add_nsp nsp_const;
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   320
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   321
fun class_rev thy =
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   322
  dest_nsp nsp_class
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   323
  #> Option.map (rev thy #class "class");
21927
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   324
fun classrel_rev thy =
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   325
  dest_nsp nsp_classrel
9677abe5d374 added handling for explicit classrel witnesses
haftmann
parents: 21915
diff changeset
   326
  #> Option.map (rev thy #classrel "class relation");
20697
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   327
fun tyco_rev thy =
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   328
  dest_nsp nsp_tyco
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   329
  #> Option.map (rev thy #tyco "type constructor");
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   330
fun instance_rev thy =
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   331
  dest_nsp nsp_inst
12952535fc2c added code_instname
haftmann
parents: 20585
diff changeset
   332
  #> Option.map (rev thy #instance "instance");
21915
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   333
fun const_rev thy =
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   334
  dest_nsp nsp_const
4e63c55f4cb4 different handling of type variable names
haftmann
parents: 21880
diff changeset
   335
  #> Option.map (rev thy #const "constant");
20353
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   336
d73e49780ef2 code generator refinements
haftmann
parents:
diff changeset
   337
end;