added subsort, norm_sort, classes;
authorwenzelm
Thu May 26 16:45:56 1994 +0200 (1994-05-26)
changeset 40216a8fe4f2250
parent 401 324ad2e02826
child 403 4c66b1577753
added subsort, norm_sort, classes;
minor internal cleanups;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu May 26 16:45:08 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu May 26 16:45:56 1994 +0200
     1.3 @@ -25,6 +25,9 @@
     1.4      val eq_sg: sg * sg -> bool
     1.5      val is_draft: sg -> bool
     1.6      val const_type: sg -> string -> typ option
     1.7 +    val classes: sg -> class list
     1.8 +    val subsort: sg -> sort * sort -> bool      (* FIXME move? *)
     1.9 +    val norm_sort: sg -> sort -> sort           (* FIXME move? *)
    1.10      val print_sg: sg -> unit
    1.11      val pprint_sg: sg -> pprint_args -> unit
    1.12      val pretty_term: sg -> term -> Pretty.T
    1.13 @@ -92,8 +95,11 @@
    1.14      stamps: string ref list};       (*unique theory indentifier*)
    1.15  
    1.16  fun rep_sg (Sg args) = args;
    1.17 +val tsig_of = #tsig o rep_sg;
    1.18  
    1.19  
    1.20 +(* stamps *)
    1.21 +
    1.22  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    1.23    | is_draft _ = false;
    1.24  
    1.25 @@ -102,10 +108,20 @@
    1.26  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    1.27  
    1.28  
    1.29 +(* consts *)
    1.30 +
    1.31  fun const_type (Sg {const_tab, ...}) c =
    1.32    Symtab.lookup (const_tab, c);
    1.33  
    1.34  
    1.35 +(* classes *)
    1.36 +
    1.37 +val classes = #classes o Type.rep_tsig o tsig_of;
    1.38 +
    1.39 +val subsort = Type.subsort o tsig_of;
    1.40 +val norm_sort = Type.norm_sort o tsig_of;
    1.41 +
    1.42 +
    1.43  
    1.44  (** print signature **)
    1.45  
    1.46 @@ -403,29 +419,15 @@
    1.47  
    1.48  (* build signature *)
    1.49  
    1.50 -(* FIXME debug *)
    1.51 -fun assert_stamps_ok stamps =
    1.52 -  let val names = map ! stamps;
    1.53 -  in
    1.54 -    if not (null (duplicates stamps)) then
    1.55 -      error "DEBUG dup stamps"
    1.56 -    else if not (null (duplicates names)) then
    1.57 -      error "DEBUG dup stamp names"
    1.58 -    else if not (null names) andalso exists (equal "#") (tl names) then
    1.59 -      error "DEBUG misplaced draft stamp name"
    1.60 -    else stamps
    1.61 -  end;
    1.62 -
    1.63  fun ext_stamps stamps name =
    1.64    let
    1.65      val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
    1.66    in
    1.67      if exists (equal name o !) stmps then
    1.68        error ("Theory already contains a " ^ quote name ^ " component")
    1.69 -    else assert_stamps_ok (ref name :: stmps)
    1.70 +    else ref name :: stmps
    1.71    end;
    1.72  
    1.73 -
    1.74  fun make_sign (syn, tsig, ctab) stamps name =
    1.75    Sg {tsig = tsig, const_tab = ctab, syn = syn,
    1.76      stamps = ext_stamps stamps name};
    1.77 @@ -521,6 +523,13 @@
    1.78          stamps = stamps2} = sg2;
    1.79  
    1.80  
    1.81 +      val stamps = merge_rev_lists stamps1 stamps2;
    1.82 +      val _ =
    1.83 +        (case duplicates (stamp_names stamps) of
    1.84 +          [] => ()
    1.85 +        | dups => raise_term ("Attempt to merge different versions of theories "
    1.86 +            ^ commas_quote dups) []);
    1.87 +
    1.88        val tsig = merge_tsigs (tsig1, tsig2);
    1.89  
    1.90        val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
    1.91 @@ -528,13 +537,7 @@
    1.92            raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
    1.93  
    1.94        val syn = Syntax.merge_syntaxes syn1 syn2;
    1.95 -
    1.96 -      val stamps = merge_rev_lists stamps1 stamps2;
    1.97 -      val dups = duplicates (stamp_names stamps);
    1.98      in
    1.99 -      if null dups then assert_stamps_ok stamps    (* FIXME debug *)
   1.100 -      else raise_term ("Attempt to merge different versions of theories " ^
   1.101 -        commas_quote dups) [];
   1.102        Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   1.103      end;
   1.104