src/Pure/sign.ML
changeset 2185 f9686e7e6d4d
parent 2184 99805d7652a9
child 2187 07c471510cf1
     1.1 --- a/src/Pure/sign.ML	Wed Nov 13 10:59:53 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 14 14:31:29 1996 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  structure Sign : SIGN =
     1.5  struct
     1.6  
     1.7 -local open Type Syntax in
     1.8 +(*local open Type Syntax in*)
     1.9  
    1.10  (** datatype sg **)
    1.11  
    1.12 @@ -79,7 +79,7 @@
    1.13  
    1.14  datatype sg =
    1.15    Sg of {
    1.16 -    tsig: Type.type_sig,                 (*order-sorted signature of types*)
    1.17 +    tsig: Type.type_sig,            (*order-sorted signature of types*)
    1.18      const_tab: typ Symtab.table,    (*types of constants*)
    1.19      syn: Syntax.syntax,             (*syntax for parsing and printing*)
    1.20      stamps: string ref list};       (*unique theory indentifier*)
    1.21 @@ -88,32 +88,46 @@
    1.22  val tsig_of = #tsig o rep_sg;
    1.23  
    1.24  
    1.25 -(*** Stamps ***)
    1.26 +(* stamps *)
    1.27  
    1.28 -(*Avoiding polymorphic equality: 10* speedup*)
    1.29 -fun mem_stamp (_:string ref, []) = false
    1.30 -  | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
    1.31 +(*inclusion, equality*)
    1.32 +local
    1.33 +  (*avoiding polymorphic equality: factor 10 speedup*)
    1.34 +  fun mem_stamp (_:string ref, []) = false
    1.35 +    | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
    1.36 +
    1.37 +  fun subset_stamp ([], ys) = true
    1.38 +    | subset_stamp (x :: xs, ys) =
    1.39 +        mem_stamp (x, ys) andalso subset_stamp (xs, ys);
    1.40  
    1.41 -fun subset_stamp ([], ys) = true
    1.42 -  | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
    1.43 +  (*fast partial test*)
    1.44 +  fun fast_sub ([]: string ref list, _) = true
    1.45 +    | fast_sub (_, []) = false
    1.46 +    | fast_sub (x :: xs, y :: ys) =
    1.47 +        if x = y then fast_sub (xs, ys)
    1.48 +        else fast_sub (x :: xs, ys);
    1.49 +in
    1.50 +  fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.51 +    s1 = s2 orelse subset_stamp (s1, s2);
    1.52 +
    1.53 +  fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.54 +    s1 = s2 orelse fast_sub (s1, s2);
    1.55  
    1.56 -fun eq_set_stamp (xs, ys) =
    1.57 -    xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
    1.58 +  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.59 +    s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1));
    1.60 +end;
    1.61 +
    1.62  
    1.63 +(*test if same theory names are contained in signatures' stamps,
    1.64 +  i.e. if signatures belong to same theory but not necessarily to the
    1.65 +  same version of it*)
    1.66 +fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.67 +  eq_set_string (pairself (map (op !)) (s1, s2));
    1.68 +
    1.69 +(*test for drafts*)
    1.70  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    1.71    | is_draft _ = false;
    1.72  
    1.73 -fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) =
    1.74 -  s1 = s2 orelse subset_stamp (s1, s2);
    1.75 -
    1.76 -fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
    1.77 -
    1.78 -(* test if same theory names are contained in signatures' stamps,
    1.79 -   i.e. if signatures belong to same theory but not necessarily to the same
    1.80 -   version of it*)
    1.81 -fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.82 -  eq_set_string (pairself (map (op !)) (s1, s2));
    1.83 -
    1.84  
    1.85  (* consts *)
    1.86  
    1.87 @@ -169,7 +183,8 @@
    1.88  
    1.89  
    1.90      val Sg {tsig, const_tab, syn, stamps} = sg;
    1.91 -    val {classes, subclass, default, tycons, abbrs, arities} = rep_tsig tsig;
    1.92 +    val {classes, subclass, default, tycons, abbrs, arities} =
    1.93 +      Type.rep_tsig tsig;
    1.94    in
    1.95      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.96      Pretty.writeln (Pretty.strs ("classes:" :: classes));
    1.97 @@ -217,19 +232,19 @@
    1.98    error ("The error(s) above occurred in type " ^ quote s);
    1.99  
   1.100  fun read_raw_typ syn tsig sort_of str =
   1.101 -  Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
   1.102 +  Syntax.read_typ syn (fn x => if_none (sort_of x) (Type.defaultS tsig)) str
   1.103      handle ERROR => err_in_type str;
   1.104  
   1.105  (*read and certify typ wrt a signature*)
   1.106  fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   1.107 -  cert_typ tsig (read_raw_typ syn tsig sort_of str)
   1.108 +  Type.cert_typ tsig (read_raw_typ syn tsig sort_of str)
   1.109      handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   1.110  
   1.111  
   1.112  
   1.113  (** certify types and terms **)   (*exception TYPE*)
   1.114  
   1.115 -fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   1.116 +fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
   1.117  
   1.118  (* check for duplicate TVars with distinct sorts *)
   1.119  fun nodup_TVars(tvars,T) = (case T of
   1.120 @@ -273,7 +288,7 @@
   1.121    let
   1.122      fun valid_const a T =
   1.123        (case const_type sg a of
   1.124 -        Some U => typ_instance (tsig, T, U)
   1.125 +        Some U => Type.typ_instance (tsig, T, U)
   1.126        | _ => false);
   1.127  
   1.128      fun atom_err (Const (a, T)) =
   1.129 @@ -285,8 +300,8 @@
   1.130        | atom_err _ = None;
   1.131  
   1.132      val norm_tm =
   1.133 -      (case it_term_types (typ_errors tsig) (tm, []) of
   1.134 -        [] => map_term_types (norm_typ tsig) tm
   1.135 +      (case it_term_types (Type.typ_errors tsig) (tm, []) of
   1.136 +        [] => map_term_types (Type.norm_typ tsig) tm
   1.137        | errs => raise_type (cat_lines errs) [] [tm]);
   1.138      val _ = nodup_Vars norm_tm;
   1.139    in
   1.140 @@ -380,14 +395,14 @@
   1.141  (* add default sort *)
   1.142  
   1.143  fun ext_defsort (syn, tsig, ctab) defsort =
   1.144 -  (syn, ext_tsig_defsort tsig defsort, ctab);
   1.145 +  (syn, Type.ext_tsig_defsort tsig defsort, ctab);
   1.146  
   1.147  
   1.148  (* add type constructors *)
   1.149  
   1.150  fun ext_types (syn, tsig, ctab) types =
   1.151    (Syntax.extend_type_gram syn types,
   1.152 -    ext_tsig_types tsig (decls_of Syntax.type_name types),
   1.153 +    Type.ext_tsig_types tsig (decls_of Syntax.type_name types),
   1.154      ctab);
   1.155  
   1.156  
   1.157 @@ -405,7 +420,7 @@
   1.158      fun decl_of (t, vs, rhs, mx) =
   1.159        rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   1.160    in
   1.161 -    (syn1, ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   1.162 +    (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   1.163    end;
   1.164  
   1.165  val ext_tyabbrs_i = ext_abbrs (K (K I));
   1.166 @@ -416,8 +431,8 @@
   1.167  
   1.168  fun ext_arities (syn, tsig, ctab) arities =
   1.169    let
   1.170 -    val tsig1 = ext_tsig_arities tsig arities;
   1.171 -    val log_types = logical_types tsig1;
   1.172 +    val tsig1 = Type.ext_tsig_arities tsig arities;
   1.173 +    val log_types = Type.logical_types tsig1;
   1.174    in
   1.175      (Syntax.extend_log_types syn log_types, tsig1, ctab)
   1.176    end;
   1.177 @@ -439,10 +454,9 @@
   1.178  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   1.179    let
   1.180      fun prep_const (c, ty, mx) = 
   1.181 -	  (c, 
   1.182 -	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
   1.183 -	   mx)
   1.184 -      handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
   1.185 +     (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.186 +       handle TYPE (msg, _, _)
   1.187 +         => (writeln msg; err_in_const (Syntax.const_name c mx));
   1.188  
   1.189      val consts = map (prep_const o rd_const syn tsig) raw_consts;
   1.190      val decls =
   1.191 @@ -480,7 +494,7 @@
   1.192        map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   1.193    in
   1.194      ext_consts_i
   1.195 -      (Syntax.extend_consts syn names, ext_tsig_classes tsig classes, ctab)
   1.196 +      (Syntax.extend_consts syn names, Type.ext_tsig_classes tsig classes, ctab)
   1.197        consts
   1.198    end;
   1.199  
   1.200 @@ -488,7 +502,7 @@
   1.201  (* add to subclass relation *)
   1.202  
   1.203  fun ext_classrel (syn, tsig, ctab) pairs =
   1.204 -  (syn, ext_tsig_subclass tsig pairs, ctab);
   1.205 +  (syn, Type.ext_tsig_subclass tsig pairs, ctab);
   1.206  
   1.207  
   1.208  (* add to syntax *)
   1.209 @@ -541,7 +555,9 @@
   1.210  (** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   1.211  
   1.212  fun merge (sg1, sg2) =
   1.213 -  if subsig (sg2, sg1) then sg1
   1.214 +  if fast_subsig (sg2, sg1) then sg1
   1.215 +  else if fast_subsig (sg1, sg2) then sg2
   1.216 +  else if subsig (sg2, sg1) then sg1
   1.217    else if subsig (sg1, sg2) then sg2
   1.218    else if is_draft sg1 orelse is_draft sg2 then
   1.219      raise_term "Illegal merge of draft signatures" []
   1.220 @@ -561,7 +577,7 @@
   1.221          | dups => raise_term ("Attempt to merge different versions of theories "
   1.222              ^ commas_quote dups) []);
   1.223  
   1.224 -      val tsig = merge_tsigs (tsig1, tsig2);
   1.225 +      val tsig = Type.merge_tsigs (tsig1, tsig2);
   1.226  
   1.227        val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   1.228          handle Symtab.DUPS cs =>
   1.229 @@ -577,7 +593,7 @@
   1.230  (** the Pure signature **)
   1.231  
   1.232  val proto_pure =
   1.233 -  make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
   1.234 +  make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null) [] "#"
   1.235    |> add_types
   1.236     (("fun", 2, NoSyn) ::
   1.237      ("prop", 0, NoSyn) ::
   1.238 @@ -607,5 +623,5 @@
   1.239    |> add_syntax Syntax.pure_applC_syntax
   1.240    |> add_name "CPure";
   1.241  
   1.242 -end
   1.243 +(*end*)
   1.244  end;