Extract common utility functions and convert symbols to strings

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Latex.elm

@@ -2,29 +2,7 @@ module Bergamot.Latex exposing (..)
 
 import Bergamot.Syntax exposing (..)
 import Bergamot.Rules exposing (..)
-
-encodeStr : String -> String
-encodeStr s =
-    let
-        go l =
-            case l of
-                '\\' :: xs -> '\\' :: go xs
-                '"' :: xs -> '\\' :: '"' :: go xs
-                x :: xs -> x :: go xs
-                [] -> []
-    in
-        String.fromList (go (String.toList s))
-
-encodeLatex : String -> String
-encodeLatex s =
-    let
-        go l =
-            case l of
-                '\\' :: xs -> String.toList "\\textbackslash " ++ go xs
-                x :: xs -> x :: go xs
-                [] -> []
-    in
-        String.fromList (go (String.toList s))
+import Bergamot.Utils exposing (..)
 
 termToLatex : (a -> String) -> Term a -> String
 termToLatex f t =

src/Bergamot/Parser.elm

@@ -2,6 +2,7 @@ module Bergamot.Parser exposing (..)
 
 import Bergamot.Syntax exposing (Term(..), Metavariable(..))
 import Bergamot.Rules exposing (Rule, RuleEnv)
+import Bergamot.Utils exposing (decodeStr)
 
 import Parser exposing (Parser, Trailing(..), (|.), (|=))
 import Set
@@ -9,19 +10,6 @@ import Set
 intLit : Parser Int
 intLit = Parser.int
 
-decodeStr : String -> String
-decodeStr str =
-    let
-        go l =
-            case l of
-                '\\' :: '"' :: rest -> '"' :: go rest
-                '\\' :: c :: rest -> c :: go rest
-                c :: rest -> c :: go rest
-                [] -> []
-        noQuotes = String.dropLeft 1 <| String.dropRight 1 <| str
-    in
-        String.fromList (go (String.toList str))
-
 strLit : Parser String
 strLit =
     let

src/Bergamot/Rules.elm

@@ -2,6 +2,7 @@ module Bergamot.Rules exposing (..)
 
 import Bergamot.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
 import Bergamot.Search as Search exposing (Search)
+import Bergamot.Utils exposing (encodeStr)
 
 import Debug
 
@@ -137,6 +138,9 @@ builtinRules t =
         Call "tostring" [IntLit i, Var output] ->
             liftUnification unify (Var output) (StringLit (String.fromInt i))
             |> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
+        Call "tostring" [Call s [], Var output] ->
+            liftUnification unify (Var output) (StringLit <| encodeStr s)
+            |> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
         _ -> fail
 
 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)

src/Bergamot/Utils.elm

@@ -0,0 +1,38 @@
+module Bergamot.Utils exposing (..)
+
+decodeStr : String -> String
+decodeStr str =
+    let
+        go l =
+            case l of
+                '\\' :: '"' :: rest -> '"' :: go rest
+                '\\' :: c :: rest -> c :: go rest
+                c :: rest -> c :: go rest
+                [] -> []
+        noQuotes = String.dropLeft 1 <| String.dropRight 1 <| str
+    in
+        String.fromList (go (String.toList str))
+
+encodeStr : String -> String
+encodeStr s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> '\\' :: go xs
+                '"' :: xs -> '\\' :: '"' :: go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        String.fromList (go (String.toList s))
+
+encodeLatex : String -> String
+encodeLatex s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> String.toList "\\textbackslash " ++ go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        String.fromList (go (String.toList s))
+