# HG changeset patch # User paulson # Date 847878170 -3600 # Node ID 29e56f003599bc0098426595378b2eb1eef74bc5 # Parent 9c2b4728641d53c36150062d456317c6654a0076 Removal of polymorphic equality via mem, subset, eq_set, etc diff -r 9c2b4728641d -r 29e56f003599 src/Pure/library.ML --- 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; diff -r 9c2b4728641d -r 29e56f003599 src/Pure/term.ML --- 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) diff -r 9c2b4728641d -r 29e56f003599 src/Pure/thm.ML --- 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) = diff -r 9c2b4728641d -r 29e56f003599 src/Pure/type.ML --- 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;