src/Pure/sign.ML
changeset 3867 3b2587c809f4
parent 3855 4bdf32173f6f
child 3877 83c5310aaaab
     1.1 --- a/src/Pure/sign.ML	Tue Oct 14 17:35:56 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 14 17:36:22 1997 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4      syn: Syntax.syntax,
     1.5      path: string list,
     1.6      spaces: (string * NameSpace.T) list,
     1.7 +    data: Data.T,
     1.8      stamps: string ref list}
     1.9    val subsig: sg * sg -> bool
    1.10    val eq_sg: sg * sg -> bool
    1.11 @@ -102,6 +103,10 @@
    1.12    val add_space: string * string list -> sg -> sg
    1.13    val add_name: string -> sg -> sg
    1.14    val make_draft: sg -> sg
    1.15 +  val print_data: sg -> unit
    1.16 +  val init_data: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T) -> sg -> sg
    1.17 +  val get_data: sg -> string -> exn
    1.18 +  val put_data: string * exn -> sg -> sg
    1.19    val merge: sg * sg -> sg
    1.20    val proto_pure: sg
    1.21    val pure: sg
    1.22 @@ -122,10 +127,10 @@
    1.23      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    1.24      path: string list,                     	(*current name space entry prefix*)
    1.25      spaces: (string * NameSpace.T) list,   	(*name spaces for consts, types etc.*)
    1.26 +    data: Data.T,				(*additional data*)
    1.27      stamps: string ref list};                   (*unique theory indentifier*)
    1.28 -
    1.29 -    (*the "ref" in stamps ensures that no two signatures are identical
    1.30 -      -- it is impossible to forge a signature*)
    1.31 +      (*the "ref" in stamps ensures that no two signatures are identical
    1.32 +        -- it is impossible to forge a signature*)
    1.33  
    1.34  fun rep_sg (Sg args) = args;
    1.35  val tsig_of = #tsig o rep_sg;
    1.36 @@ -351,7 +356,7 @@
    1.37      fun pretty_const (c, ty) = Pretty.block
    1.38        [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
    1.39  
    1.40 -    val Sg {tsig, const_tab, syn = _, path, spaces, stamps} = sg;
    1.41 +    val Sg {tsig, const_tab, syn = _, path, spaces, data = _, stamps} = sg;
    1.42      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
    1.43      val {classes, classrel, default, tycons, abbrs, arities} =
    1.44        Type.rep_tsig tsig;
    1.45 @@ -752,12 +757,13 @@
    1.46      else ref name :: stmps
    1.47    end;
    1.48  
    1.49 -fun make_sign (syn, tsig, ctab, (path, spaces)) stamps name =
    1.50 +fun make_sign (syn, tsig, ctab, (path, spaces)) data stamps name =
    1.51    Sg {tsig = tsig, const_tab = ctab, syn = syn, path = path, spaces = spaces,
    1.52 -    stamps = ext_stamps stamps name};
    1.53 +    data = data, stamps = ext_stamps stamps name};
    1.54  
    1.55 -fun extend_sign extfun name decls (Sg {tsig, const_tab, syn, path, spaces, stamps}) =
    1.56 -  make_sign (extfun (syn, tsig, const_tab, (path, spaces)) decls) stamps name;
    1.57 +fun extend_sign extfun name decls
    1.58 +    (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
    1.59 +  make_sign (extfun (syn, tsig, const_tab, (path, spaces)) decls) data stamps name;
    1.60  
    1.61  
    1.62  (* the external interfaces *)
    1.63 @@ -791,6 +797,18 @@
    1.64  val make_draft = add_name "#";
    1.65  
    1.66  
    1.67 +(* additional signature data *)
    1.68 +
    1.69 +fun print_data (Sg {data, ...}) = Data.print data;
    1.70 +fun get_data (Sg {data, ...}) = Data.get data;
    1.71 +
    1.72 +fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
    1.73 +  make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
    1.74 +
    1.75 +fun init_data (kind, e, mrg, prt) = map_data (fn d => Data.init d kind e mrg prt);
    1.76 +fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
    1.77 +
    1.78 +
    1.79  
    1.80  (** merge signatures **)    (*exception TERM*)
    1.81  
    1.82 @@ -805,9 +823,9 @@
    1.83      (*neither is union already; must form union*)
    1.84      let
    1.85        val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
    1.86 -        path = _, spaces = spaces1, stamps = stamps1} = sg1;
    1.87 +        path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1;
    1.88        val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
    1.89 -        path = _, spaces = spaces2, stamps = stamps2} = sg2;
    1.90 +        path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2;
    1.91  
    1.92  
    1.93        val stamps = merge_rev_lists stamps1 stamps2;
    1.94 @@ -830,9 +848,11 @@
    1.95          kinds ~~
    1.96            ListPair.map NameSpace.merge
    1.97              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
    1.98 +
    1.99 +      val data = Data.merge (data1, data2);
   1.100      in
   1.101        Sg {tsig = tsig, const_tab = const_tab, syn = syn,
   1.102 -        path = [], spaces = spaces, stamps = stamps}
   1.103 +        path = [], spaces = spaces, data = data, stamps = stamps}
   1.104      end;
   1.105  
   1.106  fun merge sgs =
   1.107 @@ -845,7 +865,7 @@
   1.108  (** the Pure signature **)
   1.109  
   1.110  val proto_pure =
   1.111 -  make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], [])) [] "#"
   1.112 +  make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], [])) Data.empty [] "#"
   1.113    |> add_types
   1.114     (("fun", 2, NoSyn) ::
   1.115      ("prop", 0, NoSyn) ::