[sc-479] Update encodings for better performance, add n-ary dup/tup

HigherOrderCO · Mar 1, 2024 · b5fd2e2 · b5fd2e2
1 parent 9c27eaa
commit b5fd2e2
Show file tree

Hide file tree

Showing 78 changed files with 582 additions and 617 deletions.
diff --git a/src/lib.rs b/src/lib.rs
@@ -42,7 +42,7 @@ pub const CORE_BUILTINS: [&str; 3] = ["HVM.log", "HVM.black_box", "HVM.print"];
 /// Creates a host with the hvm-core primitive definitions built-in.
 /// This needs the book as an Arc because the closure that logs
 /// data needs access to the book.
-pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOpts) -> Arc<Mutex<Host>> {
+pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, adt_encoding: AdtEncoding) -> Arc<Mutex<Host>> {
   let host = Arc::new(Mutex::new(Host::default()));
   host.lock().unwrap().insert_def(
     "HVM.log",
@@ -54,13 +54,8 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOp
         let host = host.lock().unwrap();
         let tree = host.readback_tree(&wire);
         let net = hvmc::ast::Net { root: tree, rdex: vec![] };
-        let net = hvmc_to_net(&net);
-        let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false);
-        let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding);
-        term.resugar_builtins();
-
-        readback_errors.extend(resugar_errs);
-        println!("{}{}", display_readback_errors(&readback_errors), term);
+        let (term, errs) = readback_hvmc(&net, &book, &labels, false, adt_encoding);
+        println!("{}{}", display_readback_errors(&errs), term);
       }
     }))),
   );
@@ -74,12 +69,7 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOp
         let host = host.lock().unwrap();
         let tree = host.readback_tree(&wire);
         let net = hvmc::ast::Net { root: tree, rdex: vec![] };
-        let net = hvmc_to_net(&net);
-        let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false);
-        let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding);
-        term.resugar_builtins();
-
-        readback_errors.extend(resugar_errs);
+        let (term, _errs) = readback_hvmc(&net, &book, &labels, false, adt_encoding);
         if let Term::Str { val } = term {
           println!("{val}");
         }
@@ -197,18 +187,14 @@ pub fn run_book(
 
   // Run
   let debug_hook = run_opts.debug_hook(&book, &labels);
-  let host = create_host(book.clone(), labels.clone(), compile_opts);
+  let host = create_host(book.clone(), labels.clone(), compile_opts.adt_encoding);
   host.lock().unwrap().insert_book(&core_book);
 
   let (res_lnet, stats) = run_compiled(host, mem_size, run_opts, debug_hook, book.hvmc_entrypoint());
 
-  // Readback
-  let net = hvmc_to_net(&res_lnet);
-  let (mut res_term, mut readback_errors) = net_to_term(&net, &book, &labels, run_opts.linear);
-  let resugar_errs = res_term.resugar_adts(&book, compile_opts.adt_encoding);
-  res_term.resugar_builtins();
+  let (res_term, readback_errors) =
+    readback_hvmc(&res_lnet, &book, &labels, run_opts.linear, compile_opts.adt_encoding);
 
-  readback_errors.extend(resugar_errs);
   let info = RunInfo { stats, readback_errors, net: res_lnet, book, labels };
   Ok((res_term, info))
 }
@@ -306,6 +292,24 @@ pub fn run_compiled(
   })
 }
 
+pub fn readback_hvmc(
+  net: &Net,
+  book: &Arc<Book>,
+  labels: &Arc<Labels>,
+  linear: bool,
+  adt_encoding: AdtEncoding,
+) -> (Term, Vec<ReadbackError>) {
+  let net = hvmc_to_net(net);
+  let (mut term, mut readback_errors) = net_to_term(&net, book, labels, linear);
+
+  let resugar_errs = term.resugar_adts(book, adt_encoding);
+  term.resugar_builtins();
+
+  readback_errors.extend(resugar_errs);
+
+  (term, readback_errors)
+}
+
 #[derive(Clone, Copy, Debug, Default)]
 pub struct RunOpts {
   pub single_core: bool,

diff --git a/src/term/builtins.rs b/src/term/builtins.rs
@@ -40,13 +40,16 @@ impl Term {
       }
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.encode_builtins(),
       Term::App { fun: fst, arg: snd, .. }
-      | Term::Tup { fst, snd }
-      | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. }
       | Term::Dup { val: fst, nxt: snd, .. } => {
         fst.encode_builtins();
         snd.encode_builtins();
       }
+      Term::Sup { els, .. } | Term::Tup { els } => {
+        for el in els {
+          el.encode_builtins();
+        }
+      }
       Term::Mat { args, rules } => {
         for arg in args {
           arg.encode_builtins();
@@ -81,15 +84,11 @@ impl Pattern {
     match self {
       Pattern::Lst(pats) => *self = Self::encode_list(std::mem::take(pats)),
       Pattern::Str(str) => *self = Self::encode_str(str),
-      Pattern::Ctr(_, pats) => {
+      Pattern::Ctr(_, pats) | Pattern::Tup(pats) => {
         for pat in pats {
           pat.encode_builtins();
         }
       }
-      Pattern::Tup(fst, snd) => {
-        fst.encode_builtins();
-        snd.encode_builtins();
-      }
       Pattern::Var(..) | Pattern::Num(..) => {}
     }
   }

diff --git a/src/term/check/ctrs_arities.rs b/src/term/check/ctrs_arities.rs
@@ -57,11 +57,7 @@ impl Pattern {
             return Err(MatchErr::CtrArityMismatch(name.clone(), found, *expected));
           }
         }
-        Pattern::Tup(fst, snd) => {
-          to_check.push(fst);
-          to_check.push(snd);
-        }
-        Pattern::Lst(els) => {
+        Pattern::Lst(els) | Pattern::Tup(els) => {
           for el in els {
             to_check.push(el);
           }
@@ -93,15 +89,13 @@ impl Term {
         nxt.check_ctrs_arities(arities)?;
       }
 
-      Term::Lst { els } => {
+      Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
         for el in els {
           el.check_ctrs_arities(arities)?;
         }
       }
       Term::App { fun: fst, arg: snd, .. }
-      | Term::Tup { fst, snd }
       | Term::Dup { val: fst, nxt: snd, .. }
-      | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. } => {
         fst.check_ctrs_arities(arities)?;
         snd.check_ctrs_arities(arities)?;

diff --git a/src/term/check/match_arity.rs b/src/term/check/match_arity.rs
@@ -45,15 +45,13 @@ impl Term {
         }
       }
 
-      Term::Lst { els } => {
+      Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
         for el in els {
           el.check_match_arity()?;
         }
       }
       Term::App { fun: fst, arg: snd, .. }
-      | Term::Tup { fst, snd }
       | Term::Dup { val: fst, nxt: snd, .. }
-      | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. }
       | Term::Let { val: fst, nxt: snd, .. } => {
         fst.check_match_arity()?;

diff --git a/src/term/check/type_check.rs b/src/term/check/type_check.rs
@@ -32,7 +32,7 @@ fn unify(old: Type, new: Type) -> Result<Type, MatchErr> {
     (Type::NumSucc(n), Type::Num) => Ok(Type::NumSucc(n)),
     (Type::NumSucc(a), Type::NumSucc(b)) if a == b => Ok(Type::NumSucc(a)),
 
-    (Type::Tup, Type::Tup) => Ok(Type::Tup),
+    (Type::Tup(a), Type::Tup(b)) if a == b => Ok(Type::Tup(a)),
 
     (old, new) => Err(MatchErr::TypeMismatch(new, old)),
   }

diff --git a/src/term/check/unbound_pats.rs b/src/term/check/unbound_pats.rs
@@ -53,11 +53,7 @@ impl Pattern {
           }
           check.extend(args.iter());
         }
-        Pattern::Tup(fst, snd) => {
-          check.push(fst);
-          check.push(snd);
-        }
-        Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)),
+        Pattern::Tup(args) | Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)),
         Pattern::Var(_) | Pattern::Num(_) | Pattern::Str(_) => {}
       }
     }
@@ -84,16 +80,18 @@ impl Term {
           rule.body.check_unbound_pats(is_ctr)?;
         }
       }
+      Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
+        for el in els {
+          el.check_unbound_pats(is_ctr)?;
+        }
+      }
       Term::App { fun: fst, arg: snd, .. }
-      | Term::Tup { fst, snd }
       | Term::Dup { val: fst, nxt: snd, .. }
-      | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. } => {
         fst.check_unbound_pats(is_ctr)?;
         snd.check_unbound_pats(is_ctr)?;
       }
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_unbound_pats(is_ctr)?,
-      Term::Lst { .. } => unreachable!(),
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Ref { .. }

diff --git a/src/term/check/unbound_vars.rs b/src/term/check/unbound_vars.rs
@@ -95,7 +95,9 @@ pub fn check_uses<'a>(
       }
     }
     Term::Chn { nam, bod, .. } => {
-      globals.entry(nam).or_default().0 += 1;
+      if let Some(nam) = nam {
+        globals.entry(nam).or_default().0 += 1;
+      }
       check_uses(bod, scope, globals, errs);
     }
     Term::Lnk { nam } => {
@@ -107,21 +109,27 @@ pub fn check_uses<'a>(
       check_uses(nxt, scope, globals, errs);
       pop_scope(nam.as_ref(), scope);
     }
-    Term::Dup { fst, snd, val, nxt, .. }
-    | Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => {
+    Term::Dup { bnd, val, nxt, .. } => {
       check_uses(val, scope, globals, errs);
-      push_scope(fst.as_ref(), scope);
-      push_scope(snd.as_ref(), scope);
+      for bnd in bnd.iter() {
+        push_scope(bnd.as_ref(), scope);
+      }
       check_uses(nxt, scope, globals, errs);
-      pop_scope(fst.as_ref(), scope);
-      pop_scope(snd.as_ref(), scope);
+      for bnd in bnd.iter() {
+        pop_scope(bnd.as_ref(), scope);
+      }
     }
-    Term::Let { .. } => unreachable!(),
-    Term::App { fun, arg, .. } => {
-      check_uses(fun, scope, globals, errs);
-      check_uses(arg, scope, globals, errs);
+    Term::Let { pat, val, nxt } => {
+      check_uses(val, scope, globals, errs);
+      for bnd in pat.bind_or_eras() {
+        push_scope(bnd.as_ref(), scope);
+      }
+      check_uses(nxt, scope, globals, errs);
+      for bnd in pat.bind_or_eras() {
+        pop_scope(bnd.as_ref(), scope);
+      }
     }
-    Term::Tup { fst, snd } | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } => {
+    Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
       check_uses(fst, scope, globals, errs);
       check_uses(snd, scope, globals, errs);
     }
@@ -137,7 +145,11 @@ pub fn check_uses<'a>(
         rule.pats.iter().flat_map(|p| p.binds()).rev().for_each(|nam| pop_scope(Some(nam), scope));
       }
     }
-    Term::Lst { .. } => unreachable!(),
+    Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
+      for el in els {
+        check_uses(el, scope, globals, errs);
+      }
+    }
     Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => (),
   }
 }

diff --git a/src/term/display.rs b/src/term/display.rs
@@ -47,7 +47,7 @@ impl fmt::Display for Term {
       }
       Term::Var { nam } => write!(f, "{nam}"),
       Term::Chn { tag, nam, bod } => {
-        write!(f, "{}λ${} {}", tag.display_padded(), nam, bod)
+        write!(f, "{}λ${} {}", tag.display_padded(), var_as_str(nam), bod)
       }
       Term::Lnk { nam } => write!(f, "${nam}"),
       Term::Let { pat, val, nxt } => {
@@ -68,22 +68,20 @@ impl fmt::Display for Term {
           ),
         )
       }
-      Term::Dup { tag, fst, snd, val, nxt } => {
-        write!(f, "let {}{{{} {}}} = {}; {}", tag, var_as_str(fst), var_as_str(snd), val, nxt)
+      Term::Dup { tag, bnd, val, nxt } => {
+        write!(f, "let {}{{{}}} = {}; {}", tag, DisplayJoin(|| bnd.iter().map(var_as_str), " "), val, nxt)
       }
-      Term::Sup { tag, fst, snd } => {
-        write!(f, "{}{{{} {}}}", tag, fst, snd)
+      Term::Sup { tag, els } => {
+        write!(f, "{}{{{}}}", tag, DisplayJoin(|| els, " "))
       }
       Term::Era => write!(f, "*"),
       Term::Num { val } => write!(f, "{val}"),
       Term::Str { val } => write!(f, "{val:?}"),
       Term::Opx { op, fst, snd } => {
         write!(f, "({} {} {})", op, fst, snd)
       }
-      Term::Tup { fst, snd } => write!(f, "({}, {})", fst, snd),
-      Term::Lst { els } => {
-        write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),)
-      }
+      Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),),
+      Term::Lst { els } => write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),),
       Term::Err => write!(f, "<Invalid>"),
     }
   }
@@ -109,7 +107,7 @@ impl fmt::Display for Pattern {
         write!(f, "({}{})", nam, DisplayJoin(|| pats.iter().map(|p| display!(" {p}")), ""))
       }
       Pattern::Num(num) => write!(f, "{num}"),
-      Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,),
+      Pattern::Tup(pats) => write!(f, "({})", DisplayJoin(|| pats, ", ")),
       Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats, ", ")),
       Pattern::Str(str) => write!(f, "\"{str}\""),
     }
@@ -184,7 +182,7 @@ impl fmt::Display for Type {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
       Type::Any => write!(f, "any"),
-      Type::Tup => write!(f, "tup"),
+      Type::Tup(n) => write!(f, "tup{n}"),
       Type::Num => write!(f, "num"),
       Type::NumSucc(n) => write!(f, "{n}+"),
       Type::Adt(nam) => write!(f, "{nam}"),