From 1c34714ef4dc34f6d795e23b9977fd7c1a324234 Mon Sep 17 00:00:00 2001
From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Date: Thu, 20 Apr 2017 11:05:16 +0200
Subject: [PATCH] compute normal forms w.r.t. given strategy

---
 src/Data/Rewriting/Problem/Type.hs  | 2 ++
 src/Data/Rewriting/Rules/Rewrite.hs | 8 ++++++++
 2 files changed, 10 insertions(+)

diff --git a/src/Data/Rewriting/Problem/Type.hs b/src/Data/Rewriting/Problem/Type.hs
index d76461a..bed4f5d 100644
--- a/src/Data/Rewriting/Problem/Type.hs
+++ b/src/Data/Rewriting/Problem/Type.hs
@@ -19,6 +19,8 @@ import qualified Prelude as P
 import Data.Rewriting.Rule (Rule (..))
 import qualified Data.Rewriting.Rule as Rule
 
+import Control.Applicative
+
 data StartTerms = AllTerms
                 | BasicTerms deriving (Eq, Show)
 
diff --git a/src/Data/Rewriting/Rules/Rewrite.hs b/src/Data/Rewriting/Rules/Rewrite.hs
index 101285e..251b3ee 100644
--- a/src/Data/Rewriting/Rules/Rewrite.hs
+++ b/src/Data/Rewriting/Rules/Rewrite.hs
@@ -17,6 +17,7 @@ module Data.Rewriting.Rules.Rewrite (
     outerRewrite,
     innerRewrite,
     rootRewrite,
+    normalForms,
     -- * utilities not reexported from "Data.Rewriting.Rules"
     nested,
     listContexts,
@@ -93,3 +94,10 @@ listContexts :: [a] -> [(Int, a -> [a], a)]
 listContexts = go 0 id where
     go !n f [] = []
     go !n f (x:xs) = (n, f . (: xs), x) : go (n+1) (f . (x:)) xs
+
+-- | Compute normal forms: Apply a rewriting strategy until no further steps are
+-- possible, collecting all reducts that are themselves irreducible.
+normalForms :: Strategy f v v' -> Term f v -> [Term f v]
+normalForms s t = go [t] where
+    go ts = let rss = fmap s ts in
+       [t | (t, []) <- zip ts rss] ++ go (rss >>= fmap result)