src/Pure/type.ML
changeset 16370 033d890fe91f
parent 16340 fd027bb32896
child 16444 80c8f742c6fc
     1.1 --- a/src/Pure/type.ML	Sat Jun 11 22:15:54 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Sat Jun 11 22:15:55 2005 +0200
     1.3 @@ -15,9 +15,9 @@
     1.4      Nonterminal
     1.5    type tsig
     1.6    val rep_tsig: tsig ->
     1.7 -   {classes: Sorts.classes,
     1.8 +   {classes: NameSpace.T * Sorts.classes,
     1.9      default: sort,
    1.10 -    types: (decl * stamp) Symtab.table,
    1.11 +    types: (decl * stamp) NameSpace.table,
    1.12      arities: Sorts.arities,
    1.13      log_types: string list,
    1.14      witness: (typ * sort) option}
    1.15 @@ -58,12 +58,14 @@
    1.16    val raw_unify: typ * typ -> bool
    1.17  
    1.18    (*extend and merge type signatures*)
    1.19 -  val add_classes: Pretty.pp -> (class * class list) list -> tsig -> tsig
    1.20 +  val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig
    1.21 +  val hide_classes: bool -> string list -> tsig -> tsig
    1.22    val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
    1.23    val set_defsort: sort -> tsig -> tsig
    1.24 -  val add_types: (string * int) list -> tsig -> tsig
    1.25 -  val add_abbrevs: (string * string list * typ) list -> tsig -> tsig
    1.26 -  val add_nonterminals: string list -> tsig -> tsig
    1.27 +  val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
    1.28 +  val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
    1.29 +  val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
    1.30 +  val hide_types: bool -> string list -> tsig -> tsig
    1.31    val add_arities: Pretty.pp -> arity list -> tsig -> tsig
    1.32    val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
    1.33  end;
    1.34 @@ -89,12 +91,12 @@
    1.35  
    1.36  datatype tsig =
    1.37    TSig of {
    1.38 -    classes: Sorts.classes,              (*declared classes with proper subclass relation*)
    1.39 -    default: sort,                       (*default sort on input*)
    1.40 -    types: (decl * stamp) Symtab.table,  (*declared types*)
    1.41 -    arities: Sorts.arities,              (*image specification of types wrt. sorts*)
    1.42 -    log_types: string list,              (*logical types sorted by number of arguments*)
    1.43 -    witness: (typ * sort) option};       (*witness for non-emptiness of strictest sort*)
    1.44 +    classes: NameSpace.T * Sorts.classes,   (*declared classes with proper subclass relation*)
    1.45 +    default: sort,                          (*default sort on input*)
    1.46 +    types: (decl * stamp) NameSpace.table,  (*declared types*)
    1.47 +    arities: Sorts.arities,                 (*image specification of types wrt. sorts*)
    1.48 +    log_types: string list,                 (*logical types sorted by number of arguments*)
    1.49 +    witness: (typ * sort) option};          (*witness for non-emptiness of strictest sort*)
    1.50  
    1.51  fun rep_tsig (TSig comps) = comps;
    1.52  
    1.53 @@ -102,43 +104,41 @@
    1.54    TSig {classes = classes, default = default, types = types, arities = arities,
    1.55      log_types = log_types, witness = witness};
    1.56  
    1.57 -fun map_tsig f (TSig {classes, default, types, arities, log_types, witness}) =
    1.58 -  make_tsig (f (classes, default, types, arities, log_types, witness));
    1.59 -
    1.60  fun build_tsig (classes, default, types, arities) =
    1.61    let
    1.62      fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
    1.63        | add_log_type (ts, _) = ts;
    1.64      val log_types =
    1.65 -      Symtab.foldl add_log_type ([], types)
    1.66 +      Symtab.foldl add_log_type ([], #2 types)
    1.67        |> Library.sort (Library.int_ord o pairself #2) |> map #1;
    1.68      val witness =
    1.69 -      (case Sorts.witness_sorts (classes, arities) log_types [] [Graph.keys classes] of
    1.70 +      (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
    1.71          [w] => SOME w | _ => NONE);
    1.72    in make_tsig (classes, default, types, arities, log_types, witness) end;
    1.73  
    1.74 -fun change_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
    1.75 +fun map_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
    1.76    build_tsig (f (classes, default, types, arities));
    1.77  
    1.78 -val empty_tsig = build_tsig (Graph.empty, [], Symtab.empty, Symtab.empty);
    1.79 +val empty_tsig =
    1.80 +  build_tsig ((NameSpace.empty, Graph.empty), [], NameSpace.empty_table, Symtab.empty);
    1.81  
    1.82  
    1.83  (* classes and sorts *)
    1.84  
    1.85 -fun classes (TSig {classes = C, ...}) = Graph.keys C;
    1.86 +fun classes (TSig {classes = (_, C), ...}) = Graph.keys C;
    1.87  fun defaultS (TSig {default, ...}) = default;
    1.88  fun logical_types (TSig {log_types, ...}) = log_types;
    1.89  fun universal_witness (TSig {witness, ...}) = witness;
    1.90  
    1.91 -fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq classes;
    1.92 -fun subsort (TSig {classes, ...}) = Sorts.sort_le classes;
    1.93 -fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (classes, arities);
    1.94 +fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
    1.95 +fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
    1.96 +fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
    1.97  
    1.98 -fun cert_class (TSig {classes, ...}) = Sorts.certify_class classes;
    1.99 -fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort classes;
   1.100 +fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
   1.101 +fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
   1.102  
   1.103  fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
   1.104 -  Sorts.witness_sorts (classes, arities) log_types;
   1.105 +  Sorts.witness_sorts (#2 classes, arities) log_types;
   1.106  
   1.107  
   1.108  (* certified types *)
   1.109 @@ -154,7 +154,7 @@
   1.110  
   1.111  fun certify_typ normalize syntax tsig ty =
   1.112    let
   1.113 -    val TSig {classes, types, ...} = tsig;
   1.114 +    val TSig {classes = (_, classes), types = (_, types), ...} = tsig;
   1.115      fun err msg = raise TYPE (msg, [ty], []);
   1.116  
   1.117      val check_syntax =
   1.118 @@ -338,7 +338,7 @@
   1.119        | NONE => T)
   1.120    | devar (T, tye) = T;
   1.121  
   1.122 -fun unify (tsig as TSig {classes, arities, ...}) (tyenv, maxidx) TU =
   1.123 +fun unify (tsig as TSig {classes = (_, classes), arities, ...}) (tyenv, maxidx) TU =
   1.124    let
   1.125      val tyvar_count = ref maxidx;
   1.126      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   1.127 @@ -445,10 +445,10 @@
   1.128  
   1.129  in
   1.130  
   1.131 -fun add_arities pp decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.132 +fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   1.133    let
   1.134      fun prep (t, Ss, S) =
   1.135 -      (case Symtab.lookup (types, t) of
   1.136 +      (case Symtab.lookup (#2 types, t) of
   1.137          SOME (LogicalType n, _) =>
   1.138            if length Ss = n then
   1.139              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   1.140 @@ -458,7 +458,7 @@
   1.141        | NONE => error (undecl_type t));
   1.142  
   1.143      val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   1.144 -    val arities' = fold (insert_arities pp classes) ars arities;
   1.145 +    val arities' = fold (insert_arities pp (#2 classes)) ars arities;
   1.146    in (classes, default, types, arities') end);
   1.147  
   1.148  fun rebuild_arities pp classes arities =
   1.149 @@ -481,40 +481,52 @@
   1.150    error (cat_lines (map (fn cs =>
   1.151      "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   1.152  
   1.153 -fun add_class pp (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.154 -  let
   1.155 -    val cs' = map (cert_class tsig) cs
   1.156 -      handle TYPE (msg, _, _) => error msg;
   1.157 -    val classes' = classes |> Graph.new_node (c, stamp ())
   1.158 -      handle Graph.DUP d => err_dup_classes [d];
   1.159 -    val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
   1.160 -      handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.161 -  in (classes'', default, types, arities) end);
   1.162 +fun add_class pp naming (c, cs) tsig =
   1.163 +  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.164 +    let
   1.165 +      val c' = NameSpace.full naming c;
   1.166 +      val cs' = map (cert_class tsig) cs
   1.167 +        handle TYPE (msg, _, _) => error msg;
   1.168 +      val space' = space |> NameSpace.declare naming c';
   1.169 +      val classes' = classes |> Graph.new_node (c', stamp ())
   1.170 +        handle Graph.DUP dup => err_dup_classes [dup];
   1.171 +      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c') cs')
   1.172 +        handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.173 +    in ((space', classes''), default, types, arities) end);
   1.174  
   1.175  in
   1.176  
   1.177 -val add_classes = fold o add_class;
   1.178 +val add_classes = fold oo add_class;
   1.179  
   1.180 -fun add_classrel pp ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   1.181 +fun add_classrel pp ps tsig =
   1.182 +  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.183 +    let
   1.184 +      val ps' = map (pairself (cert_class tsig)) ps
   1.185 +        handle TYPE (msg, _, _) => error msg;
   1.186 +      val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
   1.187 +        handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.188 +      val default' = default |> Sorts.norm_sort classes';
   1.189 +      val arities' = arities |> rebuild_arities pp classes';
   1.190 +    in ((space, classes'), default', types, arities') end);
   1.191 +
   1.192 +fun merge_classes pp ((space1, classes1), (space2, classes2)) =
   1.193    let
   1.194 -    val ps' = map (pairself (cert_class tsig)) ps
   1.195 -      handle TYPE (msg, _, _) => error msg;
   1.196 -    val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
   1.197 -      handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.198 -    val default' = default |> Sorts.norm_sort classes';
   1.199 -    val arities' = arities |> rebuild_arities pp classes';
   1.200 -  in (classes', default', types, arities') end);
   1.201 -
   1.202 -fun merge_classes pp CC = Graph.merge_trans_acyclic (op =) CC
   1.203 -  handle Graph.DUPS cs => err_dup_classes cs
   1.204 -    | Graph.CYCLES css => err_cyclic_classes pp css;
   1.205 +    val space = NameSpace.merge (space1, space2);
   1.206 +    val classes =
   1.207 +      Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.208 +        handle Graph.DUPS cs => err_dup_classes cs
   1.209 +          | Graph.CYCLES css => err_cyclic_classes pp css;
   1.210 +  in (space, classes) end;    
   1.211  
   1.212  end;
   1.213  
   1.214 +fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) =>
   1.215 +  ((fold (NameSpace.hide fully) cs space, classes), default, types, arities));
   1.216 +
   1.217  
   1.218  (* default sort *)
   1.219  
   1.220 -fun set_defsort S tsig = tsig |> change_tsig (fn (classes, _, types, arities) =>
   1.221 +fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) =>
   1.222    (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
   1.223  
   1.224  
   1.225 @@ -531,14 +543,19 @@
   1.226      else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   1.227    end;
   1.228  
   1.229 -fun new_decl (c, decl) types =
   1.230 -  (case Symtab.lookup (types, c) of
   1.231 -    SOME (decl', _) => err_in_decls c decl decl'
   1.232 -  | NONE => Symtab.update ((c, (decl, stamp ())), types));
   1.233 +fun new_decl naming (c, decl) (space, types) =
   1.234 +  let
   1.235 +    val c' = NameSpace.full naming c;
   1.236 +    val space' = NameSpace.declare naming c' space;
   1.237 +    val types' =
   1.238 +      (case Symtab.lookup (types, c') of
   1.239 +        SOME (decl', _) => err_in_decls c' decl decl'
   1.240 +      | NONE => Symtab.update ((c', (decl, stamp ())), types));
   1.241 +  in (space', types') end;
   1.242  
   1.243 -fun the_decl types c = fst (the (Symtab.lookup (types, c)));
   1.244 +fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c)));
   1.245  
   1.246 -fun change_types f = change_tsig (fn (classes, default, types, arities) =>
   1.247 +fun change_types f = map_tsig (fn (classes, default, types, arities) =>
   1.248    (classes, default, f types, arities));
   1.249  
   1.250  fun syntactic types (Type (c, Ts)) =
   1.251 @@ -546,7 +563,7 @@
   1.252          orelse exists (syntactic types) Ts
   1.253    | syntactic _ _ = false;
   1.254  
   1.255 -fun add_abbrev (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   1.256 +fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   1.257    let
   1.258      fun err msg =
   1.259        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   1.260 @@ -559,23 +576,27 @@
   1.261      (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
   1.262        [] => []
   1.263      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   1.264 -    types |> new_decl (a, Abbreviation (vs, rhs', syntactic types rhs'))
   1.265 +    types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   1.266    end);
   1.267  
   1.268  in
   1.269  
   1.270 -fun add_types ps = change_types (fold new_decl (ps |> map (fn (c, n) =>
   1.271 +fun add_types naming ps = change_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
   1.272    if n < 0 then err_neg_args c else (c, LogicalType n))));
   1.273  
   1.274 -val add_abbrevs = fold add_abbrev;
   1.275 -val add_nonterminals = change_types o fold new_decl o map (rpair Nonterminal);
   1.276 +val add_abbrevs = fold o add_abbrev;
   1.277 +
   1.278 +fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
   1.279  
   1.280  fun merge_types (types1, types2) =
   1.281 -  Symtab.merge Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
   1.282 +  NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
   1.283      err_in_decls d (the_decl types1 d) (the_decl types2 d);
   1.284  
   1.285  end;
   1.286  
   1.287 +fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) =>
   1.288 +  (classes, default, (fold (NameSpace.hide fully) cs space, types), arities));
   1.289 +
   1.290  
   1.291  (* merge type signatures *)
   1.292  
   1.293 @@ -587,9 +608,9 @@
   1.294        log_types = _, witness = _}) = tsig2;
   1.295  
   1.296      val classes' = merge_classes pp (classes1, classes2);
   1.297 -    val default' = Sorts.inter_sort classes' (default1, default2);
   1.298 +    val default' = Sorts.inter_sort (#2 classes') (default1, default2);
   1.299      val types' = merge_types (types1, types2);
   1.300 -    val arities' = merge_arities pp classes' (arities1, arities2);
   1.301 +    val arities' = merge_arities pp (#2 classes') (arities1, arities2);
   1.302    in build_tsig (classes', default', types', arities') end;
   1.303  
   1.304  end;