src/Pure/old_term.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 37783 95aa0afcb240
child 39687 4e9b6ada3a21
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
wenzelm@29262
     1
(*  Title:      Pure/old_term.ML
wenzelm@29262
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@29262
     3
wenzelm@37783
     4
Some outdated term operations.
wenzelm@29262
     5
*)
wenzelm@29262
     6
wenzelm@29262
     7
signature OLD_TERM =
wenzelm@29262
     8
sig
wenzelm@29270
     9
  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
wenzelm@29270
    10
  val add_term_names: term * string list -> string list
wenzelm@29270
    11
  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
wenzelm@29270
    12
  val add_typ_tfree_names: typ * string list -> string list
wenzelm@29270
    13
  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
wenzelm@29270
    14
  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
wenzelm@29270
    15
  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
wenzelm@29270
    16
  val add_term_tfree_names: term * string list -> string list
wenzelm@29270
    17
  val typ_tfrees: typ -> (string * sort) list
wenzelm@29270
    18
  val typ_tvars: typ -> (indexname * sort) list
wenzelm@29270
    19
  val term_tfrees: term -> (string * sort) list
wenzelm@29270
    20
  val term_tvars: term -> (indexname * sort) list
wenzelm@29262
    21
  val add_term_vars: term * term list -> term list
wenzelm@29262
    22
  val term_vars: term -> term list
wenzelm@29262
    23
  val add_term_frees: term * term list -> term list
wenzelm@29262
    24
  val term_frees: term -> term list
wenzelm@29262
    25
end;
wenzelm@29262
    26
wenzelm@29262
    27
structure OldTerm: OLD_TERM =
wenzelm@29262
    28
struct
wenzelm@29262
    29
wenzelm@29270
    30
(*iterate a function over all types in a term*)
wenzelm@29270
    31
fun it_term_types f =
wenzelm@29270
    32
let fun iter(Const(_,T), a) = f(T,a)
wenzelm@29270
    33
      | iter(Free(_,T), a) = f(T,a)
wenzelm@29270
    34
      | iter(Var(_,T), a) = f(T,a)
wenzelm@29270
    35
      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
wenzelm@29270
    36
      | iter(f$u, a) = iter(f, iter(u, a))
wenzelm@29270
    37
      | iter(Bound _, a) = a
wenzelm@29270
    38
in iter end
wenzelm@29270
    39
wenzelm@29270
    40
(*Accumulates the names in the term, suppressing duplicates.
wenzelm@29270
    41
  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
wenzelm@30364
    42
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
wenzelm@29270
    43
  | add_term_names (Free(a,_), bs) = insert (op =) a bs
wenzelm@29270
    44
  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
wenzelm@29270
    45
  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
wenzelm@29270
    46
  | add_term_names (_, bs) = bs;
wenzelm@29270
    47
wenzelm@29270
    48
(*Accumulates the TVars in a type, suppressing duplicates.*)
wenzelm@29270
    49
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
wenzelm@29270
    50
  | add_typ_tvars(TFree(_),vs) = vs
wenzelm@29270
    51
  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
wenzelm@29270
    52
wenzelm@29270
    53
(*Accumulates the TFrees in a type, suppressing duplicates.*)
wenzelm@29270
    54
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
wenzelm@29270
    55
  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
wenzelm@29270
    56
  | add_typ_tfree_names(TVar(_),fs) = fs;
wenzelm@29270
    57
wenzelm@29270
    58
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
wenzelm@29270
    59
  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
wenzelm@29270
    60
  | add_typ_tfrees(TVar(_),fs) = fs;
wenzelm@29270
    61
wenzelm@29270
    62
(*Accumulates the TVars in a term, suppressing duplicates.*)
wenzelm@29270
    63
val add_term_tvars = it_term_types add_typ_tvars;
wenzelm@29270
    64
wenzelm@29270
    65
(*Accumulates the TFrees in a term, suppressing duplicates.*)
wenzelm@29270
    66
val add_term_tfrees = it_term_types add_typ_tfrees;
wenzelm@29270
    67
val add_term_tfree_names = it_term_types add_typ_tfree_names;
wenzelm@29270
    68
wenzelm@29270
    69
(*Non-list versions*)
wenzelm@29270
    70
fun typ_tfrees T = add_typ_tfrees(T,[]);
wenzelm@29270
    71
fun typ_tvars T = add_typ_tvars(T,[]);
wenzelm@29270
    72
fun term_tfrees t = add_term_tfrees(t,[]);
wenzelm@29270
    73
fun term_tvars t = add_term_tvars(t,[]);
wenzelm@29270
    74
wenzelm@29270
    75
wenzelm@29270
    76
(*Accumulates the Vars in the term, suppressing duplicates.*)
wenzelm@29262
    77
fun add_term_vars (t, vars: term list) = case t of
wenzelm@35408
    78
    Var   _ => OrdList.insert Term_Ord.term_ord t vars
wenzelm@29262
    79
  | Abs (_,_,body) => add_term_vars(body,vars)
wenzelm@29262
    80
  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
wenzelm@29262
    81
  | _ => vars;
wenzelm@29262
    82
wenzelm@29262
    83
fun term_vars t = add_term_vars(t,[]);
wenzelm@29262
    84
wenzelm@29270
    85
(*Accumulates the Frees in the term, suppressing duplicates.*)
wenzelm@29262
    86
fun add_term_frees (t, frees: term list) = case t of
wenzelm@35408
    87
    Free   _ => OrdList.insert Term_Ord.term_ord t frees
wenzelm@29262
    88
  | Abs (_,_,body) => add_term_frees(body,frees)
wenzelm@29262
    89
  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
wenzelm@29262
    90
  | _ => frees;
wenzelm@29262
    91
wenzelm@29262
    92
fun term_frees t = add_term_frees(t,[]);
wenzelm@29262
    93
wenzelm@29262
    94
end;