src/Pure/General/binding.ML
author wenzelm
Wed, 29 Aug 2012 11:48:45 +0200
changeset 48992 0518bf89c777
parent 46897 ec793befc232
child 50201 c26369c9eda6
permissions -rw-r--r--
renamed Position.str_of to Position.here;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/General/binding.ML
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
30214
f84c9f10292a moved name space externalization flags back to name_space.ML;
wenzelm
parents: 29617
diff changeset
     3
    Author:     Makarius
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     4
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     5
Structured name bindings.
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     6
*)
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
     7
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
     8
type bstring = string;    (*primitive names to be bound*)
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
     9
30214
f84c9f10292a moved name space externalization flags back to name_space.ML;
wenzelm
parents: 29617
diff changeset
    10
signature BINDING =
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    11
sig
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29338
diff changeset
    12
  type binding
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    13
  val dest: binding -> bool * (string * bool) list * bstring
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    14
  val make: bstring * Position.T -> binding
30276
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
    15
  val pos_of: binding -> Position.T
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    16
  val name: bstring -> binding
30464
a858ff86883b tuned signature;
wenzelm
parents: 30410
diff changeset
    17
  val name_of: binding -> bstring
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    18
  val map_name: (bstring -> bstring) -> binding -> binding
30338
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    19
  val prefix_name: string -> binding -> binding
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    20
  val suffix_name: string -> binding -> binding
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    21
  val eq_name: binding * binding -> bool
29617
b36bcbc1be3a tuned signature;
wenzelm
parents: 29581
diff changeset
    22
  val empty: binding
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    23
  val is_empty: binding -> bool
30410
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
    24
  val qualify: bool -> string -> binding -> binding
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33157
diff changeset
    25
  val qualified: bool -> string -> binding -> binding
30464
a858ff86883b tuned signature;
wenzelm
parents: 30410
diff changeset
    26
  val qualified_name: string -> binding
30276
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
    27
  val prefix_of: binding -> (string * bool) list
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    28
  val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
30335
b3ef64cadcad Binding.str_of: removed verbose feature, include qualifier in output;
wenzelm
parents: 30276
diff changeset
    29
  val prefix: bool -> string -> binding -> binding
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    30
  val conceal: binding -> binding
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 43546
diff changeset
    31
  val pretty: binding -> Pretty.T
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 41254
diff changeset
    32
  val print: binding -> string
41254
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
    33
  val bad: binding -> string
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
    34
  val check: binding -> unit
29617
b36bcbc1be3a tuned signature;
wenzelm
parents: 29581
diff changeset
    35
end;
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    36
32590
95f4f08f950f replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents: 30795
diff changeset
    37
structure Binding: BINDING =
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    38
struct
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    39
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    40
(** representation **)
29338
52a384648d13 separator, is_qualified
haftmann
parents: 29208
diff changeset
    41
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    42
(* datatype *)
29338
52a384648d13 separator, is_qualified
haftmann
parents: 29208
diff changeset
    43
32590
95f4f08f950f replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents: 30795
diff changeset
    44
abstype binding = Binding of
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    45
 {conceal: bool,                    (*internal -- for foundational purposes only*)
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    46
  prefix: (string * bool) list,     (*system prefix*)
30276
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
    47
  qualifier: (string * bool) list,  (*user qualifier*)
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
    48
  name: bstring,                    (*base name*)
32590
95f4f08f950f replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents: 30795
diff changeset
    49
  pos: Position.T}                  (*source position*)
95f4f08f950f replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents: 30795
diff changeset
    50
with
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    51
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    52
fun make_binding (conceal, prefix, qualifier, name, pos) =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    53
  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    54
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    55
fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    56
  make_binding (f (conceal, prefix, qualifier, name, pos));
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    57
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    58
fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    59
  (conceal, prefix @ qualifier, name);
30217
894eb2034f02 renamed Binding.display to Binding.str_of, which is slightly more canonical;
wenzelm
parents: 30214
diff changeset
    60
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    61
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    62
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    63
(** basic operations **)
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    64
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    65
(* name and position *)
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    66
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    67
fun make (name, pos) = make_binding (false, [], [], name, pos);
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    68
fun name name = make (name, Position.none);
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
    69
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    70
fun pos_of (Binding {pos, ...}) = pos;
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    71
fun name_of (Binding {name, ...}) = name;
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    72
30338
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    73
fun eq_name (b, b') = name_of b = name_of b';
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    74
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    75
fun map_name f =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    76
  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    77
    (conceal, prefix, qualifier, f name, pos));
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    78
30338
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    79
val prefix_name = map_name o prefix;
51d488f3dd72 added prefix_name, suffix_name;
wenzelm
parents: 30335
diff changeset
    80
val suffix_name = map_name o suffix;
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    81
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    82
val empty = name "";
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    83
fun is_empty b = name_of b = "";
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    84
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    85
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
    86
(* user qualifier *)
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
    87
30410
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
    88
fun qualify _ "" = I
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    89
  | qualify mandatory qual =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    90
      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
    91
        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
30410
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
    92
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33157
diff changeset
    93
fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33157
diff changeset
    94
  let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33157
diff changeset
    95
  in (conceal, prefix, qualifier', name', pos) end);
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33157
diff changeset
    96
30361
8ea7a197e2e6 added qualified_name -- emulates old-style qualified bstring;
wenzelm
parents: 30338
diff changeset
    97
fun qualified_name "" = empty
8ea7a197e2e6 added qualified_name -- emulates old-style qualified bstring;
wenzelm
parents: 30338
diff changeset
    98
  | qualified_name s =
8ea7a197e2e6 added qualified_name -- emulates old-style qualified bstring;
wenzelm
parents: 30338
diff changeset
    99
      let val (qualifier, name) = split_last (Long_Name.explode s)
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   100
      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
30361
8ea7a197e2e6 added qualified_name -- emulates old-style qualified bstring;
wenzelm
parents: 30338
diff changeset
   101
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   102
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
   103
(* system prefix *)
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
   104
30276
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
   105
fun prefix_of (Binding {prefix, ...}) = prefix;
51b92d34af79 added prefix_of;
wenzelm
parents: 30242
diff changeset
   106
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   107
fun map_prefix f =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   108
  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   109
    (conceal, f prefix, qualifier, name, pos));
30222
4102bbf2af21 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
wenzelm
parents: 30217
diff changeset
   110
30335
b3ef64cadcad Binding.str_of: removed verbose feature, include qualifier in output;
wenzelm
parents: 30276
diff changeset
   111
fun prefix _ "" = I
30410
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
   112
  | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
   113
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
   114
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   115
(* conceal *)
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   116
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   117
val conceal =
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   118
  map_binding (fn (_, prefix, qualifier, name, pos) =>
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   119
    (true, prefix, qualifier, name, pos));
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   120
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 32590
diff changeset
   121
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 41254
diff changeset
   122
(* print *)
30410
ef670320e281 added qualified_name_of;
wenzelm
parents: 30361
diff changeset
   123
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 43546
diff changeset
   124
fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
46897
ec793befc232 proper printing of empty binding (again, cf. 93f6f24010c2);
wenzelm
parents: 45666
diff changeset
   125
  if name = "" then Pretty.str "\"\""
ec793befc232 proper printing of empty binding (again, cf. 93f6f24010c2);
wenzelm
parents: 45666
diff changeset
   126
  else
ec793befc232 proper printing of empty binding (again, cf. 93f6f24010c2);
wenzelm
parents: 45666
diff changeset
   127
    Pretty.markup (Position.markup pos Isabelle_Markup.binding)
ec793befc232 proper printing of empty binding (again, cf. 93f6f24010c2);
wenzelm
parents: 45666
diff changeset
   128
      [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
ec793befc232 proper printing of empty binding (again, cf. 93f6f24010c2);
wenzelm
parents: 45666
diff changeset
   129
    |> Pretty.quote;
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
   130
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 43546
diff changeset
   131
val print = Pretty.str_of o pretty;
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 41254
diff changeset
   132
41254
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   133
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   134
(* check *)
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   135
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 46897
diff changeset
   136
fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
41254
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   137
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   138
fun check binding =
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   139
  if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   140
  else legacy_feature (bad binding);
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 39442
diff changeset
   141
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
   142
end;
32590
95f4f08f950f replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents: 30795
diff changeset
   143
end;
28941
128459bd72d2 new Binding module
haftmann
parents:
diff changeset
   144
30214
f84c9f10292a moved name space externalization flags back to name_space.ML;
wenzelm
parents: 29617
diff changeset
   145
type binding = Binding.binding;
f84c9f10292a moved name space externalization flags back to name_space.ML;
wenzelm
parents: 29617
diff changeset
   146