Packages
idris2

0.2.1-alpha.1
Erlang code generator for Idris 2
Current section
Files
Jump to
Readme 1 Version 0 Dependencies Dependants Files Activity
idris2 src Idris.Idris2.Core.Value.erl
Raw
src/Idris.Idris2.Core.Value.erl

-module('Idris.Idris2.Core.Value').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--onLHS-3035'/1,
  'case--tcOnly-3022'/1,
  'dn--un--show_Show__(NHead $free)'/2,
  'dn--un--show_Show__(NF $free)'/2,
  'dn--un--showPrec_Show__(NHead $free)'/3,
  'dn--un--showPrec_Show__(NF $free)'/3,
  'dn--un--__Impl_Show_(NHead $free)'/1,
  'dn--un--__Impl_Show_(NF $free)'/1,
  'un--withHoles'/0,
  'un--withArgHoles'/0,
  'un--withAll'/0,
  'un--tcOnly'/0,
  'un--onLHS'/0,
  'un--getLoc'/2,
  'un--defaultOpts'/0
]).
'case--onLHS-3035'(V0) -> case V0 of {'Idris.Core.Value.MkEvalOpts', E0, E1, E2, E3, E4, E5, E6, E7} -> (fun (V1, V2, V3, V4, V5, V6, V7, V8) -> {'Idris.Core.Value.MkEvalOpts', V1, V2, 1, V4, V5, V6, V7, V8} end(E0, E1, E2, E3, E4, E5, E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--tcOnly-3022'(V0) -> case V0 of {'Idris.Core.Value.MkEvalOpts', E0, E1, E2, E3, E4, E5, E6, E7} -> (fun (V1, V2, V3, V4, V5, V6, V7, V8) -> {'Idris.Core.Value.MkEvalOpts', V1, V2, V3, V4, V5, 0, V7, V8} end(E0, E1, E2, E3, E4, E5, E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__(NHead $free)'(V0, V1) -> case V1 of {'Idris.Core.Value.NLocal', E0, E1} -> (fun (V2, V3) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(('Idris.Idris2.Core.TT':'un--nameAt'('erased', V0, V3, 'erased')))), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(V3)), <<"]"/utf8>>)))))) end(E0, E1)); {'Idris.Core.Value.NRef', E2, E3} -> (fun (V4, V5) -> ('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V5)) end(E2, E3)); {'Idris.Core.Value.NMeta', E4, E5, E6} -> (fun (V6, V7, V8) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"?"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"_["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V8)))), <<" closures]"/utf8>>)))))))) end(E4, E5, E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__(NF $free)'(V0, V1) -> case V1 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V2, V3, V4, V5) -> case V4 of {'Idris.Core.TT.Lam', E4, E5, E6, E7} -> (fun (V6, V7, V8, V9) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"\x{5c}"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'un--withPiInfo'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V10) -> ('dn--un--show_Show__(NF $free)'(V0, V10)) end, fun (V11) -> fun (V12) -> ('dn--un--showPrec_Show__(NF $free)'(V0, V11, V12)) end end}, V8, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V7)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('dn--un--show_Show__(NF $free)'(V0, V9)))))))))), <<" => [closure]"/utf8>>)))) end(E4, E5, E6, E7)); {'Idris.Core.TT.Let', E8, E9, E10, E11} -> (fun (V13, V14, V15, V16) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"let "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V14)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V16)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" = "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V15)), <<" in [closure]"/utf8>>)))))))))))))) end(E8, E9, E10, E11)); {'Idris.Core.TT.Pi', E12, E13, E14, E15} -> (fun (V17, V18, V19, V20) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'un--withPiInfo'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V21) -> ('dn--un--show_Show__(NF $free)'(V0, V21)) end, fun (V22) -> fun (V23) -> ('dn--un--showPrec_Show__(NF $free)'(V0, V22, V23)) end end}, V19, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V18)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('dn--un--show_Show__(NF $free)'(V0, V20)))))))))), <<" -> [closure]"/utf8>>)) end(E12, E13, E14, E15)); {'Idris.Core.TT.PVar', E16, E17, E18, E19} -> (fun (V24, V25, V26, V27) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.TT':'un--withPiInfo'('erased', {'Idris.Prelude.Show.dn--un--__mkShow', fun (V28) -> ('dn--un--show_Show__(NF $free)'(V0, V28)) end, fun (V29) -> fun (V30) -> ('dn--un--showPrec_Show__(NF $free)'(V0, V29, V30)) end end}, V26, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"pat "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V25)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('dn--un--show_Show__(NF $free)'(V0, V27)))))))))))), <<" => [closure]"/utf8>>)) end(E16, E17, E18, E19)); {'Idris.Core.TT.PLet', E20, E21, E22, E23} -> (fun (V31, V32, V33, V34) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"plet "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V32)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V34)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" = "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V33)), <<" in [closure]"/utf8>>)))))))))))))) end(E20, E21, E22, E23)); {'Idris.Core.TT.PVTy', E24, E25, E26} -> (fun (V35, V36, V37) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"pty "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Algebra':'un--showCount'(V36)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V3)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" : "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V37)), <<" => [closure]"/utf8>>)))))))))) end(E24, E25, E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1, E2, E3)); {'Idris.Core.Value.NApp', E27, E28, E29} -> (fun (V38, V39, V40) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NHead $free)'(V0, V39)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" ["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V40)))), <<" closures]"/utf8>>)))))) end(E27, E28, E29)); {'Idris.Core.Value.NDCon', E30, E31, E32, E33, E34} -> (fun (V41, V42, V43, V44, V45) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V42)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" ["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V45)))), <<" closures]"/utf8>>)))))) end(E30, E31, E32, E33, E34)); {'Idris.Core.Value.NTCon', E35, E36, E37, E38, E39} -> (fun (V46, V47, V48, V49, V50) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name':'dn--un--show_Show__Name'(V47)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" ["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V50)))), <<" closures]"/utf8>>)))))) end(E35, E36, E37, E38, E39)); {'Idris.Core.Value.NAs', E40, E41, E42, E43} -> (fun (V51, V52, V53, V54) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V53)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"@"/utf8>>, ('dn--un--show_Show__(NF $free)'(V0, V54)))))) end(E40, E41, E42, E43)); {'Idris.Core.Value.NDelayed', E44, E45, E46} -> (fun (V55, V56, V57) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"%Delayed "/utf8>>, ('dn--un--show_Show__(NF $free)'(V0, V57)))) end(E44, E45, E46)); {'Idris.Core.Value.NDelay', E47, E48, E49, E50} -> (fun (V58, V59, V60, V61) -> <<"%Delay [closure]"/utf8>> end(E47, E48, E49, E50)); {'Idris.Core.Value.NForce', E51, E52, E53, E54} -> (fun (V62, V63, V64, V65) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"%Force "/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__(NF $free)'(V0, V64)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<" ["/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Nat'(('Idris.Idris2.Prelude.Types.List':'un--length'('erased', V65)))), <<" closures]"/utf8>>)))))))) end(E51, E52, E53, E54)); {'Idris.Core.Value.NPrimVal', E55, E56} -> (fun (V66, V67) -> ('Idris.Idris2.Core.TT':'dn--un--show_Show__Constant'(V67)) end(E55, E56)); {'Idris.Core.Value.NErased', E57, E58} -> (fun (V68, V69) -> <<"[__]"/utf8>> end(E57, E58)); {'Idris.Core.Value.NType', E59} -> (fun (V70) -> <<"Type"/utf8>> end(E59)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--showPrec_Show__(NHead $free)'(V0, V1, V2) -> ('dn--un--show_Show__(NHead $free)'(V0, V2)).
'dn--un--showPrec_Show__(NF $free)'(V0, V1, V2) -> ('dn--un--show_Show__(NF $free)'(V0, V2)).
'dn--un--__Impl_Show_(NHead $free)'(V0) -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V1) -> ('dn--un--show_Show__(NHead $free)'(V0, V1)) end, fun (V2) -> fun (V3) -> ('dn--un--showPrec_Show__(NHead $free)'(V0, V2, V3)) end end}.
'dn--un--__Impl_Show_(NF $free)'(V0) -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V1) -> ('dn--un--show_Show__(NF $free)'(V0, V1)) end, fun (V2) -> fun (V3) -> ('dn--un--showPrec_Show__(NF $free)'(V0, V2, V3)) end end}.
'un--withHoles'() -> {'Idris.Core.Value.MkEvalOpts', 0, 0, 1, ('Idris.Idris2.Data.IntMap':'un--empty'('erased')), 1, 1, {'Idris.Prelude.Types.Nothing'}, []}.
'un--withArgHoles'() -> {'Idris.Core.Value.MkEvalOpts', 1, 0, 1, ('Idris.Idris2.Data.IntMap':'un--empty'('erased')), 1, 1, {'Idris.Prelude.Types.Nothing'}, []}.
'un--withAll'() -> {'Idris.Core.Value.MkEvalOpts', 1, 1, 0, ('Idris.Idris2.Data.IntMap':'un--empty'('erased')), 0, 1, {'Idris.Prelude.Types.Nothing'}, []}.
'un--tcOnly'() -> ('case--tcOnly-3022'(('un--withArgHoles'()))).
'un--onLHS'() -> ('case--onLHS-3035'(('un--defaultOpts'()))).
'un--getLoc'(V0, V1) -> case V1 of {'Idris.Core.Value.NBind', E0, E1, E2, E3} -> (fun (V2, V3, V4, V5) -> V2 end(E0, E1, E2, E3)); {'Idris.Core.Value.NApp', E4, E5, E6} -> (fun (V6, V7, V8) -> V6 end(E4, E5, E6)); {'Idris.Core.Value.NDCon', E7, E8, E9, E10, E11} -> (fun (V9, V10, V11, V12, V13) -> V9 end(E7, E8, E9, E10, E11)); {'Idris.Core.Value.NTCon', E12, E13, E14, E15, E16} -> (fun (V14, V15, V16, V17, V18) -> V14 end(E12, E13, E14, E15, E16)); {'Idris.Core.Value.NAs', E17, E18, E19, E20} -> (fun (V19, V20, V21, V22) -> V19 end(E17, E18, E19, E20)); {'Idris.Core.Value.NDelayed', E21, E22, E23} -> (fun (V23, V24, V25) -> V23 end(E21, E22, E23)); {'Idris.Core.Value.NDelay', E24, E25, E26, E27} -> (fun (V26, V27, V28, V29) -> V26 end(E24, E25, E26, E27)); {'Idris.Core.Value.NForce', E28, E29, E30, E31} -> (fun (V30, V31, V32, V33) -> V30 end(E28, E29, E30, E31)); {'Idris.Core.Value.NPrimVal', E32, E33} -> (fun (V34, V35) -> V34 end(E32, E33)); {'Idris.Core.Value.NErased', E34, E35} -> (fun (V36, V37) -> V36 end(E34, E35)); {'Idris.Core.Value.NType', E36} -> (fun (V38) -> V38 end(E36)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--defaultOpts'() -> {'Idris.Core.Value.MkEvalOpts', 1, 1, 0, ('Idris.Idris2.Data.IntMap':'un--empty'('erased')), 1, 1, {'Idris.Prelude.Types.Nothing'}, []}.
Operator	Description	Example
name:	Match package name. Supports * wildcards and repo/package form	name:phx* or name:hexpm/phoenix
description:	Full-text search of package descriptions	description:auth
depends:	Packages depending on a given package. Supports repo:package form	depends:ecto or depends:hexpm:ecto
build_tool:	Filter by build tool	build_tool:mix
updated_after:	Packages updated after an ISO8601 datetime	updated_after:2025-01-01T00:00:00Z
extra:	Match custom metadata (key,value). Nested keys are separated by commas	extra:license,MIT