--- a/src/Pure/library.ML Wed Nov 13 10:41:50 1996 +0100
+++ b/src/Pure/library.ML Wed Nov 13 10:42:50 1996 +0100
@@ -492,24 +492,12 @@
fun ([]:string list) subset_string ys = true
| (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
-fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
-
-
-(*eq_set*)
-
-fun eq_set (xs, ys) =
- xs = ys orelse (xs subset ys andalso ys subset xs);
-
-(*eq_set, optimized version for ints*)
-
-fun eq_set_int ((xs:int list), ys) =
- xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
-
-(*eq_set, optimized version for strings*)
-
+(*set equality for strings*)
fun eq_set_string ((xs:string list), ys) =
xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
+fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
+
(*removing an element from a list WITHOUT duplicates*)
fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
@@ -886,8 +874,9 @@
fun transitive_closure [] = []
| transitive_closure ((x, ys)::ps) =
let val qs = transitive_closure ps
- val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
- fun step(u, us) = (u, if x mem us then zs union us else us)
+ val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
+ fun step(u, us) = (u, if x mem_string us then zs union_string us
+ else us)
in (x, zs) :: map step qs end;
--- a/src/Pure/term.ML Wed Nov 13 10:41:50 1996 +0100
+++ b/src/Pure/term.ML Wed Nov 13 10:42:50 1996 +0100
@@ -322,6 +322,12 @@
fun mem_term (_, []) = false
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
+fun subset_term ([], ys) = true
+ | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
+
+fun eq_set_term (xs, ys) =
+ xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
+
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
fun union_term (xs, []) = xs
@@ -355,6 +361,12 @@
| union_sort ([], ys) = ys
| union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
+fun subset_sort ([], ys) = true
+ | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
+
+fun eq_set_sort (xs, ys) =
+ xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
+
(*are two term lists alpha-convertible in corresponding elements?*)
fun aconvs ([],[]) = true
| aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
--- a/src/Pure/thm.ML Wed Nov 13 10:41:50 1996 +0100
+++ b/src/Pure/thm.ML Wed Nov 13 10:42:50 1996 +0100
@@ -483,7 +483,8 @@
in
Thm {sign = sign, der = der, maxidx = maxidx,
shyps =
- (if eq_set (shyps',sorts) orelse not (!force_strip_shyps) then shyps'
+ (if eq_set_sort (shyps',sorts) orelse
+ not (!force_strip_shyps) then shyps'
else (* FIXME tmp *)
(writeln ("WARNING Removed sort hypotheses: " ^
commas (map Type.str_of_sort (shyps' \\ sorts)));
@@ -503,7 +504,7 @@
| xshyps =>
let
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
- val shyps' = logicS ins (shyps \\ xshyps);
+ val shyps' = ins_sort (logicS, shyps \\ xshyps);
val used_names = foldr add_term_tfree_names (prop :: hyps, []);
val names =
tl (variantlist (replicate (length xshyps + 1) "'", used_names));
@@ -1412,7 +1413,7 @@
| vperm(t,u) = (t=u);
fun var_perm(t,u) = vperm(t,u) andalso
- eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
+ eq_set_term (term_vars t, term_vars u)
(*simple test for looping rewrite*)
fun loops sign prems (lhs,rhs) =
--- a/src/Pure/type.ML Wed Nov 13 10:41:50 1996 +0100
+++ b/src/Pure/type.ML Wed Nov 13 10:42:50 1996 +0100
@@ -187,7 +187,7 @@
*)
fun less a (C, D) = case assoc (a, C) of
- Some ss => D mem ss
+ Some ss => D mem_string ss
| None => err_undcl_class C;
fun leq a (C, D) = C = D orelse less a (C, D);
@@ -413,8 +413,8 @@
val TySg {classes, tycons, abbrs, ...} = tsig;
fun class_err (errs, c) =
- if c mem classes then errs
- else undcl_class c ins errs;
+ if c mem_string classes then errs
+ else undcl_class c ins_string errs;
val sort_err = foldl class_err;
@@ -423,19 +423,19 @@
val errs' = foldr typ_errs (Us, errs);
fun nargs n =
if n = length Us then errs'
- else ("Wrong number of arguments: " ^ quote c) ins errs';
+ else ("Wrong number of arguments: " ^ quote c) ins_string errs';
in
(case assoc (tycons, c) of
Some n => nargs n
| None =>
(case assoc (abbrs, c) of
Some (vs, _) => nargs (length vs)
- | None => undcl_type c ins errs))
+ | None => undcl_type c ins_string errs))
end
| typ_errs (TFree (_, S), errs) = sort_err (errs, S)
| typ_errs (TVar ((x, i), S), errs) =
if i < 0 then
- ("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
+ ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
else sort_err (errs, S);
in
typ_errs (typ, errors)
@@ -460,16 +460,18 @@
fun assoc_union (as1, []) = as1
| assoc_union (as1, (key, l2) :: as2) =
- (case assoc (as1, key) of
- Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2)
+ (case assoc_string (as1, key) of
+ Some l1 => assoc_union
+ (overwrite (as1, (key, l1 union_string l2)), as2)
| None => assoc_union ((key, l2) :: as1, as2));
(* merge subclass *)
fun merge_subclass (subclass1, subclass2) =
- let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in
- if exists (op mem) subclass then
+ let val subclass = transitive_closure (assoc_union (subclass1, subclass2))
+ in
+ if exists (op mem_string) subclass then
error ("Cyclic class structure!") (* FIXME improve msg, raise TERM *)
else subclass
end;
@@ -543,7 +545,7 @@
tycons=tycons1, arities=arities1, abbrs=abbrs1},
TySg{classes=classes2, default=default2, subclass=subclass2,
tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
- let val classes' = classes1 union classes2;
+ let val classes' = classes1 union_string classes2;
val subclass' = merge_subclass (subclass1, subclass2);
val tycons' = foldl add_tycons (tycons1, tycons2)
val arities' = merge_arities subclass' (arities1, arities2);
@@ -558,7 +560,7 @@
(** add classes and subclass relations**)
fun add_classes classes cs =
- (case cs inter classes of
+ (case cs inter_string classes of
[] => cs @ classes
| dups => err_dup_classes cs);
@@ -573,12 +575,13 @@
fun add_subclass classes (subclass, (s, ges)) =
let
fun upd (subclass, s') =
- if s' mem classes then
+ if s' mem_string classes then
let val ges' = the (assoc (subclass, s))
in case assoc (subclass, s') of
- Some sups => if s mem sups
+ Some sups => if s mem_string sups
then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
- else overwrite (subclass, (s, sups union ges'))
+ else overwrite
+ (subclass, (s, sups union_string ges'))
| None => subclass
end
else err_undcl_class s'
@@ -707,7 +710,7 @@
the 'arities' association list of the given type signatrure *)
fun coregular (classes, subclass, tycons) =
- let fun ex C = if C mem classes then () else err_undcl_class(C);
+ let fun ex C = if C mem_string classes then () else err_undcl_class(C);
fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
Some(n) => if n <> length w then varying_decls(t) else
@@ -1010,7 +1013,7 @@
let fun new([],_,vmap) = vmap
| new(ixn::ixns,p as (pref,c),vmap) =
let val nm = pref ^ c
- in if nm mem used then new(ixn::ixns,nextname p, vmap)
+ in if nm mem_string used then new(ixn::ixns,nextname p, vmap)
else new(ixns, nextname p, (ixn,nm)::vmap)
end
in new end;