7b58024 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2547 from Melvar/fix-number-show

7b58024David Christiansen11 years ago

libs/prelude/Prelude/Show.idr+11−8

compare with master

unifiedsplit

@@ -91,19 +91,22 @@ showCon d conName shownArgs = showParens (d >= App) $ conName ++ shownArgs

91showArg : Show a => (x : a) -> String

92showArg x = " " ++ showPrec App x

94+firstCharIs : (Char -> Bool) -> String -> Bool

95+firstCharIs p s with (strM s)

96+ firstCharIs p "" | StrNil = False

97+ firstCharIs p (strCons c cs) | StrCons c cs = p c

98+

99+primNumShow : (a -> String) -> Prec -> a -> String

100+primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str

101+

94instance Show Int where

102instance Show Int where

95− show = prim__toStrInt

103+ showPrec = primNumShow prim__toStrInt

104

97instance Show Integer where

105instance Show Integer where

98− show = prim__toStrBigInt

106+ showPrec = primNumShow prim__toStrBigInt

107

100instance Show Double where

108instance Show Double where

101− show = prim__floatToStr

109+ showPrec = primNumShow prim__floatToStr

102−

103−firstCharIs : (Char -> Bool) -> String -> Bool

104−firstCharIs p s with (strM s)

105− firstCharIs p "" | StrNil = False

106− firstCharIs p (strCons c cs) | StrCons c cs = p c

107

110

108protectEsc : (Char -> Bool) -> String -> String -> String

111protectEsc : (Char -> Bool) -> String -> String -> String

109protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s

112protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s

rts/idris_rts.c+1−1

@@ -470,7 +470,7 @@ VAL idris_castFloatStr(VM* vm, VAL i) {

470 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);

471 SETTY(cl, STRING);

472 cl -> info.str = (char*)cl + sizeof(Closure);

473− sprintf(cl -> info.str, "%g", GETFLOAT(i));

473+ snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));

474 return cl;

475}

476

src/IRTS/CodegenJavaScript.hs+75−184

@@ -695,15 +695,15 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

695 | (LSRem (ATInt ITBig)) <- op

696 , (lhs:rhs:_) <- args = invokeMeth lhs "mod" [rhs]

697 | (LEq (ATInt ITBig)) <- op

698− , (lhs:rhs:_) <- args = invokeMeth lhs "equals" [rhs]

698+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "equals" [rhs]

699 | (LSLt (ATInt ITBig)) <- op

700− , (lhs:rhs:_) <- args = invokeMeth lhs "lesser" [rhs]

700+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "lesser" [rhs]

701 | (LSLe (ATInt ITBig)) <- op

702− , (lhs:rhs:_) <- args = invokeMeth lhs "lesserOrEquals" [rhs]

702+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "lesserOrEquals" [rhs]

703 | (LSGt (ATInt ITBig)) <- op

704− , (lhs:rhs:_) <- args = invokeMeth lhs "greater" [rhs]

704+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "greater" [rhs]

705 | (LSGe (ATInt ITBig)) <- op

706− , (lhs:rhs:_) <- args = invokeMeth lhs "greaterOrEquals" [rhs]

706+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "greaterOrEquals" [rhs]

707

708 | (LPlus ATFloat) <- op

709 , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs

@@ -714,15 +714,15 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

714 | (LSDiv ATFloat) <- op

715 , (lhs:rhs:_) <- args = translateBinaryOp "/" lhs rhs

716 | (LEq ATFloat) <- op

717− , (lhs:rhs:_) <- args = translateBinaryOp "==" lhs rhs

717+ , (lhs:rhs:_) <- args = translateCompareOp "==" lhs rhs

718 | (LSLt ATFloat) <- op

719− , (lhs:rhs:_) <- args = translateBinaryOp "<" lhs rhs

719+ , (lhs:rhs:_) <- args = translateCompareOp "<" lhs rhs

720 | (LSLe ATFloat) <- op

721− , (lhs:rhs:_) <- args = translateBinaryOp "<=" lhs rhs

721+ , (lhs:rhs:_) <- args = translateCompareOp "<=" lhs rhs

722 | (LSGt ATFloat) <- op

723− , (lhs:rhs:_) <- args = translateBinaryOp ">" lhs rhs

723+ , (lhs:rhs:_) <- args = translateCompareOp ">" lhs rhs

724 | (LSGe ATFloat) <- op

725− , (lhs:rhs:_) <- args = translateBinaryOp ">=" lhs rhs

725+ , (lhs:rhs:_) <- args = translateCompareOp ">=" lhs rhs

726

727 | (LPlus (ATInt ITChar)) <- op

728 , (lhs:rhs:_) <- args =

@@ -761,44 +761,26 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

761 ]

762

763 | (LLSHR (ITFixed IT8)) <- op

764− , (lhs:rhs:_) <- args =

765− jsPackUBits8 (

764+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp ">>" lhs rhs

766− JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

767− )

768

765

769 | (LLSHR (ITFixed IT16)) <- op

766 | (LLSHR (ITFixed IT16)) <- op

770− , (lhs:rhs:_) <- args =

771− jsPackUBits16 (

767+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp ">>" lhs rhs

772− JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

773− )

774

768

775 | (LLSHR (ITFixed IT32)) <- op

769 | (LLSHR (ITFixed IT32)) <- op

776− , (lhs:rhs:_) <- args =

777− jsPackUBits32 (

770+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp ">>" lhs rhs

778− JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

779− )

780

771

781 | (LLSHR (ITFixed IT64)) <- op

772 | (LLSHR (ITFixed IT64)) <- op

782 , (lhs:rhs:_) <- args =

773 , (lhs:rhs:_) <- args =

783 jsMeth (translateReg lhs) "shiftRight" [translateReg rhs]

774 jsMeth (translateReg lhs) "shiftRight" [translateReg rhs]

784

775

785 | (LSHL (ITFixed IT8)) <- op

776 | (LSHL (ITFixed IT8)) <- op

786− , (lhs:rhs:_) <- args =

787− jsPackUBits8 (

777+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "<<" lhs rhs

788− JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

789− )

790

778

791 | (LSHL (ITFixed IT16)) <- op

779 | (LSHL (ITFixed IT16)) <- op

792− , (lhs:rhs:_) <- args =

793− jsPackUBits16 (

780+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "<<" lhs rhs

794− JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

795− )

796

781

797 | (LSHL (ITFixed IT32)) <- op

782 | (LSHL (ITFixed IT32)) <- op

798− , (lhs:rhs:_) <- args =

799− jsPackUBits32 (

783+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "<<" lhs rhs

800− JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)

801− )

802

784

803 | (LSHL (ITFixed IT64)) <- op

785 | (LSHL (ITFixed IT64)) <- op

804 , (lhs:rhs:_) <- args =

786 , (lhs:rhs:_) <- args =

@@ -807,88 +789,52 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

807 ]

789 ]

808

790

809 | (LAnd (ITFixed IT8)) <- op

791 | (LAnd (ITFixed IT8)) <- op

810− , (lhs:rhs:_) <- args =

811− jsPackUBits8 (

792+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "&" lhs rhs

812− JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

813− )

814

793

815 | (LAnd (ITFixed IT16)) <- op

794 | (LAnd (ITFixed IT16)) <- op

816− , (lhs:rhs:_) <- args =

817− jsPackUBits16 (

795+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "&" lhs rhs

818− JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

819− )

820

796

821 | (LAnd (ITFixed IT32)) <- op

797 | (LAnd (ITFixed IT32)) <- op

822− , (lhs:rhs:_) <- args =

823− jsPackUBits32 (

798+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "&" lhs rhs

824− JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

825− )

826

799

827 | (LAnd (ITFixed IT64)) <- op

800 | (LAnd (ITFixed IT64)) <- op

828 , (lhs:rhs:_) <- args =

801 , (lhs:rhs:_) <- args =

829 jsMeth (translateReg lhs) "and" [translateReg rhs]

802 jsMeth (translateReg lhs) "and" [translateReg rhs]

830

803

831 | (LOr (ITFixed IT8)) <- op

804 | (LOr (ITFixed IT8)) <- op

832− , (lhs:rhs:_) <- args =

833− jsPackUBits8 (

805+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "|" lhs rhs

834− JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

835− )

836

806

837 | (LOr (ITFixed IT16)) <- op

807 | (LOr (ITFixed IT16)) <- op

838− , (lhs:rhs:_) <- args =

839− jsPackUBits16 (

808+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "|" lhs rhs

840− JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

841− )

842

809

843 | (LOr (ITFixed IT32)) <- op

810 | (LOr (ITFixed IT32)) <- op

844− , (lhs:rhs:_) <- args =

845− jsPackUBits32 (

811+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "|" lhs rhs

846− JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

847− )

848

812

849 | (LOr (ITFixed IT64)) <- op

813 | (LOr (ITFixed IT64)) <- op

850 , (lhs:rhs:_) <- args =

814 , (lhs:rhs:_) <- args =

851 jsMeth (translateReg lhs) "or" [translateReg rhs]

815 jsMeth (translateReg lhs) "or" [translateReg rhs]

852

816

853 | (LXOr (ITFixed IT8)) <- op

817 | (LXOr (ITFixed IT8)) <- op

854− , (lhs:rhs:_) <- args =

855− jsPackUBits8 (

818+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "^" lhs rhs

856− JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

857− )

858

819

859 | (LXOr (ITFixed IT16)) <- op

820 | (LXOr (ITFixed IT16)) <- op

860− , (lhs:rhs:_) <- args =

861− jsPackUBits16 (

821+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "^" lhs rhs

862− JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

863− )

864

822

865 | (LXOr (ITFixed IT32)) <- op

823 | (LXOr (ITFixed IT32)) <- op

866− , (lhs:rhs:_) <- args =

867− jsPackUBits32 (

824+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "^" lhs rhs

868− JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

869− )

870

825

871 | (LXOr (ITFixed IT64)) <- op

826 | (LXOr (ITFixed IT64)) <- op

872 , (lhs:rhs:_) <- args =

827 , (lhs:rhs:_) <- args =

873 jsMeth (translateReg lhs) "xor" [translateReg rhs]

828 jsMeth (translateReg lhs) "xor" [translateReg rhs]

874

829

875 | (LPlus (ATInt (ITFixed IT8))) <- op

830 | (LPlus (ATInt (ITFixed IT8))) <- op

876− , (lhs:rhs:_) <- args =

877− jsPackUBits8 (

831+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "+" lhs rhs

878− JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

879− )

880

832

881 | (LPlus (ATInt (ITFixed IT16))) <- op

833 | (LPlus (ATInt (ITFixed IT16))) <- op

882− , (lhs:rhs:_) <- args =

883− jsPackUBits16 (

834+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "+" lhs rhs

884− JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

885− )

886

835

887 | (LPlus (ATInt (ITFixed IT32))) <- op

836 | (LPlus (ATInt (ITFixed IT32))) <- op

888− , (lhs:rhs:_) <- args =

889− jsPackUBits32 (

837+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "+" lhs rhs

890− JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

891− )

892

838

893 | (LPlus (ATInt (ITFixed IT64))) <- op

839 | (LPlus (ATInt (ITFixed IT64))) <- op

894 , (lhs:rhs:_) <- args =

840 , (lhs:rhs:_) <- args =

@@ -897,22 +843,13 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

897 ]

843 ]

898

844

899 | (LMinus (ATInt (ITFixed IT8))) <- op

845 | (LMinus (ATInt (ITFixed IT8))) <- op

900− , (lhs:rhs:_) <- args =

901− jsPackUBits8 (

846+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "-" lhs rhs

902− JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

903− )

904

847

905 | (LMinus (ATInt (ITFixed IT16))) <- op

848 | (LMinus (ATInt (ITFixed IT16))) <- op

906− , (lhs:rhs:_) <- args =

907− jsPackUBits16 (

849+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "-" lhs rhs

908− JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

909− )

910

850

911 | (LMinus (ATInt (ITFixed IT32))) <- op

851 | (LMinus (ATInt (ITFixed IT32))) <- op

912− , (lhs:rhs:_) <- args =

913− jsPackUBits32 (

852+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "-" lhs rhs

914− JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

915− )

916

853

917 | (LMinus (ATInt (ITFixed IT64))) <- op

854 | (LMinus (ATInt (ITFixed IT64))) <- op

918 , (lhs:rhs:_) <- args =

855 , (lhs:rhs:_) <- args =

@@ -921,22 +858,13 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

921 ]

858 ]

922

859

923 | (LTimes (ATInt (ITFixed IT8))) <- op

860 | (LTimes (ATInt (ITFixed IT8))) <- op

924− , (lhs:rhs:_) <- args =

925− jsPackUBits8 (

861+ , (lhs:rhs:_) <- args = jsPackUBits8 $ bitsBinaryOp "*" lhs rhs

926− JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

927− )

928

862

929 | (LTimes (ATInt (ITFixed IT16))) <- op

863 | (LTimes (ATInt (ITFixed IT16))) <- op

930− , (lhs:rhs:_) <- args =

931− jsPackUBits16 (

864+ , (lhs:rhs:_) <- args = jsPackUBits16 $ bitsBinaryOp "*" lhs rhs

932− JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

933− )

934

865

935 | (LTimes (ATInt (ITFixed IT32))) <- op

866 | (LTimes (ATInt (ITFixed IT32))) <- op

936− , (lhs:rhs:_) <- args =

937− jsPackUBits32 (

867+ , (lhs:rhs:_) <- args = jsPackUBits32 $ bitsBinaryOp "*" lhs rhs

938− JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

939− )

940

868

941 | (LTimes (ATInt (ITFixed IT64))) <- op

869 | (LTimes (ATInt (ITFixed IT64))) <- op

942 , (lhs:rhs:_) <- args =

870 , (lhs:rhs:_) <- args =

@@ -945,110 +873,62 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

945 ]

873 ]

946

874

947 | (LEq (ATInt (ITFixed IT8))) <- op

875 | (LEq (ATInt (ITFixed IT8))) <- op

948− , (lhs:rhs:_) <- args =

876+ , (lhs:rhs:_) <- args = bitsCompareOp "==" lhs rhs

949− jsPackUBits8 (

950− JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

951− )

952

877

953 | (LEq (ATInt (ITFixed IT16))) <- op

878 | (LEq (ATInt (ITFixed IT16))) <- op

954− , (lhs:rhs:_) <- args =

879+ , (lhs:rhs:_) <- args = bitsCompareOp "==" lhs rhs

955− jsPackUBits16 (

956− JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

957− )

958

880

959 | (LEq (ATInt (ITFixed IT32))) <- op

881 | (LEq (ATInt (ITFixed IT32))) <- op

960− , (lhs:rhs:_) <- args =

882+ , (lhs:rhs:_) <- args = bitsCompareOp "==" lhs rhs

961− jsPackUBits32 (

962− JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

963− )

964

883

965 | (LEq (ATInt (ITFixed IT64))) <- op

884 | (LEq (ATInt (ITFixed IT64))) <- op

966− , (lhs:rhs:_) <- args =

885+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "equals" [rhs]

967− jsMeth (jsMeth (translateReg lhs) "equals" [translateReg rhs]) "and" [

968− jsBigInt (JSString $ show 0xFFFFFFFFFFFFFFFF)

969− ]

970

886

971 | (LLt (ITFixed IT8)) <- op

887 | (LLt (ITFixed IT8)) <- op

972− , (lhs:rhs:_) <- args =

888+ , (lhs:rhs:_) <- args = bitsCompareOp "<" lhs rhs

973− jsPackUBits8 (

974− JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

975− )

976

889

977 | (LLt (ITFixed IT16)) <- op

890 | (LLt (ITFixed IT16)) <- op

978− , (lhs:rhs:_) <- args =

891+ , (lhs:rhs:_) <- args = bitsCompareOp "<" lhs rhs

979− jsPackUBits16 (

980− JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

981− )

982

892

983 | (LLt (ITFixed IT32)) <- op

893 | (LLt (ITFixed IT32)) <- op

984− , (lhs:rhs:_) <- args =

894+ , (lhs:rhs:_) <- args = bitsCompareOp "<" lhs rhs

985− jsPackUBits32 (

986− JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

987− )

988

895

989 | (LLt (ITFixed IT64)) <- op

896 | (LLt (ITFixed IT64)) <- op

990− , (lhs:rhs:_) <- args = invokeMeth lhs "lesser" [rhs]

897+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "lesser" [rhs]

991

898

992 | (LLe (ITFixed IT8)) <- op

899 | (LLe (ITFixed IT8)) <- op

993− , (lhs:rhs:_) <- args =

900+ , (lhs:rhs:_) <- args = bitsCompareOp "<=" lhs rhs

994− jsPackUBits8 (

995− JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

996− )

997

901

998 | (LLe (ITFixed IT16)) <- op

902 | (LLe (ITFixed IT16)) <- op

999− , (lhs:rhs:_) <- args =

903+ , (lhs:rhs:_) <- args = bitsCompareOp "<=" lhs rhs

1000− jsPackUBits16 (

1001− JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1002− )

1003

904

1004 | (LLe (ITFixed IT32)) <- op

905 | (LLe (ITFixed IT32)) <- op

1005− , (lhs:rhs:_) <- args =

906+ , (lhs:rhs:_) <- args = bitsCompareOp "<=" lhs rhs

1006− jsPackUBits32 (

1007− JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1008− )

1009

907

1010 | (LLe (ITFixed IT64)) <- op

908 | (LLe (ITFixed IT64)) <- op

1011− , (lhs:rhs:_) <- args = invokeMeth lhs "lesserOrEquals" [rhs]

909+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "lesserOrEquals" [rhs]

1012

910

1013 | (LGt (ITFixed IT8)) <- op

911 | (LGt (ITFixed IT8)) <- op

1014− , (lhs:rhs:_) <- args =

912+ , (lhs:rhs:_) <- args = bitsCompareOp ">" lhs rhs

1015− jsPackUBits8 (

1016− JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1017− )

1018

913

1019 | (LGt (ITFixed IT16)) <- op

914 | (LGt (ITFixed IT16)) <- op

1020− , (lhs:rhs:_) <- args =

915+ , (lhs:rhs:_) <- args = bitsCompareOp ">" lhs rhs

1021− jsPackUBits16 (

1022− JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1023− )

1024 | (LGt (ITFixed IT32)) <- op

916 | (LGt (ITFixed IT32)) <- op

1025− , (lhs:rhs:_) <- args =

917+ , (lhs:rhs:_) <- args = bitsCompareOp ">" lhs rhs

1026− jsPackUBits32 (

1027− JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1028− )

1029

918

1030 | (LGt (ITFixed IT64)) <- op

919 | (LGt (ITFixed IT64)) <- op

1031− , (lhs:rhs:_) <- args = invokeMeth lhs "greater" [rhs]

920+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "greater" [rhs]

1032

921

1033 | (LGe (ITFixed IT8)) <- op

922 | (LGe (ITFixed IT8)) <- op

1034− , (lhs:rhs:_) <- args =

923+ , (lhs:rhs:_) <- args = bitsCompareOp ">=" lhs rhs

1035− jsPackUBits8 (

1036− JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1037− )

1038

924

1039 | (LGe (ITFixed IT16)) <- op

925 | (LGe (ITFixed IT16)) <- op

1040− , (lhs:rhs:_) <- args =

926+ , (lhs:rhs:_) <- args = bitsCompareOp ">=" lhs rhs

1041− jsPackUBits16 (

1042− JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1043− )

1044 | (LGe (ITFixed IT32)) <- op

927 | (LGe (ITFixed IT32)) <- op

1045− , (lhs:rhs:_) <- args =

928+ , (lhs:rhs:_) <- args = bitsCompareOp ">=" lhs rhs

1046− jsPackUBits32 (

1047− JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1048− )

1049

929

1050 | (LGe (ITFixed IT64)) <- op

930 | (LGe (ITFixed IT64)) <- op

1051− , (lhs:rhs:_) <- args = invokeMeth lhs "greaterOrEquals" [rhs]

931+ , (lhs:rhs:_) <- args = JSPreOp "+" $ invokeMeth lhs "greaterOrEquals" [rhs]

1052

932

1053 | (LUDiv (ITFixed IT8)) <- op

933 | (LUDiv (ITFixed IT8)) <- op

1054 , (lhs:rhs:_) <- args =

934 , (lhs:rhs:_) <- args =

@@ -1150,8 +1030,7 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1150 jsPackSBits32 $ JSPreOp "~" $ jsUnPackBits (translateReg arg)

1030 jsPackSBits32 $ JSPreOp "~" $ jsUnPackBits (translateReg arg)

1151

1031

1152 | (LCompl (ITFixed IT64)) <- op

1032 | (LCompl (ITFixed IT64)) <- op

1153− , (arg:_) <- args =

1154− invokeMeth arg "not" []

1033+ , (arg:_) <- args = invokeMeth arg "not" []

1155

1034

1156 | (LPlus _) <- op

1035 | (LPlus _) <- op

1157 , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs

1036 , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs

@@ -1164,15 +1043,15 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1164 | (LSRem _) <- op

1043 | (LSRem _) <- op

1165 , (lhs:rhs:_) <- args = translateBinaryOp "%" lhs rhs

1044 , (lhs:rhs:_) <- args = translateBinaryOp "%" lhs rhs

1166 | (LEq _) <- op

1045 | (LEq _) <- op

1167− , (lhs:rhs:_) <- args = translateBinaryOp "==" lhs rhs

1046+ , (lhs:rhs:_) <- args = translateCompareOp "==" lhs rhs

1168 | (LSLt _) <- op

1047 | (LSLt _) <- op

1169− , (lhs:rhs:_) <- args = translateBinaryOp "<" lhs rhs

1048+ , (lhs:rhs:_) <- args = translateCompareOp "<" lhs rhs

1170 | (LSLe _) <- op

1049 | (LSLe _) <- op

1171− , (lhs:rhs:_) <- args = translateBinaryOp "<=" lhs rhs

1050+ , (lhs:rhs:_) <- args = translateCompareOp "<=" lhs rhs

1172 | (LSGt _) <- op

1051 | (LSGt _) <- op

1173− , (lhs:rhs:_) <- args = translateBinaryOp ">" lhs rhs

1052+ , (lhs:rhs:_) <- args = translateCompareOp ">" lhs rhs

1174 | (LSGe _) <- op

1053 | (LSGe _) <- op

1175− , (lhs:rhs:_) <- args = translateBinaryOp ">=" lhs rhs

1054+ , (lhs:rhs:_) <- args = translateCompareOp ">=" lhs rhs

1176 | (LAnd _) <- op

1055 | (LAnd _) <- op

1177 , (lhs:rhs:_) <- args = translateBinaryOp "&" lhs rhs

1056 , (lhs:rhs:_) <- args = translateBinaryOp "&" lhs rhs

1178 | (LOr _) <- op

1057 | (LOr _) <- op

@@ -1189,9 +1068,9 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1189 | LStrConcat <- op

1068 | LStrConcat <- op

1190 , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs

1069 , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs

1191 | LStrEq <- op

1070 | LStrEq <- op

1192− , (lhs:rhs:_) <- args = translateBinaryOp "==" lhs rhs

1071+ , (lhs:rhs:_) <- args = translateCompareOp "==" lhs rhs

1193 | LStrLt <- op

1072 | LStrLt <- op

1194− , (lhs:rhs:_) <- args = translateBinaryOp "<" lhs rhs

1073+ , (lhs:rhs:_) <- args = translateCompareOp "<" lhs rhs

1195 | LStrLen <- op

1074 | LStrLen <- op

1196 , (arg:_) <- args = JSProj (translateReg arg) "length"

1075 , (arg:_) <- args = JSProj (translateReg arg) "length"

1197 | (LStrInt ITNative) <- op

1076 | (LStrInt ITNative) <- op

@@ -1269,13 +1148,25 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1269 , _ <- args = JSNull

1148 , _ <- args = JSNull

1270 | LExternal ex <- op

1149 | LExternal ex <- op

1271 , ex == sUN "prim__eqPtr"

1150 , ex == sUN "prim__eqPtr"

1272− , [lhs, rhs] <- args = JSBinOp "==" (translateReg lhs) (translateReg rhs)

1151+ , [lhs, rhs] <- args = translateCompareOp "==" lhs rhs

1273 | otherwise = JSError $ "Not implemented: " ++ show op

1152 | otherwise = JSError $ "Not implemented: " ++ show op

1274 where

1153 where

1275 translateBinaryOp :: String -> Reg -> Reg -> JS

1154 translateBinaryOp :: String -> Reg -> Reg -> JS

1276 translateBinaryOp op lhs rhs =

1155 translateBinaryOp op lhs rhs =

1277 JSBinOp op (translateReg lhs) (translateReg rhs)

1156 JSBinOp op (translateReg lhs) (translateReg rhs)

1278

1157

1158+ translateCompareOp :: String -> Reg -> Reg -> JS

1159+ translateCompareOp op lhs rhs =

1160+ JSPreOp "+" $ translateBinaryOp op lhs rhs

1161+

1162+ bitsBinaryOp :: String -> Reg -> Reg -> JS

1163+ bitsBinaryOp op lhs rhs =

1164+ JSBinOp op (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))

1165+

1166+ bitsCompareOp :: String -> Reg -> Reg -> JS

1167+ bitsCompareOp op lhs rhs =

1168+ JSPreOp "+" $ bitsBinaryOp op lhs rhs

1169+

1279 invokeMeth :: Reg -> String -> [Reg] -> JS

1170 invokeMeth :: Reg -> String -> [Reg] -> JS

1280 invokeMeth obj meth args =

1171 invokeMeth obj meth args =

1281 JSApp (JSProj (translateReg obj) meth) $ map translateReg args

1172 JSApp (JSProj (translateReg obj) meth) $ map translateReg args

src/IRTS/JavaScript/AST.hs+1−1

@@ -194,7 +194,7 @@ compileJS' indent (JSBinOp op lhs rhs) =

194 `T.append` compileJS' indent rhs

195

196compileJS' indent (JSPreOp op val) =

197− T.pack op `T.append` compileJS' indent val

197+ T.pack op `T.append` "(" `T.append` compileJS' indent val `T.append` ")"

198

199compileJS' indent (JSProj obj field)

200 | JSFunction {} <- obj =

test/primitives002/expected+13−13

@@ -1,15 +1,15 @@

1prim__floatToStr 0.0

2−"0.0"

2+"0"

3−prim__strToFloat "0.0"

3+prim__strToFloat 0.0

4−0.0

4+0

5prim__addFloat 1.0 1.0

6−2.0

6+2

7prim__subFloat 1.0 1.0

8−0.0

8+0

9prim__mulFloat 1.0 1.0

10−1.0

10+1

11prim__divFloat 1.0 1.0

12−1.0

12+1

13prim__slteFloat 1.0 1.0

141

15prim__sltFloat 1.0 1.0

@@ -21,13 +21,13 @@ prim__sgtFloat 1.0 1.0

21prim__eqFloat 1.0 1.0

221

23prim__floatACos 1.0

24−0.0

24+0

25prim__floatATan 1.0

260.78539816

27prim__floatCos 1.0

280.54030230

29prim__floatFloor 1.0

30−1.0

30+1

31prim__floatSin 1.0

320.84147098

33prim__floatTan 1.0

@@ -35,12 +35,12 @@ prim__floatTan 1.0

35prim__floatASin 1.0

361.57079632

37prim__floatCeil 1.0

38−1.0

38+1

39prim__floatExp 1.0

402.71828182

41prim__floatLog 1.0

42−0.0

42+0

43prim__floatSqrt 1.0

44−1.0

44+1

45prim__negFloat 1.0

46−-1.0

46+-1

test/primitives002/run+34−30

@@ -1,37 +1,41 @@

1#!/usr/bin/env bash

3−HEAD="module Main

3+HEAD='module Main

5import Data.Floats

7strtake : Nat -> String -> String

8strtake n str = pack (take n (unpack str))

10+getf : IO Double

11+getf = map cast getLine

12+

10−main : IO ()"

13+main : IO ()'

11−

14+

15+# code separated from input with '#'

12−TESTS=("prim__floatToStr 0.0"

16+TESTS=('prim__floatToStr !getf#0.0'

13−"prim__strToFloat \"0.0\""

17+ 'prim__strToFloat !getLine#0.0'

14−"prim__addFloat 1.0 1.0"

18+$'prim__addFloat !getf !getf#1.0\n1.0'

15−"prim__subFloat 1.0 1.0"

19+$'prim__subFloat !getf !getf#1.0\n1.0'

16−"prim__mulFloat 1.0 1.0"

20+$'prim__mulFloat !getf !getf#1.0\n1.0'

17−"prim__divFloat 1.0 1.0"

21+$'prim__divFloat !getf !getf#1.0\n1.0'

18−"prim__slteFloat 1.0 1.0"

22+$'prim__slteFloat !getf !getf#1.0\n1.0'

19−"prim__sltFloat 1.0 1.0"

23+$'prim__sltFloat !getf !getf#1.0\n1.0'

20−"prim__sgteFloat 1.0 1.0"

24+$'prim__sgteFloat !getf !getf#1.0\n1.0'

21−"prim__sgtFloat 1.0 1.0"

25+$'prim__sgtFloat !getf !getf#1.0\n1.0'

22−"prim__eqFloat 1.0 1.0"

26+$'prim__eqFloat !getf !getf#1.0\n1.0'

23−"prim__floatACos 1.0"

27+ 'prim__floatACos !getf#1.0'

24−"prim__floatATan 1.0"

28+ 'prim__floatATan !getf#1.0'

25−"prim__floatCos 1.0"

29+ 'prim__floatCos !getf#1.0'

26−"prim__floatFloor 1.0"

30+ 'prim__floatFloor !getf#1.0'

27−"prim__floatSin 1.0"

31+ 'prim__floatSin !getf#1.0'

28−"prim__floatTan 1.0"

32+ 'prim__floatTan !getf#1.0'

29−"prim__floatASin 1.0"

33+ 'prim__floatASin !getf#1.0'

30−"prim__floatCeil 1.0"

34+ 'prim__floatCeil !getf#1.0'

31−"prim__floatExp 1.0"

35+ 'prim__floatExp !getf#1.0'

32−"prim__floatLog 1.0"

36+ 'prim__floatLog !getf#1.0'

33−"prim__floatSqrt 1.0"

37+ 'prim__floatSqrt !getf#1.0'

34−"prim__negFloat 1.0"

38+ 'prim__negFloat !getf#1.0'

35)

39)

37generate_testfile()

41generate_testfile()

@@ -44,9 +48,9 @@ EOF

45for T in "${TESTS[@]}"

49for T in "${TESTS[@]}"

46do

50do

47− echo ${T}

51+ echo ${T%% *} ${T##*#}

48− generate_testfile "tmptest.idr" "${T}"

52+ generate_testfile "tmptest.idr" "${T%%#*}"

49− idris $@ --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}"

53+ idris "$@" --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}"

50− ./tmptest

54+ ./tmptest <<<"${T##*#}"

51 rm tmptest.idr tmptest.ibc tmptest

55 rm tmptest.idr tmptest.ibc tmptest

52done

56done

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))

1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))

2--------------

3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))

4--------------

5−App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))

5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))