{-# OPTIONS -XNoMonomorphismRestriction #-}
module REVERSE (inv_Freverse,reverse) where
import Control.Monad
import InvUtil

import Data.Tuple

import MyData
inv_Freverse = e_Freverse
data StatesOfFreverse e_0 e_DEAD = S_Freverse_0 e_0
                                 | S_Freverse_DEAD e_DEAD
e_Freverse x = case trav_Freverse_0 x of
                   S_Freverse_0 y -> y
                   _ -> fail "Input is not the range of the expression/function corresponding to the state: Freverse"
trav_Freverse_0 t = sem_Freverse_0___ t
sem_Freverse_0___ tree = S_Freverse_0 (mymplus (return tree >>= (\(r_v1) -> (\(r_x1,
                                                                               r_x2) -> do (r_v11) <- return r_x1
                                                                                           () <- (return r_x2 >>= e_E4)
                                                                                           return (r_v11)) ((,) Nil r_v1) >>= (\(r_v1) -> return r_v1))) (mymplus (return tree >>= ((\(r_v1) -> (\(r_x1,
                                                                                                                                                                                                   r_x2) -> do (r_v11) <- return r_x1
                                                                                                                                                                                                               (r_v21,
                                                                                                                                                                                                                r_v22) <- (return r_x2 >>= e_E16)
                                                                                                                                                                                                               return (r_v21,
                                                                                                                                                                                                                       r_v11,
                                                                                                                                                                                                                       r_v22)) ((,) Nil r_v1)) >=> (\(r_v1,
                                                                                                                                                                                                                                                      r_v2,
                                                                                                                                                                                                                                                      r_v3) -> (\(r_x1,
                                                                                                                                                                                                                                                                  r_x2) -> do (r_v11) <- return r_x1
                                                                                                                                                                                                                                                                              () <- (return r_x2 >>= e_E4)
                                                                                                                                                                                                                                                                              return (r_v11)) ((,) (Cons r_v1 r_v2) r_v3) >>= (\(r_v1) -> return r_v1)))) (return tree >>= ((\(r_v1) -> (\(r_x1,
                                                                                                                                                                                                                                                                                                                                                                                           r_x2) -> do (r_v11) <- return r_x1
                                                                                                                                                                                                                                                                                                                                                                                                       (r_v21,
                                                                                                                                                                                                                                                                                                                                                                                                        r_v22) <- (return r_x2 >>= e_E16)
                                                                                                                                                                                                                                                                                                                                                                                                       return (r_v21,
                                                                                                                                                                                                                                                                                                                                                                                                               r_v11,
                                                                                                                                                                                                                                                                                                                                                                                                               r_v22)) ((,) Nil r_v1)) >=> (fixApp (\(r_v1,
                                                                                                                                                                                                                                                                                                                                                                                                                                                      r_v2,
                                                                                                                                                                                                                                                                                                                                                                                                                                                      r_v3) -> (\(r_x1,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  r_x2) -> do (r_v11) <- return r_x1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (r_v21,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                               r_v22) <- (return r_x2 >>= e_E16)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              return (r_v21,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      r_v11,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      r_v22)) ((,) (Cons r_v1 r_v2) r_v3)) >=> (\(r_v1,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  r_v2,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  r_v3) -> (\(r_x1,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              r_x2) -> do (r_v11) <- return r_x1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          () <- (return r_x2 >>= e_E4)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          return (r_v11)) ((,) (Cons r_v1 r_v2) r_v3) >>= (\(r_v1) -> return r_v1)))))))
sem_Freverse_0___ _ = S_Freverse_DEAD mymzero
data StatesOfE3 e_0 e_DEAD = S_E3_0 e_0 | S_E3_DEAD e_DEAD
e_E3 x = case trav_E3_0 x of
             S_E3_0 y -> y
             _ -> fail "Input is not the range of the expression/function corresponding to the state: E3"
trav_E3_0 t = sem_E3_0___ t
sem_E3_0___ tree = S_E3_0 (return tree)
sem_E3_0___ _ = S_E3_DEAD mymzero
data StatesOfE4 e_0 e_1 e_DEAD = S_E4_0 e_0
                               | S_E4_1 e_1
                               | S_E4_DEAD e_DEAD
e_E4 x = case trav_E4_0 x of
             S_E4_1 y -> y
             _ -> fail "Input is not the range of the expression/function corresponding to the state: E4"
trav_E4_0 (Nil) = sem_E4_0_Nil Nil
trav_E4_0 t = sem_E4_0___ t
sem_E4_0_Nil tree = S_E4_1 (return ())
sem_E4_0_Nil _ = S_E4_DEAD mymzero
sem_E4_0___ tree = S_E4_0 undefined
sem_E4_0___ _ = S_E4_DEAD mymzero
data StatesOfE15 e_0 e_DEAD = S_E15_0 e_0 | S_E15_DEAD e_DEAD
e_E15 x = case trav_E15_0 x of
              S_E15_0 y -> y
              _ -> fail "Input is not the range of the expression/function corresponding to the state: E15"
trav_E15_0 t = sem_E15_0___ t
sem_E15_0___ tree = S_E15_0 (return tree)
sem_E15_0___ _ = S_E15_DEAD mymzero
data StatesOfE16 e_0 e_1 e_4 e_5 e_DEAD = S_E16_0 e_0
                                        | S_E16_1 e_1
                                        | S_E16_4 e_4
                                        | S_E16_5 e_5
                                        | S_E16_DEAD e_DEAD
e_E16 x = case trav_E16_0 x of
              S_E16_1 y -> y
              _ -> fail "Input is not the range of the expression/function corresponding to the state: E16"
trav_E16_0 (Cons t1
                 t2) = sem_E16_0_Cons (Cons t1 t2) (trav_E16_2 t1) (trav_E16_1 t2)
trav_E16_0 t = sem_E16_0___ t
trav_E16_1 t = sem_E16_1___ t
trav_E16_2 t = sem_E16_2___ t
sem_E16_0_Cons tree (S_E16_5 t1) (S_E16_4 t2) = S_E16_1 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1
                                                                                tmp_r2 <- x2_1
                                                                                (\(r_v11) (r_v21) -> return (r_v11,
                                                                                                             r_v21)) tmp_r1 tmp_r2)) t1 t2)
sem_E16_0_Cons _ _ _ = S_E16_DEAD mymzero
sem_E16_0___ tree = S_E16_0 undefined
sem_E16_0___ _ = S_E16_DEAD mymzero
sem_E16_1___ tree = S_E16_4 (return tree)
sem_E16_1___ _ = S_E16_DEAD mymzero
sem_E16_2___ tree = S_E16_5 (return tree)
sem_E16_2___ _ = S_E16_DEAD mymzero
reverse x = rev x Nil
rev (Nil) y = y
rev (Cons a x) y = rev x (Cons a y)