Current section
Files
Jump to
Current section
Files
src/Idris.Idris2.Compiler.Erlang.Erlang.erl
-module('Idris.Idris2.Compiler.Erlang.Erlang').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
'case--build-3915'/9,
'case--genCompdef-3628'/6,
'case--writeErlangModule-3538'/13,
'case--writeErlangModule-3446'/18,
'case--writeErlangModule-3329'/9,
'case--genExports-3262'/5,
'case--case block in getCompileExpr-3195'/6,
'case--getCompileExpr-3183'/4,
'nested--11416-3796--in--un--shouldCompileName'/6,
'un--writeErlangModule'/7,
'un--splitNamespaceInfo'/3,
'un--groupBy'/7,
'un--getExportFunNames'/1,
'un--getCompileExpr'/3,
'un--genExports'/5,
'un--genDeclErl'/1,
'un--genDeclAbstr'/1,
'un--genCompdef'/2,
'un--findErlangExecutable'/1,
'un--findErlangCompiler'/1,
'un--executeExpr'/3,
'un--defsPerModule'/2,
'un--defLine'/0,
'un--concatNamespaceInfo'/3,
'un--compileMainEntrypointToModules'/5,
'un--compileLibraryToModules'/4,
'un--compileLibrary'/6,
'un--compileExpr'/6,
'un--codegenErlang'/0,
'un--build'/7
]).
'case--build-3915'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Compiler.Erlang.GlobalOpts.ErlangSource'} -> (fun () -> ('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V9) -> ('un--writeErlangModule'(V5, V4, V3, V1, <<"erl"/utf8>>, fun (V10) -> ('un--genDeclErl'(V10)) end, V9)) end, V0)) end()); {'Idris.Compiler.Erlang.GlobalOpts.ErlangSourcePretty'} -> (fun () -> fun (V11) -> begin (V14 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V12) -> ('un--writeErlangModule'(V5, V4, V3, V2, <<"abstr"/utf8>>, fun (V13) -> ('un--genDeclAbstr'(V13)) end, V12)) end, V0))(V11))), case V14 of {'Idris.Prelude.Types.Left', E0} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V16) -> begin (V45 = begin (V44 = (('Idris.Idris2.Erlang.System':'un--system'('erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V19, V20, V21)) end end end end end, fun (V22) -> fun (V23) -> fun (V24) -> V23 end end end, fun (V25) -> fun (V26) -> fun (V27) -> fun (V28) -> fun (V29) -> begin (V30 = (V27(V29))), begin (V31 = (V28(V29))), (V30(V31)) end end end end end end end}, fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> fun (V36) -> begin (V37 = (V34(V36))), ((V35(V37))(V36)) end end end end end end, fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V39(V40))), (V41(V40)) end end end end}, fun (V42) -> fun (V43) -> V43 end end}, ('Idris.Idris2.Compiler.Erlang.Cmd':'un--compileAbstrToErlCmd'(1, V6, V16, V1))))(V11))), {'Idris.Prelude.Types.Right', V44} end), case V45 of {'Idris.Prelude.Types.Left', E2} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V47) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.Compiler.Erlang.GlobalOpts.AbstractFormat'} -> (fun () -> ('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V48) -> ('un--writeErlangModule'(V5, V4, V3, V1, <<"abstr"/utf8>>, fun (V49) -> ('un--genDeclAbstr'(V49)) end, V48)) end, V0)) end()); {'Idris.Compiler.Erlang.GlobalOpts.BeamFromErlangSource'} -> (fun () -> fun (V50) -> begin (V53 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V51) -> ('un--writeErlangModule'(V5, V4, V3, V2, <<"erl"/utf8>>, fun (V52) -> ('un--genDeclErl'(V52)) end, V51)) end, V0))(V50))), case V53 of {'Idris.Prelude.Types.Left', E4} -> (fun (V54) -> {'Idris.Prelude.Types.Left', V54} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V55) -> begin (V84 = begin (V83 = (('Idris.Idris2.Erlang.System':'un--system'('erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V56) -> fun (V57) -> fun (V58) -> fun (V59) -> fun (V60) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V58, V59, V60)) end end end end end, fun (V61) -> fun (V62) -> fun (V63) -> V62 end end end, fun (V64) -> fun (V65) -> fun (V66) -> fun (V67) -> fun (V68) -> begin (V69 = (V66(V68))), begin (V70 = (V67(V68))), (V69(V70)) end end end end end end end}, fun (V71) -> fun (V72) -> fun (V73) -> fun (V74) -> fun (V75) -> begin (V76 = (V73(V75))), ((V74(V76))(V75)) end end end end end end, fun (V77) -> fun (V78) -> fun (V79) -> begin (V80 = (V78(V79))), (V80(V79)) end end end end}, fun (V81) -> fun (V82) -> V82 end end}, ('Idris.Idris2.Compiler.Erlang.Cmd':'un--compileErlToBeamCmd'(V7, V55, V1))))(V50))), {'Idris.Prelude.Types.Right', V83} end), case V84 of {'Idris.Prelude.Types.Left', E6} -> (fun (V85) -> {'Idris.Prelude.Types.Left', V85} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V86) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.Compiler.Erlang.GlobalOpts.BeamFromAbstractFormat'} -> (fun () -> fun (V87) -> begin (V90 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V88) -> ('un--writeErlangModule'(V5, V4, V3, V2, <<"abstr"/utf8>>, fun (V89) -> ('un--genDeclAbstr'(V89)) end, V88)) end, V0))(V87))), case V90 of {'Idris.Prelude.Types.Left', E8} -> (fun (V91) -> {'Idris.Prelude.Types.Left', V91} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V92) -> begin (V121 = begin (V120 = (('Idris.Idris2.Erlang.System':'un--system'('erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V93) -> fun (V94) -> fun (V95) -> fun (V96) -> fun (V97) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V95, V96, V97)) end end end end end, fun (V98) -> fun (V99) -> fun (V100) -> V99 end end end, fun (V101) -> fun (V102) -> fun (V103) -> fun (V104) -> fun (V105) -> begin (V106 = (V103(V105))), begin (V107 = (V104(V105))), (V106(V107)) end end end end end end end}, fun (V108) -> fun (V109) -> fun (V110) -> fun (V111) -> fun (V112) -> begin (V113 = (V110(V112))), ((V111(V113))(V112)) end end end end end end, fun (V114) -> fun (V115) -> fun (V116) -> begin (V117 = (V115(V116))), (V117(V116)) end end end end}, fun (V118) -> fun (V119) -> V119 end end}, ('Idris.Idris2.Compiler.Erlang.Cmd':'un--compileAbstrToBeamCmd'(V6, V92, V1))))(V87))), {'Idris.Prelude.Types.Right', V120} end), case V121 of {'Idris.Prelude.Types.Left', E10} -> (fun (V122) -> {'Idris.Prelude.Types.Left', V122} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V123) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--genCompdef-3628'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V0, V6}}} end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V8) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--writeErlangModule-3538'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of 0 -> [{'Idris.Compiler.Erlang.IR.ErlExpr.Inline', ('un--defLine'())} | [{'Idris.Compiler.Erlang.IR.ErlExpr.InlineSize', ('un--defLine'()), case V6 of {'Idris.Compiler.Erlang.GlobalOpts.MkGlobalOpts', E0, E1, E2} -> (fun (V13, V14, V15) -> V15 end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end} | []]]; 1 -> []; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--writeErlangModule-3446'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of {'Idris.Prelude.Types.Right', E0} -> (fun (V18) -> case V18 of {'Idris.Builtin.MkUnit'} -> (fun () -> fun (V19) -> {'Idris.Prelude.Types.Right', V14} end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Left', E1} -> (fun (V20) -> fun (V21) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.FileErr', V14, V20}, V21)) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--writeErlangModule-3329'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Compiler.Erlang.Name.Concat', E0} -> (fun (V9) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Compiler.Erlang.Name.Split', E1, E2} -> (fun (V10, V11) -> ('Idris.Idris2.Data.List':'un--find'('erased', fun (V12) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--==_Eq__Namespace'(case V12 of {'Idris.Compiler.Erlang.ModuleOpts.MkModuleOpts', E3, E4, E5} -> (fun (V13, V14, V15) -> V13 end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V11)) end, V5)) end(E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--genExports-3262'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.CompileExpr.MkNmFun', E0, E1} -> (fun (V5, V6) -> case V5 of [] -> ('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr':'un--readExports'(V2, V1, V6)); _ -> fun (V7) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expected function definition for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V0))))}, V7)) end end end(E0, E1)); _ -> fun (V8) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expected function definition for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V0))))}, V8)) end end.
'case--case block in getCompileExpr-3195'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V8) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"No compiled definition for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V0))))}, V8)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--getCompileExpr-3183'(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 getCompileExpr-3195'(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) -> V25 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.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Compiling undefined name "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V0))))}, V27)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--11416-3796--in--un--shouldCompileName'(V0, V1, V2, V3, V4, V5) -> case V4 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> 0 end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> begin (V8 = ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V7) -> ('Idris.Idris2.Core.Name.Namespace':'un--miAsNamespace'(V7)) end, V6))), (('Idris.Idris2.Prelude.Interfaces':'un--any'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkFoldable', fun (V9) -> fun (V10) -> fun (V11) -> fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', V11, V12, V13)) end end end end end, fun (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldl_Foldable__List'('erased', 'erased', V16, V17, V18)) end end end end end}, fun (V19) -> ('Idris.Idris2.Core.Name.Namespace':'un--isParentOf'(V19, ('Idris.Idris2.Compiler.Erlang.Name':'un--getNamespace'(V5)))) end))(V8)) end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--writeErlangModule'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V7, V8) -> begin (V9 = ('case--writeErlangModule-3329'(V7, V8, V5, V4, V3, V2, V1, V0, V7))), fun (V10) -> begin (V18 = (('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> fun (V11) -> {'Idris.Prelude.Types.Right', []} end end, fun () -> fun (V12) -> fun (V13) -> ('un--genExports'(V0, V7, ('un--defLine'()), V12, V13)) end end end, ('Idris.Idris2.Prelude.Types':'dn--un-->>=_Monad__Maybe'('erased', 'erased', V9, fun (V14) -> case V14 of {'Idris.Compiler.Erlang.ModuleOpts.MkModuleOpts', E2, E3, E4} -> (fun (V15, V16, V17) -> V16 end(E2, E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end))))(V10))), case V18 of {'Idris.Prelude.Types.Left', E5} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V20) -> begin (V21 = ('Idris.Idris2.Compiler.Erlang.Name':'un--currentModuleName'(V7))), begin (V26 = ('Idris.Idris2.Prelude.Types':'dn--un-->>=_Monad__Maybe'('erased', 'erased', V9, fun (V22) -> case V22 of {'Idris.Compiler.Erlang.ModuleOpts.MkModuleOpts', E7, E8, E9} -> (fun (V23, V24, V25) -> V25 end(E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end))), begin (V30 = ('case--writeErlangModule-3538'(V7, V8, V5, V4, V3, V2, V1, V0, V9, V20, V21, V26, ('Idris.Idris2.Prelude.Types':'dn--un-->_Ord__Nat'(('Idris.Idris2.Data.Maybe':'un--fromMaybe'('erased', fun () -> case V1 of {'Idris.Compiler.Erlang.GlobalOpts.MkGlobalOpts', E10, E11, E12} -> (fun (V27, V28, V29) -> V29 end(E10, E11, E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, V26)), 0))))), begin (V31 = {'Idris.Compiler.Erlang.IR.ErlExpr.MkModule', {'Idris.Compiler.Erlang.IR.ErlExpr.MkModuleName', ('un--defLine'()), V21}, [{'Idris.Compiler.Erlang.IR.ErlExpr.NoAutoImport', ('un--defLine'())} | V30], ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V20, V8))}), begin (V32 = ('Idris.Idris2.Utils.Path':'un--</>'(V3, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(V21, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"."/utf8>>, V4))))))), begin (V33 = ('Idris.Idris2.Compiler.Erlang.Codegen.ErlExprToAbstractFormat':'un--genErlModule'(('un--defLine'()), V31))), begin (V34 = ('Idris.Idris2.Data.Strings':'un--fastAppend'(('Idris.Idris2.Compiler.Erlang.Utils.CompositeString':'un--flatten'({'Idris.Compiler.Erlang.Utils.CompositeString.Nested', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', V5, V33))}))))), begin (V63 = begin (V62 = (('Idris.Idris2.Erlang.System.File':'un--writeFile'('erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V35) -> fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V37, V38, V39)) end end end end end, fun (V40) -> fun (V41) -> fun (V42) -> V41 end end end, fun (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> begin (V48 = (V45(V47))), begin (V49 = (V46(V47))), (V48(V49)) end end end end end end end}, fun (V50) -> fun (V51) -> fun (V52) -> fun (V53) -> fun (V54) -> begin (V55 = (V52(V54))), ((V53(V55))(V54)) end end end end end end, fun (V56) -> fun (V57) -> fun (V58) -> begin (V59 = (V57(V58))), (V59(V58)) end end end end}, fun (V60) -> fun (V61) -> V61 end end}, V32, V34))(V10))), {'Idris.Prelude.Types.Right', V62} end), case V63 of {'Idris.Prelude.Types.Left', E13} -> (fun (V64) -> {'Idris.Prelude.Types.Left', V64} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V65) -> case V65 of {'Idris.Prelude.Types.Right', E15} -> (fun (V66) -> case V66 of {'Idris.Builtin.MkUnit'} -> (fun () -> {'Idris.Prelude.Types.Right', V32} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E15)); {'Idris.Prelude.Types.Left', E16} -> (fun (V67) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.FileErr', V32, V67}, V10)) end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end end end end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--splitNamespaceInfo'(V0, V1, V2) -> case V2 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V3, V4) -> begin (V5 = ('Idris.Idris2.Compiler.Erlang.Name':'un--getNamespace'(V3))), {'Idris.Builtin.MkPair', {'Idris.Compiler.Erlang.Name.Split', V1, V5}, V2} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--groupBy'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of [] -> ('Idris.Idris2.Data.SortedMap':'un--empty'('erased', 'erased', V3)); [E0 | E1] -> (fun (V7, V8) -> ('Idris.Idris2.Data.SortedMap':'dn--un--<+>_Semigroup__((SortedMap $k) $v)'('erased', 'erased', fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.Types':'dn--un--<+>_Semigroup__(List $a)'('erased', V9, V10)) end end, ('Idris.Idris2.Data.SortedMap':'un--singleton'('erased', 'erased', V3, (V4(V7)), [(V5(V7)) | []])), ('un--groupBy'('erased', 'erased', 'erased', V3, V4, V5, V8)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getExportFunNames'(V0) -> ('Idris.Idris2.Data.List':'un--mapMaybe'('erased', 'erased', fun (V1) -> ('Idris.Idris2.Prelude.Interfaces':'un--<$>'('erased', 'erased', 'erased', fun (V2) -> fun (V3) -> fun (V4) -> fun (V5) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', V4, V5)) end end end end, fun (V6) -> {'Idris.Builtin.MkPair', case V1 of {'Idris.Compiler.Erlang.ModuleOpts.MkModuleOpts', E0, E1, E2} -> (fun (V7, V8, V9) -> V7 end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V6} end, case V1 of {'Idris.Compiler.Erlang.ModuleOpts.MkModuleOpts', E3, E4, E5} -> (fun (V10, V11, V12) -> V11 end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end, V0)).
'un--getCompileExpr'(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 getCompileExpr-3195'(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) -> V84 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.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Compiling undefined name "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V1))))}, V2)) 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--genExports'(V0, V1, V2, V3, V4) -> begin (V5 = ('un--getCompileExpr'(V0, V3, 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) -> case V7 of {'Idris.Core.CompileExpr.MkNmFun', E2, E3} -> (fun (V8, V9) -> case V8 of [] -> (('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr':'un--readExports'(V1, V2, V9))(V4)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expected function definition for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3))))}, V4)) end end(E2, E3)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.InternalError', ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expected function definition for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3))))}, V4)) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--genDeclErl'(V0) -> {'Idris.Compiler.Erlang.Utils.CompositeString.Nested', [('Idris.Idris2.Compiler.Erlang.Codegen.AbstractFormatToErlangSource':'un--genDecl'(V0)) | [{'Idris.Compiler.Erlang.Utils.CompositeString.Str', <<"\x{a}"/utf8>>} | []]]}.
'un--genDeclAbstr'(V0) -> {'Idris.Compiler.Erlang.Utils.CompositeString.Nested', [('Idris.Idris2.Compiler.Erlang.Utils.PrimTerm':'un--primTermToCS'(('Idris.Idris2.Compiler.Erlang.Codegen.AbstractFormatToPrimTerm':'un--genDecl'(V0)))) | [{'Idris.Compiler.Erlang.Utils.CompositeString.Str', <<".\x{a}"/utf8>>} | []]]}.
'un--genCompdef'(V0, V1) -> case V1 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V2, V3) -> case V3 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V4, V5) -> case V5 of {'Idris.Builtin.MkPair', E4, E5} -> (fun (V6, V7) -> fun (V8) -> begin (V9 = (('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr':'un--genDef'(V2, V0, V4, V7))(V8))), case V9 of {'Idris.Prelude.Types.Left', E6} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V11) -> case V11 of {'Idris.Prelude.Types.Just', E8} -> (fun (V12) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V2, V12}}} end(E8)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5)); _ -> ('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--findErlangExecutable'(V0) -> <<"erl"/utf8>>.
'un--findErlangCompiler'(V0) -> <<"erlc"/utf8>>.
'un--executeExpr'(V0, V1, V2) -> begin (V3 = ('Idris.Idris2.Compiler.Erlang.GlobalOpts':'un--defaultGlobalOpts'())), begin (V4 = <<"main"/utf8>>), fun (V5) -> begin (V6 = ('un--compileMainEntrypointToModules'(V0, V3, V2, V4, V5))), case V6 of {'Idris.Prelude.Types.Left', E0} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V8) -> begin (V9 = ('un--build'(V0, V3, [], V1, V1, V8, V5))), case V9 of {'Idris.Prelude.Types.Left', E2} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V11) -> begin (V13 = begin (V12 = ('un--findErlangExecutable'(V5))), {'Idris.Prelude.Types.Right', V12} end), case V13 of {'Idris.Prelude.Types.Left', E4} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V15) -> begin (V44 = begin (V43 = (('Idris.Idris2.Erlang.System':'un--system'('erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V18, V19, V20)) end end end end end, fun (V21) -> fun (V22) -> fun (V23) -> V22 end end end, fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> fun (V28) -> begin (V29 = (V26(V28))), begin (V30 = (V27(V28))), (V29(V30)) end end end end end end end}, fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> begin (V36 = (V33(V35))), ((V34(V36))(V35)) end end end end end end, fun (V37) -> fun (V38) -> fun (V39) -> begin (V40 = (V38(V39))), (V40(V39)) end end end end}, fun (V41) -> fun (V42) -> V42 end end}, ('Idris.Idris2.Compiler.Erlang.Cmd':'un--executeBeamCmd'(V15, V1, V4))))(V5))), {'Idris.Prelude.Types.Right', V43} end), case V44 of {'Idris.Prelude.Types.Left', E6} -> (fun (V45) -> {'Idris.Prelude.Types.Left', V45} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V46) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} 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 end end end.
'un--defsPerModule'(V0, V1) -> ('Idris.Idris2.Data.SortedMap':'un--toList'('erased', 'erased', ('un--groupBy'('erased', 'erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V2) -> fun (V3) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--==_Eq__NamespaceInfo'(V2, V3)) end end, fun (V4) -> fun (V5) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--/=_Eq__NamespaceInfo'(V4, V5)) end end}, fun (V6) -> fun (V7) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--compare_Ord__NamespaceInfo'(V6, V7)) end end, fun (V8) -> fun (V9) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--<_Ord__NamespaceInfo'(V8, V9)) end end, fun (V10) -> fun (V11) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un-->_Ord__NamespaceInfo'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--<=_Ord__NamespaceInfo'(V12, V13)) end end, fun (V14) -> fun (V15) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un-->=_Ord__NamespaceInfo'(V14, V15)) end end, fun (V16) -> fun (V17) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--max_Ord__NamespaceInfo'(V16, V17)) end end, fun (V18) -> fun (V19) -> ('Idris.Idris2.Compiler.Erlang.Name':'dn--un--min_Ord__NamespaceInfo'(V18, V19)) end end}, fun (V20) -> ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V20)) end, fun (V21) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V21)) end, V1)))).
'un--defLine'() -> 4242.
'un--concatNamespaceInfo'(V0, V1, V2) -> {'Idris.Builtin.MkPair', {'Idris.Compiler.Erlang.Name.Concat', V1}, V2}.
'un--compileMainEntrypointToModules'(V0, V1, V2, V3, V4) -> begin (V5 = ('Idris.Idris2.Compiler.Common':'un--getCompileData'(V0, {'Idris.Compiler.Common.Cases'}, V2, 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 (V14 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V8) -> ('un--genCompdef'(('un--defLine'()), ('un--concatNamespaceInfo'('erased', V3, V8)))) end, case V7 of {'Idris.Compiler.Common.MkCompileData', E2, E3, E4, E5, E6} -> (fun (V9, V10, V11, V12, V13) -> V10 end(E2, E3, E4, E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V4))), case V14 of {'Idris.Prelude.Types.Left', E7} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V16) -> begin (V17 = {'Idris.Compiler.Erlang.Name.Concat', V3}), begin (V18 = ('Idris.Idris2.Core.Core':'un--newRef'('erased', 'erased', {'Idris.Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport.LV'}, ('Idris.Idris2.Compiler.Erlang.IR.ErlExpr.LocalVars':'un--initLocalVars'(<<"V"/utf8>>)), V4))), case V18 of {'Idris.Prelude.Types.Left', E9} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V20) -> begin (V26 = (('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr':'un--genNmExp'(V20, V17, ('Idris.Idris2.Data.NameMap':'un--empty'('erased')), ('Idris.Idris2.Core.CompileExpr':'un--forget'([], case V7 of {'Idris.Compiler.Common.MkCompileData', E11, E12, E13, E14, E15} -> (fun (V21, V22, V23, V24, V25) -> V21 end(E11, E12, E13, E14, E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))))(V4))), case V26 of {'Idris.Prelude.Types.Left', E16} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V28) -> begin (V29 = ('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport':'un--newLocalVar'(V20, V4))), case V29 of {'Idris.Prelude.Types.Left', E18} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E18)); {'Idris.Prelude.Types.Right', E19} -> (fun (V31) -> begin (V32 = (('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport':'un--genErlMain'(V20, ('un--defLine'()), V28))(V4))), case V32 of {'Idris.Prelude.Types.Left', E20} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E20)); {'Idris.Prelude.Types.Right', E21} -> (fun (V34) -> begin (V35 = {'Idris.Compiler.Erlang.IR.ErlExpr.MkFunDecl', ('un--defLine'()), {'Idris.Compiler.Erlang.IR.ErlExpr.Public'}, <<"start"/utf8>>, [], V34}), begin (V36 = {'Idris.Compiler.Erlang.IR.ErlExpr.MkFunDecl', ('un--defLine'()), {'Idris.Compiler.Erlang.IR.ErlExpr.Public'}, <<"main"/utf8>>, [V31 | []], ('Idris.Idris2.Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport':'un--genEscriptMain'(('un--defLine'()), V28))}), begin (V38 = [{'Idris.Builtin.MkPair', V17, V35} | [{'Idris.Builtin.MkPair', V17, V36} | ('Idris.Idris2.Data.List':'un--mapMaybe'('erased', 'erased', fun (V37) -> V37 end, V16))]]), {'Idris.Prelude.Types.Right', ('un--defsPerModule'('erased', V38))} end end end end(E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E19)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--compileLibraryToModules'(V0, V1, V2, V3) -> begin (V6 = ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V4) -> ('nested--11416-3796--in--un--shouldCompileName'(V3, V2, V1, V0, V3, V4)) end, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V5) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V5)) end, ('un--getExportFunNames'(V2))))))), fun (V7) -> begin (V9 = ('Idris.Idris2.Compiler.Common':'un--getExportedCompileData'(V0, {'Idris.Compiler.Common.Cases'}, fun (V8) -> ('nested--11416-3796--in--un--shouldCompileName'(V3, V2, V1, V0, V3, V8)) end, V6, V7))), case V9 of {'Idris.Prelude.Types.Left', E0} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V11) -> begin (V22 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V12) -> ('un--genCompdef'(('un--defLine'()), ('un--splitNamespaceInfo'('erased', case V1 of {'Idris.Compiler.Erlang.GlobalOpts.MkGlobalOpts', E2, E3, E4} -> (fun (V13, V14, V15) -> V14 end(E2, E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V12)))) end, ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V16) -> ('nested--11416-3796--in--un--shouldCompileName'(V3, V2, V1, V0, V3, ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V16)))) end, case V11 of {'Idris.Compiler.Common.MkCompileData', E5, E6, E7, E8, E9} -> (fun (V17, V18, V19, V20, V21) -> V18 end(E5, E6, E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))))(V7))), case V22 of {'Idris.Prelude.Types.Left', E10} -> (fun (V23) -> {'Idris.Prelude.Types.Left', V23} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V24) -> begin (V26 = ('Idris.Idris2.Data.List':'un--mapMaybe'('erased', 'erased', fun (V25) -> V25 end, V24))), {'Idris.Prelude.Types.Right', ('un--defsPerModule'('erased', V26))} end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end.
'un--compileLibrary'(V0, V1, V2, V3, V4, V5) -> begin (V6 = ('Idris.Idris2.Core.Context':'un--getDirectives'(V0, {'Idris.Core.Options.Other', <<"erlang"/utf8>>}, V5))), case V6 of {'Idris.Prelude.Types.Left', E0} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V8) -> begin (V29 = ('un--groupBy'('erased', 'erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--==_Eq__Namespace'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--/=_Eq__Namespace'(V11, V12)) end end}, fun (V13) -> fun (V14) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--compare_Ord__Namespace'(V13, V14)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--<_Ord__Namespace'(V15, V16)) end end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un-->_Ord__Namespace'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--<=_Ord__Namespace'(V19, V20)) end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un-->=_Ord__Namespace'(V21, V22)) end end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--max_Ord__Namespace'(V23, V24)) end end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--min_Ord__Namespace'(V25, V26)) end end}, fun (V27) -> ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V27)) end, fun (V28) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V28)) end, V8))), begin (V30 = ('Idris.Idris2.Data.Maybe':'un--fromMaybe'('erased', fun () -> [] end, ('Idris.Idris2.Data.SortedMap':'un--lookup'('erased', 'erased', ('Idris.Idris2.Core.Name.Namespace':'un--emptyNS'()), V29))))), begin (V31 = ('Idris.Idris2.Data.SortedMap':'un--toList'('erased', 'erased', ('Idris.Idris2.Data.SortedMap':'un--delete'('erased', 'erased', ('Idris.Idris2.Core.Name.Namespace':'un--emptyNS'()), V29))))), begin (V35 = ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V32) -> ('Idris.Idris2.Prelude.Basics':'un--uncurry'('erased', 'erased', 'erased', fun (V33) -> fun (V34) -> ('Idris.Idris2.Compiler.Erlang.ModuleOpts':'un--parseModuleOpts'(V33, V34)) end end, V32)) end, V31))), begin (V36 = ('Idris.Idris2.Compiler.Erlang.GlobalOpts':'un--parseOpts'(V30))), begin (V37 = (('un--compileLibraryToModules'(V0, V36, V35, V4))(V5))), case V37 of {'Idris.Prelude.Types.Left', E2} -> (fun (V38) -> {'Idris.Prelude.Types.Left', V38} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V39) -> begin (V40 = ('un--build'(V0, V36, V35, V1, V2, V39, V5))), case V40 of {'Idris.Prelude.Types.Left', E4} -> (fun (V41) -> {'Idris.Prelude.Types.Left', V41} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V42) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V3, V42}}} end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--compileExpr'(V0, V1, V2, V3, V4, V5) -> begin (V6 = ('Idris.Idris2.Core.Context':'un--getDirectives'(V0, {'Idris.Core.Options.Other', <<"erlang"/utf8>>}, V5))), case V6 of {'Idris.Prelude.Types.Left', E0} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V8) -> begin (V29 = ('un--groupBy'('erased', 'erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--==_Eq__Namespace'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--/=_Eq__Namespace'(V11, V12)) end end}, fun (V13) -> fun (V14) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--compare_Ord__Namespace'(V13, V14)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--<_Ord__Namespace'(V15, V16)) end end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un-->_Ord__Namespace'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--<=_Ord__Namespace'(V19, V20)) end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un-->=_Ord__Namespace'(V21, V22)) end end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--max_Ord__Namespace'(V23, V24)) end end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--min_Ord__Namespace'(V25, V26)) end end}, fun (V27) -> ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V27)) end, fun (V28) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V28)) end, V8))), begin (V30 = ('Idris.Idris2.Data.Maybe':'un--fromMaybe'('erased', fun () -> [] end, ('Idris.Idris2.Data.SortedMap':'un--lookup'('erased', 'erased', ('Idris.Idris2.Core.Name.Namespace':'un--emptyNS'()), V29))))), begin (V31 = ('Idris.Idris2.Compiler.Erlang.GlobalOpts':'un--parseOpts'(V30))), begin (V32 = V4), begin (V33 = ('un--compileMainEntrypointToModules'(V0, V31, V3, V32, V5))), case V33 of {'Idris.Prelude.Types.Left', E2} -> (fun (V34) -> {'Idris.Prelude.Types.Left', V34} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V35) -> begin (V36 = ('un--build'(V0, V31, [], V1, V2, V35, V5))), case V36 of {'Idris.Prelude.Types.Left', E4} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V38) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V4}} end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--codegenErlang'() -> {'Idris.Compiler.Common.MkCG', fun (V0) -> fun (V1) -> fun (V2) -> fun (V3) -> fun (V4) -> fun (V5) -> ('un--compileExpr'(V0, V1, V2, V3, V4, V5)) end end end end end end, fun (V6) -> fun (V7) -> fun (V8) -> ('un--executeExpr'(V6, V7, V8)) end end end, fun (V9) -> fun (V10) -> fun (V11) -> fun (V12) -> fun (V13) -> fun (V14) -> ('un--compileLibrary'(V9, V10, V11, V12, V13, V14)) end end end end end end}.
'un--build'(V0, V1, V2, V3, V4, V5, V6) -> begin (V8 = begin (V7 = ('un--findErlangExecutable'(V6))), {'Idris.Prelude.Types.Right', V7} end), case V8 of {'Idris.Prelude.Types.Left', E0} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V10) -> begin (V12 = begin (V11 = ('un--findErlangCompiler'(V6))), {'Idris.Prelude.Types.Right', V11} end), case V12 of {'Idris.Prelude.Types.Left', E2} -> (fun (V13) -> {'Idris.Prelude.Types.Left', V13} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V14) -> begin (V18 = (('case--build-3915'(V5, V4, V3, V2, V1, V0, V10, V14, case V1 of {'Idris.Compiler.Erlang.GlobalOpts.MkGlobalOpts', E4, E5, E6} -> (fun (V15, V16, V17) -> V15 end(E4, E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V6))), case V18 of {'Idris.Prelude.Types.Left', E7} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V20) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V21) -> ('Idris.Idris2.Compiler.Erlang.Name':'un--currentModuleName'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V21)))) end, V5))} end(E8)); _ -> ('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.