Added term_lpo
authornipkow
Sat Jun 25 16:07:55 2005 +0200 (2005-06-25)
changeset 16570861b9fa2c98c
parent 16569 a12992c34c12
child 16571 c1f41c98fd3c
Added term_lpo
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Sat Jun 25 16:07:13 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Sat Jun 25 16:07:55 2005 +0200
     1.3 @@ -179,6 +179,7 @@
     1.4    val terms_ord: term list * term list -> order
     1.5    val hd_ord: term * term -> order
     1.6    val termless: term * term -> bool
     1.7 +  val term_lpo: (string -> int) -> term * term -> order
     1.8    val match_bvars: (term * term) * (string * string) list -> (string * string) list
     1.9    val rename_abs: term -> term -> term -> term option
    1.10    val invent_names: string list -> string -> int -> string list
    1.11 @@ -497,6 +498,54 @@
    1.12  fun aconvs ts_us = (list_ord term_ord ts_us = EQUAL);
    1.13  fun termless tu = (term_ord tu = LESS);
    1.14  
    1.15 +(*** Lexicographic path order on terms.
    1.16 +
    1.17 +  See Baader & Nipkow, Term rewriting, CUP 1998.
    1.18 +  Without variables.  Const, Var, Bound, Free and Abs are treated all as
    1.19 +  constants.
    1.20 +
    1.21 +  f_ord maps strings to integers and serves two purposes:
    1.22 +  - Predicate on constant symbols.  Those that are not recognised by f_ord
    1.23 +    must be mapped to ~1.
    1.24 +  - Order on the recognised symbols.  These must be mapped to distinct
    1.25 +    integers >= 0.
    1.26 +
    1.27 +***)
    1.28 +
    1.29 +local
    1.30 +fun dest_hd f_ord (Const (a, T)) = 
    1.31 +      let val ord = f_ord a in
    1.32 +        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    1.33 +      end
    1.34 +  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    1.35 +  | dest_hd _ (Var v) = ((1, v), 1)
    1.36 +  | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
    1.37 +  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    1.38 +
    1.39 +fun term_lpo f_ord (s, t) =
    1.40 +  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
    1.41 +    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
    1.42 +    then case hd_ord f_ord (f, g) of
    1.43 +	GREATER =>
    1.44 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.45 +	  then GREATER else LESS
    1.46 +      | EQUAL =>
    1.47 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.48 +	  then list_ord (term_lpo f_ord) (ss, ts)
    1.49 +	  else LESS
    1.50 +      | LESS => LESS
    1.51 +    else GREATER
    1.52 +  end
    1.53 +and hd_ord f_ord (f, g) = case (f, g) of
    1.54 +    (Abs (_, T, t), Abs (_, U, u)) =>
    1.55 +      (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.56 +  | (_, _) => prod_ord (prod_ord int_ord
    1.57 +                  (prod_ord indexname_ord typ_ord)) int_ord
    1.58 +                (dest_hd f_ord f, dest_hd f_ord g)
    1.59 +in
    1.60 +val term_lpo = term_lpo
    1.61 +end;
    1.62 +
    1.63  structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
    1.64  structure Typtab = TableFun(type key = typ val ord = typ_ord);
    1.65  structure Termtab = TableFun(type key = term val ord = term_ord);