Packages

Erlang code generator for Idris 2

Current section

Files

Jump to
idris2 src Idris.Idris2.Core.CaseTree.erl
Raw

src/Idris.Idris2.Core.CaseTree.erl

-module('Idris.Idris2.Core.CaseTree').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
'case--mkTerm-8286'/4,
'case--mkPat\x{27}-8208'/5,
'case--insertCaseNames-7781'/11,
'nested--5227-8033--in--un--getSet'/7,
'nested--5227-8032--in--un--getAltSets'/7,
'nested--5227-8031--in--un--getAltSet'/7,
'dn--un--weaken_Weaken__CaseTree'/3,
'dn--un--weakenNs_Weaken__CaseTree'/4,
'dn--un--show_Show__Pat'/1,
'dn--un--show_Show__(CaseTree $vars)'/2,
'dn--un--show_Show__(CaseAlt $vars)'/2,
'dn--un--showPrec_Show__Pat'/2,
'dn--un--showPrec_Show__(CaseTree $vars)'/3,
'dn--un--showPrec_Show__(CaseAlt $vars)'/3,
'dn--un--pretty_Pretty__(CaseTree $vars)'/3,
'dn--un--pretty_Pretty__(CaseAlt $vars)'/3,
'dn--un--prettyPrec_Pretty__(CaseTree $vars)'/4,
'dn--un--prettyPrec_Pretty__(CaseAlt $vars)'/4,
'dn--un--__Impl_Weaken_CaseTree'/0,
'dn--un--__Impl_Show_Pat'/0,
'dn--un--__Impl_Show_(CaseTree $vars)'/1,
'dn--un--__Impl_Show_(CaseAlt $vars)'/1,
'dn--un--__Impl_Pretty_(CaseTree $vars)'/1,
'dn--un--__Impl_Pretty_(CaseAlt $vars)'/1,
'un--mkTerm'/2,
'un--mkPat\x{27}'/3,
'un--insertCaseNames'/6,
'un--insertCaseAltNames'/6,
'un--getRefs'/3,
'un--getNames'/4,
'un--getMetas'/2,
'un--eqTree'/4,
'un--eqAlt'/4,
'un--argToPat'/1,
'un--addRefs'/4
]).
'case--mkTerm-8286'(V0, V1, V2, V3) -> case V3 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> {'Idris.Core.TT.Local', V1, {'Idris.Prelude.Types.Nothing'}, V4} end(E0)); _ -> {'Idris.Core.TT.Ref', V1, {'Idris.Core.TT.Bound'}, V0} end.
'case--mkPat\x{27}-8208'(V0, V1, V2, V3, V4) -> case V4 of 0 -> {'Idris.Core.CaseTree.PConst', V1, V0}; 1 -> {'Idris.Core.CaseTree.PTyCon', V1, {'Idris.Core.Name.UN', ('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V0))}, 0, []}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--insertCaseNames-7781'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> {'Idris.Core.CaseTree.Case', V3, V10, ('Idris.Idris2.Core.TT':'un--insertNames'('erased', 'erased', 'erased', V9, V8, V5)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V11) -> ('un--insertCaseAltNames'('erased', 'erased', 'erased', V9, V8, V11)) end, V4))}.
'nested--5227-8033--in--un--getSet'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Core.CaseTree.Case', E0, E1, E2, E3} -> (fun (V7, V8, V9, V10) -> ('nested--5227-8032--in--un--getAltSets'('erased', V1, V2, V3, 'erased', V5, V10)) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.STerm', E4, E5} -> (fun (V11, V12) -> (((V3('erased'))(V5))(V12)) end(E4, E5)); {'Idris.Core.CaseTree.Unmatched', E6} -> (fun (V13) -> V5 end(E6)); {'Idris.Core.CaseTree.Impossible'} -> (fun () -> V5 end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--5227-8032--in--un--getAltSets'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of [] -> V5; [E0 | E1] -> (fun (V7, V8) -> ('nested--5227-8032--in--un--getAltSets'('erased', V1, V2, V3, 'erased', ('nested--5227-8031--in--un--getAltSet'('erased', V1, V2, V3, 'erased', V5, V7)), V8)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--5227-8031--in--un--getAltSet'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Core.CaseTree.ConCase', E0, E1, E2, E3} -> (fun (V7, V8, V9, V10) -> ('nested--5227-8033--in--un--getSet'('erased', V1, V2, V3, 'erased', V5, V10)) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.DelayCase', E4, E5, E6} -> (fun (V11, V12, V13) -> ('nested--5227-8033--in--un--getSet'('erased', V1, V2, V3, 'erased', V5, V13)) end(E4, E5, E6)); {'Idris.Core.CaseTree.ConstCase', E7, E8} -> (fun (V14, V15) -> ('nested--5227-8033--in--un--getSet'('erased', V1, V2, V3, 'erased', V5, V15)) end(E7, E8)); {'Idris.Core.CaseTree.DefaultCase', E9} -> (fun (V16) -> ('nested--5227-8033--in--un--getSet'('erased', V1, V2, V3, 'erased', V5, V16)) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--weaken_Weaken__CaseTree'(V0, V1, V2) -> ('dn--un--weakenNs_Weaken__CaseTree'('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__CaseTree'(V0, V1, V2, V3) -> ('un--insertCaseNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V2, V3)).
'dn--un--show_Show__Pat'(V0) -> case V0 of {'Idris.Core.CaseTree.PAs', E0, E1, E2} -> (fun (V1, V2, V3) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V2)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"@("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__Pat'(V3)), <<")"/utf8>>)))))) end(E0, E1, E2)); {'Idris.Core.CaseTree.PCon', E3, E4, E5, E6, E7} -> (fun (V4, V5, V6, V7, V8) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V5)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V9) -> ('dn--un--show_Show__Pat'(V9)) end, fun (V10) -> fun (V11) -> ('dn--un--showPrec_Show__Pat'(V10, V11)) end end}, V8)))))))))) end(E3, E4, E5, E6, E7)); {'Idris.Core.CaseTree.PTyCon', E8, E9, E10, E11} -> (fun (V12, V13, V14, V15) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"<TyCon>"/utf8>>, ('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.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V16) -> ('dn--un--show_Show__Pat'(V16)) end, fun (V17) -> fun (V18) -> ('dn--un--showPrec_Show__Pat'(V17, V18)) end end}, V15)))))))) end(E8, E9, E10, E11)); {'Idris.Core.CaseTree.PConst', E12, E13} -> (fun (V19, V20) -> ('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V20)) end(E12, E13)); {'Idris.Core.CaseTree.PArrow', E14, E15, E16, E17} -> (fun (V21, V22, V23, V24) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__Pat'(V23)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" -> "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__Pat'(V24)), <<")"/utf8>>)))))))) end(E14, E15, E16, E17)); {'Idris.Core.CaseTree.PDelay', E18, E19, E20, E21} -> (fun (V25, V26, V27, V28) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"(Delay "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__Pat'(V28)), <<")"/utf8>>)))) end(E18, E19, E20, E21)); {'Idris.Core.CaseTree.PLoc', E22, E23} -> (fun (V29, V30) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V30)) end(E22, E23)); {'Idris.Core.CaseTree.PUnmatchable', E24, E25} -> (fun (V31, V32) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<".("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'dn--un--show_Show__(Term $vars)'([], V32)), <<")"/utf8>>)))) end(E24, E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__(CaseTree $vars)'(V0, V1) -> case V1 of {'Idris.Core.CaseTree.Case', E0, E1, E2, E3} -> (fun (V2, V3, V4, V5) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"case "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V2)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"] : "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'dn--un--show_Show__(Term $vars)'(V0, V4)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" of\x{a} { "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name.Namespace':'un--showSep'(<<"\x{a} | "/utf8>>, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V6) -> ('dn--un--show_Show__(CaseAlt $vars)'(V0, V6)) end, V5)))), <<"\x{a} }"/utf8>>)))))))))))))))) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.STerm', E4, E5} -> (fun (V7, V8) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V7)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"] "/utf8>>, ('Idris.Idris2.Core.TT':'dn--un--show_Show__(Term $vars)'(V0, V8)))))))) end(E4, E5)); {'Idris.Core.CaseTree.Unmatched', E6} -> (fun (V9) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Error: "/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V9)))) end(E6)); {'Idris.Core.CaseTree.Impossible'} -> (fun () -> <<"Impossible"/utf8>> end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__(CaseAlt $vars)'(V0, V1) -> case V1 of {'Idris.Core.CaseTree.ConCase', E0, E1, E2, E3} -> (fun (V2, V3, V4, V5) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name.Namespace':'un--showSep'(<<" "/utf8>>, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V6) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V6)) end, [V2 | V4])))), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" => "/utf8>>, ('dn--un--show_Show__(CaseTree $vars)'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V4, V0)), V5)))))) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.DelayCase', E4, E5, E6} -> (fun (V7, V8, V9) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Delay "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V8)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" => "/utf8>>, ('dn--un--show_Show__(CaseTree $vars)'([V7 | [V8 | V0]], V9)))))))) end(E4, E5, E6)); {'Idris.Core.CaseTree.ConstCase', E7, E8} -> (fun (V10, V11) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Constant "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V10)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" => "/utf8>>, ('dn--un--show_Show__(CaseTree $vars)'(V0, V11)))))))) end(E7, E8)); {'Idris.Core.CaseTree.DefaultCase', E9} -> (fun (V12) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"_ => "/utf8>>, ('dn--un--show_Show__(CaseTree $vars)'(V0, V12)))) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--showPrec_Show__Pat'(V0, V1) -> ('dn--un--show_Show__Pat'(V1)).
'dn--un--showPrec_Show__(CaseTree $vars)'(V0, V1, V2) -> ('dn--un--show_Show__(CaseTree $vars)'(V0, V2)).
'dn--un--showPrec_Show__(CaseAlt $vars)'(V0, V1, V2) -> ('dn--un--show_Show__(CaseAlt $vars)'(V0, V2)).
'dn--un--pretty_Pretty__(CaseTree $vars)'(V0, V1, V2) -> case V2 of {'Idris.Core.CaseTree.Case', E0, E1, E2, E3} -> (fun (V3, V4, V5, V6) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--fromString_FromString__(Doc $ann)'('erased', <<"case"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Core.Name':'dn--un--pretty_Pretty__Name'('erased', V3)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--fromString_FromString__(Doc $ann)'('erased', <<":"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Core.TT':'dn--un--pretty_Pretty__(Term $vars)'('erased', V1, V5)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--fromString_FromString__(Doc $ann)'('erased', <<"of"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--nest'('erased', 2, ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hardline'('erased')), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--vsep'('erased', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V7) -> ('dn--un--pretty_Pretty__(CaseAlt $vars)'('erased', V1, V7)) end, V6)))))))))))))))))) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.STerm', E4, E5} -> (fun (V8, V9) -> ('Idris.Idris2.Core.TT':'dn--un--pretty_Pretty__(Term $vars)'('erased', V1, V9)) end(E4, E5)); {'Idris.Core.CaseTree.Unmatched', E6} -> (fun (V10) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"Error:"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V10)))) end(E6)); {'Idris.Core.CaseTree.Impossible'} -> (fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"Impossible"/utf8>>)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--pretty_Pretty__(CaseAlt $vars)'(V0, V1, V2) -> case V2 of {'Idris.Core.CaseTree.ConCase', E0, E1, E2, E3} -> (fun (V3, V4, V5, V6) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hsep'('erased', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V7) -> ('Idris.Idris2.Core.Name':'dn--un--pretty_Pretty__Name'('erased', V7)) end, [V3 | V5])))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"=>"/utf8>>)), {'Idris.Text.PrettyPrint.Prettyprinter.Doc.Union', fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--spaces'('erased', 1)), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V5, V1)), V6)))) end, fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--nest'('erased', 2, ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hardline'('erased')), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V5, V1)), V6)))))) end})))) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.DelayCase', E4, E5, E6} -> (fun (V8, V9, V10) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"Delay"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Core.Name':'dn--un--pretty_Pretty__Name'('erased', V9)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"=>"/utf8>>)), {'Idris.Text.PrettyPrint.Prettyprinter.Doc.Union', fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--spaces'('erased', 1)), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', [V8 | [V9 | V1]], V10)))) end, fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--nest'('erased', 2, ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hardline'('erased')), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', [V8 | [V9 | V1]], V10)))))) end})))))) end(E4, E5, E6)); {'Idris.Core.CaseTree.ConstCase', E7, E8} -> (fun (V11, V12) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Core.TT':'dn--un--pretty_Pretty__Constant'('erased', V11)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"=>"/utf8>>)), {'Idris.Text.PrettyPrint.Prettyprinter.Doc.Union', fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--spaces'('erased', 1)), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V1, V12)))) end, fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--nest'('erased', 2, ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hardline'('erased')), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V1, V12)))))) end})))) end(E7, E8)); {'Idris.Core.CaseTree.DefaultCase', E9} -> (fun (V13) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"_ =>"/utf8>>)), {'Idris.Text.PrettyPrint.Prettyprinter.Doc.Union', fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--spaces'('erased', 1)), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V1, V13)))) end, fun () -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--nest'('erased', 2, ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--hardline'('erased')), ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V1, V13)))))) end})) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--prettyPrec_Pretty__(CaseTree $vars)'(V0, V1, V2, V3) -> ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V1, V3)).
'dn--un--prettyPrec_Pretty__(CaseAlt $vars)'(V0, V1, V2, V3) -> ('dn--un--pretty_Pretty__(CaseAlt $vars)'('erased', V1, V3)).
'dn--un--__Impl_Weaken_CaseTree'() -> {'Idris.Core.TT.dn--un--__mkWeaken', fun (V0) -> fun (V1) -> fun (V2) -> ('dn--un--weaken_Weaken__CaseTree'('erased', 'erased', V2)) end end end, fun (V3) -> fun (V4) -> fun (V5) -> fun (V6) -> ('dn--un--weakenNs_Weaken__CaseTree'('erased', 'erased', V5, V6)) end end end end}.
'dn--un--__Impl_Show_Pat'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__Pat'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__Pat'(V1, V2)) end end}.
'dn--un--__Impl_Show_(CaseTree $vars)'(V0) -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V1) -> ('dn--un--show_Show__(CaseTree $vars)'(V0, V1)) end, fun (V2) -> fun (V3) -> ('dn--un--showPrec_Show__(CaseTree $vars)'(V0, V2, V3)) end end}.
'dn--un--__Impl_Show_(CaseAlt $vars)'(V0) -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V1) -> ('dn--un--show_Show__(CaseAlt $vars)'(V0, V1)) end, fun (V2) -> fun (V3) -> ('dn--un--showPrec_Show__(CaseAlt $vars)'(V0, V2, V3)) end end}.
'dn--un--__Impl_Pretty_(CaseTree $vars)'(V0) -> {'Idris.Text.PrettyPrint.Prettyprinter.Doc.dn--un--__mkPretty', fun (V1) -> fun (V2) -> ('dn--un--pretty_Pretty__(CaseTree $vars)'('erased', V0, V2)) end end, fun (V3) -> fun (V4) -> fun (V5) -> ('dn--un--prettyPrec_Pretty__(CaseTree $vars)'('erased', V0, V4, V5)) end end end}.
'dn--un--__Impl_Pretty_(CaseAlt $vars)'(V0) -> {'Idris.Text.PrettyPrint.Prettyprinter.Doc.dn--un--__mkPretty', fun (V1) -> fun (V2) -> ('dn--un--pretty_Pretty__(CaseAlt $vars)'('erased', V0, V2)) end end, fun (V3) -> fun (V4) -> fun (V5) -> ('dn--un--prettyPrec_Pretty__(CaseAlt $vars)'('erased', V0, V4, V5)) end end end}.
'un--mkTerm'(V0, V1) -> case V1 of {'Idris.Core.CaseTree.PAs', E0, E1, E2} -> (fun (V2, V3, V4) -> ('un--mkTerm'(V0, V4)) end(E0, E1, E2)); {'Idris.Core.CaseTree.PCon', E3, E4, E5, E6, E7} -> (fun (V5, V6, V7, V8, V9) -> ('Idris.Idris2.Core.TT':'un--apply'('erased', V5, {'Idris.Core.TT.Ref', V5, {'Idris.Core.TT.DataCon', V7, V8}, V6}, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V10) -> ('un--mkTerm'(V0, V10)) end, V9)))) end(E3, E4, E5, E6, E7)); {'Idris.Core.CaseTree.PTyCon', E8, E9, E10, E11} -> (fun (V11, V12, V13, V14) -> ('Idris.Idris2.Core.TT':'un--apply'('erased', V11, {'Idris.Core.TT.Ref', V11, {'Idris.Core.TT.TyCon', 0, V13}, V12}, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V15) -> ('un--mkTerm'(V0, V15)) end, V14)))) end(E8, E9, E10, E11)); {'Idris.Core.CaseTree.PConst', E12, E13} -> (fun (V16, V17) -> {'Idris.Core.TT.PrimVal', V16, V17} end(E12, E13)); {'Idris.Core.CaseTree.PArrow', E14, E15, E16, E17} -> (fun (V18, V19, V20, V21) -> {'Idris.Core.TT.Bind', V18, V19, {'Idris.Core.TT.Pi', V18, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'()), {'Idris.Core.TT.Explicit'}, ('un--mkTerm'(V0, V20))}, ('un--mkTerm'([V19 | V0], V21))} end(E14, E15, E16, E17)); {'Idris.Core.CaseTree.PDelay', E18, E19, E20, E21} -> (fun (V22, V23, V24, V25) -> {'Idris.Core.TT.TDelay', V22, V23, ('un--mkTerm'(V0, V24)), ('un--mkTerm'(V0, V25))} end(E18, E19, E20, E21)); {'Idris.Core.CaseTree.PLoc', E22, E23} -> (fun (V26, V27) -> ('case--mkTerm-8286'(V27, V26, V0, ('Idris.Idris2.Core.TT':'un--isVar'(V27, V0)))) end(E22, E23)); {'Idris.Core.CaseTree.PUnmatchable', E24, E25} -> (fun (V28, V29) -> ('Idris.Idris2.Core.TT':'un--embed'('erased', 'erased', V29)) end(E24, E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--mkPat\x{27}'(V0, V1, V2) -> case V2 of {'Idris.Core.TT.Ref', E0, E1, E2} -> (fun (V3, V4, V5) -> case V4 of {'Idris.Core.TT.Bound'} -> (fun () -> {'Idris.Core.CaseTree.PLoc', V3, V5} end()); {'Idris.Core.TT.DataCon', E3, E4} -> (fun (V6, V7) -> {'Idris.Core.CaseTree.PCon', V3, V5, V6, V7, V0} end(E3, E4)); {'Idris.Core.TT.TyCon', E5, E6} -> (fun (V8, V9) -> {'Idris.Core.CaseTree.PTyCon', V3, V5, V9, V0} end(E5, E6)); _ -> {'Idris.Core.CaseTree.PUnmatchable', ('Idris.Idris2.Core.TT':'un--getLoc'('erased', V1)), V1} end end(E0, E1, E2)); {'Idris.Core.TT.Bind', E7, E8, E9, E10} -> (fun (V10, V11, V12, V13) -> case V12 of {'Idris.Core.TT.Pi', E11, E12, E13, E14} -> (fun (V14, V15, V16, V17) -> begin (V18 = ('Idris.Idris2.Core.TT.SubstEnv':'un--subst'('erased', 'erased', {'Idris.Core.TT.Erased', V10, 1}, V13))), {'Idris.Core.CaseTree.PArrow', V10, V11, ('un--mkPat\x{27}'([], V17, V17)), ('un--mkPat\x{27}'([], V18, V18))} end end(E11, E12, E13, E14)); _ -> {'Idris.Core.CaseTree.PUnmatchable', ('Idris.Idris2.Core.TT':'un--getLoc'('erased', V1)), V1} end end(E7, E8, E9, E10)); {'Idris.Core.TT.App', E15, E16, E17} -> (fun (V19, V20, V21) -> begin (V22 = ('un--mkPat\x{27}'([], V21, V21))), ('un--mkPat\x{27}'([V22 | V0], V1, V20)) end end(E15, E16, E17)); {'Idris.Core.TT.As', E18, E19, E20, E21} -> (fun (V23, V24, V25, V26) -> case V25 of {'Idris.Core.TT.Ref', E22, E23, E24} -> (fun (V27, V28, V29) -> case V28 of {'Idris.Core.TT.Bound'} -> (fun () -> {'Idris.Core.CaseTree.PAs', V23, V29, ('un--mkPat\x{27}'([], V26, V26))} end()); _ -> ('un--mkPat\x{27}'([], V1, V26)) end end(E22, E23, E24)); _ -> ('un--mkPat\x{27}'([], V1, V26)) end end(E18, E19, E20, E21)); {'Idris.Core.TT.TDelay', E25, E26, E27, E28} -> (fun (V30, V31, V32, V33) -> {'Idris.Core.CaseTree.PDelay', V30, V31, ('un--mkPat\x{27}'([], V1, V32)), ('un--mkPat\x{27}'([], V1, V33))} end(E25, E26, E27, E28)); {'Idris.Core.TT.PrimVal', E29, E30} -> (fun (V34, V35) -> ('case--mkPat\x{27}-8208'(V35, V34, V1, V0, ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(('Idris.Idris2.Core.TT':'un--constTag'(V35)), 0)))) end(E29, E30)); {'Idris.Core.TT.TType', E31} -> (fun (V36) -> {'Idris.Core.CaseTree.PTyCon', V36, {'Idris.Core.Name.UN', <<"Type"/utf8>>}, 0, []} end(E31)); _ -> {'Idris.Core.CaseTree.PUnmatchable', ('Idris.Idris2.Core.TT':'un--getLoc'('erased', V1)), V1} end.
'un--insertCaseNames'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CaseTree.Case', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> ('case--insertCaseNames-7781'('erased', 'erased', 'erased', V6, V9, V8, V7, 'erased', V4, V3, ('Idris.Idris2.Core.TT':'un--insertNVarNames'('erased', 'erased', 'erased', 'erased', V3, V4, V7)))) end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.STerm', E4, E5} -> (fun (V10, V11) -> {'Idris.Core.CaseTree.STerm', V10, ('Idris.Idris2.Core.TT':'un--insertNames'('erased', 'erased', 'erased', V3, V4, V11))} end(E4, E5)); {'Idris.Core.CaseTree.Unmatched', E6} -> (fun (V12) -> {'Idris.Core.CaseTree.Unmatched', V12} end(E6)); {'Idris.Core.CaseTree.Impossible'} -> (fun () -> {'Idris.Core.CaseTree.Impossible'} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--insertCaseAltNames'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.CaseTree.ConCase', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> {'Idris.Core.CaseTree.ConCase', V6, V7, V8, ('un--insertCaseNames'('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)); {'Idris.Core.CaseTree.DelayCase', E4, E5, E6} -> (fun (V10, V11, V12) -> {'Idris.Core.CaseTree.DelayCase', V10, V11, ('un--insertCaseNames'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)))), V4, V12))} end(E4, E5, E6)); {'Idris.Core.CaseTree.ConstCase', E7, E8} -> (fun (V13, V14) -> {'Idris.Core.CaseTree.ConstCase', V13, ('un--insertCaseNames'('erased', 'erased', 'erased', V3, V4, V14))} end(E7, E8)); {'Idris.Core.CaseTree.DefaultCase', E9} -> (fun (V15) -> {'Idris.Core.CaseTree.DefaultCase', ('un--insertCaseNames'('erased', 'erased', 'erased', V3, V4, V15))} end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getRefs'(V0, V1, V2) -> ('un--getNames'('erased', fun (V3) -> fun (V4) -> fun (V5) -> ('Idris.Idris2.Core.TT':'un--addRefs'('erased', 1, V1, V4, V5)) end end end, ('Idris.Idris2.Data.NameMap':'un--empty'('erased')), V2)).
'un--getNames'(V0, V1, V2, V3) -> ('nested--5227-8033--in--un--getSet'('erased', V3, V2, V1, 'erased', V2, V3)).
'un--getMetas'(V0, V1) -> ('un--getNames'('erased', fun (V2) -> fun (V3) -> fun (V4) -> ('Idris.Idris2.Core.TT':'un--addMetas'('erased', V3, V4)) end end end, ('Idris.Idris2.Data.NameMap':'un--empty'('erased')), V1)).
'un--eqTree'(V0, V1, V2, V3) -> case V2 of {'Idris.Core.CaseTree.Case', E0, E1, E2, E3} -> (fun (V4, V5, V6, V7) -> case V3 of {'Idris.Core.CaseTree.Case', E4, E5, E6, E7} -> (fun (V8, V9, V10, V11) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V5, V9)), fun () -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V7)), ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V11)))), fun () -> ('Idris.Idris2.Data.Bool.Extra':'un--allTrue'(('Idris.Idris2.Data.List':'un--zipWith'('erased', 'erased', 'erased', fun (V12) -> fun (V13) -> ('un--eqAlt'('erased', 'erased', V12, V13)) end end, V7, V11)))) end)) end)) end(E4, E5, E6, E7)); _ -> 1 end end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.STerm', E8, E9} -> (fun (V14, V15) -> case V3 of {'Idris.Core.CaseTree.STerm', E10, E11} -> (fun (V16, V17) -> ('Idris.Idris2.Core.TT':'un--eqTerm'('erased', 'erased', V15, V17)) end(E10, E11)); _ -> 1 end end(E8, E9)); {'Idris.Core.CaseTree.Unmatched', E12} -> (fun (V18) -> case V3 of {'Idris.Core.CaseTree.Unmatched', E13} -> (fun (V19) -> 0 end(E13)); _ -> 1 end end(E12)); {'Idris.Core.CaseTree.Impossible'} -> (fun () -> case V3 of {'Idris.Core.CaseTree.Impossible'} -> (fun () -> 0 end()); _ -> 1 end end()); _ -> 1 end.
'un--eqAlt'(V0, V1, V2, V3) -> case V2 of {'Idris.Core.CaseTree.ConCase', E0, E1, E2, E3} -> (fun (V4, V5, V6, V7) -> case V3 of {'Idris.Core.CaseTree.ConCase', E4, E5, E6, E7} -> (fun (V8, V9, V10, V11) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V4, V8)), fun () -> ('un--eqTree'('erased', 'erased', V7, V11)) end)) end(E4, E5, E6, E7)); _ -> 1 end end(E0, E1, E2, E3)); {'Idris.Core.CaseTree.DelayCase', E8, E9, E10} -> (fun (V12, V13, V14) -> case V3 of {'Idris.Core.CaseTree.DelayCase', E11, E12, E13} -> (fun (V15, V16, V17) -> ('un--eqTree'('erased', 'erased', V14, V17)) end(E11, E12, E13)); _ -> 1 end end(E8, E9, E10)); {'Idris.Core.CaseTree.ConstCase', E14, E15} -> (fun (V18, V19) -> case V3 of {'Idris.Core.CaseTree.ConstCase', E16, E17} -> (fun (V20, V21) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Core.TT':'dn--un--==_Eq__Constant'(V18, V20)), fun () -> ('un--eqTree'('erased', 'erased', V19, V21)) end)) end(E16, E17)); _ -> 1 end end(E14, E15)); {'Idris.Core.CaseTree.DefaultCase', E18} -> (fun (V22) -> case V3 of {'Idris.Core.CaseTree.DefaultCase', E19} -> (fun (V23) -> ('un--eqTree'('erased', 'erased', V22, V23)) end(E19)); _ -> 1 end end(E18)); _ -> 1 end.
'un--argToPat'(V0) -> ('un--mkPat\x{27}'([], V0, V0)).
'un--addRefs'(V0, V1, V2, V3) -> ('un--getNames'('erased', fun (V4) -> fun (V5) -> fun (V6) -> ('Idris.Idris2.Core.TT':'un--addRefs'('erased', 1, V1, V5, V6)) end end end, V2, V3)).