rewrite: tuned code, no semantic changes
authornoschinl
Tue Apr 14 08:42:16 2015 +0200 (2015-04-14)
changeset 60055aa3d2a6dd99e
parent 60054 ef4878146485
child 60056 71c1b9b9e937
rewrite: tuned code, no semantic changes
src/HOL/Library/rewrite.ML
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 20:11:12 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Tue Apr 14 08:42:16 2015 +0200
     1.3 @@ -164,36 +164,22 @@
     1.4    then ft_arg ctxt ft
     1.5    else ft
     1.6  
     1.7 -
     1.8 -(* Return a lazy sequenze of all subterms of the focusterm for which
     1.9 -   the condition holds. *)
    1.10 -fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
    1.11 +(* Find all subterms that might be a valid point to apply a rule. *)
    1.12 +fun valid_match_points ctxt (ft : focusterm) =
    1.13    let
    1.14 -    val recurse = find_subterms ctxt condition
    1.15 -    val recursive_matches =
    1.16 -      case t of
    1.17 -        _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
    1.18 -      | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
    1.19 -      | _ => Seq.empty
    1.20 -  in
    1.21 -    (* If the condition is met, then the current focusterm is part of the
    1.22 -       sequence of results. Otherwise, only the results of the recursive
    1.23 -       application are. *)
    1.24 -    if condition ft
    1.25 -    then Seq.cons ft recursive_matches
    1.26 -    else recursive_matches
    1.27 -  end
    1.28 -
    1.29 -(* Find all subterms that might be a valid point to apply a rule. *)
    1.30 -fun valid_match_points ctxt =
    1.31 -  let
    1.32 +    fun descend (_, _ $ _, _) = [ft_fun ctxt, ft_arg ctxt]
    1.33 +      | descend (_, Abs (_, T, _), _) = [ft_abs ctxt (NONE, T)]
    1.34 +      | descend _ = []
    1.35 +    fun subseq ft =
    1.36 +      descend ft |> Seq.of_list |> Seq.maps (fn f => ft |> f |> valid_match_points ctxt)
    1.37      fun is_valid (l $ _) = is_valid l
    1.38        | is_valid (Abs (_, _, a)) = is_valid a
    1.39        | is_valid (Var _) = false
    1.40        | is_valid (Bound _) = false
    1.41        | is_valid _ = true
    1.42    in
    1.43 -    find_subterms ctxt (#2 #> is_valid )
    1.44 +    Seq.make (fn () => SOME (ft, subseq ft))
    1.45 +    |> Seq.filter (#2 #> is_valid)
    1.46    end
    1.47  
    1.48  fun is_hole (Var ((name, _), _)) = (name = holeN)