1(* Title: Pure/more_pattern.ML 2 Author: Tobias Nipkow, TU Muenchen 3 Author: Stefan Berghofer, TU Muenchen 4 5Add-ons to Higher-Order Patterns, outside the inference kernel. 6*) 7 8signature PATTERN = 9sig 10 include PATTERN 11 val matches: theory -> term * term -> bool 12 val matchess: theory -> term list * term list -> bool 13 val equiv: theory -> term * term -> bool 14 val first_order: term -> bool 15 val match_rew: theory -> term -> term * term -> (term * term) option 16 val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term 17 val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term 18end; 19 20structure Pattern: PATTERN = 21struct 22 23fun matches thy po = 24 (Pattern.match thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false; 25 26fun matchess thy (ps, os) = 27 length ps = length os andalso 28 ((fold (Pattern.match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) 29 handle Pattern.MATCH => false); 30 31fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t); 32 33fun first_order (Abs (_, _, t)) = first_order t 34 | first_order (Var _ $ _) = false 35 | first_order (t $ u) = first_order t andalso first_order u 36 | first_order _ = true; 37 38 39(* rewriting -- simple but fast *) 40 41fun match_rew thy tm (tm1, tm2) = 42 let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in 43 SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm) 44 handle Pattern.MATCH => NONE 45 end; 46 47fun gen_rewrite_term bot thy rules procs tm = 48 let 49 val skel0 = Bound 0; 50 51 fun variant_absfree bounds (x, T, t) = 52 let 53 val (x', t') = Term.dest_abs (Name.bound bounds, T, t); 54 fun abs u = Abs (x, T, abstract_over (Free (x', T), u)); 55 in (abs, t') end; 56 57 fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0) 58 | rew tm = 59 (case get_first (match_rew thy tm) rules of 60 NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs) 61 | x => x); 62 63 fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of 64 Abs (_, _, body) => 65 let val tm' = subst_bound (tm2, body) 66 in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end 67 | _ => 68 let val (skel1, skel2) = (case skel of 69 skel1 $ skel2 => (skel1, skel2) 70 | _ => (skel0, skel0)) 71 in case r bounds skel1 tm1 of 72 SOME tm1' => (case r bounds skel2 tm2 of 73 SOME tm2' => SOME (tm1' $ tm2') 74 | NONE => SOME (tm1' $ tm2)) 75 | NONE => (case r bounds skel2 tm2 of 76 SOME tm2' => SOME (tm1 $ tm2') 77 | NONE => NONE) 78 end) 79 | rew_sub r bounds skel (Abs body) = 80 let 81 val (abs, tm') = variant_absfree bounds body; 82 val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0) 83 in case r (bounds + 1) skel' tm' of 84 SOME tm'' => SOME (abs tm'') 85 | NONE => NONE 86 end 87 | rew_sub _ _ _ _ = NONE; 88 89 fun rew_bot bounds (Var _) _ = NONE 90 | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of 91 SOME tm1 => (case rew tm1 of 92 SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2)) 93 | NONE => SOME tm1) 94 | NONE => (case rew tm of 95 SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1)) 96 | NONE => NONE)); 97 98 fun rew_top bounds _ tm = (case rew tm of 99 SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of 100 SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2)) 101 | NONE => SOME tm1) 102 | NONE => (case rew_sub rew_top bounds skel0 tm of 103 SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1)) 104 | NONE => NONE)); 105 106 in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end; 107 108val rewrite_term = gen_rewrite_term true; 109val rewrite_term_top = gen_rewrite_term false; 110 111 112open Pattern; 113 114end; 115