moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
authorwenzelm
Tue Mar 03 18:31:59 2009 +0100 (2009-03-03)
changeset 302224102bbf2af21
parent 30221 14145e81a2fe
child 30223 24d975352879
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/binding.ML	Tue Mar 03 17:42:30 2009 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Tue Mar 03 18:31:59 2009 +0100
     1.3 @@ -5,77 +5,93 @@
     1.4  Structured name bindings.
     1.5  *)
     1.6  
     1.7 +type bstring = string;    (*primitive names to be bound*)
     1.8 +
     1.9  signature BINDING =
    1.10  sig
    1.11 -  val separator: string
    1.12 -  val is_qualified: string -> bool
    1.13    type binding
    1.14 +  val dest: binding -> (string * bool) list * (string * bool) list * bstring
    1.15    val str_of: binding -> string
    1.16 -  val name_pos: string * Position.T -> binding
    1.17 -  val name: string -> binding
    1.18 +  val make: bstring * Position.T -> binding
    1.19 +  val name: bstring -> binding
    1.20 +  val pos_of: binding -> Position.T
    1.21 +  val name_of: binding -> string
    1.22 +  val map_name: (bstring -> bstring) -> binding -> binding
    1.23    val empty: binding
    1.24 -  val map_base: (string -> string) -> binding -> binding
    1.25 -  val qualify: string -> binding -> binding
    1.26 +  val is_empty: binding -> bool
    1.27 +  val qualify: bool -> string -> binding -> binding
    1.28 +  val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    1.29    val add_prefix: bool -> string -> binding -> binding
    1.30 -  val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
    1.31 -  val is_empty: binding -> bool
    1.32 -  val base_name: binding -> string
    1.33 -  val pos_of: binding -> Position.T
    1.34 -  val dest: binding -> (string * bool) list * string
    1.35  end;
    1.36  
    1.37  structure Binding: BINDING =
    1.38  struct
    1.39  
    1.40 -(** qualification **)
    1.41 -
    1.42 -val separator = ".";
    1.43 -val is_qualified = exists_string (fn s => s = separator);
    1.44 +(** representation **)
    1.45  
    1.46 -fun reject_qualified kind s =
    1.47 -  if is_qualified s then
    1.48 -    error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
    1.49 -  else s;
    1.50 +(* datatype *)
    1.51  
    1.52 +type component = string * bool;   (*name with mandatory flag*)
    1.53  
    1.54 -(** binding representation **)
    1.55 -
    1.56 -datatype binding = Binding of ((string * bool) list * string) * Position.T;
    1.57 -  (* (prefix components (with mandatory flag), base name, position) *)
    1.58 +datatype binding = Binding of
    1.59 + {prefix: component list,         (*system prefix*)
    1.60 +  qualifier: component list,      (*user qualifier*)
    1.61 +  name: bstring,                  (*base name*)
    1.62 +  pos: Position.T};               (*source position*)
    1.63  
    1.64 -fun str_of (Binding ((prefix, name), _)) =
    1.65 -  let
    1.66 -    fun mk_prefix (prfx, true) = prfx
    1.67 -      | mk_prefix (prfx, false) = enclose "(" ")" prfx
    1.68 -  in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end;
    1.69 +fun make_binding (prefix, qualifier, name, pos) =
    1.70 +  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    1.71 +
    1.72 +fun map_binding f (Binding {prefix, qualifier, name, pos}) =
    1.73 +  make_binding (f (prefix, qualifier, name, pos));
    1.74 +
    1.75 +fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
    1.76  
    1.77  
    1.78 -fun name_pos (name, pos) = Binding (([], name), pos);
    1.79 -fun name name = name_pos (name, Position.none);
    1.80 -val empty = name "";
    1.81 +(* diagnostic output *)
    1.82  
    1.83 -fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
    1.84 +val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
    1.85  
    1.86 -val map_base = map_binding o apsnd;
    1.87 +fun str_of (Binding {prefix, qualifier, name, pos}) =
    1.88 +  let
    1.89 +    val text =
    1.90 +      (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
    1.91 +      str_of_components qualifier ^ ":" ^ name;
    1.92 +    val props = Position.properties_of pos;
    1.93 +  in Markup.markup (Markup.properties props (Markup.binding name)) text end;
    1.94  
    1.95 -fun qualify_base path name =
    1.96 -  if path = "" orelse name = "" then name
    1.97 -  else path ^ separator ^ name;
    1.98 +
    1.99 +
   1.100 +(** basic operations **)
   1.101 +
   1.102 +(* name and position *)
   1.103 +
   1.104 +fun make (name, pos) = make_binding ([], [], name, pos);
   1.105 +fun name name = make (name, Position.none);
   1.106  
   1.107 -val qualify = map_base o qualify_base;
   1.108 -  (*FIXME should all operations on bare names move here from name_space.ML ?*)
   1.109 +fun pos_of (Binding {pos, ...}) = pos;
   1.110 +fun name_of (Binding {name, ...}) = name;
   1.111 +
   1.112 +fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
   1.113  
   1.114 -fun add_prefix sticky "" b = b
   1.115 -  | add_prefix sticky prfx b = (map_binding o apfst)
   1.116 -      (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
   1.117 +val empty = name "";
   1.118 +fun is_empty b = name_of b = "";
   1.119 +
   1.120 +
   1.121 +(* user qualifier *)
   1.122  
   1.123 -fun map_prefix f (Binding ((prefix, name), pos)) =
   1.124 -  f prefix (name_pos (name, pos));
   1.125 +fun qualify _ "" = I
   1.126 +  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
   1.127 +      (prefix, (qual, mandatory) :: qualifier, name, pos));
   1.128 +
   1.129  
   1.130 -fun is_empty (Binding ((_, name), _)) = name = "";
   1.131 -fun base_name (Binding ((_, name), _)) = name;
   1.132 -fun pos_of (Binding (_, pos)) = pos;
   1.133 -fun dest (Binding (prefix_name, _)) = prefix_name;
   1.134 +(* system prefix *)
   1.135 +
   1.136 +fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
   1.137 +  (f prefix, qualifier, name, pos));
   1.138 +
   1.139 +fun add_prefix _ "" = I
   1.140 +  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
   1.141  
   1.142  end;
   1.143  
     2.1 --- a/src/Pure/General/name_space.ML	Tue Mar 03 17:42:30 2009 +0100
     2.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 03 18:31:59 2009 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  Cf. Pure/General/binding.ML
     2.5  *)
     2.6  
     2.7 -type bstring = string;    (*simple names to be bound -- legacy*)
     2.8  type xstring = string;    (*external names*)
     2.9  
    2.10  signature BASIC_NAME_SPACE =
    2.11 @@ -67,8 +66,8 @@
    2.12  fun hidden name = "??." ^ name;
    2.13  val is_hidden = String.isPrefix "??.";
    2.14  
    2.15 -val separator = Binding.separator;
    2.16 -val is_qualified = Binding.is_qualified;
    2.17 +val separator = ".";
    2.18 +val is_qualified = exists_string (fn s => s = separator);
    2.19  
    2.20  val implode_name = space_implode separator;
    2.21  val explode_name = space_explode separator;
    2.22 @@ -295,13 +294,13 @@
    2.23      in space |> fold (add_name name) accs |> put_accesses name accs' end;
    2.24  
    2.25  fun full_name naming b =
    2.26 -  let val (prefix, bname) = Binding.dest b
    2.27 -  in full_internal (apply_prefix prefix naming) bname end;
    2.28 +  let val (prefix, qualifier, bname) = Binding.dest b
    2.29 +  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
    2.30  
    2.31  fun declare bnaming b =
    2.32    let
    2.33 -    val (prefix, bname) = Binding.dest b;
    2.34 -    val naming = apply_prefix prefix bnaming;
    2.35 +    val (prefix, qualifier, bname) = Binding.dest b;
    2.36 +    val naming = apply_prefix (prefix @ qualifier) bnaming;
    2.37      val name = full_internal naming bname;
    2.38    in declare_internal naming name #> pair name end;
    2.39