+++ /dev/null
-
-
---================================================================================
-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 ;;