idris2

-module('Idris.Idris2.Text.Literate').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'with--isLiterateLine-2708'/5,
  'with--with block in reduce-2562'/13,
  'with--reduce-2535'/11,
  'case--extractCode-2643'/5,
  'case--reduce-2468'/10,
  'case--rawTokens-2402'/3,
  'nested--2450-2437--in--un--blank_content'/8,
  'un--untilEOL'/0,
  'un--unlit'/2,
  'un--relit'/2,
  'un--reduce'/2,
  'un--rawTokens'/2,
  'un--notCodeLine'/0,
  'un--line'/1,
  'un--isLiterateLine'/2,
  'un--extractCode'/2,
  'un--embedCode'/2,
  'un--block'/2
]).
'with--isLiterateLine-2708'(V0, V1, V2, V3, V4) -> case V3 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V5, V6) -> case V5 of [E2 | E3] -> (fun (V7, V8) -> case V7 of {'Idris.Text.Bounded.MkBounded', E4, E5, E6, E7, E8, E9} -> (fun (V9, V10, V11, V12, V13, V14) -> case V9 of {'Idris.Text.Literate.CodeLine', E10, E11} -> (fun (V15, V16) -> case V8 of [] -> case V6 of {'Idris.Builtin.MkPair', E12, E13} -> (fun (V17, V18) -> case V18 of {'Idris.Builtin.MkPair', E14, E15} -> (fun (V19, V20) -> case V20 of <<""/utf8>> -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Just', V15}, V16}; _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E14, E15)); _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E12, E13)); _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end; _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E10, E11)); _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E4, E5, E6, E7, E8, E9)); _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E2, E3)); _ -> {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V2} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in reduce-2562'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V0 of [] -> case V1 of {'Idris.Data.List.Views.Empty'} -> (fun () -> ('un--reduce'(V9, V8)) end()); _ -> case V1 of {'Idris.Data.List.Views.Snoc', E3, E4, E5} -> (fun (V13, V14, V15) -> ('un--reduce'(V9, [<<"\x{a}"/utf8>> | [('Idris.Idris2.Data.Strings':'un--unlines'(V14)) | V8]])) end(E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> case V1 of {'Idris.Data.List.Views.Snoc', E0, E1, E2} -> (fun (V16, V17, V18) -> ('un--reduce'(V9, [<<"\x{a}"/utf8>> | [('Idris.Idris2.Data.Strings':'un--unlines'(V17)) | V8]])) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'with--reduce-2535'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V1 of [] -> ('un--reduce'(V9, V10)); [E0 | E1] -> (fun (V11, V12) -> ('with--with block in reduce-2562'(V12, ('Idris.Idris2.Data.List.Views':'un--snocList'('erased', V12)), V2, V3, V4, V5, V6, V11, V10, V9, V8, V7, V0)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--extractCode-2643'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V5, V6) -> case V6 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V7, V8) -> case V8 of {'Idris.Builtin.MkPair', E4, E5} -> (fun (V9, V10) -> case V10 of <<""/utf8>> -> {'Idris.Prelude.Types.Right', ('un--reduce'(V5, []))}; _ -> {'Idris.Prelude.Types.Left', {'Idris.Text.Literate.MkLitErr', V7, V9, V10}} 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.
'case--reduce-2468'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of 0 -> ('un--reduce'(V7, [<<"\x{a}"/utf8>> | V8])); 1 -> ('un--reduce'(V7, [('Idris.Idris2.Prelude.Types':'un--substr'(('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types.Strings':'un--length'(V6)), (1 + 0))), ('Idris.Idris2.Prelude.Types.Strings':'un--length'(V5)), V5)) | V8])); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--rawTokens-2402'(V0, V1, V2) -> case V2 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V3, V4) -> {'Idris.Builtin.MkPair', ('un--block'(V3, V4)), fun (V5) -> {'Idris.Text.Literate.CodeBlock', ('Idris.Idris2.Data.Strings':'un--trim'(V3)), ('Idris.Idris2.Data.Strings':'un--trim'(V4)), V5} end} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--2450-2437--in--un--blank_content'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('Idris.Idris2.Data.Strings':'un--fastAppend'(('Idris.Idris2.Data.List':'un--replicate'('erased', ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', ('Idris.Idris2.Data.Strings':'un--lines'(V5)))), <<"\x{a}"/utf8>>)))).
'un--untilEOL'() -> ('Idris.Idris2.Text.Lexer':'un--manyUntil'('erased', ('Idris.Idris2.Text.Lexer':'un--newline'()), ('Idris.Idris2.Text.Lexer':'un--any'()))).
'un--unlit'(V0, V1) -> ('un--extractCode'(V0, V1)).
'un--relit'(V0, V1) -> ('un--embedCode'(V0, V1)).
'un--reduce'(V0, V1) -> case V0 of [] -> ('Idris.Idris2.Data.Strings':'un--fastAppend'(('Idris.Idris2.Data.List':'un--reverse'('erased', V1)))); [E0 | E1] -> (fun (V2, V3) -> case V2 of {'Idris.Text.Bounded.MkBounded', E2, E3, E4, E5, E6, E7} -> (fun (V4, V5, V6, V7, V8, V9) -> case V4 of {'Idris.Text.Literate.Any', E8} -> (fun (V10) -> ('un--reduce'(V3, [('nested--2450-2437--in--un--blank_content'(V5, V6, V7, V8, V9, V10, V3, V1)) | V1])) end(E8)); {'Idris.Text.Literate.CodeLine', E9, E10} -> (fun (V11, V12) -> ('case--reduce-2468'(V5, V6, V7, V8, V9, V12, V11, V3, V1, ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V11, ('Idris.Idris2.Data.Strings':'un--trim'(V12)))))) end(E9, E10)); {'Idris.Text.Literate.CodeBlock', E11, E12, E13} -> (fun (V13, V14, V15) -> ('with--reduce-2535'(V15, ('Idris.Idris2.Data.Strings':'un--lines'(V15)), V5, V6, V7, V8, V9, V14, V13, V3, V1)) end(E11, E12, E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E2, E3, E4, E5, E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--rawTokens'(V0, V1) -> ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V2) -> case V2 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V3, V4) -> {'Idris.Builtin.MkPair', ('un--block'(V3, V4)), fun (V5) -> {'Idris.Text.Literate.CodeBlock', ('Idris.Idris2.Data.Strings':'un--trim'(V3)), ('Idris.Idris2.Data.Strings':'un--trim'(V4)), V5} end} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, V0)), ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V6) -> {'Idris.Builtin.MkPair', ('un--line'(V6)), fun (V7) -> {'Idris.Text.Literate.CodeLine', ('Idris.Idris2.Data.Strings':'un--trim'(V6)), V7} end} end, V1)), [{'Idris.Builtin.MkPair', ('un--notCodeLine'()), fun (V8) -> {'Idris.Text.Literate.Any', V8} end} | []])))).
'un--notCodeLine'() -> ('Idris.Idris2.Text.Lexer.Core':'un--<|>'('erased', 'erased', ('Idris.Idris2.Text.Lexer':'un--newline'()), {'Idris.Text.Lexer.Core.SeqEat', ('Idris.Idris2.Text.Lexer':'un--any'()), fun () -> ('un--untilEOL'()) end})).
'un--line'(V0) -> {'Idris.Text.Lexer.Core.SeqEat', ('Idris.Idris2.Text.Lexer':'un--exact'(V0)), fun () -> ('Idris.Idris2.Text.Lexer.Core':'un--<|>'('erased', 'erased', ('Idris.Idris2.Text.Lexer':'un--newline'()), {'Idris.Text.Lexer.Core.SeqEat', ('Idris.Idris2.Text.Lexer':'un--space'()), fun () -> ('un--untilEOL'()) end})) end}.
'un--isLiterateLine'(V0, V1) -> case V0 of {'Idris.Text.Literate.MkLitStyle', E0, E1, E2} -> (fun (V2, V3, V4) -> ('with--isLiterateLine-2708'(V3, V2, V1, ('Idris.Idris2.Text.Lexer.Core':'un--lex'('erased', ('un--rawTokens'(V2, V3)), V1)), V4)) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--extractCode'(V0, V1) -> case V0 of {'Idris.Text.Literate.MkLitStyle', E0, E1, E2} -> (fun (V2, V3, V4) -> ('case--extractCode-2643'(V4, V3, V2, V1, ('Idris.Idris2.Text.Lexer.Core':'un--lex'('erased', ('un--rawTokens'(V2, V3)), V1)))) end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--embedCode'(V0, V1) -> case V0 of {'Idris.Text.Literate.MkLitStyle', E0, E1, E2} -> (fun (V2, V3, V4) -> case V2 of [E3 | E4] -> (fun (V5, V6) -> case V5 of {'Idris.Builtin.MkPair', E5, E6} -> (fun (V7, V8) -> ('Idris.Idris2.Data.Strings':'un--unlines'([V7 | [V1 | [V8 | []]]])) end(E5, E6)); _ -> V1 end end(E3, E4)); [] -> case V3 of [E7 | E8] -> (fun (V9, V10) -> ('Idris.Idris2.Data.Strings':'un--unwords'([V9 | [V1 | []]])) end(E7, E8)); _ -> V1 end; _ -> V1 end end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--block'(V0, V1) -> ('Idris.Idris2.Text.Lexer':'un--surround'({'Idris.Text.Lexer.Core.SeqEat', ('Idris.Idris2.Text.Lexer':'un--exact'(V0)), fun () -> ('un--untilEOL'()) end}, {'Idris.Text.Lexer.Core.SeqEat', ('Idris.Idris2.Text.Lexer':'un--exact'(V1)), fun () -> ('un--untilEOL'()) end}, ('Idris.Idris2.Text.Lexer':'un--any'()))).