Add Text/show, Text/replace, NaN

Only parsing for NaN, looks like doing anything useful with it will have
to wait for [this issue](idris-lang/Idris2#29)

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>

Idrall/Check.idr

@@ -7,6 +7,7 @@ import Idrall.Map
 
 import Data.List
 import Data.List1
+import Data.Strings
 
 -- alpha equivalence
 nestError : Either Error b -> Error -> Either Error b
@@ -219,6 +220,37 @@ mutual
          (t, VTextLit (MkVChunks [] "")) => pure t
          (VTextLit x, VTextLit y) => pure $ VTextLit (x <+> y)
          (t, u) => pure $ VTextAppend t u
+  eval env ETextShow =
+    pure $ VPrim $ \c =>
+      case c of
+           VTextLit (MkVChunks [] x) => pure $ VTextLit (MkVChunks [] (vTextShow x))
+           t => pure $ VTextShow t
+  eval env ETextReplace = -- Probably not right
+    pure $ VPrim $
+      \needle => pure $ VPrim $
+        \replacement => pure $ VPrim $
+          \haystack =>
+            case needle of
+                 VTextLit (MkVChunks [] "") => pure haystack
+                 VTextLit (MkVChunks [] needleText) =>
+                   case haystack of
+                        (VTextLit (MkVChunks [] haystackText)) =>
+                          case replacement of
+                               (VTextLit (MkVChunks [] replacementText)) =>
+                                 pure $ VTextLit $
+                                        MkVChunks [] $ textReplace needleText replacementText haystackText
+                               (VTextLit (MkVChunks chx replacementText)) =>
+                                 case strFromChunks chx  of
+                                      Nothing => Left $ ErrorMessage "could not make string for replacement"
+                                      (Just str) =>
+                                         pure $ VTextLit $
+                                         MkVChunks [] $ textReplace
+                                                          needleText
+                                                          replacementText
+                                                          haystackText
+                               _ => pure $ VTextReplace needle replacement haystack
+                        _ => pure $ VTextReplace needle replacement haystack
+                 k => pure $ VTextReplace needle replacement haystack
   eval env EList = do
     Right $ VPrim $ \a => Right $ VList a
   eval env (EListLit Nothing es) = do
@@ -385,6 +417,24 @@ mutual
   eval env (EEmbed (Raw x)) = absurd x
   eval env (EEmbed (Resolved x)) = eval Empty x
 
+  vTextShow : String -> String
+  vTextShow x = "\"" <+> (foldl (<+>) "" (map f (unpack x))) <+> "\""
+  where
+    f : Char -> String
+    f '"'  = "\\\""
+    f '$'  = "\\u0024"
+    f '\\' = "\\\\"
+    f '\b' = "\\b"
+    f '\n' = "\\n"
+    f '\r' = "\\r"
+    f '\t' = "\\t"
+    f '\f' = "\\f"
+    -- TODO handle this case
+    -- https://github.com/dhall-lang/dhall-haskell/blob/f33e8cff8fc51e4a562f48fcf987e6af5e09142d/dhall/src/Dhall/Eval.hs#L847
+    f c = case c <= '\x1F' of
+               True => singleton c
+               False => singleton c
+
   vToMap : (FieldName, Value) -> Value
   vToMap (MkFieldName k, v) = VRecordLit $ fromList
     [ (MkFieldName "mapKey", VTextLit $ MkVChunks [] k)
@@ -654,6 +704,12 @@ mutual
   conv env (VTextAppend t u) (VTextAppend t' u') = do
     conv env t t'
     conv env u u'
+  conv env (VTextShow t) (VTextShow t') = do
+    conv env t t'
+  conv env (VTextReplace t u v) (VTextReplace t' u' v') = do
+    conv env t t'
+    conv env u u'
+    conv env v v'
   conv env (VList a) (VList a') = conv env a a'
   conv env (VListLit _ xs) (VListLit _ xs') = convList env xs xs'
   conv env (VListAppend t u) (VListAppend t' u') = do
@@ -808,6 +864,8 @@ mutual
     let chx = traverse (mapChunks (quote env)) xs in
     Right $ ETextLit (MkChunks !chx x)
   quote env (VTextAppend t u) = pure $ ETextAppend !(quote env t) !(quote env u)
+  quote env (VTextShow t) = qApp env ETextShow t
+  quote env (VTextReplace t u v) = qAppM env ETextReplace [t, u, v]
   quote env (VList x) = qApp env EList x
   quote env (VListLit Nothing ys) =
     let ys' = traverse (quote env) ys in
@@ -1059,6 +1117,14 @@ mutual
     check cxt t VText
     check cxt u VText
     pure $ (ETextAppend t u, VText)
+  infer cxt ETextShow = pure $ (EIntegerShow, (vFun VText VText))
+    -- pure (EListBuild, VHPi "a" vType $ \a => pure $ vFun (listFoldTy a) (VList a))
+  infer cxt ETextReplace =
+    pure ( ETextReplace,
+           VHPi "needle" VText $ \needle =>
+           pure $ VHPi "replacement" VText $ \replacement =>
+           pure $ VHPi "haystack" VText $ \haystack =>
+           pure VText)
   infer cxt EList = do
     Right $ (EList, VHPi "a" vType $ \a => Right $ vType)
   infer cxt (EListLit Nothing []) = do

Idrall/Expr.idr

@@ -139,6 +139,10 @@ mutual
     | ETextLit (Chunks a)
     -- | > ETextAppend x y ~ x ++ y
     | ETextAppend (Expr a) (Expr a)
+    -- | > ETextShow ~ Text/show
+    | ETextShow
+    -- | > ETextReplace ~ Text/replace
+    | ETextReplace
     -- | > EList a ~ List a
     | EList
     -- | > EList (Some e) [e', ...] ~ [] : List a
@@ -251,6 +255,8 @@ mutual
     show EText = "EText"
     show (ETextLit x) = "(ETextLit " ++ show x ++ ")"
     show (ETextAppend x y) = "(ETextAppend " ++ show x ++ " " ++ show y ++ ")"
+    show ETextShow = "ETextShow"
+    show ETextReplace = "ETextReplace"
     show EList = "EList"
     show (EListLit Nothing xs) = "(EListLit Nothing " ++ show xs ++ ")"
     show (EListLit (Just x) xs) = "(EListLit (Just " ++ show x ++ ") " ++ show xs ++ ")"

Idrall/Map.idr

@@ -8,6 +8,8 @@ import Idrall.Value
 
 import Data.List
 
+import Debug.Trace
+
 export
 isOdd : Nat -> Bool
 isOdd Z = False
@@ -60,3 +62,23 @@ mergeWithApp' : (Monad m, Ord k) =>
                SortedMap k a ->
                m (SortedMap k a)
 mergeWithApp' f xs ys = sequence (mergeWith (\x,y => y) (map pure xs) (map pure ys))
+
+replace : Eq a => (needle : List a) -> (replacement : List a) -> (haystack : List a) -> List a
+replace needle replacement haystack = go 0 [] needle haystack
+  where
+    go : (pass : Nat) ->
+         (acc : List a) ->
+         (needle : List a) ->
+         (haystack : List a) -> List a
+    go _ acc (x :: xs) [] = acc -- End of list
+    go _ acc [] haystack = haystack -- Empty needle
+    go (S k) acc needle (y :: haystack) = -- Pass through to remove matched elements
+      go k acc needle haystack
+    go Z acc needle@(x :: xs) h@(y :: haystack) =
+      case isPrefixOf needle h of
+           False => go 0 (acc ++ [y]) needle haystack
+           True => go (length xs) (acc ++ replacement) needle haystack
+
+export
+textReplace : (needle : String) -> (replacement : String) -> (haystack : String) -> String
+textReplace needle replacement haystack = pack $ replace (unpack needle) (unpack replacement) (unpack haystack)

Idrall/Parser.idr

@@ -39,8 +39,11 @@ builtin =
   (string "List/indexed" *> pure EListIndexed) <|>
   (string "List/reverse" *> pure EListReverse) <|>
   (string "List" *> pure EList) <|>
+  (string "Text/show" *> pure ETextShow) <|>
+  (string "Text/replace" *> pure ETextReplace) <|>
   (string "None" *> pure ENone) <|>
-  (string "Optional" *> pure EOptional)
+  (string "Optional" *> pure EOptional) <|>
+  (string "NaN" *> pure (EDoubleLit (0.0/0.0)))
 
 true : Parser (Expr ImportStatement)
 true = token "True" *> pure (EBoolLit True)

Idrall/Resolve.idr

@@ -167,6 +167,8 @@ mutual
     x' <- resolve h p x
     y' <- resolve h p y
     pure (ETextAppend x' y')
+  resolve h p ETextShow = pure ETextShow
+  resolve h p ETextReplace = pure ETextReplace
   resolve h p EOptional = pure EOptional
   resolve h p ENone = pure ENone
   resolve h p (ESome x) = do

Idrall/Value.idr

@@ -57,6 +57,8 @@ mutual
     | VText
     | VTextLit VChunks
     | VTextAppend Value Value
+    | VTextShow Value
+    | VTextReplace Value Value Value
 
     | VList Ty
     | VListLit (Maybe Ty) (List Value)
@@ -191,7 +193,9 @@ mutual
 
     show (VText) = "VText"
     show (VTextLit x) = "(VTextLit " ++ show x ++ ")"
-    show (VTextAppend x y) = "(VTextLit " ++ show x ++ " " ++ show y ++ ")"
+    show (VTextAppend x y) = "(VTextAppend " ++ show x ++ " " ++ show y ++ ")"
+    show (VTextShow x) = "(VTextShow " ++ show x ++ ")"
+    show (VTextReplace x y z) = "(VTextReplace " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 
     show (VList a) = "(VList " ++ show a ++ ")"
     show (VListLit ty vs) = "(VListLit " ++ show ty ++ show vs ++ ")"