[sc-463] Remove hvm-lang as a dev-dependency by making the tests work on hvm-core ASTs only.

Cargo.toml

@@ -36,8 +36,7 @@ _fuzz_no_free = ["_fuzz"]
 
 [dev-dependencies]
 criterion = "0.5.1"
-hvm-lang = { git = "https://github.com/HigherOrderCO/hvm-lang.git" } # allows us to use the hvm-lang syntax for tests/benchmarks
-insta = "1.34.0"
+insta = { version = "1.34.0", features = ["glob"] }
 serial_test = "3.0.0"
 
 [patch."https://github.com/HigherOrderCO/hvm-core.git"]

benches/benches.rs

@@ -4,9 +4,7 @@ use hvmc::{
   host::Host,
   run::{Net as RtNet, Strict},
 };
-use hvml::{term::Book as HvmlBook, ENTRY_POINT};
 use std::{
-  ffi::OsStr,
   fs,
   path::{Path, PathBuf},
   time::Duration,
@@ -15,38 +13,11 @@ use std::{
 // Loads file and generate net from hvm-core syntax
 fn load_from_core<P: AsRef<Path>>(file: P) -> Book {
   let code = fs::read_to_string(file).unwrap();
-  let (_, code) = extract_size(&code);
 
   code.parse().unwrap()
 }
-
-// Loads file and generate net from hvm-lang syntax
-fn load_from_lang<P: AsRef<Path>>(file: P) -> Book {
-  let code = fs::read_to_string(file).unwrap();
-  let (_, code) = extract_size(&code);
-
-  let mut book = hvml::term::parser::parse_book(&code, HvmlBook::default, false).unwrap();
-  let book = hvml::compile_book(&mut book, hvml::CompileOpts::light()).unwrap().core_book;
-  book
-}
-
-fn extract_size(code: &str) -> (usize, &str) {
-  code
-    .strip_prefix("// size = ")
-    .and_then(|code| code.split_once('\n'))
-    .and_then(|(size, rest)| {
-      match size.split_ascii_whitespace().collect::<Vec<_>>().as_slice() {
-        [a, "<<", b] => a.parse::<usize>().ok().zip(b.parse::<usize>().ok()).map(|(a, b)| a << b),
-        [a] => a.parse().ok(),
-        _ => None,
-      }
-      .map(|size| (size, rest))
-    })
-    .expect("failed to extract bench size")
-}
-
 fn run_programs_dir(c: &mut Criterion) {
-  let root = PathBuf::from(format!("{}/benches/programs", env!("CARGO_MANIFEST_DIR")));
+  let root = PathBuf::from(format!("{}/tests/programs", env!("CARGO_MANIFEST_DIR")));
   run_dir(&root, None, c);
 }
 
@@ -66,18 +37,15 @@ fn run_dir(path: &PathBuf, group: Option<String>, c: &mut Criterion) {
 
       run_dir(entry, Some(group), c)
     } else {
-      run_file(entry, group.clone(), c);
+      if entry.extension().unwrap().to_str().unwrap() == "hvmc" {
+        run_file(entry, group.clone(), c);
+      }
     }
   }
 }
 
 fn run_file(path: &PathBuf, group: Option<String>, c: &mut Criterion) {
-  let book = match path.extension().and_then(OsStr::to_str) {
-    Some("hvmc") => load_from_core(path),
-    Some("hvm") => load_from_lang(path),
-    _ => panic!("invalid file found: {}", path.to_string_lossy()),
-  };
-
+  let book = load_from_core(path);
   let file_name = path.file_stem().unwrap().to_string_lossy();
 
   match group {
@@ -87,25 +55,25 @@ fn run_file(path: &PathBuf, group: Option<String>, c: &mut Criterion) {
 }
 
 fn benchmark(file_name: &str, book: Book, c: &mut Criterion) {
-  let area = RtNet::<Strict>::init_heap(1 << 24);
+  let area = RtNet::<Strict>::init_heap(1 << 29);
   let host = Host::new(&book);
   c.bench_function(file_name, |b| {
     b.iter(|| {
       let mut net = RtNet::<Strict>::new(&area);
-      net.boot(host.defs.get(ENTRY_POINT).unwrap());
+      net.boot(host.defs.get("main").unwrap());
       black_box(black_box(net).normal())
     });
   });
 }
 
 fn benchmark_group(file_name: &str, group: String, book: Book, c: &mut Criterion) {
-  let area = RtNet::<Strict>::init_heap(1 << 24);
+  let area = RtNet::<Strict>::init_heap(1 << 29);
   let host = Host::new(&book);
 
   c.benchmark_group(group).bench_function(file_name, |b| {
     b.iter(|| {
       let mut net = RtNet::<Strict>::new(&area);
-      net.boot(host.defs.get(ENTRY_POINT).unwrap());
+      net.boot(host.defs.get("main").unwrap());
       black_box(black_box(net).normal())
     });
   });
@@ -125,13 +93,13 @@ fn interact_benchmark(c: &mut Criterion) {
 
   for (name, redex) in cases {
     let mut book = Book::default();
-    book.insert(ENTRY_POINT.to_string(), Net { root: Era, rdex: vec![redex] });
+    book.insert("main".to_string(), Net { root: Era, rdex: vec![redex] });
     let area = RtNet::<Strict>::init_heap(1 << 24);
     let host = Host::new(&book);
     group.bench_function(name, |b| {
       b.iter(|| {
         let mut net = RtNet::<Strict>::new(&area);
-        net.boot(host.defs.get(ENTRY_POINT).unwrap());
+        net.boot(host.defs.get("main").unwrap());
         black_box(black_box(net).normal())
       });
     });

examples/church_encoding/church.hvmc

@@ -1,21 +1,15 @@
-@S = ((a (b c)) ({2 a (c d)} (b d)))
+@S = ((a (b c)) ({3 (c d) a} (b d)))
 @Z = (* (a a))
-
-@add = ((a (b c)) ((d (e b)) ({2 d a} (e c))))
+@add = ((a (b c)) ((d (e b)) ({11 a d} (e c))))
+@c2 = ({5 (a b) (c a)} (c b))
+@c3 = ({7 (a b) {9 (c a) (d c)}} (d b))
+@c4 = a
+& @S ~ (b a)
+& @S ~ (c b)
+& @S ~ (d c)
+& @S ~ (@Z d)
+@main = a
+& @add ~ (b (@c4 a))
+& @mul ~ (@c2 (@c3 b))
 @mul = ((a (b c)) ((d a) (d (b c))))
 
-@c2 = ({2 (a b) (b c)} (a c))
-@c3 = ({2 (a b) {3 (b c) (c d)}} (a d))
-
-@c4
-  = a
-  & @S ~ (b a)
-  & @S ~ (c b)
-  & @S ~ (d c)
-  & @S ~ (@Z d)
-
-@main
-  = a
-  & @add ~ (b (@c4 a))
-  & @mul ~ (@c2 (@c3 b))
-

examples/lambda_calculus/hoas.hvmc

@@ -1,57 +1,115 @@
-// TODO: cleanup / make readable
-
 @App = (a (b (* ((a (b c)) (* c)))))
+@C0 = a
+& @Lam ~ (@C0$S0 a)
+@C0$S0 = (* a)
+& @Lam ~ ((b b) a)
+@C1 = a
+& @Lam ~ (@C1$S0 a)
+@C1$S0 = (a b)
+& @Lam ~ ((c d) b)
+& @App ~ (a (c d))
+@C2 = a
+& @Lam ~ (@C2$S0 a)
+@C2$S0 = ({3 a b} c)
+& @Lam ~ ((d e) c)
+& @App ~ (a (f e))
+& @App ~ (b (d f))
+@C3 = a
+& @Lam ~ (@C3$S0 a)
+@C3$S0 = ({5 a {7 b c}} d)
+& @Lam ~ ((e f) d)
+& @App ~ (a (g f))
+& @App ~ (b (h g))
+& @App ~ (c (e h))
+@C4 = a
+& @Lam ~ (@C4$S0 a)
+@C4$S0 = ({9 a {11 b {13 c d}}} e)
+& @Lam ~ ((f g) e)
+& @App ~ (a (h g))
+& @App ~ (b (i h))
+& @App ~ (c (j i))
+& @App ~ (d (f j))
 @C6 = a
-& @Lam ~ (@X a)
+& @Lam ~ (@C6$S0 a)
+@C6$S0 = ({15 a {17 b {19 c {21 d {23 e f}}}}} g)
+& @Lam ~ ((h i) g)
+& @App ~ (a (j i))
+& @App ~ (b (k j))
+& @App ~ (c (l k))
+& @App ~ (d (m l))
+& @App ~ (e (n m))
+& @App ~ (f (h n))
+@C8 = a
+& @Lam ~ (@C8$S0 a)
+@C8$S0 = ({25 a {27 b {29 c {31 d {33 e {35 f g}}}}}} h)
+& @Lam ~ ((i j) h)
+& @App ~ (a (k j))
+& @App ~ (b (l k))
+& @App ~ (c (m l))
+& @App ~ (d (n m))
+& @App ~ (e (o n))
+& @App ~ (f (p o))
+& @App ~ (g (i p))
+@CS = a
+& @Lam ~ (@CS$S0 a)
+@CS$S0 = (a b)
+& @Lam ~ (({37 c d} e) b)
+& @Lam ~ ((f g) e)
+& @App ~ (c (h g))
+& @App ~ (i (f h))
+& @App ~ (a (d i))
+@FOO = a
+& @Lam ~ (@FOO$S0 a)
+@FOO$S0 = ({39 a b} c)
+& @App ~ (a (b c))
 @False = a
-& @Lam ~ (@b a)
+& @Lam ~ (@False$S0 a)
+@False$S0 = (* a)
+& @Lam ~ ((b b) a)
+@ID = a
+& @Lam ~ ((b b) a)
 @Lam = (a ((a b) (* (* b))))
-@M = (a b)
-& @reduce.app ~ (c b)
-& @reduce ~ (a c)
-@N = ((a b) (a c))
-& @reduce ~ (b c)
 @Not = a
-& @Lam ~ (@d a)
-@O = (a (b c))
-& @App ~ (d c)
-& @App ~ (a (b d))
-@P = (a b)
-& @App ~ (c b)
-& @Sub ~ (a c)
-@Q = ((a b) c)
-& @Lam ~ ((d e) c)
-& @normal ~ (b e)
-& @Sub ~ (d a)
-@R = (a (b c))
-& @App ~ (d (e c))
-& @normal ~ (b e)
-& @normal ~ (a d)
+& @Lam ~ (@Not$S0 a)
+@Not$S0 = (a b)
+& @App ~ (c (@True b))
+& @App ~ (a (@False c))
 @Sub = (a (* (* ((a b) b))))
 @True = a
-& @Lam ~ (@c a)
-@X = ({2 a {3 b {4 c {5 d {6 e f}}}}} g)
-& @Lam ~ ((h i) g)
-& @App ~ (f (j i))
-& @App ~ (e (k j))
-& @App ~ (d (l k))
-& @App ~ (c (m l))
-& @App ~ (b (n m))
-& @App ~ (a (h n))
-@b = (* a)
-& @Lam ~ ((b b) a)
-@c = (a b)
+& @Lam ~ (@True$S0 a)
+@True$S0 = (a b)
 & @Lam ~ ((* a) b)
-@d = (a b)
-& @App ~ (c (@True b))
-& @App ~ (a (@False c))
 @main = a
 & @normal ~ (b a)
 & @App ~ (c (@True b))
 & @App ~ (@C6 (@Not c))
 @normal = (a b)
 & @normal.go ~ (c b)
 & @reduce ~ (a c)
-@normal.go = ((@Q (@R ((a a) b))) b)
-@reduce = ((@Lam (@M (@Sub a))) a)
-@reduce.app = ((@N (@O (@P a))) a)
+@normal.go = ((@normal.go$S0 (@normal.go$S1 ((a a) b))) b)
+@normal.go$S0 = ((a b) c)
+& @Lam ~ ((d e) c)
+& @normal ~ (b e)
+& @Sub ~ (d a)
+@normal.go$S1 = (a (b c))
+& @App ~ (d (e c))
+& @normal ~ (b e)
+& @normal ~ (a d)
+@reduce = ((@reduce$S0 (@reduce$S1 (@reduce$S2 a))) a)
+@reduce$S0 = (a b)
+& @Lam ~ (a b)
+@reduce$S1 = (a (b c))
+& @reduce.app ~ (d (b c))
+& @reduce ~ (a d)
+@reduce$S2 = (a b)
+& @Sub ~ (a b)
+@reduce.app = ((@reduce.app$S0 (@reduce.app$S1 (@reduce.app$S2 a))) a)
+@reduce.app$S0 = ((a b) (a c))
+& @reduce ~ (b c)
+@reduce.app$S1 = (a (b (c d)))
+& @App ~ (e (c d))
+& @App ~ (a (b e))
+@reduce.app$S2 = (a (b c))
+& @App ~ (d (b c))
+& @Sub ~ (a d)
+

examples/machine_u32/num_add.hvmc

@@ -1,4 +1,4 @@
-@add = (<+ b R> (b R))
+@add = (<+ a b> (a b))
+@main = a
+& @add ~ (#123 (#100 a))
 
-@main = R
-  & @add ~ (#123 (#100 R))

examples/machine_u32/num_match.hvmc

@@ -1,6 +1,4 @@
-@pred = (?<(#0 (x x)) R> R)
-
-@main
-  = R
-  & @pred ~ (#10 R)
+@main = a
+& @pred ~ (#10 a)
+@pred = (?<(#0 (a a)) b> b)
 

examples/sort/bitonic/bitonic_sort_ctr.hvmc

@@ -1 +0,0 @@
-// constructors not implemented in HVM2 yet!

examples/sort/bitonic/bitonic_sort_lam.hvm1

@@ -52,4 +52,4 @@ Sum = λa
   let a_node = λa0 λa1 (+ ((Sum) a0) ((Sum) a1))
   (a a_leaf a_node)
 
-Main = ((Sum) ((Sort) ((Rev) ((Gen) 18 0)) 0))
+Main = ((Sum) ((Sort) ((Rev) ((Gen) 15 0)) 0))

examples/sort/bitonic/bitonic_sort_lam.hvm2

@@ -1,4 +1,5 @@
-data Tree = (Leaf x) | (Node x0 x1)
+Leaf = @x @Leaf @Node (Leaf x)
+Node = @x0 @x1 @Leaf @Node (Node x0 x1)
 
 swap = λn match n {
   0: λx0 λx1 (Node x0 x1)
@@ -54,4 +55,4 @@ sum = λa
   let a_node = λa0 λa1 (+ (sum a0) (sum a1))
   (a a_leaf a_node)
 
-main = (sum (sort (rev (gen 18 0)) 0))
+main = (sum (sort (rev (gen 10 0)) 0))