major cleanup;
authorwenzelm
Thu Feb 03 13:53:44 1994 +0100 (1994-02-03)
changeset 251c9b984c0a674
parent 250 9b5a069285ce
child 252 7532f95d7f44
major cleanup;
added eq_sig;
added print_sg (full contents), pprint_sg (stamps only);
added certify_typ, certify_term;
changed read_typ: result now certified;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Feb 03 13:53:08 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 03 13:53:44 1994 +0100
     1.3 @@ -1,236 +1,317 @@
     1.4  (*  Title:      Pure/sign.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 +    Author:     Lawrence C Paulson and Markus Wenzel
     1.9  
    1.10 -The abstract types "sg" of signatures
    1.11 +The abstract type "sg" of signatures.
    1.12 +
    1.13 +TODO:
    1.14 +  a clean modular sequential Sign.extend (using sg_ext list);
    1.15  *)
    1.16  
    1.17  signature SIGN =
    1.18  sig
    1.19 -  structure Type: TYPE
    1.20    structure Symtab: SYMTAB
    1.21    structure Syntax: SYNTAX
    1.22 +  structure Type: TYPE
    1.23    sharing Symtab = Type.Symtab
    1.24 -  type sg
    1.25 -  val extend: sg -> string ->
    1.26 -        (class * class list) list * class list *
    1.27 -        (string list * int) list *
    1.28 -        (string * indexname list * string) list *
    1.29 -        (string list * (sort list * class)) list *
    1.30 -        (string list * string)list * Syntax.sext option -> sg
    1.31 -  val merge: sg * sg -> sg
    1.32 -  val pure: sg
    1.33 -  val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.34 -  val rep_sg: sg -> {tsig: Type.type_sig,
    1.35 -                     const_tab: typ Symtab.table,
    1.36 -                     syn: Syntax.syntax,
    1.37 -                     stamps: string ref list}
    1.38 -  val string_of_term: sg -> term -> string
    1.39 -  val string_of_typ: sg -> typ -> string
    1.40 -  val subsig: sg * sg -> bool
    1.41 -  val pprint_term: sg -> term -> pprint_args -> unit
    1.42 -  val pprint_typ: sg -> typ -> pprint_args -> unit
    1.43 -  val pretty_term: sg -> term -> Syntax.Pretty.T
    1.44 -  val term_errors: sg -> term -> string list
    1.45 +  local open Type in
    1.46 +    type sg
    1.47 +    val rep_sg: sg ->
    1.48 +      {tsig: type_sig,
    1.49 +       const_tab: typ Symtab.table,
    1.50 +       syn: Syntax.syntax,
    1.51 +       stamps: string ref list}
    1.52 +    val subsig: sg * sg -> bool
    1.53 +    val eq_sg: sg * sg -> bool
    1.54 +    val print_sg: sg -> unit
    1.55 +    val pprint_sg: sg -> pprint_args -> unit
    1.56 +    val pretty_term: sg -> term -> Syntax.Pretty.T
    1.57 +    val pretty_typ: sg -> typ -> Syntax.Pretty.T
    1.58 +    val string_of_term: sg -> term -> string
    1.59 +    val string_of_typ: sg -> typ -> string
    1.60 +    val pprint_term: sg -> term -> pprint_args -> unit
    1.61 +    val pprint_typ: sg -> typ -> pprint_args -> unit
    1.62 +    val certify_typ: sg -> typ -> typ
    1.63 +    val certify_term: sg -> term -> term * typ * int
    1.64 +    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.65 +    val extend: sg -> string ->
    1.66 +      (class * class list) list * class list *
    1.67 +      (string list * int) list *
    1.68 +      (string * string list * string) list *
    1.69 +      (string list * (sort list * class)) list *
    1.70 +      (string list * string) list * Syntax.sext option -> sg
    1.71 +    val merge: sg * sg -> sg
    1.72 +    val pure: sg
    1.73 +  end
    1.74  end;
    1.75  
    1.76 -functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    1.77 +functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
    1.78  struct
    1.79  
    1.80 -structure Type = Type;
    1.81  structure Symtab = Type.Symtab;
    1.82  structure Syntax = Syntax;
    1.83 -structure Pretty = Syntax.Pretty
    1.84 +structure Pretty = Syntax.Pretty;
    1.85 +structure Type = Type;
    1.86 +open Type;
    1.87  
    1.88  
    1.89 -(* Signatures of theories. *)
    1.90 +(** datatype sg **)
    1.91 +
    1.92 +(*the "ref" in stamps ensures that no two signatures are identical -- it is
    1.93 +  impossible to forge a signature*)
    1.94  
    1.95  datatype sg =
    1.96    Sg of {
    1.97 -    tsig: Type.type_sig,            (*order-sorted signature of types*)
    1.98 +    tsig: type_sig,                 (*order-sorted signature of types*)
    1.99      const_tab: typ Symtab.table,    (*types of constants*)
   1.100      syn: Syntax.syntax,             (*syntax for parsing and printing*)
   1.101      stamps: string ref list};       (*unique theory indentifier*)
   1.102  
   1.103 -
   1.104  fun rep_sg (Sg args) = args;
   1.105  
   1.106 -fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
   1.107  
   1.108 -fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
   1.109 +fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
   1.110  
   1.111 -fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
   1.112 +fun eq_sg (sg1, sg2) = subsig (sg1, sg2) andalso subsig (sg2, sg1);
   1.113  
   1.114 -(*Is constant present in table with more generic type?*)
   1.115 -fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
   1.116 -        Some U => Type.typ_instance(tsig,T,U) | _ => false;
   1.117  
   1.118  
   1.119 -(*Check a term for errors.  Are all constants and types valid in signature?
   1.120 -  Does not check that term is well-typed!*)
   1.121 -fun term_errors (sign as Sg{tsig,const_tab,...}) =
   1.122 -  let val showtyp = string_of_typ sign
   1.123 -      fun terrs (Const (a,T), errs) =
   1.124 -	  if valid_const tsig const_tab (a,T)
   1.125 -	  then Type.type_errors tsig (T,errs)
   1.126 -	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
   1.127 -	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
   1.128 -	| terrs (Var  ((a,i),T), errs) =
   1.129 -	  if  i>=0  then  Type.type_errors tsig (T,errs)
   1.130 -	  else  ("Negative index for Var: " ^ a) :: errs
   1.131 -	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
   1.132 -	| terrs (Abs (_,T,t), errs) =
   1.133 -	      Type.type_errors tsig (T,terrs(t,errs))
   1.134 -	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
   1.135 -  in  fn t => terrs(t,[])  end;
   1.136 +(** print signature **)
   1.137 +
   1.138 +fun print_sg sg =
   1.139 +  let
   1.140 +    fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
   1.141 +
   1.142 +    fun pretty_sort [cl] = Pretty.str cl
   1.143 +      | pretty_sort cls = Pretty.str_list "{" "}" cls;
   1.144 +
   1.145 +    fun pretty_subclass (cl, cls) = Pretty.block
   1.146 +      [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
   1.147 +
   1.148 +    fun pretty_default cls = Pretty.block
   1.149 +      [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
   1.150 +
   1.151 +    fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
   1.152 +
   1.153 +    fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
   1.154 +      [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
   1.155 +        Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
   1.156 +
   1.157 +    fun pretty_arity ty (cl, []) = Pretty.block
   1.158 +          [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl]
   1.159 +      | pretty_arity ty (cl, srts) = Pretty.block
   1.160 +          [Pretty.str (ty ^ " ::"), Pretty.brk 1,
   1.161 +            Pretty.list "(" ")" (map pretty_sort srts),
   1.162 +            Pretty.brk 1, Pretty.str cl];
   1.163 +
   1.164 +    fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
   1.165 +
   1.166 +    fun pretty_const syn (c, ty) = Pretty.block
   1.167 +      [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   1.168 +
   1.169 +
   1.170 +    val Sg {tsig, const_tab, syn, stamps} = sg;
   1.171 +    val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig;
   1.172 +  in
   1.173 +    Pretty.writeln (Pretty.strs ("stamps:" :: map ! stamps));
   1.174 +    Pretty.writeln (Pretty.strs ("classes:" :: classes));
   1.175 +    Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass));
   1.176 +    Pretty.writeln (pretty_default default);
   1.177 +    Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args));
   1.178 +    Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   1.179 +    Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg)));
   1.180 +    Pretty.writeln (Pretty.big_list "consts:"
   1.181 +      (map (pretty_const syn) (Symtab.alist_of const_tab)))
   1.182 +  end;
   1.183 +
   1.184 +
   1.185 +fun pprint_sg (Sg {stamps, ...}) =
   1.186 +  Pretty.pprint (Pretty.str_list "{" "}" (map ! stamps));
   1.187 +
   1.188 +
   1.189 +
   1.190 +(** pretty printing of terms and types **)
   1.191 +
   1.192 +fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
   1.193 +fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
   1.194 +
   1.195 +fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
   1.196 +fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
   1.197 +
   1.198 +fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   1.199 +fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   1.200  
   1.201  
   1.202  
   1.203 -(** The Extend operation **)
   1.204 +(** certify types and terms **)
   1.205 +
   1.206 +(*errors are indicated by exception TYPE*)
   1.207 +
   1.208 +fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   1.209 +
   1.210 +
   1.211 +(* FIXME -> term.ML (?) *)
   1.212 +fun mapfilter_atoms f (Abs (_, _, t)) = mapfilter_atoms f t
   1.213 +  | mapfilter_atoms f (t $ u) = mapfilter_atoms f t @ mapfilter_atoms f u
   1.214 +  | mapfilter_atoms f a = (case f a of Some y => [y] | None => []);
   1.215  
   1.216 -(* Extend a signature: may add classes, types and constants. The "ref" in
   1.217 -   stamps ensures that no two signatures are identical -- it is impossible to
   1.218 -   forge a signature. *)
   1.219 +fun certify_term (sg as Sg {tsig, const_tab, ...}) tm =
   1.220 +  let
   1.221 +    fun valid_const a T =
   1.222 +      (case Symtab.lookup (const_tab, a) of
   1.223 +        Some U => typ_instance (tsig, T, U)
   1.224 +      | _ => false);
   1.225  
   1.226 -fun extend (Sg {tsig, const_tab, syn, stamps}) name
   1.227 -  (classes, default, types, abbr, arities, const_decs, opt_sext) =
   1.228 -  let
   1.229 -    fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
   1.230 +    fun atom_err (Const (a, T)) =
   1.231 +          if valid_const a T then None
   1.232 +          else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   1.233 +            quote (string_of_typ sg T))
   1.234 +      | atom_err (Var ((x, i), _)) =
   1.235 +          if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   1.236 +      | atom_err _ = None;
   1.237 +
   1.238  
   1.239 -    fun read_typ tsg sy s =
   1.240 -      Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
   1.241 +    val norm_tm =
   1.242 +      (case it_term_types (typ_errors tsig) (tm, []) of
   1.243 +        [] => map_term_types (norm_typ tsig) tm
   1.244 +      | errs => raise_type (cat_lines errs) [] [tm]);
   1.245 +  in
   1.246 +    (case mapfilter_atoms atom_err norm_tm of
   1.247 +      [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   1.248 +    | errs => raise_type (cat_lines errs) [] [norm_tm])
   1.249 +  end;
   1.250 +
   1.251 +
   1.252 +
   1.253 +(** read types **)
   1.254 +
   1.255 +(*read and certify typ wrt a signature; errors are indicated by
   1.256 +  exception ERROR (with messages already printed)*)
   1.257  
   1.258 -    fun check_typ tsg sy ty =
   1.259 -      (case Type.type_errors tsg (ty, []) of
   1.260 -        [] => ty
   1.261 -      | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
   1.262 +fun rd_typ tsig syn sort_of s =
   1.263 +  let
   1.264 +    val def_sort = defaultS tsig;
   1.265 +    val raw_ty =        (*this may raise ERROR, too!*)
   1.266 +      Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s;
   1.267 +  in
   1.268 +    cert_typ tsig raw_ty
   1.269 +      handle TYPE (msg, _, _) => error msg
   1.270 +  end
   1.271 +  handle ERROR => error ("The error(s) above occurred in type " ^ quote s);
   1.272  
   1.273 -    (*reset TVar indices to zero, renaming to preserve distinctness*)
   1.274 -    fun zero_tvar_indices T =
   1.275 +fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s;
   1.276 +
   1.277 +
   1.278 +
   1.279 +(** extend signature **)
   1.280 +
   1.281 +(*errors are indicated by exception ERROR (with messages already printed)*)
   1.282 +
   1.283 +fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
   1.284 +  let
   1.285 +    (*reset TVar indices to 0, renaming to preserve distinctness*)
   1.286 +    fun zero_tvar_idxs T =
   1.287        let
   1.288          val inxSs = typ_tvars T;
   1.289          val nms' = variantlist (map (#1 o #1) inxSs, []);
   1.290 -        val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
   1.291 -      in typ_subst_TVars tye T end;
   1.292 +        val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms');
   1.293 +      in
   1.294 +        typ_subst_TVars tye T
   1.295 +      end;
   1.296  
   1.297      (*read and check the type mentioned in a const declaration; zero type var
   1.298        indices because type inference requires it*)
   1.299 +    fun read_const tsig syn (c, s) =
   1.300 +      (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
   1.301 +        handle ERROR => error ("in declaration of constant " ^ quote c);
   1.302  
   1.303 -    fun read_consts tsg sy (cs, s) =
   1.304 -      let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
   1.305 -      in
   1.306 -        (case Type.type_errors tsg (ty, []) of
   1.307 -          [] => (cs, ty)
   1.308 -        | errs => error (cat_lines (("Error in type of constants " ^
   1.309 -            space_implode " " (map quote cs)) :: errs)))
   1.310 -      end;
   1.311 +    fun read_abbr tsig syn (c, vs, rhs_src) =
   1.312 +      (c, (map (rpair 0) vs, varifyT (rd_typ tsig syn (K None) rhs_src)
   1.313 +        handle ERROR => error ("in type abbreviation " ^ quote c)));
   1.314 +
   1.315  
   1.316 -    val tsig' = Type.extend (tsig, classes, default, types, arities);
   1.317 +    val Sg {tsig, const_tab, syn, stamps} = sg;
   1.318 +    val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
   1.319 +      flat (map #1 consts);
   1.320 +    val sext = if_none opt_sext Syntax.empty_sext;
   1.321  
   1.322 -    fun read_typ_abbr(a,v,s)=
   1.323 -      let val T = Type.varifyT(read_typ tsig' syn s)
   1.324 -      in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
   1.325 +    val tsig' = extend_tsig tsig (classes, default, types, arities);
   1.326 +    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr tsig' syn) abbrs);
   1.327  
   1.328 -    val abbr' = map read_typ_abbr abbr;
   1.329 -    val tsig'' = Type.add_abbrs(tsig',abbr');
   1.330 +    val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
   1.331 +      (logical_types tsig1, xconsts, sext);
   1.332  
   1.333 -    val read_ty =
   1.334 -      (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
   1.335 -    val log_types = Type.logical_types tsig'';
   1.336 -    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
   1.337 -    val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
   1.338 +    val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   1.339 +      (Syntax.constants sext @ consts));
   1.340  
   1.341 -    val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
   1.342 +    val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
   1.343 +      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
   1.344 +        handle Symtab.DUPLICATE c
   1.345 +          => error ("Constant " ^ quote c ^ " declared twice");
   1.346  
   1.347 -    val const_decs' =
   1.348 -      map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
   1.349 +    val stamps1 =
   1.350 +      if exists (equal name o !) stamps then
   1.351 +        error ("Theory already contains a " ^ quote name ^ " component")
   1.352 +      else stamps @ [ref name];
   1.353    in
   1.354 -    Sg {
   1.355 -      tsig = tsig'',
   1.356 -      const_tab = Symtab.st_of_declist (const_decs', const_tab)
   1.357 -        handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   1.358 -      syn = syn',
   1.359 -      stamps = ref name :: stamps}
   1.360 +    Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1}
   1.361    end;
   1.362  
   1.363  
   1.364 -(* The empty signature *)
   1.365 +
   1.366 +(** merge signatures **)
   1.367 +
   1.368 +(*errors are indicated by exception TERM*)
   1.369  
   1.370 -val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
   1.371 -  syn = Syntax.type_syn, stamps = []};
   1.372 -
   1.373 -
   1.374 -(* The pure signature *)
   1.375 +fun check_stamps stamps =
   1.376 +  (case duplicates (map ! stamps) of
   1.377 +    [] => stamps
   1.378 +  | dups => raise_term ("Attempt to merge different versions of theories " ^
   1.379 +      commas (map quote dups)) []);
   1.380  
   1.381 -val pure = extend sg0 "Pure"
   1.382 -([("logic", [])],
   1.383 - ["logic"],
   1.384 - [(["fun"], 2),
   1.385 -  (["prop"], 0),
   1.386 -  (Syntax.syntax_types, 0)],
   1.387 - [],
   1.388 - [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.389 -  (["prop"], ([], "logic"))],
   1.390 - [([Syntax.constrainC], "'a::logic => 'a")],
   1.391 - Some Syntax.pure_sext);
   1.392 +fun merge (sg1, sg2) =
   1.393 +  if subsig (sg2, sg1) then sg1
   1.394 +  else if subsig (sg1, sg2) then sg2
   1.395 +  else
   1.396 +    (*neither is union already; must form union*)
   1.397 +    let
   1.398 +      val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.399 +        stamps = stamps1} = sg1;
   1.400 +      val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.401 +        stamps = stamps2} = sg2;
   1.402 +
   1.403 +      val tsig = merge_tsigs (tsig1, tsig2);
   1.404 +
   1.405 +      val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   1.406 +        handle Symtab.DUPLICATE c =>
   1.407 +          raise_term ("Incompatible types for constant " ^ quote c) [];
   1.408 +
   1.409 +      val syn = Syntax.merge (logical_types tsig) syn1 syn2;
   1.410 +
   1.411 +      val stamps = check_stamps (merge_lists stamps1 stamps2);
   1.412 +    in
   1.413 +      Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   1.414 +    end;
   1.415  
   1.416  
   1.417  
   1.418 -(** The Merge operation **)
   1.419 -
   1.420 -(*Update table with (a,x) providing any existing asgt to "a" equals x. *)
   1.421 -fun update_eq ((a,x),tab) =
   1.422 -    case Symtab.lookup(tab,a) of
   1.423 -        None => Symtab.update((a,x), tab)
   1.424 -      | Some y => if x=y then tab
   1.425 -            else  raise TERM ("Incompatible types for constant: "^a, []);
   1.426 +(** the Pure signature **)
   1.427  
   1.428 -(*Combine tables, updating tab2 by tab1 and checking.*)
   1.429 -fun merge_tabs (tab1,tab2) =
   1.430 -    Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
   1.431 -
   1.432 -(*Combine tables, overwriting tab2 with tab1.*)
   1.433 -fun smash_tabs (tab1,tab2) =
   1.434 -    Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
   1.435 -
   1.436 -(*Combine stamps, checking that theory names are disjoint. *)
   1.437 -fun merge_stamps (stamps1,stamps2) =
   1.438 -  let val stamps = stamps1 union stamps2 in
   1.439 -  case findrep (map ! stamps) of
   1.440 -     a::_ => error ("Attempt to merge different versions of theory: " ^ a)
   1.441 -   | [] => stamps
   1.442 -  end;
   1.443 +val sg0 = Sg {tsig = tsig0, const_tab = Symtab.null,
   1.444 +  syn = Syntax.type_syn, stamps = []};
   1.445  
   1.446 -(*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
   1.447 -fun merge
   1.448 -  (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
   1.449 -   sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
   1.450 -    if stamps2 subset stamps1 then sign1
   1.451 -    else if stamps1 subset stamps2 then sign2
   1.452 -    else (*neither is union already; must form union*)
   1.453 -      let val tsig = Type.merge (tsig1, tsig2);
   1.454 -      in
   1.455 -        Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
   1.456 -          stamps = merge_stamps (stamps1, stamps2),
   1.457 -          syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
   1.458 -      end;
   1.459 -
   1.460 +val pure = extend sg0 "Pure"
   1.461 +  ([("logic", [])],
   1.462 +   ["logic"],
   1.463 +   [(["fun"], 2),
   1.464 +    (["prop"], 0),
   1.465 +    (Syntax.syntax_types, 0)],
   1.466 +   [],
   1.467 +   [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.468 +    (["prop"], ([], "logic"))],
   1.469 +   ([Syntax.constrainC], "'a::{} => 'a") :: Syntax.syntax_consts,
   1.470 +   Some Syntax.pure_sext);
   1.471  
   1.472  
   1.473 -fun read_typ(Sg{tsig,syn,...}, defS) s =
   1.474 -    let val term = Syntax.read syn Syntax.typeT s;
   1.475 -        val S0 = Type.defaultS tsig;
   1.476 -        fun defS0 s = case defS s of Some S => S | None => S0;
   1.477 -    in Syntax.typ_of_term defS0 term end;
   1.478 -
   1.479 -(** pretty printing of terms **)
   1.480 -
   1.481 -fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
   1.482 -
   1.483 -fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
   1.484 -
   1.485 -fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
   1.486 -
   1.487  end;
   1.488