-Typechecked:
-AbsBinds [] [] [(idb.t1, ShouldSucceed.idb)]
- {- nonrec -}
- idb.t1 :: ShouldSucceed.Boolean -> ShouldSucceed.Boolean
- idb.t1
- x.r91 = x.r91
-AbsBinds [a.t12, b.t13] [] [(swap.t4, ShouldSucceed.swap)]
- {- nonrec -}
- swap.t4 :: ShouldSucceed.Pair b.t13 a.t12 -> ShouldSucceed.Pair a.t12 b.t13
- swap.t4
- t.r92 = case t.r92 of
- (ShouldSucceed.Mkpair x.r93 y.r94)
- -> (ShouldSucceed.Mkpair [a.t12, b.t13]) y.r94 x.r93
-AbsBinds [] [] [(neg.t16, ShouldSucceed.neg)]
- {- nonrec -}
- neg.t16 :: ShouldSucceed.Boolean -> ShouldSucceed.Boolean
- neg.t16
- b.r95 = case b.r95 of
- ShouldSucceed.FF
- -> ShouldSucceed.TT
- ShouldSucceed.TT
- -> ShouldSucceed.FF
-AbsBinds [alpha.t26] [] [(null.t20, ShouldSucceed.null)]
- {- nonrec -}
- null.t20 :: ShouldSucceed.List alpha.t26 -> ShouldSucceed.Boolean
- null.t20
- l.r96 = case l.r96 of
- ShouldSucceed.Nil
- -> ShouldSucceed.TT
- (ShouldSucceed.Cons y.r97 ys.r98)
- -> ShouldSucceed.FF
-AbsBinds [a.t30] [] [(idl.t29, ShouldSucceed.idl)]
- {- rec -}
- idl.t29 :: ShouldSucceed.List a.t30 -> ShouldSucceed.List a.t30
- idl.t29
- xs.r99 = case xs.r99 of
- ShouldSucceed.Nil
- -> ShouldSucceed.Nil a.t30
- (ShouldSucceed.Cons y.r100 ys.r101)
- -> (ShouldSucceed.Cons a.t30)
- y.r100 (idl.t29 ys.r101)
-AbsBinds [] [] [(add.t41, ShouldSucceed.add)]
- {- rec -}
- add.t41 :: ShouldSucceed.Nat -> ShouldSucceed.Nat -> ShouldSucceed.Nat
- add.t41
- a.r102 b.r103
- = case a.r102 of
- ShouldSucceed.Zero
- -> b.r103
- (ShouldSucceed.Succ c.r104)
- -> ShouldSucceed.Succ (add.t41 c.r104 b.r103)
-AbsBinds [alpha.t49] [] [(app.t48, ShouldSucceed.app)]
- {- rec -}
- app.t48 ::
- ShouldSucceed.List alpha.t49
- -> ShouldSucceed.List alpha.t49 -> ShouldSucceed.List alpha.t49
- app.t48
- xs.r105 zs.r106
- = case xs.r105 of
- ShouldSucceed.Nil
- -> zs.r106
- (ShouldSucceed.Cons y.r107 ys.r108)
- -> (ShouldSucceed.Cons alpha.t49)
- y.r107 (app.t48 ys.r108 zs.r106)
-AbsBinds [a.t61] [] [(length.t60, ShouldSucceed.length)]
- {- rec -}
- length.t60 :: ShouldSucceed.List a.t61 -> ShouldSucceed.Nat
- length.t60
- xs.r109 = case xs.r109 of
- ShouldSucceed.Nil
- -> ShouldSucceed.Zero
- (ShouldSucceed.Cons y.r110 ys.r111)
- -> ShouldSucceed.Succ (length.t60 ys.r111)
-AbsBinds [] [] [(before.t70, ShouldSucceed.before)]
- {- rec -}
- before.t70 ::
- ShouldSucceed.List ShouldSucceed.Nat
- -> ShouldSucceed.List ShouldSucceed.Nat
- before.t70
- xs.r112 = case xs.r112 of
- ShouldSucceed.Nil
- -> ShouldSucceed.Nil ShouldSucceed.Nat
- (ShouldSucceed.Cons y.r113 ys.r114)
- -> case y.r113 of
- ShouldSucceed.Zero
- -> ShouldSucceed.Nil ShouldSucceed.Nat
- (ShouldSucceed.Succ n.r115)
- -> (ShouldSucceed.Cons
- ShouldSucceed.Nat)
- y.r113 (before.t70 ys.r114)
-AbsBinds [alpha.t95] [] [(reverse.t84, ShouldSucceed.reverse)]
- {- rec -}
- reverse.t84 :: ShouldSucceed.List alpha.t95 -> ShouldSucceed.List alpha.t95
- reverse.t84
- rs.r116 = case rs.r116 of
- ShouldSucceed.Nil
- -> ShouldSucceed.Nil alpha.t95
- (ShouldSucceed.Cons y.r117 ys.r118)
- -> (ShouldSucceed.app alpha.t95)
- (reverse.t84 ys.r118)
- ((ShouldSucceed.Cons alpha.t95)
- y.r117 (ShouldSucceed.Nil alpha.t95))
-AbsBinds [alpha.t108] [] [(flatten.t98, ShouldSucceed.flatten)]
- {- rec -}
- flatten.t98 ::
- ShouldSucceed.Tree alpha.t108 -> ShouldSucceed.List alpha.t108
- flatten.t98
- t.r119 = case t.r119 of
- (ShouldSucceed.Leaf x.r120)
- -> (ShouldSucceed.Cons alpha.t108)
- x.r120 (ShouldSucceed.Nil alpha.t108)
- (ShouldSucceed.Node l.r121 r.r122)
- -> (ShouldSucceed.app alpha.t108)
- (flatten.t98 l.r121) (flatten.t98 r.r122)
-AbsBinds [] [] [(sum.t113, ShouldSucceed.sum)]
- {- rec -}
- sum.t113 :: ShouldSucceed.Tree ShouldSucceed.Nat -> ShouldSucceed.Nat
- sum.t113
- t.r123 = case t.r123 of
- (ShouldSucceed.Leaf t.r124)
- -> t.r124
- (ShouldSucceed.Node l.r125 r.r126)
- -> ShouldSucceed.add
- (sum.t113 l.r125) (sum.t113 r.r126)
+
+--================================================================================
+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 ;;
projects / ghc-hetmet.git / blobdiff