Renamed IsString to FromString

- Renaming of the string overload interface
- Added test cases for both string and integer literals overload

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.

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

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",

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

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

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!

tests/idris2/basic042/input

@@ -0,0 +1,6 @@
+test1
+test2
+the Bool "True"
+the Bool "False"
+the Bool "42"
+:q

tests/idris2/basic042/input2

@@ -0,0 +1,6 @@
+test1
+test2
+test3
+the (Fin 3) 2
+the (Fin 3) 6
+:q

tests/idris2/basic042/run

@@ -0,0 +1,4 @@
+$1 --no-banner LiteralsString.idr < input
+$1 --no-banner LiteralsInteger.idr < input2
+
+rm -rf build