Fix readback of adts and adts matches with wrong tags, improve docs

src/term/display.rs

@@ -226,7 +226,7 @@ impl ReadbackErrors {
         return Ok(());
       }
 
-      writeln!(f, "Invalid readback:")?;
+      writeln!(f, "Readback Warning:")?;
       let mut err_counts = std::collections::HashMap::new();
       for err in &self.0 {
         if err.can_count() {
@@ -256,6 +256,14 @@ impl ReadbackError {
       ReadbackError::Cyclic => write!(f, "Cyclic Term"),
       ReadbackError::InvalidBind => write!(f, "Invalid Bind"),
       ReadbackError::InvalidAdt => write!(f, "Invalid Adt"),
+      ReadbackError::UnexpectedTag(exp, fnd) => {
+        write!(f, "Unexpected tag found during Adt readback, expected '#{}', but found ", exp)?;
+
+        match fnd {
+          Tag::Static => write!(f, "no tag"),
+          _ => write!(f, "'{}'", fnd.display()),
+        }
+      }
       ReadbackError::InvalidAdtMatch => write!(f, "Invalid Adt Match"),
       ReadbackError::InvalidStrTerm(term) => {
         write!(f, "Invalid String Character value '{}'", term.display(def_names))

src/term/net_to_term.rs

@@ -220,12 +220,12 @@ impl<'a> Reader<'a> {
   ///
   /// # Example
   ///
-  /// ```text
+  /// ```hvm
   /// // λa let (a, b) = a; (a, b)
   /// ([a b] [a b])
   ///
-  /// The node `(a, b)` is just a reconstruction of the destructuring of `a`,  
-  /// So we can skip both steps and just return the "value" unchanged:
+  /// // The node `(a, b)` is just a reconstruction of the destructuring of `a`,  
+  /// // So we can skip both steps and just return the "value" unchanged:
   ///
   /// // λa a
   /// (a a)
@@ -449,6 +449,7 @@ pub enum ReadbackError {
   InvalidAdt,
   InvalidAdtMatch,
   InvalidStrTerm(Term),
+  UnexpectedTag(Name, Tag),
 }
 
 impl ReadbackError {
@@ -460,7 +461,8 @@ impl ReadbackError {
       ReadbackError::InvalidBind => true,
       ReadbackError::InvalidAdt => true,
       ReadbackError::InvalidAdtMatch => true,
-      ReadbackError::InvalidStrTerm(..) => false,
+      ReadbackError::InvalidStrTerm(_) => false,
+      ReadbackError::UnexpectedTag(..) => false,
     }
   }
 }

src/term/resugar.rs

@@ -1,8 +1,12 @@
 use super::{
   net_to_term::{ReadbackError, Reader},
-  transform::encode_strs::{SCONS, SNIL},
+  transform::{
+    encode_adts::adt_field_tag,
+    encode_strs::{SCONS, SNIL},
+  },
   Adt, Name, Pattern, Tag, Term,
 };
+use std::borrow::BorrowMut;
 
 impl<'a> Reader<'a> {
   pub fn resugar_adts(&mut self, term: &mut Term) {
@@ -16,7 +20,6 @@ impl<'a> Reader<'a> {
         };
 
         self.resugar_adt_cons(term, adt, adt_name);
-        self.resugar_adts(term);
       }
 
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => self.resugar_adts(bod),
@@ -29,7 +32,6 @@ impl<'a> Reader<'a> {
         };
 
         self.resugar_adt_match(term, adt_name, adt);
-        self.resugar_adts(term);
       }
 
       Term::App { fun: fst, arg: snd, .. }
@@ -59,6 +61,22 @@ impl<'a> Reader<'a> {
     }
   }
 
+  /// Reconstructs adt-tagged lambdas as their constructors
+  ///
+  /// # Example
+  ///
+  /// ```hvm
+  /// data Option = (Some val) | None
+  ///
+  /// // This value:
+  /// (Some (Some None))
+  ///
+  /// // Gives the following readback:
+  /// #Option λa #Option λ* #Option.Some.val (a #Option λb #Option λ* #Option.Some.val (b #Option λ* #Option λc c))
+  ///
+  /// // Which gets resugared as:
+  /// (Some (Some None))
+  /// ```
   fn resugar_adt_cons(&mut self, term: &mut Term, adt: &Adt, adt_name: &Name) {
     let mut app = &mut *term;
     let mut current_arm = None;
@@ -85,15 +103,17 @@ impl<'a> Reader<'a> {
 
     let mut cur = &mut *app;
 
-    for _ in ctr_args {
+    for field in ctr_args.iter().rev() {
       self.deref(cur);
+      let adt_field_tag = adt_field_tag(adt_name, ctr, field);
+
       match cur {
-        Term::App { tag: Tag::Static, fun, .. } => cur = fun,
-        // Removes the tag of the application with the adt field `#adt_name.cons_name.field_name`
-        Term::App { tag: tag @ Tag::Named(_), fun, .. } => {
+        Term::App { tag: Tag::Named(tag_name), .. } if tag_name == &adt_field_tag => {
+          let Term::App { tag, fun, .. } = cur.borrow_mut() else { unreachable!() };
           *tag = Tag::Static;
           cur = fun
         }
+        Term::App { tag, .. } => return self.error(ReadbackError::UnexpectedTag(adt_field_tag, tag.clone())),
         _ => return self.error(ReadbackError::InvalidAdt),
       }
     }
@@ -105,8 +125,38 @@ impl<'a> Reader<'a> {
 
     *cur = self.book.def_names.get_ref(ctr);
     *term = std::mem::take(app);
+
+    self.resugar_adts(term);
   }
 
+  /// Reconstructs adt-tagged applications as a match term
+  ///
+  /// # Example
+  ///
+  /// ```hvm
+  /// data Option = (Some val) | None
+  ///
+  /// // This match expression:
+  /// Option.and = @a @b match a {
+  ///   Some: match b {
+  ///     Some: 1
+  ///     None: 2
+  ///   }
+  ///   None: 3
+  /// }  
+  ///
+  /// // Gives the following readback:
+  /// λa λb (#Option (a #Option.Some.val λ* λc #Option (c #Option.Some.val λ* 1 2) λ* 3) b)
+  ///
+  /// // Which gets resugared as:
+  /// λa λb (match a {
+  ///   (Some *): λc match c {
+  ///     (Some *): 1;
+  ///     (None)  : 2
+  ///   };
+  ///   (None): λ* 3
+  /// } b)
+  /// ```
   fn resugar_adt_match(&mut self, term: &mut Term, adt_name: &Name, adt: &Adt) {
     let mut cur = &mut *term;
     let mut arms = Vec::new();
@@ -118,20 +168,28 @@ impl<'a> Reader<'a> {
           let mut args = Vec::new();
           let mut arm = arg.as_mut();
 
-          for _ in ctr_args {
+          for field in ctr_args {
             self.deref(arm);
 
-            if !matches!(arm, Term::Lam { tag: Tag::Static, .. }) {
-              let nam = self.namegen.unique();
-              *arm = Term::named_lam(nam.clone(), Term::arg_call(std::mem::take(arm), Some(nam)));
-            }
+            let adt_field_tag = adt_field_tag(adt_name, ctr, field);
 
             match arm {
-              Term::Lam { nam, bod, .. } => {
+              Term::Lam { tag: Tag::Named(tag), .. } if tag == &adt_field_tag => {
+                let Term::Lam { nam, bod, .. } = arm.borrow_mut() else { unreachable!() };
+
                 args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x))));
                 arm = bod.as_mut();
               }
-              _ => unreachable!(),
+              _ => {
+                if let Term::Lam { tag, .. } = arm {
+                  self.error(ReadbackError::UnexpectedTag(adt_field_tag.clone(), tag.to_owned()));
+                }
+
+                let nam = self.namegen.unique();
+                args.push(Pattern::Var(Some(nam.clone())));
+                let tag = Tag::Named(adt_field_tag);
+                *arm = Term::tagged_app(tag, std::mem::take(&mut arm), Term::Var { nam });
+              }
             }
           }
 
@@ -145,6 +203,8 @@ impl<'a> Reader<'a> {
     let scrutinee = Box::new(std::mem::take(cur));
     let arms = arms.into_iter().rev().map(|(pat, term)| (pat, std::mem::take(term))).collect();
     *term = Term::Match { scrutinee, arms };
+
+    self.resugar_adts(term);
   }
 
   fn resugar_string(&mut self, term: Term) -> Term {

src/term/transform/encode_adts.rs

@@ -23,7 +23,7 @@ fn make_lam(adt_name: &Name, ctr_args: Vec<Name>, ctrs: Vec<Name>, ctr_name: &Na
   let ctr = Term::Var { nam: ctr_name.clone() };
 
   let app = ctr_args.iter().cloned().fold(ctr, |acc, nam| {
-    Term::tagged_app(Tag::Named(Name(format!("{}.{}.{}", adt_name, ctr_name, nam))), acc, Term::Var { nam })
+    Term::tagged_app(Tag::Named(adt_field_tag(adt_name, ctr_name, &nam)), acc, Term::Var { nam })
   });
 
   let lam =
@@ -31,3 +31,7 @@ fn make_lam(adt_name: &Name, ctr_args: Vec<Name>, ctrs: Vec<Name>, ctr_name: &Na
 
   ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
 }
+
+pub fn adt_field_tag(adt_name: &Name, ctr_name: &Name, field_name: &Name) -> Name {
+  Name(format!("{}.{}.{}", adt_name, ctr_name, field_name))
+}

tests/golden_tests/run_file/adt_match_wrong_tag.hvm

@@ -0,0 +1,3 @@
+data Option = (Some val) | None
+
+main = λa #Option (a #wrong_tag λb b *)

tests/golden_tests/run_file/adt_wrong_tag.hvm

@@ -0,0 +1,3 @@
+data Option = (Some val) | None
+
+main = (@a #Option (a #wrong_tag @x x *)) 

tests/snapshots/readback_lnet__bad_net.hvm.snap

@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/readback_lnet/bad_net.hvm
 ---
-Invalid readback:
+Readback Warning:
 Reached Root
 *

tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/adt_match_wrong_tag.hvm
+---
+Readback Warning:
+Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
+
+λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }

tests/snapshots/run_file__adt_option_and.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/adt_option_and.hvm
 ---
-λa match a { (Some g): (#Option.Some.val λb λc (match c { (Some h): (#Option.Some.val λd (λe λf (Some (f, e)) d) h); (None): λ* None } b) g); (None): λ* None }
+λa match a { (Some b): λc (match c { (Some d): λe (Some (e, d)); (None): λ* None } b); (None): λ* None }

tests/snapshots/run_file__adt_wrong_tag.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/adt_wrong_tag.hvm
+---
+Readback Warning:
+Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
+
+λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }

tests/snapshots/run_file__nested_list_and_string.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/nested_list_and_string.hvm
 ---
-Invalid readback:
+Readback Warning:
 Invalid String Character value '*'
 Invalid String Character value '[7, "1234", 9]'
 

tests/snapshots/run_file__nested_str.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/nested_str.hvm
 ---
-Invalid readback:
+Readback Warning:
 Invalid String Character value '"a"'
 Invalid String Character value '"bc"'
 Invalid String Character value '"ab"'

tests/snapshots/run_file__wrong_string.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/wrong_string.hvm
 ---
-Invalid readback:
+Readback Warning:
 Invalid String Character value '*'
 Invalid String Character value '(*, 4)'