sanitise string/char outputs

C0deine/Ast/Ast.lean

@@ -6,6 +6,7 @@
    - Thea Brick
  -/
 import Numbers
+import C0deine.AuxDefs
 import C0deine.Context.Symbol
 import C0deine.Utils.Comparison
 
@@ -202,8 +203,8 @@ instance : ToString AsnOp where toString := AsnOp.toString
 mutual
 partial def Expr.toString : Expr → String
   | num v => s!"{v}"
-  | char c => s!"'{c}'"
-  | str s => s!"\"{s}\""
+  | char c => s!"'{c.toString.sanitise}'"
+  | str s => s!"\"{s.sanitise}\""
   | «true» => "true"
   | «false» => "false"
   | null => "NULL"

C0deine/AuxDefs.lean

@@ -61,6 +61,22 @@ def String.toInt32! (s : String) : Int32 :=
   | some v => v
   | none   => panic "Int32 expected"
 
+def String.sanitise (s : String) : String :=
+  s.foldl (fun acc c =>
+    if c.toNat = 0 then acc ++ "\\0"
+    else if c = '\n' then acc ++ "\\n"
+    else if c = '\t' then acc ++ "\\t"
+    else if c.toNat = 0x0B then acc ++ "\\v"
+    else if c.toNat = 0x08 then acc ++ "\\b"
+    else if c = '\r' then acc ++ "\\r"
+    else if c.toNat = 0x0C then acc ++ "\\f"
+    else if c.toNat = 0x07 then acc ++ "\\a"
+    else if c = '\\' then acc ++ "\\\\"
+    else if c = '\'' then acc ++ "\\'"
+    else if c = '"' then acc ++ "\\\""
+    else acc ++ c.toString
+  ) ""
+
 def UInt64.max (n m : UInt64) : UInt64 :=
   if n > m then n else m
 

C0deine/Parser/Cst.lean

@@ -5,6 +5,7 @@
    - Thea Brick
  -/
 import Numbers
+import C0deine.AuxDefs
 import C0deine.Context.Symbol
 
 namespace C0deine.Cst
@@ -256,8 +257,8 @@ instance : ToString PostOp where toString := PostOp.toString
 mutual
 partial def Expr.toString : Expr → String
   | .num v  => s!"{v}"
-  | .char c => s!"'{c}'"
-  | .str s  => s!"\"{s}\""
+  | .char c => s!"'{c.toString.sanitise}'"
+  | .str s  => s!"\"{s.sanitise}\""
   | .true   => "true"
   | .false  => "false"
   | .null   => "NULL"

C0deine/Type/Tst.lean

@@ -1048,8 +1048,8 @@ instance : ToString BinOp where toString := BinOp.toString
 
 def Expr.toString : Expr Δ Γ τ → String
   | .num v       => s!"({v} : {τ})"
-  | .char c      => s!"('{c}' : {τ})"
-  | .str s       => s!"(\"{s}\" : {τ})"
+  | .char c      => s!"('{c.toString.sanitise}' : {τ})"
+  | .str s       => s!"(\"{s.sanitise}\" : {τ})"
   | .«true»      => s!"(true : {τ})"
   | .«false»     => s!"(false : {τ})"
   | .null        => s!"(NULL : {τ})"
@@ -1171,7 +1171,7 @@ instance : ToString Prog where
     let calls_str  := prog.calls.toList.map (fun (f, pure) =>
         if pure then s!"{f} (pure)" else s!"{f}")
       |> String.intercalate "\n  "
-    let string_str := prog.strings.map (·.replace "\n" "\n    ")
+    let string_str := prog.strings.map (·.sanitise)
       |> String.intercalate "\n  - "
     let prog_str := prog.header.toStrings ++ prog.body.toStrings
       |> "\n\n".intercalate