-module('Idris.Idris2.TTImp.ProcessType').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--case block in case block in processType-12598'/31,
  'case--case block in processType-12334'/25,
  'case--processType-12236'/20,
  'case--case block in findInferrable,findInf-11979'/9,
  'case--findInferrable,findInf-11938'/8,
  'case--getFnString-11773'/10,
  'case--case block in processFnOpt-11678'/11,
  'case--processFnOpt-11603'/6,
  'case--processFnOpt,collectSpec-11410'/18,
  'case--processFnOpt,getDeps-11296'/14,
  'case--processFnOpt,getDeps-11220'/13,
  'case--case block in processFnOpt,getDeps,splitPs-11114'/18,
  'case--processFnOpt,getDeps,splitPs-11073'/16,
  'case--processFnOpt,collectDDeps-10803'/15,
  'case--case block in processFnOpt,insertDeps-10718'/10,
  'case--processFnOpt,insertDeps-10675'/9,
  'case--processFnOpt-10592'/6,
  'nested--9518-11047--in--un--splitPs'/14,
  'nested--9417-10654--in--un--insertDeps'/7,
  'nested--9417-10659--in--un--getNamePos'/6,
  'nested--9417-10656--in--un--getDepsArgs'/7,
  'nested--9417-10657--in--un--getDeps'/7,
  'nested--10875-11912--in--un--findInfs'/6,
  'nested--10875-11911--in--un--findInf'/6,
  'nested--10875-11913--in--un--fi'/8,
  'nested--9417-10658--in--un--collectSpec'/8,
  'nested--9417-10655--in--un--collectDDeps'/5,
  'un--processType'/12,
  'un--processFnOpt'/4,
  'un--initDef'/8,
  'un--getRetTy'/2,
  'un--getFnString'/4,
  'un--findInferrable'/3
]).
'case--case block in case block in processType-12598'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30) -> case V30 of {'Idris.Core.Context.MkGlobalDef', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20} -> (fun (V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51) -> {'Idris.Core.Context.MkGlobalDef', V31, V32, V33, V24, V25, V36, V29, V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51} end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in processType-12334'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24) -> case V24 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V25, V26) -> fun (V27) -> begin (V56 = begin (V55 = (('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 (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V30, V31, V32)) end end end end end, fun (V33) -> fun (V34) -> fun (V35) -> V34 end end end, fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V38(V40))), begin (V42 = (V39(V40))), (V41(V42)) end end end end end end end}, fun (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> begin (V48 = (V45(V47))), ((V46(V48))(V47)) end end end end end end, fun (V49) -> fun (V50) -> fun (V51) -> begin (V52 = (V50(V51))), (V52(V51)) end end end end}, fun (V53) -> fun (V54) -> V54 end end}, V13))(V27))), {'Idris.Prelude.Types.Right', V55} end), case V56 of {'Idris.Prelude.Types.Left', E2} -> (fun (V57) -> {'Idris.Prelude.Types.Left', V57} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V58) -> begin (V59 = ('Idris.Idris2.Core.Context':'un--clearDefs'(V58, V27))), case V59 of {'Idris.Prelude.Types.Left', E4} -> (fun (V60) -> {'Idris.Prelude.Types.Left', V60} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V61) -> begin (V65 = begin (V62 = (('Idris.Idris2.Core.Normalise':'un--nf'(V13, [], V58, {'Idris.Core.Env.Nil'}, V23))(V27))), case V62 of {'Idris.Prelude.Types.Left', E6} -> (fun (V63) -> {'Idris.Prelude.Types.Left', V63} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V64) -> (('un--findInferrable'(V13, V61, V64))(V27)) end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V65 of {'Idris.Prelude.Types.Left', E8} -> (fun (V66) -> {'Idris.Prelude.Types.Left', V66} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V67) -> begin (V69 = ('Idris.Idris2.Core.Context':'un--addDef'(V13, {'Idris.Core.Name.Resolved', V17}, begin (V68 = {'Idris.Builtin.MkPair', V25, V26}), ('case--case block in case block in processType-12598'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V25, V26, V68, V58, V61, V67, ('Idris.Idris2.Core.Context':'un--newDef'(V6, V14, V5, V7, V23, V4, V22)))) end, V27))), case V69 of {'Idris.Prelude.Types.Left', E10} -> (fun (V70) -> {'Idris.Prelude.Types.Left', V70} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V71) -> begin (V76 = case ('Idris.Idris2.Prelude.Basics':'un--not'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V72) -> fun (V73) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--==_Eq__ElabOpt'(V72, V73)) end end, fun (V74) -> fun (V75) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--/=_Eq__ElabOpt'(V74, V75)) end end}, {'Idris.TTImp.Elab.Check.InCase'}, V10)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setLinearCheck'(V13, V17, 0, V27)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end), case V76 of {'Idris.Prelude.Types.Left', E12} -> (fun (V77) -> {'Idris.Prelude.Types.Left', V77} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V78) -> begin (V82 = (('Idris.Idris2.Core.Context.Log':'un--log'(V13, <<"declare.type"/utf8>>, (1 + (1 + 0)), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Setting options for "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V14)), ('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 (V79) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__FnOpt'(V79)) end, fun (V80) -> fun (V81) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__FnOpt'(V80, V81)) end end}, V3)))))))) end))(V27))), case V82 of {'Idris.Prelude.Types.Left', E14} -> (fun (V83) -> {'Idris.Prelude.Types.Left', V83} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V84) -> begin (V85 = {'Idris.Core.Name.Resolved', V17}), begin (V87 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V86) -> ('un--processFnOpt'(V13, V6, V85, V86)) end, V3))(V27))), case V87 of {'Idris.Prelude.Types.Left', E16} -> (fun (V88) -> {'Idris.Prelude.Types.Left', V88} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V89) -> begin (V104 = begin (V90 = ('Idris.Idris2.Core.Context':'un--getDefaultTotalityOption'(V13, V27))), case V90 of {'Idris.Prelude.Types.Left', E18} -> (fun (V91) -> {'Idris.Prelude.Types.Left', V91} end(E18)); {'Idris.Prelude.Types.Right', E19} -> (fun (V92) -> case ('Idris.Idris2.Prelude.Basics':'un--not'((('Idris.Idris2.Prelude.Interfaces':'un--any'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkFoldable', fun (V93) -> fun (V94) -> fun (V95) -> fun (V96) -> fun (V97) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', V95, V96, V97)) end end end end end, fun (V98) -> fun (V99) -> fun (V100) -> fun (V101) -> fun (V102) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldl_Foldable__List'('erased', 'erased', V100, V101, V102)) end end end end end}, fun (V103) -> ('Idris.Idris2.TTImp.TTImp':'un--isTotalityReq'(V103)) end))(V3)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setFlag'(V13, V6, V85, {'Idris.Core.Context.SetTotal', V92}, V27)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E19)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V104 of {'Idris.Prelude.Types.Left', E20} -> (fun (V105) -> {'Idris.Prelude.Types.Left', V105} end(E20)); {'Idris.Prelude.Types.Right', E21} -> (fun (V106) -> begin (V107 = ('Idris.Idris2.Core.Metadata':'un--addTyDecl'(V7, V13, V12, V6, {'Idris.Core.Name.Resolved', V17}, V8, V20, V27))), case V107 of {'Idris.Prelude.Types.Left', E22} -> (fun (V108) -> {'Idris.Prelude.Types.Left', V108} end(E22)); {'Idris.Prelude.Types.Right', E23} -> (fun (V109) -> begin (V110 = ('Idris.Idris2.Core.Metadata':'un--addNameType'(V7, V13, V12, V6, {'Idris.Core.Name.Resolved', V17}, V8, V20, V27))), case V110 of {'Idris.Prelude.Types.Left', E24} -> (fun (V111) -> {'Idris.Prelude.Types.Left', V111} end(E24)); {'Idris.Prelude.Types.Right', E25} -> (fun (V112) -> begin (V115 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V113) -> fun (V114) -> ('Idris.Idris2.Core.Context':'un--addToSave'(V13, V113, V114)) end end, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V20))))))(V27))), case V115 of {'Idris.Prelude.Types.Left', E26} -> (fun (V116) -> {'Idris.Prelude.Types.Left', V116} end(E26)); {'Idris.Prelude.Types.Right', E27} -> (fun (V117) -> begin (V118 = ('Idris.Idris2.Core.Context':'un--addToSave'(V13, V14, V27))), case V118 of {'Idris.Prelude.Types.Left', E28} -> (fun (V119) -> {'Idris.Prelude.Types.Left', V119} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V120) -> begin (V124 = (('Idris.Idris2.Core.Context.Log':'un--log'(V13, <<"declare.type"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Saving from "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V14)), ('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 (V121) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V121)) end, fun (V122) -> fun (V123) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V122, V123)) end end}, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V20)))))))))))) end))(V27))), case V124 of {'Idris.Prelude.Types.Left', E30} -> (fun (V125) -> {'Idris.Prelude.Types.Left', V125} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V126) -> case ('Idris.Idris2.Core.TT':'dn--un--/=_Eq__Visibility'(V4, {'Idris.Core.TT.Private'})) of 0 -> begin (V134 = ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V13, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V127) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__Name'(V127)) end, fun (V128) -> fun (V129) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__Name'(V128, V129)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V130) -> fun (V131) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(V130, V131)) end end, fun (V132) -> fun (V133) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__Name'(V132, V133)) end end}, V14, V27))), case V134 of {'Idris.Prelude.Types.Left', E32} -> (fun (V135) -> {'Idris.Prelude.Types.Left', V135} end(E32)); {'Idris.Prelude.Types.Right', E33} -> (fun (V136) -> ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V13, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V137) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__(Term $vars)'('erased', V137)) end, fun (V138) -> fun (V139) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__(Term $vars)'('erased', V138, V139)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V140) -> fun (V141) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__(Term $vars)'('erased', V140, V141)) end end, fun (V142) -> fun (V143) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', V142, V143)) end end}, V20, V27)) end(E33)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) 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 end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processType-12236'(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.Nothing'} -> (fun () -> fun (V20) -> begin (V27 = ((('Idris.Idris2.TTImp.Elab.Utils':'un--wrapErrorC'('erased', V10, fun (V26) -> {'Idris.Core.Core.InType', V6, V14, V26} end))(fun (V21) -> ('Idris.Idris2.TTImp.Elab':'un--checkTerm'(V7, V13, V12, V11, V17, {'Idris.TTImp.Elab.Check.InType'}, [{'Idris.TTImp.Elab.Check.HolesOkay'} | V10], V9, V8, {'Idris.TTImp.TTImp.IBindHere', V6, {'Idris.TTImp.TTImp.PI', ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V22) -> fun (V23) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V22, V23)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V24) -> fun (V25) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V24, V25)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))}, V0}, ('Idris.Idris2.Core.Normalise':'un--gType'('erased', V6)), V21)) end))(V20))), case V27 of {'Idris.Prelude.Types.Left', E0} -> (fun (V28) -> {'Idris.Prelude.Types.Left', V28} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V29) -> begin (V30 = (('Idris.Idris2.Core.Normalise':'un--logTermNF'([], V13, <<"declare.type"/utf8>>, (1 + (1 + (1 + 0))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Type of "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V14)))) end, {'Idris.Core.Env.Nil'}, ('Idris.Idris2.Core.Env':'un--abstractFullEnvType'(V7, V2, V8, V29))))(V20))), case V30 of {'Idris.Prelude.Types.Left', E2} -> (fun (V31) -> {'Idris.Prelude.Types.Left', V31} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V32) -> begin (V33 = (('un--initDef'(V7, V13, V12, V11, V14, V8, V29, V3))(V20))), case V33 of {'Idris.Prelude.Types.Left', E4} -> (fun (V34) -> {'Idris.Prelude.Types.Left', V34} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V35) -> begin (V36 = ('Idris.Idris2.Core.Env':'un--abstractFullEnvType'(V7, V2, V8, V29))), begin (V37 = ('Idris.Idris2.TTImp.Elab.Utils':'un--findErased'(V13, V36, V20))), case V37 of {'Idris.Prelude.Types.Left', E6} -> (fun (V38) -> {'Idris.Prelude.Types.Left', V38} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V39) -> begin (V40 = {'Idris.Prelude.Types.Nothing'}), case V39 of {'Idris.Builtin.MkPair', E8, E9} -> (fun (V41, V42) -> begin (V71 = begin (V70 = (('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 (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V45, V46, V47)) end end end end end, fun (V48) -> fun (V49) -> fun (V50) -> V49 end end end, fun (V51) -> fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> begin (V56 = (V53(V55))), begin (V57 = (V54(V55))), (V56(V57)) end end end end end end end}, fun (V58) -> fun (V59) -> fun (V60) -> fun (V61) -> fun (V62) -> begin (V63 = (V60(V62))), ((V61(V63))(V62)) end end end end end end, fun (V64) -> fun (V65) -> fun (V66) -> begin (V67 = (V65(V66))), (V67(V66)) end end end end}, fun (V68) -> fun (V69) -> V69 end end}, V13))(V20))), {'Idris.Prelude.Types.Right', V70} end), case V71 of {'Idris.Prelude.Types.Left', E10} -> (fun (V72) -> {'Idris.Prelude.Types.Left', V72} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V73) -> begin (V74 = ('Idris.Idris2.Core.Context':'un--clearDefs'(V73, V20))), case V74 of {'Idris.Prelude.Types.Left', E12} -> (fun (V75) -> {'Idris.Prelude.Types.Left', V75} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V76) -> begin (V80 = begin (V77 = (('Idris.Idris2.Core.Normalise':'un--nf'(V13, [], V73, {'Idris.Core.Env.Nil'}, V36))(V20))), case V77 of {'Idris.Prelude.Types.Left', E14} -> (fun (V78) -> {'Idris.Prelude.Types.Left', V78} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V79) -> (('un--findInferrable'(V13, V76, V79))(V20)) end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V80 of {'Idris.Prelude.Types.Left', E16} -> (fun (V81) -> {'Idris.Prelude.Types.Left', V81} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V82) -> begin (V84 = ('Idris.Idris2.Core.Context':'un--addDef'(V13, {'Idris.Core.Name.Resolved', V17}, begin (V83 = {'Idris.Builtin.MkPair', V41, V42}), ('case--case block in case block in processType-12598'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V40, V29, V32, V35, V36, V41, V42, V83, V73, V76, V82, ('Idris.Idris2.Core.Context':'un--newDef'(V6, V14, V5, V7, V36, V4, V35)))) end, V20))), case V84 of {'Idris.Prelude.Types.Left', E18} -> (fun (V85) -> {'Idris.Prelude.Types.Left', V85} end(E18)); {'Idris.Prelude.Types.Right', E19} -> (fun (V86) -> begin (V91 = case ('Idris.Idris2.Prelude.Basics':'un--not'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V87) -> fun (V88) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--==_Eq__ElabOpt'(V87, V88)) end end, fun (V89) -> fun (V90) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--/=_Eq__ElabOpt'(V89, V90)) end end}, {'Idris.TTImp.Elab.Check.InCase'}, V10)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setLinearCheck'(V13, V17, 0, V20)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end), case V91 of {'Idris.Prelude.Types.Left', E20} -> (fun (V92) -> {'Idris.Prelude.Types.Left', V92} end(E20)); {'Idris.Prelude.Types.Right', E21} -> (fun (V93) -> begin (V97 = (('Idris.Idris2.Core.Context.Log':'un--log'(V13, <<"declare.type"/utf8>>, (1 + (1 + 0)), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Setting options for "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V14)), ('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 (V94) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__FnOpt'(V94)) end, fun (V95) -> fun (V96) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__FnOpt'(V95, V96)) end end}, V3)))))))) end))(V20))), case V97 of {'Idris.Prelude.Types.Left', E22} -> (fun (V98) -> {'Idris.Prelude.Types.Left', V98} end(E22)); {'Idris.Prelude.Types.Right', E23} -> (fun (V99) -> begin (V100 = {'Idris.Core.Name.Resolved', V17}), begin (V102 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V101) -> ('un--processFnOpt'(V13, V6, V100, V101)) end, V3))(V20))), case V102 of {'Idris.Prelude.Types.Left', E24} -> (fun (V103) -> {'Idris.Prelude.Types.Left', V103} end(E24)); {'Idris.Prelude.Types.Right', E25} -> (fun (V104) -> begin (V119 = begin (V105 = ('Idris.Idris2.Core.Context':'un--getDefaultTotalityOption'(V13, V20))), case V105 of {'Idris.Prelude.Types.Left', E26} -> (fun (V106) -> {'Idris.Prelude.Types.Left', V106} end(E26)); {'Idris.Prelude.Types.Right', E27} -> (fun (V107) -> case ('Idris.Idris2.Prelude.Basics':'un--not'((('Idris.Idris2.Prelude.Interfaces':'un--any'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkFoldable', fun (V108) -> fun (V109) -> fun (V110) -> fun (V111) -> fun (V112) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', V110, V111, V112)) end end end end end, fun (V113) -> fun (V114) -> fun (V115) -> fun (V116) -> fun (V117) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldl_Foldable__List'('erased', 'erased', V115, V116, V117)) end end end end end}, fun (V118) -> ('Idris.Idris2.TTImp.TTImp':'un--isTotalityReq'(V118)) end))(V3)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setFlag'(V13, V6, V100, {'Idris.Core.Context.SetTotal', V107}, V20)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V119 of {'Idris.Prelude.Types.Left', E28} -> (fun (V120) -> {'Idris.Prelude.Types.Left', V120} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V121) -> begin (V122 = ('Idris.Idris2.Core.Metadata':'un--addTyDecl'(V7, V13, V12, V6, {'Idris.Core.Name.Resolved', V17}, V8, V29, V20))), case V122 of {'Idris.Prelude.Types.Left', E30} -> (fun (V123) -> {'Idris.Prelude.Types.Left', V123} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V124) -> begin (V125 = ('Idris.Idris2.Core.Metadata':'un--addNameType'(V7, V13, V12, V6, {'Idris.Core.Name.Resolved', V17}, V8, V29, V20))), case V125 of {'Idris.Prelude.Types.Left', E32} -> (fun (V126) -> {'Idris.Prelude.Types.Left', V126} end(E32)); {'Idris.Prelude.Types.Right', E33} -> (fun (V127) -> begin (V130 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V128) -> fun (V129) -> ('Idris.Idris2.Core.Context':'un--addToSave'(V13, V128, V129)) end end, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V29))))))(V20))), case V130 of {'Idris.Prelude.Types.Left', E34} -> (fun (V131) -> {'Idris.Prelude.Types.Left', V131} end(E34)); {'Idris.Prelude.Types.Right', E35} -> (fun (V132) -> begin (V133 = ('Idris.Idris2.Core.Context':'un--addToSave'(V13, V14, V20))), case V133 of {'Idris.Prelude.Types.Left', E36} -> (fun (V134) -> {'Idris.Prelude.Types.Left', V134} end(E36)); {'Idris.Prelude.Types.Right', E37} -> (fun (V135) -> begin (V139 = (('Idris.Idris2.Core.Context.Log':'un--log'(V13, <<"declare.type"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Saving from "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V14)), ('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 (V136) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V136)) end, fun (V137) -> fun (V138) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V137, V138)) end end}, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V29)))))))))))) end))(V20))), case V139 of {'Idris.Prelude.Types.Left', E38} -> (fun (V140) -> {'Idris.Prelude.Types.Left', V140} end(E38)); {'Idris.Prelude.Types.Right', E39} -> (fun (V141) -> case ('Idris.Idris2.Core.TT':'dn--un--/=_Eq__Visibility'(V4, {'Idris.Core.TT.Private'})) of 0 -> begin (V149 = ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V13, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V142) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__Name'(V142)) end, fun (V143) -> fun (V144) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__Name'(V143, V144)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V145) -> fun (V146) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(V145, V146)) end end, fun (V147) -> fun (V148) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__Name'(V147, V148)) end end}, V14, V20))), case V149 of {'Idris.Prelude.Types.Left', E40} -> (fun (V150) -> {'Idris.Prelude.Types.Left', V150} end(E40)); {'Idris.Prelude.Types.Right', E41} -> (fun (V151) -> ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V13, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V152) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__(Term $vars)'('erased', V152)) end, fun (V153) -> fun (V154) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__(Term $vars)'('erased', V153, V154)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V155) -> fun (V156) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__(Term $vars)'('erased', V155, V156)) end end, fun (V157) -> fun (V158) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', V157, V158)) end end}, V29, V20)) end(E41)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E37)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E35)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E33)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E19)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.Prelude.Types.Just', E42} -> (fun (V159) -> fun (V160) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.AlreadyDefined', V6, V14}, V160)) end end(E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in findInferrable,findInf-11979'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of 0 -> fun (V9) -> {'Idris.Prelude.Types.Right', V6} end; 1 -> fun (V10) -> {'Idris.Prelude.Types.Right', [V7 | V6]} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--findInferrable,findInf-11938'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V8) -> {'Idris.Prelude.Types.Right', V6} end end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V9) -> ('case--case block in findInferrable,findInf-11979'(V0, V1, V2, V3, V4, V5, V6, V9, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.Types':'dn--un--/=_Eq__Nat'(V12, V13)) end end}, V9, V6)))) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--getFnString-11773'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.TT.Str', E2} -> (fun (V12) -> fun (V13) -> {'Idris.Prelude.Types.Right', V12} end end(E2)); _ -> fun (V14) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V5, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V14)) end end end(E0, E1)); _ -> fun (V15) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V5, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V15)) end end.
'case--case block in processFnOpt-11678'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V5 of {'Idris.Core.Context.MkGlobalDef', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20} -> (fun (V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31) -> {'Idris.Core.Context.MkGlobalDef', V11, V12, V13, V14, V15, V10, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31} end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt-11603'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> begin (V29 = (('Idris.Idris2.Core.Normalise':'un--nf'(V3, [], V4, {'Idris.Core.Env.Nil'}, case V6 of {'Idris.Core.Context.MkGlobalDef', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21} -> (fun (V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28) -> V10 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V7))), case V29 of {'Idris.Prelude.Types.Left', E22} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E22)); {'Idris.Prelude.Types.Right', E23} -> (fun (V31) -> begin (V32 = (('nested--9417-10659--in--un--getNamePos'(V0, V1, V2, V3, 0, V31))(V7))), case V32 of {'Idris.Prelude.Types.Left', E24} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E24)); {'Idris.Prelude.Types.Right', E25} -> (fun (V34) -> begin (V35 = (('nested--9417-10655--in--un--collectDDeps'(V0, V1, V2, V3, V31))(V7))), case V35 of {'Idris.Prelude.Types.Left', E26} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E26)); {'Idris.Prelude.Types.Right', E27} -> (fun (V37) -> begin (V38 = (('nested--9417-10658--in--un--collectSpec'(V0, V1, V2, V3, [], V37, V34, V31))(V7))), case V38 of {'Idris.Prelude.Types.Left', E28} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V40) -> begin (V62 = ('Idris.Idris2.Core.Context':'un--addDef'(V3, V1, case V6 of {'Idris.Core.Context.MkGlobalDef', E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50} -> (fun (V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61) -> {'Idris.Core.Context.MkGlobalDef', V41, V42, V43, V44, V45, V40, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61} end(E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))), case V62 of {'Idris.Prelude.Types.Left', E51} -> (fun (V63) -> {'Idris.Prelude.Types.Left', V63} end(E51)); {'Idris.Prelude.Types.Right', E52} -> (fun (V64) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end(E52)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V65) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V2, V1}, V65)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,collectSpec-11410'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of 0 -> fun (V18) -> begin (V19 = (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, 0, V7, ('Idris.Idris2.Data.NameMap':'un--empty'('erased'))))(V18))), case V19 of {'Idris.Prelude.Types.Left', E0} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V21) -> begin (V27 = ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V22) -> ('Idris.Idris2.Prelude.Basics':'un--||'(('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V22)), fun () -> ('Idris.Idris2.Prelude.Basics':'un--not'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V23) -> fun (V24) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V23, V24)) end end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V25, V26)) end end}, ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V22)), V12)))) end)) end, ('Idris.Idris2.Data.NameMap':'un--toList'('erased', V21))))), begin (V29 = ('nested--9417-10654--in--un--insertDeps'(V0, V1, V2, V3, V13, V11, [V9 | ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V28) -> ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V28)) end, V27))]))), (('nested--9417-10658--in--un--collectSpec'(V0, V1, V2, V3, V29, V12, V11, V16))(V18)) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; 1 -> ('nested--9417-10658--in--un--collectSpec'(V0, V1, V2, V3, V13, V12, V11, V16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,getDeps-11296'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13) -> case V13 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V14, V15) -> fun (V16) -> begin (V21 = begin (V18 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V17) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, [], V11, V17)) end, V14))(V16))), case V18 of {'Idris.Prelude.Types.Left', E2} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V20) -> (('nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, 0, V20, V9))(V16)) end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V21 of {'Idris.Prelude.Types.Left', E4} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V23) -> begin (V25 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V24) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, [], V11, V24)) end, V15))(V16))), case V25 of {'Idris.Prelude.Types.Left', E6} -> (fun (V26) -> {'Idris.Prelude.Types.Left', V26} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V27) -> (('nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, 1, V27, V23))(V16)) end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,getDeps-11220'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Prelude.Types.Just', E0} -> (fun (V13) -> case V13 of {'Idris.Core.Context.TCon', E1, E2, E3, E4, E5, E6, E7, E8} -> (fun (V14, V15, V16, V17, V18, V19, V20, V21) -> fun (V22) -> {'Idris.Prelude.Types.Right', V16} end end(E1, E2, E3, E4, E5, E6, E7, E8)); _ -> fun (V23) -> {'Idris.Prelude.Types.Right', []} end end end(E0)); _ -> fun (V24) -> {'Idris.Prelude.Types.Right', []} end end.
'case--case block in processFnOpt,getDeps,splitPs-11114'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of 0 -> {'Idris.Builtin.MkPair', [V11 | V15], V16}; 1 -> {'Idris.Builtin.MkPair', V15, [V11 | V16]}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,getDeps,splitPs-11073'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15) -> case V15 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V16, V17) -> ('case--case block in processFnOpt,getDeps,splitPs-11114'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V16, V17, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V18, V19)) end end, fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.Types':'dn--un--/=_Eq__Nat'(V20, V21)) end end}, V14, V13)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,collectDDeps-10803'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14) -> case V14 of 0 -> ('nested--9417-10655--in--un--collectDDeps'(V0, V1, V2, V3, V13)); 1 -> fun (V15) -> begin (V16 = ('Idris.Idris2.Core.Normalise':'dn--un--quote_Quote__NF'(V3, [], V12, {'Idris.Core.Env.Nil'}, V7, V15))), case V16 of {'Idris.Prelude.Types.Left', E0} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V18) -> begin (V19 = ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getRefs'('erased', {'Idris.Core.Name.UN', <<"_"/utf8>>}, V18))))), begin (V20 = (('nested--9417-10655--in--un--collectDDeps'(V0, V1, V2, V3, V13))(V15))), case V20 of {'Idris.Prelude.Types.Left', E2} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V22) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V22, V19))} end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in processFnOpt,insertDeps-10718'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of 0 -> ('nested--9417-10654--in--un--insertDeps'(V0, V1, V2, V3, V7, V6, V5)); 1 -> ('nested--9417-10654--in--un--insertDeps'(V0, V1, V2, V3, [V8 | V7], V6, V5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt,insertDeps-10675'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('nested--9417-10654--in--un--insertDeps'(V0, V1, V2, V3, V7, V6, V5)) end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V9) -> ('case--case block in processFnOpt,insertDeps-10718'(V0, V1, V2, V3, V4, V5, V6, V7, V9, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.Types':'dn--un--/=_Eq__Nat'(V12, V13)) end end}, V9, V7)))) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--processFnOpt-10592'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> fun (V7) -> begin (V11 = begin (V8 = (('Idris.Idris2.Core.Normalise':'un--nf'(V3, [], V4, {'Idris.Core.Env.Nil'}, V6))(V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> (('un--getRetTy'(V4, V10))(V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V11 of {'Idris.Prelude.Types.Left', E3} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V13) -> ('Idris.Idris2.Core.Context':'un--addHintFor'(V3, V2, V13, V1, V0, 1, V7)) end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V14) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V2, V1}, V14)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9518-11047--in--un--splitPs'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13) -> case V13 of [] -> {'Idris.Builtin.MkPair', [], []}; [E0 | E1] -> (fun (V14, V15) -> ('case--processFnOpt,getDeps,splitPs-11073'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V14, V15, V12, V11, ('nested--9518-11047--in--un--splitPs'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types':'dn--un--fromInteger_Num__Nat'(1)), V11)), V12, V15)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9417-10654--in--un--insertDeps'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of [] -> V4; [E0 | E1] -> (fun (V7, V8) -> ('case--processFnOpt,insertDeps-10675'(V0, V1, V2, V3, V7, V8, V5, V4, ('Idris.Idris2.Data.List':'un--lookup'('erased', '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, V5)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9417-10659--in--un--getNamePos'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V6, V7, V8, V9) -> case V8 of {'Idris.Core.TT.Pi', E4, E5, E6, E7} -> (fun (V10, V11, V12, V13) -> fun (V14) -> begin (V43 = begin (V42 = (('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 (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V17, V18, V19)) end end end end end, fun (V20) -> fun (V21) -> fun (V22) -> V21 end end end, fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> begin (V28 = (V25(V27))), begin (V29 = (V26(V27))), (V28(V29)) end end end end end end end}, fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> begin (V35 = (V32(V34))), ((V33(V35))(V34)) end end end end end end, fun (V36) -> fun (V37) -> fun (V38) -> begin (V39 = (V37(V38))), (V39(V38)) end end end end}, fun (V40) -> fun (V41) -> V41 end end}, V3))(V14))), {'Idris.Prelude.Types.Right', V42} end), case V43 of {'Idris.Prelude.Types.Left', E8} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V45) -> begin (V49 = begin (V46 = (((V9(V45))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Erased', V6, 1}))))(V14))), case V46 of {'Idris.Prelude.Types.Left', E10} -> (fun (V47) -> {'Idris.Prelude.Types.Left', V47} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V48) -> (('nested--9417-10659--in--un--getNamePos'(V0, V1, V2, V3, ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types':'dn--un--fromInteger_Num__Nat'(1)), V4)), V48))(V14)) end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V49 of {'Idris.Prelude.Types.Left', E12} -> (fun (V50) -> {'Idris.Prelude.Types.Left', V50} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V51) -> {'Idris.Prelude.Types.Right', [{'Idris.Builtin.MkPair', V7, V4} | V51]} end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5, E6, E7)); _ -> fun (V52) -> {'Idris.Prelude.Types.Right', []} end end end(E0, E1, E2, E3)); _ -> fun (V53) -> {'Idris.Prelude.Types.Right', []} end end.
'nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, V4, V5, V6) -> case V5 of [] -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end; [E0 | E1] -> (fun (V8, V9) -> fun (V10) -> begin (V11 = (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, V4, V8, V6))(V10))), case V11 of {'Idris.Prelude.Types.Left', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V13) -> (('nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, V4, V9, V13))(V10)) end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, V4, V5, V6) -> case V5 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V7, V8, V9, V10) -> case V9 of {'Idris.Core.TT.Pi', E10, E11, E12, E13} -> (fun (V11, V12, V13, V14) -> fun (V15) -> begin (V16 = (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, V4, V14, V6))(V15))), case V16 of {'Idris.Prelude.Types.Left', E14} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V18) -> begin (V47 = begin (V46 = (('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 (V19) -> fun (V20) -> fun (V21) -> fun (V22) -> fun (V23) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V21, V22, V23)) end end end end end, fun (V24) -> fun (V25) -> fun (V26) -> V25 end end end, fun (V27) -> fun (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> begin (V32 = (V29(V31))), begin (V33 = (V30(V31))), (V32(V33)) end end end end end end end}, fun (V34) -> fun (V35) -> fun (V36) -> fun (V37) -> fun (V38) -> begin (V39 = (V36(V38))), ((V37(V39))(V38)) end end end end end end, fun (V40) -> fun (V41) -> fun (V42) -> begin (V43 = (V41(V42))), (V43(V42)) end end end end}, fun (V44) -> fun (V45) -> V45 end end}, V3))(V15))), {'Idris.Prelude.Types.Right', V46} end), case V47 of {'Idris.Prelude.Types.Left', E16} -> (fun (V48) -> {'Idris.Prelude.Types.Left', V48} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V49) -> begin (V50 = (((V10(V49))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Erased', V2, 1}))))(V15))), case V50 of {'Idris.Prelude.Types.Left', E18} -> (fun (V51) -> {'Idris.Prelude.Types.Left', V51} end(E18)); {'Idris.Prelude.Types.Right', E19} -> (fun (V52) -> (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, V4, V52, V18))(V15)) end(E19)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E10, E11, E12, E13)); _ -> fun (V53) -> begin (V54 = (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, 1, ('Idris.Idris2.Core.TT':'un--binderType'('erased', V9)), V6))(V53))), case V54 of {'Idris.Prelude.Types.Left', E4} -> (fun (V55) -> {'Idris.Prelude.Types.Left', V55} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V56) -> begin (V85 = begin (V84 = (('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 (V57) -> fun (V58) -> fun (V59) -> fun (V60) -> fun (V61) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V59, V60, V61)) end end end end end, fun (V62) -> fun (V63) -> fun (V64) -> V63 end end end, fun (V65) -> fun (V66) -> fun (V67) -> fun (V68) -> fun (V69) -> begin (V70 = (V67(V69))), begin (V71 = (V68(V69))), (V70(V71)) end end end end end end end}, fun (V72) -> fun (V73) -> fun (V74) -> fun (V75) -> fun (V76) -> begin (V77 = (V74(V76))), ((V75(V77))(V76)) end end end end end end, fun (V78) -> fun (V79) -> fun (V80) -> begin (V81 = (V79(V80))), (V81(V80)) end end end end}, fun (V82) -> fun (V83) -> V83 end end}, V3))(V53))), {'Idris.Prelude.Types.Right', V84} end), case V85 of {'Idris.Prelude.Types.Left', E6} -> (fun (V86) -> {'Idris.Prelude.Types.Left', V86} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V87) -> begin (V88 = (((V10(V87))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Erased', V2, 1}))))(V53))), case V88 of {'Idris.Prelude.Types.Left', E8} -> (fun (V89) -> {'Idris.Prelude.Types.Left', V89} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V90) -> (('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, 1, V90, V6))(V53)) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E0, E1, E2, E3)); {'Idris.Core.Value.NApp', E20, E21, E22} -> (fun (V91, V92, V93) -> case V92 of {'Idris.Core.Value.NRef', E23, E24} -> (fun (V94, V95) -> case V94 of {'Idris.Core.TT.Bound'} -> (fun () -> fun (V96) -> begin (V125 = begin (V124 = (('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 (V97) -> fun (V98) -> fun (V99) -> fun (V100) -> fun (V101) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V99, V100, V101)) end end end end end, fun (V102) -> fun (V103) -> fun (V104) -> V103 end end end, fun (V105) -> fun (V106) -> fun (V107) -> fun (V108) -> fun (V109) -> begin (V110 = (V107(V109))), begin (V111 = (V108(V109))), (V110(V111)) end end end end end end end}, fun (V112) -> fun (V113) -> fun (V114) -> fun (V115) -> fun (V116) -> begin (V117 = (V114(V116))), ((V115(V117))(V116)) end end end end end end, fun (V118) -> fun (V119) -> fun (V120) -> begin (V121 = (V119(V120))), (V121(V120)) end end end end}, fun (V122) -> fun (V123) -> V123 end end}, V3))(V96))), {'Idris.Prelude.Types.Right', V124} end), case V125 of {'Idris.Prelude.Types.Left', E25} -> (fun (V126) -> {'Idris.Prelude.Types.Left', V126} end(E25)); {'Idris.Prelude.Types.Right', E26} -> (fun (V127) -> begin (V132 = begin (V129 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V128) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, [], V127, V128)) end, V93))(V96))), case V129 of {'Idris.Prelude.Types.Left', E27} -> (fun (V130) -> {'Idris.Prelude.Types.Left', V130} end(E27)); {'Idris.Prelude.Types.Right', E28} -> (fun (V131) -> (('nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, 1, V131, V6))(V96)) end(E28)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V132 of {'Idris.Prelude.Types.Left', E29} -> (fun (V133) -> {'Idris.Prelude.Types.Left', V133} end(E29)); {'Idris.Prelude.Types.Right', E30} -> (fun (V134) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Data.NameMap':'un--insert'('erased', V95, V4, V134))} end(E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); _ -> fun (V135) -> {'Idris.Prelude.Types.Right', V6} end end end(E23, E24)); _ -> fun (V136) -> {'Idris.Prelude.Types.Right', V6} end end end(E20, E21, E22)); {'Idris.Core.Value.NDCon', E31, E32, E33, E34, E35} -> (fun (V137, V138, V139, V140, V141) -> fun (V142) -> begin (V171 = begin (V170 = (('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 (V143) -> fun (V144) -> fun (V145) -> fun (V146) -> fun (V147) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V145, V146, V147)) end end end end end, fun (V148) -> fun (V149) -> fun (V150) -> V149 end end end, fun (V151) -> fun (V152) -> fun (V153) -> fun (V154) -> fun (V155) -> begin (V156 = (V153(V155))), begin (V157 = (V154(V155))), (V156(V157)) end end end end end end end}, fun (V158) -> fun (V159) -> fun (V160) -> fun (V161) -> fun (V162) -> begin (V163 = (V160(V162))), ((V161(V163))(V162)) end end end end end end, fun (V164) -> fun (V165) -> fun (V166) -> begin (V167 = (V165(V166))), (V167(V166)) end end end end}, fun (V168) -> fun (V169) -> V169 end end}, V3))(V142))), {'Idris.Prelude.Types.Right', V170} end), case V171 of {'Idris.Prelude.Types.Left', E36} -> (fun (V172) -> {'Idris.Prelude.Types.Left', V172} end(E36)); {'Idris.Prelude.Types.Right', E37} -> (fun (V173) -> begin (V175 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V174) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, [], V173, V174)) end, V141))(V142))), case V175 of {'Idris.Prelude.Types.Left', E38} -> (fun (V176) -> {'Idris.Prelude.Types.Left', V176} end(E38)); {'Idris.Prelude.Types.Right', E39} -> (fun (V177) -> (('nested--9417-10656--in--un--getDepsArgs'(V0, V1, V2, V3, 1, V177, V6))(V142)) end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E37)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E31, E32, E33, E34, E35)); {'Idris.Core.Value.NTCon', E40, E41, E42, E43, E44} -> (fun (V178, V179, V180, V181, V182) -> fun (V183) -> begin (V212 = begin (V211 = (('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 (V184) -> fun (V185) -> fun (V186) -> fun (V187) -> fun (V188) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V186, V187, V188)) end end end end end, fun (V189) -> fun (V190) -> fun (V191) -> V190 end end end, fun (V192) -> fun (V193) -> fun (V194) -> fun (V195) -> fun (V196) -> begin (V197 = (V194(V196))), begin (V198 = (V195(V196))), (V197(V198)) end end end end end end end}, fun (V199) -> fun (V200) -> fun (V201) -> fun (V202) -> fun (V203) -> begin (V204 = (V201(V203))), ((V202(V204))(V203)) end end end end end end, fun (V205) -> fun (V206) -> fun (V207) -> begin (V208 = (V206(V207))), (V208(V207)) end end end end}, fun (V209) -> fun (V210) -> V210 end end}, V3))(V183))), {'Idris.Prelude.Types.Right', V211} end), case V212 of {'Idris.Prelude.Types.Left', E45} -> (fun (V213) -> {'Idris.Prelude.Types.Left', V213} end(E45)); {'Idris.Prelude.Types.Right', E46} -> (fun (V214) -> begin (V253 = begin (V241 = ('Idris.Idris2.Core.Context':'un--lookupDefExact'(V179, case V214 of {'Idris.Core.Context.MkDefs', E47, E48, E49, E50, E51, E52, E53, E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72} -> (fun (V215, V216, V217, V218, V219, V220, V221, V222, V223, V224, V225, V226, V227, V228, V229, V230, V231, V232, V233, V234, V235, V236, V237, V238, V239, V240) -> V215 end(E47, E48, E49, E50, E51, E52, E53, E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V183))), case V241 of {'Idris.Prelude.Types.Left', E73} -> (fun (V242) -> {'Idris.Prelude.Types.Left', V242} end(E73)); {'Idris.Prelude.Types.Right', E74} -> (fun (V243) -> case V243 of {'Idris.Prelude.Types.Just', E75} -> (fun (V244) -> case V244 of {'Idris.Core.Context.TCon', E76, E77, E78, E79, E80, E81, E82, E83} -> (fun (V245, V246, V247, V248, V249, V250, V251, V252) -> {'Idris.Prelude.Types.Right', V247} end(E76, E77, E78, E79, E80, E81, E82, E83)); _ -> {'Idris.Prelude.Types.Right', []} end end(E75)); _ -> {'Idris.Prelude.Types.Right', []} end end(E74)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V253 of {'Idris.Prelude.Types.Left', E84} -> (fun (V254) -> {'Idris.Prelude.Types.Left', V254} end(E84)); {'Idris.Prelude.Types.Right', E85} -> (fun (V255) -> (('case--processFnOpt,getDeps-11296'(V0, V1, V2, V3, V178, V182, V181, V180, V179, V6, V4, V214, V255, ('nested--9518-11047--in--un--splitPs'(V0, V1, V2, V3, V178, V182, V181, V180, V179, V6, V4, 0, V255, V182))))(V183)) end(E85)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E46)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E40, E41, E42, E43, E44)); {'Idris.Core.Value.NDelayed', E86, E87, E88} -> (fun (V256, V257, V258) -> ('nested--9417-10657--in--un--getDeps'(V0, V1, V2, V3, V4, V258, V6)) end(E86, E87, E88)); _ -> fun (V259) -> {'Idris.Prelude.Types.Right', V6} end end.
'nested--10875-11912--in--un--findInfs'(V0, V1, V2, V3, V4, V5) -> case V5 of [] -> fun (V6) -> {'Idris.Prelude.Types.Right', V3} end; [E0 | E1] -> (fun (V7, V8) -> fun (V9) -> begin (V10 = (('nested--10875-11912--in--un--findInfs'(V0, V1, V2, V3, V4, V8))(V9))), case V10 of {'Idris.Prelude.Types.Left', E2} -> (fun (V11) -> {'Idris.Prelude.Types.Left', V11} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V12) -> (('nested--10875-11911--in--un--findInf'(V0, V1, V2, V12, V4, V7))(V9)) end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--10875-11911--in--un--findInf'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NApp', E0, E1, E2} -> (fun (V6, V7, V8) -> case V7 of {'Idris.Core.Value.NRef', E3, E4} -> (fun (V9, V10) -> case V9 of {'Idris.Core.TT.Bound'} -> (fun () -> case V8 of [] -> ('case--findInferrable,findInf-11938'(V0, V1, V2, V6, V10, V4, V3, ('Idris.Idris2.Data.List':'un--lookup'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V11) -> fun (V12) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V11, V12)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V13, V14)) end end}, V10, V4)))); _ -> fun (V15) -> {'Idris.Prelude.Types.Right', V3} end end end()); _ -> fun (V16) -> {'Idris.Prelude.Types.Right', V3} end end end(E3, E4)); _ -> fun (V17) -> {'Idris.Prelude.Types.Right', V3} end end end(E0, E1, E2)); {'Idris.Core.Value.NDCon', E5, E6, E7, E8, E9} -> (fun (V18, V19, V20, V21, V22) -> fun (V23) -> begin (V25 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V24) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V2, [], V1, V24)) end, V22))(V23))), case V25 of {'Idris.Prelude.Types.Left', E10} -> (fun (V26) -> {'Idris.Prelude.Types.Left', V26} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V27) -> (('nested--10875-11912--in--un--findInfs'(V0, V1, V2, V3, V4, V27))(V23)) end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E5, E6, E7, E8, E9)); {'Idris.Core.Value.NTCon', E12, E13, E14, E15, E16} -> (fun (V28, V29, V30, V31, V32) -> fun (V33) -> begin (V35 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V34) -> ('Idris.Idris2.Core.Normalise':'un--evalClosure'(V2, [], V1, V34)) end, V32))(V33))), case V35 of {'Idris.Prelude.Types.Left', E17} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V37) -> (('nested--10875-11912--in--un--findInfs'(V0, V1, V2, V3, V4, V37))(V33)) end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E12, E13, E14, E15, E16)); {'Idris.Core.Value.NDelayed', E19, E20, E21} -> (fun (V38, V39, V40) -> ('nested--10875-11911--in--un--findInf'(V0, V1, V2, V3, V4, V40)) end(E19, E20, E21)); _ -> fun (V41) -> {'Idris.Prelude.Types.Right', V3} end end.
'nested--10875-11913--in--un--fi'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V8, V9, V10, V11) -> case V10 of {'Idris.Core.TT.Pi', E4, E5, E6, E7} -> (fun (V12, V13, V14, V15) -> begin (V16 = {'Idris.Core.Name.MN', <<"inf"/utf8>>, V4}), fun (V17) -> begin (V18 = (((V11(V1))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Ref', V8, {'Idris.Core.TT.Bound'}, V16}))))(V17))), case V18 of {'Idris.Prelude.Types.Left', E8} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V20) -> begin (V21 = (('nested--10875-11911--in--un--findInf'(V0, V1, V2, V6, V5, V15))(V17))), case V21 of {'Idris.Prelude.Types.Left', E10} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V23) -> begin (V24 = (('nested--10875-11913--in--un--fi'(V0, V1, V2, ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types':'dn--un--fromInteger_Num__Nat'(1)), V3)), ((1 + V4) rem 9223372036854775808), [{'Idris.Builtin.MkPair', V16, V3} | V5], V23, V20))(V17))), case V24 of {'Idris.Prelude.Types.Left', E12} -> (fun (V25) -> {'Idris.Prelude.Types.Left', V25} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V26) -> {'Idris.Prelude.Types.Right', V26} end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E4, E5, E6, E7)); _ -> ('nested--10875-11911--in--un--findInf'(V0, V1, V2, V6, V5, V7)) end end(E0, E1, E2, E3)); _ -> ('nested--10875-11911--in--un--findInf'(V0, V1, V2, V6, V5, V7)) end.
'nested--9417-10658--in--un--collectSpec'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V8, V9, V10, V11) -> case V10 of {'Idris.Core.TT.Pi', E4, E5, E6, E7} -> (fun (V12, V13, V14, V15) -> fun (V16) -> begin (V45 = begin (V44 = (('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 (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V19, V20, V21)) end end end end end, fun (V22) -> fun (V23) -> fun (V24) -> V23 end end end, fun (V25) -> fun (V26) -> fun (V27) -> fun (V28) -> fun (V29) -> begin (V30 = (V27(V29))), begin (V31 = (V28(V29))), (V30(V31)) end end end end end end end}, fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> fun (V36) -> begin (V37 = (V34(V36))), ((V35(V37))(V36)) end end end end end end, fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V39(V40))), (V41(V40)) end end end end}, fun (V42) -> fun (V43) -> V43 end end}, V3))(V16))), {'Idris.Prelude.Types.Right', V44} end), case V45 of {'Idris.Prelude.Types.Left', E8} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V47) -> begin (V48 = ('Idris.Idris2.Core.Context':'un--clearDefs'(V47, V16))), case V48 of {'Idris.Prelude.Types.Left', E10} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V50) -> begin (V51 = (((V11(V47))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Ref', V8, {'Idris.Core.TT.Bound'}, V9}))))(V16))), case V51 of {'Idris.Prelude.Types.Left', E12} -> (fun (V52) -> {'Idris.Prelude.Types.Left', V52} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V53) -> (('case--processFnOpt,collectSpec-11410'(V0, V1, V2, V3, V12, V13, V14, V15, V11, V9, V8, V6, V5, V4, V47, V50, V53, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V54) -> fun (V55) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V54, V55)) end end, fun (V56) -> fun (V57) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V56, V57)) end end}, V9, V0))))(V16)) end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5, E6, E7)); _ -> fun (V58) -> {'Idris.Prelude.Types.Right', V4} end end end(E0, E1, E2, E3)); _ -> fun (V59) -> {'Idris.Prelude.Types.Right', V4} end end.
'nested--9417-10655--in--un--collectDDeps'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V5, V6, V7, V8) -> case V7 of {'Idris.Core.TT.Pi', E4, E5, E6, E7} -> (fun (V9, V10, V11, V12) -> fun (V13) -> begin (V42 = begin (V41 = (('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 (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V16, V17, V18)) end end end end end, fun (V19) -> fun (V20) -> fun (V21) -> V20 end end end, fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> begin (V27 = (V24(V26))), begin (V28 = (V25(V26))), (V27(V28)) end end end end end end end}, fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> begin (V34 = (V31(V33))), ((V32(V34))(V33)) end end end end end end, fun (V35) -> fun (V36) -> fun (V37) -> begin (V38 = (V36(V37))), (V38(V37)) end end end end}, fun (V39) -> fun (V40) -> V40 end end}, V3))(V13))), {'Idris.Prelude.Types.Right', V41} end), case V42 of {'Idris.Prelude.Types.Left', E8} -> (fun (V43) -> {'Idris.Prelude.Types.Left', V43} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V44) -> begin (V45 = ('Idris.Idris2.Core.Context':'un--clearDefs'(V44, V13))), case V45 of {'Idris.Prelude.Types.Left', E10} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V47) -> begin (V48 = (((V8(V44))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Ref', V5, {'Idris.Core.TT.Bound'}, V6}))))(V13))), case V48 of {'Idris.Prelude.Types.Left', E12} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V50) -> (('case--processFnOpt,collectDDeps-10803'(V0, V1, V2, V3, V9, V10, V11, V12, V8, V6, V5, V44, V47, V50, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V51) -> fun (V52) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V51, V52)) end end, fun (V53) -> fun (V54) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V53, V54)) end end}, V6, V0))))(V13)) end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5, E6, E7)); _ -> fun (V55) -> {'Idris.Prelude.Types.Right', []} end end end(E0, E1, E2, E3)); _ -> fun (V56) -> {'Idris.Prelude.Types.Right', []} end end.
'un--processType'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11) -> case V11 of {'Idris.TTImp.TTImp.MkImpTy', E0, E1, E2} -> (fun (V12, V13, V14) -> fun (V15) -> begin (V16 = (('Idris.Idris2.Core.Context':'un--inCurrentNS'(V1, V13))(V15))), case V16 of {'Idris.Prelude.Types.Left', E3} -> (fun (V17) -> {'Idris.Prelude.Types.Left', V17} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V18) -> begin (V19 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"declare.type"/utf8>>, (1 + 0), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Processing "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)))) end))(V15))), case V19 of {'Idris.Prelude.Types.Left', E5} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V21) -> begin (V22 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"declare.type"/utf8>>, (1 + (1 + (1 + (1 + (1 + 0))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Checking type decl "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__RawImp'(V14)))))))) end))(V15))), case V22 of {'Idris.Prelude.Types.Left', E7} -> (fun (V23) -> {'Idris.Prelude.Types.Left', V23} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V24) -> begin (V25 = (('Idris.Idris2.Core.Context':'un--resolveName'(V1, V18))(V15))), case V25 of {'Idris.Prelude.Types.Left', E9} -> (fun (V26) -> {'Idris.Prelude.Types.Left', V26} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V27) -> begin (V56 = begin (V55 = (('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 (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> fun (V32) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V30, V31, V32)) end end end end end, fun (V33) -> fun (V34) -> fun (V35) -> V34 end end end, fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V38(V40))), begin (V42 = (V39(V40))), (V41(V42)) end end end end end end end}, fun (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> begin (V48 = (V45(V47))), ((V46(V48))(V47)) end end end end end end, fun (V49) -> fun (V50) -> fun (V51) -> begin (V52 = (V50(V51))), (V52(V51)) end end end end}, fun (V53) -> fun (V54) -> V54 end end}, V1))(V15))), {'Idris.Prelude.Types.Right', V55} end), case V56 of {'Idris.Prelude.Types.Left', E11} -> (fun (V57) -> {'Idris.Prelude.Types.Left', V57} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V58) -> begin (V85 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'({'Idris.Core.Name.Resolved', V27}, case V58 of {'Idris.Core.Context.MkDefs', 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, E38} -> (fun (V59, V60, V61, V62, V63, V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84) -> V59 end(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, E38)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V15))), case V85 of {'Idris.Prelude.Types.Left', E39} -> (fun (V86) -> {'Idris.Prelude.Types.Left', V86} end(E39)); {'Idris.Prelude.Types.Right', E40} -> (fun (V87) -> case V87 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V94 = ((('Idris.Idris2.TTImp.Elab.Utils':'un--wrapErrorC'('erased', V4, fun (V93) -> {'Idris.Core.Core.InType', V7, V18, V93} end))(fun (V88) -> ('Idris.Idris2.TTImp.Elab':'un--checkTerm'(V0, V1, V2, V3, V27, {'Idris.TTImp.Elab.Check.InType'}, [{'Idris.TTImp.Elab.Check.HolesOkay'} | V4], V5, V6, {'Idris.TTImp.TTImp.IBindHere', V7, {'Idris.TTImp.TTImp.PI', ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V89) -> fun (V90) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V89, V90)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V91) -> fun (V92) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V91, V92)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))}, V14}, ('Idris.Idris2.Core.Normalise':'un--gType'('erased', V7)), V88)) end))(V15))), case V94 of {'Idris.Prelude.Types.Left', E41} -> (fun (V95) -> {'Idris.Prelude.Types.Left', V95} end(E41)); {'Idris.Prelude.Types.Right', E42} -> (fun (V96) -> begin (V97 = (('Idris.Idris2.Core.Normalise':'un--logTermNF'([], V1, <<"declare.type"/utf8>>, (1 + (1 + (1 + 0))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Type of "/utf8>>, ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)))) end, {'Idris.Core.Env.Nil'}, ('Idris.Idris2.Core.Env':'un--abstractFullEnvType'(V0, V12, V6, V96))))(V15))), case V97 of {'Idris.Prelude.Types.Left', E43} -> (fun (V98) -> {'Idris.Prelude.Types.Left', V98} end(E43)); {'Idris.Prelude.Types.Right', E44} -> (fun (V99) -> begin (V100 = (('un--initDef'(V0, V1, V2, V3, V18, V6, V96, V10))(V15))), case V100 of {'Idris.Prelude.Types.Left', E45} -> (fun (V101) -> {'Idris.Prelude.Types.Left', V101} end(E45)); {'Idris.Prelude.Types.Right', E46} -> (fun (V102) -> begin (V103 = ('Idris.Idris2.Core.Env':'un--abstractFullEnvType'(V0, V12, V6, V96))), begin (V104 = ('Idris.Idris2.TTImp.Elab.Utils':'un--findErased'(V1, V103, V15))), case V104 of {'Idris.Prelude.Types.Left', E47} -> (fun (V105) -> {'Idris.Prelude.Types.Left', V105} end(E47)); {'Idris.Prelude.Types.Right', E48} -> (fun (V106) -> begin (V107 = {'Idris.Prelude.Types.Nothing'}), case V106 of {'Idris.Builtin.MkPair', E49, E50} -> (fun (V108, V109) -> begin (V138 = begin (V137 = (('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 (V110) -> fun (V111) -> fun (V112) -> fun (V113) -> fun (V114) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V112, V113, V114)) end end end end end, fun (V115) -> fun (V116) -> fun (V117) -> V116 end end end, fun (V118) -> fun (V119) -> fun (V120) -> fun (V121) -> fun (V122) -> begin (V123 = (V120(V122))), begin (V124 = (V121(V122))), (V123(V124)) end end end end end end end}, fun (V125) -> fun (V126) -> fun (V127) -> fun (V128) -> fun (V129) -> begin (V130 = (V127(V129))), ((V128(V130))(V129)) end end end end end end, fun (V131) -> fun (V132) -> fun (V133) -> begin (V134 = (V132(V133))), (V134(V133)) end end end end}, fun (V135) -> fun (V136) -> V136 end end}, V1))(V15))), {'Idris.Prelude.Types.Right', V137} end), case V138 of {'Idris.Prelude.Types.Left', E51} -> (fun (V139) -> {'Idris.Prelude.Types.Left', V139} end(E51)); {'Idris.Prelude.Types.Right', E52} -> (fun (V140) -> begin (V141 = ('Idris.Idris2.Core.Context':'un--clearDefs'(V140, V15))), case V141 of {'Idris.Prelude.Types.Left', E53} -> (fun (V142) -> {'Idris.Prelude.Types.Left', V142} end(E53)); {'Idris.Prelude.Types.Right', E54} -> (fun (V143) -> begin (V147 = begin (V144 = (('Idris.Idris2.Core.Normalise':'un--nf'(V1, [], V140, {'Idris.Core.Env.Nil'}, V103))(V15))), case V144 of {'Idris.Prelude.Types.Left', E55} -> (fun (V145) -> {'Idris.Prelude.Types.Left', V145} end(E55)); {'Idris.Prelude.Types.Right', E56} -> (fun (V146) -> (('un--findInferrable'(V1, V143, V146))(V15)) end(E56)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V147 of {'Idris.Prelude.Types.Left', E57} -> (fun (V148) -> {'Idris.Prelude.Types.Left', V148} end(E57)); {'Idris.Prelude.Types.Right', E58} -> (fun (V149) -> begin (V151 = ('Idris.Idris2.Core.Context':'un--addDef'(V1, {'Idris.Core.Name.Resolved', V27}, begin (V150 = {'Idris.Builtin.MkPair', V108, V109}), ('case--case block in case block in processType-12598'(V14, V13, V12, V10, V9, V8, V7, V0, V6, V5, V4, V3, V2, V1, V18, V21, V24, V27, V58, V107, V96, V99, V102, V103, V108, V109, V150, V140, V143, V149, ('Idris.Idris2.Core.Context':'un--newDef'(V7, V18, V8, V0, V103, V9, V102)))) end, V15))), case V151 of {'Idris.Prelude.Types.Left', E59} -> (fun (V152) -> {'Idris.Prelude.Types.Left', V152} end(E59)); {'Idris.Prelude.Types.Right', E60} -> (fun (V153) -> begin (V158 = case ('Idris.Idris2.Prelude.Basics':'un--not'(('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V154) -> fun (V155) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--==_Eq__ElabOpt'(V154, V155)) end end, fun (V156) -> fun (V157) -> ('Idris.Idris2.TTImp.Elab.Check':'dn--un--/=_Eq__ElabOpt'(V156, V157)) end end}, {'Idris.TTImp.Elab.Check.InCase'}, V4)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setLinearCheck'(V1, V27, 0, V15)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end), case V158 of {'Idris.Prelude.Types.Left', E61} -> (fun (V159) -> {'Idris.Prelude.Types.Left', V159} end(E61)); {'Idris.Prelude.Types.Right', E62} -> (fun (V160) -> begin (V164 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"declare.type"/utf8>>, (1 + (1 + 0)), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Setting options for "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)), ('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 (V161) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--show_Show__FnOpt'(V161)) end, fun (V162) -> fun (V163) -> ('Idris.Idris2.TTImp.TTImp':'dn--un--showPrec_Show__FnOpt'(V162, V163)) end end}, V10)))))))) end))(V15))), case V164 of {'Idris.Prelude.Types.Left', E63} -> (fun (V165) -> {'Idris.Prelude.Types.Left', V165} end(E63)); {'Idris.Prelude.Types.Right', E64} -> (fun (V166) -> begin (V167 = {'Idris.Core.Name.Resolved', V27}), begin (V169 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V168) -> ('un--processFnOpt'(V1, V7, V167, V168)) end, V10))(V15))), case V169 of {'Idris.Prelude.Types.Left', E65} -> (fun (V170) -> {'Idris.Prelude.Types.Left', V170} end(E65)); {'Idris.Prelude.Types.Right', E66} -> (fun (V171) -> begin (V186 = begin (V172 = ('Idris.Idris2.Core.Context':'un--getDefaultTotalityOption'(V1, V15))), case V172 of {'Idris.Prelude.Types.Left', E67} -> (fun (V173) -> {'Idris.Prelude.Types.Left', V173} end(E67)); {'Idris.Prelude.Types.Right', E68} -> (fun (V174) -> case ('Idris.Idris2.Prelude.Basics':'un--not'((('Idris.Idris2.Prelude.Interfaces':'un--any'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkFoldable', fun (V175) -> fun (V176) -> fun (V177) -> fun (V178) -> fun (V179) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldr_Foldable__List'('erased', 'erased', V177, V178, V179)) end end end end end, fun (V180) -> fun (V181) -> fun (V182) -> fun (V183) -> fun (V184) -> ('Idris.Idris2.Prelude.Types':'dn--un--foldl_Foldable__List'('erased', 'erased', V182, V183, V184)) end end end end end}, fun (V185) -> ('Idris.Idris2.TTImp.TTImp':'un--isTotalityReq'(V185)) end))(V10)))) of 0 -> ('Idris.Idris2.Core.Context':'un--setFlag'(V1, V7, V167, {'Idris.Core.Context.SetTotal', V174}, V15)); 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E68)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V186 of {'Idris.Prelude.Types.Left', E69} -> (fun (V187) -> {'Idris.Prelude.Types.Left', V187} end(E69)); {'Idris.Prelude.Types.Right', E70} -> (fun (V188) -> begin (V189 = ('Idris.Idris2.Core.Metadata':'un--addTyDecl'(V0, V1, V2, V7, {'Idris.Core.Name.Resolved', V27}, V6, V96, V15))), case V189 of {'Idris.Prelude.Types.Left', E71} -> (fun (V190) -> {'Idris.Prelude.Types.Left', V190} end(E71)); {'Idris.Prelude.Types.Right', E72} -> (fun (V191) -> begin (V192 = ('Idris.Idris2.Core.Metadata':'un--addNameType'(V0, V1, V2, V7, {'Idris.Core.Name.Resolved', V27}, V6, V96, V15))), case V192 of {'Idris.Prelude.Types.Left', E73} -> (fun (V193) -> {'Idris.Prelude.Types.Left', V193} end(E73)); {'Idris.Prelude.Types.Right', E74} -> (fun (V194) -> begin (V197 = (('Idris.Idris2.Core.Core':'un--traverse_'('erased', 'erased', fun (V195) -> fun (V196) -> ('Idris.Idris2.Core.Context':'un--addToSave'(V1, V195, V196)) end end, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V96))))))(V15))), case V197 of {'Idris.Prelude.Types.Left', E75} -> (fun (V198) -> {'Idris.Prelude.Types.Left', V198} end(E75)); {'Idris.Prelude.Types.Right', E76} -> (fun (V199) -> begin (V200 = ('Idris.Idris2.Core.Context':'un--addToSave'(V1, V18, V15))), case V200 of {'Idris.Prelude.Types.Left', E77} -> (fun (V201) -> {'Idris.Prelude.Types.Left', V201} end(E77)); {'Idris.Prelude.Types.Right', E78} -> (fun (V202) -> begin (V206 = (('Idris.Idris2.Core.Context.Log':'un--log'(V1, <<"declare.type"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Saving from "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V18)), ('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 (V203) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V203)) end, fun (V204) -> fun (V205) -> ('Idris.Idris2.Core.Name':'dn--un--showPrec_Show__Name'(V204, V205)) end end}, ('Idris.Idris2.Data.NameMap':'un--keys'('erased', ('Idris.Idris2.Core.TT':'un--getMetas'('erased', V96)))))))))))) end))(V15))), case V206 of {'Idris.Prelude.Types.Left', E79} -> (fun (V207) -> {'Idris.Prelude.Types.Left', V207} end(E79)); {'Idris.Prelude.Types.Right', E80} -> (fun (V208) -> case ('Idris.Idris2.Core.TT':'dn--un--/=_Eq__Visibility'(V9, {'Idris.Core.TT.Private'})) of 0 -> begin (V216 = ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V1, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V209) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__Name'(V209)) end, fun (V210) -> fun (V211) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__Name'(V210, V211)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V212) -> fun (V213) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(V212, V213)) end end, fun (V214) -> fun (V215) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__Name'(V214, V215)) end end}, V18, V15))), case V216 of {'Idris.Prelude.Types.Left', E81} -> (fun (V217) -> {'Idris.Prelude.Types.Left', V217} end(E81)); {'Idris.Prelude.Types.Right', E82} -> (fun (V218) -> ('Idris.Idris2.Core.Context':'un--addHashWithNames'('erased', V1, {'Idris.Core.Hash.dn--un--__mkHashable', fun (V219) -> ('Idris.Idris2.Core.Hash':'dn--un--hash_Hashable__(Term $vars)'('erased', V219)) end, fun (V220) -> fun (V221) -> ('Idris.Idris2.Core.Hash':'dn--un--hashWithSalt_Hashable__(Term $vars)'('erased', V220, V221)) end end}, {'Idris.Core.Context.dn--un--__mkHasNames', fun (V222) -> fun (V223) -> ('Idris.Idris2.Core.Context':'dn--un--full_HasNames__(Term $vars)'('erased', V222, V223)) end end, fun (V224) -> fun (V225) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', V224, V225)) end end}, V96, V15)) end(E82)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E80)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E78)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E76)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E74)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E72)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E70)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E66)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E64)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E62)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E60)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E58)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E54)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E52)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E49, E50)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E48)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E46)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E44)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end()); {'Idris.Prelude.Types.Just', E83} -> (fun (V226) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.AlreadyDefined', V7, V18}, V15)) end(E83)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E40)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end 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 end(E0, E1, E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--processFnOpt'(V0, V1, V2, V3) -> case V3 of {'Idris.TTImp.TTImp.Inline'} -> (fun () -> fun (V4) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.Inline'}, V4)) end end()); {'Idris.TTImp.TTImp.TCInline'} -> (fun () -> fun (V5) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.TCInline'}, V5)) end end()); {'Idris.TTImp.TTImp.Hint', E0} -> (fun (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}, V0))(V7))), {'Idris.Prelude.Types.Right', V35} end), case V36 of {'Idris.Prelude.Types.Left', E1} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V38) -> begin (V65 = ('Idris.Idris2.Core.Context':'un--lookupTyExact'(V2, case V38 of {'Idris.Core.Context.MkDefs', E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28} -> (fun (V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64) -> V39 end(E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))), case V65 of {'Idris.Prelude.Types.Left', E29} -> (fun (V66) -> {'Idris.Prelude.Types.Left', V66} end(E29)); {'Idris.Prelude.Types.Right', E30} -> (fun (V67) -> case V67 of {'Idris.Prelude.Types.Just', E31} -> (fun (V68) -> begin (V72 = begin (V69 = (('Idris.Idris2.Core.Normalise':'un--nf'(V0, [], V38, {'Idris.Core.Env.Nil'}, V68))(V7))), case V69 of {'Idris.Prelude.Types.Left', E32} -> (fun (V70) -> {'Idris.Prelude.Types.Left', V70} end(E32)); {'Idris.Prelude.Types.Right', E33} -> (fun (V71) -> (('un--getRetTy'(V38, V71))(V7)) end(E33)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V72 of {'Idris.Prelude.Types.Left', E34} -> (fun (V73) -> {'Idris.Prelude.Types.Left', V73} end(E34)); {'Idris.Prelude.Types.Right', E35} -> (fun (V74) -> ('Idris.Idris2.Core.Context':'un--addHintFor'(V0, V1, V74, V2, V6, 1, V7)) end(E35)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E31)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V1, V2}, V7)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.TTImp.TTImp.GlobalHint', E36} -> (fun (V75) -> fun (V76) -> ('Idris.Idris2.Core.Context':'un--addGlobalHint'(V0, V2, V75, V76)) end end(E36)); {'Idris.TTImp.TTImp.ExternFn'} -> (fun () -> fun (V77) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.Inline'}, V77)) end end()); {'Idris.TTImp.TTImp.ForeignFn', E37} -> (fun (V78) -> fun (V79) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.Inline'}, V79)) end end(E37)); {'Idris.TTImp.TTImp.Invertible'} -> (fun () -> fun (V80) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.Invertible'}, V80)) end end()); {'Idris.TTImp.TTImp.Totality', E38} -> (fun (V81) -> fun (V82) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.SetTotal', V81}, V82)) end end(E38)); {'Idris.TTImp.TTImp.Macro'} -> (fun () -> fun (V83) -> ('Idris.Idris2.Core.Context':'un--setFlag'(V0, V1, V2, {'Idris.Core.Context.Macro'}, V83)) end end()); {'Idris.TTImp.TTImp.SpecArgs', E39} -> (fun (V84) -> fun (V85) -> begin (V114 = begin (V113 = (('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 (V86) -> fun (V87) -> fun (V88) -> fun (V89) -> fun (V90) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V88, V89, V90)) end end end end end, fun (V91) -> fun (V92) -> fun (V93) -> V92 end end end, fun (V94) -> fun (V95) -> fun (V96) -> fun (V97) -> fun (V98) -> begin (V99 = (V96(V98))), begin (V100 = (V97(V98))), (V99(V100)) end end end end end end end}, fun (V101) -> fun (V102) -> fun (V103) -> fun (V104) -> fun (V105) -> begin (V106 = (V103(V105))), ((V104(V106))(V105)) end end end end end end, fun (V107) -> fun (V108) -> fun (V109) -> begin (V110 = (V108(V109))), (V110(V109)) end end end end}, fun (V111) -> fun (V112) -> V112 end end}, V0))(V85))), {'Idris.Prelude.Types.Right', V113} end), case V114 of {'Idris.Prelude.Types.Left', E40} -> (fun (V115) -> {'Idris.Prelude.Types.Left', V115} end(E40)); {'Idris.Prelude.Types.Right', E41} -> (fun (V116) -> begin (V143 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V2, case V116 of {'Idris.Core.Context.MkDefs', E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67} -> (fun (V117, V118, V119, V120, V121, V122, V123, V124, V125, V126, V127, V128, V129, V130, V131, V132, V133, V134, V135, V136, V137, V138, V139, V140, V141, V142) -> V117 end(E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V85))), case V143 of {'Idris.Prelude.Types.Left', E68} -> (fun (V144) -> {'Idris.Prelude.Types.Left', V144} end(E68)); {'Idris.Prelude.Types.Right', E69} -> (fun (V145) -> case V145 of {'Idris.Prelude.Types.Just', E70} -> (fun (V146) -> begin (V168 = (('Idris.Idris2.Core.Normalise':'un--nf'(V0, [], V116, {'Idris.Core.Env.Nil'}, case V146 of {'Idris.Core.Context.MkGlobalDef', E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83, E84, E85, E86, E87, E88, E89, E90, E91} -> (fun (V147, V148, V149, V150, V151, V152, V153, V154, V155, V156, V157, V158, V159, V160, V161, V162, V163, V164, V165, V166, V167) -> V149 end(E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83, E84, E85, E86, E87, E88, E89, E90, E91)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V85))), case V168 of {'Idris.Prelude.Types.Left', E92} -> (fun (V169) -> {'Idris.Prelude.Types.Left', V169} end(E92)); {'Idris.Prelude.Types.Right', E93} -> (fun (V170) -> begin (V171 = (('nested--9417-10659--in--un--getNamePos'(V84, V2, V1, V0, 0, V170))(V85))), case V171 of {'Idris.Prelude.Types.Left', E94} -> (fun (V172) -> {'Idris.Prelude.Types.Left', V172} end(E94)); {'Idris.Prelude.Types.Right', E95} -> (fun (V173) -> begin (V174 = (('nested--9417-10655--in--un--collectDDeps'(V84, V2, V1, V0, V170))(V85))), case V174 of {'Idris.Prelude.Types.Left', E96} -> (fun (V175) -> {'Idris.Prelude.Types.Left', V175} end(E96)); {'Idris.Prelude.Types.Right', E97} -> (fun (V176) -> begin (V177 = (('nested--9417-10658--in--un--collectSpec'(V84, V2, V1, V0, [], V176, V173, V170))(V85))), case V177 of {'Idris.Prelude.Types.Left', E98} -> (fun (V178) -> {'Idris.Prelude.Types.Left', V178} end(E98)); {'Idris.Prelude.Types.Right', E99} -> (fun (V179) -> begin (V201 = ('Idris.Idris2.Core.Context':'un--addDef'(V0, V2, case V146 of {'Idris.Core.Context.MkGlobalDef', E100, E101, E102, E103, E104, E105, E106, E107, E108, E109, E110, E111, E112, E113, E114, E115, E116, E117, E118, E119, E120} -> (fun (V180, V181, V182, V183, V184, V185, V186, V187, V188, V189, V190, V191, V192, V193, V194, V195, V196, V197, V198, V199, V200) -> {'Idris.Core.Context.MkGlobalDef', V180, V181, V182, V183, V184, V179, V186, V187, V188, V189, V190, V191, V192, V193, V194, V195, V196, V197, V198, V199, V200} end(E100, E101, E102, E103, E104, E105, E106, E107, E108, E109, E110, E111, E112, E113, E114, E115, E116, E117, E118, E119, E120)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V85))), case V201 of {'Idris.Prelude.Types.Left', E121} -> (fun (V202) -> {'Idris.Prelude.Types.Left', V202} end(E121)); {'Idris.Prelude.Types.Right', E122} -> (fun (V203) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}} end(E122)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E99)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E97)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E95)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E93)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E70)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V1, V2}, V85)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E69)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E41)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--initDef'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of [] -> fun (V8) -> begin (V9 = ('Idris.Idris2.Core.Context':'un--addUserHole'(V1, V4, 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) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Context.None'}} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; [E2 | E3] -> (fun (V12, V13) -> case V12 of {'Idris.TTImp.TTImp.ExternFn'} -> (fun () -> fun (V14) -> begin (V43 = begin (V42 = (('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 (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V17, V18, V19)) end end end end end, fun (V20) -> fun (V21) -> fun (V22) -> V21 end end end, fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> begin (V28 = (V25(V27))), begin (V29 = (V26(V27))), (V28(V29)) end end end end end end end}, fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> begin (V35 = (V32(V34))), ((V33(V35))(V34)) end end end end end end, fun (V36) -> fun (V37) -> fun (V38) -> begin (V39 = (V37(V38))), (V39(V38)) end end end end}, fun (V40) -> fun (V41) -> V41 end end}, V1))(V14))), {'Idris.Prelude.Types.Right', V42} end), case V43 of {'Idris.Prelude.Types.Left', E4} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V45) -> begin (V46 = ('Idris.Idris2.Core.Normalise':'un--getArity'(V1, V0, V45, V5, V6, V14))), case V46 of {'Idris.Prelude.Types.Left', E6} -> (fun (V47) -> {'Idris.Prelude.Types.Left', V47} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V48) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Context.ExternDef', V48}} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end()); {'Idris.TTImp.TTImp.ForeignFn', E8} -> (fun (V49) -> fun (V50) -> begin (V79 = begin (V78 = (('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 (V51) -> fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V53, V54, V55)) end end end end end, fun (V56) -> fun (V57) -> fun (V58) -> V57 end end end, fun (V59) -> fun (V60) -> fun (V61) -> fun (V62) -> fun (V63) -> begin (V64 = (V61(V63))), begin (V65 = (V62(V63))), (V64(V65)) end end end end end end end}, fun (V66) -> fun (V67) -> fun (V68) -> fun (V69) -> fun (V70) -> begin (V71 = (V68(V70))), ((V69(V71))(V70)) end end end end end end, fun (V72) -> fun (V73) -> fun (V74) -> begin (V75 = (V73(V74))), (V75(V74)) end end end end}, fun (V76) -> fun (V77) -> V77 end end}, V1))(V50))), {'Idris.Prelude.Types.Right', V78} end), case V79 of {'Idris.Prelude.Types.Left', E9} -> (fun (V80) -> {'Idris.Prelude.Types.Left', V80} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V81) -> begin (V82 = ('Idris.Idris2.Core.Normalise':'un--getArity'(V1, V0, V81, V5, V6, V50))), case V82 of {'Idris.Prelude.Types.Left', E11} -> (fun (V83) -> {'Idris.Prelude.Types.Left', V83} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V84) -> begin (V86 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V85) -> ('un--getFnString'(V1, V2, V3, V85)) end, V49))(V50))), case V86 of {'Idris.Prelude.Types.Left', E13} -> (fun (V87) -> {'Idris.Prelude.Types.Left', V87} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V88) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Context.ForeignDef', V84, V88}} end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E8)); _ -> ('un--initDef'(V0, V1, V2, V3, V4, V5, V6, V13)) end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getRetTy'(V0, V1) -> case V1 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V2, V3, V4, V5) -> case V4 of {'Idris.Core.TT.Pi', E4, E5, E6, E7} -> (fun (V6, V7, V8, V9) -> fun (V10) -> begin (V11 = (((V5(V0))(('Idris.Idris2.Core.Normalise':'un--toClosure'('erased', ('Idris.Idris2.Core.Value':'un--defaultOpts'()), {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.Erased', V2, 1}))))(V10))), case V11 of {'Idris.Prelude.Types.Left', E8} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V13) -> (('un--getRetTy'(V0, V13))(V10)) end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5, E6, E7)); _ -> fun (V14) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', ('Idris.Idris2.Core.Value':'un--getLoc'('erased', V1)), <<"Can only add hints for concrete return types"/utf8>>}, V14)) end end end(E0, E1, E2, E3)); {'Idris.Core.Value.NTCon', E10, E11, E12, E13, E14} -> (fun (V15, V16, V17, V18, V19) -> fun (V20) -> {'Idris.Prelude.Types.Right', V16} end end(E10, E11, E12, E13, E14)); _ -> fun (V21) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', ('Idris.Idris2.Core.Value':'un--getLoc'('erased', V1)), <<"Can only add hints for concrete return types"/utf8>>}, V21)) end end.
'un--getFnString'(V0, V1, V2, V3) -> case V3 of {'Idris.TTImp.TTImp.IPrimVal', E11, E12} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.Str', E24} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E24)); _ -> fun (V8) -> begin (V9 = (('Idris.Idris2.Core.Context':'un--resolveName'(V0, {'Idris.Core.Name.UN', <<"[foreign]"/utf8>>}))(V8))), case V9 of {'Idris.Prelude.Types.Left', E13} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V11) -> begin (V12 = ('Idris.Idris2.TTImp.TTImp':'un--getFC'(V3))), begin (V13 = ('Idris.Idris2.Core.Normalise':'un--gnf'([], {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.PrimVal', V12, {'Idris.Core.TT.StringType'}}))), begin (V14 = ('Idris.Idris2.TTImp.Elab':'un--checkTerm'([], V0, V1, V2, V11, {'Idris.TTImp.Elab.Check.InExpr'}, [], [], {'Idris.Core.Env.Nil'}, V3, V13, V8))), case V14 of {'Idris.Prelude.Types.Left', E15} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V16) -> begin (V45 = begin (V44 = (('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 (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V19, V20, V21)) end end end end end, fun (V22) -> fun (V23) -> fun (V24) -> V23 end end end, fun (V25) -> fun (V26) -> fun (V27) -> fun (V28) -> fun (V29) -> begin (V30 = (V27(V29))), begin (V31 = (V28(V29))), (V30(V31)) end end end end end end end}, fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> fun (V36) -> begin (V37 = (V34(V36))), ((V35(V37))(V36)) end end end end end end, fun (V38) -> fun (V39) -> fun (V40) -> begin (V41 = (V39(V40))), (V41(V40)) end end end end}, fun (V42) -> fun (V43) -> V43 end end}, V0))(V8))), {'Idris.Prelude.Types.Right', V44} end), case V45 of {'Idris.Prelude.Types.Left', E17} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V47) -> begin (V48 = (('Idris.Idris2.Core.Normalise':'un--nf'(V0, [], V47, {'Idris.Core.Env.Nil'}, V16))(V8))), case V48 of {'Idris.Prelude.Types.Left', E19} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V50) -> case V50 of {'Idris.Core.Value.NPrimVal', E21, E22} -> (fun (V51, V52) -> case V52 of {'Idris.Core.TT.Str', E23} -> (fun (V53) -> {'Idris.Prelude.Types.Right', V53} end(E23)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V12, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V8)) end end(E21, E22)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V12, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V8)) end end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E11, E12)); _ -> fun (V54) -> begin (V55 = (('Idris.Idris2.Core.Context':'un--resolveName'(V0, {'Idris.Core.Name.UN', <<"[foreign]"/utf8>>}))(V54))), case V55 of {'Idris.Prelude.Types.Left', E0} -> (fun (V56) -> {'Idris.Prelude.Types.Left', V56} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V57) -> begin (V58 = ('Idris.Idris2.TTImp.TTImp':'un--getFC'(V3))), begin (V59 = ('Idris.Idris2.Core.Normalise':'un--gnf'([], {'Idris.Core.Env.Nil'}, {'Idris.Core.TT.PrimVal', V58, {'Idris.Core.TT.StringType'}}))), begin (V60 = ('Idris.Idris2.TTImp.Elab':'un--checkTerm'([], V0, V1, V2, V57, {'Idris.TTImp.Elab.Check.InExpr'}, [], [], {'Idris.Core.Env.Nil'}, V3, V59, V54))), case V60 of {'Idris.Prelude.Types.Left', E2} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V62) -> begin (V91 = begin (V90 = (('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 (V63) -> fun (V64) -> fun (V65) -> fun (V66) -> fun (V67) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V65, V66, V67)) end end end end end, fun (V68) -> fun (V69) -> fun (V70) -> V69 end end end, fun (V71) -> fun (V72) -> fun (V73) -> fun (V74) -> fun (V75) -> begin (V76 = (V73(V75))), begin (V77 = (V74(V75))), (V76(V77)) end end end end end end end}, fun (V78) -> fun (V79) -> fun (V80) -> fun (V81) -> fun (V82) -> begin (V83 = (V80(V82))), ((V81(V83))(V82)) end end end end end end, fun (V84) -> fun (V85) -> fun (V86) -> begin (V87 = (V85(V86))), (V87(V86)) end end end end}, fun (V88) -> fun (V89) -> V89 end end}, V0))(V54))), {'Idris.Prelude.Types.Right', V90} end), case V91 of {'Idris.Prelude.Types.Left', E4} -> (fun (V92) -> {'Idris.Prelude.Types.Left', V92} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V93) -> begin (V94 = (('Idris.Idris2.Core.Normalise':'un--nf'(V0, [], V93, {'Idris.Core.Env.Nil'}, V62))(V54))), case V94 of {'Idris.Prelude.Types.Left', E6} -> (fun (V95) -> {'Idris.Prelude.Types.Left', V95} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V96) -> case V96 of {'Idris.Core.Value.NPrimVal', E8, E9} -> (fun (V97, V98) -> case V98 of {'Idris.Core.TT.Str', E10} -> (fun (V99) -> {'Idris.Prelude.Types.Right', V99} end(E10)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V58, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V54)) end end(E8, E9)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V58, <<"%foreign calling convention must evaluate to a String"/utf8>>}, V54)) end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end.
'un--findInferrable'(V0, V1, V2) -> ('nested--10875-11913--in--un--fi'(V2, V1, V0, 0, 0, [], [], V2)).