src/Pure/term.ML
changeset 16537 954495db0f07
parent 16338 3d1851acb4d0
child 16570 861b9fa2c98c
     1.1 --- a/src/Pure/term.ML	Wed Jun 22 19:41:22 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jun 22 19:41:23 2005 +0200
     1.3 @@ -21,6 +21,15 @@
     1.4      Type  of string * typ list |
     1.5      TFree of string * sort |
     1.6      TVar  of indexname * sort
     1.7 +  datatype term =
     1.8 +    Const of string * typ |
     1.9 +    Free of string * typ |
    1.10 +    Var of indexname * typ |
    1.11 +    Bound of int |
    1.12 +    Abs of string * typ * term |
    1.13 +    op $ of term * term
    1.14 +  exception TYPE of string * typ list * term list
    1.15 +  exception TERM of string * term list
    1.16    val --> : typ * typ -> typ
    1.17    val ---> : typ list * typ -> typ
    1.18    val is_TVar: typ -> bool
    1.19 @@ -30,18 +39,6 @@
    1.20    val binder_types: typ -> typ list
    1.21    val body_type: typ -> typ
    1.22    val strip_type: typ -> typ list * typ
    1.23 -  datatype term =
    1.24 -    Const of string * typ |
    1.25 -    Free of string * typ |
    1.26 -    Var of indexname * typ |
    1.27 -    Bound of int |
    1.28 -    Abs of string * typ * term |
    1.29 -    op $ of term * term
    1.30 -  structure Vartab : TABLE
    1.31 -  structure Typtab : TABLE
    1.32 -  structure Termtab : TABLE
    1.33 -  exception TYPE of string * typ list * term list
    1.34 -  exception TERM of string * term list
    1.35    val is_Bound: term -> bool
    1.36    val is_Const: term -> bool
    1.37    val is_Free: term -> bool
    1.38 @@ -70,6 +67,11 @@
    1.39    val map_type_tfree: (string * sort -> typ) -> typ -> typ
    1.40    val map_term_types: (typ -> typ) -> term -> term
    1.41    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    1.42 +  structure Vartab: TABLE
    1.43 +  structure Typtab: TABLE
    1.44 +  structure Termtab: TABLE
    1.45 +  val aconv: term * term -> bool
    1.46 +  val aconvs: term list * term list -> bool
    1.47    val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    1.48    val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    1.49    val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    1.50 @@ -99,8 +101,6 @@
    1.51    val eq_ix: indexname * indexname -> bool
    1.52    val ins_ix: indexname * indexname list -> indexname list
    1.53    val mem_ix: indexname * indexname list -> bool
    1.54 -  val aconv: term * term -> bool
    1.55 -  val aconvs: term list * term list -> bool
    1.56    val mem_term: term * term list -> bool
    1.57    val subset_term: term list * term list -> bool
    1.58    val eq_set_term: term list * term list -> bool
    1.59 @@ -130,7 +130,7 @@
    1.60    val maxidx_of_terms: term list -> int
    1.61    val variant: string list -> string -> string
    1.62    val variantlist: string list * string list -> string list
    1.63 -        (* note reversed order of args wrt. variant! *)
    1.64 +    (*note reversed order of args wrt. variant!*)
    1.65    val variant_abs: string * typ * term -> string * term
    1.66    val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
    1.67    val add_new_id: string list * string -> string list
    1.68 @@ -171,6 +171,14 @@
    1.69  signature TERM =
    1.70  sig
    1.71    include BASIC_TERM
    1.72 +  val indexname_ord: indexname * indexname -> order
    1.73 +  val sort_ord: sort * sort -> order
    1.74 +  val typ_ord: typ * typ -> order
    1.75 +  val typs_ord: typ list * typ list -> order
    1.76 +  val term_ord: term * term -> order
    1.77 +  val terms_ord: term list * term list -> order
    1.78 +  val hd_ord: term * term -> order
    1.79 +  val termless: term * term -> bool
    1.80    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    1.81    val rename_abs: term -> term -> term -> term option
    1.82    val invent_names: string list -> string -> int -> string list
    1.83 @@ -180,13 +188,6 @@
    1.84    val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    1.85    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.86    val add_frees: (string * typ) list * term -> (string * typ) list
    1.87 -  val indexname_ord: indexname * indexname -> order
    1.88 -  val typ_ord: typ * typ -> order
    1.89 -  val typs_ord: typ list * typ list -> order
    1.90 -  val term_ord: term * term -> order
    1.91 -  val terms_ord: term list * term list -> order
    1.92 -  val hd_ord: term * term -> order
    1.93 -  val termless: term * term -> bool
    1.94    val no_dummyT: typ -> typ
    1.95    val dummy_patternN: string
    1.96    val no_dummy_patterns: term -> term
    1.97 @@ -204,7 +205,7 @@
    1.98  
    1.99  (*Indexnames can be quickly renamed by adding an offset to the integer part,
   1.100    for resolution.*)
   1.101 -type indexname = string*int;
   1.102 +type indexname = string * int;
   1.103  
   1.104  (* Types are classified by sorts. *)
   1.105  type class = string;
   1.106 @@ -224,8 +225,6 @@
   1.107    It is possible to create meaningless terms containing loose bound vars
   1.108    or type mismatches.  But such terms are not allowed in rules. *)
   1.109  
   1.110 -
   1.111 -
   1.112  datatype term =
   1.113      Const of string * typ
   1.114    | Free  of string * typ
   1.115 @@ -234,14 +233,12 @@
   1.116    | Abs   of string*typ*term
   1.117    | op $  of term*term;
   1.118  
   1.119 -
   1.120 -(*For errors involving type mismatches*)
   1.121 +(*Errors involving type mismatches*)
   1.122  exception TYPE of string * typ list * term list;
   1.123  
   1.124 -(*For system errors involving terms*)
   1.125 +(*Errors errors involving terms*)
   1.126  exception TERM of string * term list;
   1.127  
   1.128 -
   1.129  (*Note variable naming conventions!
   1.130      a,b,c: string
   1.131      f,g,h: functions (including terms of function type)
   1.132 @@ -256,6 +253,17 @@
   1.133  
   1.134  (** Types **)
   1.135  
   1.136 +(*dummy type for parsing and printing etc.*)
   1.137 +val dummyT = Type ("dummy", []);
   1.138 +
   1.139 +fun no_dummyT typ =
   1.140 +  let
   1.141 +    fun check (T as Type ("dummy", _)) =
   1.142 +          raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   1.143 +      | check (Type (_, Ts)) = List.app check Ts
   1.144 +      | check _ = ();
   1.145 +  in check typ; typ end;
   1.146 +
   1.147  fun S --> T = Type("fun",[S,T]);
   1.148  
   1.149  (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   1.150 @@ -268,6 +276,7 @@
   1.151  fun dest_TFree (TFree x) = x
   1.152    | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   1.153  
   1.154 +
   1.155  (** Discriminators **)
   1.156  
   1.157  fun is_Bound (Bound _) = true
   1.158 @@ -289,6 +298,7 @@
   1.159  fun is_funtype (Type("fun",[_,_])) = true
   1.160    | is_funtype _ = false;
   1.161  
   1.162 +
   1.163  (** Destructors **)
   1.164  
   1.165  fun dest_Const (Const x) =  x
   1.166 @@ -426,6 +436,72 @@
   1.167  in iter end
   1.168  
   1.169  
   1.170 +(** Comparing terms, types etc. **)
   1.171 +
   1.172 +fun indexname_ord ((x, i), (y, j)) =
   1.173 +  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   1.174 +
   1.175 +val sort_ord = list_ord string_ord;
   1.176 +
   1.177 +
   1.178 +(* typ_ord *)
   1.179 +
   1.180 +fun typ_ord TU =
   1.181 +  if pointer_eq TU then EQUAL
   1.182 +  else
   1.183 +    (case TU of
   1.184 +      (Type x, Type y) => prod_ord string_ord typs_ord (x, y)
   1.185 +    | (Type _, _) => GREATER
   1.186 +    | (TFree _, Type _) => LESS
   1.187 +    | (TFree x, TFree y) => prod_ord string_ord sort_ord (x, y)
   1.188 +    | (TFree _, TVar _) => GREATER
   1.189 +    | (TVar _, Type _) => LESS
   1.190 +    | (TVar _, TFree _) => LESS
   1.191 +    | (TVar x, TVar y) => prod_ord indexname_ord sort_ord (x, y))
   1.192 +and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
   1.193 +
   1.194 +
   1.195 +(* term_ord *)
   1.196 +
   1.197 +(*a linear well-founded AC-compatible ordering for terms:
   1.198 +  s < t <=> 1. size(s) < size(t) or
   1.199 +            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   1.200 +            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   1.201 +               (s1..sn) < (t1..tn) (lexicographically)*)
   1.202 +
   1.203 +fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   1.204 +  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   1.205 +  | dest_hd (Var v) = (v, 2)
   1.206 +  | dest_hd (Bound i) = ((("", i), dummyT), 3)
   1.207 +  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   1.208 +
   1.209 +fun term_ord tu =
   1.210 +  if pointer_eq tu then EQUAL
   1.211 +  else
   1.212 +    (case tu of
   1.213 +      (Abs (_, T, t), Abs(_, U, u)) =>
   1.214 +        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   1.215 +      | (t, u) =>
   1.216 +        (case int_ord (size_of_term t, size_of_term u) of
   1.217 +          EQUAL =>
   1.218 +            let
   1.219 +              val (f, ts) = strip_comb t
   1.220 +              and (g, us) = strip_comb u
   1.221 +            in case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord end
   1.222 +        | ord => ord))
   1.223 +and hd_ord (f, g) =
   1.224 +  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   1.225 +and terms_ord (ts, us) = list_ord term_ord (ts, us);
   1.226 +
   1.227 +fun op aconv tu = (term_ord tu = EQUAL);
   1.228 +fun aconvs ts_us = (list_ord term_ord ts_us = EQUAL);
   1.229 +fun termless tu = (term_ord tu = LESS);
   1.230 +
   1.231 +structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
   1.232 +structure Typtab = TableFun(type key = typ val ord = typ_ord);
   1.233 +structure Termtab = TableFun(type key = term val ord = term_ord);
   1.234 +
   1.235 +
   1.236  (** Connectives of higher order logic **)
   1.237  
   1.238  fun itselfT ty = Type ("itself", [ty]);
   1.239 @@ -551,15 +627,6 @@
   1.240  (*insertion into list, optimized version for indexnames*)
   1.241  fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   1.242  
   1.243 -(*Tests whether 2 terms are alpha-convertible and have same type.
   1.244 -  Note that constants may have more than one type.*)
   1.245 -fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   1.246 -  | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
   1.247 -  | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
   1.248 -  | (Bound i)    aconv (Bound j)    = i=j
   1.249 -  | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   1.250 -  | (f$t)        aconv (g$u)        = (f aconv g) andalso (t aconv u)
   1.251 -  | _ aconv _  =  false;
   1.252  
   1.253  (** Membership, insertion, union for terms **)
   1.254  
   1.255 @@ -582,11 +649,6 @@
   1.256    | inter_term (x::xs, ys) =
   1.257        if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
   1.258  
   1.259 -(*are two term lists alpha-convertible in corresponding elements?*)
   1.260 -fun aconvs ([],[]) = true
   1.261 -  | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   1.262 -  | aconvs _ = false;
   1.263 -
   1.264  (*A fast unification filter: true unless the two terms cannot be unified.
   1.265    Terms must be NORMAL.  Treats all Vars as distinct. *)
   1.266  fun could_unify (t,u) =
   1.267 @@ -702,20 +764,20 @@
   1.268  (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   1.269  fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
   1.270  
   1.271 -(*First order means in all terms of the form f(t1,...,tn) no argument has a 
   1.272 -  function type. The meta-quantifier "all" is excluded--its argument always 
   1.273 +(*First order means in all terms of the form f(t1,...,tn) no argument has a
   1.274 +  function type. The meta-quantifier "all" is excluded--its argument always
   1.275    has a function type--through a recursive call into its body.*)
   1.276  fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   1.277 -  | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = 
   1.278 +  | first_order1 Ts (Const("all",_)$Abs(a,T,body)) =
   1.279        not (is_funtype T) andalso first_order1 (T::Ts) body
   1.280    | first_order1 Ts t =
   1.281        case strip_comb t of
   1.282 -	       (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.283 -	     | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.284 -	     | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.285 -	     | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.286 -	     | (Abs _, ts) => false (*not in beta-normal form*)
   1.287 -	     | _ => error "first_order: unexpected case";
   1.288 +               (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.289 +             | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.290 +             | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.291 +             | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.292 +             | (Abs _, ts) => false (*not in beta-normal form*)
   1.293 +             | _ => error "first_order: unexpected case";
   1.294  
   1.295  val is_first_order = first_order1 [];
   1.296  
   1.297 @@ -744,19 +806,6 @@
   1.298  
   1.299  (**** Syntax-related declarations ****)
   1.300  
   1.301 -
   1.302 -(*Dummy type for parsing and printing.  Will be replaced during type inference. *)
   1.303 -val dummyT = Type("dummy",[]);
   1.304 -
   1.305 -fun no_dummyT typ =
   1.306 -  let
   1.307 -    fun check (T as Type ("dummy", _)) =
   1.308 -          raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   1.309 -      | check (Type (_, Ts)) = List.app check Ts
   1.310 -      | check _ = ();
   1.311 -  in check typ; typ end;
   1.312 -
   1.313 -
   1.314  (*** Printing ***)
   1.315  
   1.316  (*Makes a variant of a name distinct from the names in bs.
   1.317 @@ -783,6 +832,7 @@
   1.318          else a :: invent_names used b (n - 1)
   1.319        end;
   1.320  
   1.321 +
   1.322  (** Consts etc. **)
   1.323  
   1.324  fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
   1.325 @@ -906,6 +956,7 @@
   1.326    | add_term_tvar_ixns(f$t,ixns) =
   1.327        add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   1.328  
   1.329 +
   1.330  (** Frees and Vars **)
   1.331  
   1.332  (*a partial ordering (not reflexive) for atomic terms*)
   1.333 @@ -996,60 +1047,6 @@
   1.334  fun term_varnames t = add_term_varnames ([], t);
   1.335  
   1.336  
   1.337 -(** type and term orders **)
   1.338 -
   1.339 -fun indexname_ord ((x, i), (y, j)) =
   1.340 -  (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
   1.341 -
   1.342 -val sort_ord = list_ord String.compare;
   1.343 -
   1.344 -
   1.345 -(* typ_ord *)
   1.346 -
   1.347 -fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
   1.348 -  | typ_ord (Type _, _) = GREATER
   1.349 -  | typ_ord (TFree _, Type _) = LESS
   1.350 -  | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
   1.351 -  | typ_ord (TFree _, TVar _) = GREATER
   1.352 -  | typ_ord (TVar _, Type _) = LESS
   1.353 -  | typ_ord (TVar _, TFree _) = LESS
   1.354 -  | typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y)
   1.355 -and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
   1.356 -
   1.357 -
   1.358 -(* term_ord *)
   1.359 -
   1.360 -(*a linear well-founded AC-compatible ordering for terms:
   1.361 -  s < t <=> 1. size(s) < size(t) or
   1.362 -            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   1.363 -            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   1.364 -               (s1..sn) < (t1..tn) (lexicographically)*)
   1.365 -
   1.366 -fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   1.367 -  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   1.368 -  | dest_hd (Var v) = (v, 2)
   1.369 -  | dest_hd (Bound i) = ((("", i), dummyT), 3)
   1.370 -  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   1.371 -
   1.372 -fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
   1.373 -      (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   1.374 -  | term_ord (t, u) =
   1.375 -      (case Int.compare (size_of_term t, size_of_term u) of
   1.376 -        EQUAL =>
   1.377 -          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   1.378 -            (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
   1.379 -          end
   1.380 -      | ord => ord)
   1.381 -and hd_ord (f, g) =
   1.382 -  prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
   1.383 -and terms_ord (ts, us) = list_ord term_ord (ts, us);
   1.384 -
   1.385 -fun termless tu = (term_ord tu = LESS);
   1.386 -
   1.387 -structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
   1.388 -structure Typtab = TableFun(type key = typ val ord = typ_ord);
   1.389 -structure Termtab = TableFun(type key = term val ord = term_ord);
   1.390 -
   1.391  
   1.392  (*** Compression of terms and types by sharing common subtrees.
   1.393       Saves 50-75% on storage requirements.  As it is a bit slow,