idris2

-module('Idris.Idris2.Core.Context.Data').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--case block in addData-1399'/20,
  'case--addData-1314'/17,
  'case--case block in addData,addDataConstructors-1137'/21,
  'case--addData,addDataConstructors-1090'/18,
  'case--case block in getPs-827'/10,
  'case--getPs-800'/6,
  'case--updateParams,mergeArg-628'/15,
  'case--updateParams,couldBeParam-561'/5,
  'case--dropReps,toNothing-458'/14,
  'nested--6241-439--in--un--toNothing'/8,
  'nested--6559-728--in--un--shrink'/12,
  'nested--6370-603--in--un--mergeArg'/6,
  'nested--6753-899--in--un--justPos'/4,
  'nested--6370-547--in--un--couldBeParam'/5,
  'nested--6914-1055--in--un--conVisibility'/10,
  'nested--6914-1054--in--un--allDet'/10,
  'nested--6914-1056--in--un--addDataConstructors'/12,
  'un--updateParams'/4,
  'un--toPos'/2,
  'un--paramPos'/3,
  'un--getPs'/5,
  'un--getConPs'/5,
  'un--dropReps'/2,
  'un--addData'/5
]).
'case--case block in addData-1399'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19) -> case V9 of {'Idris.Core.Context.MkDefs', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25} -> (fun (V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45) -> {'Idris.Core.Context.MkDefs', V19, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45} end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--addData-1314'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16) -> case V16 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V17, V18) -> fun (V19) -> begin (V20 = (('nested--6914-1056--in--un--addDataConstructors'(V0, V1, V2, V3, V4, V5, V6, V7, V8, 0, V4, V18))(V19))), case V20 of {'Idris.Prelude.Types.Left', E2} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V22) -> begin (V77 = begin (V76 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V25, V26, V27)) end end end end end, fun (V28) -> fun (V29) -> fun (V30) -> V29 end end end, fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> begin (V36 = (V33(V35))), begin (V37 = (V34(V35))), (V36(V37)) end end end end end end end}, fun (V38) -> fun (V39) -> fun (V40) -> fun (V41) -> fun (V42) -> begin (V43 = (V40(V42))), ((V41(V43))(V42)) end end end end end end, fun (V44) -> fun (V45) -> fun (V46) -> begin (V47 = (V45(V46))), (V47(V46)) end end end end}, fun (V48) -> fun (V49) -> V49 end end}, V8, case V9 of {'Idris.Core.Context.MkDefs', 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, E29} -> (fun (V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75) -> {'Idris.Core.Context.MkDefs', V22, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64, V65, V66, V67, V68, V69, V70, V71, V72, V73, V74, V75} end(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, E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V19))), {'Idris.Prelude.Types.Right', V76} end), case V77 of {'Idris.Prelude.Types.Left', E30} -> (fun (V78) -> {'Idris.Prelude.Types.Left', V78} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V79) -> {'Idris.Prelude.Types.Right', V17} end(E31)); _ -> ('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--case block in addData,addDataConstructors-1137'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20) -> case V20 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('nested--6914-1056--in--un--addDataConstructors'(V0, V1, V2, V3, V4, V5, V6, V7, V8, ((V15 + 1) rem 9223372036854775808), V13, V18)) end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V21) -> fun (V22) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.AlreadyDefined', V12, V11}, V22)) end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--addData,addDataConstructors-1090'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17) -> case V17 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V18, V19) -> fun (V20) -> begin (V21 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V11, V14))(V20))), case V21 of {'Idris.Prelude.Types.Left', E2} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V23) -> case V23 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> (('nested--6914-1056--in--un--addDataConstructors'(V0, V1, V2, V3, V4, V5, V6, V7, V8, ((V15 + 1) rem 9223372036854775808), V13, V19))(V20)) end()); {'Idris.Prelude.Types.Just', E4} -> (fun (V24) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.AlreadyDefined', V12, V11}, V20)) end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--case block in getPs-827'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of 0 -> fun (V10) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V11) -> case V11 of {'Idris.Prelude.Types.Left', E0} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V13}} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('un--updateParams'(V0, V1, V4, V8)), V10)) end; 1 -> fun (V14) -> {'Idris.Prelude.Types.Right', V4} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--getPs-800'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V6, V7) -> case V6 of {'Idris.Core.TT.Ref', E2, E3, E4} -> (fun (V8, V9, V10) -> ('case--case block in getPs-827'(V0, V1, V2, V3, V4, V8, V9, V10, V7, ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V10, V3)))) end(E2, E3, E4)); _ -> fun (V11) -> {'Idris.Prelude.Types.Right', V4} end end end(E0, E1)); _ -> fun (V12) -> {'Idris.Prelude.Types.Right', V4} end end.
'case--updateParams,mergeArg-628'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14) -> case V14 of 0 -> {'Idris.Prelude.Types.Just', {'Idris.Core.TT.Local', V13, V12, V10}}; 1 -> {'Idris.Prelude.Types.Nothing'}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--updateParams,couldBeParam-561'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.TT.Local', E0, E1, E2} -> (fun (V5, V6, V7) -> {'Idris.Prelude.Types.Just', {'Idris.Core.TT.Local', V5, V6, V7}} end(E0, E1, E2)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'case--dropReps,toNothing-458'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13) -> case V13 of 0 -> {'Idris.Prelude.Types.Nothing'}; 1 -> V12; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--6241-439--in--un--toNothing'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Prelude.Types.Just', E0} -> (fun (V8) -> case V8 of {'Idris.Core.TT.Local', E1, E2, E3} -> (fun (V9, V10, V11) -> begin (V12 = {'Idris.Prelude.Types.Just', {'Idris.Core.TT.Local', V9, V10, V11}}), ('case--dropReps,toNothing-458'('erased', V1, 'erased', 'erased', V4, V5, V6, 'erased', V9, V10, V11, 'erased', V12, ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V1, V11)))) end end(E1, E2, E3)); _ -> V7 end end(E0)); _ -> V7 end.
'nested--6559-728--in--un--shrink'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11) -> case V11 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V12) -> ('Idris.Idris2.Core.TT':'un--shrinkTerm'('erased', 'erased', V12, {'Idris.Core.TT.DropCons', {'Idris.Core.TT.SubRefl'}})) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--6370-603--in--un--mergeArg'(V0, V1, V2, V3, V4, V5) -> case V4 of {'Idris.Prelude.Types.Just', E0} -> (fun (V6) -> case V6 of {'Idris.Core.TT.Local', E1, E2, E3} -> (fun (V7, V8, V9) -> case V5 of {'Idris.Core.TT.Local', E4, E5, E6} -> (fun (V10, V11, V12) -> ('case--updateParams,mergeArg-628'(V0, V1, V2, V3, 'erased', V10, V11, V12, 'erased', 'erased', V9, 'erased', V8, V7, ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V9, V12)))) end(E4, E5, E6)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E1, E2, E3)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E0)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'nested--6753-899--in--un--justPos'(V0, V1, V2, V3) -> case V3 of [] -> []; [E0 | E1] -> (fun (V4, V5) -> case V4 of {'Idris.Prelude.Types.Just', E2} -> (fun (V6) -> [V2 | ('nested--6753-899--in--un--justPos'('erased', V1, ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types':'dn--un--fromInteger_Num__Nat'(1)), V2)), V5))] end(E2)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> ('nested--6753-899--in--un--justPos'('erased', V1, ('Idris.Idris2.Prelude.Types':'dn--un--+_Num__Nat'(('Idris.Idris2.Prelude.Types':'dn--un--fromInteger_Num__Nat'(1)), V2)), V5)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--6370-547--in--un--couldBeParam'(V0, V1, V2, V3, V4) -> begin (V5 = ('Idris.Idris2.Core.Normalise':'un--etaContract'(V0, V1, V3, V4))), case V5 of {'Idris.Prelude.Types.Left', E0} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V7) -> {'Idris.Prelude.Types.Right', case V7 of {'Idris.Core.TT.Local', E2, E3, E4} -> (fun (V8, V9, V10) -> {'Idris.Prelude.Types.Just', {'Idris.Core.TT.Local', V8, V9, V10}} end(E2, E3, E4)); _ -> {'Idris.Prelude.Types.Nothing'} end} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'nested--6914-1055--in--un--conVisibility'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.TT.Export'} -> (fun () -> {'Idris.Core.TT.Private'} end()); _ -> V9 end.
'nested--6914-1054--in--un--allDet'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of 0 -> []; _ -> begin (V10 = (V9 - 1)), ('Idris.Idris2.Prelude.Types':'dn--un--rangeFromTo_Range__Nat'(0, V10)) end end.
'nested--6914-1056--in--un--addDataConstructors'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11) -> case V10 of [] -> fun (V12) -> {'Idris.Prelude.Types.Right', V11} end; [E0 | E1] -> (fun (V13, V14) -> case V13 of {'Idris.Core.Context.MkCon', E2, E3, E4, E5} -> (fun (V15, V16, V17, V18) -> begin (V19 = ('Idris.Idris2.Core.Context':'un--newDef'(V15, V16, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'()), V7, V18, ('nested--6914-1055--in--un--conVisibility'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V6)), {'Idris.Core.Context.DCon', V9, V17, {'Idris.Prelude.Types.Nothing'}}))), fun (V20) -> begin (V21 = (('Idris.Idris2.Core.Context':'un--addCtxt'(V16, V19, V11))(V20))), case V21 of {'Idris.Prelude.Types.Left', E6} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V23) -> case V23 of {'Idris.Builtin.MkPair', E8, E9} -> (fun (V24, V25) -> begin (V26 = (('Idris.Idris2.Core.Context':'un--lookupCtxtExact'(V16, V11))(V20))), case V26 of {'Idris.Prelude.Types.Left', E10} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V28) -> case V28 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> (('nested--6914-1056--in--un--addDataConstructors'(V0, V1, V2, V3, V4, V5, V6, V7, V8, ((V9 + 1) rem 9223372036854775808), V14, V25))(V20)) end()); {'Idris.Prelude.Types.Just', E12} -> (fun (V29) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.AlreadyDefined', V15, V16}, V20)) end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E8, E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end(E2, E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--updateParams'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V4) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V5) -> case V5 of {'Idris.Prelude.Types.Left', E0} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V7) -> {'Idris.Prelude.Types.Right', ('un--dropReps'('erased', V7))} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V8) -> fun (V9) -> ('nested--6370-547--in--un--couldBeParam'(V0, V1, V3, V8, V9)) end end, V3)), V4)) end end()); {'Idris.Prelude.Types.Just', E2} -> (fun (V10) -> fun (V11) -> {'Idris.Prelude.Types.Right', ('un--dropReps'('erased', ('Idris.Idris2.Data.List':'un--zipWith'('erased', 'erased', 'erased', fun (V12) -> fun (V13) -> ('nested--6370-603--in--un--mergeArg'(V0, V1, V10, V3, V12, V13)) end end, V10, V3))))} end end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--toPos'(V0, V1) -> case V1 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> [] end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V2) -> ('nested--6753-899--in--un--justPos'('erased', V2, 0, V2)) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--paramPos'(V0, V1, V2) -> case V2 of [] -> fun (V3) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end; _ -> fun (V4) -> begin (V6 = (('Idris.Idris2.Core.Core':'un--traverse'('erased', 'erased', fun (V5) -> ('un--getConPs'(V0, [], {'Idris.Prelude.Types.Nothing'}, V1, V5)) end, V2))(V4))), case V6 of {'Idris.Prelude.Types.Left', E0} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V8) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', ('Idris.Idris2.Data.List':'un--intersectAll'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.Types':'dn--un--==_Eq__Nat'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.Types':'dn--un--/=_Eq__Nat'(V11, V12)) end end}, V8))}} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end.
'un--getPs'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.TT.Bind', 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 (V17 = (('un--getPs'(V0, [V6 | V1], ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V14) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V15) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V16) -> ('Idris.Idris2.Core.TT':'dn--un--weaken_Weaken__Term'('erased', 'erased', V16)) end, V15)) end, V14)) end, V2)), V3, V8))(V13))), case V17 of {'Idris.Prelude.Types.Left', E8} -> (fun (V18) -> {'Idris.Prelude.Types.Left', V18} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V19) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V20) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V21) -> ('nested--6559-728--in--un--shrink'(V0, V1, V5, V9, V10, V11, V12, V6, V8, V3, V2, V21)) end, V20)) end, V19))} end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E4, E5, E6, E7)); _ -> ('case--getPs-800'(V0, V1, V4, V3, V2, ('Idris.Idris2.Core.TT':'un--getFnArgs'('erased', V4)))) end end(E0, E1, E2, E3)); _ -> ('case--getPs-800'(V0, V1, V4, V3, V2, ('Idris.Idris2.Core.TT':'un--getFnArgs'('erased', V4)))) end.
'un--getConPs'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.TT.Bind', E2, E3, E4, E5} -> (fun (V5, V6, V7, V8) -> case V7 of {'Idris.Core.TT.Pi', E8, E9, E10, E11} -> (fun (V9, V10, V11, V12) -> fun (V13) -> begin (V14 = (('un--getPs'(V0, V1, V2, V3, V12))(V13))), case V14 of {'Idris.Prelude.Types.Left', E12} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V16) -> (('un--getConPs'(V0, [V6 | V1], ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V17) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V18) -> ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__Maybe'('erased', 'erased', fun (V19) -> ('Idris.Idris2.Core.TT':'dn--un--weaken_Weaken__Term'('erased', 'erased', V19)) end, V18)) end, V17)) end, V16)), V3, V8))(V13)) end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E8, E9, E10, E11)); {'Idris.Core.TT.Let', E14, E15, E16, E17} -> (fun (V20, V21, V22, V23) -> ('un--getConPs'(V0, V1, V2, V3, ('Idris.Idris2.Core.TT.SubstEnv':'un--subst'('erased', 'erased', V22, V8)))) end(E14, E15, E16, E17)); _ -> fun (V24) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V25) -> case V25 of {'Idris.Prelude.Types.Left', E6} -> (fun (V26) -> {'Idris.Prelude.Types.Left', V26} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V27) -> {'Idris.Prelude.Types.Right', ('un--toPos'('erased', V27))} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('un--getPs'(V0, V1, V2, V3, V4)), V24)) end end end(E2, E3, E4, E5)); _ -> fun (V28) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', fun (V29) -> case V29 of {'Idris.Prelude.Types.Left', E0} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V31) -> {'Idris.Prelude.Types.Right', ('un--toPos'('erased', V31))} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, ('un--getPs'(V0, V1, V2, V3, V4)), V28)) end end.
'un--dropReps'(V0, V1) -> case V1 of [] -> []; [E0 | E1] -> (fun (V2, V3) -> case V2 of {'Idris.Prelude.Types.Just', E2} -> (fun (V4) -> case V4 of {'Idris.Core.TT.Local', E3, E4, E5} -> (fun (V5, V6, V7) -> [{'Idris.Prelude.Types.Just', {'Idris.Core.TT.Local', V5, V6, V7}} | ('un--dropReps'('erased', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V8) -> ('nested--6241-439--in--un--toNothing'('erased', V7, 'erased', 'erased', V6, V5, V3, V8)) end, V3))))] end(E3, E4, E5)); _ -> [V2 | ('un--dropReps'('erased', V3))] end end(E2)); _ -> [V2 | ('un--dropReps'('erased', V3))] end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--addData'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.Context.MkData', E0, E1} -> (fun (V5, V6) -> case V5 of {'Idris.Core.Context.MkCon', E2, E3, E4, E5} -> (fun (V7, V8, V9, V10) -> fun (V11) -> begin (V40 = begin (V39 = (('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 (V12) -> fun (V13) -> fun (V14) -> fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V14, V15, V16)) end end end end end, fun (V17) -> fun (V18) -> fun (V19) -> V18 end end end, fun (V20) -> fun (V21) -> fun (V22) -> fun (V23) -> fun (V24) -> begin (V25 = (V22(V24))), begin (V26 = (V23(V24))), (V25(V26)) end end end end end end end}, fun (V27) -> fun (V28) -> fun (V29) -> fun (V30) -> fun (V31) -> begin (V32 = (V29(V31))), ((V30(V32))(V31)) end end end end end end, fun (V33) -> fun (V34) -> fun (V35) -> begin (V36 = (V34(V35))), (V36(V35)) end end end end}, fun (V37) -> fun (V38) -> V38 end end}, V0))(V11))), {'Idris.Prelude.Types.Right', V39} end), case V40 of {'Idris.Prelude.Types.Left', E6} -> (fun (V41) -> {'Idris.Prelude.Types.Left', V41} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V42) -> begin (V43 = ('Idris.Idris2.Core.Context':'un--getNextTypeTag'(V0, V11))), 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 (V46 = ('nested--6914-1054--in--un--allDet'(V10, V9, V8, V7, V6, V3, V2, V1, V0, V9))), begin (V52 = (('un--paramPos'(V0, {'Idris.Core.Name.Resolved', V3}, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V47) -> case V47 of {'Idris.Core.Context.MkCon', E10, E11, E12, E13} -> (fun (V48, V49, V50, V51) -> V51 end(E10, E11, E12, E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, V6))))(V11))), case V52 of {'Idris.Prelude.Types.Left', E14} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V54) -> begin (V55 = ('Idris.Idris2.Data.Maybe':'un--fromMaybe'('erased', fun () -> V46 end, V54))), begin (V57 = (('Idris.Idris2.Core.Context.Log':'un--log'(V0, <<"declare.data.parameters"/utf8>>, (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))))))))))))), fun () -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Positions of parameters for datatype"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V8)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<": ["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name.Namespace':'un--showSep'(<<", "/utf8>>, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V56) -> ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V56)) end, V55)))), <<"]"/utf8>>)))))))) end))(V11))), case V57 of {'Idris.Prelude.Types.Left', E16} -> (fun (V58) -> {'Idris.Prelude.Types.Left', V58} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V59) -> begin (V65 = ('Idris.Idris2.Core.Context':'un--newDef'(V7, V8, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'()), V1, V10, V2, {'Idris.Core.Context.TCon', V45, V9, V55, V46, ('Idris.Idris2.Core.Context':'un--defaultFlags'()), [], ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V60) -> case V60 of {'Idris.Core.Context.MkCon', E18, E19, E20, E21} -> (fun (V61, V62, V63, V64) -> V62 end(E18, E19, E20, E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, V6)), {'Idris.Prelude.Types.Nothing'}}))), begin (V92 = (('Idris.Idris2.Core.Context':'un--addCtxt'(V8, V65, case V42 of {'Idris.Core.Context.MkDefs', E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47} -> (fun (V66, V67, V68, V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85, V86, V87, V88, V89, V90, V91) -> V66 end(E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V11))), case V92 of {'Idris.Prelude.Types.Left', E48} -> (fun (V93) -> {'Idris.Prelude.Types.Left', V93} end(E48)); {'Idris.Prelude.Types.Right', E49} -> (fun (V94) -> case V94 of {'Idris.Builtin.MkPair', E50, E51} -> (fun (V95, V96) -> begin (V97 = (('nested--6914-1056--in--un--addDataConstructors'(V10, V9, V8, V7, V6, V3, V2, V1, V0, 0, V6, V96))(V11))), case V97 of {'Idris.Prelude.Types.Left', E52} -> (fun (V98) -> {'Idris.Prelude.Types.Left', V98} end(E52)); {'Idris.Prelude.Types.Right', E53} -> (fun (V99) -> begin (V154 = begin (V153 = (('Idris.Idris2.Erlang.Data.IORef':'un--writeIORef'('erased', 'erased', {'Idris.Prelude.IO.dn--un--__mkHasIO', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V100) -> fun (V101) -> fun (V102) -> fun (V103) -> fun (V104) -> ('Idris.Idris2.Prelude.IO':'dn--un--map_Functor__IO'('erased', 'erased', V102, V103, V104)) end end end end end, fun (V105) -> fun (V106) -> fun (V107) -> V106 end end end, fun (V108) -> fun (V109) -> fun (V110) -> fun (V111) -> fun (V112) -> begin (V113 = (V110(V112))), begin (V114 = (V111(V112))), (V113(V114)) end end end end end end end}, fun (V115) -> fun (V116) -> fun (V117) -> fun (V118) -> fun (V119) -> begin (V120 = (V117(V119))), ((V118(V120))(V119)) end end end end end end, fun (V121) -> fun (V122) -> fun (V123) -> begin (V124 = (V122(V123))), (V124(V123)) end end end end}, fun (V125) -> fun (V126) -> V126 end end}, V0, case V42 of {'Idris.Core.Context.MkDefs', E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79} -> (fun (V127, V128, V129, V130, V131, V132, V133, V134, V135, V136, V137, V138, V139, V140, V141, V142, V143, V144, V145, V146, V147, V148, V149, V150, V151, V152) -> {'Idris.Core.Context.MkDefs', V99, V128, V129, V130, V131, V132, V133, V134, V135, V136, V137, V138, V139, V140, V141, V142, V143, V144, V145, V146, V147, V148, V149, V150, V151, V152} end(E54, E55, E56, E57, E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end))(V11))), {'Idris.Prelude.Types.Right', V153} end), case V154 of {'Idris.Prelude.Types.Left', E80} -> (fun (V155) -> {'Idris.Prelude.Types.Left', V155} end(E80)); {'Idris.Prelude.Types.Right', E81} -> (fun (V156) -> {'Idris.Prelude.Types.Right', V95} end(E81)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E53)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E50, E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E49)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E2, E3, E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.