Added term cache to function condrew in order to speed up rewriting.
authorberghofe
Fri Dec 10 16:57:01 2004 +0100 (2004-12-10)
changeset 15399683d83051d6a
parent 15398 055c01162eaa
child 15400 50bbdabd7326
Added term cache to function condrew in order to speed up rewriting.
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Dec 10 16:55:58 2004 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Dec 10 16:57:01 2004 +0100
     1.3 @@ -94,22 +94,32 @@
     1.4  
     1.5      fun rew tm =
     1.6        Pattern.rewrite_term tsig [] (condrew' :: procs) tm
     1.7 -    and condrew' tm = get_first (fn (_, (prems, (tm1, tm2))) =>
     1.8 +    and condrew' tm =
     1.9        let
    1.10 -        fun ren t = if_none (Term.rename_abs tm1 tm t) t;
    1.11 -        val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    1.12 -        val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
    1.13 -        val prems' = map (pairself (subst_vars env o inc o ren)) prems;
    1.14 -        val env' = Envir.Envir
    1.15 -          {maxidx = foldl Int.max
    1.16 -            (~1, map (Int.max o pairself maxidx_of_term) prems'),
    1.17 -           iTs = Vartab.make Tenv, asol = Vartab.make tenv};
    1.18 -        val env'' = foldl (fn (env, p) =>
    1.19 -          Pattern.unify (sign, env, [pairself rew p])) (env', prems')
    1.20 -      in Some (Envir.norm_term env'' (inc (ren tm2)))
    1.21 -      end handle Pattern.MATCH => None | Pattern.Unif => None)
    1.22 -        (sort (Int.compare o pairself fst)
    1.23 -          (Net.match_term rules (Pattern.eta_contract tm)));
    1.24 +        val cache = ref ([] : (term * term) list);
    1.25 +        fun lookup f x = (case assoc (!cache, x) of
    1.26 +            None =>
    1.27 +              let val y = f x
    1.28 +              in (cache := (x, y) :: !cache; y) end
    1.29 +          | Some y => y);
    1.30 +      in
    1.31 +        get_first (fn (_, (prems, (tm1, tm2))) =>
    1.32 +        let
    1.33 +          fun ren t = if_none (Term.rename_abs tm1 tm t) t;
    1.34 +          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    1.35 +          val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
    1.36 +          val prems' = map (pairself (subst_vars env o inc o ren)) prems;
    1.37 +          val env' = Envir.Envir
    1.38 +            {maxidx = foldl Int.max
    1.39 +              (~1, map (Int.max o pairself maxidx_of_term) prems'),
    1.40 +             iTs = Vartab.make Tenv, asol = Vartab.make tenv};
    1.41 +          val env'' = foldl (fn (env, p) =>
    1.42 +            Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
    1.43 +        in Some (Envir.norm_term env'' (inc (ren tm2)))
    1.44 +        end handle Pattern.MATCH => None | Pattern.Unif => None)
    1.45 +          (sort (Int.compare o pairself fst)
    1.46 +            (Net.match_term rules (Pattern.eta_contract tm)))
    1.47 +      end;
    1.48  
    1.49    in rew end;
    1.50