Current section
Files
Jump to
Current section
Files
src/Idris.Idris2.Core.CompileExpr.erl
-module('Idris.Idris2.Core.CompileExpr').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
'case--mkLocals-3139'/10,
'case--case block in resolveRef-3003'/15,
'case--resolveRef-2946'/13,
'case--case block in find-2475'/10,
'case--find-2436'/8,
'case--shrinkCExp-2010'/8,
'case--insertNames-1595'/10,
'case--uniqueName-922'/4,
'dn--un--weaken_Weaken__CExp'/3,
'dn--un--weakenNs_Weaken__CExp'/4,
'dn--un--show_Show__NamedDef'/1,
'dn--un--show_Show__NamedConstAlt'/1,
'dn--un--show_Show__NamedConAlt'/1,
'dn--un--show_Show__NamedCExp'/1,
'dn--un--show_Show__CFType'/1,
'dn--un--show_Show__CDef'/1,
'dn--un--show_Show__(CExp $vars)'/2,
'dn--un--showPrec_Show__NamedDef'/2,
'dn--un--showPrec_Show__NamedConstAlt'/2,
'dn--un--showPrec_Show__NamedConAlt'/2,
'dn--un--showPrec_Show__NamedCExp'/2,
'dn--un--showPrec_Show__CFType'/2,
'dn--un--showPrec_Show__CDef'/2,
'dn--un--showPrec_Show__(CExp $vars)'/3,
'dn--un--__Impl_Weaken_CExp'/0,
'dn--un--__Impl_Show_NamedDef'/0,
'dn--un--__Impl_Show_NamedConstAlt'/0,
'dn--un--__Impl_Show_NamedConAlt'/0,
'dn--un--__Impl_Show_NamedCExp'/0,
'dn--un--__Impl_Show_CFType'/0,
'dn--un--__Impl_Show_CDef'/0,
'dn--un--__Impl_Show_(CExp $vars)'/1,
'un--uniqueName'/3,
'un--tryNext'/1,
'un--substs'/4,
'un--substEnv'/6,
'un--substConstAlt'/6,
'un--substConAlt'/6,
'un--shrinkConstAlt'/4,
'un--shrinkConAlt'/4,
'un--shrinkCExp'/4,
'un--resolveRef'/9,
'un--refsToLocals'/4,
'un--mkLocalsConstAlt'/6,
'un--mkLocalsConAlt'/6,
'un--mkLocals'/6,
'un--insertNamesConstAlt'/6,
'un--insertNamesConAlt'/6,
'un--insertNames'/6,
'un--getLocName'/5,
'un--getFC'/2,
'un--forgetExp'/3,
'un--forgetDef'/1,
'un--forgetConstAlt'/3,
'un--forgetConAlt'/3,
'un--forget'/2,
'un--findDrop'/5,
'un--find'/7,
'un--embed'/3,
'un--elem'/3,
'un--conArgs'/3,
'un--addLocs'/3
]).
'case--mkLocals-3139'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> {'Idris.Core.CompileExpr.CLocal', V9, V6}.
'case--case block in resolveRef-3003'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14) -> {'Idris.Prelude.Types.Just', {'Idris.Core.CompileExpr.CLocal', V14, V5}}.
'case--resolveRef-2946'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of 0 -> ('case--case block in resolveRef-3003'('erased', V1, V2, V3, V4, V5, 'erased', V7, 'erased', V9, 'erased', 'erased', 'erased', 'erased', ('Idris.Idris2.Core.TT':'un--weakenNVar'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--+'('erased', 'erased', 'erased', V9, V7)), 0)))); 1 -> ('un--resolveRef'('erased', 'erased', 'erased', 'erased', V9, ('Idris.Idris2.Core.TT.SizeOf':'un--sucR'('erased', 'erased', 'erased', V7)), V1, V5, V4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in find-2475'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V5 of 0 -> {'Idris.Core.CompileExpr.CLocal', 0, V6}; _ -> begin (V10 = (V5 - 1)), ('dn--un--weaken_Weaken__CExp'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V6, V7, V10, V2)))) end end.
'case--find-2436'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V5 of 0 -> case V7 of {'Idris.Core.TT.SizedView.Z'} -> (fun () -> ('un--findDrop'('erased', 'erased', V6, V4, V3)) end()); _ -> case V7 of {'Idris.Core.TT.SizedView.S', E1} -> (fun (V8) -> case V4 of 0 -> {'Idris.Core.CompileExpr.CLocal', 0, V6}; _ -> begin (V9 = (V4 - 1)), ('dn--un--weaken_Weaken__CExp'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V6, V8, V9, V3)))) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> case V7 of {'Idris.Core.TT.SizedView.S', E0} -> (fun (V10) -> case V4 of 0 -> {'Idris.Core.CompileExpr.CLocal', 0, V6}; _ -> begin (V11 = (V4 - 1)), ('dn--un--weaken_Weaken__CExp'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V6, V10, V11, V3)))) end end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'case--shrinkCExp-2010'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Core.CompileExpr.CErased', V5} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V8) -> {'Idris.Core.CompileExpr.CLocal', V8, V5} end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--insertNames-1595'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> {'Idris.Core.CompileExpr.CLocal', V9, V6}.
'case--uniqueName-922'(V0, V1, V2, V3) -> case V3 of 0 -> ('un--uniqueName'('erased', ('un--tryNext'(V2)), V1)); 1 -> V2; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--weaken_Weaken__CExp'(V0, V1, V2) -> ('dn--un--weakenNs_Weaken__CExp'('erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')))), V2)).
'dn--un--weakenNs_Weaken__CExp'(V0, V1, V2, V3) -> ('un--insertNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V2, V3)).
'dn--un--show_Show__NamedDef'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkNmFun', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V3) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)) end, fun (V4) -> fun (V5) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V4, V5)) end end}, V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<": "/utf8>>, ('dn--un--show_Show__NamedCExp'(V2)))))) end(E0, E1)); {'Idris.Core.CompileExpr.MkNmCon', E2, E3, E4} -> (fun (V6, V7, V8) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Constructor tag "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V9) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V9)) end, fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V10, V11)) end end}, V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" arity "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V7)), ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> <<""/utf8>> end, fun () -> fun (V12) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" (newtype by "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V12)), <<")"/utf8>>)))) end end, V8)))))))))) end(E2, E3, E4)); {'Idris.Core.CompileExpr.MkNmForeign', E5, E6, E7} -> (fun (V13, V14, V15) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Foreign call "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V16) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V16)) end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__String'(V17, V18)) end end}, V13)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V19) -> ('dn--un--show_Show__CFType'(V19)) end, fun (V20) -> fun (V21) -> ('dn--un--showPrec_Show__CFType'(V20, V21)) end end}, V14)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" -> "/utf8>>, ('dn--un--show_Show__CFType'(V15)))))))))))) end(E5, E6, E7)); {'Idris.Core.CompileExpr.MkNmError', E8} -> (fun (V22) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Error: "/utf8>>, ('dn--un--show_Show__NamedCExp'(V22)))) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__NamedConstAlt'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkNConstAlt', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%constcase "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V2)), <<")"/utf8>>)))))))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__NamedConAlt'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkNConAlt', E0, E1, E2, E3} -> (fun (V1, V2, V3, V4) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%concase "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V5) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V5)) end, fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V6, V7)) end end}, V2)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V8) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V8)) end, fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V9, V10)) end end}, V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V4)), <<")"/utf8>>)))))))))))))))) end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__NamedCExp'(V0) -> case V0 of {'Idris.Core.CompileExpr.NmLocal', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"!"/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V2)))) end(E0, E1)); {'Idris.Core.CompileExpr.NmRef', E2, E3} -> (fun (V3, V4) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V4)) end(E2, E3)); {'Idris.Core.CompileExpr.NmLam', E4, E5, E6} -> (fun (V5, V6, V7) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%lam "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V7)), <<")"/utf8>>)))))))) end(E4, E5, E6)); {'Idris.Core.CompileExpr.NmLet', E7, E8, E9, E10} -> (fun (V8, V9, V10, V11) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%let "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V9)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V10)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V11)), <<")"/utf8>>)))))))))))) end(E7, E8, E9, E10)); {'Idris.Core.CompileExpr.NmApp', E11, E12, E13} -> (fun (V12, V13, V14) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V13)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V15) -> ('dn--un--show_Show__NamedCExp'(V15)) end, fun (V16) -> fun (V17) -> ('dn--un--showPrec_Show__NamedCExp'(V16, V17)) end end}, V14)), <<")"/utf8>>)))))))) end(E11, E12, E13)); {'Idris.Core.CompileExpr.NmCon', E14, E15, E16, E17} -> (fun (V18, V19, V20, V21) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%con "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V19)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V22) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V22)) end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V23, V24)) end end}, V20)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V25) -> ('dn--un--show_Show__NamedCExp'(V25)) end, fun (V26) -> fun (V27) -> ('dn--un--showPrec_Show__NamedCExp'(V26, V27)) end end}, V21)), <<")"/utf8>>)))))))))))) end(E14, E15, E16, E17)); {'Idris.Core.CompileExpr.NmOp', E18, E19, E20, E21} -> (fun (V28, V29, V30, V31) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'dn--un--show_Show__(PrimFn $arity)'('erased', V30)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Data.Vect':'dn--un--show_Show__((Vect $len) $elem)'('erased', 'erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V32) -> ('dn--un--show_Show__NamedCExp'(V32)) end, fun (V33) -> fun (V34) -> ('dn--un--showPrec_Show__NamedCExp'(V33, V34)) end end}, V31)), <<")"/utf8>>)))))))) end(E18, E19, E20, E21)); {'Idris.Core.CompileExpr.NmExtPrim', E22, E23, E24} -> (fun (V35, V36, V37) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%extern "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V36)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V38) -> ('dn--un--show_Show__NamedCExp'(V38)) end, fun (V39) -> fun (V40) -> ('dn--un--showPrec_Show__NamedCExp'(V39, V40)) end end}, V37)), <<")"/utf8>>)))))))) end(E22, E23, E24)); {'Idris.Core.CompileExpr.NmForce', E25, E26} -> (fun (V41, V42) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%force "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V42)), <<")"/utf8>>)))) end(E25, E26)); {'Idris.Core.CompileExpr.NmDelay', E27, E28} -> (fun (V43, V44) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%delay "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V44)), <<")"/utf8>>)))) end(E27, E28)); {'Idris.Core.CompileExpr.NmConCase', E29, E30, E31, E32} -> (fun (V45, V46, V47, V48) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%case "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V46)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V49) -> ('dn--un--show_Show__NamedConAlt'(V49)) end, fun (V50) -> fun (V51) -> ('dn--un--showPrec_Show__NamedConAlt'(V50, V51)) end end}, V47)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V52) -> ('dn--un--show_Show__NamedCExp'(V52)) end, fun (V53) -> fun (V54) -> ('dn--un--showPrec_Show__NamedCExp'(V53, V54)) end end}, V48)), <<")"/utf8>>)))))))))))) end(E29, E30, E31, E32)); {'Idris.Core.CompileExpr.NmConstCase', E33, E34, E35, E36} -> (fun (V55, V56, V57, V58) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(%case "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__NamedCExp'(V56)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V59) -> ('dn--un--show_Show__NamedConstAlt'(V59)) end, fun (V60) -> fun (V61) -> ('dn--un--showPrec_Show__NamedConstAlt'(V60, V61)) end end}, V57)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V62) -> ('dn--un--show_Show__NamedCExp'(V62)) end, fun (V63) -> fun (V64) -> ('dn--un--showPrec_Show__NamedCExp'(V63, V64)) end end}, V58)), <<")"/utf8>>)))))))))))) end(E33, E34, E35, E36)); {'Idris.Core.CompileExpr.NmPrimVal', E37, E38} -> (fun (V65, V66) -> ('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V66)) end(E37, E38)); {'Idris.Core.CompileExpr.NmErased', E39} -> (fun (V67) -> <<"___"/utf8>> end(E39)); {'Idris.Core.CompileExpr.NmCrash', E40, E41} -> (fun (V68, V69) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(CRASH "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V69)), <<")"/utf8>>)))) end(E40, E41)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__CFType'(V0) -> case V0 of {'Idris.Core.CompileExpr.CFUnit'} -> (fun () -> <<"Unit"/utf8>> end()); {'Idris.Core.CompileExpr.CFInt'} -> (fun () -> <<"Int"/utf8>> end()); {'Idris.Core.CompileExpr.CFUnsigned8'} -> (fun () -> <<"Bits_8"/utf8>> end()); {'Idris.Core.CompileExpr.CFUnsigned16'} -> (fun () -> <<"Bits_16"/utf8>> end()); {'Idris.Core.CompileExpr.CFUnsigned32'} -> (fun () -> <<"Bits_32"/utf8>> end()); {'Idris.Core.CompileExpr.CFUnsigned64'} -> (fun () -> <<"Bits_64"/utf8>> end()); {'Idris.Core.CompileExpr.CFString'} -> (fun () -> <<"String"/utf8>> end()); {'Idris.Core.CompileExpr.CFDouble'} -> (fun () -> <<"Double"/utf8>> end()); {'Idris.Core.CompileExpr.CFChar'} -> (fun () -> <<"Char"/utf8>> end()); {'Idris.Core.CompileExpr.CFPtr'} -> (fun () -> <<"Ptr"/utf8>> end()); {'Idris.Core.CompileExpr.CFGCPtr'} -> (fun () -> <<"GCPtr"/utf8>> end()); {'Idris.Core.CompileExpr.CFBuffer'} -> (fun () -> <<"Buffer"/utf8>> end()); {'Idris.Core.CompileExpr.CFWorld'} -> (fun () -> <<"%World"/utf8>> end()); {'Idris.Core.CompileExpr.CFFun', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__CFType'(V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" -> "/utf8>>, ('dn--un--show_Show__CFType'(V2)))))) end(E0, E1)); {'Idris.Core.CompileExpr.CFIORes', E2} -> (fun (V3) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"IORes "/utf8>>, ('dn--un--show_Show__CFType'(V3)))) end(E2)); {'Idris.Core.CompileExpr.CFStruct', E3, E4} -> (fun (V4, V5) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"struct "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V4)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Core.Name.Namespace':'un--showSep'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V6) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V7) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V7)) end, fun (V8) -> fun (V9) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__String'(V8, V9)) end end}, {'Idris.Prelude.Show.dn--un--__mkShow', fun (V10) -> ('dn--un--show_Show__CFType'(V10)) end, fun (V11) -> fun (V12) -> ('dn--un--showPrec_Show__CFType'(V11, V12)) end end}}, V6)) end, V5)))))))))) end(E3, E4)); {'Idris.Core.CompileExpr.CFUser', E5, E6} -> (fun (V13, V14) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V13)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Core.Name.Namespace':'un--showSep'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V15) -> ('dn--un--show_Show__CFType'(V15)) end, V14)))))))) end(E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__CDef'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V3) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)) end, fun (V4) -> fun (V5) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V4, V5)) end end}, V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<": "/utf8>>, ('dn--un--show_Show__(CExp $vars)'(V1, V2)))))) end(E0, E1)); {'Idris.Core.CompileExpr.MkCon', E2, E3, E4} -> (fun (V6, V7, V8) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Constructor tag "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(Maybe $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V9) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V9)) end, fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V10, V11)) end end}, V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" arity "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V7)), ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> <<""/utf8>> end, fun () -> fun (V12) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" (newtype by "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V12)), <<")"/utf8>>)))) end end, V8)))))))))) end(E2, E3, E4)); {'Idris.Core.CompileExpr.MkForeign', E5, E6, E7} -> (fun (V13, V14, V15) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Foreign call "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V16) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V16)) end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__String'(V17, V18)) end end}, V13)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V19) -> ('dn--un--show_Show__CFType'(V19)) end, fun (V20) -> fun (V21) -> ('dn--un--showPrec_Show__CFType'(V20, V21)) end end}, V14)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" -> "/utf8>>, ('dn--un--show_Show__CFType'(V15)))))))))))) end(E5, E6, E7)); {'Idris.Core.CompileExpr.MkError', E8} -> (fun (V22) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Error: "/utf8>>, ('dn--un--show_Show__(CExp $vars)'([], V22)))) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__(CExp $vars)'(V0, V1) -> ('dn--un--show_Show__NamedCExp'(('un--forget'(V0, V1)))).
'dn--un--showPrec_Show__NamedDef'(V0, V1) -> ('dn--un--show_Show__NamedDef'(V1)).
'dn--un--showPrec_Show__NamedConstAlt'(V0, V1) -> ('dn--un--show_Show__NamedConstAlt'(V1)).
'dn--un--showPrec_Show__NamedConAlt'(V0, V1) -> ('dn--un--show_Show__NamedConAlt'(V1)).
'dn--un--showPrec_Show__NamedCExp'(V0, V1) -> ('dn--un--show_Show__NamedCExp'(V1)).
'dn--un--showPrec_Show__CFType'(V0, V1) -> ('dn--un--show_Show__CFType'(V1)).
'dn--un--showPrec_Show__CDef'(V0, V1) -> ('dn--un--show_Show__CDef'(V1)).
'dn--un--showPrec_Show__(CExp $vars)'(V0, V1, V2) -> ('dn--un--show_Show__(CExp $vars)'(V0, V2)).
'dn--un--__Impl_Weaken_CExp'() -> {'Idris.Core.TT.dn--un--__mkWeaken', fun (V0) -> fun (V1) -> fun (V2) -> ('dn--un--weaken_Weaken__CExp'('erased', 'erased', V2)) end end end, fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> ('dn--un--weakenNs_Weaken__CExp'('erased', 'erased', V5, V6)) end end end end}.
'dn--un--__Impl_Show_NamedDef'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__NamedDef'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__NamedDef'(V1, V2)) end end}.
'dn--un--__Impl_Show_NamedConstAlt'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__NamedConstAlt'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__NamedConstAlt'(V1, V2)) end end}.
'dn--un--__Impl_Show_NamedConAlt'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__NamedConAlt'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__NamedConAlt'(V1, V2)) end end}.
'dn--un--__Impl_Show_NamedCExp'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__NamedCExp'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__NamedCExp'(V1, V2)) end end}.
'dn--un--__Impl_Show_CFType'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__CFType'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__CFType'(V1, V2)) end end}.
'dn--un--__Impl_Show_CDef'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__CDef'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__CDef'(V1, V2)) end end}.
'dn--un--__Impl_Show_(CExp $vars)'(V0) -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V1) -> ('dn--un--show_Show__(CExp $vars)'(V0, V1)) end, fun (V2) -> fun (V3) -> ('dn--un--showPrec_Show__(CExp $vars)'(V0, V2, V3)) end end}.
'un--uniqueName'(V0, V1, V2) -> ('case--uniqueName-922'('erased', V2, V1, ('un--elem'('erased', V1, V2)))).
'un--tryNext'(V0) -> case V0 of {'Idris.Core.Name.UN', E0} -> (fun (V1) -> {'Idris.Core.Name.MN', V1, 0} end(E0)); {'Idris.Core.Name.MN', E1, E2} -> (fun (V2, V3) -> {'Idris.Core.Name.MN', V2, ((1 + V3) rem 9223372036854775808)} end(E1, E2)); _ -> {'Idris.Core.Name.MN', ('Idris.Idris2.Core.Name':'un--nameRoot'(V0)), 0} end.
'un--substs'(V0, V1, V2, V3) -> ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V2, V3)).
'un--substEnv'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V6, V7) -> ('un--find'('erased', 'erased', 'erased', V7, V3, V6, V4)) end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V8, V9) -> {'Idris.Core.CompileExpr.CRef', V8, V9} end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V10, V11, V12) -> begin (V13 = ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V12))), {'Idris.Core.CompileExpr.CLam', V10, V11, V13} end end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V14, V15, V16, V17, V18) -> begin (V19 = ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V18))), {'Idris.Core.CompileExpr.CLet', V14, V15, V16, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V17)), V19} end end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V20, V21, V22) -> {'Idris.Core.CompileExpr.CApp', V20, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V21)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V23) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V23)) end, V22))} end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V24, V25, V26, V27) -> {'Idris.Core.CompileExpr.CCon', V24, V25, V26, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V28) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V28)) end, V27))} end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V29, V30, V31, V32) -> {'Idris.Core.CompileExpr.COp', V29, V30, V31, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V33) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V33)) end, V32))} end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V34, V35, V36) -> {'Idris.Core.CompileExpr.CExtPrim', V34, V35, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V37) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V37)) end, V36))} end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V38, V39) -> {'Idris.Core.CompileExpr.CForce', V38, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V39))} end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V40, V41) -> {'Idris.Core.CompileExpr.CDelay', V40, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V41))} end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V42, V43, V44, V45) -> {'Idris.Core.CompileExpr.CConCase', V42, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V43)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V46) -> ('un--substConAlt'('erased', 'erased', 'erased', V3, V4, V46)) end, V44)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V47) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V47)) end, V45))} end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V48, V49, V50, V51) -> {'Idris.Core.CompileExpr.CConstCase', V48, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V49)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V52) -> ('un--substConstAlt'('erased', 'erased', 'erased', V3, V4, V52)) end, V50)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V53) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V53)) end, V51))} end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V54, V55) -> {'Idris.Core.CompileExpr.CPrimVal', V54, V55} end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V56) -> {'Idris.Core.CompileExpr.CErased', V56} end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V57, V58) -> {'Idris.Core.CompileExpr.CCrash', V57, V58} end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--substConstAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V6, V7) -> {'Idris.Core.CompileExpr.MkConstAlt', V6, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V7))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--substConAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> {'Idris.Core.CompileExpr.MkConAlt', V6, V7, V8, ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--+'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V8)), V3)), V4, V9))} end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--shrinkConstAlt'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V4, V5) -> {'Idris.Core.CompileExpr.MkConstAlt', V4, ('un--shrinkCExp'('erased', 'erased', V2, V5))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--shrinkConAlt'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V4, V5, V6, V7) -> {'Idris.Core.CompileExpr.MkConAlt', V4, V5, V6, ('un--shrinkCExp'('erased', 'erased', ('Idris.Idris2.Core.TT':'un--subExtend'('erased', 'erased', V6, V2)), V7))} end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--shrinkCExp'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V4, V5) -> ('case--shrinkCExp-2010'('erased', 'erased', 'erased', V4, 'erased', V5, V2, ('Idris.Idris2.Core.TT':'un--subElem'('erased', 'erased', 'erased', V4, 'erased', V2)))) end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V6, V7) -> {'Idris.Core.CompileExpr.CRef', V6, V7} end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V8, V9, V10) -> begin (V11 = ('un--shrinkCExp'('erased', 'erased', {'Idris.Core.TT.KeepCons', V2}, V10))), {'Idris.Core.CompileExpr.CLam', V8, V9, V11} end end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V12, V13, V14, V15, V16) -> begin (V17 = ('un--shrinkCExp'('erased', 'erased', {'Idris.Core.TT.KeepCons', V2}, V16))), {'Idris.Core.CompileExpr.CLet', V12, V13, V14, ('un--shrinkCExp'('erased', 'erased', V2, V15)), V17} end end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V18, V19, V20) -> {'Idris.Core.CompileExpr.CApp', V18, ('un--shrinkCExp'('erased', 'erased', V2, V19)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V21) -> ('un--shrinkCExp'('erased', 'erased', V2, V21)) end, V20))} end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V22, V23, V24, V25) -> {'Idris.Core.CompileExpr.CCon', V22, V23, V24, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V26) -> ('un--shrinkCExp'('erased', 'erased', V2, V26)) end, V25))} end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V27, V28, V29, V30) -> {'Idris.Core.CompileExpr.COp', V27, V28, V29, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V31) -> ('un--shrinkCExp'('erased', 'erased', V2, V31)) end, V30))} end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V32, V33, V34) -> {'Idris.Core.CompileExpr.CExtPrim', V32, V33, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V35) -> ('un--shrinkCExp'('erased', 'erased', V2, V35)) end, V34))} end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V36, V37) -> {'Idris.Core.CompileExpr.CForce', V36, ('un--shrinkCExp'('erased', 'erased', V2, V37))} end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V38, V39) -> {'Idris.Core.CompileExpr.CDelay', V38, ('un--shrinkCExp'('erased', 'erased', V2, V39))} end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V40, V41, V42, V43) -> {'Idris.Core.CompileExpr.CConCase', V40, ('un--shrinkCExp'('erased', 'erased', V2, V41)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V44) -> ('un--shrinkConAlt'('erased', 'erased', V2, V44)) end, V42)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V45) -> ('un--shrinkCExp'('erased', 'erased', V2, V45)) end, V43))} end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V46, V47, V48, V49) -> {'Idris.Core.CompileExpr.CConstCase', V46, ('un--shrinkCExp'('erased', 'erased', V2, V47)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V50) -> ('un--shrinkConstAlt'('erased', 'erased', V2, V50)) end, V48)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V51) -> ('un--shrinkCExp'('erased', 'erased', V2, V51)) end, V49))} end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V52, V53) -> {'Idris.Core.CompileExpr.CPrimVal', V52, V53} end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V54) -> {'Idris.Core.CompileExpr.CErased', V54} end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V55, V56) -> {'Idris.Core.CompileExpr.CCrash', V55, V56} end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--resolveRef'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V6 of {'Idris.Core.TT.Bounds.None'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); {'Idris.Core.TT.Bounds.Add', E0, E1, E2} -> (fun (V9, V10, V11) -> ('case--resolveRef-2946'('erased', V11, V10, V9, V8, V7, 'erased', V5, 'erased', V4, 'erased', 'erased', ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V8, V10)))) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--refsToLocals'(V0, V1, V2, V3) -> case V2 of {'Idris.Core.TT.Bounds.None'} -> (fun () -> V3 end()); _ -> ('un--mkLocals'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V2, V3)) end.
'un--mkLocalsConstAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V6, V7) -> {'Idris.Core.CompileExpr.MkConstAlt', V6, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V7))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--mkLocalsConAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> begin (V10 = V9), {'Idris.Core.CompileExpr.MkConAlt', V6, V7, V8, ('un--mkLocals'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--+'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V8)), V3)), V4, V10))} end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--mkLocals'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V6, V7) -> ('case--mkLocals-3139'('erased', 'erased', 'erased', V6, 'erased', 'erased', V7, V4, V3, ('Idris.Idris2.Core.TT':'un--addVars'('erased', 'erased', 'erased', 'erased', V3, V4, V6)))) end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V8, V9) -> ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> {'Idris.Core.CompileExpr.CRef', V8, V9} end, fun () -> fun (V10) -> V10 end end, ('un--resolveRef'('erased', 'erased', 'erased', 'erased', V3, ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V4, V8, V9)))) end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V11, V12, V13) -> begin (V14 = ('un--mkLocals'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V13))), {'Idris.Core.CompileExpr.CLam', V11, V12, V14} end end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V15, V16, V17, V18, V19) -> begin (V20 = ('un--mkLocals'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V19))), {'Idris.Core.CompileExpr.CLet', V15, V16, V17, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V18)), V20} end end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V21, V22, V23) -> {'Idris.Core.CompileExpr.CApp', V21, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V22)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V24) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V24)) end, V23))} end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V25, V26, V27, V28) -> {'Idris.Core.CompileExpr.CCon', V25, V26, V27, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V29) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V29)) end, V28))} end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V30, V31, V32, V33) -> {'Idris.Core.CompileExpr.COp', V30, V31, V32, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V34) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V34)) end, V33))} end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V35, V36, V37) -> {'Idris.Core.CompileExpr.CExtPrim', V35, V36, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V38) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V38)) end, V37))} end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V39, V40) -> {'Idris.Core.CompileExpr.CForce', V39, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V40))} end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V41, V42) -> {'Idris.Core.CompileExpr.CDelay', V41, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V42))} end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V43, V44, V45, V46) -> {'Idris.Core.CompileExpr.CConCase', V43, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V44)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V47) -> ('un--mkLocalsConAlt'('erased', 'erased', 'erased', V3, V4, V47)) end, V45)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V48) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V48)) end, V46))} end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V49, V50, V51, V52) -> {'Idris.Core.CompileExpr.CConstCase', V49, ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V50)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V53) -> ('un--mkLocalsConstAlt'('erased', 'erased', 'erased', V3, V4, V53)) end, V51)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V54) -> ('un--mkLocals'('erased', 'erased', 'erased', V3, V4, V54)) end, V52))} end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V55, V56) -> {'Idris.Core.CompileExpr.CPrimVal', V55, V56} end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V57) -> {'Idris.Core.CompileExpr.CErased', V57} end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V58, V59) -> {'Idris.Core.CompileExpr.CCrash', V58, V59} end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--insertNamesConstAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V6, V7) -> {'Idris.Core.CompileExpr.MkConstAlt', V6, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V7))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--insertNamesConAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> begin (V10 = V9), {'Idris.Core.CompileExpr.MkConAlt', V6, V7, V8, ('un--insertNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--+'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--mkSizeOf'('erased', V8)), V3)), V4, V10))} end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--insertNames'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V6, V7) -> ('case--insertNames-1595'('erased', 'erased', 'erased', 'erased', V6, 'erased', V7, V4, V3, ('Idris.Idris2.Core.TT':'un--insertNVarNames'('erased', 'erased', 'erased', 'erased', V3, V4, V6)))) end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V8, V9) -> {'Idris.Core.CompileExpr.CRef', V8, V9} end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V10, V11, V12) -> begin (V13 = ('un--insertNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V12))), {'Idris.Core.CompileExpr.CLam', V10, V11, V13} end end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V14, V15, V16, V17, V18) -> begin (V19 = ('un--insertNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V18))), {'Idris.Core.CompileExpr.CLet', V14, V15, V16, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V17)), V19} end end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V20, V21, V22) -> {'Idris.Core.CompileExpr.CApp', V20, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V21)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V23) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V23)) end, V22))} end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V24, V25, V26, V27) -> {'Idris.Core.CompileExpr.CCon', V24, V25, V26, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V28) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V28)) end, V27))} end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V29, V30, V31, V32) -> {'Idris.Core.CompileExpr.COp', V29, V30, V31, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V33) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V33)) end, V32))} end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V34, V35, V36) -> {'Idris.Core.CompileExpr.CExtPrim', V34, V35, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V37) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V37)) end, V36))} end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V38, V39) -> {'Idris.Core.CompileExpr.CForce', V38, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V39))} end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V40, V41) -> {'Idris.Core.CompileExpr.CDelay', V40, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V41))} end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V42, V43, V44, V45) -> {'Idris.Core.CompileExpr.CConCase', V42, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V43)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V46) -> ('un--insertNamesConAlt'('erased', 'erased', 'erased', V3, V4, V46)) end, V44)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V47) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V47)) end, V45))} end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V48, V49, V50, V51) -> {'Idris.Core.CompileExpr.CConstCase', V48, ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V49)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V52) -> ('un--insertNamesConstAlt'('erased', 'erased', 'erased', V3, V4, V52)) end, V50)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V53) -> ('un--insertNames'('erased', 'erased', 'erased', V3, V4, V53)) end, V51))} end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V54, V55) -> {'Idris.Core.CompileExpr.CPrimVal', V54, V55} end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V56) -> {'Idris.Core.CompileExpr.CErased', V56} end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V57, V58) -> {'Idris.Core.CompileExpr.CCrash', V57, V58} end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getLocName'(V0, V1, V2, V3, V4) -> case V2 of 0 -> case V3 of {'Idris.Core.CompileExpr.::', E2, E3} -> (fun (V5, V6) -> V5 end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; _ -> begin (V7 = (V2 - 1)), case V3 of {'Idris.Core.CompileExpr.::', E0, E1} -> (fun (V8, V9) -> ('un--getLocName'('erased', 'erased', V7, V9, 'erased')) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end.
'un--getFC'(V0, V1) -> case V1 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V2, V3) -> V3 end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V4, V5) -> V4 end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V6, V7, V8) -> V6 end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V9, V10, V11, V12, V13) -> V9 end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V14, V15, V16) -> V14 end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V17, V18, V19, V20) -> V17 end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V21, V22, V23, V24) -> V22 end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V25, V26, V27) -> V25 end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V28, V29) -> V28 end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V30, V31) -> V30 end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V32, V33, V34, V35) -> V32 end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V36, V37, V38, V39) -> V36 end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V40, V41) -> V40 end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V42) -> V42 end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V43, V44) -> V43 end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--forgetExp'(V0, V1, V2) -> case V2 of {'Idris.Core.CompileExpr.CLocal', E0, E1} -> (fun (V3, V4) -> {'Idris.Core.CompileExpr.NmLocal', V4, ('un--getLocName'('erased', 'erased', V3, V1, 'erased'))} end(E0, E1)); {'Idris.Core.CompileExpr.CRef', E2, E3} -> (fun (V5, V6) -> {'Idris.Core.CompileExpr.NmRef', V5, V6} end(E2, E3)); {'Idris.Core.CompileExpr.CLam', E4, E5, E6} -> (fun (V7, V8, V9) -> begin (V10 = ('un--addLocs'('erased', [V8 | []], V1))), {'Idris.Core.CompileExpr.NmLam', V7, ('un--getLocName'('erased', 'erased', 0, V10, 'erased')), ('un--forgetExp'('erased', V10, V9))} end end(E4, E5, E6)); {'Idris.Core.CompileExpr.CLet', E7, E8, E9, E10, E11} -> (fun (V11, V12, V13, V14, V15) -> begin (V16 = ('un--addLocs'('erased', [V12 | []], V1))), {'Idris.Core.CompileExpr.NmLet', V11, ('un--getLocName'('erased', 'erased', 0, V16, 'erased')), ('un--forgetExp'('erased', V1, V14)), ('un--forgetExp'('erased', V16, V15))} end end(E7, E8, E9, E10, E11)); {'Idris.Core.CompileExpr.CApp', E12, E13, E14} -> (fun (V17, V18, V19) -> {'Idris.Core.CompileExpr.NmApp', V17, ('un--forgetExp'('erased', V1, V18)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V20) -> ('un--forgetExp'('erased', V1, V20)) end, V19))} end(E12, E13, E14)); {'Idris.Core.CompileExpr.CCon', E15, E16, E17, E18} -> (fun (V21, V22, V23, V24) -> {'Idris.Core.CompileExpr.NmCon', V21, V22, V23, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V25) -> ('un--forgetExp'('erased', V1, V25)) end, V24))} end(E15, E16, E17, E18)); {'Idris.Core.CompileExpr.COp', E19, E20, E21, E22} -> (fun (V26, V27, V28, V29) -> {'Idris.Core.CompileExpr.NmOp', V26, V27, V28, ('Idris.Idris2.Data.Vect':'dn--un--map_Functor__(Vect $n)'('erased', 'erased', 'erased', fun (V30) -> ('un--forgetExp'('erased', V1, V30)) end, V29))} end(E19, E20, E21, E22)); {'Idris.Core.CompileExpr.CExtPrim', E23, E24, E25} -> (fun (V31, V32, V33) -> {'Idris.Core.CompileExpr.NmExtPrim', V31, V32, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V34) -> ('un--forgetExp'('erased', V1, V34)) end, V33))} end(E23, E24, E25)); {'Idris.Core.CompileExpr.CForce', E26, E27} -> (fun (V35, V36) -> {'Idris.Core.CompileExpr.NmForce', V35, ('un--forgetExp'('erased', V1, V36))} end(E26, E27)); {'Idris.Core.CompileExpr.CDelay', E28, E29} -> (fun (V37, V38) -> {'Idris.Core.CompileExpr.NmDelay', V37, ('un--forgetExp'('erased', V1, V38))} end(E28, E29)); {'Idris.Core.CompileExpr.CConCase', E30, E31, E32, E33} -> (fun (V39, V40, V41, V42) -> {'Idris.Core.CompileExpr.NmConCase', V39, ('un--forgetExp'('erased', V1, V40)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V43) -> ('un--forgetConAlt'('erased', V1, V43)) end, V41)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V44) -> ('un--forgetExp'('erased', V1, V44)) end, V42))} end(E30, E31, E32, E33)); {'Idris.Core.CompileExpr.CConstCase', E34, E35, E36, E37} -> (fun (V45, V46, V47, V48) -> {'Idris.Core.CompileExpr.NmConstCase', V45, ('un--forgetExp'('erased', V1, V46)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V49) -> ('un--forgetConstAlt'('erased', V1, V49)) end, V47)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V50) -> ('un--forgetExp'('erased', V1, V50)) end, V48))} end(E34, E35, E36, E37)); {'Idris.Core.CompileExpr.CPrimVal', E38, E39} -> (fun (V51, V52) -> {'Idris.Core.CompileExpr.NmPrimVal', V51, V52} end(E38, E39)); {'Idris.Core.CompileExpr.CErased', E40} -> (fun (V53) -> {'Idris.Core.CompileExpr.NmErased', V53} end(E40)); {'Idris.Core.CompileExpr.CCrash', E41, E42} -> (fun (V54, V55) -> {'Idris.Core.CompileExpr.NmCrash', V54, V55} end(E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--forgetDef'(V0) -> case V0 of {'Idris.Core.CompileExpr.MkFun', E0, E1} -> (fun (V1, V2) -> begin (V3 = ('un--addLocs'('erased', V1, {'Idris.Core.CompileExpr.Nil'}))), begin (V4 = ('un--conArgs'('erased', V1, V3))), {'Idris.Core.CompileExpr.MkNmFun', V4, ('un--forget'(V1, V2))} end end end(E0, E1)); {'Idris.Core.CompileExpr.MkCon', E2, E3, E4} -> (fun (V5, V6, V7) -> {'Idris.Core.CompileExpr.MkNmCon', V5, V6, V7} end(E2, E3, E4)); {'Idris.Core.CompileExpr.MkForeign', E5, E6, E7} -> (fun (V8, V9, V10) -> {'Idris.Core.CompileExpr.MkNmForeign', V8, V9, V10} end(E5, E6, E7)); {'Idris.Core.CompileExpr.MkError', E8} -> (fun (V11) -> {'Idris.Core.CompileExpr.MkNmError', ('un--forget'([], V11))} end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--forgetConstAlt'(V0, V1, V2) -> case V2 of {'Idris.Core.CompileExpr.MkConstAlt', E0, E1} -> (fun (V3, V4) -> {'Idris.Core.CompileExpr.MkNConstAlt', V3, ('un--forgetExp'('erased', V1, V4))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--forgetConAlt'(V0, V1, V2) -> case V2 of {'Idris.Core.CompileExpr.MkConAlt', E0, E1, E2, E3} -> (fun (V3, V4, V5, V6) -> begin (V7 = ('un--addLocs'('erased', V5, V1))), {'Idris.Core.CompileExpr.MkNConAlt', V3, V4, ('un--conArgs'('erased', V5, V7)), ('un--forgetExp'('erased', V7, V6))} end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--forget'(V0, V1) -> ('un--forgetExp'('erased', ('un--addLocs'('erased', V0, {'Idris.Core.CompileExpr.Nil'})), V1)).
'un--findDrop'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.SubstCEnv.Nil'} -> (fun () -> {'Idris.Core.CompileExpr.CLocal', V3, V2} end()); _ -> case V3 of 0 -> case V4 of {'Idris.Core.CompileExpr.SubstCEnv.::', E2, E3} -> (fun (V5, V6) -> V5 end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; _ -> begin (V7 = (V3 - 1)), case V4 of {'Idris.Core.CompileExpr.SubstCEnv.::', E0, E1} -> (fun (V8, V9) -> ('un--findDrop'('erased', 'erased', V2, V7, V9)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end.
'un--find'(V0, V1, V2, V3, V4, V5, V6) -> ('case--find-2436'('erased', 'erased', 'erased', V6, V5, V4, V3, ('Idris.Idris2.Core.TT':'un--sizedView'('erased', 'erased', V4)))).
'un--embed'(V0, V1, V2) -> ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V2)).
'un--elem'(V0, V1, V2) -> case V2 of {'Idris.Core.CompileExpr.Nil'} -> (fun () -> 1 end()); {'Idris.Core.CompileExpr.::', E0, E1} -> (fun (V3, V4) -> ('Idris.Idris2.Prelude.Basics':'un--||'(('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V1, V3)), fun () -> ('un--elem'('erased', V1, V4)) end)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--conArgs'(V0, V1, V2) -> case V1 of [] -> []; [E0 | E1] -> (fun (V3, V4) -> case V2 of {'Idris.Core.CompileExpr.::', E2, E3} -> (fun (V5, V6) -> [V5 | ('un--conArgs'('erased', V4, V6))] end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--addLocs'(V0, V1, V2) -> case V1 of [] -> V2; [E0 | E1] -> (fun (V3, V4) -> begin (V5 = ('un--addLocs'('erased', V4, V2))), {'Idris.Core.CompileExpr.::', ('un--uniqueName'('erased', V3, V5)), V5} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.