tuned term_ord: less garbage;
authorwenzelm
Fri Jul 01 22:35:20 2005 +0200 (2005-07-01)
changeset 16667f56080acd176
parent 16666 9a987b59ecab
child 16668 fdb4992cf1d2
tuned term_ord: less garbage;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Jul 01 22:34:50 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Jul 01 22:35:20 2005 +0200
     1.3 @@ -176,7 +176,6 @@
     1.4    val typ_ord: typ * typ -> order
     1.5    val typs_ord: typ list * typ list -> order
     1.6    val term_ord: term * term -> order
     1.7 -  val terms_ord: term list * term list -> order
     1.8    val hd_ord: term * term -> order
     1.9    val termless: term * term -> bool
    1.10    val term_lpo: (string -> int) -> term * term -> order
    1.11 @@ -474,6 +473,10 @@
    1.12              2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
    1.13              3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
    1.14                 (s1..sn) < (t1..tn) (lexicographically)*)
    1.15 +local
    1.16 +
    1.17 +fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
    1.18 +  | hd_depth p = p;
    1.19  
    1.20  fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
    1.21    | dest_hd (Free (a, T)) = (((a, 0), T), 1)
    1.22 @@ -481,30 +484,46 @@
    1.23    | dest_hd (Bound i) = ((("", i), dummyT), 3)
    1.24    | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
    1.25  
    1.26 +in
    1.27 +
    1.28  fun term_ord tu =
    1.29    if pointer_eq tu then EQUAL
    1.30    else
    1.31      (case tu of
    1.32        (Abs (_, T, t), Abs(_, U, u)) =>
    1.33          (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.34 -      | (t, u) =>
    1.35 +    | (t, u) =>
    1.36          (case int_ord (size_of_term t, size_of_term u) of
    1.37            EQUAL =>
    1.38              let
    1.39 -              val (f, ts) = strip_comb t
    1.40 -              and (g, us) = strip_comb u
    1.41 -            in case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord end
    1.42 +              val (f, m) = hd_depth (t, 0)
    1.43 +              and (g, n) = hd_depth (u, 0);
    1.44 +            in
    1.45 +              (case hd_ord (f, g) of EQUAL =>
    1.46 +                (case int_ord (m, n) of EQUAL => args_ord (t, u) | ord => ord)
    1.47 +              | ord => ord)
    1.48 +            end
    1.49          | ord => ord))
    1.50  and hd_ord (f, g) =
    1.51    prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
    1.52 -and terms_ord (ts, us) = list_ord term_ord (ts, us);
    1.53 +and args_ord (f $ t, g $ u) =
    1.54 +      (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
    1.55 +  | args_ord _ = EQUAL;
    1.56  
    1.57  fun op aconv tu = (term_ord tu = EQUAL);
    1.58  fun aconvs ts_us = (list_ord term_ord ts_us = EQUAL);
    1.59  fun termless tu = (term_ord tu = LESS);
    1.60  
    1.61 -(*** Lexicographic path order on terms.
    1.62 +structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
    1.63 +structure Typtab = TableFun(type key = typ val ord = typ_ord);
    1.64 +structure Termtab = TableFun(type key = term val ord = term_ord);
    1.65  
    1.66 +end;
    1.67 +
    1.68 +
    1.69 +(** Lexicographic path order on terms **)
    1.70 +
    1.71 +(*
    1.72    See Baader & Nipkow, Term rewriting, CUP 1998.
    1.73    Without variables.  Const, Var, Bound, Free and Abs are treated all as
    1.74    constants.
    1.75 @@ -515,10 +534,10 @@
    1.76    - Order on the recognised symbols.  These must be mapped to distinct
    1.77      integers >= 0.
    1.78  
    1.79 -***)
    1.80 +*)
    1.81  
    1.82  local
    1.83 -fun dest_hd f_ord (Const (a, T)) = 
    1.84 +fun dest_hd f_ord (Const (a, T)) =
    1.85        let val ord = f_ord a in
    1.86          if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    1.87        end
    1.88 @@ -531,13 +550,13 @@
    1.89    let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
    1.90      if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
    1.91      then case hd_ord f_ord (f, g) of
    1.92 -	GREATER =>
    1.93 -	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.94 -	  then GREATER else LESS
    1.95 +        GREATER =>
    1.96 +          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.97 +          then GREATER else LESS
    1.98        | EQUAL =>
    1.99 -	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   1.100 -	  then list_ord (term_lpo f_ord) (ss, ts)
   1.101 -	  else LESS
   1.102 +          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   1.103 +          then list_ord (term_lpo f_ord) (ss, ts)
   1.104 +          else LESS
   1.105        | LESS => LESS
   1.106      else GREATER
   1.107    end
   1.108 @@ -551,10 +570,6 @@
   1.109  val term_lpo = term_lpo
   1.110  end;
   1.111  
   1.112 -structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
   1.113 -structure Typtab = TableFun(type key = typ val ord = typ_ord);
   1.114 -structure Termtab = TableFun(type key = term val ord = term_ord);
   1.115 -
   1.116  
   1.117  (** Connectives of higher order logic **)
   1.118  
   1.119 @@ -821,19 +836,19 @@
   1.120  (*First order means in all terms of the form f(t1,...,tn) no argument has a
   1.121    function type. The supplied quantifiers are excluded: their argument always
   1.122    has a function type through a recursive call into its body.*)
   1.123 -fun is_first_order quants = 
   1.124 +fun is_first_order quants =
   1.125    let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   1.126 -	| first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   1.127 -	    q mem_string quants  andalso   (*it is a known quantifier*)
   1.128 +        | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   1.129 +            q mem_string quants  andalso   (*it is a known quantifier*)
   1.130              not (is_funtype T)   andalso first_order1 (T::Ts) body
   1.131 -	| first_order1 Ts t =
   1.132 -	    case strip_comb t of
   1.133 -		 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.134 -	       | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.135 -	       | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.136 -	       | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.137 -	       | (Abs _, ts) => false (*not in beta-normal form*)
   1.138 -	       | _ => error "first_order: unexpected case"
   1.139 +        | first_order1 Ts t =
   1.140 +            case strip_comb t of
   1.141 +                 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.142 +               | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.143 +               | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.144 +               | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   1.145 +               | (Abs _, ts) => false (*not in beta-normal form*)
   1.146 +               | _ => error "first_order: unexpected case"
   1.147      in  first_order1 []  end;
   1.148  
   1.149  (*Computing the maximum index of a typ*)