{-# OPTIONS -XNoMonomorphismRestriction #-} module TABA_REVERSE_LET (inv_Ftaba_reverse_let,taba_reverse_let) where import Control.Monad import InvUtil import Data.Tuple import MyData inv_Ftaba_reverse_let = runI . e_Ftaba_reverse_let data StatesOfFtaba_reverse_let e_0 = S_Ftaba_reverse_let_0 e_0 e_Ftaba_reverse_let x = case trav_Ftaba_reverse_let_0 x of S_Ftaba_reverse_let_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: Ftaba_reverse_let" trav_Ftaba_reverse_let_0 t = sem_Ftaba_reverse_let_0___ t sem_Ftaba_reverse_let_0___ tree = S_Ftaba_reverse_let_0 (return tree >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E7) return (r_v11)) (Pair Nil r_v1) >>= (\(r_v1) -> return r_v1))) data StatesOfE7 e_1 e_5 e_6 e_7 e_10 e_11 e_12 = S_E7_1 e_1 | S_E7_5 e_5 | S_E7_6 e_6 | S_E7_7 e_7 | S_E7_10 e_10 | S_E7_11 e_11 | S_E7_12 e_12 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 (Pair t1 t2) = sem_E7_0_Pair (Pair t1 t2) (trav_E7_4 t1) (trav_E7_1 t2) trav_E7_0 t = sem_E7_0___ t trav_E7_1 (Nil) = sem_E7_1_Nil Nil trav_E7_1 (Cons t1 t2) = sem_E7_1_Cons (Cons t1 t2) (trav_E7_3 t1) (trav_E7_2 t2) trav_E7_1 t = sem_E7_1___ t trav_E7_2 t = sem_E7_2___ t trav_E7_3 t = sem_E7_3___ t trav_E7_4 t = sem_E7_4___ t sem_E7_0_Pair tree (S_E7_12 t1) (S_E7_6 t2) = S_E7_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 (r_v21) <- return r_x2 return (r_v11, r_v21)) ((,) Z r_v1)) >=> (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E8) return (r_v11)) (Pair r_v1 r_v2))) tmp_r1 tmp_r2)) t1 t2) sem_E7_0_Pair tree (S_E7_12 t1) (S_E7_7 t2) = S_E7_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_v21, r_v11, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1) -> do (r_v11, r_v12) <- (return r_x1 >>= e_E35) return (r_v11, r_v12)) (Pair (Cons r_v1 r_v2) r_v3)) >=> ((\(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_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E8) return (r_v11)) (Pair r_v1 r_v2)))) tmp_r1 tmp_r2)) t1 t2) sem_E7_0___ tree = S_E7_5 undefined sem_E7_1_Cons tree (S_E7_11 t1) (S_E7_10 t2) = S_E7_7 ((\(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_E7_1_Nil tree = S_E7_6 (return ()) sem_E7_1___ tree = S_E7_5 undefined sem_E7_2___ tree = S_E7_10 (return tree) sem_E7_3___ tree = S_E7_11 (return tree) sem_E7_4___ tree = S_E7_12 (return tree, return tree) data StatesOfE8 e_1 e_7 e_8 e_11 e_12 e_13 e_14 e_15 e_17 = S_E8_1 e_1 | S_E8_7 e_7 | S_E8_8 e_8 | S_E8_11 e_11 | S_E8_12 e_12 | S_E8_13 e_13 | S_E8_14 e_14 | S_E8_15 e_15 | S_E8_17 e_17 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 (Pair t1 t2) = sem_E8_0_Pair (Pair t1 t2) (trav_E8_4 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_3 t1) (trav_E8_2 t2) trav_E8_1 t = sem_E8_1___ t trav_E8_2 t = sem_E8_2___ t trav_E8_3 t = sem_E8_3___ t trav_E8_4 (Z) = sem_E8_4_Z Z trav_E8_4 (S t1) = sem_E8_4_S (S t1) (trav_E8_5 t1) trav_E8_4 t = sem_E8_4___ t trav_E8_5 t = sem_E8_5___ t sem_E8_0_Pair tree (S_E8_14 t1) (S_E8_7 t2) = S_E8_1 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\() () -> return ()) (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) Nil) tmp_r1 tmp_r2)) t1 t2) sem_E8_0_Pair tree (S_E8_15 t1) (S_E8_8 t2) = S_E8_1 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v21, r_v11, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E57) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Pair r_v2 r_v3) 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___ tree = S_E8_13 undefined sem_E8_1_Cons tree (S_E8_12 t1) (S_E8_11 t2) = S_E8_8 ((\(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_E8_1_Nil tree = S_E8_7 (return ()) sem_E8_1___ tree = S_E8_13 undefined sem_E8_2___ tree = S_E8_11 (return tree) sem_E8_3___ tree = S_E8_12 (return tree) sem_E8_4_S tree (S_E8_17 t1) = S_E8_15 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E8_4_Z tree = S_E8_14 (return ()) sem_E8_4___ tree = S_E8_13 undefined sem_E8_5___ tree = S_E8_17 (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 StatesOfE16 e_0 = S_E16_0 e_0 e_E16 x = case trav_E16_0 x of S_E16_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E16" trav_E16_0 t = sem_E16_0___ t sem_E16_0___ tree = S_E16_0 (return tree) data StatesOfE17 e_0 = S_E17_0 e_0 e_E17 x = case trav_E17_0 x of S_E17_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E17" trav_E17_0 t = sem_E17_0___ t sem_E17_0___ tree = S_E17_0 (return tree) data StatesOfE35 e_3 e_5 e_6 e_7 e_10 e_11 e_12 = S_E35_3 e_3 | S_E35_5 e_5 | S_E35_6 e_6 | S_E35_7 e_7 | S_E35_10 e_10 | S_E35_11 e_11 | S_E35_12 e_12 e_E35 x = case trav_E35_0 x of S_E35_3 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E35" trav_E35_0 (Pair t1 t2) = sem_E35_0_Pair (Pair t1 t2) (trav_E35_4 t1) (trav_E35_1 t2) trav_E35_0 t = sem_E35_0___ t trav_E35_1 (Nil) = sem_E35_1_Nil Nil trav_E35_1 (Cons t1 t2) = sem_E35_1_Cons (Cons t1 t2) (trav_E35_3 t1) (trav_E35_2 t2) trav_E35_1 t = sem_E35_1___ t trav_E35_2 t = sem_E35_2___ t trav_E35_3 t = sem_E35_3___ t trav_E35_4 t = sem_E35_4___ t sem_E35_0_Pair tree (S_E35_12 t1) (S_E35_6 t2) = S_E35_3 ((\(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_v11, r_v21)) ((,) Z r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_E35_0_Pair tree (S_E35_12 t1) (S_E35_7 t2) = S_E35_3 ((\(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_v21, r_v11, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1) -> do (r_v11, r_v12) <- (return r_x1 >>= e_E35) return (r_v11, r_v12)) (Pair (Cons r_v1 r_v2) r_v3)) >=> (\(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))) tmp_r1 tmp_r2)) t1 t2) sem_E35_0___ tree = S_E35_5 undefined sem_E35_1_Cons tree (S_E35_11 t1) (S_E35_10 t2) = S_E35_7 ((\(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_E35_1_Nil tree = S_E35_6 (return ()) sem_E35_1___ tree = S_E35_5 undefined sem_E35_2___ tree = S_E35_10 (return tree) sem_E35_3___ tree = S_E35_11 (return tree) sem_E35_4___ tree = S_E35_12 (return tree, return tree) data StatesOfE36 e_0 = S_E36_0 e_0 e_E36 x = case trav_E36_0 x of S_E36_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E36" trav_E36_0 t = sem_E36_0___ t sem_E36_0___ tree = S_E36_0 (return tree) data StatesOfE37 e_0 = S_E37_0 e_0 e_E37 x = case trav_E37_0 x of S_E37_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E37" trav_E37_0 t = sem_E37_0___ t sem_E37_0___ tree = S_E37_0 (return tree) data StatesOfE57 e_3 e_7 e_8 e_11 e_12 e_13 e_14 e_15 e_17 = S_E57_3 e_3 | S_E57_7 e_7 | S_E57_8 e_8 | S_E57_11 e_11 | S_E57_12 e_12 | S_E57_13 e_13 | S_E57_14 e_14 | S_E57_15 e_15 | S_E57_17 e_17 e_E57 x = case trav_E57_0 x of S_E57_3 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E57" trav_E57_0 (Pair t1 t2) = sem_E57_0_Pair (Pair t1 t2) (trav_E57_4 t1) (trav_E57_1 t2) trav_E57_0 t = sem_E57_0___ t trav_E57_1 (Nil) = sem_E57_1_Nil Nil trav_E57_1 (Cons t1 t2) = sem_E57_1_Cons (Cons t1 t2) (trav_E57_3 t1) (trav_E57_2 t2) trav_E57_1 t = sem_E57_1___ t trav_E57_2 t = sem_E57_2___ t trav_E57_3 t = sem_E57_3___ t trav_E57_4 (Z) = sem_E57_4_Z Z trav_E57_4 (S t1) = sem_E57_4_S (S t1) (trav_E57_5 t1) trav_E57_4 t = sem_E57_4___ t trav_E57_5 t = sem_E57_5___ t sem_E57_0_Pair tree (S_E57_14 t1) (S_E57_7 t2) = S_E57_3 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\() () -> return ()) (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) Nil) tmp_r1 tmp_r2)) t1 t2) sem_E57_0_Pair tree (S_E57_15 t1) (S_E57_8 t2) = S_E57_3 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\f g m1 m2 -> f m1 m2 >>= g) (\(r_v11) (r_v21, r_v22) -> return (r_v21, r_v11, r_v22)) ((\(r_v1, r_v2, r_v3) -> (\(r_x1, r_x2) -> do (r_v11) <- (return r_x1 >>= e_E57) (r_v21) <- return r_x2 return (r_v21, r_v11)) ((,) (Pair r_v2 r_v3) 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_E57_0___ tree = S_E57_13 undefined sem_E57_1_Cons tree (S_E57_12 t1) (S_E57_11 t2) = S_E57_8 ((\(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_E57_1_Nil tree = S_E57_7 (return ()) sem_E57_1___ tree = S_E57_13 undefined sem_E57_2___ tree = S_E57_11 (return tree) sem_E57_3___ tree = S_E57_12 (return tree) sem_E57_4_S tree (S_E57_17 t1) = S_E57_15 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E57_4_Z tree = S_E57_14 (return ()) sem_E57_4___ tree = S_E57_13 undefined sem_E57_5___ tree = S_E57_17 (return tree) data StatesOfE58 e_0 = S_E58_0 e_0 e_E58 x = case trav_E58_0 x of S_E58_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E58" trav_E58_0 t = sem_E58_0___ t sem_E58_0___ tree = S_E58_0 (return tree) data StatesOfE65 e_0 = S_E65_0 e_0 e_E65 x = case trav_E65_0 x of S_E65_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E65" trav_E65_0 t = sem_E65_0___ t sem_E65_0___ tree = S_E65_0 (return tree) taba_reverse_let x = letAt2 (h (idshape x)) letAt2 (Pair (Nil) y) = y h (Pair n x) = hImpl n x hImpl (Z) y = Pair y Nil hImpl (S x) y = letAt28 (hImpl x y) letAt28 (Pair (Cons a x1) y1) = Pair x1 (Cons a y1) idshape (Nil) = Pair Z Nil idshape (Cons a x) = letAt52 (idshape x) a letAt52 (Pair n x) a = Pair (S n) (Cons a x)