src/Pure/type.ML
changeset 27302 8d12ac6a3e1c
parent 27273 d54ae0bdad80
child 27313 07754b7ba89d
     1.1 --- a/src/Pure/type.ML	Fri Jun 20 21:00:25 2008 +0200
     1.2 +++ b/src/Pure/type.ML	Fri Jun 20 21:00:26 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val rep_tsig: tsig ->
     1.5     {classes: NameSpace.T * Sorts.algebra,
     1.6      default: sort,
     1.7 -    types: (decl * serial) NameSpace.table,
     1.8 +    types: ((decl * Markup.property list) * serial) NameSpace.table,
     1.9      log_types: string list}
    1.10    val empty_tsig: tsig
    1.11    val defaultS: tsig -> sort
    1.12 @@ -40,6 +40,7 @@
    1.13    val cert_typ: tsig -> typ -> typ
    1.14    val arity_number: tsig -> string -> int
    1.15    val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
    1.16 +  val the_tags: tsig -> string -> Markup.property list
    1.17  
    1.18    (*special treatment of type vars*)
    1.19    val strip_sorts: typ -> typ
    1.20 @@ -72,9 +73,9 @@
    1.21    val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
    1.22    val hide_class: bool -> string -> tsig -> tsig
    1.23    val set_defsort: sort -> tsig -> tsig
    1.24 -  val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
    1.25 -  val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
    1.26 -  val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
    1.27 +  val add_type: NameSpace.naming -> Markup.property list -> bstring * int -> tsig -> tsig
    1.28 +  val add_abbrev: NameSpace.naming -> Markup.property list -> string * string list * typ -> tsig -> tsig
    1.29 +  val add_nonterminal: NameSpace.naming -> Markup.property list -> string -> tsig -> tsig
    1.30    val hide_type: bool -> string -> tsig -> tsig
    1.31    val add_arity: Pretty.pp -> arity -> tsig -> tsig
    1.32    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
    1.33 @@ -104,7 +105,7 @@
    1.34    TSig of {
    1.35      classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    1.36      default: sort,                          (*default sort on input*)
    1.37 -    types: (decl * serial) NameSpace.table, (*declared types*)
    1.38 +    types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*)
    1.39      log_types: string list};                (*logical types sorted by number of arguments*)
    1.40  
    1.41  fun rep_tsig (TSig comps) = comps;
    1.42 @@ -115,7 +116,7 @@
    1.43  fun build_tsig ((space, classes), default, types) =
    1.44    let
    1.45      val log_types =
    1.46 -      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
    1.47 +      Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) []
    1.48        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
    1.49    in make_tsig ((space, classes), default, types, log_types) end;
    1.50  
    1.51 @@ -125,6 +126,10 @@
    1.52  val empty_tsig =
    1.53    build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
    1.54  
    1.55 +fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
    1.56 +
    1.57 +fun the_tags tsig = snd o the o lookup_type tsig;
    1.58 +
    1.59  
    1.60  (* classes and sorts *)
    1.61  
    1.62 @@ -177,7 +182,6 @@
    1.63  
    1.64  fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
    1.65    let
    1.66 -    val TSig {types = (_, types), ...} = tsig;
    1.67      fun err msg = raise TYPE (msg, [ty], []);
    1.68  
    1.69      val check_logical =
    1.70 @@ -189,7 +193,7 @@
    1.71              val Ts' = map cert Ts;
    1.72              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    1.73            in
    1.74 -            (case Symtab.lookup types c of
    1.75 +            (case lookup_type tsig c of
    1.76                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.77              | SOME (Abbreviation (vs, U, syn), _) =>
    1.78                 (nargs (length vs);
    1.79 @@ -215,8 +219,8 @@
    1.80  
    1.81  (* type arities *)
    1.82  
    1.83 -fun arity_number (TSig {types = (_, types), ...}) a =
    1.84 -  (case Symtab.lookup types a of
    1.85 +fun arity_number tsig a =
    1.86 +  (case lookup_type tsig a of
    1.87      SOME (LogicalType n, _) => n
    1.88    | _ => error (undecl_type a));
    1.89  
    1.90 @@ -514,7 +518,7 @@
    1.91  fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
    1.92    let
    1.93      val _ =
    1.94 -      (case Symtab.lookup (#2 types) t of
    1.95 +      (case lookup_type tsig t of
    1.96          SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
    1.97        | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
    1.98        | NONE => error (undecl_type t));
    1.99 @@ -554,17 +558,17 @@
   1.100      else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   1.101    end;
   1.102  
   1.103 -fun new_decl naming (c, decl) (space, types) =
   1.104 +fun new_decl naming tags (c, decl) (space, types) =
   1.105    let
   1.106      val c' = NameSpace.full naming c;
   1.107      val space' = NameSpace.declare naming c' space;
   1.108      val types' =
   1.109        (case Symtab.lookup types c' of
   1.110 -        SOME (decl', _) => err_in_decls c' decl decl'
   1.111 -      | NONE => Symtab.update (c', (decl, serial ())) types);
   1.112 +        SOME ((decl', _), _) => err_in_decls c' decl decl'
   1.113 +      | NONE => Symtab.update (c', ((decl, tags), serial ())) types);
   1.114    in (space', types') end;
   1.115  
   1.116 -fun the_decl (_, types) = fst o the o Symtab.lookup types;
   1.117 +fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;
   1.118  
   1.119  fun map_types f = map_tsig (fn (classes, default, types) =>
   1.120    let
   1.121 @@ -574,11 +578,16 @@
   1.122    in (classes, default, (space', tab')) end);
   1.123  
   1.124  fun syntactic types (Type (c, Ts)) =
   1.125 -      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
   1.126 +      (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false)
   1.127          orelse exists (syntactic types) Ts
   1.128    | syntactic _ _ = false;
   1.129  
   1.130 -fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   1.131 +in
   1.132 +
   1.133 +fun add_type naming tags (c, n) = if n < 0 then err_neg_args c else
   1.134 +  map_types (new_decl naming tags (c, LogicalType n));
   1.135 +
   1.136 +fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   1.137    let
   1.138      fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
   1.139      val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
   1.140 @@ -590,17 +599,10 @@
   1.141      (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
   1.142        [] => []
   1.143      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   1.144 -    types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   1.145 +    types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   1.146    end);
   1.147  
   1.148 -in
   1.149 -
   1.150 -fun add_types naming ps = map_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
   1.151 -  if n < 0 then err_neg_args c else (c, LogicalType n))));
   1.152 -
   1.153 -val add_abbrevs = fold o add_abbrev;
   1.154 -
   1.155 -fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal);
   1.156 +fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
   1.157  
   1.158  fun merge_types (types1, types2) =
   1.159    NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)