Merge pull request #508 from ShinKage/string-overload

Overloaded strings interface

docs/source/reference/index.rst

@@ -20,3 +20,4 @@ This is a placeholder, to get set up with readthedocs.
    envvars
    postfixprojs
    literate
+   overloadedlit

docs/source/reference/overloadedlit.rst

@@ -0,0 +1,47 @@
+Overloaded literals
+===================
+
+.. role:: idris(code)
+    :language: idris
+
+The compiler provides directives for literals overloading, respectively
+``%stringLit <fun>`` and ``%integerLit <fun>`` for string and integer literals. During
+elaboration, the given function is applied to the corresponding literal.
+In the Prelude these functions are set to ``fromString`` and ``fromInteger``.
+
+The interface ``FromString ty`` provides the ``fromString : String -> ty`` function,
+while the ``Num ty`` interface provides the ``fromInteger : Integer -> ty`` function
+for all numerical types.
+
+Restricted overloads
+--------------------
+Although the overloading of literals can be achieved by implementing the interfaces
+described above, in principle only a function with the correct signature and name
+is enough to achieve the desired behaviour. This can be exploited to obtain more
+restrictive overloading such as converting literals to ``Fin n`` values, where
+integer literals greater or equal to n are not constructible values for the type.
+Additional implicit arguments can be added to the function signature, in particular
+auto implicit arguments for searching proofs. As an example, this is the implementation
+of ``fromInteger`` for ``Fin n``.
+
+.. code-block:: idris
+
+    public export
+    fromInteger : (x : Integer) -> {n : Nat} ->
+                  {auto prf : (IsJust (integerToFin x n))} ->
+                  Fin n
+    fromInteger {n} x {prf} with (integerToFin x n)
+    fromInteger {n} x {prf = ItIsJust} | Just y = y
+
+The ``prf`` auto implicit is an automatically constructed proof (if possible) that
+the literal is suitable for the ``Fin n`` type. The restricted behaviour can be
+observed in the REPL, where the failure to construct a valid proof is caught during
+the type-checking phase and not at runtime:
+
+.. code-block:: idris
+
+    Main> the (Fin 3) 2
+    FS (FS FZ)
+    Main> the (Fin 3) 5
+    (interactive):1:13--1:14:Can't find an implementation for IsJust (integerToFin 5 3) at:
+    1	the (Fin 3) 5

libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -360,6 +360,10 @@ export
 Pretty String where
   pretty = vsep . map unsafeTextWithoutNewLines . lines
 
+public export
+FromString (Doc ann) where
+  fromString = pretty
+
 ||| Variant of `encloseSep` with braces and comma as separator.
 export
 list : List (Doc ann) -> Doc ann

libs/prelude/Builtin.idr

@@ -183,3 +183,24 @@ delay x = Delay x
 public export
 force : Lazy a -> a
 force x = Force x
+
+%stringLit fromString
+
+||| Interface for types that can be constructed from string literals.
+public export
+interface FromString ty where
+  ||| Conversion from String.
+  fromString : String -> ty
+
+%allow_overloads fromString
+
+%inline
+public export
+FromString String where
+  fromString s = s
+
+%defaulthint
+%inline
+public export
+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/ideMode/ideMode001/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:240} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:241}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:240}_[] ?{_:241}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:242}_[] ?{_:241}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:231}_[] ?{_:230}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:240} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:241}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:240}_[] ?{_:241}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:242}_[] ?{_:241}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:231}_[] ?{_:230}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

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