Packages

idris2

0.2.1-alpha.1
0.2.1-alpha.1

Erlang code generator for Idris 2

Current section

Files

Jump to
Readme
1 Version
0 Dependencies
Dependants
Files
Activity
idris2 src Idris.Idris2.Erlang.System.Concurrency.erl
Raw

src/Idris.Idris2.Erlang.System.Concurrency.erl 

-module('Idris.Idris2.Erlang.System.Concurrency').

-compile('no_auto_import').

-compile('inline').

-compile({'inline_size',24}).

-export([

  'case--erlReceive-1179'/7,

  'un--prim__erlReceive'/2,

  'un--erlSpawnLink'/3,

  'un--erlSpawn'/3,

  'un--erlSend'/5,

  'un--erlSelf'/2,

  'un--erlReceive'/6

]).

'case--erlReceive-1179'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Prelude.Types.Just', E0} -> (fun (V7) -> case case case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E7, E8} -> (fun (V8, V9) -> V8 end(E7, E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E4, E5, E6} -> (fun (V10, V11, V12) -> V10 end(E4, E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E1, E2, E3} -> (fun (V13, V14, V15) -> ((V14('erased'))(('Idris.Idris2.Erlang.Decode':'un--erlDecodeDef'('erased', 'erased', {'Idris.Erlang.Types.ETErlTerm'}, fun () -> V4 end, V3, V7)))) end(E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> case case case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E15, E16} -> (fun (V16, V17) -> V16 end(E15, E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E12, E13, E14} -> (fun (V18, V19, V20) -> V18 end(E12, E13, E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E9, E10, E11} -> (fun (V21, V22, V23) -> ((V22('erased'))(V4)) end(E9, E10, E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--prim__erlReceive'(V0, V1) -> receive E0 -> (fun (V2) -> {'Idris.Prelude.Types.Just', V2} end(E0)) after V0 -> {'Idris.Prelude.Types.Nothing'} end.

'un--erlSpawnLink'(V0, V1, V2) -> case case case V1 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E6, E7} -> (fun (V3, V4) -> V3 end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E3, E4, E5} -> (fun (V5, V6, V7) -> V5 end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E0, E1, E2} -> (fun (V8, V9, V10) -> ((V9('erased'))(('erlang':'apply'('erlang', 'spawn_link', [fun () -> ('Idris.Idris2.PrimIO':'un--unsafePerformIO'('erased', fun (V11) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V12) -> V12 end, V2, V11)) end)) end | []])))) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--erlSpawn'(V0, V1, V2) -> case case case V1 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E6, E7} -> (fun (V3, V4) -> V3 end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E3, E4, E5} -> (fun (V5, V6, V7) -> V5 end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E0, E1, E2} -> (fun (V8, V9, V10) -> ((V9('erased'))(('erlang':'apply'('erlang', 'spawn', [fun () -> ('Idris.Idris2.PrimIO':'un--unsafePerformIO'('erased', fun (V11) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V12) -> V12 end, V2, V11)) end)) end | []])))) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--erlSend'(V0, V1, V2, V3, V4) -> case case ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2)) of {'Idris.Prelude.IO.dn--un--__mkHasIO', E19, E20} -> (fun (V5, V6) -> V5 end(E19, E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E0, E1, E2} -> (fun (V7, V8, V9) -> ((((V8('erased'))('erased'))(case case case ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2)) of {'Idris.Prelude.IO.dn--un--__mkHasIO', E9, E10} -> (fun (V19, V20) -> V19 end(E9, E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E6, E7, E8} -> (fun (V21, V22, V23) -> V21 end(E6, E7, E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E3, E4, E5} -> (fun (V24, V25, V26) -> ((V25('erased'))(('erlang':'apply'('erlang', 'send', [V3 | [V4 | []]])))) end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(fun (V10) -> case case case ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2)) of {'Idris.Prelude.IO.dn--un--__mkHasIO', E17, E18} -> (fun (V11, V12) -> V11 end(E17, E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E14, E15, E16} -> (fun (V13, V14, V15) -> V13 end(E14, E15, E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E11, E12, E13} -> (fun (V16, V17, V18) -> ((V17('erased'))({'Idris.Builtin.MkUnit'})) end(E11, E12, E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end)) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--erlSelf'(V0, V1) -> case case case V1 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E6, E7} -> (fun (V2, V3) -> V2 end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E3, E4, E5} -> (fun (V4, V5, V6) -> V4 end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E0, E1, E2} -> (fun (V7, V8, V9) -> ((V8('erased'))(('erlang':'apply'('erlang', 'self', [])))) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--erlReceive'(V0, V1, V2, V3, V4, V5) -> case case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E23, E24} -> (fun (V6, V7) -> V6 end(E23, E24)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E0, E1, E2} -> (fun (V8, V9, V10) -> ((((V9('erased'))('erased'))(case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E3, E4} -> (fun (V29, V30) -> ((V30('erased'))(fun (V31) -> receive E5 -> (fun (V32) -> {'Idris.Prelude.Types.Just', V32} end(E5)) after V3 -> {'Idris.Prelude.Types.Nothing'} end end)) end(E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(fun (V11) -> case V11 of {'Idris.Prelude.Types.Just', E6} -> (fun (V12) -> case case case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E13, E14} -> (fun (V13, V14) -> V13 end(E13, E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E10, E11, E12} -> (fun (V15, V16, V17) -> V15 end(E10, E11, E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E7, E8, E9} -> (fun (V18, V19, V20) -> ((V19('erased'))(('Idris.Idris2.Erlang.Decode':'un--erlDecodeDef'('erased', 'erased', {'Idris.Erlang.Types.ETErlTerm'}, fun () -> V4 end, V5, V12)))) end(E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E6)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> case case case V2 of {'Idris.Prelude.IO.dn--un--__mkHasIO', E21, E22} -> (fun (V21, V22) -> V21 end(E21, E22)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkMonad', E18, E19, E20} -> (fun (V23, V24, V25) -> V23 end(E18, E19, E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end of {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', E15, E16, E17} -> (fun (V26, V27, V28) -> ((V27('erased'))(V4)) end(E15, E16, E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end)) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.