Removal of polymorphic equality via mem, subset, eq_set, etc
authorpaulson
Wed Nov 13 10:42:50 1996 +0100 (1996-11-13)
changeset 218229e56f003599
parent 2181 9c2b4728641d
child 2183 8d42a7bccf0b
Removal of polymorphic equality via mem, subset, eq_set, etc
src/Pure/library.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/library.ML	Wed Nov 13 10:41:50 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 13 10:42:50 1996 +0100
     1.3 @@ -492,24 +492,12 @@
     1.4  fun ([]:string list) subset_string ys = true
     1.5    | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
     1.6  
     1.7 -fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
     1.8 -
     1.9 -
    1.10 -(*eq_set*)
    1.11 -
    1.12 -fun eq_set (xs, ys) =
    1.13 -  xs = ys orelse (xs subset ys andalso ys subset xs);
    1.14 -
    1.15 -(*eq_set, optimized version for ints*)
    1.16 -
    1.17 -fun eq_set_int ((xs:int list), ys) =
    1.18 -  xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
    1.19 -
    1.20 -(*eq_set, optimized version for strings*)
    1.21 -
    1.22 +(*set equality for strings*)
    1.23  fun eq_set_string ((xs:string list), ys) =
    1.24    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
    1.25  
    1.26 +fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
    1.27 +
    1.28  
    1.29  (*removing an element from a list WITHOUT duplicates*)
    1.30  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
    1.31 @@ -886,8 +874,9 @@
    1.32  fun transitive_closure [] = []
    1.33    | transitive_closure ((x, ys)::ps) =
    1.34        let val qs = transitive_closure ps
    1.35 -          val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
    1.36 -          fun step(u, us) = (u, if x mem us then zs union us else us)
    1.37 +          val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
    1.38 +          fun step(u, us) = (u, if x mem_string us then zs union_string us 
    1.39 +				else us)
    1.40        in (x, zs) :: map step qs end;
    1.41  
    1.42  
     2.1 --- a/src/Pure/term.ML	Wed Nov 13 10:41:50 1996 +0100
     2.2 +++ b/src/Pure/term.ML	Wed Nov 13 10:42:50 1996 +0100
     2.3 @@ -322,6 +322,12 @@
     2.4  fun mem_term (_, []) = false
     2.5    | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
     2.6  
     2.7 +fun subset_term ([], ys) = true
     2.8 +  | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
     2.9 +
    2.10 +fun eq_set_term (xs, ys) =
    2.11 +    xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
    2.12 +
    2.13  fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
    2.14  
    2.15  fun union_term (xs, []) = xs
    2.16 @@ -355,6 +361,12 @@
    2.17    | union_sort ([], ys) = ys
    2.18    | union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
    2.19  
    2.20 +fun subset_sort ([], ys) = true
    2.21 +  | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
    2.22 +
    2.23 +fun eq_set_sort (xs, ys) =
    2.24 +    xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
    2.25 +
    2.26  (*are two term lists alpha-convertible in corresponding elements?*)
    2.27  fun aconvs ([],[]) = true
    2.28    | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
     3.1 --- a/src/Pure/thm.ML	Wed Nov 13 10:41:50 1996 +0100
     3.2 +++ b/src/Pure/thm.ML	Wed Nov 13 10:42:50 1996 +0100
     3.3 @@ -483,7 +483,8 @@
     3.4    in
     3.5      Thm {sign = sign, der = der, maxidx = maxidx,
     3.6  	 shyps =
     3.7 -	 (if eq_set (shyps',sorts) orelse not (!force_strip_shyps) then shyps'
     3.8 +	 (if eq_set_sort (shyps',sorts) orelse 
     3.9 +	     not (!force_strip_shyps) then shyps'
    3.10  	  else    (* FIXME tmp *)
    3.11  	      (writeln ("WARNING Removed sort hypotheses: " ^
    3.12  			commas (map Type.str_of_sort (shyps' \\ sorts)));
    3.13 @@ -503,7 +504,7 @@
    3.14    | xshyps =>
    3.15        let
    3.16          val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
    3.17 -        val shyps' = logicS ins (shyps \\ xshyps);
    3.18 +        val shyps' = ins_sort (logicS, shyps \\ xshyps);
    3.19          val used_names = foldr add_term_tfree_names (prop :: hyps, []);
    3.20          val names =
    3.21            tl (variantlist (replicate (length xshyps + 1) "'", used_names));
    3.22 @@ -1412,7 +1413,7 @@
    3.23    | vperm(t,u) = (t=u);
    3.24  
    3.25  fun var_perm(t,u) = vperm(t,u) andalso
    3.26 -                    eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
    3.27 +                    eq_set_term (term_vars t, term_vars u)
    3.28  
    3.29  (*simple test for looping rewrite*)
    3.30  fun loops sign prems (lhs,rhs) =
     4.1 --- a/src/Pure/type.ML	Wed Nov 13 10:41:50 1996 +0100
     4.2 +++ b/src/Pure/type.ML	Wed Nov 13 10:42:50 1996 +0100
     4.3 @@ -187,7 +187,7 @@
     4.4  *)
     4.5  
     4.6  fun less a (C, D) = case assoc (a, C) of
     4.7 -     Some ss => D mem ss
     4.8 +     Some ss => D mem_string ss
     4.9     | None => err_undcl_class C;
    4.10  
    4.11  fun leq a (C, D)  =  C = D orelse less a (C, D);
    4.12 @@ -413,8 +413,8 @@
    4.13      val TySg {classes, tycons, abbrs, ...} = tsig;
    4.14  
    4.15      fun class_err (errs, c) =
    4.16 -      if c mem classes then errs
    4.17 -      else undcl_class c ins errs;
    4.18 +      if c mem_string classes then errs
    4.19 +      else undcl_class c ins_string errs;
    4.20  
    4.21      val sort_err = foldl class_err;
    4.22  
    4.23 @@ -423,19 +423,19 @@
    4.24              val errs' = foldr typ_errs (Us, errs);
    4.25              fun nargs n =
    4.26                if n = length Us then errs'
    4.27 -              else ("Wrong number of arguments: " ^ quote c) ins errs';
    4.28 +              else ("Wrong number of arguments: " ^ quote c) ins_string errs';
    4.29            in
    4.30              (case assoc (tycons, c) of
    4.31                Some n => nargs n
    4.32              | None =>
    4.33                  (case assoc (abbrs, c) of
    4.34                    Some (vs, _) => nargs (length vs)
    4.35 -                | None => undcl_type c ins errs))
    4.36 +                | None => undcl_type c ins_string errs))
    4.37            end
    4.38      | typ_errs (TFree (_, S), errs) = sort_err (errs, S)
    4.39      | typ_errs (TVar ((x, i), S), errs) =
    4.40          if i < 0 then
    4.41 -          ("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
    4.42 +          ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
    4.43          else sort_err (errs, S);
    4.44    in
    4.45      typ_errs (typ, errors)
    4.46 @@ -460,16 +460,18 @@
    4.47  
    4.48  fun assoc_union (as1, []) = as1
    4.49    | assoc_union (as1, (key, l2) :: as2) =
    4.50 -      (case assoc (as1, key) of
    4.51 -        Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2)
    4.52 +      (case assoc_string (as1, key) of
    4.53 +        Some l1 => assoc_union 
    4.54 +	              (overwrite (as1, (key, l1 union_string l2)), as2)
    4.55        | None => assoc_union ((key, l2) :: as1, as2));
    4.56  
    4.57  
    4.58  (* merge subclass *)
    4.59  
    4.60  fun merge_subclass (subclass1, subclass2) =
    4.61 -  let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in
    4.62 -    if exists (op mem) subclass then
    4.63 +  let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) 
    4.64 +  in
    4.65 +    if exists (op mem_string) subclass then
    4.66        error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
    4.67      else subclass
    4.68    end;
    4.69 @@ -543,7 +545,7 @@
    4.70                       tycons=tycons1, arities=arities1, abbrs=abbrs1},
    4.71                  TySg{classes=classes2, default=default2, subclass=subclass2,
    4.72                       tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
    4.73 -  let val classes' = classes1 union classes2;
    4.74 +  let val classes' = classes1 union_string classes2;
    4.75        val subclass' = merge_subclass (subclass1, subclass2);
    4.76        val tycons' = foldl add_tycons (tycons1, tycons2)
    4.77        val arities' = merge_arities subclass' (arities1, arities2);
    4.78 @@ -558,7 +560,7 @@
    4.79  (** add classes and subclass relations**)
    4.80  
    4.81  fun add_classes classes cs =
    4.82 -  (case cs inter classes of
    4.83 +  (case cs inter_string classes of
    4.84      [] => cs @ classes
    4.85    | dups => err_dup_classes cs);
    4.86  
    4.87 @@ -573,12 +575,13 @@
    4.88  fun add_subclass classes (subclass, (s, ges)) =
    4.89    let
    4.90      fun upd (subclass, s') =
    4.91 -      if s' mem classes then
    4.92 +      if s' mem_string classes then
    4.93          let val ges' = the (assoc (subclass, s))
    4.94          in case assoc (subclass, s') of
    4.95 -             Some sups => if s mem sups
    4.96 +             Some sups => if s mem_string sups
    4.97                             then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
    4.98 -                           else overwrite (subclass, (s, sups union ges'))
    4.99 +                           else overwrite 
   4.100 +			          (subclass, (s, sups union_string ges'))
   4.101             | None => subclass
   4.102          end
   4.103        else err_undcl_class s'
   4.104 @@ -707,7 +710,7 @@
   4.105     the 'arities' association list of the given type signatrure  *)
   4.106  
   4.107  fun coregular (classes, subclass, tycons) =
   4.108 -  let fun ex C = if C mem classes then () else err_undcl_class(C);
   4.109 +  let fun ex C = if C mem_string classes then () else err_undcl_class(C);
   4.110  
   4.111        fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
   4.112              Some(n) => if n <> length w then varying_decls(t) else
   4.113 @@ -1010,7 +1013,7 @@
   4.114    let fun new([],_,vmap) = vmap
   4.115          | new(ixn::ixns,p as (pref,c),vmap) =
   4.116              let val nm = pref ^ c
   4.117 -            in if nm mem used then new(ixn::ixns,nextname p, vmap)
   4.118 +            in if nm mem_string used then new(ixn::ixns,nextname p, vmap)
   4.119                 else new(ixns, nextname p, (ixn,nm)::vmap)
   4.120              end
   4.121    in new end;