src/Pure/sign.ML
changeset 3877 83c5310aaaab
parent 3867 3b2587c809f4
child 3886 eb0681305d3f
     1.1 --- a/src/Pure/sign.ML	Wed Oct 15 15:15:22 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Oct 15 15:17:32 1997 +0200
     1.3 @@ -102,12 +102,14 @@
     1.4    val add_path: string -> sg -> sg
     1.5    val add_space: string * string list -> sg -> sg
     1.6    val add_name: string -> sg -> sg
     1.7 -  val make_draft: sg -> sg
     1.8 -  val print_data: sg -> unit
     1.9 -  val init_data: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T) -> sg -> sg
    1.10 +  val init_data: string * exn * (exn -> exn) * (exn * exn -> exn) *
    1.11 +    (string -> exn -> unit) -> sg -> sg
    1.12    val get_data: sg -> string -> exn
    1.13    val put_data: string * exn -> sg -> sg
    1.14 +  val print_data: sg -> string -> unit
    1.15 +  val prep_ext: sg -> sg
    1.16    val merge: sg * sg -> sg
    1.17 +  val nontriv_merge: sg * sg -> sg
    1.18    val proto_pure: sg
    1.19    val pure: sg
    1.20    val cpure: sg
    1.21 @@ -356,12 +358,13 @@
    1.22      fun pretty_const (c, ty) = Pretty.block
    1.23        [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
    1.24  
    1.25 -    val Sg {tsig, const_tab, syn = _, path, spaces, data = _, stamps} = sg;
    1.26 +    val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
    1.27      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
    1.28      val {classes, classrel, default, tycons, abbrs, arities} =
    1.29        Type.rep_tsig tsig;
    1.30    in
    1.31      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.32 +    Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data));
    1.33      Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
    1.34      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
    1.35      Pretty.writeln (pretty_classes classes);
    1.36 @@ -799,26 +802,32 @@
    1.37  
    1.38  (* additional signature data *)
    1.39  
    1.40 -fun print_data (Sg {data, ...}) = Data.print data;
    1.41 -fun get_data (Sg {data, ...}) = Data.get data;
    1.42 -
    1.43  fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
    1.44    make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
    1.45  
    1.46 -fun init_data (kind, e, mrg, prt) = map_data (fn d => Data.init d kind e mrg prt);
    1.47 +fun init_data (kind, e, ext, mrg, prt) =
    1.48 +  map_data (fn d => Data.init d kind e ext mrg prt);
    1.49 +
    1.50 +fun get_data (Sg {data, ...}) = Data.get data;
    1.51  fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
    1.52 +fun print_data (Sg {data, ...}) kind = Data.print data kind;
    1.53 +
    1.54 +(*prepare extension*)
    1.55 +val prep_ext = map_data Data.prep_ext;
    1.56  
    1.57  
    1.58  
    1.59  (** merge signatures **)    (*exception TERM*)
    1.60  
    1.61 -fun merge_aux (sg1, sg2) =
    1.62 +fun merge_aux triv_only (sg1, sg2) =
    1.63    if fast_subsig (sg2, sg1) then sg1
    1.64    else if fast_subsig (sg1, sg2) then sg2
    1.65    else if subsig (sg2, sg1) then sg1
    1.66    else if subsig (sg1, sg2) then sg2
    1.67    else if is_draft sg1 orelse is_draft sg2 then
    1.68      raise TERM ("Illegal merge of draft signatures", [])
    1.69 +  else if triv_only then
    1.70 +    raise TERM ("Illegal non-trivial merge of signatures", [])
    1.71    else
    1.72      (*neither is union already; must form union*)
    1.73      let
    1.74 @@ -855,11 +864,14 @@
    1.75          path = [], spaces = spaces, data = data, stamps = stamps}
    1.76      end;
    1.77  
    1.78 -fun merge sgs =
    1.79 -  (case handle_error merge_aux sgs of
    1.80 +fun gen_merge triv sgs =
    1.81 +  (case handle_error (merge_aux triv) sgs of
    1.82      OK sg => sg
    1.83    | Error msg => raise TERM (msg, []));
    1.84  
    1.85 +val merge = gen_merge true;
    1.86 +val nontriv_merge = gen_merge false;
    1.87 +
    1.88  
    1.89  
    1.90  (** the Pure signature **)