Small Rew module in which we tested rewriting with an algebraic data type
authorNorman Ramsey <nr@cs.tufts.edu>
Tue, 27 Jul 2010 02:58:20 +0000 (22:58 -0400)
committerNorman Ramsey <nr@cs.tufts.edu>
Tue, 27 Jul 2010 02:58:20 +0000 (22:58 -0400)
paper/.gitignore
paper/Rew.hs [new file with mode: 0644]

index 6ff8592..b6c880e 100644 (file)
@@ -6,6 +6,8 @@ oodfopt.tex
 nrbib.tex
 _darcs
 *~
+*.hi
+*.o
 
 dfopt.txt
 dfoptdu.tex
diff --git a/paper/Rew.hs b/paper/Rew.hs
new file mode 100644 (file)
index 0000000..d4bf3c6
--- /dev/null
@@ -0,0 +1,46 @@
+module Rew
+where
+
+data Rew a = No
+           | Mk a
+           | Then (Rew a) (Rew a)
+           | Iter (Rew a)
+
+rewrite :: Rew (node -> fact -> Maybe graph)
+        -> node -> fact -> Maybe (graph, Rew (node -> fact -> Maybe graph))
+rewrite_direct rs n f = rew rs
+    where rew No       = Nothing
+          rew (Mk r)   =
+              case r n f of Nothing -> Nothing
+                            Just g -> Just (g, No)
+          rew (r1 `Then` r2) =
+              case rew r1 of
+                Nothing -> rew r2
+                Just (g, r1') -> Just (g, r1' `Then` r2)
+          rew (Iter r) =
+              case rew r of
+                Nothing -> Nothing
+                Just (g, r') -> Just (g, r' `Then` Iter r)
+
+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 (j . add r2) (rew r2 j n)
+  rew (Iter r)       j n = rew r (j . add (Iter r)) n
+  add tail (g, r) = (g, r `Then` tail)
+
+rewritem :: Monad m => Rew (node -> fact -> m (Maybe graph))
+         -> node -> fact -> m (Maybe (graph, Rew (node -> fact -> m (Maybe graph))))
+rewritem rs node f = rew rs (return . Just) (return Nothing)
+ where
+  rew No     j n = n
+  rew (Mk r) j n = do mg <- r node f
+                      case mg of Nothing -> n
+                                 Just g -> j (g, No)
+  rew (r1 `Then` r2) j n = rew r1 (j . add r2) (rew r2 j n)
+  rew (Iter r)       j n = rew r (j . add (Iter r)) n
+  add tail (g, r) = (g, r `Then` tail)
+