src/Pure/sign.ML
changeset 620 f787eb061618
parent 583 550292083e66
child 623 ca9f5dbab880
     1.1 --- a/src/Pure/sign.ML	Mon Sep 26 17:36:10 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Sep 26 17:55:45 1994 +0100
     1.3 @@ -3,9 +3,6 @@
     1.4      Author:     Lawrence C Paulson and Markus Wenzel
     1.5  
     1.6  The abstract type "sg" of signatures.
     1.7 -
     1.8 -TODO:
     1.9 -  clean
    1.10  *)
    1.11  
    1.12  signature SIGN =
    1.13 @@ -33,6 +30,7 @@
    1.14      val pprint_sg: sg -> pprint_args -> unit
    1.15      val pretty_term: sg -> term -> Pretty.T
    1.16      val pretty_typ: sg -> typ -> Pretty.T
    1.17 +    val pretty_sort: sort -> Pretty.T
    1.18      val string_of_term: sg -> term -> string
    1.19      val string_of_typ: sg -> typ -> string
    1.20      val pprint_term: sg -> term -> pprint_args -> unit
    1.21 @@ -111,13 +109,16 @@
    1.22    Symtab.lookup (const_tab, c);
    1.23  
    1.24  
    1.25 -(* classes *)
    1.26 +(* classes and sorts *)
    1.27  
    1.28  val classes = #classes o Type.rep_tsig o tsig_of;
    1.29  
    1.30  val subsort = Type.subsort o tsig_of;
    1.31  val norm_sort = Type.norm_sort o tsig_of;
    1.32  
    1.33 +fun pretty_sort [c] = Pretty.str c
    1.34 +  | pretty_sort cs = Pretty.str_list "{" "}" cs;
    1.35 +
    1.36  
    1.37  
    1.38  (** print signature **)
    1.39 @@ -128,9 +129,6 @@
    1.40    let
    1.41      fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
    1.42  
    1.43 -    fun pretty_sort [cl] = Pretty.str cl
    1.44 -      | pretty_sort cls = Pretty.str_list "{" "}" cls;
    1.45 -
    1.46      fun pretty_subclass (cl, cls) = Pretty.block
    1.47        [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
    1.48  
    1.49 @@ -140,7 +138,7 @@
    1.50      fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
    1.51  
    1.52      fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
    1.53 -      [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
    1.54 +      [prt_typ syn (Type (ty, map (fn v => TVar ((v, 0), [])) vs)),
    1.55          Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
    1.56  
    1.57      fun pretty_arity ty (cl, []) = Pretty.block
    1.58 @@ -264,32 +262,7 @@
    1.59  
    1.60  
    1.61  
    1.62 -(** extend signature **)    (*exception ERROR*)
    1.63 -
    1.64 -(* FIXME -> type.ML *)
    1.65 -
    1.66 -(* FIXME replace? *)
    1.67 -fun varify_typ (Type (t, tys)) = Type (t, map varify_typ tys)
    1.68 -  | varify_typ (TFree (a, s)) = TVar ((a, 0), s)
    1.69 -  | varify_typ (ty as TVar _) =
    1.70 -      raise_type "Illegal schematic type variable" [ty] [];
    1.71 -
    1.72 -
    1.73 -(* fake newstyle interfaces *) (* FIXME -> type.ML *)
    1.74 -
    1.75 -fun ext_tsig_classes tsig classes =
    1.76 -  extend_tsig tsig (classes, [], [], []);
    1.77 -
    1.78 -(* FIXME varify_typ, rem_sorts; norm_typ (?) *)
    1.79 -fun ext_tsig_abbrs tsig abbrs = Type.ext_tsig_abbrs tsig
    1.80 -  (map (fn (t, vs, rhs) => (t, (map (rpair 0) vs, varifyT rhs))) abbrs);
    1.81 -
    1.82 -fun ext_tsig_arities tsig arities = extend_tsig tsig
    1.83 -  ([], [], [], flat (map (fn (t, ss, cs) => map (fn c => ([t], (ss, c))) cs) arities));
    1.84 -
    1.85 -
    1.86 -
    1.87 -(** extension functions **)  (*exception ERROR*)
    1.88 +(** signature extension functions **)  (*exception ERROR*)
    1.89  
    1.90  fun decls_of name_of mfixs =
    1.91    map (fn (x, y, mx) => (name_of x mx, y)) mfixs;
    1.92 @@ -354,15 +327,9 @@
    1.93    (c, read_raw_typ syn tsig (K None) ty_src, mx)
    1.94      handle ERROR => err_in_const (Syntax.const_name c mx);
    1.95  
    1.96 -(* FIXME move *)
    1.97 -fun no_tvars ty =
    1.98 -  if null (typ_tvars ty) then ty
    1.99 -  else raise_type "Illegal schematic type variable(s)" [ty] [];
   1.100 -
   1.101  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   1.102    let
   1.103 -    (* FIXME clean *)
   1.104 -    fun prep_const (c, ty, mx) = (c, varify_typ (cert_typ tsig (no_tvars ty)), mx)
   1.105 +    fun prep_const (c, ty, mx) = (c, varifyT (cert_typ tsig (no_tvars ty)), mx)
   1.106        handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
   1.107  
   1.108      val consts = map (prep_const o rd_const syn tsig) raw_consts;
   1.109 @@ -461,7 +428,7 @@
   1.110  
   1.111  
   1.112  
   1.113 -(** merge signatures **)    (*exception TERM*)
   1.114 +(** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   1.115  
   1.116  fun merge (sg1, sg2) =
   1.117    if subsig (sg2, sg1) then sg1