-module('Idris.Idris2.Compiler.Inline').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--compileAndInlineAll,nonErased-6844'/4,
  'case--case block in mergeLamDef-6782'/6,
  'case--mergeLamDef-6770'/4,
  'case--case block in fixArityDef-6709'/6,
  'case--fixArityDef-6697'/4,
  'case--case block in inlineDef-6636'/6,
  'case--inlineDef-6624'/4,
  'case--mergeLam-6590'/4,
  'case--mergeLambdas-6435'/5,
  'case--case block in fixArityTm-5883'/9,
  'case--fixArityTm-5865'/7,
  'case--pickConstAlt-5759'/14,
  'case--case block in pickAlt-5570'/18,
  'case--pickAlt-5529'/18,
  'case--evalAlt-5399'/13,
  'case--extendLoc-5354'/9,
  'case--eval-5202'/13,
  'case--eval-5091'/13,
  'case--eval-4990'/10,
  'case--eval-4752'/13,
  'case--case block in case block in case block in eval-4485'/17,
  'case--case block in case block in eval-4442'/15,
  'case--case block in eval-4412'/13,
  'case--eval-4282'/10,
  'case--tryApply-4159'/10,
  'case--evalLocal-4071'/11,
  'case--usedCon-3927'/9,
  'case--used-3607'/10,
  'case--used-3514'/9,
  'case--largest-3461'/6,
  'case--takeFromStack-3348'/8,
  'nested--9900-6052--in--un--traverseArgs'/9,
  'nested--10957-6826--in--un--nonErased'/3,
  'nested--7858-5492--in--un--matches'/21,
  'nested--9900-6226--in--un--fixArityConstAlt'/8,
  'nested--9900-6168--in--un--fixArityAlt'/8,
  'un--usedConst'/5,
  'un--usedCon'/5,
  'un--used'/5,
  'un--unloadApp'/4,
  'un--unload'/3,
  'un--tryApply'/8,
  'un--takeFromStack'/5,
  'un--refToLocal'/4,
  'un--pickConstAlt'/10,
  'un--pickAlt'/10,
  'un--mkBounds'/1,
  'un--mergeLambdas'/2,
  'un--mergeLamDef'/3,
  'un--mergeLam'/2,
  'un--largest'/4,
  'un--inlineDef'/3,
  'un--inline'/3,
  'un--getNewArgs'/3,
  'un--getLams'/5,
  'un--getArity'/1,
  'un--genName'/3,
  'un--fixArityTm'/4,
  'un--fixArityExp'/3,
  'un--fixArityDef'/3,
  'un--fixArity'/2,
  'un--extendLoc'/6,
  'un--extend'/6,
  'un--evalLocal'/11,
  'un--evalConstAlt'/8,
  'un--evalAlt'/9,
  'un--eval'/8,
  'un--doEval'/5,
  'un--compileAndInlineAll'/2,
  'un--Stack'/1
]).
'case--compileAndInlineAll,nonErased-6844'(V0, V1, V2, V3) -> case V3 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> fun (V5) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--/=_Eq__ZeroOneOmega'(case V4 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26) -> V13 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V27) -> fun (V28) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V27, V28)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V29) -> fun (V30) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V29, V30)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))))} end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V31) -> {'Idris.Prelude.Types.Right', 1} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in mergeLamDef-6782'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> begin (V8 = (('un--mergeLam'(V1, V6))(V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> ('Idris.Idris2.Core.Context':'un--setCompiled'(V1, V0, V10, V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V11) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--mergeLamDef-6770'(V0, V1, V2, V3) -> case V3 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> begin (V5 = {'Idris.Prelude.Types.Just', V4}), ('case--case block in mergeLamDef-6782'(V0, V1, V2, V4, V5, case V4 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26) -> V24 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V27) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in fixArityDef-6709'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> begin (V8 = (('un--fixArity'(V1, V6))(V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> ('Idris.Idris2.Core.Context':'un--setCompiled'(V1, V0, V10, V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V11) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--fixArityDef-6697'(V0, V1, V2, V3) -> case V3 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> begin (V5 = {'Idris.Prelude.Types.Just', V4}), ('case--case block in fixArityDef-6709'(V0, V1, V2, V4, V5, case V4 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26) -> V24 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V27) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in inlineDef-6636'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> begin (V8 = (('un--inline'(V1, V0, V6))(V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> ('Idris.Idris2.Core.Context':'un--setCompiled'(V1, V0, V10, V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V11) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--inlineDef-6624'(V0, V1, V2, V3) -> case V3 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> begin (V5 = {'Idris.Prelude.Types.Just', V4}), ('case--case block in inlineDef-6636'(V0, V1, V2, V4, V5, case V4 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26) -> V24 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V27) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--mergeLam-6590'(V0, V1, V2, V3) -> case V3 of {'Idris.Builtin.DPair.MkDPair', E0, E1} -> (fun (V4, V5) -> fun (V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkFun', V4, V5}} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--mergeLambdas-6435'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Builtin.DPair.MkDPair', E0, E1} -> (fun (V5, V6) -> case V6 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V7, V8) -> begin (V9 = ('Idris.Idris2.Core.CompileExpr':'un--substs'(V5, V1, V7, V8))), begin (V10 = ('Idris.Idris2.Data.List':'un--reverse'('erased', ('un--getNewArgs'('erased', V5, V7))))), begin (V11 = ('Idris.Idris2.Core.CompileExpr':'un--mkLocals'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V1)), ('un--mkBounds'(V10)), V9))), {'Idris.Builtin.DPair.MkDPair', ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V1, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V10, [])))), V11} end end end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in fixArityTm-5883'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Prelude.Types.Just', E0} -> (fun (V9) -> begin (V10 = ('un--getArity'(V9))), fun (V11) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, V10, {'Idris.Core.CompileExpr.CApp', V2, {'Idris.Core.CompileExpr.CRef', V2, V1}, []}, V3))} end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V12) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V3, {'Idris.Core.CompileExpr.CRef', V2, V1}))} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--fixArityTm-5865'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Prelude.Types.Just', E0} -> (fun (V7) -> begin (V8 = {'Idris.Prelude.Types.Just', V7}), ('case--case block in fixArityTm-5883'(V0, V1, V2, V3, V4, V5, V7, V8, case V7 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29) -> V27 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V30) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V3, {'Idris.Core.CompileExpr.CRef', V2, V1}))} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--pickConstAlt-5759'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13) -> case V13 of 0 -> fun (V14) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V15) -> case V15 of {'Idris.Prelude.Types.Left', E0} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V17) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V17}} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('un--eval'(V4, V3, V0, V12, V11, V10, V9, V5)), V14)) end; 1 -> ('un--pickConstAlt'(V4, V3, V0, V12, V11, V10, V9, {'Idris.Core.CompileExpr.CPrimVal', V2, V1}, V7, V8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in pickAlt-5570'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V19) -> begin (V20 = ('un--extend'('erased', 'erased', V13, V1, V5, V19))), fun (V21) -> begin (V22 = (('un--eval'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V5, V6)), V0, V16, V15, V14, V20, V12, V7))(V21))), case V22 of {'Idris.Prelude.Types.Left', E1} -> (fun (V23) -> {'Idris.Prelude.Types.Left', V23} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V24) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V24}} end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--pickAlt-5529'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of 0 -> ('case--case block in pickAlt-5570'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, ('Idris.Idris2.Data.LengthMatch':'un--checkLengthMatch'('erased', 'erased', V1, V5)))); 1 -> ('un--pickAlt'(V6, V0, V16, V15, V14, V13, V12, {'Idris.Core.CompileExpr.CCon', V4, V3, V2, V1}, V10, V11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--evalAlt-5399'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V13, V14) -> fun (V15) -> begin (V16 = (('un--eval'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V0, V2)), V1, V11, V10, V8, V14, V6, V3))(V15))), case V16 of {'Idris.Prelude.Types.Left', E2} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkConAlt', V5, V4, V0, ('Idris.Idris2.Core.CompileExpr':'un--refsToLocals'('erased', 'erased', V13, V18))}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--extendLoc-5354'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V9, V10) -> fun (V11) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', {'Idris.Core.TT.Bounds.Add', V2, V7, V9}, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V5, V7}, V10}}} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--eval-5202'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V13) -> begin (V15 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V14) -> ('un--eval'(V0, V1, V10, V9, V8, V7, V6, V14)) end, V2))(V13))), case V15 of {'Idris.Prelude.Types.Left', E0} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V17) -> begin (V19 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V18) -> ('un--evalConstAlt'(V0, V1, V10, V9, V8, V7, V6, V18)) end, V3))(V13))), case V19 of {'Idris.Prelude.Types.Left', E2} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V21) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConstCase', V5, V11, V21, V17}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.Prelude.Types.Just', E4} -> (fun (V22) -> fun (V23) -> {'Idris.Prelude.Types.Right', V22} end end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--eval-5091'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V13) -> begin (V15 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V14) -> ('un--eval'(V0, V1, V10, V9, V8, V7, V6, V14)) end, V2))(V13))), case V15 of {'Idris.Prelude.Types.Left', E0} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V17) -> begin (V19 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V18) -> ('un--evalAlt'(V0, V1, V10, V9, V5, V8, V7, V6, V18)) end, V3))(V13))), case V19 of {'Idris.Prelude.Types.Left', E2} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V21) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConCase', V5, V11, V21, V17}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.Prelude.Types.Just', E4} -> (fun (V22) -> fun (V23) -> {'Idris.Prelude.Types.Right', V22} end end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--eval-4990'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.CompileExpr.CDelay', E0, E1} -> (fun (V10, V11) -> ('un--eval'([], V1, V8, V7, V6, {'Idris.Compiler.Inline.Nil'}, V4, V11)) end(E0, E1)); _ -> fun (V12) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CForce', V3, V9}))} end end.
'case--eval-4752'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of 0 -> fun (V13) -> begin (V14 = (('un--eval'(V2, V1, V10, V9, V8, V7, [], V4))(V13))), case V14 of {'Idris.Prelude.Types.Left', E0} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V16) -> (('un--eval'([V0 | V2], V1, V10, V9, V8, {'Idris.Compiler.Inline.::', V16, V7}, V6, V3))(V13)) end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 1 -> fun (V17) -> begin (V18 = ('un--genName'(V9, <<"letv"/utf8>>, V17))), case V18 of {'Idris.Prelude.Types.Left', E2} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V20) -> begin (V21 = (('un--eval'([V0 | V2], V1, V10, V9, V8, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V5, V20}, V7}, V6, V3))(V17))), case V21 of {'Idris.Prelude.Types.Left', E4} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V23) -> begin (V24 = (('un--eval'(V2, V1, V10, V9, V8, V7, [], V4))(V17))), case V24 of {'Idris.Prelude.Types.Left', E6} -> (fun (V25) -> {'Idris.Prelude.Types.Left', V25} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V26) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CLet', V5, V0, 0, V26, ('un--refToLocal'('erased', V20, V0, V23))}} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in case block in case block in eval-4485'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16) -> case V16 of 0 -> fun (V17) -> begin (V18 = (('un--tryApply'(V0, V1, V8, V7, [V2 | V6], V4, V5, V14))(V17))), case V18 of {'Idris.Prelude.Types.Left', E0} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V20) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Data.Maybe':'un--fromMaybe'('erased', fun () -> ('un--unloadApp'('erased', V15, V4, {'Idris.Core.CompileExpr.CRef', V3, V2})) end, V20))} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 1 -> fun (V21) -> {'Idris.Prelude.Types.Right', ('un--unloadApp'('erased', V15, V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14) -> case V14 of {'Idris.Prelude.Types.Just', E0} -> (fun (V15) -> begin (V16 = ('un--getArity'(V15))), ('case--case block in case block in case block in eval-4485'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V15, V16, ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V17) -> fun (V18) -> ('Idris.Idris2.Core.Context':'dn--un--==_Eq__DefFlag'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Core.Context':'dn--un--/=_Eq__DefFlag'(V19, V20)) end end}, {'Idris.Core.Context.Inline'}, case V12 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41) -> V32 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)), fun () -> ('Idris.Idris2.Prelude.Basics':'un--not'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V42) -> fun (V43) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V42, V43)) end end, fun (V44) -> fun (V45) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V44, V45)) end end}, V2, V6)))) end)))) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V46) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in eval-4412'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Prelude.Types.Just', E0} -> (fun (V13) -> begin (V14 = {'Idris.Prelude.Types.Just', V13}), ('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V13, V14, case V13 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V33 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V36) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--eval-4282'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V10, V11) -> case V10 of 0 -> case V11 of [E106 | E107] -> (fun (V12, V13) -> case V13 of [E160 | E161] -> (fun (V14, V15) -> case V15 of [E214 | E215] -> (fun (V16, V17) -> case V17 of [E268 | E269] -> (fun (V18, V19) -> case V19 of [E322 | E323] -> (fun (V20, V21) -> fun (V22) -> begin (V23 = ('un--genName'(V7, <<"act"/utf8>>, V22))), case V23 of {'Idris.Prelude.Types.Left', E324} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E324)); {'Idris.Prelude.Types.Right', E325} -> (fun (V25) -> begin (V26 = (('un--eval'([], V1, V8, V7, V6, {'Idris.Compiler.Inline.Nil'}, [], {'Idris.Core.CompileExpr.CApp', V3, V18, [{'Idris.Core.CompileExpr.CRef', V3, V25} | [V20 | []]]}))(V22))), case V26 of {'Idris.Prelude.Types.Left', E326} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E326)); {'Idris.Prelude.Types.Right', E327} -> (fun (V28) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V21, {'Idris.Core.CompileExpr.CLet', V3, V25, 1, {'Idris.Core.CompileExpr.CApp', V3, V16, [V20 | []]}, ('un--refToLocal'('erased', V25, V25, V28))}))} end(E327)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E325)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E322, E323)); _ -> fun (V29) -> begin (V58 = begin (V57 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V32, V33, V34)) end end end end end, fun (V35) -> fun (V36) -> fun (V37) -> V36 end end end, fun (V38) -> fun (V39) -> fun (V40) -> fun (V41) -> fun (V42) -> begin (V43 = (V40(V42))), begin (V44 = (V41(V42))), (V43(V44)) end end end end end end end}, fun (V45) -> fun (V46) -> fun (V47) -> fun (V48) -> fun (V49) -> begin (V50 = (V47(V49))), ((V48(V50))(V49)) end end end end end end, fun (V51) -> fun (V52) -> fun (V53) -> begin (V54 = (V52(V53))), (V54(V53)) end end end end}, fun (V55) -> fun (V56) -> V56 end end}, V8))(V29))), {'Idris.Prelude.Types.Right', V57} end), case V58 of {'Idris.Prelude.Types.Left', E270} -> (fun (V59) -> {'Idris.Prelude.Types.Left', V59} end(E270)); {'Idris.Prelude.Types.Right', E271} -> (fun (V60) -> begin (V87 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V60 of {'Idris.Core.Context.MkDefs', E272, E273, E274, E275, E276, E277, E278, E279, E280, E281, E282, E283, E284, E285, E286, E287, E288, E289, E290, E291, E292, E293, E294, E295, E296, E297} -> (fun (V61, V62, V63, V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85, V86) -> V61 end(E272, E273, E274, E275, E276, E277, E278, E279, E280, E281, E282, E283, E284, E285, E286, E287, E288, E289, E290, E291, E292, E293, E294, E295, E296, E297)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V29))), case V87 of {'Idris.Prelude.Types.Left', E298} -> (fun (V88) -> {'Idris.Prelude.Types.Left', V88} end(E298)); {'Idris.Prelude.Types.Right', E299} -> (fun (V89) -> case V89 of {'Idris.Prelude.Types.Just', E300} -> (fun (V90) -> begin (V91 = {'Idris.Prelude.Types.Just', V90}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V60, V90, V91, case V90 of {'Idris.Core.Context.MkGlobalDef', E301, E302, E303, E304, E305, E306, E307, E308, E309, E310, E311, E312, E313, E314, E315, E316, E317, E318, E319, E320, E321} -> (fun (V92, V93, V94, V95, V96, V97, V98, V99, V100, V101, V102, V103, V104, V105, V106, V107, V108, V109, V110, V111, V112) -> V110 end(E301, E302, E303, E304, E305, E306, E307, E308, E309, E310, E311, E312, E313, E314, E315, E316, E317, E318, E319, E320, E321)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V29)) end end(E300)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E299)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E271)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E268, E269)); _ -> fun (V113) -> begin (V142 = begin (V141 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V114) -> fun (V115) -> fun (V116) -> fun (V117) -> fun (V118) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V116, V117, V118)) end end end end end, fun (V119) -> fun (V120) -> fun (V121) -> V120 end end end, fun (V122) -> fun (V123) -> fun (V124) -> fun (V125) -> fun (V126) -> begin (V127 = (V124(V126))), begin (V128 = (V125(V126))), (V127(V128)) end end end end end end end}, fun (V129) -> fun (V130) -> fun (V131) -> fun (V132) -> fun (V133) -> begin (V134 = (V131(V133))), ((V132(V134))(V133)) end end end end end end, fun (V135) -> fun (V136) -> fun (V137) -> begin (V138 = (V136(V137))), (V138(V137)) end end end end}, fun (V139) -> fun (V140) -> V140 end end}, V8))(V113))), {'Idris.Prelude.Types.Right', V141} end), case V142 of {'Idris.Prelude.Types.Left', E216} -> (fun (V143) -> {'Idris.Prelude.Types.Left', V143} end(E216)); {'Idris.Prelude.Types.Right', E217} -> (fun (V144) -> begin (V171 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V144 of {'Idris.Core.Context.MkDefs', E218, E219, E220, E221, E222, E223, E224, E225, E226, E227, E228, E229, E230, E231, E232, E233, E234, E235, E236, E237, E238, E239, E240, E241, E242, E243} -> (fun (V145, V146, V147, V148, V149, V150, V151, V152, V153, V154, V155, V156, V157, V158, V159, V160, V161, V162, V163, V164, V165, V166, V167, V168, V169, V170) -> V145 end(E218, E219, E220, E221, E222, E223, E224, E225, E226, E227, E228, E229, E230, E231, E232, E233, E234, E235, E236, E237, E238, E239, E240, E241, E242, E243)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V113))), case V171 of {'Idris.Prelude.Types.Left', E244} -> (fun (V172) -> {'Idris.Prelude.Types.Left', V172} end(E244)); {'Idris.Prelude.Types.Right', E245} -> (fun (V173) -> case V173 of {'Idris.Prelude.Types.Just', E246} -> (fun (V174) -> begin (V175 = {'Idris.Prelude.Types.Just', V174}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V144, V174, V175, case V174 of {'Idris.Core.Context.MkGlobalDef', E247, E248, E249, E250, E251, E252, E253, E254, E255, E256, E257, E258, E259, E260, E261, E262, E263, E264, E265, E266, E267} -> (fun (V176, V177, V178, V179, V180, V181, V182, V183, V184, V185, V186, V187, V188, V189, V190, V191, V192, V193, V194, V195, V196) -> V194 end(E247, E248, E249, E250, E251, E252, E253, E254, E255, E256, E257, E258, E259, E260, E261, E262, E263, E264, E265, E266, E267)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V113)) end end(E246)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E245)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E217)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E214, E215)); _ -> fun (V197) -> begin (V226 = begin (V225 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V198) -> fun (V199) -> fun (V200) -> fun (V201) -> fun (V202) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V200, V201, V202)) end end end end end, fun (V203) -> fun (V204) -> fun (V205) -> V204 end end end, fun (V206) -> fun (V207) -> fun (V208) -> fun (V209) -> fun (V210) -> begin (V211 = (V208(V210))), begin (V212 = (V209(V210))), (V211(V212)) end end end end end end end}, fun (V213) -> fun (V214) -> fun (V215) -> fun (V216) -> fun (V217) -> begin (V218 = (V215(V217))), ((V216(V218))(V217)) end end end end end end, fun (V219) -> fun (V220) -> fun (V221) -> begin (V222 = (V220(V221))), (V222(V221)) end end end end}, fun (V223) -> fun (V224) -> V224 end end}, V8))(V197))), {'Idris.Prelude.Types.Right', V225} end), case V226 of {'Idris.Prelude.Types.Left', E162} -> (fun (V227) -> {'Idris.Prelude.Types.Left', V227} end(E162)); {'Idris.Prelude.Types.Right', E163} -> (fun (V228) -> begin (V255 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V228 of {'Idris.Core.Context.MkDefs', E164, E165, E166, E167, E168, E169, E170, E171, E172, E173, E174, E175, E176, E177, E178, E179, E180, E181, E182, E183, E184, E185, E186, E187, E188, E189} -> (fun (V229, V230, V231, V232, V233, V234, V235, V236, V237, V238, V239, V240, V241, V242, V243, V244, V245, V246, V247, V248, V249, V250, V251, V252, V253, V254) -> V229 end(E164, E165, E166, E167, E168, E169, E170, E171, E172, E173, E174, E175, E176, E177, E178, E179, E180, E181, E182, E183, E184, E185, E186, E187, E188, E189)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V197))), case V255 of {'Idris.Prelude.Types.Left', E190} -> (fun (V256) -> {'Idris.Prelude.Types.Left', V256} end(E190)); {'Idris.Prelude.Types.Right', E191} -> (fun (V257) -> case V257 of {'Idris.Prelude.Types.Just', E192} -> (fun (V258) -> begin (V259 = {'Idris.Prelude.Types.Just', V258}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V228, V258, V259, case V258 of {'Idris.Core.Context.MkGlobalDef', E193, E194, E195, E196, E197, E198, E199, E200, E201, E202, E203, E204, E205, E206, E207, E208, E209, E210, E211, E212, E213} -> (fun (V260, V261, V262, V263, V264, V265, V266, V267, V268, V269, V270, V271, V272, V273, V274, V275, V276, V277, V278, V279, V280) -> V278 end(E193, E194, E195, E196, E197, E198, E199, E200, E201, E202, E203, E204, E205, E206, E207, E208, E209, E210, E211, E212, E213)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V197)) end end(E192)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E191)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E163)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E160, E161)); _ -> fun (V281) -> begin (V310 = begin (V309 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V282) -> fun (V283) -> fun (V284) -> fun (V285) -> fun (V286) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V284, V285, V286)) end end end end end, fun (V287) -> fun (V288) -> fun (V289) -> V288 end end end, fun (V290) -> fun (V291) -> fun (V292) -> fun (V293) -> fun (V294) -> begin (V295 = (V292(V294))), begin (V296 = (V293(V294))), (V295(V296)) end end end end end end end}, fun (V297) -> fun (V298) -> fun (V299) -> fun (V300) -> fun (V301) -> begin (V302 = (V299(V301))), ((V300(V302))(V301)) end end end end end end, fun (V303) -> fun (V304) -> fun (V305) -> begin (V306 = (V304(V305))), (V306(V305)) end end end end}, fun (V307) -> fun (V308) -> V308 end end}, V8))(V281))), {'Idris.Prelude.Types.Right', V309} end), case V310 of {'Idris.Prelude.Types.Left', E108} -> (fun (V311) -> {'Idris.Prelude.Types.Left', V311} end(E108)); {'Idris.Prelude.Types.Right', E109} -> (fun (V312) -> begin (V339 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V312 of {'Idris.Core.Context.MkDefs', E110, E111, E112, E113, E114, E115, E116, E117, E118, E119, E120, E121, E122, E123, E124, E125, E126, E127, E128, E129, E130, E131, E132, E133, E134, E135} -> (fun (V313, V314, V315, V316, V317, V318, V319, V320, V321, V322, V323, V324, V325, V326, V327, V328, V329, V330, V331, V332, V333, V334, V335, V336, V337, V338) -> V313 end(E110, E111, E112, E113, E114, E115, E116, E117, E118, E119, E120, E121, E122, E123, E124, E125, E126, E127, E128, E129, E130, E131, E132, E133, E134, E135)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V281))), case V339 of {'Idris.Prelude.Types.Left', E136} -> (fun (V340) -> {'Idris.Prelude.Types.Left', V340} end(E136)); {'Idris.Prelude.Types.Right', E137} -> (fun (V341) -> case V341 of {'Idris.Prelude.Types.Just', E138} -> (fun (V342) -> begin (V343 = {'Idris.Prelude.Types.Just', V342}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V312, V342, V343, case V342 of {'Idris.Core.Context.MkGlobalDef', E139, E140, E141, E142, E143, E144, E145, E146, E147, E148, E149, E150, E151, E152, E153, E154, E155, E156, E157, E158, E159} -> (fun (V344, V345, V346, V347, V348, V349, V350, V351, V352, V353, V354, V355, V356, V357, V358, V359, V360, V361, V362, V363, V364) -> V362 end(E139, E140, E141, E142, E143, E144, E145, E146, E147, E148, E149, E150, E151, E152, E153, E154, E155, E156, E157, E158, E159)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V281)) end end(E138)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E137)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E109)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E106, E107)); _ -> fun (V365) -> begin (V394 = begin (V393 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V366) -> fun (V367) -> fun (V368) -> fun (V369) -> fun (V370) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V368, V369, V370)) end end end end end, fun (V371) -> fun (V372) -> fun (V373) -> V372 end end end, fun (V374) -> fun (V375) -> fun (V376) -> fun (V377) -> fun (V378) -> begin (V379 = (V376(V378))), begin (V380 = (V377(V378))), (V379(V380)) end end end end end end end}, fun (V381) -> fun (V382) -> fun (V383) -> fun (V384) -> fun (V385) -> begin (V386 = (V383(V385))), ((V384(V386))(V385)) end end end end end end, fun (V387) -> fun (V388) -> fun (V389) -> begin (V390 = (V388(V389))), (V390(V389)) end end end end}, fun (V391) -> fun (V392) -> V392 end end}, V8))(V365))), {'Idris.Prelude.Types.Right', V393} end), case V394 of {'Idris.Prelude.Types.Left', E54} -> (fun (V395) -> {'Idris.Prelude.Types.Left', V395} end(E54)); {'Idris.Prelude.Types.Right', E55} -> (fun (V396) -> begin (V423 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V396 of {'Idris.Core.Context.MkDefs', E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81} -> (fun (V397, V398, V399, V400, V401, V402, V403, V404, V405, V406, V407, V408, V409, V410, V411, V412, V413, V414, V415, V416, V417, V418, V419, V420, V421, V422) -> V397 end(E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V365))), case V423 of {'Idris.Prelude.Types.Left', E82} -> (fun (V424) -> {'Idris.Prelude.Types.Left', V424} end(E82)); {'Idris.Prelude.Types.Right', E83} -> (fun (V425) -> case V425 of {'Idris.Prelude.Types.Just', E84} -> (fun (V426) -> begin (V427 = {'Idris.Prelude.Types.Just', V426}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V396, V426, V427, case V426 of {'Idris.Core.Context.MkGlobalDef', E85, E86, E87, E88, E89, E90, E91, E92, E93, E94, E95, E96, E97, E98, E99, E100, E101, E102, E103, E104, E105} -> (fun (V428, V429, V430, V431, V432, V433, V434, V435, V436, V437, V438, V439, V440, V441, V442, V443, V444, V445, V446, V447, V448) -> V446 end(E85, E86, E87, E88, E89, E90, E91, E92, E93, E94, E95, E96, E97, E98, E99, E100, E101, E102, E103, E104, E105)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V365)) end end(E84)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E83)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E55)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end; _ -> fun (V449) -> begin (V478 = begin (V477 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V450) -> fun (V451) -> fun (V452) -> fun (V453) -> fun (V454) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V452, V453, V454)) end end end end end, fun (V455) -> fun (V456) -> fun (V457) -> V456 end end end, fun (V458) -> fun (V459) -> fun (V460) -> fun (V461) -> fun (V462) -> begin (V463 = (V460(V462))), begin (V464 = (V461(V462))), (V463(V464)) end end end end end end end}, fun (V465) -> fun (V466) -> fun (V467) -> fun (V468) -> fun (V469) -> begin (V470 = (V467(V469))), ((V468(V470))(V469)) end end end end end end, fun (V471) -> fun (V472) -> fun (V473) -> begin (V474 = (V472(V473))), (V474(V473)) end end end end}, fun (V475) -> fun (V476) -> V476 end end}, V8))(V449))), {'Idris.Prelude.Types.Right', V477} end), case V478 of {'Idris.Prelude.Types.Left', E2} -> (fun (V479) -> {'Idris.Prelude.Types.Left', V479} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V480) -> begin (V507 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V480 of {'Idris.Core.Context.MkDefs', E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29} -> (fun (V481, V482, V483, V484, V485, V486, V487, V488, V489, V490, V491, V492, V493, V494, V495, V496, V497, V498, V499, V500, V501, V502, V503, V504, V505, V506) -> V481 end(E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V449))), case V507 of {'Idris.Prelude.Types.Left', E30} -> (fun (V508) -> {'Idris.Prelude.Types.Left', V508} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V509) -> case V509 of {'Idris.Prelude.Types.Just', E32} -> (fun (V510) -> begin (V511 = {'Idris.Prelude.Types.Just', V510}), (('case--case block in case block in eval-4442'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V480, V510, V511, case V510 of {'Idris.Core.Context.MkGlobalDef', E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53} -> (fun (V512, V513, V514, V515, V516, V517, V518, V519, V520, V521, V522, V523, V524, V525, V526, V527, V528, V529, V530, V531, V532) -> V530 end(E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V449)) end end(E32)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CRef', V3, V2}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--tryApply-4159'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Prelude.Types.Just', E0} -> (fun (V10) -> case V10 of {'Idris.Builtin.MkPair', E1, E2} -> (fun (V11, V12) -> fun (V13) -> begin (V14 = (('un--eval'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V0, V3)), V2, V8, V7, V6, V11, V12, ('Idris.Idris2.Core.CompileExpr':'un--embed'('erased', 'erased', V1))))(V13))), case V14 of {'Idris.Prelude.Types.Left', E3} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V16) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V16}} end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V17) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--evalLocal-4071'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V6 of [] -> fun (V11) -> {'Idris.Prelude.Types.Right', V4} end; _ -> ('un--eval'(V2, V0, V10, V9, V7, V3, V6, ('Idris.Idris2.Core.CompileExpr':'dn--un--weakenNs_Weaken__CExp'('erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V2)), V4)))) end.
'case--usedCon-3927'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> ('un--used'('erased', ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V5, V1)), V8, 'erased', V6)).
'case--used-3607'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of 0 -> 1000; 1 -> V8; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--used-3514'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of 0 -> 1; 1 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--largest-3461'(V0, V1, V2, V3, V4, V5) -> case V5 of 0 -> ('un--largest'('erased', V1, V2, V3)); 1 -> ('un--largest'('erased', V1, V4, V3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--takeFromStack-3348'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V8, V9) -> ('Idris.Idris2.Prelude.Types':'dn--un--pure_Applicative__Maybe'('erased', {'Idris.Builtin.MkPair', {'Idris.Compiler.Inline.::', V2, V8}, V9})) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9900-6052--in--un--traverseArgs'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Data.Vect.Nil'} -> (fun () -> fun (V9) -> {'Idris.Prelude.Types.Right', {'Idris.Data.Vect.Nil'}} end end()); {'Idris.Data.Vect.::', E0, E1} -> (fun (V10, V11) -> fun (V12) -> begin (V13 = (('un--fixArityTm'(V7, V5, V10, []))(V12))), case V13 of {'Idris.Prelude.Types.Left', E2} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V15) -> begin (V16 = (('nested--9900-6052--in--un--traverseArgs'(V0, V1, V2, V3, V4, V5, 'erased', V7, V11))(V12))), case V16 of {'Idris.Prelude.Types.Left', E4} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Data.Vect.::', V15, V18}} end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--10957-6826--in--un--nonErased'(V0, V1, V2) -> begin (V31 = begin (V30 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V5, V6, V7)) end end end end end, fun (V8) -> fun (V9) -> fun (V10) -> V9 end end end, fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> begin (V16 = (V13(V15))), begin (V17 = (V14(V15))), (V16(V17)) end end end end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> begin (V23 = (V20(V22))), ((V21(V23))(V22)) end end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V25(V26))), (V27(V26)) end end end end}, fun (V28) -> fun (V29) -> V29 end end}, V0))(V2))), {'Idris.Prelude.Types.Right', V30} end), case V31 of {'Idris.Prelude.Types.Left', E0} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V33) -> begin (V60 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V1, case V33 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59) -> V34 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2))), case V60 of {'Idris.Prelude.Types.Left', E28} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V62) -> case V62 of {'Idris.Prelude.Types.Just', E30} -> (fun (V63) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--/=_Eq__ZeroOneOmega'(case V63 of {'Idris.Core.Context.MkGlobalDef', E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51} -> (fun (V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84) -> V71 end(E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V85) -> fun (V86) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V85, V86)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V87) -> fun (V88) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V87, V88)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))))} end(E30)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', 1} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'nested--7858-5492--in--un--matches'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20) -> case V18 of {'Idris.Prelude.Types.Just', E0} -> (fun (V21) -> case V20 of {'Idris.Prelude.Types.Just', E1} -> (fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V21, V22)) end(E1)); _ -> 1 end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> case V20 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V17, V19)) end()); _ -> 1 end end()); _ -> 1 end.
'nested--9900-6226--in--un--fixArityConstAlt'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V8, V9) -> fun (V10) -> begin (V11 = (('un--fixArityTm'(V0, V6, V9, []))(V10))), case V11 of {'Idris.Prelude.Types.Left', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkConstAlt', V8, V13}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9900-6168--in--un--fixArityAlt'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V8, V9, V10, V11) -> fun (V12) -> begin (V13 = (('un--fixArityTm'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V10, V0)), V6, V11, []))(V12))), case V13 of {'Idris.Prelude.Types.Left', E4} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V15) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkConAlt', V8, V9, V10, V15}} end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--usedConst'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V5, V6) -> ('un--used'('erased', V1, V2, 'erased', V6)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--usedCon'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V5, V6, V7, V8) -> ('case--usedCon-3927'('erased', V1, V2, V5, V6, V7, V8, 'erased', ('Idris.Idris2.Core.TT':'dn--un--weakenNs_Weaken__Var'('erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V7)), V2)))) end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--used'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V5, V6) -> ('case--used-3514'('erased', V1, 'erased', V6, V5, 'erased', V2, 'erased', ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V2, V5)))) end(E0, E1)); {'Idris.Core.CompileExpr.CLam', E2, E3, E4} -> (fun (V7, V8, V9) -> ('un--used'('erased', [V8 | V1], (1 + V2), 'erased', V9)) end(E2, E3, E4)); {'Idris.Core.CompileExpr.CLet', E5, E6, E7, E8, E9} -> (fun (V10, V11, V12, V13, V14) -> case V12 of 1 -> begin (V15 = ((('un--used'('erased', V1, V2, 'erased', V13)) + ('un--used'('erased', [V11 | V1], (1 + V2), 'erased', V14))) rem 9223372036854775808)), ('case--used-3607'('erased', V1, V2, V10, V11, V14, V13, 'erased', V15, ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V15, 0)))) end; 0 -> ((('un--used'('erased', V1, V2, 'erased', V13)) + ('un--used'('erased', [V11 | V1], (1 + V2), 'erased', V14))) rem 9223372036854775808); _ -> 0 end end(E5, E6, E7, E8, E9)); {'Idris.Core.CompileExpr.CApp', E10, E11, E12} -> (fun (V16, V17, V18) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', fun (V19) -> fun (V20) -> ((V19 + V20) rem 9223372036854775808) end end, ('un--used'('erased', V1, V2, 'erased', V17)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V21) -> ('un--used'('erased', V1, V2, 'erased', V21)) end, V18)))) end(E10, E11, E12)); {'Idris.Core.CompileExpr.CCon', E13, E14, E15, E16} -> (fun (V22, V23, V24, V25) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', fun (V26) -> fun (V27) -> ((V26 + V27) rem 9223372036854775808) end end, 0, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V28) -> ('un--used'('erased', V1, V2, 'erased', V28)) end, V25)))) end(E13, E14, E15, E16)); {'Idris.Core.CompileExpr.COp', E17, E18, E19, E20} -> (fun (V29, V30, V31, V32) -> ('Idris.Idris2.Data.Vect':'dn--un--foldr_Foldable__(Vect $n)'('erased', 'erased', 'erased', fun (V33) -> fun (V34) -> ((V33 + V34) rem 9223372036854775808) end end, 0, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V35) -> ('un--used'('erased', V1, V2, 'erased', V35)) end, V32)))) end(E17, E18, E19, E20)); {'Idris.Core.CompileExpr.CExtPrim', E21, E22, E23} -> (fun (V36, V37, V38) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', fun (V39) -> fun (V40) -> ((V39 + V40) rem 9223372036854775808) end end, 0, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V41) -> ('un--used'('erased', V1, V2, 'erased', V41)) end, V38)))) end(E21, E22, E23)); {'Idris.Core.CompileExpr.CForce', E24, E25} -> (fun (V42, V43) -> ('un--used'('erased', V1, V2, 'erased', V43)) end(E24, E25)); {'Idris.Core.CompileExpr.CDelay', E26, E27} -> (fun (V44, V45) -> ('un--used'('erased', V1, V2, 'erased', V45)) end(E26, E27)); {'Idris.Core.CompileExpr.CConCase', E28, E29, E30, E31} -> (fun (V46, V47, V48, V49) -> ((('un--used'('erased', V1, V2, 'erased', V47)) + ('un--largest'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V50) -> fun (V51) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V50, V51)) end end, fun (V52) -> fun (V53) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V52, V53)) end end}, fun (V54) -> fun (V55) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V54, V55)) end end, fun (V56) -> fun (V57) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V56, V57)) end end, fun (V58) -> fun (V59) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V58, V59)) end end, fun (V60) -> fun (V61) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<=_Ord__Int'(V60, V61)) end end, fun (V62) -> fun (V63) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->=_Ord__Int'(V62, V63)) end end, fun (V64) -> fun (V65) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--max_Ord__Int'(V64, V65)) end end, fun (V66) -> fun (V67) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--min_Ord__Int'(V66, V67)) end end}, ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> 0 end, fun () -> fun (V68) -> ('un--used'('erased', V1, V2, 'erased', V68)) end end, V49)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V69) -> ('un--usedCon'('erased', V1, V2, 'erased', V69)) end, V48))))) rem 9223372036854775808) end(E28, E29, E30, E31)); {'Idris.Core.CompileExpr.CConstCase', E32, E33, E34, E35} -> (fun (V70, V71, V72, V73) -> ((('un--used'('erased', V1, V2, 'erased', V71)) + ('un--largest'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V74) -> fun (V75) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V74, V75)) end end, fun (V76) -> fun (V77) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V76, V77)) end end}, fun (V78) -> fun (V79) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V78, V79)) end end, fun (V80) -> fun (V81) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V80, V81)) end end, fun (V82) -> fun (V83) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V82, V83)) end end, fun (V84) -> fun (V85) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<=_Ord__Int'(V84, V85)) end end, fun (V86) -> fun (V87) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->=_Ord__Int'(V86, V87)) end end, fun (V88) -> fun (V89) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--max_Ord__Int'(V88, V89)) end end, fun (V90) -> fun (V91) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--min_Ord__Int'(V90, V91)) end end}, ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> 0 end, fun () -> fun (V92) -> ('un--used'('erased', V1, V2, 'erased', V92)) end end, V73)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V93) -> ('un--usedConst'('erased', V1, V2, 'erased', V93)) end, V72))))) rem 9223372036854775808) end(E32, E33, E34, E35)); _ -> 0 end.
'un--unloadApp'(V0, V1, V2, V3) -> ('un--unload'('erased', ('Idris.Idris2.Data.List':'un--drop'('erased', V1, V2)), {'Idris.Core.CompileExpr.CApp', ('Idris.Idris2.Core.CompileExpr':'un--getFC'('erased', V3)), V3, ('Idris.Idris2.Data.List':'un--take'('erased', V1, V2))})).
'un--unload'(V0, V1, V2) -> case V1 of [] -> V2; [E0 | E1] -> (fun (V3, V4) -> ('un--unload'('erased', V4, {'Idris.Core.CompileExpr.CApp', ('Idris.Idris2.Core.CompileExpr':'un--getFC'('erased', V2)), V2, [V3 | []]})) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--tryApply'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V8, V9) -> ('case--tryApply-4159'(V8, V9, V1, V0, V6, V5, V4, V3, V2, ('un--takeFromStack'('erased', 'erased', V6, V5, V8)))) end(E0, E1)); _ -> fun (V10) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end.
'un--takeFromStack'(V0, V1, V2, V3, V4) -> case V3 of [E0 | E1] -> (fun (V5, V6) -> case V4 of [E2 | E3] -> (fun (V7, V8) -> ('Idris.Idris2.Prelude.Types':'dn--un-->>=_Monad__Maybe'('erased', 'erased', ('un--takeFromStack'('erased', 'erased', V2, V6, V8)), fun (V9) -> case V9 of {'Idris.Builtin.MkPair', E4, E5} -> (fun (V10, V11) -> ('Idris.Idris2.Prelude.Types':'dn--un--pure_Applicative__Maybe'('erased', {'Idris.Builtin.MkPair', {'Idris.Compiler.Inline.::', V5, V10}, V11})) end(E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end)) end(E2, E3)); _ -> case V4 of [] -> ('Idris.Idris2.Prelude.Types':'dn--un--pure_Applicative__Maybe'('erased', {'Idris.Builtin.MkPair', V2, V3})); _ -> case V3 of [] -> {'Idris.Prelude.Types.Nothing'}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> case V4 of [] -> ('Idris.Idris2.Prelude.Types':'dn--un--pure_Applicative__Maybe'('erased', {'Idris.Builtin.MkPair', V2, V3})); _ -> case V3 of [] -> {'Idris.Prelude.Types.Nothing'}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end.
'un--refToLocal'(V0, V1, V2, V3) -> ('Idris.Idris2.Core.CompileExpr':'un--refsToLocals'('erased', 'erased', {'Idris.Core.TT.Bounds.Add', V2, V1, {'Idris.Core.TT.Bounds.None'}}, V3)).
'un--pickConstAlt'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V7 of {'Idris.Core.CompileExpr.CPrimVal', E0, E1} -> (fun (V10, V11) -> case V8 of [] -> ('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V12) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V12)) end, V9)); [E2 | E3] -> (fun (V13, V14) -> case V13 of {'Idris.Core.CompileExpr.MkConstAlt', E4, E5} -> (fun (V15, V16) -> ('case--pickConstAlt-5759'(V2, V11, V10, V1, V0, V16, V15, V14, V9, V6, V5, V4, V3, ('Idris.Idris2.Core.TT':'dn--un--==_Eq__Constant'(V11, V15)))) end(E4, E5)); _ -> fun (V17) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end end(E2, E3)); _ -> fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end end(E0, E1)); _ -> fun (V19) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end.
'un--pickAlt'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V7 of {'Idris.Core.CompileExpr.CCon', E0, E1, E2, E3} -> (fun (V10, V11, V12, V13) -> case V8 of [] -> ('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V14) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V14)) end, V9)); [E4 | E5] -> (fun (V15, V16) -> case V15 of {'Idris.Core.CompileExpr.MkConAlt', E6, E7, E8, E9} -> (fun (V17, V18, V19, V20) -> ('case--pickAlt-5529'(V1, V13, V12, V11, V10, V19, V0, V20, V18, V17, V16, V9, V6, V5, V4, V3, V2, ('nested--7858-5492--in--un--matches'(V1, V13, V12, V11, V10, V19, V0, V20, V18, V17, V16, V9, V6, V5, V4, V3, V2, V11, V12, V17, V18)))) end(E6, E7, E8, E9)); _ -> fun (V21) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end end(E4, E5)); _ -> fun (V22) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end end(E0, E1, E2, E3)); _ -> fun (V23) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end.
'un--mkBounds'(V0) -> case V0 of [] -> {'Idris.Core.TT.Bounds.None'}; [E0 | E1] -> (fun (V1, V2) -> {'Idris.Core.TT.Bounds.Add', V1, V1, ('un--mkBounds'(V2))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--mergeLambdas'(V0, V1) -> case V1 of {'Idris.Core.CompileExpr.CLam', E0, E1, E2} -> (fun (V2, V3, V4) -> ('case--mergeLambdas-6435'(V3, V0, V4, V2, ('un--getLams'('erased', [], 0, {'Idris.Core.CompileExpr.SubstCEnv.Nil'}, {'Idris.Core.CompileExpr.CLam', V2, V3, V4})))) end(E0, E1, E2)); _ -> {'Idris.Builtin.DPair.MkDPair', V0, V1} end.
'un--mergeLamDef'(V0, V1, V2) -> begin (V31 = begin (V30 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V5, V6, V7)) end end end end end, fun (V8) -> fun (V9) -> fun (V10) -> V9 end end end, fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> begin (V16 = (V13(V15))), begin (V17 = (V14(V15))), (V16(V17)) end end end end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> begin (V23 = (V20(V22))), ((V21(V23))(V22)) end end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V25(V26))), (V27(V26)) end end end end}, fun (V28) -> fun (V29) -> V29 end end}, V0))(V2))), {'Idris.Prelude.Types.Right', V30} end), case V31 of {'Idris.Prelude.Types.Left', E0} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V33) -> begin (V60 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V1, case V33 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59) -> V34 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2))), case V60 of {'Idris.Prelude.Types.Left', E28} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V62) -> case V62 of {'Idris.Prelude.Types.Just', E30} -> (fun (V63) -> begin (V64 = {'Idris.Prelude.Types.Just', V63}), (('case--case block in mergeLamDef-6782'(V1, V0, V33, V63, V64, case V63 of {'Idris.Core.Context.MkGlobalDef', E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51} -> (fun (V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85) -> V83 end(E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2)) end end(E30)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--mergeLam'(V0, V1) -> case V1 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V2, V3) -> ('case--mergeLam-6590'(V2, V3, V0, ('un--mergeLambdas'(V2, V3)))) end(E0, E1)); _ -> fun (V4) -> {'Idris.Prelude.Types.Right', V1} end end.
'un--largest'(V0, V1, V2, V3) -> case V3 of [] -> V2; [E0 | E1] -> (fun (V4, V5) -> ('case--largest-3461'('erased', V1, V4, V5, V2, case V1 of {'Idris.Prelude.EqOrd.dn--un--__mkOrd', E2, E3, E4, E5, E6, E7, E8, E9} -> (fun (V6, V7, V8, V9, V10, V11, V12, V13) -> ((V9(V4))(V2)) end(E2, E3, E4, E5, E6, E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--inlineDef'(V0, V1, V2) -> begin (V31 = begin (V30 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V5, V6, V7)) end end end end end, fun (V8) -> fun (V9) -> fun (V10) -> V9 end end end, fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> begin (V16 = (V13(V15))), begin (V17 = (V14(V15))), (V16(V17)) end end end end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> begin (V23 = (V20(V22))), ((V21(V23))(V22)) end end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V25(V26))), (V27(V26)) end end end end}, fun (V28) -> fun (V29) -> V29 end end}, V0))(V2))), {'Idris.Prelude.Types.Right', V30} end), case V31 of {'Idris.Prelude.Types.Left', E0} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V33) -> begin (V60 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V1, case V33 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59) -> V34 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2))), case V60 of {'Idris.Prelude.Types.Left', E28} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V62) -> case V62 of {'Idris.Prelude.Types.Just', E30} -> (fun (V63) -> begin (V64 = {'Idris.Prelude.Types.Just', V63}), (('case--case block in inlineDef-6636'(V1, V0, V33, V63, V64, case V63 of {'Idris.Core.Context.MkGlobalDef', E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51} -> (fun (V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85) -> V83 end(E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2)) end end(E30)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--inline'(V0, V1, V2) -> case V2 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V3, V4) -> fun (V5) -> begin (V6 = ('un--doEval'(V3, V0, V1, V4, V5))), case V6 of {'Idris.Prelude.Types.Left', E2} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V8) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkFun', V3, V8}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> fun (V9) -> {'Idris.Prelude.Types.Right', V2} end end.
'un--getNewArgs'(V0, V1, V2) -> case V1 of [] -> case V2 of {'Idris.Core.CompileExpr.SubstCEnv.Nil'} -> (fun () -> [] end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; [E0 | E1] -> (fun (V3, V4) -> case V2 of {'Idris.Core.CompileExpr.SubstCEnv.::', E2, E3} -> (fun (V5, V6) -> case V5 of {'Idris.Core.CompileExpr.CRef', E4, E5} -> (fun (V7, V8) -> [V8 | ('un--getNewArgs'('erased', V4, V6))] end(E4, E5)); _ -> [V3 | ('un--getNewArgs'('erased', V4, V6))] end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getLams'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.CLam', E0, E1, E2} -> (fun (V5, V6, V7) -> ('un--getLams'('erased', [V6 | V1], ((V2 + 1) rem 9223372036854775808), {'Idris.Core.CompileExpr.SubstCEnv.::', {'Idris.Core.CompileExpr.CRef', V5, {'Idris.Core.Name.MN', <<"ext"/utf8>>, V2}}, V3}, V7)) end(E0, E1, E2)); _ -> {'Idris.Builtin.DPair.MkDPair', V1, {'Idris.Builtin.MkPair', V3, V4}} end.
'un--getArity'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V1)) end(E0, E1)); {'Idris.Core.CompileExpr.MkCon', E2, E3, E4} -> (fun (V3, V4, V5) -> V4 end(E2, E3, E4)); {'Idris.Core.CompileExpr.MkForeign', E5, E6, E7} -> (fun (V6, V7, V8) -> ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V7)) end(E5, E6, E7)); {'Idris.Core.CompileExpr.MkError', E8} -> (fun (V9) -> 0 end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--genName'(V0, V1, V2) -> begin (V31 = begin (V30 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V5, V6, V7)) end end end end end, fun (V8) -> fun (V9) -> fun (V10) -> V9 end end end, fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> begin (V16 = (V13(V15))), begin (V17 = (V14(V15))), (V16(V17)) end end end end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> begin (V23 = (V20(V22))), ((V21(V23))(V22)) end end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V25(V26))), (V27(V26)) end end end end}, fun (V28) -> fun (V29) -> V29 end end}, V0))(V2))), {'Idris.Prelude.Types.Right', V30} end), case V31 of {'Idris.Prelude.Types.Left', E0} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V33) -> begin (V62 = begin (V61 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V34) -> fun (V35) -> fun (V36) -> fun (V37) -> fun (V38) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V36, V37, V38)) end end end end end, fun (V39) -> fun (V40) -> fun (V41) -> V40 end end end, fun (V42) -> fun (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> begin (V47 = (V44(V46))), begin (V48 = (V45(V46))), (V47(V48)) end end end end end end end}, fun (V49) -> fun (V50) -> fun (V51) -> fun (V52) -> fun (V53) -> begin (V54 = (V51(V53))), ((V52(V54))(V53)) end end end end end end, fun (V55) -> fun (V56) -> fun (V57) -> begin (V58 = (V56(V57))), (V58(V57)) end end end end}, fun (V59) -> fun (V60) -> V60 end end}, V0, ((V33 + 1) rem 9223372036854775808)))(V2))), {'Idris.Prelude.Types.Right', V61} end), case V62 of {'Idris.Prelude.Types.Left', E2} -> (fun (V63) -> {'Idris.Prelude.Types.Left', V63} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V64) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Name.MN', V1, V33}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--fixArityTm'(V0, V1, V2, V3) -> case V2 of {'Idris.Core.CompileExpr.CRef', E0, E1} -> (fun (V4, V5) -> fun (V6) -> begin (V35 = begin (V34 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V7) -> fun (V8) -> fun (V9) -> fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V9, V10, V11)) end end end end end, fun (V12) -> fun (V13) -> fun (V14) -> V13 end end end, fun (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> begin (V20 = (V17(V19))), begin (V21 = (V18(V19))), (V20(V21)) end end end end end end end}, fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V24(V26))), ((V25(V27))(V26)) end end end end end end, fun (V28) -> fun (V29) -> fun (V30) -> begin (V31 = (V29(V30))), (V31(V30)) end end end end}, fun (V32) -> fun (V33) -> V33 end end}, V1))(V6))), {'Idris.Prelude.Types.Right', V34} end), case V35 of {'Idris.Prelude.Types.Left', E2} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V37) -> begin (V64 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V5, case V37 of {'Idris.Core.Context.MkDefs', E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29} -> (fun (V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63) -> V38 end(E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V6))), case V64 of {'Idris.Prelude.Types.Left', E30} -> (fun (V65) -> {'Idris.Prelude.Types.Left', V65} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V66) -> case V66 of {'Idris.Prelude.Types.Just', E32} -> (fun (V67) -> begin (V68 = {'Idris.Prelude.Types.Just', V67}), (('case--case block in fixArityTm-5883'(V0, V5, V4, V3, V1, V37, V67, V68, case V67 of {'Idris.Core.Context.MkGlobalDef', E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53} -> (fun (V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85, V86, V87, V88, V89) -> V87 end(E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V6)) end end(E32)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V3, {'Idris.Core.CompileExpr.CRef', V4, V5}))} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); {'Idris.Core.CompileExpr.CLam', E54, E55, E56} -> (fun (V90, V91, V92) -> fun (V93) -> begin (V94 = (('un--fixArityTm'([V91 | V0], V1, V92, []))(V93))), case V94 of {'Idris.Prelude.Types.Left', E57} -> (fun (V95) -> {'Idris.Prelude.Types.Left', V95} end(E57)); {'Idris.Prelude.Types.Right', E58} -> (fun (V96) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CLam', V90, V91, V96}, V3))} end(E58)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E54, E55, E56)); {'Idris.Core.CompileExpr.CLet', E59, E60, E61, E62, E63} -> (fun (V97, V98, V99, V100, V101) -> fun (V102) -> begin (V103 = (('un--fixArityTm'(V0, V1, V100, []))(V102))), case V103 of {'Idris.Prelude.Types.Left', E64} -> (fun (V104) -> {'Idris.Prelude.Types.Left', V104} end(E64)); {'Idris.Prelude.Types.Right', E65} -> (fun (V105) -> begin (V106 = (('un--fixArityTm'([V98 | V0], V1, V101, []))(V102))), case V106 of {'Idris.Prelude.Types.Left', E66} -> (fun (V107) -> {'Idris.Prelude.Types.Left', V107} end(E66)); {'Idris.Prelude.Types.Right', E67} -> (fun (V108) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CLet', V97, V98, V99, V105, V108}, V3))} end(E67)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E65)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E59, E60, E61, E62, E63)); {'Idris.Core.CompileExpr.CApp', E68, E69, E70} -> (fun (V109, V110, V111) -> fun (V112) -> begin (V114 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V113) -> ('un--fixArityTm'(V0, V1, V113, [])) end, V111))(V112))), case V114 of {'Idris.Prelude.Types.Left', E71} -> (fun (V115) -> {'Idris.Prelude.Types.Left', V115} end(E71)); {'Idris.Prelude.Types.Right', E72} -> (fun (V116) -> (('un--fixArityTm'(V0, V1, V110, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V116, V3))))(V112)) end(E72)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E68, E69, E70)); {'Idris.Core.CompileExpr.CCon', E73, E74, E75, E76} -> (fun (V117, V118, V119, V120) -> case V3 of [] -> fun (V121) -> begin (V123 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V122) -> ('un--fixArityTm'(V0, V1, V122, [])) end, V120))(V121))), case V123 of {'Idris.Prelude.Types.Left', E77} -> (fun (V124) -> {'Idris.Prelude.Types.Left', V124} end(E77)); {'Idris.Prelude.Types.Right', E78} -> (fun (V125) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CCon', V117, V118, V119, V125}} end(E78)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> case V3 of [] -> fun (V126) -> {'Idris.Prelude.Types.Right', V2} end; _ -> fun (V127) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, V2, V3))} end end end end(E73, E74, E75, E76)); {'Idris.Core.CompileExpr.COp', E79, E80, E81, E82} -> (fun (V128, V129, V130, V131) -> case V3 of [] -> fun (V132) -> begin (V133 = (('nested--9900-6052--in--un--traverseArgs'(V0, V128, V131, V130, V129, V1, 'erased', V0, V131))(V132))), case V133 of {'Idris.Prelude.Types.Left', E83} -> (fun (V134) -> {'Idris.Prelude.Types.Left', V134} end(E83)); {'Idris.Prelude.Types.Right', E84} -> (fun (V135) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.COp', V128, V129, V130, V135}} end(E84)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> case V3 of [] -> fun (V136) -> {'Idris.Prelude.Types.Right', V2} end; _ -> fun (V137) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, V2, V3))} end end end end(E79, E80, E81, E82)); {'Idris.Core.CompileExpr.CExtPrim', E85, E86, E87} -> (fun (V138, V139, V140) -> case V3 of [] -> fun (V141) -> begin (V143 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V142) -> ('un--fixArityTm'(V0, V1, V142, [])) end, V140))(V141))), case V143 of {'Idris.Prelude.Types.Left', E88} -> (fun (V144) -> {'Idris.Prelude.Types.Left', V144} end(E88)); {'Idris.Prelude.Types.Right', E89} -> (fun (V145) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CExtPrim', V138, V139, V145}} end(E89)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> case V3 of [] -> fun (V146) -> {'Idris.Prelude.Types.Right', V2} end; _ -> fun (V147) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, V2, V3))} end end end end(E85, E86, E87)); {'Idris.Core.CompileExpr.CForce', E90, E91} -> (fun (V148, V149) -> fun (V150) -> begin (V151 = (('un--fixArityTm'(V0, V1, V149, []))(V150))), case V151 of {'Idris.Prelude.Types.Left', E92} -> (fun (V152) -> {'Idris.Prelude.Types.Left', V152} end(E92)); {'Idris.Prelude.Types.Right', E93} -> (fun (V153) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CForce', V148, V153}, V3))} end(E93)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E90, E91)); {'Idris.Core.CompileExpr.CDelay', E94, E95} -> (fun (V154, V155) -> fun (V156) -> begin (V157 = (('un--fixArityTm'(V0, V1, V155, []))(V156))), case V157 of {'Idris.Prelude.Types.Left', E96} -> (fun (V158) -> {'Idris.Prelude.Types.Left', V158} end(E96)); {'Idris.Prelude.Types.Right', E97} -> (fun (V159) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CDelay', V154, V159}, V3))} end(E97)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E94, E95)); {'Idris.Core.CompileExpr.CConCase', E98, E99, E100, E101} -> (fun (V160, V161, V162, V163) -> fun (V164) -> begin (V165 = (('un--fixArityTm'(V0, V1, V161, []))(V164))), case V165 of {'Idris.Prelude.Types.Left', E102} -> (fun (V166) -> {'Idris.Prelude.Types.Left', V166} end(E102)); {'Idris.Prelude.Types.Right', E103} -> (fun (V167) -> begin (V169 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V168) -> ('nested--9900-6168--in--un--fixArityAlt'(V0, V163, V162, V161, V160, V3, V1, V168)) end, V162))(V164))), case V169 of {'Idris.Prelude.Types.Left', E104} -> (fun (V170) -> {'Idris.Prelude.Types.Left', V170} end(E104)); {'Idris.Prelude.Types.Right', E105} -> (fun (V171) -> begin (V173 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V172) -> ('un--fixArityTm'(V0, V1, V172, [])) end, V163))(V164))), case V173 of {'Idris.Prelude.Types.Left', E106} -> (fun (V174) -> {'Idris.Prelude.Types.Left', V174} end(E106)); {'Idris.Prelude.Types.Right', E107} -> (fun (V175) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CConCase', V160, V167, V171, V175}, V3))} end(E107)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E105)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E103)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E98, E99, E100, E101)); {'Idris.Core.CompileExpr.CConstCase', E108, E109, E110, E111} -> (fun (V176, V177, V178, V179) -> fun (V180) -> begin (V181 = (('un--fixArityTm'(V0, V1, V177, []))(V180))), case V181 of {'Idris.Prelude.Types.Left', E112} -> (fun (V182) -> {'Idris.Prelude.Types.Left', V182} end(E112)); {'Idris.Prelude.Types.Right', E113} -> (fun (V183) -> begin (V185 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V184) -> ('nested--9900-6226--in--un--fixArityConstAlt'(V0, V179, V178, V177, V176, V3, V1, V184)) end, V178))(V180))), case V185 of {'Idris.Prelude.Types.Left', E114} -> (fun (V186) -> {'Idris.Prelude.Types.Left', V186} end(E114)); {'Idris.Prelude.Types.Right', E115} -> (fun (V187) -> begin (V189 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V188) -> ('un--fixArityTm'(V0, V1, V188, [])) end, V179))(V180))), case V189 of {'Idris.Prelude.Types.Left', E116} -> (fun (V190) -> {'Idris.Prelude.Types.Left', V190} end(E116)); {'Idris.Prelude.Types.Right', E117} -> (fun (V191) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, {'Idris.Core.CompileExpr.CConstCase', V176, V183, V187, V191}, V3))} end(E117)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E115)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E113)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E108, E109, E110, E111)); _ -> case V3 of [] -> fun (V192) -> {'Idris.Prelude.Types.Right', V2} end; _ -> fun (V193) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Compiler.CompileExpr':'un--expandToArity'(V0, 0, V2, V3))} end end end.
'un--fixArityExp'(V0, V1, V2) -> ('un--fixArityTm'(V0, V1, V2, [])).
'un--fixArityDef'(V0, V1, V2) -> begin (V31 = begin (V30 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V5, V6, V7)) end end end end end, fun (V8) -> fun (V9) -> fun (V10) -> V9 end end end, fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> begin (V16 = (V13(V15))), begin (V17 = (V14(V15))), (V16(V17)) end end end end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> begin (V23 = (V20(V22))), ((V21(V23))(V22)) end end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V25(V26))), (V27(V26)) end end end end}, fun (V28) -> fun (V29) -> V29 end end}, V0))(V2))), {'Idris.Prelude.Types.Right', V30} end), case V31 of {'Idris.Prelude.Types.Left', E0} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V33) -> begin (V60 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V1, case V33 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59) -> V34 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2))), case V60 of {'Idris.Prelude.Types.Left', E28} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V62) -> case V62 of {'Idris.Prelude.Types.Just', E30} -> (fun (V63) -> begin (V64 = {'Idris.Prelude.Types.Just', V63}), (('case--case block in fixArityDef-6709'(V1, V0, V33, V63, V64, case V63 of {'Idris.Core.Context.MkGlobalDef', E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51} -> (fun (V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85) -> V83 end(E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V2)) end end(E30)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--fixArity'(V0, V1) -> case V1 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V2, V3) -> fun (V4) -> begin (V5 = (('un--fixArityTm'(V2, V0, V3, []))(V4))), case V5 of {'Idris.Prelude.Types.Left', E2} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V7) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkFun', V2, V7}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); {'Idris.Core.CompileExpr.MkError', E4} -> (fun (V8) -> fun (V9) -> begin (V10 = (('un--fixArityTm'([], V0, V8, []))(V9))), case V10 of {'Idris.Prelude.Types.Left', E5} -> (fun (V11) -> {'Idris.Prelude.Types.Left', V11} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V12) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkError', V12}} end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4)); _ -> fun (V13) -> {'Idris.Prelude.Types.Right', V1} end end.
'un--extendLoc'(V0, V1, V2, V3, V4, V5) -> case V5 of [] -> fun (V6) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', {'Idris.Core.TT.Bounds.None'}, V4}} end; [E0 | E1] -> (fun (V7, V8) -> fun (V9) -> begin (V10 = ('un--genName'(V2, <<"cv"/utf8>>, V9))), case V10 of {'Idris.Prelude.Types.Left', E2} -> (fun (V11) -> {'Idris.Prelude.Types.Left', V11} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V12) -> begin (V13 = (('un--extendLoc'('erased', 'erased', V2, V3, V4, V8))(V9))), case V13 of {'Idris.Prelude.Types.Left', E4} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V15) -> case V15 of {'Idris.Builtin.MkPair', E6, E7} -> (fun (V16, V17) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', {'Idris.Core.TT.Bounds.Add', V7, V12, V16}, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V3, V12}, V17}}} end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--extend'(V0, V1, V2, V3, V4, V5) -> case V3 of [] -> case V4 of [] -> case V5 of {'Idris.Data.LengthMatch.NilMatch'} -> (fun () -> V2 end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end; [E0 | E1] -> (fun (V6, V7) -> case V4 of [E2 | E3] -> (fun (V8, V9) -> case V5 of {'Idris.Data.LengthMatch.ConsMatch', E4} -> (fun (V10) -> {'Idris.Compiler.Inline.::', V6, ('un--extend'('erased', 'erased', V2, V7, V9, V10))} end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--evalLocal'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V1 of [] -> fun (V11) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V7, {'Idris.Core.CompileExpr.CLocal', V9, V5}))} end; [E0 | E1] -> (fun (V12, V13) -> case V8 of {'Idris.Compiler.Inline.::', E2, E3} -> (fun (V14, V15) -> case V9 of 0 -> case V7 of [] -> fun (V16) -> {'Idris.Prelude.Types.Right', V14} end; _ -> ('un--eval'(V13, V2, V3, V4, V6, V15, V7, ('Idris.Idris2.Core.CompileExpr':'dn--un--weakenNs_Weaken__CExp'('erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V13)), V14)))) end; _ -> begin (V17 = (V9 - 1)), ('un--evalLocal'('erased', V13, V2, V3, V4, V5, V6, V7, V15, V17, 'erased')) end end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--evalConstAlt'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V8, V9) -> fun (V10) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V11) -> case V11 of {'Idris.Prelude.Types.Left', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkConstAlt', V8, V13}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V9)), V10)) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--evalAlt'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V9, V10, V11, V12) -> fun (V13) -> begin (V14 = (('un--extendLoc'('erased', 'erased', V3, V4, V6, V11))(V13))), case V14 of {'Idris.Prelude.Types.Left', E4} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V16) -> case V16 of {'Idris.Builtin.MkPair', E6, E7} -> (fun (V17, V18) -> begin (V19 = (('un--eval'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V11, V0)), V1, V2, V3, V5, V18, V7, V12))(V13))), case V19 of {'Idris.Prelude.Types.Left', E8} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V21) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.MkConAlt', V9, V10, V11, ('Idris.Idris2.Core.CompileExpr':'un--refsToLocals'('erased', 'erased', V17, V21))}} end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--eval'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.CompileExpr.CLocal', E234, E235} -> (fun (V8, V9) -> ('un--evalLocal'('erased', V0, V1, V2, V3, V9, V4, V6, V5, V8, 'erased')) end(E234, E235)); {'Idris.Core.CompileExpr.CRef', E236, E237} -> (fun (V10, V11) -> ('case--eval-4282'(V0, V1, V11, V10, V6, V5, V4, V3, V2, {'Idris.Builtin.MkPair', ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V11, {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--primIONS'()), {'Idris.Core.Name.UN', <<"io_bind"/utf8>>}})), V6})) end(E236, E237)); _ -> case V6 of [] -> case V7 of {'Idris.Core.CompileExpr.CLam', E148, E149, E150} -> (fun (V12, V13, V14) -> fun (V15) -> begin (V16 = ('un--genName'(V3, <<"lamv"/utf8>>, V15))), case V16 of {'Idris.Prelude.Types.Left', E151} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E151)); {'Idris.Prelude.Types.Right', E152} -> (fun (V18) -> begin (V19 = (('un--eval'([V13 | V0], V1, V2, V3, V4, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V12, V18}, V5}, [], V14))(V15))), case V19 of {'Idris.Prelude.Types.Left', E153} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E153)); {'Idris.Prelude.Types.Right', E154} -> (fun (V21) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CLam', V12, V13, ('un--refToLocal'('erased', V18, V13, V21))}} end(E154)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E152)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E148, E149, E150)); _ -> case V7 of {'Idris.Core.CompileExpr.CLet', E74, E75, E76, E77, E78} -> (fun (V22, V23, V24, V25, V26) -> case V24 of 1 -> fun (V27) -> begin (V28 = ('un--genName'(V3, <<"letv"/utf8>>, V27))), case V28 of {'Idris.Prelude.Types.Left', E79} -> (fun (V29) -> {'Idris.Prelude.Types.Left', V29} end(E79)); {'Idris.Prelude.Types.Right', E80} -> (fun (V30) -> begin (V31 = (('un--eval'([V23 | V0], V1, V2, V3, V4, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V22, V30}, V5}, [], V26))(V27))), case V31 of {'Idris.Prelude.Types.Left', E81} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E81)); {'Idris.Prelude.Types.Right', E82} -> (fun (V33) -> begin (V34 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V25))(V27))), case V34 of {'Idris.Prelude.Types.Left', E83} -> (fun (V35) -> {'Idris.Prelude.Types.Left', V35} end(E83)); {'Idris.Prelude.Types.Right', E84} -> (fun (V36) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CLet', V22, V23, 1, V36, ('un--refToLocal'('erased', V30, V23, V33))}))} end(E84)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E82)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E80)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 0 -> begin (V37 = ('un--used'('erased', [V23 | ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V0, V1))], 0, 'erased', V26))), ('case--eval-4752'(V23, V1, V0, V26, V25, V22, V6, V5, V4, V3, V2, V37, ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V37, 1)))) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E74, E75, E76, E77, E78)); {'Idris.Core.CompileExpr.CApp', E85, E86, E87} -> (fun (V38, V39, V40) -> fun (V41) -> begin (V43 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V42) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V42)) end, V40))(V41))), case V43 of {'Idris.Prelude.Types.Left', E88} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E88)); {'Idris.Prelude.Types.Right', E89} -> (fun (V45) -> (('un--eval'(V0, V1, V2, V3, V4, V5, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V45, V6)), V39))(V41)) end(E89)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E85, E86, E87)); {'Idris.Core.CompileExpr.CCon', E90, E91, E92, E93} -> (fun (V46, V47, V48, V49) -> fun (V50) -> begin (V52 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V51) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V51)) end, V49))(V50))), case V52 of {'Idris.Prelude.Types.Left', E94} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E94)); {'Idris.Prelude.Types.Right', E95} -> (fun (V54) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCon', V46, V47, V48, V54}))} end(E95)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E90, E91, E92, E93)); {'Idris.Core.CompileExpr.COp', E96, E97, E98, E99} -> (fun (V55, V56, V57, V58) -> fun (V59) -> begin (V61 = (('Idris.Idris2.Core.Core':'un--traverseVect'('erased', 'erased', 'erased', fun (V60) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V60)) end, V58))(V59))), case V61 of {'Idris.Prelude.Types.Left', E100} -> (fun (V62) -> {'Idris.Prelude.Types.Left', V62} end(E100)); {'Idris.Prelude.Types.Right', E101} -> (fun (V63) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.COp', V55, V56, V57, V63}))} end(E101)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E96, E97, E98, E99)); {'Idris.Core.CompileExpr.CExtPrim', E102, E103, E104} -> (fun (V64, V65, V66) -> fun (V67) -> begin (V69 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V68) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V68)) end, V66))(V67))), case V69 of {'Idris.Prelude.Types.Left', E105} -> (fun (V70) -> {'Idris.Prelude.Types.Left', V70} end(E105)); {'Idris.Prelude.Types.Right', E106} -> (fun (V71) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CExtPrim', V64, V65, V71}))} end(E106)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E102, E103, E104)); {'Idris.Core.CompileExpr.CForce', E107, E108} -> (fun (V72, V73) -> fun (V74) -> begin (V75 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V73))(V74))), case V75 of {'Idris.Prelude.Types.Left', E109} -> (fun (V76) -> {'Idris.Prelude.Types.Left', V76} end(E109)); {'Idris.Prelude.Types.Right', E110} -> (fun (V77) -> case V77 of {'Idris.Core.CompileExpr.CDelay', E111, E112} -> (fun (V78, V79) -> (('un--eval'([], V1, V2, V3, V4, {'Idris.Compiler.Inline.Nil'}, V6, V79))(V74)) end(E111, E112)); _ -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CForce', V72, V77}))} end end(E110)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E107, E108)); {'Idris.Core.CompileExpr.CDelay', E113, E114} -> (fun (V80, V81) -> fun (V82) -> begin (V83 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V81))(V82))), case V83 of {'Idris.Prelude.Types.Left', E115} -> (fun (V84) -> {'Idris.Prelude.Types.Left', V84} end(E115)); {'Idris.Prelude.Types.Right', E116} -> (fun (V85) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CDelay', V80, V85}))} end(E116)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E113, E114)); {'Idris.Core.CompileExpr.CConCase', E117, E118, E119, E120} -> (fun (V86, V87, V88, V89) -> fun (V90) -> begin (V91 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V87))(V90))), case V91 of {'Idris.Prelude.Types.Left', E121} -> (fun (V92) -> {'Idris.Prelude.Types.Left', V92} end(E121)); {'Idris.Prelude.Types.Right', E122} -> (fun (V93) -> begin (V94 = (('un--pickAlt'(V0, V1, V2, V3, V4, V5, V6, V93, V88, V89))(V90))), case V94 of {'Idris.Prelude.Types.Left', E123} -> (fun (V95) -> {'Idris.Prelude.Types.Left', V95} end(E123)); {'Idris.Prelude.Types.Right', E124} -> (fun (V96) -> case V96 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V98 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V97) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V97)) end, V89))(V90))), case V98 of {'Idris.Prelude.Types.Left', E125} -> (fun (V99) -> {'Idris.Prelude.Types.Left', V99} end(E125)); {'Idris.Prelude.Types.Right', E126} -> (fun (V100) -> begin (V102 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V101) -> ('un--evalAlt'(V0, V1, V2, V3, V86, V4, V5, V6, V101)) end, V88))(V90))), case V102 of {'Idris.Prelude.Types.Left', E127} -> (fun (V103) -> {'Idris.Prelude.Types.Left', V103} end(E127)); {'Idris.Prelude.Types.Right', E128} -> (fun (V104) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConCase', V86, V93, V104, V100}} end(E128)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E126)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E129} -> (fun (V105) -> {'Idris.Prelude.Types.Right', V105} end(E129)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E124)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E122)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E117, E118, E119, E120)); {'Idris.Core.CompileExpr.CConstCase', E130, E131, E132, E133} -> (fun (V106, V107, V108, V109) -> fun (V110) -> begin (V111 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V107))(V110))), case V111 of {'Idris.Prelude.Types.Left', E134} -> (fun (V112) -> {'Idris.Prelude.Types.Left', V112} end(E134)); {'Idris.Prelude.Types.Right', E135} -> (fun (V113) -> begin (V114 = (('un--pickConstAlt'(V0, V1, V2, V3, V4, V5, V6, V113, V108, V109))(V110))), case V114 of {'Idris.Prelude.Types.Left', E136} -> (fun (V115) -> {'Idris.Prelude.Types.Left', V115} end(E136)); {'Idris.Prelude.Types.Right', E137} -> (fun (V116) -> case V116 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V118 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V117) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V117)) end, V109))(V110))), case V118 of {'Idris.Prelude.Types.Left', E138} -> (fun (V119) -> {'Idris.Prelude.Types.Left', V119} end(E138)); {'Idris.Prelude.Types.Right', E139} -> (fun (V120) -> begin (V122 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V121) -> ('un--evalConstAlt'(V0, V1, V2, V3, V4, V5, V6, V121)) end, V108))(V110))), case V122 of {'Idris.Prelude.Types.Left', E140} -> (fun (V123) -> {'Idris.Prelude.Types.Left', V123} end(E140)); {'Idris.Prelude.Types.Right', E141} -> (fun (V124) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConstCase', V106, V113, V124, V120}} end(E141)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E139)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E142} -> (fun (V125) -> {'Idris.Prelude.Types.Right', V125} end(E142)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E137)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E135)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E130, E131, E132, E133)); {'Idris.Core.CompileExpr.CPrimVal', E143, E144} -> (fun (V126, V127) -> fun (V128) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CPrimVal', V126, V127}))} end end(E143, E144)); {'Idris.Core.CompileExpr.CErased', E145} -> (fun (V129) -> fun (V130) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CErased', V129}))} end end(E145)); {'Idris.Core.CompileExpr.CCrash', E146, E147} -> (fun (V131, V132) -> fun (V133) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCrash', V131, V132}))} end end(E146, E147)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; [E155 | E156] -> (fun (V134, V135) -> case V7 of {'Idris.Core.CompileExpr.CLam', E231, E232, E233} -> (fun (V136, V137, V138) -> ('un--eval'([V137 | V0], V1, V2, V3, V4, {'Idris.Compiler.Inline.::', V134, V5}, V135, V138)) end(E231, E232, E233)); _ -> case V7 of {'Idris.Core.CompileExpr.CLet', E157, E158, E159, E160, E161} -> (fun (V139, V140, V141, V142, V143) -> case V141 of 1 -> fun (V144) -> begin (V145 = ('un--genName'(V3, <<"letv"/utf8>>, V144))), case V145 of {'Idris.Prelude.Types.Left', E162} -> (fun (V146) -> {'Idris.Prelude.Types.Left', V146} end(E162)); {'Idris.Prelude.Types.Right', E163} -> (fun (V147) -> begin (V148 = (('un--eval'([V140 | V0], V1, V2, V3, V4, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V139, V147}, V5}, [], V143))(V144))), case V148 of {'Idris.Prelude.Types.Left', E164} -> (fun (V149) -> {'Idris.Prelude.Types.Left', V149} end(E164)); {'Idris.Prelude.Types.Right', E165} -> (fun (V150) -> begin (V151 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V142))(V144))), case V151 of {'Idris.Prelude.Types.Left', E166} -> (fun (V152) -> {'Idris.Prelude.Types.Left', V152} end(E166)); {'Idris.Prelude.Types.Right', E167} -> (fun (V153) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CLet', V139, V140, 1, V153, ('un--refToLocal'('erased', V147, V140, V150))}))} end(E167)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E165)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E163)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 0 -> begin (V154 = ('un--used'('erased', [V140 | ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V0, V1))], 0, 'erased', V143))), ('case--eval-4752'(V140, V1, V0, V143, V142, V139, V6, V5, V4, V3, V2, V154, ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V154, 1)))) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E157, E158, E159, E160, E161)); {'Idris.Core.CompileExpr.CApp', E168, E169, E170} -> (fun (V155, V156, V157) -> fun (V158) -> begin (V160 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V159) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V159)) end, V157))(V158))), case V160 of {'Idris.Prelude.Types.Left', E171} -> (fun (V161) -> {'Idris.Prelude.Types.Left', V161} end(E171)); {'Idris.Prelude.Types.Right', E172} -> (fun (V162) -> (('un--eval'(V0, V1, V2, V3, V4, V5, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V162, V6)), V156))(V158)) end(E172)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E168, E169, E170)); {'Idris.Core.CompileExpr.CCon', E173, E174, E175, E176} -> (fun (V163, V164, V165, V166) -> fun (V167) -> begin (V169 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V168) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V168)) end, V166))(V167))), case V169 of {'Idris.Prelude.Types.Left', E177} -> (fun (V170) -> {'Idris.Prelude.Types.Left', V170} end(E177)); {'Idris.Prelude.Types.Right', E178} -> (fun (V171) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCon', V163, V164, V165, V171}))} end(E178)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E173, E174, E175, E176)); {'Idris.Core.CompileExpr.COp', E179, E180, E181, E182} -> (fun (V172, V173, V174, V175) -> fun (V176) -> begin (V178 = (('Idris.Idris2.Core.Core':'un--traverseVect'('erased', 'erased', 'erased', fun (V177) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V177)) end, V175))(V176))), case V178 of {'Idris.Prelude.Types.Left', E183} -> (fun (V179) -> {'Idris.Prelude.Types.Left', V179} end(E183)); {'Idris.Prelude.Types.Right', E184} -> (fun (V180) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.COp', V172, V173, V174, V180}))} end(E184)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E179, E180, E181, E182)); {'Idris.Core.CompileExpr.CExtPrim', E185, E186, E187} -> (fun (V181, V182, V183) -> fun (V184) -> begin (V186 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V185) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V185)) end, V183))(V184))), case V186 of {'Idris.Prelude.Types.Left', E188} -> (fun (V187) -> {'Idris.Prelude.Types.Left', V187} end(E188)); {'Idris.Prelude.Types.Right', E189} -> (fun (V188) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CExtPrim', V181, V182, V188}))} end(E189)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E185, E186, E187)); {'Idris.Core.CompileExpr.CForce', E190, E191} -> (fun (V189, V190) -> fun (V191) -> begin (V192 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V190))(V191))), case V192 of {'Idris.Prelude.Types.Left', E192} -> (fun (V193) -> {'Idris.Prelude.Types.Left', V193} end(E192)); {'Idris.Prelude.Types.Right', E193} -> (fun (V194) -> case V194 of {'Idris.Core.CompileExpr.CDelay', E194, E195} -> (fun (V195, V196) -> (('un--eval'([], V1, V2, V3, V4, {'Idris.Compiler.Inline.Nil'}, V6, V196))(V191)) end(E194, E195)); _ -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CForce', V189, V194}))} end end(E193)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E190, E191)); {'Idris.Core.CompileExpr.CDelay', E196, E197} -> (fun (V197, V198) -> fun (V199) -> begin (V200 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V198))(V199))), case V200 of {'Idris.Prelude.Types.Left', E198} -> (fun (V201) -> {'Idris.Prelude.Types.Left', V201} end(E198)); {'Idris.Prelude.Types.Right', E199} -> (fun (V202) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CDelay', V197, V202}))} end(E199)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E196, E197)); {'Idris.Core.CompileExpr.CConCase', E200, E201, E202, E203} -> (fun (V203, V204, V205, V206) -> fun (V207) -> begin (V208 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V204))(V207))), case V208 of {'Idris.Prelude.Types.Left', E204} -> (fun (V209) -> {'Idris.Prelude.Types.Left', V209} end(E204)); {'Idris.Prelude.Types.Right', E205} -> (fun (V210) -> begin (V211 = (('un--pickAlt'(V0, V1, V2, V3, V4, V5, V6, V210, V205, V206))(V207))), case V211 of {'Idris.Prelude.Types.Left', E206} -> (fun (V212) -> {'Idris.Prelude.Types.Left', V212} end(E206)); {'Idris.Prelude.Types.Right', E207} -> (fun (V213) -> case V213 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V215 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V214) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V214)) end, V206))(V207))), case V215 of {'Idris.Prelude.Types.Left', E208} -> (fun (V216) -> {'Idris.Prelude.Types.Left', V216} end(E208)); {'Idris.Prelude.Types.Right', E209} -> (fun (V217) -> begin (V219 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V218) -> ('un--evalAlt'(V0, V1, V2, V3, V203, V4, V5, V6, V218)) end, V205))(V207))), case V219 of {'Idris.Prelude.Types.Left', E210} -> (fun (V220) -> {'Idris.Prelude.Types.Left', V220} end(E210)); {'Idris.Prelude.Types.Right', E211} -> (fun (V221) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConCase', V203, V210, V221, V217}} end(E211)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E209)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E212} -> (fun (V222) -> {'Idris.Prelude.Types.Right', V222} end(E212)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E207)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E205)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E200, E201, E202, E203)); {'Idris.Core.CompileExpr.CConstCase', E213, E214, E215, E216} -> (fun (V223, V224, V225, V226) -> fun (V227) -> begin (V228 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V224))(V227))), case V228 of {'Idris.Prelude.Types.Left', E217} -> (fun (V229) -> {'Idris.Prelude.Types.Left', V229} end(E217)); {'Idris.Prelude.Types.Right', E218} -> (fun (V230) -> begin (V231 = (('un--pickConstAlt'(V0, V1, V2, V3, V4, V5, V6, V230, V225, V226))(V227))), case V231 of {'Idris.Prelude.Types.Left', E219} -> (fun (V232) -> {'Idris.Prelude.Types.Left', V232} end(E219)); {'Idris.Prelude.Types.Right', E220} -> (fun (V233) -> case V233 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V235 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V234) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V234)) end, V226))(V227))), case V235 of {'Idris.Prelude.Types.Left', E221} -> (fun (V236) -> {'Idris.Prelude.Types.Left', V236} end(E221)); {'Idris.Prelude.Types.Right', E222} -> (fun (V237) -> begin (V239 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V238) -> ('un--evalConstAlt'(V0, V1, V2, V3, V4, V5, V6, V238)) end, V225))(V227))), case V239 of {'Idris.Prelude.Types.Left', E223} -> (fun (V240) -> {'Idris.Prelude.Types.Left', V240} end(E223)); {'Idris.Prelude.Types.Right', E224} -> (fun (V241) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConstCase', V223, V230, V241, V237}} end(E224)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E222)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E225} -> (fun (V242) -> {'Idris.Prelude.Types.Right', V242} end(E225)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E220)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E218)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E213, E214, E215, E216)); {'Idris.Core.CompileExpr.CPrimVal', E226, E227} -> (fun (V243, V244) -> fun (V245) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CPrimVal', V243, V244}))} end end(E226, E227)); {'Idris.Core.CompileExpr.CErased', E228} -> (fun (V246) -> fun (V247) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CErased', V246}))} end end(E228)); {'Idris.Core.CompileExpr.CCrash', E229, E230} -> (fun (V248, V249) -> fun (V250) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCrash', V248, V249}))} end end(E229, E230)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E155, E156)); _ -> case V7 of {'Idris.Core.CompileExpr.CLet', E0, E1, E2, E3, E4} -> (fun (V251, V252, V253, V254, V255) -> case V253 of 1 -> fun (V256) -> begin (V257 = ('un--genName'(V3, <<"letv"/utf8>>, V256))), case V257 of {'Idris.Prelude.Types.Left', E5} -> (fun (V258) -> {'Idris.Prelude.Types.Left', V258} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V259) -> begin (V260 = (('un--eval'([V252 | V0], V1, V2, V3, V4, {'Idris.Compiler.Inline.::', {'Idris.Core.CompileExpr.CRef', V251, V259}, V5}, [], V255))(V256))), case V260 of {'Idris.Prelude.Types.Left', E7} -> (fun (V261) -> {'Idris.Prelude.Types.Left', V261} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V262) -> begin (V263 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V254))(V256))), case V263 of {'Idris.Prelude.Types.Left', E9} -> (fun (V264) -> {'Idris.Prelude.Types.Left', V264} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V265) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CLet', V251, V252, 1, V265, ('un--refToLocal'('erased', V259, V252, V262))}))} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 0 -> begin (V266 = ('un--used'('erased', [V252 | ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V0, V1))], 0, 'erased', V255))), ('case--eval-4752'(V252, V1, V0, V255, V254, V251, V6, V5, V4, V3, V2, V266, ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V266, 1)))) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1, E2, E3, E4)); {'Idris.Core.CompileExpr.CApp', E11, E12, E13} -> (fun (V267, V268, V269) -> fun (V270) -> begin (V272 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V271) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V271)) end, V269))(V270))), case V272 of {'Idris.Prelude.Types.Left', E14} -> (fun (V273) -> {'Idris.Prelude.Types.Left', V273} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V274) -> (('un--eval'(V0, V1, V2, V3, V4, V5, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V274, V6)), V268))(V270)) end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E11, E12, E13)); {'Idris.Core.CompileExpr.CCon', E16, E17, E18, E19} -> (fun (V275, V276, V277, V278) -> fun (V279) -> begin (V281 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V280) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V280)) end, V278))(V279))), case V281 of {'Idris.Prelude.Types.Left', E20} -> (fun (V282) -> {'Idris.Prelude.Types.Left', V282} end(E20)); {'Idris.Prelude.Types.Right', E21} -> (fun (V283) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCon', V275, V276, V277, V283}))} end(E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E16, E17, E18, E19)); {'Idris.Core.CompileExpr.COp', E22, E23, E24, E25} -> (fun (V284, V285, V286, V287) -> fun (V288) -> begin (V290 = (('Idris.Idris2.Core.Core':'un--traverseVect'('erased', 'erased', 'erased', fun (V289) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V289)) end, V287))(V288))), case V290 of {'Idris.Prelude.Types.Left', E26} -> (fun (V291) -> {'Idris.Prelude.Types.Left', V291} end(E26)); {'Idris.Prelude.Types.Right', E27} -> (fun (V292) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.COp', V284, V285, V286, V292}))} end(E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E22, E23, E24, E25)); {'Idris.Core.CompileExpr.CExtPrim', E28, E29, E30} -> (fun (V293, V294, V295) -> fun (V296) -> begin (V298 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V297) -> ('un--eval'(V0, V1, V2, V3, V4, V5, [], V297)) end, V295))(V296))), case V298 of {'Idris.Prelude.Types.Left', E31} -> (fun (V299) -> {'Idris.Prelude.Types.Left', V299} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V300) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CExtPrim', V293, V294, V300}))} end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E28, E29, E30)); {'Idris.Core.CompileExpr.CForce', E33, E34} -> (fun (V301, V302) -> fun (V303) -> begin (V304 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V302))(V303))), case V304 of {'Idris.Prelude.Types.Left', E35} -> (fun (V305) -> {'Idris.Prelude.Types.Left', V305} end(E35)); {'Idris.Prelude.Types.Right', E36} -> (fun (V306) -> case V306 of {'Idris.Core.CompileExpr.CDelay', E37, E38} -> (fun (V307, V308) -> (('un--eval'([], V1, V2, V3, V4, {'Idris.Compiler.Inline.Nil'}, V6, V308))(V303)) end(E37, E38)); _ -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CForce', V301, V306}))} end end(E36)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E33, E34)); {'Idris.Core.CompileExpr.CDelay', E39, E40} -> (fun (V309, V310) -> fun (V311) -> begin (V312 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V310))(V311))), case V312 of {'Idris.Prelude.Types.Left', E41} -> (fun (V313) -> {'Idris.Prelude.Types.Left', V313} end(E41)); {'Idris.Prelude.Types.Right', E42} -> (fun (V314) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CDelay', V309, V314}))} end(E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E39, E40)); {'Idris.Core.CompileExpr.CConCase', E43, E44, E45, E46} -> (fun (V315, V316, V317, V318) -> fun (V319) -> begin (V320 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V316))(V319))), case V320 of {'Idris.Prelude.Types.Left', E47} -> (fun (V321) -> {'Idris.Prelude.Types.Left', V321} end(E47)); {'Idris.Prelude.Types.Right', E48} -> (fun (V322) -> begin (V323 = (('un--pickAlt'(V0, V1, V2, V3, V4, V5, V6, V322, V317, V318))(V319))), case V323 of {'Idris.Prelude.Types.Left', E49} -> (fun (V324) -> {'Idris.Prelude.Types.Left', V324} end(E49)); {'Idris.Prelude.Types.Right', E50} -> (fun (V325) -> case V325 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V327 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V326) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V326)) end, V318))(V319))), case V327 of {'Idris.Prelude.Types.Left', E51} -> (fun (V328) -> {'Idris.Prelude.Types.Left', V328} end(E51)); {'Idris.Prelude.Types.Right', E52} -> (fun (V329) -> begin (V331 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V330) -> ('un--evalAlt'(V0, V1, V2, V3, V315, V4, V5, V6, V330)) end, V317))(V319))), case V331 of {'Idris.Prelude.Types.Left', E53} -> (fun (V332) -> {'Idris.Prelude.Types.Left', V332} end(E53)); {'Idris.Prelude.Types.Right', E54} -> (fun (V333) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConCase', V315, V322, V333, V329}} end(E54)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E52)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E55} -> (fun (V334) -> {'Idris.Prelude.Types.Right', V334} end(E55)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E50)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E48)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E43, E44, E45, E46)); {'Idris.Core.CompileExpr.CConstCase', E56, E57, E58, E59} -> (fun (V335, V336, V337, V338) -> fun (V339) -> begin (V340 = (('un--eval'(V0, V1, V2, V3, V4, V5, [], V336))(V339))), case V340 of {'Idris.Prelude.Types.Left', E60} -> (fun (V341) -> {'Idris.Prelude.Types.Left', V341} end(E60)); {'Idris.Prelude.Types.Right', E61} -> (fun (V342) -> begin (V343 = (('un--pickConstAlt'(V0, V1, V2, V3, V4, V5, V6, V342, V337, V338))(V339))), case V343 of {'Idris.Prelude.Types.Left', E62} -> (fun (V344) -> {'Idris.Prelude.Types.Left', V344} end(E62)); {'Idris.Prelude.Types.Right', E63} -> (fun (V345) -> case V345 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V347 = (('Idris.Idris2.Core.Core':'un--traverseOpt'('erased', 'erased', fun (V346) -> ('un--eval'(V0, V1, V2, V3, V4, V5, V6, V346)) end, V338))(V339))), case V347 of {'Idris.Prelude.Types.Left', E64} -> (fun (V348) -> {'Idris.Prelude.Types.Left', V348} end(E64)); {'Idris.Prelude.Types.Right', E65} -> (fun (V349) -> begin (V351 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V350) -> ('un--evalConstAlt'(V0, V1, V2, V3, V4, V5, V6, V350)) end, V337))(V339))), case V351 of {'Idris.Prelude.Types.Left', E66} -> (fun (V352) -> {'Idris.Prelude.Types.Left', V352} end(E66)); {'Idris.Prelude.Types.Right', E67} -> (fun (V353) -> {'Idris.Prelude.Types.Right', {'Idris.Core.CompileExpr.CConstCase', V335, V342, V353, V349}} end(E67)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E65)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E68} -> (fun (V354) -> {'Idris.Prelude.Types.Right', V354} end(E68)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E63)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E61)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E56, E57, E58, E59)); {'Idris.Core.CompileExpr.CPrimVal', E69, E70} -> (fun (V355, V356) -> fun (V357) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CPrimVal', V355, V356}))} end end(E69, E70)); {'Idris.Core.CompileExpr.CErased', E71} -> (fun (V358) -> fun (V359) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CErased', V358}))} end end(E71)); {'Idris.Core.CompileExpr.CCrash', E72, E73} -> (fun (V360, V361) -> fun (V362) -> {'Idris.Prelude.Types.Right', ('un--unload'('erased', V6, {'Idris.Core.CompileExpr.CCrash', V360, V361}))} end end(E72, E73)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end.
'un--doEval'(V0, V1, V2, V3, V4) -> begin (V5 = ('Idris.Idris2.Core.Core':'un--newRef'('erased', 'erased', {'Idris.Compiler.Inline.LVar'}, 0, V4))), case V5 of {'Idris.Prelude.Types.Left', E0} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V7) -> begin (V8 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"compiler.inline.eval"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V2)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<": "/utf8>>, ('Idris.Idris2.Core.CompileExpr':'dn--un--show_Show__(CExp $vars)'(V0, V3)))))) end))(V4))), case V8 of {'Idris.Prelude.Types.Left', E2} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V10) -> begin (V11 = (('un--eval'([], V0, V1, V7, [], {'Idris.Compiler.Inline.Nil'}, [], V3))(V4))), case V11 of {'Idris.Prelude.Types.Left', E4} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V13) -> begin (V14 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"compiler.inline.eval"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Inlined: "/utf8>>, ('Idris.Idris2.Core.CompileExpr':'dn--un--show_Show__(CExp $vars)'(V0, V13)))) end))(V4))), case V14 of {'Idris.Prelude.Types.Left', E6} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V16) -> {'Idris.Prelude.Types.Right', V13} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--compileAndInlineAll'(V0, V1) -> begin (V30 = begin (V29 = (('Idris.Idris2.Erlang.Data.IORef':'un--readIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V2) -> fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V4, V5, V6)) end end end end end, fun (V7) -> fun (V8) -> fun (V9) -> V8 end end end, fun (V10) -> fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> begin (V15 = (V12(V14))), begin (V16 = (V13(V14))), (V15(V16)) end end end end end end end}, fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> begin (V22 = (V19(V21))), ((V20(V22))(V21)) end end end end end end, fun (V23) -> fun (V24) -> fun (V25) -> begin (V26 = (V24(V25))), (V26(V25)) end end end end}, fun (V27) -> fun (V28) -> V28 end end}, V0))(V1))), {'Idris.Prelude.Types.Right', V29} end), case V30 of {'Idris.Prelude.Types.Left', E0} -> (fun (V31) -> {'Idris.Prelude.Types.Left', V31} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V32) -> begin (V59 = ('Idris.Idris2.Data.NameMap':'un--keys'('erased', case V32 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58) -> V54 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))), begin (V62 = (('Idris.Idris2.Core.Core':'un--filterM'('erased', fun (V60) -> fun (V61) -> ('nested--10957-6826--in--un--nonErased'(V0, V60, V61)) end end, V59))(V1))), case V62 of {'Idris.Prelude.Types.Left', E28} -> (fun (V63) -> {'Idris.Prelude.Types.Left', V63} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V64) -> begin (V67 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V65) -> fun (V66) -> ('Idris.Idris2.Compiler.CompileExpr':'un--compileDef'(V0, V65, V66)) end end, V64))(V1))), case V67 of {'Idris.Prelude.Types.Left', E30} -> (fun (V68) -> {'Idris.Prelude.Types.Left', V68} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V69) -> begin (V72 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V70) -> fun (V71) -> ('un--inlineDef'(V0, V70, V71)) end end, V64))(V1))), case V72 of {'Idris.Prelude.Types.Left', E32} -> (fun (V73) -> {'Idris.Prelude.Types.Left', V73} end(E32)); {'Idris.Prelude.Types.Right', E33} -> (fun (V74) -> begin (V77 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V75) -> fun (V76) -> ('un--mergeLamDef'(V0, V75, V76)) end end, V64))(V1))), case V77 of {'Idris.Prelude.Types.Left', E34} -> (fun (V78) -> {'Idris.Prelude.Types.Left', V78} end(E34)); {'Idris.Prelude.Types.Right', E35} -> (fun (V79) -> begin (V82 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V80) -> fun (V81) -> ('un--fixArityDef'(V0, V80, V81)) end end, V64))(V1))), case V82 of {'Idris.Prelude.Types.Left', E36} -> (fun (V83) -> {'Idris.Prelude.Types.Left', V83} end(E36)); {'Idris.Prelude.Types.Right', E37} -> (fun (V84) -> begin (V87 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V85) -> fun (V86) -> ('un--inlineDef'(V0, V85, V86)) end end, V64))(V1))), case V87 of {'Idris.Prelude.Types.Left', E38} -> (fun (V88) -> {'Idris.Prelude.Types.Left', V88} end(E38)); {'Idris.Prelude.Types.Right', E39} -> (fun (V89) -> begin (V92 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V90) -> fun (V91) -> ('un--mergeLamDef'(V0, V90, V91)) end end, V64))(V1))), case V92 of {'Idris.Prelude.Types.Left', E40} -> (fun (V93) -> {'Idris.Prelude.Types.Left', V93} end(E40)); {'Idris.Prelude.Types.Right', E41} -> (fun (V94) -> (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V95) -> fun (V96) -> ('un--fixArityDef'(V0, V95, V96)) end end, V64))(V1)) end(E41)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E37)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E35)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E33)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--Stack'(V0) -> {'Idris.Prelude.Types.List', {'Idris.Core.CompileExpr.CExp', V0}}.