idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity
1d762d4920
Idris2/tests/codegen/con001/expected
Edwin Brady 1d762d4920 Print constructor labels correctly
2021-05-13 16:09:12 +01:00

48 lines
10 KiB
Plaintext
Raw Blame History

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}])
Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con [cons] Builtin.MkPair Just 0 [(%con [record] Prelude.Interfaces.MkFoldable Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input])))))))), (%lam elem (%lam {arg:N} (Prelude.Types.toList [!{arg:N}])))]), (%con [record] Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con [cons] Builtin.MkPair Just 0 [(%con [record] Prelude.Num.MkIntegral Just 0 [(%con [record] Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con [cons] Builtin.MkPair Just 0 [(%con [record] Prelude.EqOrd.MkOrd Just 0 [(%con [cons] Prelude.EqOrd.MkEq Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con [record] Prelude.Num.MkNeg Just 0 [(%con [record] Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
Prelude.Basics.Nil = Constructor tag Just 0 arity 0
Prelude.Basics.:: = Constructor tag Just 1 arity 2
Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase [cons] Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase [cons] Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
Builtin.MkPair = Constructor tag Just 0 arity 2
Prelude.Types.toList = [{ext:N}]: !{ext:N}
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (%case (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing) [(%constcase 1 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase [record] Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase [record] Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))] Nothing))])])), (%constcase 0 (%case (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing) [(%constcase 1 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase [record] Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase [record] Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))])])), (%constcase 0 (%con [cons] Prelude.Basics.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Basics.Nil Just 0 [])]))] Nothing))] Nothing)
Prelude.Types.null = [{arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%delay Lazy 1)), (%concase [cons] Prelude.Basics.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 0))] Nothing)
Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Basics.Nil Just 0 [] !{arg:N}), (%concase [cons] Prelude.Basics.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [!{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [nil] Prelude.Basics.Nil Just 0 [] !{arg:N}), (%concase [cons] Prelude.Basics.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [!{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase [record] Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case !{arg:N} [(%concase [record] Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase [record] Prelude.Interfaces.MkApplicative Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing))] Nothing), !{ext:N}])
Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [cons] Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (%case (!{arg:N} [!{e:N}]) [(%constcase 1 (%con [cons] Prelude.Basics.:: Just 1 [!{e:N}, (%con [nil] Prelude.Basics.Nil Just 0 [])])), (%constcase 0 (%con [cons] Prelude.Basics.:: Just 1 [!{e:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{e:N})])]))] Nothing))] Nothing)
Prelude.Types.prim__integerToNat = [{arg:N}]: (%case (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 0)] Just 1) [(%constcase 1 (Builtin.believe_me [!{arg:N}])), (%constcase 0 0)] Nothing)
Prelude.Types.countFrom = [{arg:N}, {arg:N}]: (%con [cons] Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
Prelude.Num.negate = [{arg:N}]: (-Int [0, !{arg:N}])
Prelude.Num.mod = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])]) [(%constcase 0 (%Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:L:C--L:C"]))
Prelude.Num.div = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])]) [(%constcase 0 (/Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:L:C--L:C"]))
Prelude.Num.- = [{ext:N}, {ext:N}]: (-Int [!{ext:N}, !{ext:N}])
Prelude.Num.MkNum = Constructor tag Just 0 arity 3
Prelude.Num.MkNeg = Constructor tag Just 0 arity 3
Prelude.Num.MkIntegral = Constructor tag Just 0 arity 3
Prelude.EqOrd.min = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]) [(%constcase 1 !{arg:N}), (%constcase 0 !{arg:N})] Nothing)
Prelude.EqOrd.max = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]) [(%constcase 1 !{arg:N}), (%constcase 0 !{arg:N})] Nothing)
Prelude.EqOrd.compare = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]) [(%constcase 1 0), (%constcase 0 (%case (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]) [(%constcase 1 1), (%constcase 0 2)] Nothing))] Nothing)
Prelude.EqOrd.> = [{arg:N}, {arg:N}]: (%case (>Int [!{arg:N}, !{arg:N}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.>= = [{arg:N}, {arg:N}]: (%case (>=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (%case (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]) [(%constcase 1 0), (%constcase 0 1)] Nothing)
Prelude.EqOrd.MkOrd = Constructor tag Just 0 arity 8
Prelude.EqOrd.MkEq = Constructor tag Just 0 arity 2
Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase [record] Prelude.Interfaces.MkFoldable Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {eta:N} (%case (Builtin.snd [!{arg:N}]) [(%concase [record] Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{eta:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase [record] Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
Prelude.Interfaces.MkFoldable = Constructor tag Just 0 arity 5
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.unsafeDestroyWorld [___, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])
Reference in New Issue View Git Blame Copy Permalink