Improve readback of unaplied or invalid strings

src/term/net_to_term.rs

@@ -1,4 +1,8 @@
-use super::{term_to_net::Labels, var_id_to_name, Book, DefId, MatchNum, Name, Op, Tag, Term, Val};
+use super::{
+  term_to_net::Labels,
+  transform::encode_strs::{SCONS, SNIL},
+  var_id_to_name, Book, DefId, MatchNum, Name, Op, Tag, Term, Val,
+};
 use crate::{
   net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
   term::Pattern,
@@ -269,20 +273,34 @@ impl<'a> Reader<'a> {
 
 impl<'a> Reader<'a> {
   fn resugar_string(&mut self, term: &mut Term) -> Term {
-    let mut s = String::new();
-    fn go(t: &mut Term, s: &mut String, rd: &mut Reader<'_>) {
-      match t {
-        Term::Lam { bod, .. } => go(bod, s, rd),
+    fn go(term: &mut Term, str_term: &mut Term, rd: &mut Reader<'_>) {
+      match term {
+        Term::Lam { bod, .. } => go(bod, str_term, rd),
         Term::App { tag, arg, .. } if *tag == Tag::string_scons_head() => {
-          if let Term::Num { val } = &**arg {
-            s.push(unsafe { char::from_u32_unchecked(*val as u32) });
-          } else {
-            rd.error(ReadbackError::InvalidStrTerm)
+          match arg.as_mut() {
+            Term::Num { val } => {
+              let num = *val;
+              match str_term {
+                Term::Str { ref mut val } => {
+                  val.push(unsafe { char::from_u32_unchecked(num as u32) });
+                },
+                app @ Term::App { .. } => {
+                  insert_string_cons(app, Term::Num { val: num });
+                },
+                _ => unreachable!(),
+              };
+            }
+            Term::Lam { tag, bod, .. } if *tag == Tag::string() => {
+              recover_constructors(str_term, rd.resugar_string(bod));
+              rd.error(ReadbackError::InvalidStrTerm)
+            },
+            Term::Var { nam } => recover_constructors(str_term, Term::Var { nam: nam.clone() }),
+            _ => rd.error(ReadbackError::InvalidStrTerm),
           }
         }
         Term::App { fun, arg, .. } => {
-          go(fun, s, rd);
-          go(arg, s, rd);
+          go(fun, str_term, rd);
+          go(arg, str_term, rd);
         }
         Term::Var { .. } => {}
         Term::Chn { .. }
@@ -300,8 +318,9 @@ impl<'a> Reader<'a> {
         | Term::Era => rd.error(ReadbackError::InvalidStrTerm),
       }
     }
-    go(term, &mut s, self);
-    Term::Str { val: s }
+    let mut str = Term::Str { val: String::new() };
+    go(term, &mut str, self);
+    str
   }
 
   fn resugar_list(&mut self, term: &mut Term) -> Term {
@@ -333,6 +352,51 @@ impl<'a> Reader<'a> {
   }
 }
 
+/// Recover string constructors when it is not possible to correctly readback a string
+fn recover_constructors(term: &mut Term, cons_term: Term) {
+  match term {
+    Term::Str { val } => {
+      let snil = Term::Var { nam: Name::new(SNIL) };
+      let last_term = string_cons(cons_term, snil);
+      *term = string_app(val, last_term)
+    }
+    app @ Term::App { .. } => insert_string_cons(app, cons_term),
+    _ => unreachable!(),
+  }
+}
+
+// TODO: `λa (SCons a (SCons 'b' (SCons 'c' SNil)))` could be read back as `λa (SCons a "bc")`
+// but the order in witch decode_str is run complicates this as the `SNil` could be another variable.
+// If decode_str is changed to the reverse order,
+// the hability to just push new chars to the string would be lost,
+// but the readback could be improved.
+//
+/// Inserts a term as an application with the last argument of an app chain
+fn insert_string_cons(app: &mut Term, term: Term) {
+  match app {
+    Term::App { arg, .. } => insert_string_cons(arg, term),
+    app => *app = string_cons(term, std::mem::take(app)),
+  }
+}
+
+/// If the string is empty, returns the arg
+/// Otherwise, converts to a `(SCONS str_term arg)` application
+fn string_app(val: &str, arg: Term) -> Term {
+  let str_term = match val.len() {
+    0 => return arg,
+    1 => Term::Num { val: val.chars().nth(0).unwrap().try_into().unwrap() },
+    _ => Term::Str { val: val.to_owned() },
+  };
+
+  string_cons(str_term, arg)
+}
+
+fn string_cons(term: Term, arg: Term) -> Term {
+  let svar = Term::Var { nam: Name::new(SCONS) };
+  let cons = Term::App { tag: Tag::Auto, fun: Box::new(svar), arg: Box::new(term) };
+  Term::App { tag: Tag::Auto, fun: Box::new(cons), arg: Box::new(arg) }
+}
+
 /// Represents `let (fst, snd) = val` if `tag` is `None`, and `dup#tag fst snd = val` otherwise.
 #[derive(Default)]
 struct Split {

src/term/transform/encode_strs.rs

@@ -3,11 +3,11 @@ use indexmap::IndexMap;
 
 use crate::term::{Adt, Book, Name, Tag, Term};
 
-const STRING: &str = "String";
-const SNIL: &str = "SNil";
-const SCONS: &str = "SCons";
-const HEAD: &str = "head";
-const TAIL: &str = "tail";
+pub const STRING: &str = "String";
+pub const SNIL: &str = "SNil";
+pub const SCONS: &str = "SCons";
+pub const HEAD: &str = "head";
+pub const TAIL: &str = "tail";
 
 impl Book {
   pub fn encode_strs(&mut self) -> Result<(), String> {

tests/golden_tests/run_file/nested_str.hvm

@@ -1 +1,6 @@
-Main = (SCons "a" SNil)
+Main = (
+  (SCons "a" SNil),
+  (SCons 'a' (SCons "bc" SNil)),
+  (SCons "ab" (SCons 'c' SNil)),
+  (SCons "ab" (SCons "cd" SNil))
+)

tests/golden_tests/run_file/unaplied_str.hvm

@@ -0,0 +1 @@
+main = λa λb (SCons a (SCons 'b' (SCons 'c' (SCons b  SNil))))

tests/snapshots/run_file__nested_str.hvm.snap

@@ -2,5 +2,5 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/nested_str.hvm
 ---
-Invalid readback: [InvalidStrTerm]
-""
+Invalid readback: [InvalidStrTerm, InvalidStrTerm, InvalidStrTerm, InvalidStrTerm, InvalidStrTerm]
+(((SCons "a" SNil), (SCons 97 (SCons "bc" SNil))), ((SCons "ab" (SCons 99 SNil)), (SCons "ab" (SCons "cd" SNil))))

tests/snapshots/run_file__unaplied_str.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/unaplied_str.hvm
+---
+λa λb (SCons a (SCons 98 (SCons 99 (SCons b SNil))))