From c28133b7d928c9d2b37077d66ea288697c9392eb Mon Sep 17 00:00:00 2001 From: Giuseppe Lomurno Date: Wed, 5 Aug 2020 01:38:57 +0200 Subject: [PATCH] Renamed IsString to FromString - Renaming of the string overload interface - Added test cases for both string and integer literals overload --- .../Text/PrettyPrint/Prettyprinter/Doc.idr | 2 +- libs/prelude/Builtin.idr | 6 ++-- tests/Main.idr | 2 +- tests/idris2/basic042/LiteralsInteger.idr | 31 +++++++++++++++++++ tests/idris2/basic042/LiteralsString.idr | 21 +++++++++++++ tests/idris2/basic042/expected | 20 ++++++++++++ tests/idris2/basic042/input | 6 ++++ tests/idris2/basic042/input2 | 6 ++++ tests/idris2/basic042/run | 4 +++ 9 files changed, 93 insertions(+), 5 deletions(-) create mode 100644 tests/idris2/basic042/LiteralsInteger.idr create mode 100644 tests/idris2/basic042/LiteralsString.idr create mode 100644 tests/idris2/basic042/expected create mode 100644 tests/idris2/basic042/input create mode 100644 tests/idris2/basic042/input2 create mode 100755 tests/idris2/basic042/run diff --git a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr index dd82e918f..3da2a26e2 100644 --- a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr +++ b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr @@ -361,7 +361,7 @@ Pretty String where pretty = vsep . map unsafeTextWithoutNewLines . lines public export -IsString (Doc ann) where +FromString (Doc ann) where fromString = pretty ||| Variant of `encloseSep` with braces and comma as separator. diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index 57e0c6023..f4bf0a32a 100644 --- a/libs/prelude/Builtin.idr +++ b/libs/prelude/Builtin.idr @@ -188,7 +188,7 @@ force x = Force x ||| Interface for types that can be constructed from string literals. public export -interface IsString ty where +interface FromString ty where ||| Conversion from String. fromString : String -> ty @@ -196,11 +196,11 @@ interface IsString ty where %inline public export -IsString String where +FromString String where fromString s = s %defaulthint %inline public export -defaultString : IsString String +defaultString : FromString String defaultString = %search diff --git a/tests/Main.idr b/tests/Main.idr index f54c0196d..1426d8de5 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -41,7 +41,7 @@ idrisTests "basic026", "basic027", "basic028", "basic029", "basic030", "basic031", "basic032", "basic033", "basic034", "basic035", "basic036", "basic037", "basic038", "basic039", "basic040", - "basic041", + "basic041", "basic042", -- Coverage checking "coverage001", "coverage002", "coverage003", "coverage004", "coverage005", "coverage006", "coverage007", "coverage008", diff --git a/tests/idris2/basic042/LiteralsInteger.idr b/tests/idris2/basic042/LiteralsInteger.idr new file mode 100644 index 000000000..50f18f041 --- /dev/null +++ b/tests/idris2/basic042/LiteralsInteger.idr @@ -0,0 +1,31 @@ +import Data.Fin + +%default total + +data ZeroOneOmega = Zero | One | Omega + +Num ZeroOneOmega where + Zero + a = a + a + Zero = a + One + a = Omega + a + One = Omega + Omega + Omega = Omega + + Zero * _ = Zero + _ * Zero = Zero + One * a = a + a * One = a + Omega * Omega = Omega + + fromInteger 0 = Zero + fromInteger 1 = One + fromInteger _ = Omega + +test1 : ZeroOneOmega +test1 = 0 + +test2 : ZeroOneOmega +test2 = 1 + +test3 : ZeroOneOmega +test3 = 8 diff --git a/tests/idris2/basic042/LiteralsString.idr b/tests/idris2/basic042/LiteralsString.idr new file mode 100644 index 000000000..2c3b21bd7 --- /dev/null +++ b/tests/idris2/basic042/LiteralsString.idr @@ -0,0 +1,21 @@ +import Data.Maybe + +%default total + +FromString Int where + fromString x = cast x + +test1 : Int +test1 = "42" + +test2 : Int +test2 = "abc" + +convert : String -> Maybe Bool +convert "True" = Just True +convert "False" = Just False +convert _ = Nothing + +fromString : (str : String) -> {auto prf : IsJust (convert str)} -> Bool +fromString str {prf} with (convert str) + fromString str {prf = ItIsJust} | (Just ret) = ret diff --git a/tests/idris2/basic042/expected b/tests/idris2/basic042/expected new file mode 100644 index 000000000..a7600ca29 --- /dev/null +++ b/tests/idris2/basic042/expected @@ -0,0 +1,20 @@ +1/1: Building LiteralsString (LiteralsString.idr) +Main> 42 +Main> 0 +Main> True +Main> False +Main> (interactive):1:10--1:14:Can't find an implementation for IsJust Nothing at: +1 the Bool "42" + ^^^^ + +Main> Bye for now! +1/1: Building LiteralsInteger (LiteralsInteger.idr) +Main> Zero +Main> One +Main> Omega +Main> FS (FS FZ) +Main> (interactive):1:13--1:14:Can't find an implementation for IsJust (integerToFin 6 3) at: +1 the (Fin 3) 6 + ^ + +Main> Bye for now! diff --git a/tests/idris2/basic042/input b/tests/idris2/basic042/input new file mode 100644 index 000000000..d65813f2c --- /dev/null +++ b/tests/idris2/basic042/input @@ -0,0 +1,6 @@ +test1 +test2 +the Bool "True" +the Bool "False" +the Bool "42" +:q diff --git a/tests/idris2/basic042/input2 b/tests/idris2/basic042/input2 new file mode 100644 index 000000000..beb0cdc3e --- /dev/null +++ b/tests/idris2/basic042/input2 @@ -0,0 +1,6 @@ +test1 +test2 +test3 +the (Fin 3) 2 +the (Fin 3) 6 +:q diff --git a/tests/idris2/basic042/run b/tests/idris2/basic042/run new file mode 100755 index 000000000..c54efe946 --- /dev/null +++ b/tests/idris2/basic042/run @@ -0,0 +1,4 @@ +$1 --no-banner LiteralsString.idr < input +$1 --no-banner LiteralsInteger.idr < input2 + +rm -rf build