src/Pure/old_term.ML
author blanchet
Thu, 16 Dec 2010 22:45:02 +0100
changeset 41220 4d11b0de7dd8
parent 39687 4e9b6ada3a21
permissions -rw-r--r--
discriminate SMT errors a bit better
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/old_term.ML
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     3
37783
95aa0afcb240 tuned comment;
wenzelm
parents: 35408
diff changeset
     4
Some outdated term operations.
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     5
*)
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     6
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     7
signature OLD_TERM =
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
     8
sig
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
     9
  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    10
  val add_term_names: term * string list -> string list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    11
  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    12
  val add_typ_tfree_names: typ * string list -> string list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    13
  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    14
  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    15
  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    16
  val add_term_tfree_names: term * string list -> string list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    17
  val typ_tfrees: typ -> (string * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    18
  val typ_tvars: typ -> (indexname * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    19
  val term_tfrees: term -> (string * sort) list
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    20
  val term_tvars: term -> (indexname * sort) list
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    21
  val add_term_vars: term * term list -> term list
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    22
  val term_vars: term -> term list
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    23
  val add_term_frees: term * term list -> term list
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    24
  val term_frees: term -> term list
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    25
end;
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    26
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    27
structure OldTerm: OLD_TERM =
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    28
struct
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    29
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    30
(*iterate a function over all types in a term*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    31
fun it_term_types f =
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    32
let fun iter(Const(_,T), a) = f(T,a)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    33
      | iter(Free(_,T), a) = f(T,a)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    34
      | iter(Var(_,T), a) = f(T,a)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    35
      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    36
      | iter(f$u, a) = iter(f, iter(u, a))
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    37
      | iter(Bound _, a) = a
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    38
in iter end
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    39
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    40
(*Accumulates the names in the term, suppressing duplicates.
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    41
  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
    42
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    43
  | add_term_names (Free(a,_), bs) = insert (op =) a bs
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    44
  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    45
  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    46
  | add_term_names (_, bs) = bs;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    47
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    48
(*Accumulates the TVars in a type, suppressing duplicates.*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    49
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    50
  | add_typ_tvars(TFree(_),vs) = vs
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    51
  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    52
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    53
(*Accumulates the TFrees in a type, suppressing duplicates.*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    54
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    55
  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    56
  | add_typ_tfree_names(TVar(_),fs) = fs;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    57
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    58
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    59
  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    60
  | add_typ_tfrees(TVar(_),fs) = fs;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    61
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    62
(*Accumulates the TVars in a term, suppressing duplicates.*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    63
val add_term_tvars = it_term_types add_typ_tvars;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    64
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    65
(*Accumulates the TFrees in a term, suppressing duplicates.*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    66
val add_term_tfrees = it_term_types add_typ_tfrees;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    67
val add_term_tfree_names = it_term_types add_typ_tfree_names;
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    68
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    69
(*Non-list versions*)
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    70
fun typ_tfrees T = add_typ_tfrees(T,[]);
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    71
fun typ_tvars T = add_typ_tvars(T,[]);
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    72
fun term_tfrees t = add_term_tfrees(t,[]);
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    73
fun term_tvars t = add_term_tvars(t,[]);
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    74
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    75
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    76
(*Accumulates the Vars in the term, suppressing duplicates.*)
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    77
fun add_term_vars (t, vars: term list) = case t of
39687
4e9b6ada3a21 modernized structure Ord_List;
wenzelm
parents: 37783
diff changeset
    78
    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    79
  | Abs (_,_,body) => add_term_vars(body,vars)
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    80
  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    81
  | _ => vars;
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    82
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    83
fun term_vars t = add_term_vars(t,[]);
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    84
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
    85
(*Accumulates the Frees in the term, suppressing duplicates.*)
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    86
fun add_term_frees (t, frees: term list) = case t of
39687
4e9b6ada3a21 modernized structure Ord_List;
wenzelm
parents: 37783
diff changeset
    87
    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
29262
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    88
  | Abs (_,_,body) => add_term_frees(body,frees)
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    89
  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    90
  | _ => frees;
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    91
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    92
fun term_frees t = add_term_frees(t,[]);
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    93
3ee4656b9e0c Some old-style term operations.
wenzelm
parents:
diff changeset
    94
end;