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

@@ -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
+