Test_sample.re

open Alcotest;
open Test_interface;
module Hazelnut = Hazelnut_lib.Hazelnut;

module TypCtx = Map.Make(String);
type typctx = Hazelnut.TypCtx.t(Hazelnut.Htyp.t);

// =====================================================================
// End-to-end sample: build the function  λx:Num. x + 1  at the empty
// hole cursor using only Zexp.Cursor(EHole) as the starting state, and
// check that the final cursor-erased expression matches the expected
// H-expression.  This is a miniature analogue of the "walk through"
// examples from Hazelnut 2017, §2, specialised to this calculus.
//
// The expression we want to build:
//
//     ▶LM◀
//   → λx:▶Hole◀.LM
//   → λx:▶Num◀.LM
//   → λx:Num.▶LM◀
//   → λx:Num.▶x◀
//   → λx:Num.x+▶LM◀
//   → λx:Num.x+▶1◀
// =====================================================================

let steps: list((Hazelnut.Action.t, Hazelnut.Zexp.t)) = [
  // 1. Construct a λ around the hole.  The cursor ends up on the
  //    annotation; the exact cursor position is implementation-defined,
  //    so we only check erasures from here on.
  (Construct(Lam("x")), LLam("x", Cursor(Hole), EHole)),
  // 2. Construct Num on the annotation: λx:▶Num◀.LM
  (Construct(Num), LLam("x", Cursor(Num), EHole)),
  // 3. Move the cursor to the body: λx:Num.▶LM◀
  (Move(Parent), Cursor(Lam("x", Num, EHole))),
  (Move(Child(Two)), RLam("x", Num, Cursor(EHole))),
  // 4. Construct the variable reference.
  (Construct(Var("x")), RLam("x", Num, Cursor(Var("x")))),
  // 5. Construct a Plus: λx:Num. x + ▶LM◀
  (Construct(Plus), RLam("x", Num, RPlus(Var("x"), Cursor(EHole)))),
  // 6. Construct the number literal 1.
  (
    Construct(NumLit(1)),
    RLam("x", Num, RPlus(Var("x"), Cursor(NumLit(1)))),
  ),
];

let test_build_incr = () => {
  let start: Hazelnut.Zexp.t = Cursor(EHole);
  let (_, final_ze) =
    List.fold_left(
      ((ze, _), (a, expected)) => {
        let ze' = Hazelnut.syn_action(ze, a);
        check(
          zexp_typ,
          "step produces expected zipper",
          ze',
          expected,
        );
        (ze', expected);
      },
      (start, start),
      steps,
    );
  let erased = Hazelnut.erase_exp(final_ze);
  let expected: Hazelnut.Hexp.t =
    Lam("x", Num, Plus(Var("x"), NumLit(1)));
  check(hexp_typ, "final erasure = λx:Num.x+1", erased, expected);

  // After building, marking the result should leave no marks and
  // should synthesize Num → Num.
  let (em, t) = Hazelnut.mark_syn(TypCtx.empty, erased);
  check(
    hexp_typ,
    "final expression is markless",
    em,
    expected,
  );
  check(
    htyp_typ,
    "final expression synthesises Num→Num",
    t,
    Arrow(Num, Num),
  );
};

// End-to-end example of a free-variable error being caught by the
// marker.  We try to build  x + 1  without introducing a binder for x;
// after re-marking, the x should be wrapped in a Mark(_, Free).
let test_free_variable_flow = () => {
  let actions: list(Hazelnut.Action.t) = [
    Construct(Var("x")),
    Construct(Plus),
    Construct(NumLit(1)),
  ];
  let final_ze =
    List.fold_left(
      (ze, a) => Hazelnut.syn_action(ze, a),
      Hazelnut.Zexp.Cursor(EHole),
      actions,
    );
  let erased = Hazelnut.erase_exp(final_ze);
  check(
    hexp_typ,
    "raw erasure = x + 1",
    erased,
    Plus(Var("x"), NumLit(1)),
  );
  let (em, t) = Hazelnut.mark_syn(TypCtx.empty, erased);
  check(
    hexp_typ,
    "x gets Free mark after re-marking",
    em,
    Plus(Mark(Var("x"), Free), NumLit(1)),
  );
  check(htyp_typ, "Plus synthesises Num", t, Num);
};

let sample_tests = [
  ("build_incr", `Quick, test_build_incr),
  ("free_variable_flow", `Quick, test_free_variable_flow),
];