{-# OPTIONS -XNoMonomorphismRestriction #-} module SNOCREV (inv_Freverse,reverse) where import Control.Monad import InvUtil import Data.Tuple import MyData inv_Freverse = runI . e_Freverse data StatesOfFreverse e_1 e_5 e_7 e_8 e_9 = S_Freverse_1 e_1 | S_Freverse_5 e_5 | S_Freverse_7 e_7 | S_Freverse_8 e_8 | S_Freverse_9 e_9 e_Freverse x = case trav_Freverse_0 x of S_Freverse_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: Freverse" trav_Freverse_0 (Nil) = sem_Freverse_0_Nil Nil trav_Freverse_0 (Cons t1 t2) = sem_Freverse_0_Cons (Cons t1 t2) (trav_Freverse_2 t1) (trav_Freverse_1 t2) trav_Freverse_0 t = sem_Freverse_0___ t trav_Freverse_1 (Nil) = sem_Freverse_1_Nil Nil trav_Freverse_1 (Cons t1 t2) = sem_Freverse_1_Cons (Cons t1 t2) (trav_Freverse_2 t1) (trav_Freverse_1 t2) trav_Freverse_1 t = sem_Freverse_1___ t trav_Freverse_2 t = sem_Freverse_2___ t sem_Freverse_0_Cons tree (S_Freverse_9 t1) (S_Freverse_8 t2) = S_Freverse_1 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_2 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v11, r_v21, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E8) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Cons r_v1 r_v3) r_v2)) >=> (\(r_v1, r_v2) -> return (Cons r_v1 r_v2))) tmp_r1 tmp_r2)) t1 t2) sem_Freverse_0_Cons tree (S_Freverse_9 t1) (S_Freverse_7 t2) = S_Freverse_1 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) () -> return (r_v11)) ((\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E8) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) Nil r_v1)) >=> (\(r_v1, r_v2) -> return (Cons r_v1 r_v2))) tmp_r1 tmp_r2)) t1 t2) sem_Freverse_0_Nil tree = S_Freverse_1 (return () >>= (\() -> return Nil)) sem_Freverse_0___ tree = S_Freverse_5 undefined sem_Freverse_1_Cons tree (S_Freverse_9 t1) (S_Freverse_8 t2) = S_Freverse_8 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_2 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v11, r_v21, r_v22)) (\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Cons r_v1 r_v3) r_v2)) tmp_r1 tmp_r2)) t1 t2) sem_Freverse_1_Cons tree (S_Freverse_9 t1) (S_Freverse_7 t2) = S_Freverse_8 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) () -> return (r_v11)) (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) Nil r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_Freverse_1_Nil tree = S_Freverse_7 (return ()) sem_Freverse_1___ tree = S_Freverse_5 undefined sem_Freverse_2___ tree = S_Freverse_9 (return tree, return tree) data StatesOfE8 e_1 e_5 e_7 e_8 e_9 = S_E8_1 e_1 | S_E8_5 e_5 | S_E8_7 e_7 | S_E8_8 e_8 | S_E8_9 e_9 e_E8 x = case trav_E8_0 x of S_E8_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E8" trav_E8_0 (Nil) = sem_E8_0_Nil Nil trav_E8_0 (Cons t1 t2) = sem_E8_0_Cons (Cons t1 t2) (trav_E8_2 t1) (trav_E8_1 t2) trav_E8_0 t = sem_E8_0___ t trav_E8_1 (Nil) = sem_E8_1_Nil Nil trav_E8_1 (Cons t1 t2) = sem_E8_1_Cons (Cons t1 t2) (trav_E8_2 t1) (trav_E8_1 t2) trav_E8_1 t = sem_E8_1___ t trav_E8_2 t = sem_E8_2___ t sem_E8_0_Cons tree (S_E8_9 t1) (S_E8_8 t2) = S_E8_1 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_2 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v11, r_v21, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E8) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Cons r_v1 r_v3) r_v2)) >=> (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (Cons r_v1 r_v2))) tmp_r1 tmp_r2)) t1 t2) sem_E8_0_Cons tree (S_E8_9 t1) (S_E8_7 t2) = S_E8_1 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) () -> return (r_v11)) ((\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E8) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) Nil r_v1)) >=> (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (Cons r_v1 r_v2))) tmp_r1 tmp_r2)) t1 t2) sem_E8_0_Nil tree = S_E8_1 (return () >>= (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) Nil)) sem_E8_0___ tree = S_E8_5 undefined sem_E8_1_Cons tree (S_E8_9 t1) (S_E8_8 t2) = S_E8_8 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_2 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v11, r_v21, r_v22)) (\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Cons r_v1 r_v3) r_v2)) tmp_r1 tmp_r2)) t1 t2) sem_E8_1_Cons tree (S_E8_9 t1) (S_E8_7 t2) = S_E8_8 ((\(x1_1, x1_2) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) () -> return (r_v11)) (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) Nil r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_E8_1_Nil tree = S_E8_7 (return ()) sem_E8_1___ tree = S_E8_5 undefined sem_E8_2___ tree = S_E8_9 (return tree, return tree) data StatesOfE9 e_0 = S_E9_0 e_0 e_E9 x = case trav_E9_0 x of S_E9_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E9" trav_E9_0 t = sem_E9_0___ t sem_E9_0___ tree = S_E9_0 (return tree) data StatesOfE10 e_0 = S_E10_0 e_0 e_E10 x = case trav_E10_0 x of S_E10_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E10" trav_E10_0 t = sem_E10_0___ t sem_E10_0___ tree = S_E10_0 (return tree) data StatesOfE25 e_0 = S_E25_0 e_0 e_E25 x = case trav_E25_0 x of S_E25_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E25" trav_E25_0 t = sem_E25_0___ t sem_E25_0___ tree = S_E25_0 (return tree) data StatesOfE26 e_0 = S_E26_0 e_0 e_E26 x = case trav_E26_0 x of S_E26_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E26" trav_E26_0 t = sem_E26_0___ t sem_E26_0___ tree = S_E26_0 (return tree) reverse (Nil) = Nil reverse (Cons a x) = snoc (reverse x) a snoc (Nil) b = Cons b Nil snoc (Cons a x) b = Cons a (snoc x b)