src/Pure/term.ML
changeset 14786 24a7bc97a27a
parent 14695 9c78044b99c3
child 14829 cfa5fe01a7b7
     1.1 --- a/src/Pure/term.ML	Fri May 21 21:23:12 2004 +0200
     1.2 +++ b/src/Pure/term.ML	Fri May 21 21:23:37 2004 +0200
     1.3 @@ -99,13 +99,6 @@
     1.4    val eq_ix: indexname * indexname -> bool
     1.5    val ins_ix: indexname * indexname list -> indexname list
     1.6    val mem_ix: indexname * indexname list -> bool
     1.7 -  val eq_sort: sort * class list -> bool
     1.8 -  val mem_sort: sort * class list list -> bool
     1.9 -  val subset_sort: sort list * class list list -> bool
    1.10 -  val eq_set_sort: sort list * sort list -> bool
    1.11 -  val ins_sort: sort * class list list -> class list list
    1.12 -  val union_sort: sort list * sort list -> sort list
    1.13 -  val rems_sort: sort list * sort list -> sort list
    1.14    val aconv: term * term -> bool
    1.15    val aconvs: term list * term list -> bool
    1.16    val mem_term: term * term list -> bool
    1.17 @@ -192,11 +185,14 @@
    1.18    val terms_ord: term list * term list -> order
    1.19    val hd_ord: term * term -> order
    1.20    val termless: term * term -> bool
    1.21 +  val no_dummyT: typ -> typ
    1.22    val dummy_patternN: string
    1.23    val no_dummy_patterns: term -> term
    1.24    val replace_dummy_patterns: int * term -> int * term
    1.25    val is_replaced_dummy_pattern: indexname -> bool
    1.26    val adhoc_freeze_vars: term -> term * string list
    1.27 +  val string_of_vname: indexname -> string
    1.28 +  val string_of_vname': indexname -> string
    1.29  end;
    1.30  
    1.31  structure Term: TERM =
    1.32 @@ -533,6 +529,7 @@
    1.33  fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
    1.34    | betapply (f,u) = f$u;
    1.35  
    1.36 +
    1.37  (** Equality, membership and insertion of indexnames (string*ints) **)
    1.38  
    1.39  (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
    1.40 @@ -576,29 +573,6 @@
    1.41    | inter_term (x::xs, ys) =
    1.42        if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
    1.43  
    1.44 -(** Equality, membership and insertion of sorts (string lists) **)
    1.45 -
    1.46 -fun eq_sort ([]:sort, []) = true
    1.47 -  | eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts)
    1.48 -  | eq_sort (_, _) = false;
    1.49 -
    1.50 -fun mem_sort (_:sort, []) = false
    1.51 -  | mem_sort (S, S'::Ss) = eq_sort (S, S') orelse mem_sort(S,Ss);
    1.52 -
    1.53 -fun ins_sort(S,Ss) = if mem_sort(S,Ss) then Ss else S :: Ss;
    1.54 -
    1.55 -fun union_sort (xs, []) = xs
    1.56 -  | union_sort ([], ys) = ys
    1.57 -  | union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
    1.58 -
    1.59 -fun subset_sort ([], ys) = true
    1.60 -  | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
    1.61 -
    1.62 -fun eq_set_sort (xs, ys) =
    1.63 -    xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
    1.64 -
    1.65 -val rems_sort = gen_rems eq_sort;
    1.66 -
    1.67  (*are two term lists alpha-convertible in corresponding elements?*)
    1.68  fun aconvs ([],[]) = true
    1.69    | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
    1.70 @@ -737,6 +711,14 @@
    1.71  (*Dummy type for parsing and printing.  Will be replaced during type inference. *)
    1.72  val dummyT = Type("dummy",[]);
    1.73  
    1.74 +fun no_dummyT typ =
    1.75 +  let
    1.76 +    fun check (T as Type ("dummy", _)) =
    1.77 +          raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
    1.78 +      | check (Type (_, Ts)) = seq check Ts
    1.79 +      | check _ = ();
    1.80 +  in check typ; typ end;
    1.81 +
    1.82  (*read a numeral of the given radix, normally 10*)
    1.83  fun read_radixint (radix: int, cs) : int * string list =
    1.84    let val zero = ord"0"
    1.85 @@ -1121,8 +1103,22 @@
    1.86    in (subst_atomic insts tm, xs) end;
    1.87  
    1.88  
    1.89 +(* string_of_vname *)
    1.90 +
    1.91 +fun string_of_vname (x, i) =
    1.92 +  let
    1.93 +    val si = string_of_int i;
    1.94 +    val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true;
    1.95 +  in
    1.96 +    if dot then "?" ^ x ^ "." ^ si
    1.97 +    else if i = 0 then "?" ^ x
    1.98 +    else "?" ^ x ^ si
    1.99 +  end;
   1.100 +
   1.101 +fun string_of_vname' (x, ~1) = x
   1.102 +  | string_of_vname' xi = string_of_vname xi;
   1.103 +
   1.104  end;
   1.105  
   1.106 -
   1.107  structure BasicTerm: BASIC_TERM = Term;
   1.108  open BasicTerm;