replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
authorwenzelm
Fri May 05 21:59:47 2006 +0200 (2006-05-05 ago)
changeset 19579b802d1804b77
parent 19578 f93b7637a5e6
child 19580 c878a09fb849
replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Fri May 05 21:59:46 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Fri May 05 21:59:47 2006 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
     1.5    | arity_sorts pp (TSig {classes, arities, ...}) a S =
     1.6        Sorts.mg_domain (#2 classes, arities) a S
     1.7 -        handle Sorts.DOMAIN d => Sorts.domain_error pp d;
     1.8 +        handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
     1.9  
    1.10  
    1.11  
    1.12 @@ -385,7 +385,7 @@
    1.13      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
    1.14  
    1.15      fun mg_domain a S =
    1.16 -      Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
    1.17 +      Sorts.mg_domain (classes, arities) a S handle Sorts.CLASS_ERROR _ => raise TUNIFY;
    1.18  
    1.19      fun meet (_, []) tye = tye
    1.20        | meet (TVar (xi, S'), S) tye =
    1.21 @@ -542,15 +542,18 @@
    1.22  
    1.23  fun the_decl (_, types) = fst o the o Symtab.lookup types;
    1.24  
    1.25 -fun change_types f = map_tsig (fn (classes, default, types, arities) =>
    1.26 -  (classes, default, f types, arities));
    1.27 +fun map_types f = map_tsig (fn (classes, default, types, arities) =>
    1.28 +  let
    1.29 +    val (space', tab') = f types;
    1.30 +    val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
    1.31 +  in (classes, default, (space', tab'), arities) end);
    1.32  
    1.33  fun syntactic types (Type (c, Ts)) =
    1.34        (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
    1.35          orelse exists (syntactic types) Ts
    1.36    | syntactic _ _ = false;
    1.37  
    1.38 -fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
    1.39 +fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
    1.40    let
    1.41      fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
    1.42      val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
    1.43 @@ -567,12 +570,12 @@
    1.44  
    1.45  in
    1.46  
    1.47 -fun add_types naming ps = change_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
    1.48 +fun add_types naming ps = map_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
    1.49    if n < 0 then err_neg_args c else (c, LogicalType n))));
    1.50  
    1.51  val add_abbrevs = fold o add_abbrev;
    1.52  
    1.53 -fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
    1.54 +fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal);
    1.55  
    1.56  fun merge_types (types1, types2) =
    1.57    NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>