{-# OPTIONS -XNoMonomorphismRestriction #-} module PEANO2BIN (inv_Fpeano2bin,peano2bin) where import Control.Monad import InvUtil import Data.Tuple import MyData inv_Fpeano2bin = runI . e_Fpeano2bin data StatesOfFpeano2bin e_1 e_5 e_7 e_8 e_9 = S_Fpeano2bin_1 e_1 | S_Fpeano2bin_5 e_5 | S_Fpeano2bin_7 e_7 | S_Fpeano2bin_8 e_8 | S_Fpeano2bin_9 e_9 e_Fpeano2bin x = case trav_Fpeano2bin_0 x of S_Fpeano2bin_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: Fpeano2bin" trav_Fpeano2bin_0 (Cons t1 t2) = sem_Fpeano2bin_0_Cons (Cons t1 t2) (trav_Fpeano2bin_2 t1) (trav_Fpeano2bin_1 t2) trav_Fpeano2bin_0 t = sem_Fpeano2bin_0___ t trav_Fpeano2bin_1 (Nil) = sem_Fpeano2bin_1_Nil Nil trav_Fpeano2bin_1 (Cons t1 t2) = sem_Fpeano2bin_1_Cons (Cons t1 t2) (trav_Fpeano2bin_2 t1) (trav_Fpeano2bin_1 t2) trav_Fpeano2bin_1 t = sem_Fpeano2bin_1___ t trav_Fpeano2bin_2 t = sem_Fpeano2bin_2___ t sem_Fpeano2bin_0_Cons tree (S_Fpeano2bin_9 t1) (S_Fpeano2bin_8 t2) = S_Fpeano2bin_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair r_v1 (S r_v2)) >>= (\(r_v1) -> return r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_Fpeano2bin_0_Cons tree (S_Fpeano2bin_9 t1) (S_Fpeano2bin_7 t2) = S_Fpeano2bin_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) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair r_v1 Z) >>= (\(r_v1) -> return r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_Fpeano2bin_0___ tree = S_Fpeano2bin_5 undefined sem_Fpeano2bin_1_Cons tree (S_Fpeano2bin_9 t1) (S_Fpeano2bin_8 t2) = S_Fpeano2bin_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair r_v1 (S r_v2)) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E20) return (r_v11)) r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_Fpeano2bin_1_Cons tree (S_Fpeano2bin_9 t1) (S_Fpeano2bin_7 t2) = S_Fpeano2bin_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) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair r_v1 Z) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E20) return (r_v11)) r_v1)) tmp_r1 tmp_r2)) t1 t2) sem_Fpeano2bin_1_Nil tree = S_Fpeano2bin_7 (return ()) sem_Fpeano2bin_1___ tree = S_Fpeano2bin_5 undefined sem_Fpeano2bin_2___ tree = S_Fpeano2bin_9 (return tree, return tree) data StatesOfE3 e_1 e_7 e_8 e_9 e_11 e_12 e_13 e_14 = S_E3_1 e_1 | S_E3_7 e_7 | S_E3_8 e_8 | S_E3_9 e_9 | S_E3_11 e_11 | S_E3_12 e_12 | S_E3_13 e_13 | S_E3_14 e_14 e_E3 x = case trav_E3_0 x of S_E3_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E3" trav_E3_0 (Pair t1 t2) = sem_E3_0_Pair (Pair t1 t2) (trav_E3_3 t1) (trav_E3_1 t2) trav_E3_0 t = sem_E3_0___ t trav_E3_1 (Z) = sem_E3_1_Z Z trav_E3_1 (S t1) = sem_E3_1_S (S t1) (trav_E3_2 t1) trav_E3_1 t = sem_E3_1___ t trav_E3_2 t = sem_E3_2___ t trav_E3_3 (B1) = sem_E3_3_B1 B1 trav_E3_3 (B0) = sem_E3_3_B0 B0 trav_E3_3 t = sem_E3_3___ t sem_E3_0_Pair tree (S_E3_12 t1) (S_E3_8 t2) = S_E3_1 ((\(x1_1, x1_2) (x2_1, x2_2) -> (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)) Z) tmp_r1 tmp_r2)) t1 t2) sem_E3_0_Pair tree (S_E3_12 t1) (S_E3_9 t2) = S_E3_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E3_0_Pair tree (S_E3_13 t1) (S_E3_8 t2) = S_E3_1 ((\(x1_1, x1_2) (x2_1, x2_2) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_2 (\f g m1 m2 -> f m1 m2 >>= g) (\() () -> return ()) (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S Z)) tmp_r1 tmp_r2)) t1 t2) sem_E3_0_Pair tree (S_E3_13 t1) (S_E3_9 t2) = S_E3_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E3_0_Pair tree (S_E3_14 t1) (S_E3_9 t2) = S_E3_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E3_0___ tree = S_E3_7 undefined sem_E3_1_S tree (S_E3_11 t1) = S_E3_9 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E3_1_Z tree = S_E3_8 (return (), return ()) sem_E3_1___ tree = S_E3_7 undefined sem_E3_2___ tree = S_E3_11 (return tree) sem_E3_3_B0 tree = S_E3_12 (return (), return tree) sem_E3_3_B1 tree = S_E3_13 (return (), return tree) sem_E3_3___ tree = S_E3_14 (return tree) data StatesOfE4 e_0 = S_E4_0 e_0 e_E4 x = case trav_E4_0 x of S_E4_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E4" trav_E4_0 t = sem_E4_0___ t sem_E4_0___ tree = S_E4_0 (return tree) data StatesOfE20 e_0 e_1 e_3 = S_E20_0 e_0 | S_E20_1 e_1 | S_E20_3 e_3 e_E20 x = case trav_E20_0 x of S_E20_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E20" trav_E20_0 (S t1) = sem_E20_0_S (S t1) (trav_E20_1 t1) trav_E20_0 t = sem_E20_0___ t trav_E20_1 t = sem_E20_1___ t sem_E20_0_S tree (S_E20_3 t1) = S_E20_1 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E20_0___ tree = S_E20_0 undefined sem_E20_1___ tree = S_E20_3 (return tree) data StatesOfE42 e_4 e_7 e_8 e_9 e_11 e_12 e_13 e_14 = S_E42_4 e_4 | S_E42_7 e_7 | S_E42_8 e_8 | S_E42_9 e_9 | S_E42_11 e_11 | S_E42_12 e_12 | S_E42_13 e_13 | S_E42_14 e_14 e_E42 x = case trav_E42_0 x of S_E42_4 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E42" trav_E42_0 (Pair t1 t2) = sem_E42_0_Pair (Pair t1 t2) (trav_E42_3 t1) (trav_E42_1 t2) trav_E42_0 t = sem_E42_0___ t trav_E42_1 (Z) = sem_E42_1_Z Z trav_E42_1 (S t1) = sem_E42_1_S (S t1) (trav_E42_2 t1) trav_E42_1 t = sem_E42_1___ t trav_E42_2 t = sem_E42_2___ t trav_E42_3 (B1) = sem_E42_3_B1 B1 trav_E42_3 (B0) = sem_E42_3_B0 B0 trav_E42_3 t = sem_E42_3___ t sem_E42_0_Pair tree (S_E42_12 t1) (S_E42_8 t2) = S_E42_4 ((\(x1_1, x1_2) (x2_1, x2_2) -> (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)) Z) tmp_r1 tmp_r2)) t1 t2) sem_E42_0_Pair tree (S_E42_12 t1) (S_E42_9 t2) = S_E42_4 ((\(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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E42_0_Pair tree (S_E42_13 t1) (S_E42_8 t2) = S_E42_4 ((\(x1_1, x1_2) (x2_1, x2_2) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_2 (\f g m1 m2 -> f m1 m2 >>= g) (\() () -> return ()) (\() -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S Z)) tmp_r1 tmp_r2)) t1 t2) sem_E42_0_Pair tree (S_E42_13 t1) (S_E42_9 t2) = S_E42_4 ((\(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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E42_0_Pair tree (S_E42_14 t1) (S_E42_9 t2) = S_E42_4 ((\(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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E42) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S (S r_v1)))) tmp_r1 tmp_r2)) t1 t2) sem_E42_0___ tree = S_E42_7 undefined sem_E42_1_S tree (S_E42_11 t1) = S_E42_9 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E42_1_Z tree = S_E42_8 (return (), return ()) sem_E42_1___ tree = S_E42_7 undefined sem_E42_2___ tree = S_E42_11 (return tree) sem_E42_3_B0 tree = S_E42_12 (return (), return tree) sem_E42_3_B1 tree = S_E42_13 (return (), return tree) sem_E42_3___ tree = S_E42_14 (return tree) data StatesOfE43 e_0 = S_E43_0 e_0 e_E43 x = case trav_E43_0 x of S_E43_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E43" trav_E43_0 t = sem_E43_0___ t sem_E43_0___ tree = S_E43_0 (return tree) peano2bin x = testHalve (halve x) testHalve (Pair b (Z)) = Cons b Nil testHalve (Pair b (S x)) = Cons b (peano2bin (S x)) halve (Z) = Pair B0 Z halve (S (Z)) = Pair B1 Z halve (S (S x)) = letAt37 (halve x) letAt37 (Pair b s) = Pair b (S s)