From 546265f2e62a290fe8fa0f8923a58fb081999d61 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 1 Dec 2023 12:55:11 -0800
Subject: [PATCH] Add string literals to the term language

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Latex.elm  |  2 +-
 src/Bergamot/Parser.elm | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm
index fd8cba7..061f809 100644
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@@ -24,7 +24,7 @@ termToLatex f t =
         Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
         Var x -> f x
         IntLit i -> String.fromInt i
-        StringLit s -> "\"" ++ s ++ "\""
+        StringLit s -> "\\text{" ++ "``" ++ s ++ "''" ++ "}"
 
 metavariableToLatex : Metavariable -> String
 metavariableToLatex (MkMetavariable s) =
diff --git a/src/Bergamot/Parser.elm b/src/Bergamot/Parser.elm
index 81d8f3f..7630dbc 100644
--- a/src/Bergamot/Parser.elm
+++ b/src/Bergamot/Parser.elm
@@ -9,6 +9,42 @@ import Set
 intLit : Parser Int
 intLit = Parser.int
 
+decodeStr : String -> String
+decodeStr str =
+    let
+        go l =
+            case l of
+                '\\' :: 'n' :: rest -> '\n' :: go rest
+                '\\' :: '\\' :: rest -> '\\' :: go rest
+                '\\' :: '"' :: 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
+        char = Parser.map decodeStr <| Parser.getChompedString <|
+            Parser.oneOf
+                [ Parser.backtrackable <|
+                    Parser.chompIf (\c -> c == '\\')
+                    |. Parser.chompIf (\c -> True)
+                , Parser.backtrackable <| Parser.chompIf (\c -> c /= '"')
+                ]
+    in
+        Parser.map (String.join "") <| Parser.sequence
+            { start = "\""
+            , separator = ""
+            , end = "\""
+            , spaces = Parser.succeed ()
+            , item = char
+            , trailing = Optional
+            }
+
+
 name : Parser String
 name = Parser.variable
     { start = \c -> Char.isAlphaNum c || c == '_'
@@ -44,6 +80,7 @@ term = Parser.lazy (\() -> Parser.oneOf
     , Parser.backtrackable <|
       Parser.succeed Var |= variable
     , Parser.succeed IntLit |= intLit
+    , Parser.succeed StringLit |= strLit
     ])
 
 rule : Parser Rule