idris2

-module('Idris.Idris2.TTImp.Interactive.GenerateDef').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--makeDefN-5537'/7,
  'case--case block in propBindableUsed-5449'/4,
  'case--propBindableUsed-5434'/2,
  'case--case block in propBindableUsed,getProp-5381'/6,
  'case--propBindableUsed,getProp-5366'/4,
  'case--case block in makeDef-5280'/13,
  'case--makeDef-5210'/6,
  'case--makeDefFromType-5066'/16,
  'case--mkSplits-4970'/9,
  'case--mkSplits-4934'/8,
  'case--case block in generateSplits-4709'/13,
  'case--generateSplits-4681'/10,
  'case--trySplit-4584'/9,
  'case--trySplit,updateLHS-4519'/12,
  'case--trySplit,updateLHS-4461'/12,
  'case--case block in case block in case block in expandClause-4161'/20,
  'case--case block in case block in expandClause-4108'/15,
  'case--case block in expandClause-4085'/10,
  'case--expandClause-4063'/9,
  'case--case block in fnName-3946'/2,
  'case--fnName-3933'/3,
  'nested--12690-4430--in--un--valid'/9,
  'nested--12210-4007--in--un--updateRHS'/9,
  'nested--12690-4432--in--un--updateLHS'/10,
  'nested--12170-3967--in--un--mkUniqueName'/5,
  'nested--13722-5348--in--un--getProp'/2,
  'nested--12690-4431--in--un--fixNames'/9,
  'nested--12210-4008--in--un--dropLams'/9,
  'un--uniqueRHS'/2,
  'un--trySplit'/9,
  'un--tryAllSplits'/7,
  'un--splittableNames'/1,
  'un--propBindableUsed'/1,
  'un--mostUsed'/2,
  'un--mkSplits'/7,
  'un--makeDefSort'/8,
  'un--makeDefN'/7,
  'un--makeDefFromType'/9,
  'un--makeDef'/6,
  'un--generateSplits'/7,
  'un--fnName'/2,
  'un--expandClause'/8,
  'un--collectClauses'/3,
  'un--bindableUsed'/1
]).
'case--makeDefN-5537'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V7, V8) -> fun (V9) -> {'Idris.Prelude.Types.Right', V7} end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in propBindableUsed-5449'(V0, V1, V2, V3) -> case V3 of 0 -> 1.0; 1 -> ('Idris.Idris2.Prelude.Num':'dn--un--/_Fractional__Double'(('Idris.Idris2.Prelude.Types':'dn--un--cast_Cast__Nat_Double'(V2)), ('Idris.Idris2.Prelude.Types':'dn--un--cast_Cast__Nat_Double'(V1)))); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--propBindableUsed-5434'(V0, V1) -> case V1 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V2, V3) -> ('case--case block in propBindableUsed-5449'(V0, V2, V3, ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V2, 0)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in propBindableUsed,getProp-5381'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Builtin.MkPair', V3, V4} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> case V6 of {'Idris.Builtin.MkPair', E1, E2} -> (fun (V7, V8) -> {'Idris.Builtin.MkPair', ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(V3, ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V11, V12)) end end}, V7)))))), ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(V4, ('Idris.Idris2.Prelude.Types.List':'un--length'('erased', ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V13) -> fun (V14) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V13, V14)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V15, V16)) end end}, V8))))))} end(E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--propBindableUsed,getProp-5366'(V0, V1, V2, V3) -> case V3 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V4, V5) -> ('case--case block in propBindableUsed,getProp-5381'(V0, V1, V2, V4, V5, ('un--bindableUsed'(V1)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in makeDef-5280'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9} -> (fun (V13, V14, V15, V16, V17, V18, V19, V20, V21, V22) -> {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', V13, V14, V15, V16, V17, V18, V19, V20, V21, {'Idris.Prelude.Types.Just', fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> ('un--makeDefFromType'(V4, V3, V2, V5, V23, V24, V25, V26, V27)) end end end end end}} end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--makeDef-5210'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> case V6 of {'Idris.Builtin.MkPair', E1, E2} -> (fun (V7, V8) -> case V8 of {'Idris.Builtin.MkPair', E3, E4} -> (fun (V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E5, E6} -> (fun (V11, V12) -> fun (V13) -> begin (V14 = (('Idris.Idris2.Core.Context':'un--getFullName'(V4, V9))(V13))), 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.Idris2.Core.Context.Log':'un--logTerm'([], V4, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Searching for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V16)))) end, V12, V13))), case V17 of {'Idris.Prelude.Types.Left', E9} -> (fun (V18) -> {'Idris.Prelude.Types.Left', V18} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V19) -> begin (V21 = begin (V20 = {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V7, {'Idris.Builtin.MkPair', V9, {'Idris.Builtin.MkPair', V11, V12}}}}), ('case--case block in makeDef-5280'(V0, V1, V2, V3, V4, V7, V9, V11, V12, V20, V16, V19, ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--initSearchOpts'(0, (1 + (1 + (1 + (1 + (1 + 0))))))))) end), ('un--makeDefFromType'(V4, V3, V2, V7, V21, V16, V11, V12, V13)) end end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V22) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V22)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--makeDefFromType-5066'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15) -> case V15 of {'Idris.Prelude.Types.Just', E0} -> (fun (V16) -> fun (V17) -> begin (V18 = (('un--mkSplits'(V7, V6, V5, V4, V3, V16, V14))(V17))), case V18 of {'Idris.Prelude.Types.Left', E1} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V20) -> begin (V49 = begin (V48 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V21) -> fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V23, V24, V25)) end end end end end, fun (V26) -> fun (V27) -> fun (V28) -> V27 end end end, fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> begin (V34 = (V31(V33))), begin (V35 = (V32(V33))), (V34(V35)) end end end end end end end}, fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V38(V40))), ((V39(V41))(V40)) end end end end end end, fun (V42) -> fun (V43) -> fun (V44) -> begin (V45 = (V43(V44))), (V45(V44)) end end end end}, fun (V46) -> fun (V47) -> V47 end end}, V7, V8))(V17))), {'Idris.Prelude.Types.Right', V48} end), case V49 of {'Idris.Prelude.Types.Left', E3} -> (fun (V50) -> {'Idris.Prelude.Types.Left', V50} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V51) -> begin (V80 = begin (V79 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> fun (V56) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V54, V55, V56)) end end end end end, fun (V57) -> fun (V58) -> fun (V59) -> V58 end end end, fun (V60) -> fun (V61) -> fun (V62) -> fun (V63) -> fun (V64) -> begin (V65 = (V62(V64))), begin (V66 = (V63(V64))), (V65(V66)) end end end end end end end}, fun (V67) -> fun (V68) -> fun (V69) -> fun (V70) -> fun (V71) -> begin (V72 = (V69(V71))), ((V70(V72))(V71)) end end end end end end, fun (V73) -> fun (V74) -> fun (V75) -> begin (V76 = (V74(V75))), (V76(V75)) end end end end}, fun (V77) -> fun (V78) -> V78 end end}, V6, V9))(V17))), {'Idris.Prelude.Types.Right', V79} end), case V80 of {'Idris.Prelude.Types.Left', E5} -> (fun (V81) -> {'Idris.Prelude.Types.Left', V81} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V82) -> begin (V111 = begin (V110 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V83) -> fun (V84) -> fun (V85) -> fun (V86) -> fun (V87) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V85, V86, V87)) end end end end end, fun (V88) -> fun (V89) -> fun (V90) -> V89 end end end, fun (V91) -> fun (V92) -> fun (V93) -> fun (V94) -> fun (V95) -> begin (V96 = (V93(V95))), begin (V97 = (V94(V95))), (V96(V97)) end end end end end end end}, fun (V98) -> fun (V99) -> fun (V100) -> fun (V101) -> fun (V102) -> begin (V103 = (V100(V102))), ((V101(V103))(V102)) end end end end end end, fun (V104) -> fun (V105) -> fun (V106) -> begin (V107 = (V105(V106))), (V107(V106)) end end end end}, fun (V108) -> fun (V109) -> V109 end end}, V5, V10))(V17))), {'Idris.Prelude.Types.Right', V110} end), case V111 of {'Idris.Prelude.Types.Left', E7} -> (fun (V112) -> {'Idris.Prelude.Types.Left', V112} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V113) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.TTImp.Interactive.ExprSearch':'dn--un--map_Functor__Search'('erased', 'erased', fun (V114) -> {'Idris.Builtin.MkPair', V4, V114} end, V20))} end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V115) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V4, V2}, V115)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--mkSplits-4970'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V3 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9} -> (fun (V9, V10, V11, V12, V13, V14, V15, V16, V17, V18) -> {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', V9, V10, V11, V12, V13, V14, V15, 1, 0, V18} end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--mkSplits-4934'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of 0 -> fun (V8) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V8)) end; 1 -> fun (V9) -> ('un--expandClause'(V0, V6, V5, V4, V3, V2, V1, V9)) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in generateSplits-4709'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of 0 -> ('un--splittableNames'(V1)); 1 -> ('Idris.Idris2.Data.List':'un--reverse'('erased', ('un--splittableNames'(V1)))); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--generateSplits-4681'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V10, V11) -> begin (V23 = begin (V12 = {'Idris.Builtin.MkPair', V10, V11}), ('case--case block in generateSplits-4709'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V11, V10, V12, case V4 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11} -> (fun (V13, V14, V15, V16, V17, V18, V19, V20, V21, V22) -> V19 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end), ('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V24) -> fun (V25) -> ('un--trySplit'(V8, V7, V6, V2, V1, V10, V0, V24, V25)) end end, V23)) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--trySplit-4584'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.TTImp.Interactive.CaseSplit.OK', E0} -> (fun (V9) -> fun (V10) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V0, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V11) -> {'Idris.TTImp.TTImp.PatClause', V4, ('nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V11, V3)), V1} end, ('Idris.Idris2.Data.List':'un--mapMaybe'('erased', 'erased', fun (V12) -> ('nested--12690-4430--in--un--valid'(V0, V1, V2, V3, V4, V5, V6, V7, V12)) end, V9))))}} end end(E0)); _ -> fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V0, []}} end end.
'case--trySplit,updateLHS-4519'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11) -> case V11 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.TTImp.TTImp.IBindVar', V9, V8} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V12) -> ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V12)) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--trySplit,updateLHS-4461'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11) -> case V11 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.TTImp.TTImp.IVar', V9, V8} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V12) -> ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V12)) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in case block in case block in expandClause-4161'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19) -> case V19 of {'Idris.Prelude.Types.Just', E0} -> (fun (V20) -> case V20 of {'Idris.Core.Context.Hole', E1, E2} -> (fun (V21, V22) -> fun (V23) -> begin (V30 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expression search for "/utf8>>, ('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 (V24) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V24)) end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V25, V26)) end end}, {'Idris.Prelude.Show.dn--un--__mkShow', fun (V27) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V27)) end, fun (V28) -> fun (V29) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V28, V29)) end end}}, {'Idris.Builtin.MkPair', V17, V16})))) end))(V23))), case V30 of {'Idris.Prelude.Types.Left', E3} -> (fun (V31) -> {'Idris.Prelude.Types.Left', V31} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V32) -> begin (V33 = ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--exprSearchOpts'(V0, V6, V5, V3, V4, {'Idris.Core.Name.Resolved', V16}, [], V23))), case V33 of {'Idris.Prelude.Types.Left', E5} -> (fun (V34) -> {'Idris.Prelude.Types.Left', V34} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V35) -> (('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--traverse'('erased', 'erased', fun (V36) -> begin (V37 = ('nested--12210-4008--in--un--dropLams'(V0, V1, V2, V3, V4, V5, V6, V21, V36))), fun (V38) -> begin (V39 = (('Idris.Idris2.Core.Normalise':'un--logTermNF'(V9, V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> <<"Got clause"/utf8>> end, V12, V11))(V38))), case V39 of {'Idris.Prelude.Types.Left', E7} -> (fun (V40) -> {'Idris.Prelude.Types.Left', V40} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V41) -> begin (V42 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"        = "/utf8>>, ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__RawImp'(V37)))) end))(V38))), case V42 of {'Idris.Prelude.Types.Left', E9} -> (fun (V43) -> {'Idris.Prelude.Types.Left', V43} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V44) -> {'Idris.Prelude.Types.Right', [('nested--12210-4007--in--un--updateRHS'(V0, V1, V2, V3, V4, V5, V6, V7, V37)) | []]} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end, V35))(V23)) end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E1, E2)); _ -> fun (V45) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V4, <<"No searchable hole on RHS"/utf8>>}, V45)) end end end(E0)); _ -> fun (V46) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V4, <<"No searchable hole on RHS"/utf8>>}, V46)) end end.
'case--case block in case block in expandClause-4108'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14) -> case V14 of {'Idris.Core.TT.Meta', E0, E1, E2, E3} -> (fun (V15, V16, V17, V18) -> fun (V19) -> begin (V48 = begin (V47 = (('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 (V20) -> fun (V21) -> fun (V22) -> fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V22, V23, V24)) end end end end end, fun (V25) -> fun (V26) -> fun (V27) -> V26 end end end, fun (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> begin (V33 = (V30(V32))), begin (V34 = (V31(V32))), (V33(V34)) end end end end end end end}, fun (V35) -> fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> begin (V40 = (V37(V39))), ((V38(V40))(V39)) end end end end end end, fun (V41) -> fun (V42) -> fun (V43) -> begin (V44 = (V42(V43))), (V44(V43)) end end end end}, fun (V45) -> fun (V46) -> V46 end end}, V0))(V19))), {'Idris.Prelude.Types.Right', V47} end), case V48 of {'Idris.Prelude.Types.Left', E4} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V50) -> begin (V77 = ('Idris.Idris2.Core.Context':'un--lookupDefExact'({'Idris.Core.Name.Resolved', V17}, case V50 of {'Idris.Core.Context.MkDefs', E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31} -> (fun (V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76) -> V51 end(E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V19))), case V77 of {'Idris.Prelude.Types.Left', E32} -> (fun (V78) -> {'Idris.Prelude.Types.Left', V78} end(E32)); {'Idris.Prelude.Types.Right', E33} -> (fun (V79) -> case V79 of {'Idris.Prelude.Types.Just', E34} -> (fun (V80) -> case V80 of {'Idris.Core.Context.Hole', E35, E36} -> (fun (V81, V82) -> begin (V89 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Expression search for "/utf8>>, ('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 (V83) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V83)) end, fun (V84) -> fun (V85) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V84, V85)) end end}, {'Idris.Prelude.Show.dn--un--__mkShow', fun (V86) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V86)) end, fun (V87) -> fun (V88) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__Int'(V87, V88)) end end}}, {'Idris.Builtin.MkPair', V16, V17})))) end))(V19))), case V89 of {'Idris.Prelude.Types.Left', E37} -> (fun (V90) -> {'Idris.Prelude.Types.Left', V90} end(E37)); {'Idris.Prelude.Types.Right', E38} -> (fun (V91) -> begin (V92 = ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--exprSearchOpts'(V0, V6, V5, V3, V4, {'Idris.Core.Name.Resolved', V17}, [], V19))), case V92 of {'Idris.Prelude.Types.Left', E39} -> (fun (V93) -> {'Idris.Prelude.Types.Left', V93} end(E39)); {'Idris.Prelude.Types.Right', E40} -> (fun (V94) -> (('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--traverse'('erased', 'erased', fun (V95) -> begin (V96 = ('nested--12210-4008--in--un--dropLams'(V0, V1, V2, V3, V4, V5, V6, V81, V95))), fun (V97) -> begin (V98 = (('Idris.Idris2.Core.Normalise':'un--logTermNF'(V9, V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> <<"Got clause"/utf8>> end, V12, V11))(V97))), case V98 of {'Idris.Prelude.Types.Left', E41} -> (fun (V99) -> {'Idris.Prelude.Types.Left', V99} end(E41)); {'Idris.Prelude.Types.Right', E42} -> (fun (V100) -> begin (V101 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"        = "/utf8>>, ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__RawImp'(V96)))) end))(V97))), case V101 of {'Idris.Prelude.Types.Left', E43} -> (fun (V102) -> {'Idris.Prelude.Types.Left', V102} end(E43)); {'Idris.Prelude.Types.Right', E44} -> (fun (V103) -> {'Idris.Prelude.Types.Right', [('nested--12210-4007--in--un--updateRHS'(V0, V1, V2, V3, V4, V5, V6, V7, V96)) | []]} end(E44)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end, V94))(V19)) end(E40)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E38)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E35, E36)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V4, <<"No searchable hole on RHS"/utf8>>}, V19)) end end(E34)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V4, <<"No searchable hole on RHS"/utf8>>}, V19)) end end(E33)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3)); _ -> fun (V104) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V4, <<"No searchable hole on RHS"/utf8>>}, V104)) end end.
'case--case block in expandClause-4085'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V8 of {'Idris.Core.Context.MkClause', E0, E1, E2, E3} -> (fun (V10, V11, V12, V13) -> begin (V14 = {'Idris.Core.Context.MkClause', V10, V11, V12, V13}), ('case--case block in case block in expandClause-4108'(V0, V1, V2, V3, V4, V5, V6, V7, V9, V10, V13, V12, V11, V14, ('Idris.Idris2.Core.TT':'un--getFn'('erased', V13)))) end end(E0, E1, E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--expandClause-4063'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Prelude.Types.Right', E0} -> (fun (V9) -> begin (V10 = {'Idris.Prelude.Types.Right', V9}), case V9 of {'Idris.Core.Context.MkClause', E1, E2, E3, E4} -> (fun (V11, V12, V13, V14) -> begin (V15 = {'Idris.Core.Context.MkClause', V11, V12, V13, V14}), ('case--case block in case block in expandClause-4108'(V0, V1, V2, V3, V4, V5, V6, V7, V10, V11, V14, V13, V12, V15, ('Idris.Idris2.Core.TT':'un--getFn'('erased', V14)))) end end(E1, E2, E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E0)); {'Idris.Prelude.Types.Left', E5} -> (fun (V16) -> fun (V17) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V17)) end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in fnName-3946'(V0, V1) -> case V1 of 0 -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(V0, <<")"/utf8>>)))); 1 -> <<"op"/utf8>>; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--fnName-3933'(V0, V1, V2) -> case V2 of 0 -> V0; 1 -> case V1 of 0 -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"("/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(V0, <<")"/utf8>>)))); 1 -> <<"op"/utf8>>; _ -> ('erlang':'throw'("Error: Unreachable branch")) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--12690-4430--in--un--valid'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.TTImp.Interactive.CaseSplit.Valid', E0, E1} -> (fun (V9, V10) -> {'Idris.Prelude.Types.Just', V10} end(E0, E1)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'nested--12210-4007--in--un--updateRHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V7 of {'Idris.TTImp.TTImp.PatClause', E0, E1, E2} -> (fun (V9, V10, V11) -> {'Idris.TTImp.TTImp.PatClause', V9, V10, V8} end(E0, E1, E2)); {'Idris.TTImp.TTImp.WithClause', E3, E4, E5, E6, E7} -> (fun (V12, V13, V14, V15, V16) -> {'Idris.TTImp.TTImp.WithClause', V12, V13, V14, V15, V16} end(E3, E4, E5, E6, E7)); {'Idris.TTImp.TTImp.ImpossibleClause', E8, E9} -> (fun (V17, V18) -> {'Idris.TTImp.TTImp.ImpossibleClause', V17, V18} end(E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.TTImp.TTImp.IVar', E0, E1} -> (fun (V10, V11) -> ('case--trySplit,updateLHS-4461'(V0, V1, V2, V3, V4, V5, V6, V7, V11, V10, V8, ('Idris.Idris2.Data.List':'un--lookup'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V12) -> fun (V13) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V12, V13)) end end, fun (V14) -> fun (V15) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V14, V15)) end end}, V11, V8)))) end(E0, E1)); {'Idris.TTImp.TTImp.IBindVar', E2, E3} -> (fun (V16, V17) -> ('case--trySplit,updateLHS-4519'(V0, V1, V2, V3, V4, V5, V6, V7, V17, V16, V8, ('Idris.Idris2.Data.List':'un--lookup'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V18) -> fun (V19) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V18, V19)) end end, fun (V20) -> fun (V21) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V20, V21)) end end}, {'Idris.Core.Name.UN', V17}, V8)))) end(E2, E3)); {'Idris.TTImp.TTImp.IApp', E4, E5, E6} -> (fun (V22, V23, V24) -> {'Idris.TTImp.TTImp.IApp', V22, ('nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V23)), ('nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V24))} end(E4, E5, E6)); {'Idris.TTImp.TTImp.IImplicitApp', E7, E8, E9, E10} -> (fun (V25, V26, V27, V28) -> {'Idris.TTImp.TTImp.IImplicitApp', V25, ('nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V26)), V27, ('nested--12690-4432--in--un--updateLHS'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V28))} end(E7, E8, E9, E10)); _ -> V9 end.
'nested--12170-3967--in--un--mkUniqueName'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.TTImp.TTImp.IHole', E0, E1} -> (fun (V5, V6) -> fun (V7) -> begin (V36 = begin (V35 = (('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 (V8) -> fun (V9) -> fun (V10) -> fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V10, V11, V12)) end end end end end, fun (V13) -> fun (V14) -> fun (V15) -> V14 end end end, fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> begin (V21 = (V18(V20))), begin (V22 = (V19(V20))), (V21(V22)) end end end end end end end}, fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> begin (V28 = (V25(V27))), ((V26(V28))(V27)) end end end end end end, fun (V29) -> fun (V30) -> fun (V31) -> begin (V32 = (V30(V31))), (V32(V31)) end end end end}, fun (V33) -> fun (V34) -> V34 end end}, V3))(V7))), {'Idris.Prelude.Types.Right', V35} end), case V36 of {'Idris.Prelude.Types.Left', E2} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V38) -> begin (V39 = ('Idris.Idris2.TTImp.Utils':'un--uniqueName'(V38, [], V6, V7))), case V39 of {'Idris.Prelude.Types.Left', E4} -> (fun (V40) -> {'Idris.Prelude.Types.Left', V40} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V41) -> {'Idris.Prelude.Types.Right', {'Idris.TTImp.TTImp.IHole', V5, V41}} end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> fun (V42) -> {'Idris.Prelude.Types.Right', V4} end end.
'nested--13722-5348--in--un--getProp'(V0, V1) -> case V1 of [] -> {'Idris.Builtin.MkPair', 0, 0}; [E0 | E1] -> (fun (V2, V3) -> ('case--propBindableUsed,getProp-5366'(V0, V2, V3, ('nested--13722-5348--in--un--getProp'(V0, V3)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.TTImp.TTImp.IVar', E0, E1} -> (fun (V9, V10) -> case V10 of {'Idris.Core.Name.UN', E2} -> (fun (V11) -> {'Idris.TTImp.TTImp.IBindVar', V9, V11} end(E2)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V12, V13) -> {'Idris.TTImp.TTImp.Implicit', V9, 0} end(E3, E4)); _ -> V8 end end(E0, E1)); {'Idris.TTImp.TTImp.IApp', E5, E6, E7} -> (fun (V14, V15, V16) -> {'Idris.TTImp.TTImp.IApp', V14, ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V15)), ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V16))} end(E5, E6, E7)); {'Idris.TTImp.TTImp.IImplicitApp', E8, E9, E10, E11} -> (fun (V17, V18, V19, V20) -> {'Idris.TTImp.TTImp.IImplicitApp', V17, ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V18)), V19, ('nested--12690-4431--in--un--fixNames'(V0, V1, V2, V3, V4, V5, V6, V7, V20))} end(E8, E9, E10, E11)); _ -> V8 end.
'nested--12210-4008--in--un--dropLams'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V7 of 0 -> V8; _ -> begin (V9 = (V7 - 1)), case V8 of {'Idris.TTImp.TTImp.ILam', E0, E1, E2, E3, E4, E5} -> (fun (V10, V11, V12, V13, V14, V15) -> ('nested--12210-4008--in--un--dropLams'(V0, V1, V2, V3, V4, V5, V6, V9, V15)) end(E0, E1, E2, E3, E4, E5)); _ -> V8 end end end.
'un--uniqueRHS'(V0, V1) -> case V1 of {'Idris.TTImp.TTImp.PatClause', E0, E1, E2} -> (fun (V2, V3, V4) -> fun (V5) -> begin (V6 = (('nested--12170-3967--in--un--mkUniqueName'(V4, V3, V2, V0, V4))(V5))), case V6 of {'Idris.Prelude.Types.Left', E3} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V8) -> {'Idris.Prelude.Types.Right', {'Idris.TTImp.TTImp.PatClause', V2, V3, V8}} end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2)); _ -> fun (V9) -> {'Idris.Prelude.Types.Right', V1} end end.
'un--trySplit'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> begin (V9 = (('Idris.Idris2.TTImp.Interactive.CaseSplit':'un--getSplitsLHS'(V0, V1, V2, V3, 0, V5, V7))(V8))), case V9 of {'Idris.Prelude.Types.Left', E0} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V11) -> case V11 of {'Idris.TTImp.Interactive.CaseSplit.OK', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V7, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V13) -> {'Idris.TTImp.TTImp.PatClause', V3, ('nested--12690-4432--in--un--updateLHS'(V7, V6, V5, V4, V3, V2, V1, V0, V13, V4)), V6} end, ('Idris.Idris2.Data.List':'un--mapMaybe'('erased', 'erased', fun (V14) -> ('nested--12690-4430--in--un--valid'(V7, V6, V5, V4, V3, V2, V1, V0, V14)) end, V12))))}} end(E2)); _ -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V7, []}} end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--tryAllSplits'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of [] -> fun (V7) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V7)) end; [E0 | E1] -> (fun (V8, V9) -> case V8 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V10, V11) -> case V11 of [] -> ('un--tryAllSplits'(V0, V1, V2, V3, V4, V5, V9)); _ -> fun (V12) -> begin (V13 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Splitting on "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V10)))) end))(V12))), case V13 of {'Idris.Prelude.Types.Left', E4} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V15) -> (('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--trySearch'('erased', V0, V2, fun (V16) -> begin (V18 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V17) -> ('un--mkSplits'(V0, V1, V2, V3, V4, V5, V17)) end, V11))(V16))), case V18 of {'Idris.Prelude.Types.Left', E6} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V20) -> (('un--collectClauses'(V0, V2, V20))(V16)) end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end, ('un--tryAllSplits'(V0, V1, V2, V3, V4, V5, V9))))(V12)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--splittableNames'(V0) -> case V0 of {'Idris.TTImp.TTImp.IApp', E0, E1, E2} -> (fun (V1, V2, V3) -> case V3 of {'Idris.TTImp.TTImp.IBindVar', E3, E4} -> (fun (V4, V5) -> ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', ('un--splittableNames'(V2)), [{'Idris.Core.Name.UN', V5} | []])) end(E3, E4)); _ -> ('un--splittableNames'(V2)) end end(E0, E1, E2)); {'Idris.TTImp.TTImp.IImplicitApp', E5, E6, E7, E8} -> (fun (V6, V7, V8, V9) -> ('un--splittableNames'(V7)) end(E5, E6, E7, E8)); _ -> [] end.
'un--propBindableUsed'(V0) -> ('case--propBindableUsed-5434'(V0, ('nested--13722-5348--in--un--getProp'(V0, V0)))).
'un--mostUsed'(V0, V1) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Double'(('un--propBindableUsed'(V1)), ('un--propBindableUsed'(V0)))).
'un--mkSplits'(V0, V1, V2, V3, V4, V5, V6) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--trySearch'('erased', V0, V2, ('case--mkSplits-4934'(V0, V6, V5, V4, V3, V2, V1, case V4 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9} -> (fun (V7, V8, V9, V10, V11, V12, V13, V14, V15, V16) -> V14 end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)), fun (V17) -> begin (V18 = (('un--generateSplits'(V1, V0, V2, V3, V4, V5, V6))(V17))), case V18 of {'Idris.Prelude.Types.Left', E10} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V20) -> begin (V48 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Splits: "/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V21) -> ('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 (V22) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V22)) end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V23, V24)) end end}, {'Idris.Prelude.Show.dn--un--__mkShow', fun (V25) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V26) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__ImpClause'(V26)) end, fun (V27) -> fun (V28) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__ImpClause'(V27, V28)) end end}, V25)) end, fun (V29) -> fun (V30) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V31) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__ImpClause'(V31)) end, fun (V32) -> fun (V33) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__ImpClause'(V32, V33)) end end}, V29, V30)) end end}}, V21)) end, fun (V34) -> fun (V35) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V36) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V36)) end, fun (V37) -> fun (V38) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V37, V38)) end end}, {'Idris.Prelude.Show.dn--un--__mkShow', fun (V39) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V40) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__ImpClause'(V40)) end, fun (V41) -> fun (V42) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__ImpClause'(V41, V42)) end end}, V39)) end, fun (V43) -> fun (V44) -> ('Idris.Idris2.Prelude.Show':'dn--un--showPrec_Show__(List $a)'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V45) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__ImpClause'(V45)) end, fun (V46) -> fun (V47) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__ImpClause'(V46, V47)) end end}, V43, V44)) end end}}, V34, V35)) end end}, V20)))) end))(V17))), case V48 of {'Idris.Prelude.Types.Left', E12} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V50) -> (('un--tryAllSplits'(V0, V1, V2, V3, case V4 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E14, E15, E16, E17, E18, E19, E20, E21, E22, E23} -> (fun (V51, V52, V53, V54, V55, V56, V57, V58, V59, V60) -> {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', V51, V52, V53, V54, V55, V56, V57, 1, 0, V60} end(E14, E15, E16, E17, E18, E19, E20, E21, E22, E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5, V20))(V17)) end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end)).
'un--makeDefSort'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--searchSort'('erased', V0, V2, V4, fun (V8) -> ('un--makeDef'(V0, V1, V2, V3, V6, V8)) end, fun (V9) -> fun (V10) -> ((V5(('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V9))))(('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V10)))) end end, V7)).
'un--makeDefN'(V0, V1, V2, V3, V4, V5, V6) -> begin (V8 = ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--searchN'('erased', V0, V2, V4, fun (V7) -> ('un--makeDef'(V0, V1, V2, V3, V5, V7)) end, V6))), case V8 of {'Idris.Prelude.Types.Left', E0} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V10) -> case V10 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V11, V12) -> {'Idris.Prelude.Types.Right', V11} end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--makeDefFromType'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> ('Idris.Idris2.Core.UnifyState':'un--tryUnify'('erased', V0, V2, fun (V9) -> begin (V10 = ('Idris.Idris2.Core.Context':'un--branch'(V0, V9))), case V10 of {'Idris.Prelude.Types.Left', E0} -> (fun (V11) -> {'Idris.Prelude.Types.Left', V11} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V12) -> begin (V41 = begin (V40 = (('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 (V13) -> fun (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V15, V16, V17)) end end end end end, fun (V18) -> fun (V19) -> fun (V20) -> V19 end end end, fun (V21) -> fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> begin (V26 = (V23(V25))), begin (V27 = (V24(V25))), (V26(V27)) end end end end end end end}, fun (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> begin (V33 = (V30(V32))), ((V31(V33))(V32)) end end end end end end, fun (V34) -> fun (V35) -> fun (V36) -> begin (V37 = (V35(V36))), (V37(V36)) end end end end}, fun (V38) -> fun (V39) -> V39 end end}, V1))(V9))), {'Idris.Prelude.Types.Right', V40} end), case V41 of {'Idris.Prelude.Types.Left', E2} -> (fun (V42) -> {'Idris.Prelude.Types.Left', V42} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V43) -> begin (V72 = begin (V71 = (('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 (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> fun (V48) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V46, V47, V48)) end end end end end, fun (V49) -> fun (V50) -> fun (V51) -> V50 end end end, fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> fun (V56) -> begin (V57 = (V54(V56))), begin (V58 = (V55(V56))), (V57(V58)) end end end end end end end}, fun (V59) -> fun (V60) -> fun (V61) -> fun (V62) -> fun (V63) -> begin (V64 = (V61(V63))), ((V62(V64))(V63)) end end end end end end, fun (V65) -> fun (V66) -> fun (V67) -> begin (V68 = (V66(V67))), (V68(V67)) end end end end}, fun (V69) -> fun (V70) -> V70 end end}, V2))(V9))), {'Idris.Prelude.Types.Right', V71} end), case V72 of {'Idris.Prelude.Types.Left', E4} -> (fun (V73) -> {'Idris.Prelude.Types.Left', V73} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V74) -> begin (V78 = begin (V75 = (('Idris.Idris2.Core.Normalise':'un--nf'(V0, [], V12, {'Idris.Core.Env.Nil'}, V7))(V9))), case V75 of {'Idris.Prelude.Types.Left', E6} -> (fun (V76) -> {'Idris.Prelude.Types.Left', V76} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V77) -> (('Idris.Idris2.TTImp.Interactive.CaseSplit':'un--getEnvArgNames'(V0, V12, V6, V77))(V9)) end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V78 of {'Idris.Prelude.Types.Left', E8} -> (fun (V79) -> {'Idris.Prelude.Types.Left', V79} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V80) -> begin (V81 = ('Idris.Idris2.Data.List':'un--replicate'('erased', V6, {'Idris.TTImp.TTImp.Implicit', V3, 0}))), begin (V82 = ('Idris.Idris2.TTImp.Utils':'un--uniqueName'(V12, [], ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('un--fnName'(1, V5)), <<"_rhs"/utf8>>)), V9))), case V82 of {'Idris.Prelude.Types.Left', E10} -> (fun (V83) -> {'Idris.Prelude.Types.Left', V83} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V84) -> begin (V86 = {'Idris.TTImp.TTImp.PatClause', V3, ('Idris.Idris2.TTImp.TTImp':'un--apply'({'Idris.TTImp.TTImp.IVar', V3, V5}, ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V81, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V85) -> {'Idris.TTImp.TTImp.IBindVar', V3, V85} end, V80)))))), {'Idris.TTImp.TTImp.IHole', V3, V84}}), (('case--makeDefFromType-5066'(V7, V6, V5, V4, V3, V2, V1, V0, V12, V43, V74, V80, V81, V84, V86, ('Idris.Idris2.Core.Context':'un--getNameID'(V5, case V12 of {'Idris.Core.Context.MkDefs', E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37} -> (fun (V87, V88, V89, V90, V91, V92, V93, V94, V95, V96, V97, V98, V99, V100, V101, V102, V103, V104, V105, V106, V107, V108, V109, V110, V111, V112) -> V87 end(E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))))(V9)) end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E9)); _ -> ('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, fun (V113) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V113)) end, V8)).
'un--makeDef'(V0, V1, V2, V3, V4, V5) -> begin (V6 = ('Idris.Idris2.Core.Metadata':'un--findTyDeclAt'(V1, V3, 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) -> case V8 of {'Idris.Prelude.Types.Just', E2} -> (fun (V9) -> case V9 of {'Idris.Builtin.MkPair', E3, E4} -> (fun (V10, V11) -> case V11 of {'Idris.Builtin.MkPair', E5, E6} -> (fun (V12, V13) -> case V13 of {'Idris.Builtin.MkPair', E7, E8} -> (fun (V14, V15) -> begin (V16 = (('Idris.Idris2.Core.Context':'un--getFullName'(V0, V12))(V5))), case V16 of {'Idris.Prelude.Types.Left', E9} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V18) -> begin (V19 = ('Idris.Idris2.Core.Context.Log':'un--logTerm'([], V0, <<"interaction.generate"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Searching for "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)))) end, V15, V5))), case V19 of {'Idris.Prelude.Types.Left', E11} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V21) -> begin (V23 = begin (V22 = {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V10, {'Idris.Builtin.MkPair', V12, {'Idris.Builtin.MkPair', V14, V15}}}}), ('case--case block in makeDef-5280'(V4, V3, V2, V1, V0, V10, V12, V14, V15, V22, V18, V21, ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--initSearchOpts'(0, (1 + (1 + (1 + (1 + (1 + 0))))))))) end), ('un--makeDefFromType'(V0, V1, V2, V10, V23, V18, V14, V15, V5)) end end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E7, E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E3, E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E2)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V5)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--generateSplits'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.TTImp.TTImp.ImpossibleClause', E0, E1} -> (fun (V7, V8) -> fun (V9) -> {'Idris.Prelude.Types.Right', []} end end(E0, E1)); {'Idris.TTImp.TTImp.WithClause', E2, E3, E4, E5, E6} -> (fun (V10, V11, V12, V13, V14) -> fun (V15) -> {'Idris.Prelude.Types.Right', []} end end(E2, E3, E4, E5, E6)); {'Idris.TTImp.TTImp.PatClause', E7, E8, E9} -> (fun (V16, V17, V18) -> fun (V19) -> begin (V24 = (('Idris.Idris2.TTImp.Elab':'un--elabTerm'([], V1, V0, V2, V5, {'Idris.TTImp.Elab.Check.InLHS', ('Idris.Idris2.Algebra.Semiring':'un--linear'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V20) -> fun (V21) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V20, V21)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V22) -> fun (V23) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V22, V23)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))}, [], [], {'Idris.Core.Env.Nil'}, {'Idris.TTImp.TTImp.IBindHere', V3, {'Idris.TTImp.TTImp.PATTERN'}, V17}, {'Idris.Prelude.Types.Nothing'}))(V19))), case V24 of {'Idris.Prelude.Types.Left', E10} -> (fun (V25) -> {'Idris.Prelude.Types.Left', V25} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V26) -> case V26 of {'Idris.Builtin.MkPair', E12, E13} -> (fun (V27, V28) -> begin (V40 = begin (V29 = {'Idris.Builtin.MkPair', V27, V28}), ('case--case block in generateSplits-4709'(V18, V17, V16, V5, V4, V3, V2, V1, V0, V28, V27, V29, case V4 of {'Idris.TTImp.Interactive.ExprSearch.MkSearchOpts', E14, E15, E16, E17, E18, E19, E20, E21, E22, E23} -> (fun (V30, V31, V32, V33, V34, V35, V36, V37, V38, V39) -> V36 end(E14, E15, E16, E17, E18, E19, E20, E21, E22, E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end)) end), (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V41) -> fun (V42) -> ('un--trySplit'(V0, V1, V2, V16, V17, V27, V18, V41, V42)) end end, V40))(V19)) end end(E12, E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E7, E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--fnName'(V0, V1) -> case V1 of {'Idris.Core.Name.UN', E0} -> (fun (V2) -> ('case--fnName-3933'(V2, V0, ('Idris.Idris2.Parser.Lexer.Common':'un--isIdentNormal'(V2)))) end(E0)); {'Idris.Core.Name.NS', E1, E2} -> (fun (V3, V4) -> ('un--fnName'(V0, V4)) end(E1, E2)); {'Idris.Core.Name.DN', E3, E4} -> (fun (V5, V6) -> V5 end(E3, E4)); _ -> ('Idris.Idris2.Core.Name':'un--nameRoot'(V1)) end.
'un--expandClause'(V0, V1, V2, V3, V4, V5, V6, V7) -> begin (V8 = (('un--uniqueRHS'(V0, V6))(V7))), 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 (V15 = (('Idris.Idris2.TTImp.ProcessDef':'un--checkClause'([], V0, V1, V2, ('Idris.Idris2.Algebra.Semiring':'un--linear'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V11) -> fun (V12) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V11, V12)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V13) -> fun (V14) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V13, V14)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())})), {'Idris.Core.TT.Private'}, {'Idris.Core.TT.PartialOK'}, 1, V5, [], [], {'Idris.Core.Env.Nil'}, V10))(V7))), case V15 of {'Idris.Prelude.Types.Left', E2} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V17) -> case V17 of {'Idris.Prelude.Types.Right', E4} -> (fun (V18) -> begin (V19 = {'Idris.Prelude.Types.Right', V18}), case V18 of {'Idris.Core.Context.MkClause', E5, E6, E7, E8} -> (fun (V20, V21, V22, V23) -> begin (V24 = {'Idris.Core.Context.MkClause', V20, V21, V22, V23}), (('case--case block in case block in expandClause-4108'(V0, V6, V5, V4, V3, V2, V1, V10, V19, V20, V23, V22, V21, V24, ('Idris.Idris2.Core.TT':'un--getFn'('erased', V23))))(V7)) end end(E5, E6, E7, E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E4)); {'Idris.Prelude.Types.Left', E9} -> (fun (V25) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--noResult'('erased', V7)) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--collectClauses'(V0, V1, V2) -> case V2 of [] -> fun (V3) -> ('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--one'('erased', [], V3)) end; [E0 | E1] -> (fun (V4, V5) -> fun (V6) -> begin (V7 = (('un--collectClauses'(V0, V1, V5))(V6))), case V7 of {'Idris.Prelude.Types.Left', E2} -> (fun (V8) -> {'Idris.Prelude.Types.Left', V8} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V9) -> (('Idris.Idris2.TTImp.Interactive.ExprSearch':'un--combine'('erased', 'erased', 'erased', V0, V1, fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V10, V11)) end end, V4, V9))(V6)) end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--bindableUsed'(V0) -> case V0 of {'Idris.TTImp.TTImp.PatClause', E0, E1, E2} -> (fun (V1, V2, V3) -> begin (V4 = ('Idris.Idris2.TTImp.Utils':'un--findIBindVars'(V2))), begin (V5 = ('Idris.Idris2.TTImp.Utils':'un--findAllNames'([], V3))), {'Idris.Prelude.Types.Just', {'Idris.Builtin.MkPair', V4, ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V6) -> ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V7) -> fun (V8) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V7, V8)) end end, fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V9, V10)) end end}, V6, V4)) end, V5))}} end end end(E0, E1, E2)); _ -> {'Idris.Prelude.Types.Nothing'} end.