author Norman Ramsey Mon, 26 Jul 2010 18:24:25 +0000 (14:24 -0400) committer Norman Ramsey Mon, 26 Jul 2010 18:24:25 +0000 (14:24 -0400)
 paper/dfopt.tex patch | blob | history

index bfd0fa6..85d48b6 100644 (file)
@@ -1732,6 +1732,19 @@ When we apply a rewrite function to a node and a fact,
we choose the first function in the sequence that returns $@Just@\;g$,
and we recursively analyze and rewrite~$g$ using the remaining
functions in the sequence.
+\begin{smallcode}
+rewrite :: FwdRewrite' n f -> -> n e x -> f
+        -> Maybe (Graph n e x, FwdRewrite' n f)
+rewrite rs node f = rew rs Just Nothing
+ where
+  rew No     j n = n
+  rew (Mk r) j n =
+     case r node f of Nothing -> n
+                      Just g -> j (g, No)
+  rew (r1 Then r2) j n = rew r1 (plus j r2) (rew r2 j n)
+  rew (Iter r)       j n = rew r (plus j (Iter r)) n
+  plus j tail (g, r) = j (g, r Then tail)
+\end{smallcode}
If~all functions in the sequence return @Nothing@, rewriting returns
@Nothing@.
The~model works because we needn't \emph{actually} check an infinite