idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1220 ] Update arity of constuctors to reflect erased args (#1225)

Browse Source
This commit is contained in:
Zoe Stafford 2021-03-29 15:08:06 +01:00 committed by GitHub
parent 802113772f
commit f255026d1b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 157 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Compiler/CompileExpr.idr
View File

@ -629,8 +629,14 @@ toCDef n ty (Builtin {arity} op)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n _ (DCon tag arity pos)
= let nt = maybe Nothing (Just . snd) pos in
pure $ MkCon (Just tag) arity nt
= do let nt = snd <$> pos
defs <- get Ctxt
args <- numArgs {vars = []} defs (Ref EmptyFC (DataCon tag arity) n)
let arity' = case args of
NewTypeBy ar _ => ar
EraseArgs ar erased => ar `minus` length erased
Arity ar => ar
pure $ MkCon (Just tag) arity' nt
toCDef n _ (TCon tag arity _ _ _ _ _ _)
= pure $ MkCon Nothing arity Nothing
-- We do want to be able to compile these, but also report an error at run time

6
tests/Main.idr
View File

@ -248,6 +248,11 @@ baseLibraryTests = MkTestPool [Chez, Node]
, "system_info001"
]
codegenTests : TestPool
codegenTests = MkTestPool []
[ "con001"
]
main : IO ()
main = runner
[ testPaths "ttimp" ttimpTests
@ -271,6 +276,7 @@ main = runner
, testPaths "racket" racketTests
, testPaths "node" nodeTests
, testPaths "templates" templateTests
, testPaths "codegen" codegenTests
] where
testPaths : String -> TestPool -> TestPool

7
tests/codegen/con001/CatCases.idr Normal file
View File

@ -0,0 +1,7 @@
import System.File
main : IO ()
main = do
Right str <- readFile "Main.cases"
| Left err => putStrLn "Error:" *> printLn err
putStrLn str

2
tests/codegen/con001/Main.idr Normal file
View File

@ -0,0 +1,2 @@
main : IO Int
main = pure $ sum $ [1 .. 100]

128
tests/codegen/con001/expected Normal file
View File

@ -0,0 +1,128 @@
Dumping case trees to Main.cases
prim__add_Int = [{arg:0}, {arg:1}]: (+Int [!{arg:0}, !{arg:1}])
prim__add_Integer = [{arg:0}, {arg:1}]: (+Integer [!{arg:0}, !{arg:1}])
prim__sub_Int = [{arg:0}, {arg:1}]: (-Int [!{arg:0}, !{arg:1}])
prim__sub_Integer = [{arg:0}, {arg:1}]: (-Integer [!{arg:0}, !{arg:1}])
prim__mul_Int = [{arg:0}, {arg:1}]: (*Int [!{arg:0}, !{arg:1}])
prim__mul_Integer = [{arg:0}, {arg:1}]: (*Integer [!{arg:0}, !{arg:1}])
prim__div_Int = [{arg:0}, {arg:1}]: (/Int [!{arg:0}, !{arg:1}])
prim__mod_Int = [{arg:0}, {arg:1}]: (%Int [!{arg:0}, !{arg:1}])
prim__lt_Int = [{arg:0}, {arg:1}]: (<Int [!{arg:0}, !{arg:1}])
prim__lte_Int = [{arg:0}, {arg:1}]: (<=Int [!{arg:0}, !{arg:1}])
prim__lte_Integer = [{arg:0}, {arg:1}]: (<=Integer [!{arg:0}, !{arg:1}])
prim__eq_Int = [{arg:0}, {arg:1}]: (==Int [!{arg:0}, !{arg:1}])
prim__gte_Int = [{arg:0}, {arg:1}]: (>=Int [!{arg:0}, !{arg:1}])
prim__gt_Int = [{arg:0}, {arg:1}]: (>Int [!{arg:0}, !{arg:1}])
prim__believe_me = [{arg:0}, {arg:1}, {arg:2}]: (believe_me [!{arg:0}, !{arg:1}, !{arg:2}])
prim__crash = [{arg:0}, {arg:1}]: (crash [!{arg:0}, !{arg:1}])
prim__cast_IntegerInt = [{arg:0}]: (cast-Integer-Int [!{arg:0}])
Main.main = [{ext:0}]: ((Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 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:1123} (Prelude.Types.null [___, !{arg:1123}])))]), (%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))])])]) [(Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:184} (%lam {arg:185} (Prelude.Num.div [!{arg:184}, !{arg:185}]))), (%lam {arg:186} (%lam {arg:187} (Prelude.Num.mod [!{arg:186}, !{arg:187}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))]), (%lam {arg:371} (%lam {arg:372} (Prelude.EqOrd.compare [!{arg:371}, !{arg:372}]))), (%lam {arg:373} (%lam {arg:374} (Prelude.EqOrd.< [!{arg:373}, !{arg:374}]))), (%lam {arg:375} (%lam {arg:376} (Prelude.EqOrd.> [!{arg:375}, !{arg:376}]))), (%lam {arg:377} (%lam {arg:378} (Prelude.EqOrd.<= [!{arg:377}, !{arg:378}]))), (%lam {arg:379} (%lam {arg:380} (Prelude.EqOrd.>= [!{arg:379}, !{arg:380}]))), (%lam {arg:381} (%lam {arg:382} (Prelude.EqOrd.max [!{arg:381}, !{arg:382}]))), (%lam {arg:383} (%lam {arg:384} (Prelude.EqOrd.min [!{arg:383}, !{arg:384}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:56} (Prelude.Num.negate [!{arg:56}])), (%lam {arg:57} (%lam {arg:58} (Prelude.Num.- [!{arg:57}, !{arg:58}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
Prelude.Basics.not = [{arg:0}]: (%case !{arg:0} [(%constcase 0 1), (%constcase 1 0)] Nothing)
Prelude.Basics.intToBool = [{arg:0}]: (%case !{arg:0} [(%constcase 0 1)] Just 0)
Prelude.Basics.True = Constructor tag Just 0 arity 0
Prelude.Basics.False = Constructor tag Just 1 arity 0
Prelude.Basics.Bool = Constructor tag Nothing arity 0
Prelude.Basics.&& = [{arg:0}, {arg:1}]: (%case !{arg:0} [(%constcase 0 (%force Lazy !{arg:1})), (%constcase 1 1)] Nothing)
Builtin.snd = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Builtin.MkPair Just 0 [{e:2}, {e:3}] !{e:3})] Nothing)
Builtin.idris_crash = [{arg:0}, {ext:0}]: (crash [___, !{ext:0}])
Builtin.fst = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Builtin.MkPair Just 0 [{e:2}, {e:3}] !{e:2})] Nothing)
Builtin.believe_me = [{arg:0}, {arg:1}, {ext:0}]: (believe_me [___, ___, !{ext:0}])
Builtin.assert_total = [{arg:0}, {arg:1}]: !{arg:1}
Builtin.MkPair = Constructor tag Just 0 arity 2
Prelude.Types.case block in rangeFromThen = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:5} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:5}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)]))] Nothing))])), (%constcase 1 (Prelude.Types.countFrom [___, !{arg:2}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:2}]) [!{arg:3}]))] Nothing)]))] Nothing))]))] Nothing)
Prelude.Types.case block in case block in case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:2}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.Nil Just 0 []))] Nothing)
Prelude.Types.case block in case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:6} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:3} [!{arg:6}]) [!{arg:2}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:4}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in case block in rangeFromThenTo [___, !{arg:1}, !{arg:4}, !{arg:3}, !{arg:2}, (Prelude.Basics.&& [(%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] ((!{e:1} [!{arg:4}]) [!{arg:3}]))] Nothing), (%delay Lazy (%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] ((!{e:1} [!{arg:3}]) [!{arg:2}]))] Nothing))])]))] Nothing)
Prelude.Types.case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:6} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:6}]) [!{arg:4}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:6} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:6}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromThenTo [___, !{arg:1}, !{arg:4}, !{arg:3}, !{arg:2}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:3} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:2}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing)]))] Nothing)
Prelude.Types.case block in case block in rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:5} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:5} [!{arg:5}]) [!{arg:2}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:3}, (%lam x (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!x]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:3}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
Prelude.Types.case block in rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:5} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:6} [!{arg:5}]) [!{arg:3}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:5} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:5}]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [___, !{arg:1}, !{arg:3}, !{arg:2}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:2}]) [!{arg:3}]))] Nothing)]))] Nothing)
Prelude.Types.case block in takeBefore = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (%con Prelude.Types.Nil Just 0 [])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:1}, (Prelude.Types.takeBefore [___, !{arg:3}, (%force Inf !{arg:2})])]))] Nothing)
Prelude.Types.case block in takeUntil = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:1}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:1}, (Prelude.Types.takeUntil [___, !{arg:3}, (%force Inf !{arg:2})])]))] Nothing)
Prelude.Types.case block in prim__integerToNat = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:0}])), (%constcase 1 0)] Nothing)
Prelude.Types.rangeFrom = [{arg:0}, {arg:1}, {arg:2}]: (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:3} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]) [!{arg:3}]))] Nothing))])
Prelude.Types.rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (Prelude.Types.case block in rangeFromTo [___, !{arg:1}, !{arg:2}, !{arg:3}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)])
Prelude.Types.rangeFromThen = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (Prelude.Types.case block in rangeFromThen [___, !{arg:1}, !{arg:2}, !{arg:3}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)])
Prelude.Types.rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (Prelude.Types.case block in rangeFromThenTo [___, !{arg:1}, !{arg:2}, !{arg:3}, !{arg:4}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:2}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing)])
Prelude.Types.null = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] (%delay Lazy 1))] Nothing)
Prelude.Types.foldr = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%concase Prelude.Types.Nil Just 0 [] !{arg:3}), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] ((!{arg:2} [!{e:2}]) [(Prelude.Types.foldr [___, ___, !{arg:2}, !{arg:3}, !{e:3}])]))] Nothing)
Prelude.Types.foldl = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%concase Prelude.Types.Nil Just 0 [] !{arg:3}), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] (Prelude.Types.foldl [___, ___, !{arg:2}, ((!{arg:2} [!{arg:3}]) [!{e:2}]), !{e:3}]))] Nothing)
Prelude.Types.Range at Prelude/Types.idr:719:1--725:37 = Constructor tag Just 0 arity 4
Prelude.Types.Range implementation at Prelude/Types.idr:751:1--773:48 = [{arg:0}, {arg:1}]: (%con Prelude.Types.Range at Prelude/Types.idr:719:1--725:37 Just 0 [(%lam {arg:4770} (%lam {arg:4771} (Prelude.Types.rangeFromTo [___, !{arg:1}, !{arg:4770}, !{arg:4771}]))), (%lam {arg:4772} (%lam {arg:4773} (%lam {arg:4774} (Prelude.Types.rangeFromThenTo [___, !{arg:1}, !{arg:4772}, !{arg:4773}, !{arg:4774}])))), (%lam {arg:4775} (Prelude.Types.rangeFrom [___, !{arg:1}, !{arg:4775}])), (%lam {arg:4776} (%lam {arg:4777} (Prelude.Types.rangeFromThen [___, !{arg:1}, !{arg:4776}, !{arg:4777}])))])
Prelude.Types.Foldable implementation at Prelude/Types.idr:356:1--365:22 = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 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:1123} (Prelude.Types.null [___, !{arg:1123}])))])
Prelude.Types.takeUntil = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Types.Stream.:: Just 0 [{e:1}, {e:2}] (Prelude.Types.case block in takeUntil [___, !{e:1}, !{e:2}, !{arg:1}, (!{arg:1} [!{e:1}])]))] Nothing)
Prelude.Types.takeBefore = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Types.Stream.:: Just 0 [{e:1}, {e:2}] (Prelude.Types.case block in takeBefore [___, !{e:1}, !{e:2}, !{arg:1}, (!{arg:1} [!{e:1}])]))] Nothing)
Prelude.Types.rangeFromTo = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Types.Range at Prelude/Types.idr:719:1--725:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.Types.prim__integerToNat = [{arg:0}]: (Prelude.Types.case block in prim__integerToNat [!{arg:0}, (%case (<=Integer [0, !{arg:0}]) [(%constcase 0 1)] Just 0)])
Prelude.Types.countFrom = [{arg:0}, {arg:1}, {arg:2}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:1}, (%delay Inf (Prelude.Types.countFrom [___, (!{arg:2} [!{arg:1}]), !{arg:2}]))])
Prelude.Types.Z = Constructor tag Just 0 arity 0
Prelude.Types.Stream.Stream = Constructor tag Nothing arity 1
Prelude.Types.Nil = Constructor tag Just 0 arity 0
Prelude.Types.:: = Constructor tag Just 1 arity 2
Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
Prelude.Num.case block in mod = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 1 (%Int [!{arg:1}, !{arg:0}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:116:3--118:40"]))
Prelude.Num.case block in div = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 1 (/Int [!{arg:1}, !{arg:0}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:113:3--115:40"]))
Prelude.Num.negate = [{arg:0}]: (-Int [0, !{arg:0}])
Prelude.Num.mod = [{arg:0}, {arg:1}]: (Prelude.Num.case block in mod [!{arg:1}, !{arg:0}, (Prelude.EqOrd.== [!{arg:1}, (cast-Integer-Int [0])])])
Prelude.Num.fromInteger = [{ext:0}]: (cast-Integer-Int [!{ext:0}])
Prelude.Num.div = [{arg:0}, {arg:1}]: (Prelude.Num.case block in div [!{arg:1}, !{arg:0}, (Prelude.EqOrd.== [!{arg:1}, (cast-Integer-Int [0])])])
Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 = Constructor tag Just 0 arity 3
Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 = Constructor tag Just 0 arity 3
Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 = Constructor tag Just 0 arity 3
Prelude.Num.Constraint (Num ty) = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing)
Prelude.Num.Num implementation at Prelude/Num.idr:95:1--100:38 = []: (%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))])
Prelude.Num.Neg implementation at Prelude/Num.idr:102:1--105:22 = []: (%con Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:56} (Prelude.Num.negate [!{arg:56}])), (%lam {arg:57} (%lam {arg:58} (Prelude.Num.- [!{arg:57}, !{arg:58}])))])
Prelude.Num.Integral implementation at Prelude/Num.idr:111:1--118:40 = []: (%con Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:184} (%lam {arg:185} (Prelude.Num.div [!{arg:184}, !{arg:185}]))), (%lam {arg:186} (%lam {arg:187} (Prelude.Num.mod [!{arg:186}, !{arg:187}])))])
Prelude.Num.- = [{ext:0}, {ext:1}]: (-Int [!{ext:0}, !{ext:1}])
Prelude.Num.+ = [{ext:0}, {ext:1}]: (+Int [!{ext:0}, !{ext:1}])
Prelude.Num.* = [{ext:0}, {ext:1}]: (*Int [!{ext:0}, !{ext:1}])
Prelude.Num.fromInteger = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (!{e:3} [!{arg:2}])))] Nothing)
Prelude.Num.- = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (%lam {arg:3} ((!{e:3} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.Num.+ = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.EqOrd.case block in case block in compare = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 1), (%constcase 1 2)] Nothing)
Prelude.EqOrd.case block in compare = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 0), (%constcase 1 (Prelude.EqOrd.case block in case block in compare [!{arg:0}, !{arg:1}, (Prelude.EqOrd.== [!{arg:1}, !{arg:0}])]))] Nothing)
Prelude.EqOrd.case block in max = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 !{arg:1}), (%constcase 1 !{arg:0})] Nothing)
Prelude.EqOrd.case block in min = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 !{arg:1}), (%constcase 1 !{arg:0})] Nothing)
Prelude.EqOrd.min = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in min [!{arg:1}, !{arg:0}, (Prelude.EqOrd.< [!{arg:0}, !{arg:1}])])
Prelude.EqOrd.max = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in max [!{arg:1}, !{arg:0}, (Prelude.EqOrd.> [!{arg:0}, !{arg:1}])])
Prelude.EqOrd.compare = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in compare [!{arg:1}, !{arg:0}, (Prelude.EqOrd.< [!{arg:0}, !{arg:1}])])
Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 = Constructor tag Just 0 arity 8
Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 = Constructor tag Just 0 arity 2
Prelude.EqOrd.Constraint (Eq ty) = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing)
Prelude.EqOrd.Ord implementation at Prelude/EqOrd.idr:128:1--135:43 = []: (%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))]), (%lam {arg:371} (%lam {arg:372} (Prelude.EqOrd.compare [!{arg:371}, !{arg:372}]))), (%lam {arg:373} (%lam {arg:374} (Prelude.EqOrd.< [!{arg:373}, !{arg:374}]))), (%lam {arg:375} (%lam {arg:376} (Prelude.EqOrd.> [!{arg:375}, !{arg:376}]))), (%lam {arg:377} (%lam {arg:378} (Prelude.EqOrd.<= [!{arg:377}, !{arg:378}]))), (%lam {arg:379} (%lam {arg:380} (Prelude.EqOrd.>= [!{arg:379}, !{arg:380}]))), (%lam {arg:381} (%lam {arg:382} (Prelude.EqOrd.max [!{arg:381}, !{arg:382}]))), (%lam {arg:383} (%lam {arg:384} (Prelude.EqOrd.min [!{arg:383}, !{arg:384}])))])
Prelude.EqOrd.Eq implementation at Prelude/EqOrd.idr:36:1--38:40 = []: (%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))])
Prelude.EqOrd.> = [{arg:0}, {arg:1}]: (%case (>Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.>= = [{arg:0}, {arg:1}]: (%case (>=Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case (==Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case (<Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd.<= = [{arg:0}, {arg:1}]: (%case (<=Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
Prelude.EqOrd./= = [{arg:0}, {arg:1}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:0}, !{arg:1}])])
Prelude.EqOrd.LT = Constructor tag Just 0 arity 0
Prelude.EqOrd.GT = Constructor tag Just 2 arity 0
Prelude.EqOrd.EQ = Constructor tag Just 1 arity 0
Prelude.EqOrd.>= = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:6} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.EqOrd.> = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:4} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.EqOrd.<= = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:5} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:3} [!{arg:2}]) [!{arg:3}]))))] Nothing)
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:67:1--74:38 = Constructor tag Just 0 arity 2 (newtype by 1)
Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 = Constructor tag Just 0 arity 3
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:140:1--143:35 = Constructor tag Just 0 arity 3
Prelude.Interfaces.sum = [{arg:0}, {arg:1}, {arg:2}]: (%case (Builtin.fst [___, ___, !{arg:2}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:3} (((((!{e:1} [___]) [___]) [(%case (Builtin.snd [___, ___, !{arg:2}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (%lam {arg:4} (%lam {arg:5} ((!{e:6} [!{arg:4}]) [!{arg:5}]))))] Nothing)]) [(%case (Builtin.snd [___, ___, !{arg:2}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [0]))] Nothing)]) [!{arg:3}])))] Nothing)
Prelude.Interfaces.pure = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:140:1--143:35 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:3} ((!{e:2} [___]) [!{arg:3}])))] Nothing)
Prelude.Interfaces.foldr = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (%case !{arg:3} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:4} (%lam {arg:5} (%lam {arg:6} (((((!{e:1} [___]) [___]) [!{arg:4}]) [!{arg:5}]) [!{arg:6}])))))] Nothing)
Prelude.Interfaces.foldl = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (%case !{arg:3} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:219:1--244:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:4} (%lam {arg:5} (%lam {arg:6} (((((!{e:2} [___]) [___]) [!{arg:4}]) [!{arg:5}]) [!{arg:6}])))))] Nothing)
PrimIO.case block in unsafePerformIO = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:3}])
PrimIO.case block in case block in io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}, {arg:6}, {arg:7}]: (!{arg:7} [!{arg:6}])
PrimIO.case block in io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:5}, ___, (!{arg:3} [!{arg:5}])])
PrimIO.unsafePerformIO = [{arg:0}, {arg:1}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:1}, ___, (!{arg:1} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:0}, {arg:1}, {arg:2}]: !{arg:2}
PrimIO.unsafeCreateWorld = [{arg:0}, {arg:1}]: (!{arg:1} [%MkWorld])
PrimIO.io_pure = [{arg:0}, {arg:1}, {ext:0}]: !{arg:1}
PrimIO.io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:3}, ___, (!{arg:2} [!{ext:0}])])
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:0}, {arg:1}, {ext:0}]: !{arg:1}
Prelude.IO.map = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (%let {act:3} (!{arg:3} [!{ext:0}]) (!{arg:2} [!{act:3}]))
Prelude.IO.Functor implementation at Prelude/IO.idr:15:1--17:46 = [{ext:4}, {ext:1}, {ext:2}, {ext:3}, {ext:0}]: (Prelude.IO.map [___, ___, !{ext:2}, !{ext:3}, !{ext:0}])
Prelude.IO.Applicative implementation at Prelude/IO.idr:19:1--26:30 = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:140:1--143:35 Just 0 [(%lam b (%lam a (%lam func (%lam {arg:143} (%lam {eta:0} (Prelude.IO.map [___, ___, !func, !{arg:143}, !{eta:0}])))))), (%lam a (%lam {arg:556} (%lam {eta:0} !{arg:556}))), (%lam b (%lam a (%lam {arg:557} (%lam {arg:559} (%lam {eta:0} (%let {act:17} (!{arg:557} [!{eta:0}]) (%let {act:16} (!{arg:559} [!{eta:0}]) (!{act:17} [!{act:16}]))))))))])
Prelude.IO.<*> = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (%let {act:6} (!{arg:2} [!{ext:0}]) (%let {act:5} (!{arg:3} [!{ext:0}]) (!{act:6} [!{act:5}])))

6
tests/codegen/con001/run Executable file
View File

@ -0,0 +1,6 @@
$1 --no-color --console-width 0 --no-banner --dumpcases Main.cases -o Main Main.idr
$1 --no-color --console-width 0 --no-banner --exec main CatCases.idr
rm -rf build
rm Main.cases