Add Term::Invalid for invalid readbacks

src/term/builtins.rs

@@ -56,7 +56,12 @@ impl Term {
           arm.encode_builtins();
         }
       }
-      Term::Var { .. } | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Era => {}
+      Term::Var { .. }
+      | Term::Lnk { .. }
+      | Term::Ref { .. }
+      | Term::Num { .. }
+      | Term::Era
+      | Term::Invalid => {}
     }
   }
 

src/term/check/unbound_pats.rs

@@ -82,7 +82,8 @@ impl Term {
       | Term::Ref { .. }
       | Term::Num { .. }
       | Term::Str { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
     }
     Ok(())
   }

src/term/check/unbound_vars.rs

@@ -109,7 +109,7 @@ pub fn check_uses<'a>(
       }
     }
     Term::List { .. } => unreachable!(),
-    Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => (),
+    Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => (),
   }
   Ok(())
 }

src/term/display.rs

@@ -78,6 +78,7 @@ impl Term {
       Term::List { els } => {
         write!(f, "[{}]", DisplayJoin(|| els.iter().map(|el| display!("{}", el.display(def_names))), ", "),)
       }
+      Term::Invalid => write!(f, "<Invalid>"),
     })
   }
 }
@@ -252,6 +253,7 @@ impl ReadbackError {
   pub fn display<'a>(&'a self, def_names: &'a DefNames) -> impl Display + '_ {
     DisplayFn(move |f| match self {
       ReadbackError::InvalidNumericMatch => write!(f, "Invalid Numeric Match"),
+      ReadbackError::InvalidNumericOp => write!(f, "Invalid Numeric Operation"),
       ReadbackError::ReachedRoot => write!(f, "Reached Root"),
       ReadbackError::Cyclic => write!(f, "Cyclic Term"),
       ReadbackError::InvalidBind => write!(f, "Invalid Bind"),

src/term/mod.rs

@@ -153,6 +153,7 @@ pub enum Term {
   },
   #[default]
   Era,
+  Invalid,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -450,7 +451,7 @@ impl Term {
         fst.subst(from, to);
         snd.subst(from, to);
       }
-      Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => (),
+      Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => (),
     }
   }
 
@@ -480,7 +481,8 @@ impl Term {
       | Term::Ref { .. }
       | Term::Num { .. }
       | Term::Str { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
     }
   }
 
@@ -551,7 +553,7 @@ impl Term {
             free_vars.extend(fvs);
           }
         }
-        Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => {}
+        Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => {}
       }
     }
 
@@ -593,7 +595,12 @@ impl Term {
         Term::Lam { bod, .. } => {
           go(bod, decls, uses);
         }
-        Term::Var { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era => (),
+        Term::Var { .. }
+        | Term::Num { .. }
+        | Term::Str { .. }
+        | Term::Ref { .. }
+        | Term::Era
+        | Term::Invalid => (),
       }
     }
     let mut decls = Default::default();
@@ -622,23 +629,30 @@ impl Term {
       let succ = (Pattern::Num(MatchNum::Succ(Some(succ_label))), succ_term);
       Term::Match { scrutinee: Box::new(scrutinee), arms: vec![zero, succ] }
     } else {
-      let match_bind = succ_label.clone().unwrap_or_else(|| Name::new("*"));
+      match succ_label {
+        Some(succ) => {
+          let match_bind = succ.clone();
 
-      if let Some(label) = &succ_label {
-        let new_label = Name(format!("{}-1", label));
-        succ_term.subst(label, &Term::Var { nam: new_label.clone() });
-        succ_label = Some(new_label);
-      }
+          let new_label = Name(format!("{}-1", succ));
+          succ_term.subst(&succ, &Term::Var { nam: new_label.clone() });
+          succ_label = Some(new_label);
 
-      let succ = (Pattern::Num(MatchNum::Succ(Some(succ_label))), succ_term);
+          let succ = (Pattern::Num(MatchNum::Succ(Some(succ_label))), succ_term);
 
-      Term::Let {
-        pat: Pattern::Var(Some(match_bind.clone())),
-        val: Box::new(scrutinee),
-        nxt: Box::new(Term::Match {
-          scrutinee: Box::new(Term::Var { nam: match_bind }),
-          arms: vec![zero, succ],
-        }),
+          Term::Let {
+            pat: Pattern::Var(Some(match_bind.clone())),
+            val: Box::new(scrutinee),
+            nxt: Box::new(Term::Match {
+              scrutinee: Box::new(Term::Var { nam: match_bind }),
+              arms: vec![zero, succ],
+            }),
+          }
+        }
+        None => {
+          let succ = (Pattern::Num(MatchNum::Succ(None)), succ_term);
+
+          Term::Match { scrutinee: Box::new(scrutinee), arms: vec![zero, succ] }
+        }
       }
     }
   }

src/term/net_to_term.rs

@@ -108,12 +108,19 @@ impl<'a> Reader<'a> {
             let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
             let succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
 
-            let Term::Lam { nam, bod, .. } = succ_term else { unreachable!() };
-
-            Term::new_native_match(scrutinee, zero_term, nam, *bod)
+            match succ_term {
+              Term::Lam { nam, bod, .. } => Term::new_native_match(scrutinee, zero_term, nam, *bod),
+              _ => {
+                self.error(ReadbackError::InvalidNumericMatch);
+                Term::new_native_match(scrutinee, zero_term, None, succ_term)
+              }
+            }
           }
         }
-        _ => unreachable!(),
+        _ => {
+          self.error(ReadbackError::InvalidNumericMatch);
+          Term::Invalid
+        }
       },
       Ref { def_id } => {
         if self.book.is_def_name_generated(def_id) {
@@ -179,11 +186,14 @@ impl<'a> Reader<'a> {
 
           Term::Opx { op: Op::from_hvmc_label(opr), fst: Box::new(fst), snd: Box::new(snd) }
         }
-        _ => unreachable!(),
+        _ => {
+          self.error(ReadbackError::InvalidNumericOp);
+          Term::Invalid
+        }
       },
       Rot => {
         self.error(ReadbackError::ReachedRoot);
-        Term::Era
+        Term::Invalid
       }
       Tup => match next.slot() {
         // If we're visiting a port 0, then it is a Tup.
@@ -302,7 +312,12 @@ impl Term {
         n
       }
       Term::List { .. } => unreachable!(),
-      Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era => 0,
+      Term::Lnk { .. }
+      | Term::Num { .. }
+      | Term::Str { .. }
+      | Term::Ref { .. }
+      | Term::Era
+      | Term::Invalid => 0,
     };
     if n >= threshold {
       let Split { tag, fst, snd, val } = std::mem::take(split);
@@ -370,7 +385,12 @@ impl Term {
         }
       }
       Term::Let { .. } | Term::List { .. } => unreachable!(),
-      Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => {}
+      Term::Var { .. }
+      | Term::Lnk { .. }
+      | Term::Num { .. }
+      | Term::Str { .. }
+      | Term::Era
+      | Term::Invalid => {}
     }
   }
 }
@@ -441,6 +461,7 @@ pub struct ReadbackErrors(pub Vec<ReadbackError>);
 #[derive(Debug)]
 pub enum ReadbackError {
   InvalidNumericMatch,
+  InvalidNumericOp,
   ReachedRoot,
   Cyclic,
   InvalidBind,
@@ -454,6 +475,7 @@ impl ReadbackError {
   pub fn can_count(&self) -> bool {
     match self {
       ReadbackError::InvalidNumericMatch => true,
+      ReadbackError::InvalidNumericOp => true,
       ReadbackError::ReachedRoot => true,
       ReadbackError::Cyclic => true,
       ReadbackError::InvalidBind => true,

src/term/resugar.rs

@@ -55,7 +55,8 @@ impl<'a> Reader<'a> {
       | Term::Var { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
-      | Term::Era => {}
+      | Term::Era
+      | Term::Invalid => {}
     }
   }
 

src/term/term_to_net.rs

@@ -290,6 +290,7 @@ impl<'a> EncodeTermState<'a> {
 
         Some(Port(tup, 0))
       }
+      Term::Invalid => unreachable!(),
     }
   }
 

src/term/transform/definition_pruning.rs

@@ -126,7 +126,8 @@ impl Book {
       | Term::Num { .. }
       | Term::Str { .. }
       | Term::List { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
     }
   }
 

src/term/transform/desugar_implicit_match_binds.rs

@@ -77,7 +77,8 @@ impl Term {
       | Term::Num { .. }
       | Term::Str { .. }
       | Term::Lnk { .. }
-      | Term::Var { .. } => (),
+      | Term::Var { .. }
+      | Term::Invalid => (),
       Term::Let { pat: _, .. } => {
         unreachable!("Expected destructor let expressions to have been desugared already")
       }

src/term/transform/desugar_let_destructors.rs

@@ -37,7 +37,8 @@ impl Term {
       | Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Ref { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
 
       Term::Let { .. } => {
         let Term::Let { pat, mut val, mut nxt } = std::mem::take(self) else { unreachable!() };

src/term/transform/desugar_match_expressions.rs

@@ -150,7 +150,8 @@ impl Term {
       | Term::Num { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
-      | Term::Era => {}
+      | Term::Era
+      | Term::Invalid => {}
 
       Term::List { .. } => unreachable!(),
       Term::Match { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
@@ -244,7 +245,8 @@ impl Term {
       | Term::Num { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
       Term::List { .. } => unreachable!(),
     }
     Ok(())

src/term/transform/detach_supercombinators.rs

@@ -275,7 +275,9 @@ impl Term {
         }
         Term::Ref { def_id } if *def_id == term_info.rule_id => Detach::Recursive,
         Term::Let { .. } | Term::List { .. } => unreachable!(),
-        Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => Detach::Combinator,
+        Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => {
+          Detach::Combinator
+        }
       }
     }
 

src/term/transform/encode_pattern_matching.rs

@@ -322,7 +322,8 @@ fn normal_order_step(term: &mut Term) -> bool {
     | Term::Num { .. }
     | Term::Str { .. }
     | Term::Ref { .. }
-    | Term::Era => false,
+    | Term::Era
+    | Term::Invalid => false,
   }
 }
 
@@ -397,6 +398,7 @@ fn subst_rule_body(term: &mut Term, subst_var: &Name, body: &Term, name_gen: &mu
     | Term::Num { .. }
     | Term::Str { .. }
     | Term::Ref { .. }
-    | Term::Era => (),
+    | Term::Era
+    | Term::Invalid => (),
   }
 }

src/term/transform/eta_reduction.rs

@@ -66,7 +66,8 @@ impl Term {
       | Term::Str { .. }
       | Term::List { .. }
       | Term::Ref { .. }
-      | Term::Era => {}
+      | Term::Era
+      | Term::Invalid => {}
     }
   }
 }

src/term/transform/linearize.rs

@@ -81,7 +81,8 @@ fn count_var_uses_in_term(term: &Term, uses: &mut HashMap<Name, Val>) {
       }
     }
     Term::List { .. } => unreachable!("Should have been desugared already"),
-    Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => (),
+    Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => {
+    }
   }
 }
 
@@ -224,7 +225,8 @@ fn term_to_affine(
       }
     }
     Term::List { .. } => unreachable!("Should have been desugared already"),
-    Term::Era | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } => (),
+    Term::Era | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Invalid => {
+    }
   };
 }
 

src/term/transform/resolve_ctrs_in_pats.rs

@@ -71,7 +71,8 @@ impl Term {
       | Term::Num { .. }
       | Term::Str { .. }
       | Term::List { .. }
-      | Term::Era => (),
+      | Term::Era
+      | Term::Invalid => (),
     }
   }
 }

src/term/transform/resolve_refs.rs

@@ -94,7 +94,12 @@ impl Term {
         }
       }
       Term::List { .. } => unreachable!("Should have been desugared already"),
-      Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => (),
+      Term::Lnk { .. }
+      | Term::Ref { .. }
+      | Term::Num { .. }
+      | Term::Str { .. }
+      | Term::Era
+      | Term::Invalid => (),
     }
     Ok(())
   }

src/term/transform/simplify_ref_to_ref.rs

@@ -68,6 +68,8 @@ pub fn subst_ref_to_ref(term: &mut Term, ref_map: &BTreeMap<DefId, DefId>) -> bo
       subst
     }
     Term::List { .. } => unreachable!("Should have been desugared already"),
-    Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => false,
+    Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Invalid => {
+      false
+    }
   }
 }

src/term/transform/unique_names.rs

@@ -81,7 +81,12 @@ impl UniqueNameGenerator {
       }
       // Global lam names are already unique, so no need to do anything
       Term::Chn { bod, .. } => self.unique_names_in_term(bod),
-      Term::Lnk { .. } | Term::Ref { .. } | Term::Era | Term::Num { .. } | Term::Str { .. } => (),
+      Term::Lnk { .. }
+      | Term::Ref { .. }
+      | Term::Era
+      | Term::Num { .. }
+      | Term::Str { .. }
+      | Term::Invalid => (),
 
       Term::Let { .. } => {
         unreachable!("Let terms other than tuple destruction should have been desugared already.")

tests/golden_tests/readback_lnet/invalid_mat_mat.hvm

@@ -0,0 +1,3 @@
+(a b)
+& (#1 (* #2)) ~ (c d)
+& ?<(#3 (* #4)) ?<d b>> ~ ?<c a>

tests/golden_tests/readback_lnet/invalid_op2_op2.hvm

@@ -0,0 +1,3 @@
+(a b)
+& #1 ~ (c d)
+& <+ #1 <+ d b>> ~ <+ c a>

tests/snapshots/readback_lnet__bad_net.hvm.snap

@@ -4,4 +4,4 @@ input_file: tests/golden_tests/readback_lnet/bad_net.hvm
 ---
 Readback Warning:
 Reached Root
-*
+<Invalid>

tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/readback_lnet/invalid_mat_mat.hvm
+---
+Readback Warning:
+Invalid Numeric Match with 4 occurrences
+
+λa match match <Invalid> { 0: 3; +: 4 } { 0: <Invalid>; +: <Invalid> }

tests/snapshots/readback_lnet__invalid_op2_op2.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/readback_lnet/invalid_op2_op2.hvm
+---
+Readback Warning:
+Invalid Op2 with 2 occurrences
+
+λa (+ (+ <Invalid> 1) (1 <Invalid>))