{-# OPTIONS -XNoMonomorphismRestriction #-} module DUPDOUBLE (inv_Fdouble,double) where import Control.Monad import InvUtil import Data.Tuple import MyData inv_Fdouble = e_Fdouble data StatesOfFdouble e_0 e_2 e_DEAD = S_Fdouble_0 e_0 | S_Fdouble_2 e_2 | S_Fdouble_DEAD e_DEAD e_Fdouble x = case trav_Fdouble_0 x of S_Fdouble_0 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: Fdouble" trav_Fdouble_0 (S t1) = sem_Fdouble_0_S (S t1) (trav_Fdouble_1 t1) trav_Fdouble_0 t = sem_Fdouble_0___ t trav_Fdouble_1 (S t1) = sem_Fdouble_1_S (S t1) (trav_Fdouble_1 t1) trav_Fdouble_1 t = sem_Fdouble_1___ t sem_Fdouble_0_S tree (S_Fdouble_2 t1) = S_Fdouble_0 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair Z r_v1) >>= (\(r_v1) -> return r_v1))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair (S r_v2) r_v1) >>= (\(r_v1) -> return r_v1)) (r_v11, r_v12)) tmp_r1))) t1) sem_Fdouble_0_S _ _ = S_Fdouble_DEAD mymzero sem_Fdouble_0___ tree = S_Fdouble_0 (return tree >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E3) return (r_v11)) (Pair Z r_v1) >>= (\(r_v1) -> return r_v1))) sem_Fdouble_0___ _ = S_Fdouble_DEAD mymzero sem_Fdouble_1_S tree (S_Fdouble_2 t1) = S_Fdouble_2 ((\(x1_1) -> (mymplus (return tree >>= (\(r_v1) -> (\(r_x1) -> do (r_v11, r_v12) <- (return r_x1 >>= e_E37) return (r_v11, r_v12)) (Pair Z r_v1))) (do tmp_r1 <- x1_1 (\(r_v11, r_v12) -> (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11, r_v12) <- (return r_x1 >>= e_E37) return (r_v11, r_v12)) (Pair (S r_v2) r_v1)) (r_v11, r_v12)) tmp_r1))) t1) sem_Fdouble_1_S _ _ = S_Fdouble_DEAD mymzero sem_Fdouble_1___ tree = S_Fdouble_2 (return tree >>= (\(r_v1) -> (\(r_x1) -> do (r_v11, r_v12) <- (return r_x1 >>= e_E37) return (r_v11, r_v12)) (Pair Z r_v1))) sem_Fdouble_1___ _ = S_Fdouble_DEAD mymzero data StatesOfE3 e_1 e_7 e_8 e_10 e_11 e_12 e_13 e_15 e_DEAD = S_E3_1 e_1 | S_E3_7 e_7 | S_E3_8 e_8 | S_E3_10 e_10 | S_E3_11 e_11 | S_E3_12 e_12 | S_E3_13 e_13 | S_E3_15 e_15 | S_E3_DEAD e_DEAD 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 (Z) = sem_E3_3_Z Z trav_E3_3 (S t1) = sem_E3_3_S (S t1) (trav_E3_4 t1) trav_E3_3 t = sem_E3_3___ t trav_E3_4 t = sem_E3_4___ t sem_E3_0_Pair tree (S_E3_12 t1) (S_E3_7 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) (\() () -> 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_13 t1) (S_E3_8 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_E14) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1))) tmp_r1 tmp_r2)) t1 t2) sem_E3_0_Pair _ _ _ = S_E3_DEAD mymzero sem_E3_0___ tree = S_E3_11 undefined sem_E3_0___ _ = S_E3_DEAD mymzero sem_E3_1_S tree (S_E3_10 t1) = S_E3_8 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E3_1_S _ _ = S_E3_DEAD mymzero sem_E3_1_Z tree = S_E3_7 (return ()) sem_E3_1_Z _ = S_E3_DEAD mymzero sem_E3_1___ tree = S_E3_11 undefined sem_E3_1___ _ = S_E3_DEAD mymzero sem_E3_2___ tree = S_E3_10 (return tree) sem_E3_2___ _ = S_E3_DEAD mymzero sem_E3_3_S tree (S_E3_15 t1) = S_E3_13 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E3_3_S _ _ = S_E3_DEAD mymzero sem_E3_3_Z tree = S_E3_12 (return ()) sem_E3_3_Z _ = S_E3_DEAD mymzero sem_E3_3___ tree = S_E3_11 undefined sem_E3_3___ _ = S_E3_DEAD mymzero sem_E3_4___ tree = S_E3_15 (return tree) sem_E3_4___ _ = S_E3_DEAD mymzero data StatesOfE4 e_0 e_DEAD = S_E4_0 e_0 | S_E4_DEAD e_DEAD 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) sem_E4_0___ _ = S_E4_DEAD mymzero data StatesOfE14 e_3 e_7 e_8 e_10 e_11 e_12 e_13 e_15 e_DEAD = S_E14_3 e_3 | S_E14_7 e_7 | S_E14_8 e_8 | S_E14_10 e_10 | S_E14_11 e_11 | S_E14_12 e_12 | S_E14_13 e_13 | S_E14_15 e_15 | S_E14_DEAD e_DEAD e_E14 x = case trav_E14_0 x of S_E14_3 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E14" trav_E14_0 (Pair t1 t2) = sem_E14_0_Pair (Pair t1 t2) (trav_E14_3 t1) (trav_E14_1 t2) trav_E14_0 t = sem_E14_0___ t trav_E14_1 (Z) = sem_E14_1_Z Z trav_E14_1 (S t1) = sem_E14_1_S (S t1) (trav_E14_2 t1) trav_E14_1 t = sem_E14_1___ t trav_E14_2 t = sem_E14_2___ t trav_E14_3 (Z) = sem_E14_3_Z Z trav_E14_3 (S t1) = sem_E14_3_S (S t1) (trav_E14_4 t1) trav_E14_3 t = sem_E14_3___ t trav_E14_4 t = sem_E14_4___ t sem_E14_0_Pair tree (S_E14_12 t1) (S_E14_7 t2) = S_E14_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)) Z) tmp_r1 tmp_r2)) t1 t2) sem_E14_0_Pair tree (S_E14_13 t1) (S_E14_8 t2) = S_E14_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) -> return (r_v11, r_v21)) (\(r_v1, r_v2) -> (\(r_x1) -> do (r_v11) <- (return r_x1 >>= e_E14) return (r_v11)) (Pair r_v1 r_v2) >>= (\(r_v1) -> (\(r_x1) -> do (r_v11) <- return r_x1 return (r_v11)) (S r_v1))) tmp_r1 tmp_r2)) t1 t2) sem_E14_0_Pair _ _ _ = S_E14_DEAD mymzero sem_E14_0___ tree = S_E14_11 undefined sem_E14_0___ _ = S_E14_DEAD mymzero sem_E14_1_S tree (S_E14_10 t1) = S_E14_8 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E14_1_S _ _ = S_E14_DEAD mymzero sem_E14_1_Z tree = S_E14_7 (return ()) sem_E14_1_Z _ = S_E14_DEAD mymzero sem_E14_1___ tree = S_E14_11 undefined sem_E14_1___ _ = S_E14_DEAD mymzero sem_E14_2___ tree = S_E14_10 (return tree) sem_E14_2___ _ = S_E14_DEAD mymzero sem_E14_3_S tree (S_E14_15 t1) = S_E14_13 ((\(x1_1) -> (do tmp_r1 <- x1_1 (\(r_v11) -> return (r_v11)) tmp_r1)) t1) sem_E14_3_S _ _ = S_E14_DEAD mymzero sem_E14_3_Z tree = S_E14_12 (return ()) sem_E14_3_Z _ = S_E14_DEAD mymzero sem_E14_3___ tree = S_E14_11 undefined sem_E14_3___ _ = S_E14_DEAD mymzero sem_E14_4___ tree = S_E14_15 (return tree) sem_E14_4___ _ = S_E14_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 StatesOfE37 e_0 e_1 e_4 e_5 e_DEAD = S_E37_0 e_0 | S_E37_1 e_1 | S_E37_4 e_4 | S_E37_5 e_5 | S_E37_DEAD e_DEAD e_E37 x = case trav_E37_0 x of S_E37_1 y -> y _ -> fail "Input is not the range of the expression/function corresponding to the state: E37" trav_E37_0 (Pair t1 t2) = sem_E37_0_Pair (Pair t1 t2) (trav_E37_2 t1) (trav_E37_1 t2) trav_E37_0 t = sem_E37_0___ t trav_E37_1 t = sem_E37_1___ t trav_E37_2 t = sem_E37_2___ t sem_E37_0_Pair tree (S_E37_5 t1) (S_E37_4 t2) = S_E37_1 ((\(x1_1) (x2_1) -> (do tmp_r1 <- x1_1 tmp_r2 <- x2_1 (\(r_v11) (r_v21) -> return (r_v21, r_v11)) tmp_r1 tmp_r2)) t1 t2) sem_E37_0_Pair _ _ _ = S_E37_DEAD mymzero sem_E37_0___ tree = S_E37_0 undefined sem_E37_0___ _ = S_E37_DEAD mymzero sem_E37_1___ tree = S_E37_4 (return tree) sem_E37_1___ _ = S_E37_DEAD mymzero sem_E37_2___ tree = S_E37_5 (return tree) sem_E37_2___ _ = S_E37_DEAD mymzero double n = add (dup n) dup (Z) = Pair Z Z dup (S n) = dSuc (dup n) dSuc (Pair m n) = Pair (S m) (S n) add (Pair (Z) m) = m add (Pair (S n) m) = S (add (Pair n m))