type constructors now with markup
authorhaftmann
Fri Jun 20 21:00:26 2008 +0200 (2008-06-20)
changeset 273028d12ac6a3e1c
parent 27301 bf7d82193a2e
child 27303 d6fef33c5c69
type constructors now with markup
src/Pure/codegen.ML
src/Pure/display.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/codegen.ML	Fri Jun 20 21:00:25 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri Jun 20 21:00:26 2008 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4      val tc = Sign.intern_type thy s;
     1.5    in
     1.6      case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
     1.7 -      SOME (Type.LogicalType i, _) =>
     1.8 +      SOME ((Type.LogicalType i, _), _) =>
     1.9          if num_args_of (fst syn) > i then
    1.10            error ("More arguments than corresponding type constructor " ^ s)
    1.11          else (case AList.lookup (op =) types tc of
     2.1 --- a/src/Pure/display.ML	Fri Jun 20 21:00:25 2008 +0200
     2.2 +++ b/src/Pure/display.ML	Fri Jun 20 21:00:26 2008 +0200
     2.3 @@ -149,14 +149,14 @@
     2.4        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
     2.5  
     2.6      val tfrees = map (fn v => TFree (v, []));
     2.7 -    fun pretty_type syn (t, (Type.LogicalType n, _)) =
     2.8 +    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
     2.9            if syn then NONE
    2.10            else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
    2.11 -      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    2.12 +      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
    2.13            if syn <> syn' then NONE
    2.14            else SOME (Pretty.block
    2.15              [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    2.16 -      | pretty_type syn (t, (Type.Nonterminal, _)) =
    2.17 +      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
    2.18            if not syn then NONE
    2.19            else SOME (prt_typ (Type (t, [])));
    2.20  
     3.1 --- a/src/Pure/sign.ML	Fri Jun 20 21:00:25 2008 +0200
     3.2 +++ b/src/Pure/sign.ML	Fri Jun 20 21:00:26 2008 +0200
     3.3 @@ -439,7 +439,8 @@
     3.4    let
     3.5      val syn' = Syntax.update_type_gram types syn;
     3.6      val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
     3.7 -    val tsig' = Type.add_types naming decls tsig;
     3.8 +    val tags = [(Markup.theory_nameN, Context.theory_name thy)];
     3.9 +    val tsig' = fold (Type.add_type naming tags) decls tsig;
    3.10    in (naming, syn', tsig', consts) end);
    3.11  
    3.12  
    3.13 @@ -448,7 +449,7 @@
    3.14  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    3.15    let
    3.16      val syn' = Syntax.update_consts ns syn;
    3.17 -    val tsig' = Type.add_nonterminals naming ns tsig;
    3.18 +    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
    3.19    in (naming, syn', tsig', consts) end);
    3.20  
    3.21  
    3.22 @@ -462,7 +463,7 @@
    3.23        val a' = Syntax.type_name a mx;
    3.24        val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    3.25          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    3.26 -      val tsig' = Type.add_abbrevs naming [abbr] tsig;
    3.27 +      val tsig' = Type.add_abbrev naming [] abbr tsig;
    3.28      in (naming, syn', tsig', consts) end);
    3.29  
    3.30  val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
     4.1 --- a/src/Pure/type.ML	Fri Jun 20 21:00:25 2008 +0200
     4.2 +++ b/src/Pure/type.ML	Fri Jun 20 21:00:26 2008 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4    val rep_tsig: tsig ->
     4.5     {classes: NameSpace.T * Sorts.algebra,
     4.6      default: sort,
     4.7 -    types: (decl * serial) NameSpace.table,
     4.8 +    types: ((decl * Markup.property list) * serial) NameSpace.table,
     4.9      log_types: string list}
    4.10    val empty_tsig: tsig
    4.11    val defaultS: tsig -> sort
    4.12 @@ -40,6 +40,7 @@
    4.13    val cert_typ: tsig -> typ -> typ
    4.14    val arity_number: tsig -> string -> int
    4.15    val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
    4.16 +  val the_tags: tsig -> string -> Markup.property list
    4.17  
    4.18    (*special treatment of type vars*)
    4.19    val strip_sorts: typ -> typ
    4.20 @@ -72,9 +73,9 @@
    4.21    val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
    4.22    val hide_class: bool -> string -> tsig -> tsig
    4.23    val set_defsort: sort -> tsig -> tsig
    4.24 -  val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
    4.25 -  val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
    4.26 -  val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
    4.27 +  val add_type: NameSpace.naming -> Markup.property list -> bstring * int -> tsig -> tsig
    4.28 +  val add_abbrev: NameSpace.naming -> Markup.property list -> string * string list * typ -> tsig -> tsig
    4.29 +  val add_nonterminal: NameSpace.naming -> Markup.property list -> string -> tsig -> tsig
    4.30    val hide_type: bool -> string -> tsig -> tsig
    4.31    val add_arity: Pretty.pp -> arity -> tsig -> tsig
    4.32    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
    4.33 @@ -104,7 +105,7 @@
    4.34    TSig of {
    4.35      classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    4.36      default: sort,                          (*default sort on input*)
    4.37 -    types: (decl * serial) NameSpace.table, (*declared types*)
    4.38 +    types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*)
    4.39      log_types: string list};                (*logical types sorted by number of arguments*)
    4.40  
    4.41  fun rep_tsig (TSig comps) = comps;
    4.42 @@ -115,7 +116,7 @@
    4.43  fun build_tsig ((space, classes), default, types) =
    4.44    let
    4.45      val log_types =
    4.46 -      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
    4.47 +      Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) []
    4.48        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
    4.49    in make_tsig ((space, classes), default, types, log_types) end;
    4.50  
    4.51 @@ -125,6 +126,10 @@
    4.52  val empty_tsig =
    4.53    build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
    4.54  
    4.55 +fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
    4.56 +
    4.57 +fun the_tags tsig = snd o the o lookup_type tsig;
    4.58 +
    4.59  
    4.60  (* classes and sorts *)
    4.61  
    4.62 @@ -177,7 +182,6 @@
    4.63  
    4.64  fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
    4.65    let
    4.66 -    val TSig {types = (_, types), ...} = tsig;
    4.67      fun err msg = raise TYPE (msg, [ty], []);
    4.68  
    4.69      val check_logical =
    4.70 @@ -189,7 +193,7 @@
    4.71              val Ts' = map cert Ts;
    4.72              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    4.73            in
    4.74 -            (case Symtab.lookup types c of
    4.75 +            (case lookup_type tsig c of
    4.76                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
    4.77              | SOME (Abbreviation (vs, U, syn), _) =>
    4.78                 (nargs (length vs);
    4.79 @@ -215,8 +219,8 @@
    4.80  
    4.81  (* type arities *)
    4.82  
    4.83 -fun arity_number (TSig {types = (_, types), ...}) a =
    4.84 -  (case Symtab.lookup types a of
    4.85 +fun arity_number tsig a =
    4.86 +  (case lookup_type tsig a of
    4.87      SOME (LogicalType n, _) => n
    4.88    | _ => error (undecl_type a));
    4.89  
    4.90 @@ -514,7 +518,7 @@
    4.91  fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
    4.92    let
    4.93      val _ =
    4.94 -      (case Symtab.lookup (#2 types) t of
    4.95 +      (case lookup_type tsig t of
    4.96          SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
    4.97        | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
    4.98        | NONE => error (undecl_type t));
    4.99 @@ -554,17 +558,17 @@
   4.100      else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   4.101    end;
   4.102  
   4.103 -fun new_decl naming (c, decl) (space, types) =
   4.104 +fun new_decl naming tags (c, decl) (space, types) =
   4.105    let
   4.106      val c' = NameSpace.full naming c;
   4.107      val space' = NameSpace.declare naming c' space;
   4.108      val types' =
   4.109        (case Symtab.lookup types c' of
   4.110 -        SOME (decl', _) => err_in_decls c' decl decl'
   4.111 -      | NONE => Symtab.update (c', (decl, serial ())) types);
   4.112 +        SOME ((decl', _), _) => err_in_decls c' decl decl'
   4.113 +      | NONE => Symtab.update (c', ((decl, tags), serial ())) types);
   4.114    in (space', types') end;
   4.115  
   4.116 -fun the_decl (_, types) = fst o the o Symtab.lookup types;
   4.117 +fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;
   4.118  
   4.119  fun map_types f = map_tsig (fn (classes, default, types) =>
   4.120    let
   4.121 @@ -574,11 +578,16 @@
   4.122    in (classes, default, (space', tab')) end);
   4.123  
   4.124  fun syntactic types (Type (c, Ts)) =
   4.125 -      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
   4.126 +      (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false)
   4.127          orelse exists (syntactic types) Ts
   4.128    | syntactic _ _ = false;
   4.129  
   4.130 -fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   4.131 +in
   4.132 +
   4.133 +fun add_type naming tags (c, n) = if n < 0 then err_neg_args c else
   4.134 +  map_types (new_decl naming tags (c, LogicalType n));
   4.135 +
   4.136 +fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   4.137    let
   4.138      fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
   4.139      val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
   4.140 @@ -590,17 +599,10 @@
   4.141      (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
   4.142        [] => []
   4.143      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   4.144 -    types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   4.145 +    types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   4.146    end);
   4.147  
   4.148 -in
   4.149 -
   4.150 -fun add_types naming ps = map_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
   4.151 -  if n < 0 then err_neg_args c else (c, LogicalType n))));
   4.152 -
   4.153 -val add_abbrevs = fold o add_abbrev;
   4.154 -
   4.155 -fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal);
   4.156 +fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
   4.157  
   4.158  fun merge_types (types1, types2) =
   4.159    NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)