src/Pure/sign.ML
changeset 3967 edd5ff9371f8
parent 3956 d59fe4579004
child 3969 9c742951a923
     1.1 --- a/src/Pure/sign.ML	Tue Oct 21 17:48:06 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 21 18:09:13 1997 +0200
     1.3 @@ -18,14 +18,20 @@
     1.4  signature SIGN =
     1.5  sig
     1.6    type sg
     1.7 +  type sg_ref
     1.8    val rep_sg: sg ->
     1.9 -   {tsig: Type.type_sig,
    1.10 +   {id: string ref,			(* FIXME hide!? *)
    1.11 +    self: sg_ref,
    1.12 +    tsig: Type.type_sig,
    1.13      const_tab: typ Symtab.table,
    1.14      syn: Syntax.syntax,
    1.15      path: string list,
    1.16      spaces: (string * NameSpace.T) list,
    1.17      data: Data.T,
    1.18 -    stamps: string ref list}
    1.19 +    stamps: string ref list}		(* FIXME hide!? *)
    1.20 +  val tsig_of: sg -> Type.type_sig
    1.21 +  val deref: sg_ref -> sg
    1.22 +  val self_ref: sg -> sg_ref
    1.23    val subsig: sg * sg -> bool
    1.24    val eq_sg: sg * sg -> bool
    1.25    val same_sg: sg * sg -> bool
    1.26 @@ -108,9 +114,9 @@
    1.27    val get_data: sg -> string -> exn
    1.28    val put_data: string * exn -> sg -> sg
    1.29    val print_data: sg -> string -> unit
    1.30 -  val prep_ext: sg -> sg
    1.31 +  val merge_refs: sg_ref * sg_ref -> sg_ref
    1.32 +  val make_draft: sg -> sg
    1.33    val merge: sg * sg -> sg
    1.34 -  val nontriv_merge: sg * sg -> sg
    1.35    val proto_pure: sg
    1.36    val pure: sg
    1.37    val cpure: sg
    1.38 @@ -121,22 +127,55 @@
    1.39  structure Sign : SIGN =
    1.40  struct
    1.41  
    1.42 +
    1.43  (** datatype sg **)
    1.44  
    1.45  datatype sg =
    1.46    Sg of {
    1.47 +    id: string ref,				(*id*)
    1.48 +    self: sg_ref,				(*mutable self reference*)
    1.49      tsig: Type.type_sig,                        (*order-sorted signature of types*)
    1.50      const_tab: typ Symtab.table,                (*type schemes of constants*)
    1.51      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    1.52      path: string list,                     	(*current name space entry prefix*)
    1.53      spaces: (string * NameSpace.T) list,   	(*name spaces for consts, types etc.*)
    1.54      data: Data.T,				(*additional data*)
    1.55 -    stamps: string ref list};                   (*unique theory indentifier*)
    1.56 +    stamps: string ref list}                    (*unique theory indentifier*)
    1.57        (*the "ref" in stamps ensures that no two signatures are identical
    1.58          -- it is impossible to forge a signature*)
    1.59 +and sg_ref =
    1.60 +  SgRef of sg ref option;
    1.61  
    1.62 +(*make signature*)
    1.63 +fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.64 +  Sg {id = id, self = self, tsig = tsig, const_tab = const_tab, syn = syn,
    1.65 +    path = path, spaces = spaces, data = data, stamps = stamps};
    1.66 +
    1.67 +(*dest signature*)
    1.68  fun rep_sg (Sg args) = args;
    1.69  val tsig_of = #tsig o rep_sg;
    1.70 +val self_ref = #self o rep_sg;
    1.71 +
    1.72 +fun get_data (Sg {data, ...}) = Data.get data;
    1.73 +fun print_data (Sg {data, ...}) = Data.print data;
    1.74 +
    1.75 +
    1.76 +(*show stamps*)
    1.77 +fun stamp_names stamps = rev (map ! stamps);
    1.78 +
    1.79 +fun pretty_sg (Sg {stamps, ...}) = Pretty.str_list "{" "}" (stamp_names stamps);
    1.80 +val pprint_sg = Pretty.pprint o pretty_sg;
    1.81 +
    1.82 +
    1.83 +(* signature id *)
    1.84 +
    1.85 +fun deref (SgRef (Some (ref sg))) = sg
    1.86 +  | deref (SgRef None) = sys_error "Sign.deref";
    1.87 +
    1.88 +fun check_stale (sg as Sg {id, self = SgRef (Some (ref (Sg {id = id', ...}))), ...}) =
    1.89 +      if id = id' then sg
    1.90 +      else raise TERM ("Stale signature: " ^ Pretty.str_of (pretty_sg sg), [])
    1.91 +  | check_stale _ = sys_error "Sign.check_stale";
    1.92  
    1.93  
    1.94  (* inclusion and equality *)
    1.95 @@ -157,28 +196,62 @@
    1.96          if x = y then fast_sub (xs, ys)
    1.97          else fast_sub (x :: xs, ys);
    1.98  in
    1.99 -  fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.100 -    s1 = s2 orelse subset_stamp (s1, s2);
   1.101 +  fun eq_sg (sg1 as Sg {id = id1, ...}, sg2 as Sg {id = id2, ...}) =
   1.102 +    (check_stale sg1; check_stale sg2; id1 = id2);
   1.103  
   1.104 -  fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.105 -    s1 = s2 orelse fast_sub (s1, s2);
   1.106 +  fun subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.107 +    eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   1.108  
   1.109 -  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.110 -    s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1));
   1.111 +  fun fast_subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.112 +    eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
   1.113  end;
   1.114  
   1.115  
   1.116  (*test if same theory names are contained in signatures' stamps,
   1.117    i.e. if signatures belong to same theory but not necessarily to the
   1.118    same version of it*)
   1.119 -fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.120 -  eq_set_string (pairself (map (op !)) (s1, s2));
   1.121 +fun same_sg (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.122 +  eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   1.123  
   1.124  (*test for drafts*)
   1.125  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   1.126    | is_draft _ = false;
   1.127  
   1.128  
   1.129 +(* build signature *)
   1.130 +
   1.131 +fun ext_stamps stamps (id as ref name) =
   1.132 +  let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
   1.133 +    if exists (equal name o !) stmps then
   1.134 +      error ("Theory already contains a " ^ quote name ^ " component")
   1.135 +    else id :: stmps
   1.136 +  end;
   1.137 +
   1.138 +fun create_sign self stamps name (syn, tsig, ctab, (path, spaces), data) =
   1.139 +  let
   1.140 +    val id = ref name;
   1.141 +    val sign =
   1.142 +      make_sign (id, self, tsig, ctab, syn, path, spaces, data, ext_stamps stamps id);
   1.143 +  in
   1.144 +    (case self of
   1.145 +      SgRef (Some r) => r := sign
   1.146 +    | _ => sys_error "Sign.create_sign");
   1.147 +    sign
   1.148 +  end;
   1.149 +
   1.150 +fun extend_sign extfun name decls
   1.151 +    (sg as Sg {id = _, self, tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.152 +  let
   1.153 +    val _ = check_stale sg;
   1.154 +    val (self', data') =
   1.155 +      if is_draft sg then (self, data)
   1.156 +      else (SgRef (Some (ref sg)), Data.prep_ext data);
   1.157 +  in
   1.158 +    create_sign self' stamps name
   1.159 +      (extfun (syn, tsig, const_tab, (path, spaces), data') decls)
   1.160 +  end;
   1.161 +
   1.162 +
   1.163  (* consts *)
   1.164  
   1.165  fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
   1.166 @@ -320,6 +393,7 @@
   1.167    val intern_tycons = intrn_tycons o spaces_of;
   1.168  
   1.169    fun full_name (Sg {path, ...}) = full path;
   1.170 +
   1.171  end;
   1.172  
   1.173  
   1.174 @@ -368,8 +442,6 @@
   1.175  
   1.176  (** print signature **)
   1.177  
   1.178 -fun stamp_names stamps = rev (map ! stamps);
   1.179 -
   1.180  fun print_sg sg =
   1.181    let
   1.182      fun prt_cls c = pretty_sort sg [c];
   1.183 @@ -405,7 +477,7 @@
   1.184      fun pretty_const (c, ty) = Pretty.block
   1.185        [prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   1.186  
   1.187 -    val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.188 +    val Sg {id = _, self = _, tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.189      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
   1.190      val {classes, classrel, default, tycons, abbrs, arities} =
   1.191        Type.rep_tsig tsig;
   1.192 @@ -424,12 +496,6 @@
   1.193    end;
   1.194  
   1.195  
   1.196 -fun pretty_sg (Sg {stamps, ...}) =
   1.197 -  Pretty.str_list "{" "}" (stamp_names stamps);
   1.198 -
   1.199 -val pprint_sg = Pretty.pprint o pretty_sg;
   1.200 -
   1.201 -
   1.202  
   1.203  (** read types **)  (*exception ERROR*)
   1.204  
   1.205 @@ -598,18 +664,18 @@
   1.206  
   1.207  (* add default sort *)
   1.208  
   1.209 -fun ext_defsort int (syn, tsig, ctab, (path, spaces)) S =
   1.210 +fun ext_defsort int (syn, tsig, ctab, (path, spaces), data) S =
   1.211    (syn, Type.ext_tsig_defsort tsig (if int then intrn_sort spaces S else S),
   1.212 -    ctab, (path, spaces));
   1.213 +    ctab, (path, spaces), data);
   1.214  
   1.215  
   1.216  (* add type constructors *)
   1.217  
   1.218 -fun ext_types (syn, tsig, ctab, (path, spaces)) types =
   1.219 +fun ext_types (syn, tsig, ctab, (path, spaces), data) types =
   1.220    let val decls = decls_of path Syntax.type_name types in
   1.221      (Syntax.extend_type_gram syn types,
   1.222        Type.ext_tsig_types tsig decls, ctab,
   1.223 -      (path, add_names spaces typeK (map fst decls)))
   1.224 +      (path, add_names spaces typeK (map fst decls)), data)
   1.225    end;
   1.226  
   1.227  
   1.228 @@ -619,7 +685,7 @@
   1.229    (t, vs, read_raw_typ syn tsig spaces (K None) rhs_src)
   1.230      handle ERROR => error ("in type abbreviation " ^ t);
   1.231  
   1.232 -fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces)) abbrs =
   1.233 +fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
   1.234    let
   1.235      fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
   1.236      val syn' = Syntax.extend_type_gram syn (map mfix_of abbrs);
   1.237 @@ -630,7 +696,7 @@
   1.238      val spaces' = add_names spaces typeK (map #1 abbrs');
   1.239      val decls = map (rd_abbr syn' tsig spaces') abbrs';
   1.240    in
   1.241 -    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'))
   1.242 +    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data)
   1.243    end;
   1.244  
   1.245  fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
   1.246 @@ -639,7 +705,7 @@
   1.247  
   1.248  (* add type arities *)
   1.249  
   1.250 -fun ext_arities int (syn, tsig, ctab, (path, spaces)) arities =
   1.251 +fun ext_arities int (syn, tsig, ctab, (path, spaces), data) arities =
   1.252    let
   1.253      fun intrn_arity (c, Ss, S) =
   1.254        (intrn spaces typeK c, map (intrn_sort spaces) Ss, intrn_sort spaces S);
   1.255 @@ -647,7 +713,7 @@
   1.256      val tsig' = Type.ext_tsig_arities tsig (intrn arities);
   1.257      val log_types = Type.logical_types tsig';
   1.258    in
   1.259 -    (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces))
   1.260 +    (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
   1.261    end;
   1.262  
   1.263  
   1.264 @@ -667,7 +733,7 @@
   1.265    (c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
   1.266      handle ERROR => err_in_const (const_name path c mx);
   1.267  
   1.268 -fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces)) raw_consts =
   1.269 +fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces), data) raw_consts =
   1.270    let
   1.271      fun prep_const (c, ty, mx) =
   1.272        (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.273 @@ -682,7 +748,7 @@
   1.274      (Syntax.extend_const_gram syn prmode consts, tsig,
   1.275        Symtab.extend_new (ctab, decls)
   1.276          handle Symtab.DUPS cs => err_dup_consts cs,
   1.277 -      (path, add_names spaces constK (map fst decls)))
   1.278 +      (path, add_names spaces constK (map fst decls)), data)
   1.279    end;
   1.280  
   1.281  val ext_consts_i = ext_cnsts no_read false ("", true);
   1.282 @@ -706,7 +772,7 @@
   1.283    end;
   1.284  
   1.285  
   1.286 -fun ext_classes int (syn, tsig, ctab, (path, spaces)) classes =
   1.287 +fun ext_classes int (syn, tsig, ctab, (path, spaces), data) classes =
   1.288    let
   1.289      val names = map fst classes;
   1.290      val consts =
   1.291 @@ -720,62 +786,51 @@
   1.292    in
   1.293      ext_consts_i
   1.294        (Syntax.extend_consts syn names,
   1.295 -        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'))
   1.296 +        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
   1.297      consts
   1.298    end;
   1.299  
   1.300  
   1.301  (* add to classrel *)
   1.302  
   1.303 -fun ext_classrel int (syn, tsig, ctab, (path, spaces)) pairs =
   1.304 +fun ext_classrel int (syn, tsig, ctab, (path, spaces), data) pairs =
   1.305    let val intrn = if int then map (pairself (intrn_class spaces)) else I in
   1.306 -    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces))
   1.307 +    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data)
   1.308    end;
   1.309  
   1.310  
   1.311  (* add to syntax *)
   1.312  
   1.313 -fun ext_syn extfun (syn, tsig, ctab, names) args =
   1.314 -  (extfun syn args, tsig, ctab, names);
   1.315 +fun ext_syn extfun (syn, tsig, ctab, names, data) args =
   1.316 +  (extfun syn args, tsig, ctab, names, data);
   1.317  
   1.318  
   1.319  (* add to path *)
   1.320  
   1.321 -fun ext_path (syn, tsig, ctab, (path, spaces)) elem =
   1.322 +fun ext_path (syn, tsig, ctab, (path, spaces), data) elem =
   1.323    let
   1.324      val path' =
   1.325        if elem = ".." andalso not (null path) then fst (split_last path)
   1.326        else if elem = "/" then []
   1.327        else path @ NameSpace.unpack elem;
   1.328    in
   1.329 -    (syn, tsig, ctab, (path', spaces))
   1.330 +    (syn, tsig, ctab, (path', spaces), data)
   1.331    end;      
   1.332  
   1.333  
   1.334  (* add to name space *)
   1.335  
   1.336 -fun ext_space (syn, tsig, ctab, (path, spaces)) (kind, names) =
   1.337 -  (syn, tsig, ctab, (path, add_names spaces kind names));
   1.338 +fun ext_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
   1.339 +  (syn, tsig, ctab, (path, add_names spaces kind names), data);
   1.340  
   1.341  
   1.342 -(* build signature *)
   1.343 +(* signature data *)
   1.344  
   1.345 -fun ext_stamps stamps name =
   1.346 -  let
   1.347 -    val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
   1.348 -  in
   1.349 -    if exists (equal name o !) stmps then
   1.350 -      error ("Theory already contains a " ^ quote name ^ " component")
   1.351 -    else ref name :: stmps
   1.352 -  end;
   1.353 +fun ext_init_data (syn, tsig, ctab, names, data) (kind, e, ext, mrg, prt) =
   1.354 +  (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
   1.355  
   1.356 -fun make_sign (syn, tsig, ctab, (path, spaces)) data stamps name =
   1.357 -  Sg {tsig = tsig, const_tab = ctab, syn = syn, path = path, spaces = spaces,
   1.358 -    data = data, stamps = ext_stamps stamps name};
   1.359 -
   1.360 -fun extend_sign extfun name decls
   1.361 -    (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.362 -  make_sign (extfun (syn, tsig, const_tab, (path, spaces)) decls) data stamps name;
   1.363 +fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
   1.364 +  (syn, tsig, ctab, names, Data.put data kind e);
   1.365  
   1.366  
   1.367  (* the external interfaces *)
   1.368 @@ -804,49 +859,48 @@
   1.369  val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
   1.370  val add_path         = extend_sign ext_path "#";
   1.371  val add_space        = extend_sign ext_space "#";
   1.372 +val init_data        = extend_sign ext_init_data "#";
   1.373 +val put_data         = extend_sign ext_put_data "#";
   1.374  fun add_name name sg = extend_sign K name () sg;
   1.375  
   1.376  val make_draft = add_name "#";
   1.377  
   1.378  
   1.379 -(* additional signature data *)
   1.380  
   1.381 -fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.382 -  make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
   1.383 +(** merge signatures **)    (*exception TERM*)
   1.384  
   1.385 -fun init_data (kind, e, ext, mrg, prt) =
   1.386 -  map_data (fn d => Data.init d kind e ext mrg prt);
   1.387 +(* merge of sg_refs -- trivial only *)
   1.388  
   1.389 -fun get_data (Sg {data, ...}) = Data.get data;
   1.390 -fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
   1.391 -fun print_data (Sg {data, ...}) kind = Data.print data kind;
   1.392 -
   1.393 -(*prepare extension*)
   1.394 -fun prep_ext sg =
   1.395 -  map_data Data.prep_ext sg |> add_path "/";
   1.396 +fun merge_refs (sgr1 as SgRef (Some (ref sg1)),
   1.397 +        sgr2 as SgRef (Some (ref sg2))) =
   1.398 +      if fast_subsig (sg2, sg1) then sgr1
   1.399 +      else if fast_subsig (sg1, sg2) then sgr2
   1.400 +      else if subsig (sg2, sg1) then sgr1
   1.401 +      else if subsig (sg1, sg2) then sgr2
   1.402 +      else raise TERM ("Attempt to do non-trivial merge of signatures", [])
   1.403 +  | merge_refs _ = sys_error "Sign.merge_refs";
   1.404  
   1.405  
   1.406  
   1.407 -(** merge signatures **)    (*exception TERM*)
   1.408 +(* proper merge *)
   1.409  
   1.410 -fun merge_aux triv_only (sg1, sg2) =
   1.411 -  if fast_subsig (sg2, sg1) then sg1
   1.412 -  else if fast_subsig (sg1, sg2) then sg2
   1.413 -  else if subsig (sg2, sg1) then sg1
   1.414 +fun merge_aux (sg1, sg2) =
   1.415 +  if subsig (sg2, sg1) then sg1
   1.416    else if subsig (sg1, sg2) then sg2
   1.417    else if is_draft sg1 orelse is_draft sg2 then
   1.418 -    raise TERM ("Illegal merge of draft signatures", [])
   1.419 -  else if triv_only then
   1.420 -    raise TERM ("Illegal non-trivial merge of signatures", [])
   1.421 +    raise TERM ("Attempt to merge draft signatures", [])
   1.422    else
   1.423      (*neither is union already; must form union*)
   1.424      let
   1.425 -      val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.426 +      val Sg {id = _, self = _, tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.427          path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1;
   1.428 -      val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.429 +      val Sg {id = _, self = _, tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.430          path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2;
   1.431  
   1.432  
   1.433 +      val id = ref "";
   1.434 +      val self_ref = ref sg1;			(*dummy value*)
   1.435 +      val self = SgRef (Some self_ref);
   1.436        val stamps = merge_rev_lists stamps1 stamps2;
   1.437        val _ =
   1.438          (case duplicates (stamp_names stamps) of
   1.439 @@ -855,13 +909,12 @@
   1.440              ^ commas_quote dups, []));
   1.441  
   1.442        val tsig = Type.merge_tsigs (tsig1, tsig2);
   1.443 -
   1.444        val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   1.445          handle Symtab.DUPS cs =>
   1.446            raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
   1.447 -
   1.448        val syn = Syntax.merge_syntaxes syn1 syn2;
   1.449  
   1.450 +      val path = [];
   1.451        val kinds = distinct (map fst (spaces1 @ spaces2));
   1.452        val spaces =
   1.453          kinds ~~
   1.454 @@ -869,25 +922,27 @@
   1.455              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
   1.456  
   1.457        val data = Data.merge (data1, data2);
   1.458 +
   1.459 +      val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps);
   1.460      in
   1.461 -      Sg {tsig = tsig, const_tab = const_tab, syn = syn,
   1.462 -        path = [], spaces = spaces, data = data, stamps = stamps}
   1.463 +      self_ref := sign; sign
   1.464      end;
   1.465  
   1.466 -fun gen_merge triv sgs =
   1.467 -  (case handle_error (merge_aux triv) sgs of
   1.468 +fun merge sg1_sg2 =
   1.469 +  (case handle_error merge_aux sg1_sg2 of
   1.470      OK sg => sg
   1.471    | Error msg => raise TERM (msg, []));
   1.472  
   1.473 -val merge = gen_merge true;
   1.474 -val nontriv_merge = gen_merge false;
   1.475 -
   1.476  
   1.477  
   1.478  (** the Pure signature **)
   1.479  
   1.480 +val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
   1.481 +  Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
   1.482 +
   1.483  val proto_pure =
   1.484 -  make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], [])) Data.empty [] "#"
   1.485 +  create_sign (SgRef (Some (ref dummy_sg))) [] "#"
   1.486 +    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty)
   1.487    |> add_types
   1.488     (("fun", 2, NoSyn) ::
   1.489      ("prop", 0, NoSyn) ::