--- /dev/null
+TOP = ../../..
+include $(TOP)/mk/boilerplate.mk
+
+HS_SRCS = $(wildcard *.hs)
+
+SRC_RUNTEST_OPTS += -accept-output -o1 $*.stdout -o2 $*.stderr -x 0
+HC_OPTS += -noC -O -ddump-simpl -dcore-lint
+
+%.o : %.hs
+
+%.o : %.hs
+ $(RUNTEST) $(HC) $(RUNTEST_OPTS) $(HC_OPTS) -c $< -o $@ -osuf $(subst .,,$(suffix $@))
+
+all :: $(HS_OBJS)
+
+include $(TOP)/mk/target.mk
--- /dev/null
+--!!! Desugaring sections with function-type arguments
+-- Although this is really a desugaring test, the problem is
+-- only tickled by the simplifier
+
+-- type Foo a b = a -> (b -> a) -> b
+module Test where
+
+(++++) :: (a -> (b -> a) -> b) -> (a -> (b -> a) -> b) -> a -> (b -> a) -> b
+x ++++ y = y
+
+g a xs = map (++++ a) xs
+
+h b xs = map (b ++++) xs
--- /dev/null
+
+
+================================================================================
+Simplified:
+++++{-r3h,x-} ::
+ _forall_
+ [a{-auX-} b{-auY-}]
+ =>
+ (a{-auX-} -> (b{-auY-} -> a{-auX-}) -> b{-auY-})
+ -> (a{-auX-} -> (b{-auY-} -> a{-auX-}) -> b{-auY-})
+ -> a{-auX-}
+ -> (b{-auY-} -> a{-auX-})
+ -> b{-auY-}
+_A>_ 2 {-# L #-}
+++++{-r3h,x-} =
+ _/\_ a{-sE8-} b{-sE9-} -> \ x_sDl ::
+ a{-sE8-} -> (b{-sE9-} -> a{-sE8-}) -> b{-sE9-}
+ {-# L #-}
+ x_sDl y_sCR ::
+ a{-sE8-} -> (b{-sE9-} -> a{-sE8-}) -> b{-sE9-}
+ {-# L #-}
+ y_sCR ->
+ y_sCR
+g{-r3j,x-} ::
+ _forall_
+ [a{-avh-} b{-avi-} rk0{-avq-}]
+ =>
+ {PrelBase.Functor{-2b,p-} rk0{-avq-}}
+ -> (a{-avh-} -> (b{-avi-} -> a{-avh-}) -> b{-avi-})
+ -> rk0{-avq-} (a{-avh-} -> (b{-avi-} -> a{-avh-}) -> b{-avi-})
+ -> rk0{-avq-} (a{-avh-} -> (b{-avi-} -> a{-avh-}) -> b{-avi-})
+_A>_ 3 {-# L #-}
+g{-r3j,x-} =
+ _/\_ a{-sEd-} b{-sEe-} rk0{-sEf-} -> \ d.Functor_sDp ::
+ {PrelBase.Functor{-2b,p-} rk0{-sEf-}}
+ {-# L #-}
+ d.Functor_sDp a_sDk ::
+ a{-sEd-}
+ -> (b{-sEe-} -> a{-sEd-})
+ -> b{-sEe-}
+ {-# L #-}
+ a_sDk xs_sDV ::
+ rk0{-sEf-} (a{-sEd-}
+ -> (b{-sEe-}
+ -> a{-sEd-})
+ -> b{-sEe-})
+ {-# L #-}
+ xs_sDV ->
+ let {
+ ds_sDr ::
+ (a{-sEd-} -> (b{-sEe-} -> a{-sEd-}) -> b{-sEe-})
+ -> a{-sEd-}
+ -> (b{-sEe-} -> a{-sEd-})
+ -> b{-sEe-}
+ _A>_ 1 {-# L #-}
+ ds_sDr =
+ \ ds_sDq ::
+ a{-sEd-} -> (b{-sEe-} -> a{-sEd-}) -> b{-sEe-}
+ {-# L #-}
+ ds_sDq ->
+ a_sDk
+ } in
+ d.Functor_sDp
+ _@_ (a{-sEd-} -> (b{-sEe-} -> a{-sEd-}) -> b{-sEe-})
+ _@_ (a{-sEd-} -> (b{-sEe-} -> a{-sEd-}) -> b{-sEe-})
+ ds_sDr
+ xs_sDV
+h{-r3i,x-} ::
+ _forall_
+ [a{-avI-} b{-avK-} rk0{-avT-}]
+ =>
+ {PrelBase.Functor{-2b,p-} rk0{-avT-}}
+ -> (a{-avI-} -> (b{-avK-} -> a{-avI-}) -> b{-avK-})
+ -> rk0{-avT-} (a{-avI-} -> (b{-avK-} -> a{-avI-}) -> b{-avK-})
+ -> rk0{-avT-} (a{-avI-} -> (b{-avK-} -> a{-avI-}) -> b{-avK-})
+_A>_ 3 {-# L #-}
+h{-r3i,x-} =
+ _/\_ a{-sEl-} b{-sEm-} rk0{-sEn-} -> \ d.Functor_sDZ ::
+ {PrelBase.Functor{-2b,p-} rk0{-sEn-}}
+ {-# L #-}
+ d.Functor_sDZ b_sEg ::
+ a{-sEl-}
+ -> (b{-sEm-} -> a{-sEl-})
+ -> b{-sEm-}
+ {-# L #-}
+ b_sEg xs_sEh ::
+ rk0{-sEn-} (a{-sEl-}
+ -> (b{-sEm-}
+ -> a{-sEl-})
+ -> b{-sEm-})
+ {-# L #-}
+ xs_sEh ->
+ let {
+ ds_sE0 ::
+ (a{-sEl-} -> (b{-sEm-} -> a{-sEl-}) -> b{-sEm-})
+ -> a{-sEl-}
+ -> (b{-sEm-} -> a{-sEl-})
+ -> b{-sEm-}
+ _A>_ 1 {-# L #-}
+ ds_sE0 =
+ \ ds_sDU ::
+ a{-sEl-} -> (b{-sEm-} -> a{-sEl-}) -> b{-sEm-}
+ {-# L #-}
+ ds_sDU ->
+ ds_sDU
+ } in
+ d.Functor_sDZ
+ _@_ (a{-sEl-} -> (b{-sEm-} -> a{-sEl-}) -> b{-sEm-})
+ _@_ (a{-sEl-} -> (b{-sEm-} -> a{-sEl-}) -> b{-sEm-})
+ ds_sE0
+ xs_sEh
--- /dev/null
+--!!! class/instance mumble that failed Lint at one time
+--
+module Test where
+class Foo a where
+ op :: Int -> a -> Bool
+
+data Wibble a b c = MkWibble a b c
+
+instance (Foo a, Foo b, Foo c) => Foo (Wibble a b c) where
+ op x y = error "xxx"
--- /dev/null
+
+
+================================================================================
+Simplified:
+nrlit_sMT ::
+ [PrelBase.Char{-38,p-}]
+{-# L #-}
+nrlit_sMT =
+ PackedString.unpackCString#{-8F,p-}
+ "xxx"
+$d1{-rJ7,x-} ::
+ _forall_
+ [a{-r3g-} b{-r3h-} c{-r3i-}]
+ =>
+ {Foo{-r3j,x-} a{-r3g-}}
+ -> {Foo{-r3j,x-} b{-r3h-}}
+ -> {Foo{-r3j,x-} c{-r3i-}}
+ -> {Foo{-r3j,x-} (Wibble{-r3y,x-} a{-r3g-} b{-r3h-} c{-r3i-})}
+_A>_ 3 {-# L #-}
+$d1{-rJ7,x-} =
+ _/\_ a{-sMG-} b{-sMH-} c{-sMI-} -> \ d.Foo_sLN ::
+ {Foo{-r3j,x-} a{-sMG-}}
+ {-# L #-}
+ d.Foo_sLN d.Foo_sLM ::
+ {Foo{-r3j,x-} b{-sMH-}}
+ {-# L #-}
+ d.Foo_sLM d.Foo_sLL ::
+ {Foo{-r3j,x-} c{-sMI-}}
+ {-# L #-}
+ d.Foo_sLL ->
+ let {
+ op_sLp ::
+ PrelBase.Int{-3g,p-}
+ -> Wibble{-r3y,x-} a{-sMG-} b{-sMH-} c{-sMI-}
+ -> PrelBase.Bool{-34,p-}
+ _A>_ 2 {-# L #-}
+ op_sLp =
+ \ x_sLs ::
+ PrelBase.Int{-3g,p-}
+ {-# L #-}
+ x_sLs y_sLq ::
+ Wibble{-r3y,x-} a{-sMG-} b{-sMH-} c{-sMI-}
+ {-# L #-}
+ y_sLq ->
+ IOBase.error{-87,p-}
+ _@_ PrelBase.Bool{-34,p-} nrlit_sMT } in
+ let {
+ op_sLO ::
+ PrelBase.Int{-3g,p-}
+ -> Wibble{-r3y,x-} a{-sMG-} b{-sMH-} c{-sMI-}
+ -> PrelBase.Bool{-34,p-}
+ _A>_ 2 {-# L #-}
+ op_sLO =
+ op_sLp } in
+ let {
+ d.Foo_sLP ::
+ {Foo{-r3j,x-} (Wibble{-r3y,x-} a{-sMG-} b{-sMH-} c{-sMI-})}
+ _A>_ 2 {-# L #-}
+ d.Foo_sLP =
+ op_sLp
+ } in
+ op_sLp
+$d2{-rJ2,x-} ::
+ _forall_
+ [a{-r3s-} b{-r3t-} c{-r3u-}]
+ =>
+ {PrelBase.Eval{-24,p-} (Wibble{-r3y,x-} a{-r3s-} b{-r3t-} c{-r3u-})}
+_A>_ 0 {-# L #-}
+$d2{-rJ2,x-} =
+ _/\_ a{-sMV-} b{-sMW-} c{-sMX-} ->
+ let {
+ d.Eval_sM2 ::
+ {PrelBase.Eval{-24,p-} (Wibble{-r3y,x-} a{-sMV-} b{-sMW-} c{-sMX-})}
+ {-# L #-}
+ d.Eval_sM2 =
+ PrelBase.void{-8G,p-}
+ } in
+ PrelBase.void{-8G,p-}
+nrlit_sMU ::
+ [PrelBase.Char{-38,p-}]
+{-# L #-}
+nrlit_sMU =
+ PackedString.unpackCString#{-8F,p-}
+ "Class Foo Method op"
+$mop{-rIV,x-} ::
+ _forall_
+ [a{-r3w-}]
+ =>
+ {Foo{-r3j,x-} a{-r3w-}}
+ -> PrelBase.Int{-3g,p-}
+ -> a{-r3w-}
+ -> PrelBase.Bool{-34,p-}
+_A>_ 3 {-# L #-}
+$mop{-rIV,x-} =
+ _/\_ a{-sMJ-} -> \ d.Foo_sMg ::
+ {Foo{-r3j,x-} a{-sMJ-}}
+ {-# L #-}
+ d.Foo_sMg ->
+ GHCerr.noDefaultMethodError{-8k,p-}
+ _@_ (PrelBase.Int{-3g,p-} -> a{-sMJ-} -> PrelBase.Bool{-34,p-})
+ nrlit_sMU
+op{-r3z,x-} ::
+ _forall_
+ [a{-r3w-}]
+ =>
+ {Foo{-r3j,x-} a{-r3w-}}
+ -> PrelBase.Int{-3g,p-}
+ -> a{-r3w-}
+ -> PrelBase.Bool{-34,p-}
+_A>_ 1 {-# L #-}
+op{-r3z,x-} =
+ _/\_ a{-sMK-} -> \ tpl_sMf ::
+ {Foo{-r3j,x-} a{-sMK-}}
+ {-# L #-}
+ tpl_sMf ->
+ tpl_sMf
+MkWibble{-r3x,x-}{i} ::
+ _forall_
+ [a{-r3s-} b{-r3t-} c{-r3u-}]
+ =>
+ a{-r3s-}
+ -> b{-r3t-}
+ -> c{-r3u-}
+ -> Wibble{-r3y,x-} a{-r3s-} b{-r3t-} c{-r3u-}
+_A>_ 3 {-# L #-}
+MkWibble{-r3x,x-}{i} =
+ _/\_ a{-sMO-} b{-sMP-} c{-sMQ-} -> \ tpl_sML ::
+ a{-sMO-}
+ {-# L #-}
+ tpl_sML tpl_sMM ::
+ b{-sMP-}
+ {-# L #-}
+ tpl_sMM tpl_sMN ::
+ c{-sMQ-}
+ {-# L #-}
+ tpl_sMN ->
+ MkWibble{-r3x,x-}{i}
+ {_@_ a{-sMO-} _@_ b{-sMP-} _@_ c{-sMQ-} tpl_sML tpl_sMM tpl_sMN}
--- /dev/null
+--!! INLINE on recursive functions.
+{-
+Date: Thu, 8 Dec 94 11:38:24 GMT
+From: Julian Seward (DRL PhD) <sewardj@computer-science.manchester.ac.uk>
+Message-Id: <9412081138.AA16652@rdf009.cs.man.ac.uk>
+To: partain@dcs.gla.ac.uk
+-}
+module ShouldFail where
+
+type IMonad a
+ = IMonadState -> IMonadReturn a
+
+data IMonadReturn a
+ = IMonadOk IMonadState a
+ | IMonadFail IMonadState String
+
+type IMonadState
+ = Int
+
+
+returnI r = \s0 -> IMonadOk s0 r
+
+failI msg = \s0 -> IMonadFail s0 msg
+
+thenI m k
+ = \s0 -> case m s0 of
+ IMonadFail s1 msg -> IMonadFail s1 msg
+ IMonadOk s1 r1 -> k r1 s1
+
+tickI n = \s0 -> IMonadOk (s0+n) ()
+
+mapI f [] = returnI []
+mapI f (x:xs) = f x `thenI` ( \ fx ->
+ mapI f xs `thenI` ( \ fxs ->
+ returnI (fx:fxs)
+ ))
+
+{-# INLINE returnI #-}
+{-# INLINE failI #-}
+{-# INLINE thenI #-}
+{-# INLINE tickI #-}
+{-# INLINE mapI #-}
--- /dev/null
+TOP = ../../..
+include $(TOP)/mk/boilerplate.mk
+
+HS_SRCS = $(wildcard *.lhs)
+
+SRC_RUNTEST_OPTS += -accept-output -o1 $*.stdout -o2 $*.stderr -x 0
+HC_OPTS += -noC -O -ddump-simpl -dcore-lint -dppr-user
+
+%.o : %.lhs
+
+%.o : %.lhs
+ $(RUNTEST) $(HC) $(RUNTEST_OPTS) -- $(HC_OPTS) -c $< -o $@ -osuf $(subst .,,$(suffix $@))
+
+all :: $(HS_OBJS)
+
+include $(TOP)/mk/target.mk
--- /dev/null
+> module Test where
+> data Boolean = FF | TT
+> data Pair a b = MkPair a b
+> data LList alpha = Nill | Conss alpha (LList alpha)
+> data Nat = Zero | Succ Nat
+> data Tree x = Leaf x | Node (Tree x) (Tree x)
+> data A a = MkA a (A a)
+>
+> append :: LList a -> LList a -> LList a
+> append xs ys = case xs of
+> Conss z zs -> Conss z (append zs ys)
+> v -> ys
+
+
+
+
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d5' ::
+ `{PrelBase.Eval (Pair a{-r3U-} b{-r3V-})}'
+`$d5' =
+ _/\_ `a{-s1gp-}' `b{-s1gq-}' ->
+ `PrelBase.void'
+`$d4' ::
+ `{PrelBase.Eval (LList alpha{-r3S-})}'
+`$d4' =
+ _/\_ `alpha{-s1gr-}' ->
+ `PrelBase.void'
+`$d2' ::
+ `{PrelBase.Eval (Tree x{-r3P-})}'
+`$d2' =
+ _/\_ `x{-s1gs-}' ->
+ `PrelBase.void'
+`$d1' ::
+ `{PrelBase.Eval (A a{-r3N-})}'
+`$d1' =
+ _/\_ `a{-s1gt-}' ->
+ `PrelBase.void'
+`MkPair' ::
+ `a{-r3U-} -> b{-r3V-} -> Pair a{-r3U-} b{-r3V-}'
+`MkPair' =
+ _/\_ `a{-s1gc-}' `b{-s1gd-}' -> \ `tpl' ::
+ `a{-s1gc-}'
+ `tpl' `tpl' ::
+ `b{-s1gd-}'
+ `tpl' ->
+ `MkPair'
+ {_@_ `a{-s1gc-}' _@_ `b{-s1gd-}' `tpl' `tpl'}
+`MkA' ::
+ `a{-r3N-} -> A a{-r3N-} -> A a{-r3N-}'
+`MkA' =
+ _/\_ `a{-s1ge-}' -> \ `tpl' ::
+ `a{-s1ge-}'
+ `tpl' `tpl' ::
+ `A a{-s1ge-}'
+ `tpl' ->
+ `MkA'
+ {_@_ `a{-s1ge-}' `tpl' `tpl'}
+`FF' ::
+ `Boolean'
+`FF' =
+ `FF'
+ {}
+`TT' ::
+ `Boolean'
+`TT' =
+ `TT'
+ {}
+`Nill' ::
+ `LList alpha{-r3S-}'
+`Nill' =
+ _/\_ `alpha{-s1gf-}' ->
+ `Nill'
+ {_@_ `alpha{-s1gf-}'}
+`Conss' ::
+ `alpha{-r3S-} -> LList alpha{-r3S-} -> LList alpha{-r3S-}'
+`Conss' =
+ _/\_ `alpha{-s1gg-}' -> \ `tpl' ::
+ `alpha{-s1gg-}'
+ `tpl' `tpl' ::
+ `LList alpha{-s1gg-}'
+ `tpl' ->
+ `Conss'
+ {_@_ `alpha{-s1gg-}' `tpl' `tpl'}
+Rec {
+`append' ::
+ `LList a{-aH9-} -> LList a{-aH9-} -> LList a{-aH9-}'
+`append' =
+ _/\_ `a{-s1gh-}' -> \ `xs' ::
+ `LList a{-s1gh-}'
+ `xs' `ys' ::
+ `LList a{-s1gh-}'
+ `ys' ->
+ case `xs' of {
+ `Nill' ->
+ `ys';
+ `Conss' `z' `zs' ->
+ let {
+ `ds' ::
+ `LList a{-s1gh-}'
+ `ds' =
+ `append'
+ _@_ `a{-s1gh-}' `zs' `ys'
+ } in
+ `Conss'
+ {_@_ `a{-s1gh-}' `z' `ds'};
+ }
+end Rec }
+`Zero' ::
+ `Nat'
+`Zero' =
+ `Zero'
+ {}
+`Succ' ::
+ `Nat -> Nat'
+`Succ' =
+ \ `tpl' ::
+ `Nat'
+ `tpl' ->
+ `Succ'
+ {`tpl'}
+`Leaf' ::
+ `x{-r3P-} -> Tree x{-r3P-}'
+`Leaf' =
+ _/\_ `x{-s1gl-}' -> \ `tpl' ::
+ `x{-s1gl-}'
+ `tpl' ->
+ `Leaf'
+ {_@_ `x{-s1gl-}' `tpl'}
+`Node' ::
+ `Tree x{-r3P-} -> Tree x{-r3P-} -> Tree x{-r3P-}'
+`Node' =
+ _/\_ `x{-s1go-}' -> \ `tpl' ::
+ `Tree x{-s1go-}'
+ `tpl' `tpl' ::
+ `Tree x{-s1go-}'
+ `tpl' ->
+ `Node'
+ {_@_ `x{-s1go-}' `tpl' `tpl'}
+`$d6' ::
+ `{PrelBase.Eval Boolean}'
+`$d6' =
+ `PrelBase.void'
+`$d3' ::
+ `{PrelBase.Eval Nat}'
+`$d3' =
+ `PrelBase.void'
--- /dev/null
+> module Test where
+> fact :: Int -> Int
+> fact n = if n==0 then 2 else (fact n) * n
--- /dev/null
+
+
+--================================================================================
+Simplified:
+Rec {
+`s1BQ' ::
+ `GHC.Int# -> PrelBase.Int'
+`s1BQ' =
+ \ `ww' ::
+ `GHC.Int#'
+ `ww' ->
+ case# `ww' of {
+ 0 ->
+ `PrelBase.I#'
+ {2};
+ `s' ->
+ case
+ `s1BQ'
+ `ww'
+ of {
+ `PrelBase.I#' `s1tCY' ->
+ case# *#! `s1tCY' `ww' of { `s1tDv' ->
+ `PrelBase.I#'
+ {`s1tDv'};};};
+ }
+end Rec }
+`fact' ::
+ `PrelBase.Int -> PrelBase.Int'
+`fact' =
+ \ `n' ::
+ `PrelBase.Int'
+ `n' ->
+ case `n' of { `PrelBase.I#' `ww' ->
+ `s1BQ'
+ `ww';}
--- /dev/null
+> module Test where
+> data Fun = MkFun (Fun -> Fun)
+> data LList a = Nill | Conss a (LList a)
+
+> id :: Fun -> Fun
+> id f = f
--- /dev/null
+> module Test where
+> data Goo a = Gsimpl | Gcompl ([Goo a])
+> data Moo a b = Msimple | Mcompl (Moo b a)
+
+
+> idGoo :: Goo a -> Goo a
+> idGoo x = x
+
+> idMoo :: Moo a -> Moo a
+> idMoo x = x
--- /dev/null
+TEST OF DEFACTORISATION FOR FUNCTIONS THAT DROP
+ POLYMORPHIC VARIABLES
+
+> module Test where
+> data Boolean = FF | TT
+> data Pair a b = MkPair a b
+> data LList alpha = Nill | Conss alpha (LList alpha)
+> data Nat = Zero | Succ Nat
+> data Tree x = Leaf x | Node (Tree x) (Tree x)
+> data A a = MkA a (A a)
+>
+> append :: LList a -> LList a -> LList a
+> append xs ys = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (append zs ys)
+
+The following function drops @b@.
+
+> flat :: Tree (Pair a b) -> LList a
+> flat t = case t of
+> Leaf (MkPair a b) -> Conss a Nill
+> Node l r -> append (flat l) (flat r)
+>
+> fl :: Boolean -> LList Boolean
+> fl x = flat (Leaf (MkPair TT Zero))
+>
+
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d5' ::
+ `{PrelBase.Eval (Pair a{-r4b-} b{-r4c-})}'
+`$d5' =
+ _/\_ `a{-s1NX-}' `b{-s1NY-}' ->
+ `PrelBase.void'
+`$d4' ::
+ `{PrelBase.Eval (LList alpha{-r49-})}'
+`$d4' =
+ _/\_ `alpha{-s1NZ-}' ->
+ `PrelBase.void'
+`$d2' ::
+ `{PrelBase.Eval (Tree x{-r46-})}'
+`$d2' =
+ _/\_ `x{-s1O0-}' ->
+ `PrelBase.void'
+`$d1' ::
+ `{PrelBase.Eval (A a{-r44-})}'
+`$d1' =
+ _/\_ `a{-s1O1-}' ->
+ `PrelBase.void'
+`MkPair' ::
+ `a{-r4b-} -> b{-r4c-} -> Pair a{-r4b-} b{-r4c-}'
+`MkPair' =
+ _/\_ `a{-s1NI-}' `b{-s1NJ-}' -> \ `tpl' ::
+ `a{-s1NI-}'
+ `tpl' `tpl' ::
+ `b{-s1NJ-}'
+ `tpl' ->
+ `MkPair'
+ {_@_ `a{-s1NI-}' _@_ `b{-s1NJ-}' `tpl' `tpl'}
+`MkA' ::
+ `a{-r44-} -> A a{-r44-} -> A a{-r44-}'
+`MkA' =
+ _/\_ `a{-s1NK-}' -> \ `tpl' ::
+ `a{-s1NK-}'
+ `tpl' `tpl' ::
+ `A a{-s1NK-}'
+ `tpl' ->
+ `MkA'
+ {_@_ `a{-s1NK-}' `tpl' `tpl'}
+`FF' ::
+ `Boolean'
+`FF' =
+ `FF'
+ {}
+`TT' ::
+ `Boolean'
+`TT' =
+ `TT'
+ {}
+`Nill' ::
+ `LList alpha{-r49-}'
+`Nill' =
+ _/\_ `alpha{-s1NL-}' ->
+ `Nill'
+ {_@_ `alpha{-s1NL-}'}
+`Conss' ::
+ `alpha{-r49-} -> LList alpha{-r49-} -> LList alpha{-r49-}'
+`Conss' =
+ _/\_ `alpha{-s1NM-}' -> \ `tpl' ::
+ `alpha{-s1NM-}'
+ `tpl' `tpl' ::
+ `LList alpha{-s1NM-}'
+ `tpl' ->
+ `Conss'
+ {_@_ `alpha{-s1NM-}' `tpl' `tpl'}
+Rec {
+`append' ::
+ `LList a{-aHq-} -> LList a{-aHq-} -> LList a{-aHq-}'
+`append' =
+ _/\_ `a{-s1NN-}' -> \ `xs' ::
+ `LList a{-s1NN-}'
+ `xs' `ys' ::
+ `LList a{-s1NN-}'
+ `ys' ->
+ case `xs' of {
+ `Nill' ->
+ `ys';
+ `Conss' `z' `zs' ->
+ let {
+ `ds' ::
+ `LList a{-s1NN-}'
+ `ds' =
+ `append'
+ _@_ `a{-s1NN-}' `zs' `ys'
+ } in
+ `Conss'
+ {_@_ `a{-s1NN-}' `z' `ds'};
+ }
+end Rec }
+Rec {
+`flat' ::
+ `Tree (Pair a{-aHT-} b{-aHU-}) -> LList a{-aHT-}'
+`flat' =
+ _/\_ `b{-s1NQ-}' `a{-s1NP-}' -> \ `s' ::
+ `Tree (Pair a{-s1NP-} b{-s1NQ-})'
+ `s' ->
+ case `s' of {
+ `Leaf' `ds' ->
+ case `ds' of { `MkPair' `a' `b' ->
+ let {
+ `ds' ::
+ `LList a{-s1NP-}'
+ `ds' =
+ `Nill'
+ {_@_ `a{-s1NP-}'}
+ } in
+ `Conss'
+ {_@_ `a{-s1NP-}' `a' `ds'};};
+ `Node' `l' `r' ->
+ case
+ `flat'
+ _@_ `b{-s1NQ-}' _@_ `a{-s1NP-}' `l'
+ of {
+ `ds' ->
+ let {
+ `ds' ::
+ `LList a{-s1NP-}'
+ `ds' =
+ `flat'
+ _@_ `b{-s1NQ-}' _@_ `a{-s1NP-}' `r'
+ } in
+ `append'
+ _@_ `a{-s1NP-}' `ds' `ds';};
+ }
+end Rec }
+`Zero' ::
+ `Nat'
+`Zero' =
+ `Zero'
+ {}
+`Succ' ::
+ `Nat -> Nat'
+`Succ' =
+ \ `tpl' ::
+ `Nat'
+ `tpl' ->
+ `Succ'
+ {`tpl'}
+`Leaf' ::
+ `x{-r46-} -> Tree x{-r46-}'
+`Leaf' =
+ _/\_ `x{-s1NU-}' -> \ `tpl' ::
+ `x{-s1NU-}'
+ `tpl' ->
+ `Leaf'
+ {_@_ `x{-s1NU-}' `tpl'}
+`Node' ::
+ `Tree x{-r46-} -> Tree x{-r46-} -> Tree x{-r46-}'
+`Node' =
+ _/\_ `x{-s1NV-}' -> \ `tpl' ::
+ `Tree x{-s1NV-}'
+ `tpl' `tpl' ::
+ `Tree x{-s1NV-}'
+ `tpl' ->
+ `Node'
+ {_@_ `x{-s1NV-}' `tpl' `tpl'}
+`$d6' ::
+ `{PrelBase.Eval Boolean}'
+`$d6' =
+ `PrelBase.void'
+`$d3' ::
+ `{PrelBase.Eval Nat}'
+`$d3' =
+ `PrelBase.void'
+`s1h2' ::
+ `Pair Boolean Nat'
+`s1h2' =
+ `MkPair'
+ {_@_ `Boolean' _@_ `Nat' `TT' `Zero'}
+`s1h7' ::
+ `Tree (Pair Boolean Nat)'
+`s1h7' =
+ `Leaf'
+ {_@_ (`Pair' `Boolean' `Nat') `s1h2'}
+`s1l4' ::
+ `LList Boolean'
+`s1l4' =
+ `flat'
+ _@_ `Nat' _@_ `Boolean' `s1h7'
+`fl' ::
+ `Boolean -> LList Boolean'
+`fl' =
+ \ `x' ::
+ `Boolean'
+ `x' ->
+ `s1l4'
--- /dev/null
+> module Test where
+> data Boolean = FF | TT
+> data Pair a b = MkPair a b
+> data LList alpha = Nill | Conss alpha (LList alpha)
+> data Nat = Zero | Succ Nat
+> data Tree x = Leaf x | Node (Tree x) (Tree x)
+> data A a = MkA a (A a)
+
+> {-
+> map :: (a -> b) -> [a] -> [b]
+> map f xs = case xs of
+> [] -> []
+> (y:ys) -> (f y):(map f ys)
+
+> map_ide :: [[a]] -> [[a]]
+> map_ide = map (\x->x)
+>-}
+
+> id :: a -> a
+> id x = x
+
+> idNat :: Nat -> Nat
+> idNat x = x
+
+> idBool :: Boolean -> Boolean
+> idBool x = x
+
+> fun :: (a->b) -> a -> b
+> fun f x = g f
+> where
+> g f = f x
+
--- /dev/null
+> module Test where
+> data Moo a b = Msimple | Mcompl (Moo b a)
+
+
+> idMoo :: Moo a -> Moo a
+> idMoo x = x
--- /dev/null
+> module Test where
+> data Boolean = FF | TT
+> data Pair a b = MkPair a b
+> data LList alpha = Nill | Conss alpha (LList alpha)
+> data Nat = Zero | Succ Nat
+> data Tree x = Leaf x | Node (Tree x) (Tree x)
+> data A a = MkA a (A a)
+>{-
+> id :: a -> a
+> id x = x
+>
+> idb :: Boolean -> Boolean
+> idb b = b
+>
+> swap :: Pair a b -> Pair b a
+> swap t = case t of
+> MkPair x y -> MkPair y x
+>
+> bang :: A (A a) -> Boolean
+> bang x = case x of
+> MkA y ys -> TT
+>
+> neg :: Boolean -> Boolean
+> neg b = case b of
+> FF -> TT
+> TT -> FF
+>
+> null :: LList x -> Boolean
+> null l = case l of
+> Nill -> TT
+> _ -> FF
+>
+> loop :: Boolean -> a
+> loop b = loop b
+>-}
+> idl :: LList a -> LList a
+> idl xs = case xs of
+> Conss y ys -> Conss y (idl ys)
+> _ -> Nill
+>{-
+> idn :: Nat -> Nat
+> idn n = case n of
+> Zero -> Zero
+> Succ m -> Succ (idn m)
+>
+> add :: Nat -> Nat -> Nat
+> add a b = case a of
+> Zero -> b
+> Succ c -> Succ (add c b)
+>
+> length :: LList a -> Nat
+> length xs = case xs of
+> Nill -> Zero
+> Conss y ys -> Succ(length ys)
+>
+> before :: LList Nat -> LList Nat
+> before xs = case xs of
+> Nill -> Nill
+> Conss y ys -> case y of
+> Zero -> Nill
+> Succ n -> Conss y (before ys)
+>
+> reverse :: LList a -> LList a
+> reverse rs = case rs of
+> Nill -> Nill
+> Conss y ys -> append (reverse ys) (Conss y Nill)
+>
+> f :: Nat -> Nat
+> f n = case n of
+> Zero -> Zero
+> Succ m -> Succ (g m)
+>
+> g :: Nat -> Nat
+> g n = case n of
+> Zero -> Zero
+> Succ m -> Succ (f m)
+>
+> append :: LList a -> LList a -> LList a
+> append xs ys = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (append zs ys)
+>
+> flatten :: Tree alpha -> LList alpha
+> flatten t = case t of
+> Leaf x -> Conss x Nill
+> Node l r -> append (flatten l) (flatten r)
+>
+> sum :: Tree Nat -> Nat
+> sum t = case t of
+> Leaf t -> t
+> Node l r -> add (sum l) (sum r)
+>
+> suml :: LList Nat -> Nat
+> suml Nill = Zero
+> suml (Conss n ns) = add n (suml ns)
+>
+> map :: (a -> b) -> LList a -> LList b
+> map f xs = case xs of
+> Nill -> Nill
+> Conss y ys -> Conss (f y) (map f ys)
+>-}
+
+
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d5' ::
+ `{PrelBase.Eval (Pair a{-r3R-} b{-r3S-})}'
+`$d5' =
+ _/\_ `a{-s1g3-}' `b{-s1g4-}' ->
+ `PrelBase.void'
+`$d4' ::
+ `{PrelBase.Eval (LList alpha{-r3P-})}'
+`$d4' =
+ _/\_ `alpha{-s1g5-}' ->
+ `PrelBase.void'
+`$d2' ::
+ `{PrelBase.Eval (Tree x{-r3M-})}'
+`$d2' =
+ _/\_ `x{-s1g6-}' ->
+ `PrelBase.void'
+`$d1' ::
+ `{PrelBase.Eval (A a{-r3K-})}'
+`$d1' =
+ _/\_ `a{-s1g7-}' ->
+ `PrelBase.void'
+`MkPair' ::
+ `a{-r3R-} -> b{-r3S-} -> Pair a{-r3R-} b{-r3S-}'
+`MkPair' =
+ _/\_ `a{-s1fQ-}' `b{-s1fR-}' -> \ `tpl' ::
+ `a{-s1fQ-}'
+ `tpl' `tpl' ::
+ `b{-s1fR-}'
+ `tpl' ->
+ `MkPair'
+ {_@_ `a{-s1fQ-}' _@_ `b{-s1fR-}' `tpl' `tpl'}
+`MkA' ::
+ `a{-r3K-} -> A a{-r3K-} -> A a{-r3K-}'
+`MkA' =
+ _/\_ `a{-s1fS-}' -> \ `tpl' ::
+ `a{-s1fS-}'
+ `tpl' `tpl' ::
+ `A a{-s1fS-}'
+ `tpl' ->
+ `MkA'
+ {_@_ `a{-s1fS-}' `tpl' `tpl'}
+`FF' ::
+ `Boolean'
+`FF' =
+ `FF'
+ {}
+`TT' ::
+ `Boolean'
+`TT' =
+ `TT'
+ {}
+`Nill' ::
+ `LList alpha{-r3P-}'
+`Nill' =
+ _/\_ `alpha{-s1fT-}' ->
+ `Nill'
+ {_@_ `alpha{-s1fT-}'}
+`Conss' ::
+ `alpha{-r3P-} -> LList alpha{-r3P-} -> LList alpha{-r3P-}'
+`Conss' =
+ _/\_ `alpha{-s1fU-}' -> \ `tpl' ::
+ `alpha{-s1fU-}'
+ `tpl' `tpl' ::
+ `LList alpha{-s1fU-}'
+ `tpl' ->
+ `Conss'
+ {_@_ `alpha{-s1fU-}' `tpl' `tpl'}
+Rec {
+`idl' ::
+ `LList a{-aH5-} -> LList a{-aH5-}'
+`idl' =
+ _/\_ `a{-s1fV-}' -> \ `xs' ::
+ `LList a{-s1fV-}'
+ `xs' ->
+ case `xs' of {
+ `Nill' ->
+ `Nill'
+ {_@_ `a{-s1fV-}'};
+ `Conss' `y' `ys' ->
+ let {
+ `ds' ::
+ `LList a{-s1fV-}'
+ `ds' =
+ `idl'
+ _@_ `a{-s1fV-}' `ys'
+ } in
+ `Conss'
+ {_@_ `a{-s1fV-}' `y' `ds'};
+ }
+end Rec }
+`Zero' ::
+ `Nat'
+`Zero' =
+ `Zero'
+ {}
+`Succ' ::
+ `Nat -> Nat'
+`Succ' =
+ \ `tpl' ::
+ `Nat'
+ `tpl' ->
+ `Succ'
+ {`tpl'}
+`Leaf' ::
+ `x{-r3M-} -> Tree x{-r3M-}'
+`Leaf' =
+ _/\_ `x{-s1fZ-}' -> \ `tpl' ::
+ `x{-s1fZ-}'
+ `tpl' ->
+ `Leaf'
+ {_@_ `x{-s1fZ-}' `tpl'}
+`Node' ::
+ `Tree x{-r3M-} -> Tree x{-r3M-} -> Tree x{-r3M-}'
+`Node' =
+ _/\_ `x{-s1g2-}' -> \ `tpl' ::
+ `Tree x{-s1g2-}'
+ `tpl' `tpl' ::
+ `Tree x{-s1g2-}'
+ `tpl' ->
+ `Node'
+ {_@_ `x{-s1g2-}' `tpl' `tpl'}
+`$d6' ::
+ `{PrelBase.Eval Boolean}'
+`$d6' =
+ `PrelBase.void'
+`$d3' ::
+ `{PrelBase.Eval Nat}'
+`$d3' =
+ `PrelBase.void'
--- /dev/null
+THIS TEST IS FOR TYPE SYNONIMS AND FACTORISATION IN THEIR PRESENCE.
+
+> module Test where
+> data M a = A | B a (M a)
+> data L a = N | C a (Syn a)
+> type Syn b = L b
+>
+> idL :: L (Syn c) -> L (Syn c)
+> idL N = N
+> idL (C x l) = C x (idL l)
+>
+> idM:: M (L (Syn x)) -> M (L (Syn x))
+> idM A = A
+> idM (B x l) = B (idL x) (idM l)
+
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d2' ::
+ `{PrelBase.Eval (M a{-r3H-})}'
+`$d2' =
+ _/\_ `a{-s191-}' ->
+ `PrelBase.void'
+`$d1' ::
+ `{PrelBase.Eval (L a{-r3F-})}'
+`$d1' =
+ _/\_ `a{-s192-}' ->
+ `PrelBase.void'
+`A' ::
+ `M a{-r3H-}'
+`A' =
+ _/\_ `a{-s18T-}' ->
+ `A' {_@_ `a{-s18T-}'}
+`B' ::
+ `a{-r3H-} -> M a{-r3H-} -> M a{-r3H-}'
+`B' =
+ _/\_ `a{-s18U-}' -> \ `tpl' ::
+ `a{-s18U-}'
+ `tpl' `tpl' ::
+ `M a{-s18U-}'
+ `tpl' ->
+ `B' {_@_ `a{-s18U-}' `tpl' `tpl'}
+`N' ::
+ `L a{-r3F-}'
+`N' =
+ _/\_ `a{-s18V-}' ->
+ `N' {_@_ `a{-s18V-}'}
+`C' ::
+ `a{-r3F-} -> Syn a{-r3F-} -> L a{-r3F-}'
+`C' =
+ _/\_ `a{-s18W-}' -> \ `tpl' ::
+ `a{-s18W-}'
+ `tpl' `tpl' ::
+ `Syn a{-s18W-}'
+ `tpl' ->
+ `C' {_@_ `a{-s18W-}' `tpl' `tpl'}
+Rec {
+`idL' ::
+ `L (Syn c{-aGI-}) -> L (Syn c{-aGI-})'
+`idL' =
+ _/\_ `c{-s18X-}' -> \ `ds' ::
+ `L (Syn c{-s18X-})'
+ `ds' ->
+ case `ds' of {
+ `N' ->
+ `N' {_@_ (`Syn' `c{-s18X-}')};
+ `C' `x' `l' ->
+ let {
+ `ds' ::
+ `L (Syn c{-s18X-})'
+ `ds' =
+ `idL'
+ _@_ `c{-s18X-}' `l'
+ } in
+ `C' {_@_ (`Syn' `c{-s18X-}') `x' `ds'};
+ }
+end Rec }
+Rec {
+`idM' ::
+ `M (L (Syn x{-aH8-})) -> M (L (Syn x{-aH8-}))'
+`idM' =
+ _/\_ `x{-s18Z-}' -> \ `ds' ::
+ `M (L (Syn x{-s18Z-}))'
+ `ds' ->
+ case `ds' of {
+ `A' ->
+ `A' {_@_ (`L' (`Syn' `x{-s18Z-}'))};
+ `B' `x' `l' ->
+ let {
+ `ds' ::
+ `L (Syn x{-s18Z-})'
+ `ds' =
+ `idL'
+ _@_ `x{-s18Z-}' `x' } in
+ let {
+ `ds' ::
+ `M (L (Syn x{-s18Z-}))'
+ `ds' =
+ `idM'
+ _@_ `x{-s18Z-}' `l'
+ } in
+ `B' {_@_ (`L' (`Syn' `x{-s18Z-}')) `ds' `ds'};
+ }
+end Rec }
--- /dev/null
+> module Test where
+> data LList t = Nill | Conss t (LList t)
+> data BBool = TTrue | FFalse
+
+> f Nill = TTrue
+> f (Conss a as) = FFalse
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d2' ::
+ `{PrelBase.Eval (LList t{-r3s-})}'
+`$d2' =
+ _/\_ `t{-sUf-}' ->
+ `PrelBase.void'
+`Nill' ::
+ `LList t{-r3s-}'
+`Nill' =
+ _/\_ `t{-sUc-}' ->
+ `Nill'
+ {_@_ `t{-sUc-}'}
+`Conss' ::
+ `t{-r3s-} -> LList t{-r3s-} -> LList t{-r3s-}'
+`Conss' =
+ _/\_ `t{-sUd-}' -> \ `tpl' ::
+ `t{-sUd-}'
+ `tpl' `tpl' ::
+ `LList t{-sUd-}'
+ `tpl' ->
+ `Conss'
+ {_@_ `t{-sUd-}' `tpl' `tpl'}
+`TTrue' ::
+ `BBool'
+`TTrue' =
+ `TTrue'
+ {}
+`FFalse' ::
+ `BBool'
+`FFalse' =
+ `FFalse'
+ {}
+`f' ::
+ `LList t{-aGi-} -> BBool'
+`f' =
+ _/\_ `t{-sUe-}' -> \ `ds' ::
+ `LList t{-sUe-}'
+ `ds' ->
+ case `ds' of {
+ `Nill' ->
+ `TTrue'
+ {};
+ `Conss' `a' `as' ->
+ `FFalse'
+ {};
+ }
+`$d1' ::
+ `{PrelBase.Eval BBool}'
+`$d1' =
+ `PrelBase.void'
--- /dev/null
+> module Test where
+> a :: [a] -> [[a]]
+> a x = [x]
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`a' ::
+ `[a{-amL-}] -> [[a{-amL-}]]'
+`a' =
+ _/\_ `a{-srv-}' -> \ `s' ::
+ `[a{-srv-}]'
+ `s' ->
+ let {
+ `ds' ::
+ `[[a{-srv-}]]'
+ `ds' =
+ `PrelBase.[]'
+ {_@_ [`a{-srv-}']}
+ } in
+ `PrelBase.:'
+ {_@_ [`a{-srv-}'] `s' `ds'}
--- /dev/null
+> module Test where
+> data Boolean = FF | TT
+> data Pair a b = Mkpair a b
+> data LList alpha = Nill | Conss alpha (LList alpha)
+> data Nat = Zero | Succ Nat
+> data Tree t = Leaf t | Node (Tree t) (Tree t)
+> data A a = MkA a (A a)
+> data Foo baz = MkFoo (Foo (Foo baz))
+>{-
+> append1 :: LList a -> LList a -> LList a
+> append1 xs ys = append2 xs
+> where
+> append2 xs = case xs of
+> Nill -> ys
+> Conss x xs -> Conss x (append3 xs)
+> append3 xs = case xs of
+> Nill -> ys
+> Conss x xs -> Conss x (append2 xs)
+>
+> loop :: a -> a
+> loop x = loop x
+>
+> hd :: LList b -> b
+> hd Nill = loop
+> hd (Conss y ys) = y
+>
+> hdb :: LList (LList b) -> LList b
+> hdb = hd
+>
+> append :: [a] -> [a] -> [a]
+> append [] ys = ys
+> append (x:xs) ys = x:(append xs ys)
+>
+> f :: [a] -> [a]
+> f y = append x (f y)
+> where x = append x (f y)
+>-}
+> app :: LList a -> LList a -> LList a
+> app Nill Nill = Nill
+> app xs ys = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (app zs ys)
+>{-
+> app :: LList a -> LList a -> LList a
+> app xs ys = case xs of
+> Nill -> case ys of
+> Nill -> Nill
+> Conss u us -> ap
+> Conss a as -> ap
+> where ap = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (app zs ys)
+>
+> app :: LList a -> LList a -> LList a
+> app xs ys = case xs of
+> Nill -> case ys of
+> Nill -> Nill
+> Conss u us -> ap xs ys
+> Conss a as -> ap xs ys
+>
+> ap xs ys = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (app zs ys)
+>
+> ap :: LList a -> LList a -> LList a
+> ap xs ys = case xs of
+> Nill -> ys
+> Conss z zs -> Conss z (ap zs ys)
+>
+> app :: LList a -> LList a -> LList a
+> app xs ys = case xs of
+> Nill -> case ys of
+> Nill -> Nill
+> Conss u us -> ap xs ys
+> Conss a as -> ap xs ys
+>-}
--- /dev/null
+
+
+--================================================================================
+Simplified:
+`$d6' ::
+ `{PrelBase.Eval (Pair a{-r3Z-} b{-r40-})}'
+`$d6' =
+ _/\_ `a{-s1oF-}' `b{-s1oG-}' ->
+ `PrelBase.void'
+`$d5' ::
+ `{PrelBase.Eval (LList alpha{-r3X-})}'
+`$d5' =
+ _/\_ `alpha{-s1oH-}' ->
+ `PrelBase.void'
+`$d3' ::
+ `{PrelBase.Eval (Tree t{-r3U-})}'
+`$d3' =
+ _/\_ `t{-s1oI-}' ->
+ `PrelBase.void'
+`$d2' ::
+ `{PrelBase.Eval (A a{-r3S-})}'
+`$d2' =
+ _/\_ `a{-s1oJ-}' ->
+ `PrelBase.void'
+`$d1' ::
+ `{PrelBase.Eval (Foo baz{-r3Q-})}'
+`$d1' =
+ _/\_ `baz{-s1oK-}' ->
+ `PrelBase.void'
+`Mkpair' ::
+ `a{-r3Z-} -> b{-r40-} -> Pair a{-r3Z-} b{-r40-}'
+`Mkpair' =
+ _/\_ `a{-s1op-}' `b{-s1oq-}' -> \ `tpl' ::
+ `a{-s1op-}'
+ `tpl' `tpl' ::
+ `b{-s1oq-}'
+ `tpl' ->
+ `Mkpair'
+ {_@_ `a{-s1op-}' _@_ `b{-s1oq-}' `tpl' `tpl'}
+`MkA' ::
+ `a{-r3S-} -> A a{-r3S-} -> A a{-r3S-}'
+`MkA' =
+ _/\_ `a{-s1or-}' -> \ `tpl' ::
+ `a{-s1or-}'
+ `tpl' `tpl' ::
+ `A a{-s1or-}'
+ `tpl' ->
+ `MkA'
+ {_@_ `a{-s1or-}' `tpl' `tpl'}
+`MkFoo' ::
+ `Foo (Foo baz{-r3Q-}) -> Foo baz{-r3Q-}'
+`MkFoo' =
+ _/\_ `baz{-s1os-}' -> \ `tpl' ::
+ `Foo (Foo baz{-s1os-})'
+ `tpl' ->
+ `MkFoo'
+ {_@_ `baz{-s1os-}' `tpl'}
+`FF' ::
+ `Boolean'
+`FF' =
+ `FF'
+ {}
+`TT' ::
+ `Boolean'
+`TT' =
+ `TT'
+ {}
+`Nill' ::
+ `LList alpha{-r3X-}'
+`Nill' =
+ _/\_ `alpha{-s1ot-}' ->
+ `Nill'
+ {_@_ `alpha{-s1ot-}'}
+`Conss' ::
+ `alpha{-r3X-} -> LList alpha{-r3X-} -> LList alpha{-r3X-}'
+`Conss' =
+ _/\_ `alpha{-s1ou-}' -> \ `tpl' ::
+ `alpha{-s1ou-}'
+ `tpl' `tpl' ::
+ `LList alpha{-s1ou-}'
+ `tpl' ->
+ `Conss'
+ {_@_ `alpha{-s1ou-}' `tpl' `tpl'}
+Rec {
+`app' ::
+ `LList a{-aHn-} -> LList a{-aHn-} -> LList a{-aHn-}'
+`app' =
+ _/\_ `a{-s1ov-}' -> \ `ds' ::
+ `LList a{-s1ov-}'
+ `ds' `ds' ::
+ `LList a{-s1ov-}'
+ `ds' ->
+ case `ds' of {
+ `Conss' `ds' `ds' ->
+ let {
+ `ds' ::
+ `LList a{-s1ov-}'
+ `ds' =
+ `app'
+ _@_ `a{-s1ov-}' `ds' `ds'
+ } in
+ `Conss'
+ {_@_ `a{-s1ov-}' `ds' `ds'};
+ `Nill' ->
+ case `ds' of {
+ `Conss' `ds' `ds' ->
+ `Conss'
+ {_@_ `a{-s1ov-}' `ds' `ds'};
+ `Nill' ->
+ `Nill'
+ {_@_ `a{-s1ov-}'};
+ };
+ }
+end Rec }
+`Zero' ::
+ `Nat'
+`Zero' =
+ `Zero'
+ {}
+`Succ' ::
+ `Nat -> Nat'
+`Succ' =
+ \ `tpl' ::
+ `Nat'
+ `tpl' ->
+ `Succ'
+ {`tpl'}
+`Leaf' ::
+ `t{-r3U-} -> Tree t{-r3U-}'
+`Leaf' =
+ _/\_ `t{-s1oB-}' -> \ `tpl' ::
+ `t{-s1oB-}'
+ `tpl' ->
+ `Leaf'
+ {_@_ `t{-s1oB-}' `tpl'}
+`Node' ::
+ `Tree t{-r3U-} -> Tree t{-r3U-} -> Tree t{-r3U-}'
+`Node' =
+ _/\_ `t{-s1oE-}' -> \ `tpl' ::
+ `Tree t{-s1oE-}'
+ `tpl' `tpl' ::
+ `Tree t{-s1oE-}'
+ `tpl' ->
+ `Node'
+ {_@_ `t{-s1oE-}' `tpl' `tpl'}
+`$d7' ::
+ `{PrelBase.Eval Boolean}'
+`$d7' =
+ `PrelBase.void'
+`$d4' ::
+ `{PrelBase.Eval Nat}'
+`$d4' =
+ `PrelBase.void'