maintain tags (Markup.property list);
authorwenzelm
Sun Sep 30 16:20:34 2007 +0200 (2007-09-30 ago)
changeset 247722b838dfeca1e
parent 24771 6c7e94742afa
child 24773 ec3a04e6f1a9
maintain tags (Markup.property list);
tuned;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Sun Sep 30 16:20:33 2007 +0200
     1.2 +++ b/src/Pure/consts.ML	Sun Sep 30 16:20:34 2007 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val the_declaration: T -> string -> typ                           (*exception TYPE*)
     1.5    val is_monomorphic: T -> string -> bool                           (*exception TYPE*)
     1.6    val the_constraint: T -> string -> typ                            (*exception TYPE*)
     1.7 +  val the_tags: T -> string -> Markup.property list                 (*exception TYPE*)
     1.8    val space_of: T -> NameSpace.T
     1.9    val intern: T -> xstring -> string
    1.10    val extern: T -> string -> xstring
    1.11 @@ -28,9 +29,9 @@
    1.12    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    1.13    val typargs: T -> string * typ -> typ list
    1.14    val instance: T -> string * typ list -> typ
    1.15 -  val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T
    1.16 +  val declare: bool -> NameSpace.naming -> Markup.property list -> (bstring * typ) -> T -> T
    1.17    val constrain: string * typ option -> T -> T
    1.18 -  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
    1.19 +  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Markup.property list ->
    1.20      bstring * term -> T -> (term * term) * T
    1.21    val hide: bool -> string -> T -> T
    1.22    val empty: T
    1.23 @@ -49,9 +50,7 @@
    1.24    LogicalConst of int list list |      (*typargs positions*)
    1.25    Abbreviation of term * term * bool   (*rhs, normal rhs, force_expand*);
    1.26  
    1.27 -type decl =
    1.28 -  (typ * kind) *
    1.29 -  bool; (*authentic syntax*)
    1.30 +type decl = {T: typ, kind: kind, tags: Markup.property list, authentic: bool};
    1.31  
    1.32  datatype T = Consts of
    1.33   {decls: (decl * serial) NameSpace.table,
    1.34 @@ -77,7 +76,7 @@
    1.35  
    1.36  fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
    1.37   {constants = (space,
    1.38 -    Symtab.fold (fn (c, (((T, kind), _), _)) =>
    1.39 +    Symtab.fold (fn (c, ({T, kind, ...}, _)) =>
    1.40        Symtab.update (c, (T, dest_kind kind))) decls Symtab.empty),
    1.41    constraints = (space, constraints)};
    1.42  
    1.43 @@ -86,17 +85,17 @@
    1.44  
    1.45  fun the_const (Consts ({decls = (_, tab), ...}, _)) c =
    1.46    (case Symtab.lookup tab c of
    1.47 -    SOME decl => decl
    1.48 +    SOME (decl, _) => decl
    1.49    | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []));
    1.50  
    1.51  fun logical_const consts c =
    1.52 -  (case #1 (#1 (the_const consts c)) of
    1.53 -    (T, LogicalConst ps) => (T, ps)
    1.54 +  (case the_const consts c of
    1.55 +    {T, kind = LogicalConst ps, ...} => (T, ps)
    1.56    | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
    1.57  
    1.58  fun the_abbreviation consts c =
    1.59 -  (case #1 (#1 (the_const consts c)) of
    1.60 -    (T, Abbreviation (t, t', _)) => (T, (t, t'))
    1.61 +  (case the_const consts c of
    1.62 +    {T, kind = Abbreviation (t, t', _), ...} => (T, (t, t'))
    1.63    | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
    1.64  
    1.65  val the_declaration = #1 oo logical_const;
    1.66 @@ -106,7 +105,9 @@
    1.67  fun the_constraint (consts as Consts ({constraints, ...}, _)) c =
    1.68    (case Symtab.lookup constraints c of
    1.69      SOME T => T
    1.70 -  | NONE => #1 (#1 (#1 (the_const consts c))));
    1.71 +  | NONE => #T (the_const consts c));
    1.72 +
    1.73 +val the_tags = #tags oo the_const;
    1.74  
    1.75  
    1.76  (* name space and syntax *)
    1.77 @@ -118,12 +119,12 @@
    1.78  
    1.79  fun extern_early consts c =
    1.80    (case try (the_const consts) c of
    1.81 -    SOME ((_, true), _) => Syntax.constN ^ c
    1.82 +    SOME {authentic = true, ...} => Syntax.constN ^ c
    1.83    | _ => extern consts c);
    1.84  
    1.85  fun syntax consts (c, mx) =
    1.86    let
    1.87 -    val ((T, _), authentic) = #1 (the_const consts c) handle TYPE (msg, _, _) => error msg;
    1.88 +    val {T, authentic, ...} = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.89      val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
    1.90    in (c', T, mx) end;
    1.91  
    1.92 @@ -135,7 +136,7 @@
    1.93  fun read_const consts raw_c =
    1.94    let
    1.95      val c = intern consts raw_c;
    1.96 -    val (((T, _), _), _) = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.97 +    val {T, ...} = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.98    in Const (c, T) end;
    1.99  
   1.100  
   1.101 @@ -157,7 +158,7 @@
   1.102          | Const (c, T) =>
   1.103              let
   1.104                val T' = certT T;
   1.105 -              val (U, kind) = #1 (#1 (the_const consts c));
   1.106 +              val {T = U, kind, ...} = the_const consts c;
   1.107              in
   1.108                if not (Type.raw_instance (T', U)) then
   1.109                  err "Illegal type for constant" (c, T)
   1.110 @@ -213,7 +214,7 @@
   1.111  
   1.112  (* declarations *)
   1.113  
   1.114 -fun declare naming ((c, declT), authentic) = map_consts (fn (decls, constraints, rev_abbrevs) =>
   1.115 +fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
   1.116    let
   1.117      fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
   1.118        | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)
   1.119 @@ -221,8 +222,10 @@
   1.120      and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is
   1.121        | args_of_list [] _ _ = I;
   1.122      val decl =
   1.123 -      (((declT, LogicalConst (map #2 (rev (args_of declT [] [])))), authentic), serial ());
   1.124 -  in (extend_decls naming (c, decl) decls, constraints, rev_abbrevs) end);
   1.125 +      {T = declT, kind = LogicalConst (map #2 (rev (args_of declT [] []))),
   1.126 +        tags = tags, authentic = authentic};
   1.127 +    val decls' = decls |> extend_decls naming (c, (decl, serial ()));
   1.128 +  in (decls', constraints, rev_abbrevs) end);
   1.129  
   1.130  
   1.131  (* constraints *)
   1.132 @@ -256,7 +259,7 @@
   1.133  
   1.134  in
   1.135  
   1.136 -fun abbreviate pp tsig naming mode (c, raw_rhs) consts =
   1.137 +fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =
   1.138    let
   1.139      val cert_term = certify pp tsig false consts;
   1.140      val expand_term = certify pp tsig true consts;
   1.141 @@ -276,8 +279,10 @@
   1.142    in
   1.143      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
   1.144        let
   1.145 -        val decls' = decls |> extend_decls naming
   1.146 -          (c, (((T, Abbreviation (rhs, rhs', force_expand)), true), serial ()));
   1.147 +        val decl =
   1.148 +          {T = T, kind = Abbreviation (rhs, rhs', force_expand), tags = tags, authentic = true};
   1.149 +        val decls' = decls
   1.150 +          |> extend_decls naming (c, (decl, serial ()));
   1.151          val rev_abbrevs' = rev_abbrevs
   1.152            |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
   1.153        in (decls', constraints, rev_abbrevs') end)