Quelle more_pattern.ML Sprache: SML

(*  Title:      Pure/more_pattern.ML
    Author:     Tobias Nipkow, TU Muenchen
    Author:     Stefan Berghofer, TU Muenchen

Add-ons to Higher-Order Patterns, outside the inference kernel.
*)

signature PATTERN =
sig
  include PATTERN
  val matches: theory -> term * term -> bool
  val matchess: theory -> term list * term list -> bool
  val equiv: theory -> term * term -> bool
  val first_order: term -> bool
  val match_rew: theory -> term -> term * term -> (term * term) option
  val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
  val rewrite_term_topdown: theory -> (term * term) list -> (term -> term option) list -> term -> term
  val rewrite_term_yoyo: theory -> (term * term) list -> (term -> term option) list -> term -> term
end;

structure Pattern: PATTERN =
struct

fun matches thy po =
  (Pattern.match thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;

fun matchess thy (ps, os) =
  length ps = length os andalso
    ((fold (Pattern.match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true)
      handle Pattern.MATCH => false);

fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);

fun first_order (Abs (_, _, t)) = first_order t
  | first_order (Var _ $ _) = false
  | first_order (t $ u) = first_order t andalso first_order u
  | first_order _ = true;

(* rewriting -- simple but fast *)

fun match_rew thy tm (tm1, tm2) =
  let val rtm = perhaps (Term.rename_abs tm1 tm) tm2 in
    SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
      handle Pattern.MATCH => NONE
  end;

local

val skel0 = Bound 0;
val skel_fun = fn skel $ _ => skel | _ => skel0;
val skel_arg = fn _ $ skel => skel | _ => skel0;
val skel_body = fn Abs (_, _, skel) => skel | _ => skel0;

datatype mode = Bottom | Top | Yoyo;

fun rewrite_term_mode mode thy rules procs =
  let
    fun variant_absfree bounds x tm =
      let
        val ((x', T), t') =
          Term.dest_abs_fresh (Name.bound bounds) tm
            handle Term.USED_FREE _ => Term.dest_abs_global tm;  (* FIXME proper context *)
        fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
      in (abs, t') end;

    fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
      | rew tm =
          (case get_first (match_rew thy tm) rules of
            NONE => Option.map (rpair skel0) (get_first (fn proc => proc tm) procs)
          | some => some);

    fun rew_sub rw bounds _ (Abs (_, _, body) $ t) =
          let val t' = subst_bound (t, body)
          in SOME (perhaps (rew_sub rw bounds skel0) t') end
      | rew_sub rw bounds skel (t $ u) =
          (case (rw bounds (skel_fun skel) t, rw bounds (skel_arg skel) u) of
            (SOME t', SOME u') => SOME (t' $ u')
          | (SOME t', NONE) => SOME (t' $ u)
          | (NONE, SOME u') => SOME (t $ u')
          | (NONE, NONE) => NONE)
      | rew_sub rw bounds skel (t as Abs (x, _, _)) =
          let val (abs, t') = variant_absfree bounds x t
          in Option.map abs (rw (bounds + 1) (skel_body skel) t') end
      | rew_sub _ _ _ _ = NONE;

    (* bottom-up with skeleton *)

    fun rew_bottom _ (Var _) _ = NONE
      | rew_bottom bounds skel t =
          (case rew_sub rew_bottom bounds skel t of
            SOME t1 =>
              (case rew t1 of
                SOME (t2, skel') => SOME (perhaps (rew_bottom bounds skel') t2)
              | NONE => SOME t1)
          | NONE =>
              (case rew t of
                SOME (t1, skel') => SOME (perhaps (rew_bottom bounds skel') t1)
              | NONE => NONE));

    (* top-down *)

    fun rew_top bounds _ t =
      (case rew t of
        SOME (t1, _) =>
          (case rew_sub rew_top bounds skel0 t1 of
            SOME t2 => SOME (perhaps (rew_top bounds skel0) t2)
          | NONE => SOME t1)
      | NONE =>
          (case rew_sub rew_top bounds skel0 t of
            SOME t1 => SOME (perhaps (rew_top bounds skel0) t1)
          | NONE => NONE));

    (* yoyo: see also Ast.normalize *)

    val rew_yoyo1 = perhaps_loop (rew #> Option.map #1);

    fun rew_yoyo2 bounds _ t =
      (case rew_yoyo1 t of
        SOME t1 =>
          (case rew_sub rew_yoyo2 bounds skel0 t1 of
            SOME t2 => SOME (perhaps rew_yoyo1 t2)
          | NONE => SOME t1)
      | NONE =>
          (case rew_sub rew_yoyo2 bounds skel0 t of
            SOME t1 => SOME (perhaps rew_yoyo1 t1)
          | NONE => NONE));

    fun rew_yoyo bounds skel = perhaps_loop (rew_yoyo2 bounds skel);
  in
    perhaps ((case mode of Bottom => rew_bottom | Top => rew_top | Yoyo => rew_yoyo) 0 skel0)
  end;

in

val rewrite_term = rewrite_term_mode Bottom;
val rewrite_term_topdown = rewrite_term_mode Top;
val rewrite_term_yoyo = rewrite_term_mode Yoyo;

end;

open Pattern;

end;

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.