From 65f242ec6a8ed31dbd4b3e3664ca28f361364827 Mon Sep 17 00:00:00 2001
From: Bart Wijgers <bartwijgers@hotmail.com>
Date: Sat, 28 Sep 2019 22:20:25 +0200
Subject: [PATCH] Add "normalizeProgramPath" to WLP.ProgramPath
Some functions seem to assume that the program paths are formed by a
fully left-associative application of the Seq constructor (as in: Seq
Skip $ Seq Skip $ ... $ Seq Skip Skip). Therefore, this function is
added; it will turn any string of Seq'ed statements into this shape.
Using this function will do no harm (other than possibly spending effort
into doing nothing), so use it accordingly.
---
src/WLP/ProgramPath.hs | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/src/WLP/ProgramPath.hs b/src/WLP/ProgramPath.hs
index f8e1d29..d36df2d 100644
--- a/src/WLP/ProgramPath.hs
+++ b/src/WLP/ProgramPath.hs
@@ -2,6 +2,7 @@ module WLP.ProgramPath
( ProgramPath
, getProgramPaths
, PathLength
+ , normalizeProgramPath
)
where
@@ -159,3 +160,13 @@ unrollWhile g ml s = uw' g ml s []
[] -> []
xs -> (xs ++ uw' g ml s xs)
+-- | Normalizes a program path. This changes all instances of `Seq (Seq s1 s2)
+-- s3` into `Seq s1 (Seq s2 s3)`, which should avoid a bunch of error later on.
+normalizeProgramPath :: ProgramPath -> ProgramPath
+normalizeProgramPath (Seq (Seq s1 s2) s3)
+ = let n1 = normalizeProgramPath s1
+ n2 = normalizeProgramPath s2
+ n3 = normalizeProgramPath s3
+ in Seq n1 (Seq n2 n3)
+normalizeProgramPath x = x
+
--
GitLab