{-# OPTIONS -XNoMonomorphismRestriction #-} module SIGMA (inv_Fsigma,sigma) where import Control.Monad import InvUtil import Data.Tuple import MyData inv_Fsigma = e_Fsigma data StatesOfFsigma e_0 e_2 e_DEAD = S_Fsigma_0 e_0 | S_Fsigma_2 e_2 | S_Fsigma_DEAD e_DEAD e_Fsigma x = case trav_Fsigma_0 x of S_Fsigma_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: Fsigma" trav_Fsigma_0 (Z) = sem_Fsigma_0_Z Z trav_Fsigma_0 (S t1) = sem_Fsigma_0_S (S t1) (trav_Fsigma_1 t1) trav_Fsigma_0 t = sem_Fsigma_0___ t trav_Fsigma_1 (S t1) = sem_Fsigma_1_S (S t1) (trav_Fsigma_1 t1) trav_Fsigma_1 t = sem_Fsigma_1___ t sem_Fsigma_0_S tree (S_Fsigma_2 t1) = S_Fsigma_0 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> return (S r_v1)))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) (S r_v1) r_v2) >>= (\(r_v1) -> return (S r_v1))) (r_v11, r_v12)) tmp_r1))) t1) sem_Fsigma_0_S _ _ = S_Fsigma_DEAD mymzero sem_Fsigma_0_Z tree = S_Fsigma_0 (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> return (S r_v1)))) (return () >>= (\() -> return Z))) sem_Fsigma_0_Z _ = S_Fsigma_DEAD mymzero sem_Fsigma_0___ tree = S_Fsigma_0 (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> return (S r_v1)))) sem_Fsigma_0___ _ = S_Fsigma_DEAD mymzero sem_Fsigma_1_S tree (S_Fsigma_2 t1) = S_Fsigma_2 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) Z r_v1))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) (S r_v1) r_v2)) (r_v11, r_v12)) tmp_r1))) t1) sem_Fsigma_1_S _ _ = S_Fsigma_DEAD mymzero sem_Fsigma_1___ tree = S_Fsigma_2 (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) Z r_v1))) sem_Fsigma_1___ _ = S_Fsigma_DEAD mymzero data StatesOfE7 e_0 e_1 e_3 e_DEAD = S_E7_0 e_0 | S_E7_1 e_1 | S_E7_3 e_3 | S_E7_DEAD e_DEAD e_E7 x = case trav_E7_0 x of S_E7_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E7" trav_E7_0 (S t1) = sem_E7_0_S (S t1) (trav_E7_1 t1) trav_E7_0 t = sem_E7_0___ t trav_E7_1 t = sem_E7_1___ t sem_E7_0_S tree (S_E7_3 t1) = S_E7_1 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E7_0_S _ _ = S_E7_DEAD mymzero sem_E7_0___ tree = S_E7_0 undefined sem_E7_0___ _ = S_E7_DEAD mymzero sem_E7_1___ tree = S_E7_3 (return tree) sem_E7_1___ _ = S_E7_DEAD mymzero data StatesOfE9 e_0 e_2 e_DEAD = S_E9_0 e_0 | S_E9_2 e_2 | S_E9_DEAD e_DEAD 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 (Z) = sem_E9_0_Z Z trav_E9_0 (S t1) = sem_E9_0_S (S t1) (trav_E9_1 t1) trav_E9_0 t = sem_E9_0___ t trav_E9_1 (S t1) = sem_E9_1_S (S t1) (trav_E9_1 t1) trav_E9_1 t = sem_E9_1___ t sem_E9_0_S tree (S_E9_2 t1) = S_E9_0 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1)))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) (S r_v1) r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1))) (r_v11, r_v12)) tmp_r1))) t1) sem_E9_0_S _ _ = S_E9_DEAD mymzero sem_E9_0_Z tree = S_E9_0 (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1)))) (return () >>= (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) Z))) sem_E9_0_Z _ = S_E9_DEAD mymzero sem_E9_0___ tree = S_E9_0 (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E7) (r_v21) <- (return r_x2 >>= e_E9) do tv1 <- checkEqPrim r_v11 r_v21 return (tv1)) ((,) Z r_v1) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1)))) sem_E9_0___ _ = S_E9_DEAD mymzero sem_E9_1_S tree (S_E9_2 t1) = S_E9_2 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) Z r_v1))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) (S r_v1) r_v2)) (r_v11, r_v12)) tmp_r1))) t1) sem_E9_1_S _ _ = S_E9_DEAD mymzero sem_E9_1___ tree = S_E9_2 (return tree >>= (\(r_v1) -> (\(r_x1, r_x2) -> do (r_v11) <- return r_x1 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) Z r_v1))) sem_E9_1___ _ = S_E9_DEAD mymzero data StatesOfE10 e_0 e_DEAD = S_E10_0 e_0 | S_E10_DEAD e_DEAD 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) sem_E10_0___ _ = S_E10_DEAD mymzero data StatesOfE21 e_0 e_DEAD = S_E21_0 e_0 | S_E21_DEAD e_DEAD e_E21 x = case trav_E21_0 x of S_E21_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E21" trav_E21_0 t = sem_E21_0___ t sem_E21_0___ tree = S_E21_0 (return tree) sem_E21_0___ _ = S_E21_DEAD mymzero data StatesOfE22 e_0 e_DEAD = S_E22_0 e_0 | S_E22_DEAD e_DEAD e_E22 x = case trav_E22_0 x of S_E22_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E22" trav_E22_0 t = sem_E22_0___ t sem_E22_0___ tree = S_E22_0 (return tree) sem_E22_0___ _ = S_E22_DEAD mymzero sigma (Z) = Z sigma (S n) = add (S n) (sigma n) add (Z) n = n add (S m) n = S (add m n)