mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
73d374e435
Don't just have a placeholder. While this doesn't have a huge effect (if any) on performance, it does generate smaller output for Chez to process, and is tidier. Perhaps it's good for other back ends too, ones that don't optimise as much as Chez does. Only doing named functions, not higher order functions. HOFs may be worth doing too, if we can, since this could remove lambdas and make fewer closures. The increment in TTC Version is necessary because otherwise there could be inconsistencies between libraries and clients erasure properties.
37 lines
3.5 KiB
Plaintext
37 lines
3.5 KiB
Plaintext
Dumping case trees to Main.cases
|
|
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
|
|
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
|
|
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
|
|
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
|
|
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
|
|
Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [1, (Main.plus [!{e:N}, !{arg:N}])])))
|
|
Main.main = [{ext:N}]: (Main.plus [(+Integer [1, 0]), (+Integer [1, (+Integer [1, 0])])])
|
|
Main.Z = Constructor tag Just 1 arity 0
|
|
Main.S = Constructor tag Just 0 arity 1
|
|
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
|
|
Prelude.Basics.True = Constructor tag Just 0 arity 0
|
|
Prelude.Basics.False = Constructor tag Just 1 arity 0
|
|
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
|
|
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
|
|
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
|
|
Prelude.Types.Z = Constructor tag Just 0 arity 0
|
|
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
|
|
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
|
Prelude.Interfaces.pure = [{arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
|
|
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
|
|
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
|
|
PrimIO.case block in io_bind = [{arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [!{arg:N}, ___, (!{arg:N} [!{arg:N}])])
|
|
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
|
|
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
|
|
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])
|
|
PrimIO.io_pure = [{arg:N}, {ext:N}]: !{arg:N}
|
|
PrimIO.io_bind = [{arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [!{arg:N}, (!{arg:N} [!{ext:N}])])
|
|
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
|
|
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
|
|
Prelude.IO.pure = [{arg:N}, {ext:N}]: !{arg:N}
|
|
Prelude.IO.map = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
|
|
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [!{ext:N}, !{ext:N}, !{ext:N}])
|
|
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [!func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
|
|
Prelude.IO.<*> = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
|
|
|