src/Pure/term.ML
changeset 15573 cf53c2dcf440
parent 15570 8d8c70b41bab
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/term.ML	Fri Mar 04 10:58:04 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Mar 04 11:44:26 2005 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4    val --> : typ * typ -> typ
     1.5    val ---> : typ list * typ -> typ
     1.6    val is_TVar: typ -> bool
     1.7 +  val is_funtype: typ -> bool
     1.8    val domain_type: typ -> typ
     1.9    val range_type: typ -> typ
    1.10    val binder_types: typ -> typ list
    1.11 @@ -45,6 +46,7 @@
    1.12    val is_Const: term -> bool
    1.13    val is_Free: term -> bool
    1.14    val is_Var: term -> bool
    1.15 +  val is_first_order: term -> bool
    1.16    val dest_Type: typ -> string * typ list
    1.17    val dest_Const: term -> string * typ
    1.18    val dest_Free: term -> string * typ
    1.19 @@ -277,6 +279,10 @@
    1.20  fun is_TVar (TVar _) = true
    1.21    | is_TVar _ = false;
    1.22  
    1.23 +(*Differs from proofterm/is_fun in its treatment of TVar*)
    1.24 +fun is_funtype (Type("fun",[_,_])) = true
    1.25 +  | is_funtype _ = false;
    1.26 +
    1.27  (** Destructors **)
    1.28  
    1.29  fun dest_Const (Const x) =  x
    1.30 @@ -679,6 +685,26 @@
    1.31    in subst end;
    1.32  
    1.33  
    1.34 +(** Identifying first-order terms **)
    1.35 +
    1.36 +(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
    1.37 +fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
    1.38 +
    1.39 +(*First order means in all terms of the form f(t1,...,tn) no argument has a function
    1.40 +  type.*)
    1.41 +fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    1.42 +  | first_order1 Ts t =
    1.43 +      case strip_comb t of
    1.44 +	       (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.45 +	     | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.46 +	     | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.47 +	     | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.48 +	     | (Abs _, ts) => false (*not in beta-normal form*)
    1.49 +	     | _ => error "first_order: unexpected case";
    1.50 +
    1.51 +val is_first_order = first_order1 [];
    1.52 +
    1.53 +
    1.54  (*Computing the maximum index of a typ*)
    1.55  fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
    1.56    | maxidx_of_typ(TFree _) = ~1