[sc-543] Add hvml test on example programs

examples/all_tree.hvm

@@ -0,0 +1,18 @@
+data Bool = True | False
+
+data Tree
+  = (Node lft rgt)
+  | (Leaf val)
+
+and True True = True
+and _    _    = False
+
+all (Node lft rgt) = (and (all lft) (all rgt))
+all (Leaf val)     = val
+
+main = (all (gen 8))
+
+gen = λn switch n {
+  0: (Leaf True)
+  _: let tree = (gen n-1); (Node tree tree)
+}

examples/alloc_small_tree.hvm

@@ -0,0 +1,18 @@
+T = λt λf t
+F = λt λf f
+And = λpλq (p q F)
+
+Z = λs λz (z)
+S = λn λs λz (s n)
+
+Add = λa λb (a (S b))
+Mul = λa λb λf (a (b f))
+Pow = λa λb (a (Mul b) (S Z))
+
+Node = λa λb λn λl (n a b)
+Leaf = λn λl l
+
+Alloc = λn (n (λp (Node (Alloc p) (Alloc p))) Leaf)
+Destroy = λt (t (λaλb (And (Destroy a) (Destroy b))) T)
+
+Main = (Destroy (Alloc (Pow (S (S Z)) (S (S (S (S Z)))))))

examples/example.hvm

@@ -19,8 +19,8 @@
 
 // You can use 'switch' to pattern match native numbers
 // The `_` arm binds the `scrutinee`-1 variable to the the value of the number -1
-(Num.pred) = λn 
-  switch n { 
+(Num.pred) = λn
+  switch n {
     0: 0
     _: n-1
   }
@@ -52,8 +52,9 @@ data Boxed = (Box val)
 (Box.map (Box val) f) = (Box (f val))
 
 (Box.unbox) = λbox
-  let (Box val) = box
-  val
+  match box {
+    Box: box.val
+  }
 
 // Use tuples to store two values together without needing to create a new data type
 (Tuple.new fst snd) =
@@ -71,7 +72,7 @@ data Boxed = (Box val)
 // You can execute a program in HVM with "cargo run -- --run <path to file>"
 // Other options are "--check" (the default mode) to just see if the file is well formed
 // and "--compile" to output hvm-core code.
-(main) = 
+(main) =
   let tup = (Tuple.new None (Num.pred 5))
 
   let fst = (Tuple.fst tup)

examples/fib.hvm

@@ -0,0 +1,11 @@
+add = λa λb (+ a b)
+
+fib = λx switch x {
+  0: 1
+  _: let p = x-1; switch p {
+    0: 1
+    _: (+ (fib p) (fib p-1))
+  }
+}
+
+main = (fib 30)

examples/gen_tree_kind2.hvm

@@ -0,0 +1,17 @@
+_Char = 0
+_List = λ_T 0
+_List.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
+_List.nil = λ_P λ_cons λ_nil _nil
+_Nat = 0
+_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
+_Nat.zero = λ_P λ_succ λ_zero _zero
+_String = (_List _Char)
+_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
+_String.nil = λ_P λ_cons λ_nil _nil
+_Tree = λ_A 0
+_Tree.gen = λ_n λ_x switch _n = _n { 0: _Tree.leaf _: let _n-1 = _n-1 (((_Tree.node _x) ((_Tree.gen _n-1) (+ (* _x 2) 1))) ((_Tree.gen _n-1) (+ (* _x 2) 2))) }
+_Tree.leaf = λ_P λ_node λ_leaf _leaf
+_Tree.node = λ_val λ_lft λ_rgt λ_P λ_node λ_leaf (((_node _val) _lft) _rgt)
+_main = ((_Tree.gen 8) 2)
+
+main = _main

examples/neg_fusion.hvm

@@ -0,0 +1,24 @@
+// size = 1 << 8
+
+Mul = λn λm λs (n (m s))
+
+// Church nat
+C2 = λf λx (f (f x))
+
+// Church powers of two
+P2 = (Mul C2 C2) // 4
+P3 = (Mul C2 P2) // 8
+P4 = (Mul C2 P3) // 16
+P5 = (Mul C2 P4) // 32
+P6 = (Mul C2 P5) // 64
+P7 = (Mul C2 P6) // 128
+P8 = (Mul C2 P7) // 256
+
+// Booleans
+True = λt λf t
+False = λt λf f
+Not = λb ((b False) True)
+Neg = λb λt λf (b f t)
+
+// Negates 'true' 256 times: 'neg' is faster than 'not' because it fuses
+Main = (P8 Neg True)

tests/golden_tests.rs

@@ -418,3 +418,36 @@ fn io() {
     }),
   ])
 }
+
+#[test]
+fn examples() -> Result<(), Diagnostics> {
+  let examples_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("examples");
+
+  for entry in WalkDir::new(examples_path)
+    .min_depth(1)
+    .into_iter()
+    .filter_map(|e| e.ok())
+    .filter(|e| e.path().extension().map_or(false, |ext| ext == "hvm"))
+  {
+    let path = entry.path();
+    eprintln!("Testing {}", path.display());
+    let code = std::fs::read_to_string(path).map_err(|e| e.to_string())?;
+
+    let book = do_parse_book(&code, path).unwrap();
+    let mut compile_opts = CompileOpts::default_strict();
+    compile_opts.linearize_matches = hvml::OptLevel::Extra;
+    let diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let (res, _) = run_book(book, None, RunOpts::default(), compile_opts, diagnostics_cfg, None)?;
+
+    let mut settings = insta::Settings::clone_current();
+    settings.set_prepend_module_to_snapshot(false);
+    settings.set_omit_expression(true);
+    settings.set_input_file(path);
+
+    settings.bind(|| {
+      assert_snapshot!(format!("examples__{}", path.file_name().unwrap().to_str().unwrap()), res);
+    });
+  }
+
+  Ok(())
+}

tests/snapshots/examples__all_tree.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/examples/all_tree.hvm
+---
+True

tests/snapshots/examples__alloc_small_tree.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/examples/alloc_small_tree.hvm
+---
+λa λ* a

tests/snapshots/examples__callcc.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/callcc.hvm
+---
+52

tests/snapshots/examples__example.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/example.hvm
+---
+8

tests/snapshots/examples__fib.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/examples/fib.hvm
+---
+1346269

tests/snapshots/examples__fusing_add.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/fusing_add.hvm
+---
+λa λb λ* (b λc λ* (c a))

tests/snapshots/examples__fusing_not.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/fusing_not.hvm
+---
+λa λb λc (a b c)

tests/snapshots/examples__gen_tree_kind2.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/examples/gen_tree_kind2.hvm
+---
+λ* λa λ* (a 2 λ* λb λ* (b 5 λ* λc λ* (c 11 λ* λd λ* (d 23 λ* λe λ* (e 47 λ* λf λ* (f 95 λ* λg λ* (g 191 λ* λh λ* (h 383 λ* λ* λi i λ* λ* λj j) λ* λk λ* (k 384 λ* λ* λl l λ* λ* λm m)) λ* λn λ* (n 192 λ* λo λ* (o 385 λ* λ* λp p λ* λ* λq q) λ* λr λ* (r 386 λ* λ* λs s λ* λ* λt t))) λ* λu λ* (u 96 λ* λv λ* (v 193 λ* λw λ* (w 387 λ* λ* λx x λ* λ* λy y) λ* λz λ* (z 388 λ* λ* λab ab λ* λ* λbb bb)) λ* λcb λ* (cb 194 λ* λdb λ* (db 389 λ* λ* λeb eb λ* λ* λfb fb) λ* λgb λ* (gb 390 λ* λ* λhb hb λ* λ* λib ib)))) λ* λjb λ* (jb 48 λ* λkb λ* (kb 97 λ* λlb λ* (lb 195 λ* λmb λ* (mb 391 λ* λ* λnb nb λ* λ* λob ob) λ* λpb λ* (pb 392 λ* λ* λqb qb λ* λ* λrb rb)) λ* λsb λ* (sb 196 λ* λtb λ* (tb 393 λ* λ* λub ub λ* λ* λvb vb) λ* λwb λ* (wb 394 λ* λ* λxb xb λ* λ* λyb yb))) λ* λzb λ* (zb 98 λ* λac λ* (ac 197 λ* λbc λ* (bc 395 λ* λ* λcc cc λ* λ* λdc dc) λ* λec λ* (ec 396 λ* λ* λfc fc λ* λ* λgc gc)) λ* λhc λ* (hc 198 λ* λic λ* (ic 397 λ* λ* λjc jc λ* λ* λkc kc) λ* λlc λ* (lc 398 λ* λ* λmc mc λ* λ* λnc nc))))) λ* λoc λ* (oc 24 λ* λpc λ* (pc 49 λ* λqc λ* (qc 99 λ* λrc λ* (rc 199 λ* λsc λ* (sc 399 λ* λ* λtc tc λ* λ* λuc uc) λ* λvc λ* (vc 400 λ* λ* λwc wc λ* λ* λxc xc)) λ* λyc λ* (yc 200 λ* λzc λ* (zc 401 λ* λ* λad ad λ* λ* λbd bd) λ* λcd λ* (cd 402 λ* λ* λdd dd λ* λ* λed ed))) λ* λfd λ* (fd 100 λ* λgd λ* (gd 201 λ* λhd λ* (hd 403 λ* λ* λid id λ* λ* λjd jd) λ* λkd λ* (kd 404 λ* λ* λld ld λ* λ* λmd md)) λ* λnd λ* (nd 202 λ* λod λ* (od 405 λ* λ* λpd pd λ* λ* λqd qd) λ* λrd λ* (rd 406 λ* λ* λsd sd λ* λ* λtd td)))) λ* λud λ* (ud 50 λ* λvd λ* (vd 101 λ* λwd λ* (wd 203 λ* λxd λ* (xd 407 λ* λ* λyd yd λ* λ* λzd zd) λ* λae λ* (ae 408 λ* λ* λbe be λ* λ* λce ce)) λ* λde λ* (de 204 λ* λee λ* (ee 409 λ* λ* λfe fe λ* λ* λge ge) λ* λhe λ* (he 410 λ* λ* λie ie λ* λ* λje je))) λ* λke λ* (ke 102 λ* λle λ* (le 205 λ* λme λ* (me 411 λ* λ* λne ne λ* λ* λoe oe) λ* λpe λ* (pe 412 λ* λ* λqe qe λ* λ* λre re)) λ* λse λ* (se 206 λ* λte λ* (te 413 λ* λ* λue ue λ* λ* λve ve) λ* λwe λ* (we 414 λ* λ* λxe xe λ* λ* λye ye)))))) λ* λze λ* (ze 12 λ* λaf λ* (af 25 λ* λbf λ* (bf 51 λ* λcf λ* (cf 103 λ* λdf λ* (df 207 λ* λef λ* (ef 415 λ* λ* λff ff λ* λ* λgf gf) λ* λhf λ* (hf 416 λ* λ* λif if λ* λ* λjf jf)) λ* λkf λ* (kf 208 λ* λlf λ* (lf 417 λ* λ* λmf mf λ* λ* λnf nf) λ* λof λ* (of 418 λ* λ* λpf pf λ* λ* λqf qf))) λ* λrf λ* (rf 104 λ* λsf λ* (sf 209 λ* λtf λ* (tf 419 λ* λ* λuf uf λ* λ* λvf vf) λ* λwf λ* (wf 420 λ* λ* λxf xf λ* λ* λyf yf)) λ* λzf λ* (zf 210 λ* λag λ* (ag 421 λ* λ* λbg bg λ* λ* λcg cg) λ* λdg λ* (dg 422 λ* λ* λeg eg λ* λ* λfg fg)))) λ* λgg λ* (gg 52 λ* λhg λ* (hg 105 λ* λig λ* (ig 211 λ* λjg λ* (jg 423 λ* λ* λkg kg λ* λ* λlg lg) λ* λmg λ* (mg 424 λ* λ* λng ng λ* λ* λog og)) λ* λpg λ* (pg 212 λ* λqg λ* (qg 425 λ* λ* λrg rg λ* λ* λsg sg) λ* λtg λ* (tg 426 λ* λ* λug ug λ* λ* λvg vg))) λ* λwg λ* (wg 106 λ* λxg λ* (xg 213 λ* λyg λ* (yg 427 λ* λ* λzg zg λ* λ* λah ah) λ* λbh λ* (bh 428 λ* λ* λch ch λ* λ* λdh dh)) λ* λeh λ* (eh 214 λ* λfh λ* (fh 429 λ* λ* λgh gh λ* λ* λhh hh) λ* λih λ* (ih 430 λ* λ* λjh jh λ* λ* λkh kh))))) λ* λlh λ* (lh 26 λ* λmh λ* (mh 53 λ* λnh λ* (nh 107 λ* λoh λ* (oh 215 λ* λph λ* (ph 431 λ* λ* λqh qh λ* λ* λrh rh) λ* λsh λ* (sh 432 λ* λ* λth th λ* λ* λuh uh)) λ* λvh λ* (vh 216 λ* λwh λ* (wh 433 λ* λ* λxh xh λ* λ* λyh yh) λ* λzh λ* (zh 434 λ* λ* λai ai λ* λ* λbi bi))) λ* λci λ* (ci 108 λ* λdi λ* (di 217 λ* λei λ* (ei 435 λ* λ* λfi fi λ* λ* λgi gi) λ* λhi λ* (hi 436 λ* λ* λii ii λ* λ* λji ji)) λ* λki λ* (ki 218 λ* λli λ* (li 437 λ* λ* λmi mi λ* λ* λni ni) λ* λoi λ* (oi 438 λ* λ* λpi pi λ* λ* λqi qi)))) λ* λri λ* (ri 54 λ* λsi λ* (si 109 λ* λti λ* (ti 219 λ* λui λ* (ui 439 λ* λ* λvi vi λ* λ* λwi wi) λ* λxi λ* (xi 440 λ* λ* λyi yi λ* λ* λzi zi)) λ* λaj λ* (aj 220 λ* λbj λ* (bj 441 λ* λ* λcj cj λ* λ* λdj dj) λ* λej λ* (ej 442 λ* λ* λfj fj λ* λ* λgj gj))) λ* λhj λ* (hj 110 λ* λij λ* (ij 221 λ* λjj λ* (jj 443 λ* λ* λkj kj λ* λ* λlj lj) λ* λmj λ* (mj 444 λ* λ* λnj nj λ* λ* λoj oj)) λ* λpj λ* (pj 222 λ* λqj λ* (qj 445 λ* λ* λrj rj λ* λ* λsj sj) λ* λtj λ* (tj 446 λ* λ* λuj uj λ* λ* λvj vj))))))) λ* λwj λ* (wj 6 λ* λxj λ* (xj 13 λ* λyj λ* (yj 27 λ* λzj λ* (zj 55 λ* λak λ* (ak 111 λ* λbk λ* (bk 223 λ* λck λ* (ck 447 λ* λ* λdk dk λ* λ* λek ek) λ* λfk λ* (fk 448 λ* λ* λgk gk λ* λ* λhk hk)) λ* λik λ* (ik 224 λ* λjk λ* (jk 449 λ* λ* λkk kk λ* λ* λlk lk) λ* λmk λ* (mk 450 λ* λ* λnk nk λ* λ* λok ok))) λ* λpk λ* (pk 112 λ* λqk λ* (qk 225 λ* λrk λ* (rk 451 λ* λ* λsk sk λ* λ* λtk tk) λ* λuk λ* (uk 452 λ* λ* λvk vk λ* λ* λwk wk)) λ* λxk λ* (xk 226 λ* λyk λ* (yk 453 λ* λ* λzk zk λ* λ* λal al) λ* λbl λ* (bl 454 λ* λ* λcl cl λ* λ* λdl dl)))) λ* λel λ* (el 56 λ* λfl λ* (fl 113 λ* λgl λ* (gl 227 λ* λhl λ* (hl 455 λ* λ* λil il λ* λ* λjl jl) λ* λkl λ* (kl 456 λ* λ* λll ll λ* λ* λml ml)) λ* λnl λ* (nl 228 λ* λol λ* (ol 457 λ* λ* λpl pl λ* λ* λql ql) λ* λrl λ* (rl 458 λ* λ* λsl sl λ* λ* λtl tl))) λ* λul λ* (ul 114 λ* λvl λ* (vl 229 λ* λwl λ* (wl 459 λ* λ* λxl xl λ* λ* λyl yl) λ* λzl λ* (zl 460 λ* λ* λam am λ* λ* λbm bm)) λ* λcm λ* (cm 230 λ* λdm λ* (dm 461 λ* λ* λem em λ* λ* λfm fm) λ* λgm λ* (gm 462 λ* λ* λhm hm λ* λ* λim im))))) λ* λjm λ* (jm 28 λ* λkm λ* (km 57 λ* λlm λ* (lm 115 λ* λmm λ* (mm 231 λ* λnm λ* (nm 463 λ* λ* λom om λ* λ* λpm pm) λ* λqm λ* (qm 464 λ* λ* λrm rm λ* λ* λsm sm)) λ* λtm λ* (tm 232 λ* λum λ* (um 465 λ* λ* λvm vm λ* λ* λwm wm) λ* λxm λ* (xm 466 λ* λ* λym ym λ* λ* λzm zm))) λ* λan λ* (an 116 λ* λbn λ* (bn 233 λ* λcn λ* (cn 467 λ* λ* λdn dn λ* λ* λen en) λ* λfn λ* (fn 468 λ* λ* λgn gn λ* λ* λhn hn)) λ* λin λ* (in 234 λ* λjn λ* (jn 469 λ* λ* λkn kn λ* λ* λln ln) λ* λmn λ* (mn 470 λ* λ* λnn nn λ* λ* λon on)))) λ* λpn λ* (pn 58 λ* λqn λ* (qn 117 λ* λrn λ* (rn 235 λ* λsn λ* (sn 471 λ* λ* λtn tn λ* λ* λun un) λ* λvn λ* (vn 472 λ* λ* λwn wn λ* λ* λxn xn)) λ* λyn λ* (yn 236 λ* λzn λ* (zn 473 λ* λ* λao ao λ* λ* λbo bo) λ* λco λ* (co 474 λ* λ* λdo do λ* λ* λeo eo))) λ* λfo λ* (fo 118 λ* λgo λ* (go 237 λ* λho λ* (ho 475 λ* λ* λio io λ* λ* λjo jo) λ* λko λ* (ko 476 λ* λ* λlo lo λ* λ* λmo mo)) λ* λno λ* (no 238 λ* λoo λ* (oo 477 λ* λ* λpo po λ* λ* λqo qo) λ* λro λ* (ro 478 λ* λ* λso so λ* λ* λto to)))))) λ* λuo λ* (uo 14 λ* λvo λ* (vo 29 λ* λwo λ* (wo 59 λ* λxo λ* (xo 119 λ* λyo λ* (yo 239 λ* λzo λ* (zo 479 λ* λ* λap ap λ* λ* λbp bp) λ* λcp λ* (cp 480 λ* λ* λdp dp λ* λ* λep ep)) λ* λfp λ* (fp 240 λ* λgp λ* (gp 481 λ* λ* λhp hp λ* λ* λip ip) λ* λjp λ* (jp 482 λ* λ* λkp kp λ* λ* λlp lp))) λ* λmp λ* (mp 120 λ* λnp λ* (np 241 λ* λop λ* (op 483 λ* λ* λpp pp λ* λ* λqp qp) λ* λrp λ* (rp 484 λ* λ* λsp sp λ* λ* λtp tp)) λ* λup λ* (up 242 λ* λvp λ* (vp 485 λ* λ* λwp wp λ* λ* λxp xp) λ* λyp λ* (yp 486 λ* λ* λzp zp λ* λ* λaq aq)))) λ* λbq λ* (bq 60 λ* λcq λ* (cq 121 λ* λdq λ* (dq 243 λ* λeq λ* (eq 487 λ* λ* λfq fq λ* λ* λgq gq) λ* λhq λ* (hq 488 λ* λ* λiq iq λ* λ* λjq jq)) λ* λkq λ* (kq 244 λ* λlq λ* (lq 489 λ* λ* λmq mq λ* λ* λnq nq) λ* λoq λ* (oq 490 λ* λ* λpq pq λ* λ* λqq qq))) λ* λrq λ* (rq 122 λ* λsq λ* (sq 245 λ* λtq λ* (tq 491 λ* λ* λuq uq λ* λ* λvq vq) λ* λwq λ* (wq 492 λ* λ* λxq xq λ* λ* λyq yq)) λ* λzq λ* (zq 246 λ* λar λ* (ar 493 λ* λ* λbr br λ* λ* λcr cr) λ* λdr λ* (dr 494 λ* λ* λer er λ* λ* λfr fr))))) λ* λgr λ* (gr 30 λ* λhr λ* (hr 61 λ* λir λ* (ir 123 λ* λjr λ* (jr 247 λ* λkr λ* (kr 495 λ* λ* λlr lr λ* λ* λmr mr) λ* λnr λ* (nr 496 λ* λ* λor or λ* λ* λpr pr)) λ* λqr λ* (qr 248 λ* λrr λ* (rr 497 λ* λ* λsr sr λ* λ* λtr tr) λ* λur λ* (ur 498 λ* λ* λvr vr λ* λ* λwr wr))) λ* λxr λ* (xr 124 λ* λyr λ* (yr 249 λ* λzr λ* (zr 499 λ* λ* λas as λ* λ* λbs bs) λ* λcs λ* (cs 500 λ* λ* λds ds λ* λ* λes es)) λ* λfs λ* (fs 250 λ* λgs λ* (gs 501 λ* λ* λhs hs λ* λ* λis is) λ* λjs λ* (js 502 λ* λ* λks ks λ* λ* λls ls)))) λ* λms λ* (ms 62 λ* λns λ* (ns 125 λ* λos λ* (os 251 λ* λps λ* (ps 503 λ* λ* λqs qs λ* λ* λrs rs) λ* λss λ* (ss 504 λ* λ* λts ts λ* λ* λus us)) λ* λvs λ* (vs 252 λ* λws λ* (ws 505 λ* λ* λxs xs λ* λ* λys ys) λ* λzs λ* (zs 506 λ* λ* λat at λ* λ* λbt bt))) λ* λct λ* (ct 126 λ* λdt λ* (dt 253 λ* λet λ* (et 507 λ* λ* λft ft λ* λ* λgt gt) λ* λht λ* (ht 508 λ* λ* λit it λ* λ* λjt jt)) λ* λkt λ* (kt 254 λ* λlt λ* (lt 509 λ* λ* λmt mt λ* λ* λnt nt) λ* λot λ* (ot 510 λ* λ* λpt pt λ* λ* λqt qt))))))))

tests/snapshots/examples__neg_fusion.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/examples/neg_fusion.hvm
+---
+λa λ* a