Stringify string literals on Rust side

Cargo.lock

@@ -176,7 +176,7 @@ dependencies = [
 
 [[package]]
 name = "kind2"
-version = "0.2.59"
+version = "0.2.62"
 dependencies = [
  "clap",
  "highlight_error",

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "kind2"
-version = "0.2.62"
+version = "0.2.63"
 edition = "2021"
 description = "A pure functional functional language that uses the HVM."
 repository = "https://github.com/Kindelia/Kind2"

src/language.rs

@@ -1885,7 +1885,30 @@ pub fn compile_book(book: &Book) -> String {
 // Stringification
 // ===============
 
+pub fn interpret_as_string(term: &Term) -> Option<String> {
+  let mut text = String::new();
+  let mut term = term;
+  loop {
+    if let Term::Ctr { name, args, .. } = term {
+      if name == "String.cons" && args.len() == 2 {
+        if let Term::Num { numb, .. } = *args[0] {
+          text.push(char::from_u32(numb as u32).unwrap_or('\0'));
+          term = &*args[1];
+        }
+        continue;
+      }
+      if name == "String.nil" && args.len() == 0 {
+        return Some(text);
+      }
+    }
+    return None;
+  }
+}
+
 pub fn show_term(term: &Term) -> String {
+  if let Some(as_string) = interpret_as_string(term) {
+    return format!("\"{}\"", as_string);
+  }
   match term {
     Term::Typ { .. } => {
       format!("Type")

src/to_hvm.rs

@@ -4,6 +4,9 @@
 use crate::language::{*};
 
 pub fn to_hvm_term(book: &Book, term: &Term) -> String {
+  if let Some(as_string) = interpret_as_string(term) {
+    return format!("\"{}\"", as_string);
+  }
   match term {
     Term::Typ { .. } => {
       format!("Type")