src/Pure/term.ML
changeset 8408 4d981311dab7
parent 7638 f586d7995474
child 8609 ec57bc9340e8
equal deleted inserted replaced
8407:d522ad1809e9 8408:4d981311dab7
    33     Free of string * typ |
    33     Free of string * typ |
    34     Var of indexname * typ |
    34     Var of indexname * typ |
    35     Bound of int |
    35     Bound of int |
    36     Abs of string * typ * term |
    36     Abs of string * typ * term |
    37     $ of term * term
    37     $ of term * term
       
    38   structure Vartab : TABLE
       
    39   structure Termtab : TABLE
    38   exception TYPE of string * typ list * term list
    40   exception TYPE of string * typ list * term list
    39   exception TERM of string * term list
    41   exception TERM of string * term list
    40   val is_Bound: term -> bool
    42   val is_Bound: term -> bool
    41   val is_Const: term -> bool
    43   val is_Const: term -> bool
    42   val is_Free: term -> bool
    44   val is_Free: term -> bool
    88   val loose_bvar: term * int -> bool
    90   val loose_bvar: term * int -> bool
    89   val loose_bvar1: term * int -> bool
    91   val loose_bvar1: term * int -> bool
    90   val subst_bounds: term list * term -> term
    92   val subst_bounds: term list * term -> term
    91   val subst_bound: term * term -> term
    93   val subst_bound: term * term -> term
    92   val subst_TVars: (indexname * typ) list -> term -> term
    94   val subst_TVars: (indexname * typ) list -> term -> term
       
    95   val subst_TVars_Vartab: typ Vartab.table -> term -> term
    93   val betapply: term * term -> term
    96   val betapply: term * term -> term
    94   val eq_ix: indexname * indexname -> bool
    97   val eq_ix: indexname * indexname -> bool
    95   val ins_ix: indexname * indexname list -> indexname list
    98   val ins_ix: indexname * indexname list -> indexname list
    96   val mem_ix: indexname * indexname list -> bool
    99   val mem_ix: indexname * indexname list -> bool
    97   val eq_sort: sort * class list -> bool
   100   val eq_sort: sort * class list -> bool
   112   val could_unify: term * term -> bool
   115   val could_unify: term * term -> bool
   113   val subst_free: (term * term) list -> term -> term
   116   val subst_free: (term * term) list -> term -> term
   114   val subst_atomic: (term * term) list -> term -> term
   117   val subst_atomic: (term * term) list -> term -> term
   115   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   118   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   116   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   119   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
       
   120   val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
   117   val subst_Vars: (indexname * term) list -> term -> term
   121   val subst_Vars: (indexname * term) list -> term -> term
   118   val incr_tvar: int -> typ -> typ
   122   val incr_tvar: int -> typ -> typ
   119   val xless: (string * int) * indexname -> bool
   123   val xless: (string * int) * indexname -> bool
   120   val atless: term * term -> bool
   124   val atless: term * term -> bool
   121   val insert_aterm: term * term list -> term list
   125   val insert_aterm: term * term list -> term list
   965   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   969   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   966 and terms_ord (ts, us) = list_ord term_ord (ts, us);
   970 and terms_ord (ts, us) = list_ord term_ord (ts, us);
   967 
   971 
   968 fun termless tu = (term_ord tu = LESS);
   972 fun termless tu = (term_ord tu = LESS);
   969 
   973 
       
   974 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
       
   975 structure Termtab = TableFun(type key = term val ord = term_ord);
       
   976 
       
   977 (*Substitute for type Vars in a type, version using Vartab*)
       
   978 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
       
   979   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
       
   980 	| subst(T as TFree _) = T
       
   981 	| subst(T as TVar(ixn, _)) =
       
   982             (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U)
       
   983   in subst T end;
       
   984 
       
   985 (*Substitute for type Vars in a term, version using Vartab*)
       
   986 val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
   970 
   987 
   971 
   988 
   972 (*** Compression of terms and types by sharing common subtrees.  
   989 (*** Compression of terms and types by sharing common subtrees.  
   973      Saves 50-75% on storage requirements.  As it is fairly slow, 
   990      Saves 50-75% on storage requirements.  As it is fairly slow, 
   974      it is called only for axioms, stored theorems, etc. ***)
   991      it is called only for axioms, stored theorems, etc. ***)
  1042 end;
  1059 end;
  1043 
  1060 
  1044 
  1061 
  1045 structure BasicTerm: BASIC_TERM = Term;
  1062 structure BasicTerm: BASIC_TERM = Term;
  1046 open BasicTerm;
  1063 open BasicTerm;
  1047 
       
  1048 structure Vartab = TableFun(type key = indexname val ord = Term.indexname_ord);
       
  1049 structure Termtab = TableFun(type key = term val ord = Term.term_ord);