src/Pure/sign.ML
changeset 2180 934572a94139
parent 2144 ddb8499c772b
child 2184 99805d7652a9
equal deleted inserted replaced
2179:018906568ef0 2180:934572a94139
    86 
    86 
    87 fun rep_sg (Sg args) = args;
    87 fun rep_sg (Sg args) = args;
    88 val tsig_of = #tsig o rep_sg;
    88 val tsig_of = #tsig o rep_sg;
    89 
    89 
    90 
    90 
    91 (* stamps *)
    91 (*** Stamps ***)
       
    92 
       
    93 (*Avoiding polymorphic equality: 10* speedup*)
       
    94 fun mem_stamp (_:string ref, []) = false
       
    95   | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
       
    96 
       
    97 fun subset_stamp ([], ys) = true
       
    98   | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
       
    99 
       
   100 fun eq_set_stamp (xs, ys) =
       
   101     xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
    92 
   102 
    93 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   103 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    94   | is_draft _ = false;
   104   | is_draft _ = false;
    95 
   105 
    96 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
   106 fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
    97 
   107 
    98 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
   108 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
    99 
   109 
   100 (* test if same theory names are contained in signatures' stamps,
   110 (* test if same theory names are contained in signatures' stamps,
   101    i.e. if signatures belong to same theory but not necessarily to the same
   111    i.e. if signatures belong to same theory but not necessarily to the same
   102    version of it*)
   112    version of it*)
   103 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   113 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   104   eq_set (pairself (map (op !)) (s1, s2));
   114   eq_set_string (pairself (map (op !)) (s1, s2));
   105 
   115 
   106 
   116 
   107 (* consts *)
   117 (* consts *)
   108 
   118 
   109 fun const_type (Sg {const_tab, ...}) c =
   119 fun const_type (Sg {const_tab, ...}) c =