--================================================================================ Typechecked: {- nonrec -} Leaf{-rg,x-}{i} = _/\_ t{-r5r-} -> \ tpl_B1 -> Leaf{-rg,x-}{i} {_@_ t{-r5r-} tpl_B1} Node{-rf,x-}{i} = _/\_ t{-r5r-} -> \ tpl_B1 tpl_B2 -> Node{-rf,x-}{i} {_@_ t{-r5r-} tpl_B1 tpl_B2} {- nonrec -} Zero{-rl,x-}{i} = Zero{-rl,x-}{i} {} Succ{-rk,x-}{i} = \ tpl_B1 -> Succ{-rk,x-}{i} {tpl_B1} {- nonrec -} Nil{-rq,x-}{i} = _/\_ alpha{-r5u-} -> Nil{-rq,x-}{i} {_@_ alpha{-r5u-}} Cons{-rp,x-}{i} = _/\_ alpha{-r5u-} -> \ tpl_B1 tpl_B2 -> Cons{-rp,x-}{i} {_@_ alpha{-r5u-} tpl_B1 tpl_B2} {- nonrec -} Mkpair{-r5B,x-}{i} = _/\_ a{-r5w-} b{-r5x-} -> \ tpl_B1 tpl_B2 -> Mkpair{-r5B,x-}{i} {_@_ a{-r5w-} _@_ b{-r5x-} tpl_B1 tpl_B2} {- nonrec -} FF{-rx,x-}{i} = FF{-rx,x-}{i} {} TT{-rw,x-}{i} = TT{-rw,x-}{i} {} {- rec -} AbsBinds [t{-aMR-}] [] [([t{-aMR-}], $d1{-rMX,x-}, d.Eval_aMt)] d.Eval_aMt = ({-dict-} [] []) {- rec -} AbsBinds [] [] [([], $d2{-rMZ,x-}, d.Eval_aMy)] d.Eval_aMy = ({-dict-} [] []) {- rec -} AbsBinds [alpha{-aMS-}] [] [([alpha{-aMS-}], $d3{-rN1,x-}, d.Eval_aME)] d.Eval_aME = ({-dict-} [] []) {- rec -} AbsBinds [a{-aMT-}, b{-aMU-}] [] [([a{-aMT-}, b{-aMU-}], $d4{-rN3,x-}, d.Eval_aML)] d.Eval_aML = ({-dict-} [] []) {- rec -} AbsBinds [] [] [([], $d5{-rN5,x-}, d.Eval_aMQ)] d.Eval_aMQ = ({-dict-} [] []) {- nonrec -} {- rec -} AbsBinds [] [] [([], before{-r4a,x-}, before_aIA)] before_aIA xs_r4Y = case xs_r4Y of Nil{-rq,x-}{i} -> Nil{-rq,x-}{i} Nat{-r5z,x-} (Cons{-rp,x-}{i} y_r51 ys_r52) -> case y_r51 of Zero{-rl,x-}{i} -> Nil{-rq,x-}{i} Nat{-r5z,x-} (Succ{-rk,x-}{i} n_r55) -> Cons{-rp,x-}{i} Nat{-r5z,x-} y_r51 before{-r4a,x-} ys_r52 {- nonrec -} {- rec -} AbsBinds [a{-aJ2-}] [] [([a{-aJ2-}], lEngth{-r49,x-}, lEngth_aIZ)] lEngth_aIZ xs_r4S = case xs_r4S of Nil{-rq,x-}{i} -> Zero{-rl,x-}{i} (Cons{-rp,x-}{i} y_r4V ys_r4W) -> Succ{-rk,x-}{i} lEngth{-r49,x-} a{-aJ2-} ys_r4W {- nonrec -} {- rec -} AbsBinds [alpha{-aJo-}] [] [([alpha{-aJo-}], app{-r48,x-}, app_aJl)] app_aJl xs_r4K zs_r4M = case xs_r4K of Nil{-rq,x-}{i} -> zs_r4M (Cons{-rp,x-}{i} y_r4P ys_r4Q) -> Cons{-rp,x-}{i} alpha{-aJo-} y_r4P app{-r48,x-} alpha{-aJo-} ys_r4Q zs_r4M {- nonrec -} {- rec -} AbsBinds [alpha{-aJO-}] [] [([alpha{-aJO-}], rEverse{-r4b,x-}, rEverse_aJL)] rEverse_aJL rs_r57 = case rs_r57 of Nil{-rq,x-}{i} -> Nil{-rq,x-}{i} alpha{-aJO-} (Cons{-rp,x-}{i} y_r5a ys_r5b) -> app{-r48,x-} alpha{-aJO-} rEverse{-r4b,x-} alpha{-aJO-} ys_r5b Cons{-rp,x-}{i} alpha{-aJO-} y_r5a Nil{-rq,x-}{i} alpha{-aJO-} {- nonrec -} {- rec -} AbsBinds [alpha{-aKi-}] [] [([alpha{-aKi-}], flatten{-r4c,x-}, flatten_aKf)] flatten_aKf t_r5d = case t_r5d of (Leaf{-rg,x-}{i} x_r5f) -> Cons{-rp,x-}{i} alpha{-aKi-} x_r5f Nil{-rq,x-}{i} alpha{-aKi-} (Node{-rf,x-}{i} l_r5h r_r5i) -> app{-r48,x-} alpha{-aKi-} flatten{-r4c,x-} alpha{-aKi-} l_r5h flatten{-r4c,x-} alpha{-aKi-} r_r5i {- nonrec -} {- rec -} AbsBinds [] [] [([], add{-r47,x-}, add_aKH)] add_aKH a_r4D b_r4F = case a_r4D of Zero{-rl,x-}{i} -> b_r4F (Succ{-rk,x-}{i} c_r4I) -> Succ{-rk,x-}{i} add{-r47,x-} c_r4I b_r4F {- nonrec -} {- rec -} AbsBinds [] [] [([], sUm{-r4d,x-}, sUm_aKR)] sUm_aKR t_r5k = case t_r5k of (Leaf{-rg,x-}{i} t_r5m) -> t_r5m (Node{-rf,x-}{i} l_r5o r_r5p) -> add{-r47,x-} sUm{-r4d,x-} l_r5o sUm{-r4d,x-} r_r5p {- nonrec -} {- rec -} AbsBinds [a{-aLe-}] [] [([a{-aLe-}], idl{-r46,x-}, idl_aLb)] idl_aLb xs_r4x = case xs_r4x of Nil{-rq,x-}{i} -> Nil{-rq,x-}{i} a{-aLe-} (Cons{-rp,x-}{i} y_r4A ys_r4B) -> Cons{-rp,x-}{i} a{-aLe-} y_r4A idl{-r46,x-} a{-aLe-} ys_r4B {- nonrec -} {- nonrec -} AbsBinds [alpha{-aLD-}] [] [([alpha{-aLD-}], nUll{-r45,x-}, nUll_aLA)] nUll_aLA l_r4r = case l_r4r of Nil{-rq,x-}{i} -> TT{-rw,x-}{i} (Cons{-rp,x-}{i} y_r4u ys_r4v) -> FF{-rx,x-}{i} {- nonrec -} {- nonrec -} AbsBinds [] [] [([], neg{-r44,x-}, neg_aLP)] neg_aLP b_r4n = case b_r4n of FF{-rx,x-}{i} -> TT{-rw,x-}{i} TT{-rw,x-}{i} -> FF{-rx,x-}{i} {- nonrec -} {- nonrec -} AbsBinds [a{-aM3-}, b{-aM4-}] [] [([b{-aM4-}, a{-aM3-}], swap{-r43,x-}, swap_aM0)] swap_aM0 t_r4i = case t_r4i of (Mkpair{-r5B,x-}{i} x_r4k y_r4l) -> Mkpair{-r5B,x-}{i} [b{-aM4-}, a{-aM3-}] y_r4l x_r4k {- nonrec -} {- nonrec -} AbsBinds [] [] [([], idb{-r42,x-}, idb_aMl)] idb_aMl x_r4g = x_r4g {- nonrec -} ghc: module version changed to 1; reason: no old .hi file _interface_ ShouldSucceed 1 _instance_modules_ ArrBase IO PrelNum _usages_ PrelBase 1 :: $d37 1 $d39 1 $d41 1 $d46 1 Eval 1; _exports_ ShouldSucceed add app before flatten idb idl lEngth nUll neg rEverse sUm swap Boolean(FF TT) List(Nil Cons) Nat(Zero Succ) Pair(Mkpair) Tree(Leaf Node); _instances_ instance _forall_ [a] => {PrelBase.Eval (Tree a)} = $d1; instance {PrelBase.Eval Nat} = $d2; instance _forall_ [a] => {PrelBase.Eval (List a)} = $d3; instance _forall_ [a b] => {PrelBase.Eval (Pair a b)} = $d4; instance {PrelBase.Eval Boolean} = $d5; _declarations_ 1 $d1 _:_ _forall_ [a] => {PrelBase.Eval (Tree a)} ;; 1 $d2 _:_ {PrelBase.Eval Nat} ;; 1 $d3 _:_ _forall_ [a] => {PrelBase.Eval (List a)} ;; 1 $d4 _:_ _forall_ [a b] => {PrelBase.Eval (Pair a b)} ;; 1 $d5 _:_ {PrelBase.Eval Boolean} ;; 1 data Boolean = FF | TT ; 1 data List r5u = Nil | Cons r5u (List r5u) ; 1 data Nat = Zero | Succ Nat ; 1 data Pair r5w r5x = Mkpair r5w r5x ; 1 data Tree r5r = Leaf r5r | Node (Tree r5r) (Tree r5r) ; 1 add _:_ Nat -> Nat -> Nat ;; 1 app _:_ _forall_ [a] => List a -> List a -> List a ;; 1 before _:_ List Nat -> List Nat ;; 1 flatten _:_ _forall_ [a] => Tree a -> List a ;; 1 idb _:_ Boolean -> Boolean ;; 1 idl _:_ _forall_ [a] => List a -> List a ;; 1 lEngth _:_ _forall_ [a] => List a -> Nat ;; 1 nUll _:_ _forall_ [a] => List a -> Boolean ;; 1 neg _:_ Boolean -> Boolean ;; 1 rEverse _:_ _forall_ [a] => List a -> List a ;; 1 sUm _:_ Tree Nat -> Nat ;; 1 swap _:_ _forall_ [a b] => Pair b a -> Pair a b ;;