Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add ana and ana_action tests #9

Draft
wants to merge 17 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 16 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1 +1,4 @@
_build
/_build/

.DS_Store
node_modules/
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ clean:
dune clean

deps:
opam install dune reason incr_dom ocaml-lsp-server
opam install dune reason incr_dom ocaml-lsp-server ppx_deriving

.PHONY: test
test:
Expand Down
2 changes: 1 addition & 1 deletion hazelnut/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@
(name hazelnut_lib)
(libraries core incr_dom monad_lib)
(preprocess
(pps ppx_jane)))
(pps ppx_jane ppx_deriving.show)))
8 changes: 4 additions & 4 deletions hazelnut/hazelnut.re
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,15 @@ let compare_string = String.compare;
let compare_int = Int.compare;

module Htyp = {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Arrow(t, t)
| Num
| Hole;
};

module Hexp = {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Var(string)
| Lam(string, t)
Expand All @@ -26,15 +26,15 @@ module Hexp = {
};

module Ztyp = {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Cursor(Htyp.t)
| LArrow(t, Htyp.t)
| RArrow(Htyp.t, t);
};

module Zexp = {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Cursor(Hexp.t)
| Lam(string, t)
Expand Down
8 changes: 4 additions & 4 deletions hazelnut/hazelnut.rei
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
module Htyp: {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Arrow(t, t)
| Num
| Hole;
};

module Hexp: {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Var(string)
| Lam(string, t)
Expand All @@ -20,15 +20,15 @@ module Hexp: {
};

module Ztyp: {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Cursor(Htyp.t)
| LArrow(t, Htyp.t)
| RArrow(Htyp.t, t);
};

module Zexp: {
[@deriving (sexp, compare)]
[@deriving (sexp, compare, show({with_path: false}))]
type t =
| Cursor(Hexp.t)
| Lam(string, t)
Expand Down
68 changes: 68 additions & 0 deletions test/Test_ana.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
open Alcotest;
module Hazelnut = Hazelnut_lib.Hazelnut;

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

let test_asubsume_1 = () => {
let ctx: typctx = TypCtx.empty;
let he: Hazelnut.Hexp.t = Lit(1);
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = false;
check(bool, "same bool", given, expected);
};

let test_asubsume_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let he: Hazelnut.Hexp.t = Var("x");
let ht: Hazelnut.Htyp.t = Num;
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = true;
check(bool, "same bool", given, expected);
};

let test_asubsume_3 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num));
let he: Hazelnut.Hexp.t = Var("x");
let ht: Hazelnut.Htyp.t = Hole;
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = true;
check(bool, "same bool", given, expected);
};

let test_alam_1 = () => {
let ctx: typctx = TypCtx.empty;
let he: Hazelnut.Hexp.t = Lam("x", Plus(Lit(1), Lit(2)));
let ht: Hazelnut.Htyp.t = Arrow(Arrow(Num, Num), Num);
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = true;
check(bool, "same bool", given, expected);
};

let test_alam_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let he: Hazelnut.Hexp.t = Lam("f", Plus(Var("x"), Lit(2)));
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = true;
check(bool, "same bool", given, expected);
};

let test_alam_3 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num));
let he: Hazelnut.Hexp.t = Lam("f", Plus(Var("x"), Lit(2)));
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: bool = Hazelnut.ana(ctx, he, ht);
let expected: bool = false;
check(bool, "same bool", given, expected);
};

let ana_tests = [
("test_asubsume_1", `Quick, test_asubsume_1),
("test_asubsume_2", `Quick, test_asubsume_2),
("test_asubsume_3", `Quick, test_asubsume_3),
("test_alam_1", `Quick, test_alam_1),
("test_alam_2", `Quick, test_alam_2),
("test_alam_3", `Quick, test_alam_3),
];
212 changes: 212 additions & 0 deletions test/Test_ana_action.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,212 @@
open Alcotest;
open Test_interface;
module Hazelnut = Hazelnut_lib.Hazelnut;

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

let test_aamove_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(Lam("f", Plus(Lit(1), Lit(2))));
let a: Hazelnut.Action.t = Move(Child(One));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(Lam("f", Cursor(Plus(Lit(1), Lit(2)))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aamove_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let ze: Hazelnut.Zexp.t = Cursor(Ap(Lam("f", Lit(1)), Var("x")));
let a: Hazelnut.Action.t = Move(Child(Two));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(RAp(Lam("f", Lit(1)), Cursor(Var("x"))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aamove_3 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t =
RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num)));
let a: Hazelnut.Action.t = Move(Parent);
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(Cursor(Asc(Lam("f", Lit(1)), Arrow(Num, Num))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aadel_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t =
RAsc(Lam("f", Lit(1)), Cursor(Arrow(Num, Num)));
let a: Hazelnut.Action.t = Del;
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(RAsc(Lam("f", Lit(1)), Cursor(Hole)));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aadel_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let ze: Hazelnut.Zexp.t =
RAsc(Lam("f", Plus(Lit(1), Var("x"))), RArrow(Num, Cursor(Num)));
let a: Hazelnut.Action.t = Del;
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(
RAsc(Lam("f", Plus(Lit(1), Var("x"))), RArrow(Num, Cursor(Hole))),
);
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconasc_1 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let ze: Hazelnut.Zexp.t = Cursor(Var("x"));
let a: Hazelnut.Action.t = Construct(Asc);
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(RAsc(Var("x"), Cursor(Num)));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconasc_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num));
let ze: Hazelnut.Zexp.t = Cursor(Var("x"));
let a: Hazelnut.Action.t = Construct(Asc);
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(RAsc(Var("x"), Cursor(Arrow(Num, Num))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconvar_1 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Arrow(Num, Num));
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Var("x"));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(NEHole(Cursor(Var("x"))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconvar_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Var("x"));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(Cursor(Var("x")));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconlam1_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lam("x"));
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(Lam("x", Cursor(EHole)));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconlam1_2 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lam("x"));
let ht: Hazelnut.Htyp.t = Arrow(Hole, Hole);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(Lam("x", Cursor(EHole)));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconlam2_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lam("x"));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(NEHole(RAsc(Lam("x", EHole), LArrow(Cursor(Hole), Hole))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconlam2_2 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lam("y"));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(NEHole(RAsc(Lam("y", EHole), LArrow(Cursor(Hole), Hole))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconnumlit_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lit(1));
let ht: Hazelnut.Htyp.t = Arrow(Num, Num);
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(NEHole(Cursor(Lit(1))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aaconnumlit_2 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(EHole);
let a: Hazelnut.Action.t = Construct(Lit(-1));
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = Some(Cursor(Lit(-1)));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aafinish_1 = () => {
let ctx: typctx = TypCtx.empty;
let ze: Hazelnut.Zexp.t = Cursor(NEHole(Plus(Lit(1), Lit(1))));
let a: Hazelnut.Action.t = Finish;
let ht: Hazelnut.Htyp.t = Num;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) =
Some(Cursor(Plus(Lit(1), Lit(1))));
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let test_aafinish_2 = () => {
let ctx: typctx = TypCtx.singleton("x", Hazelnut.Htyp.Num);
let ze: Hazelnut.Zexp.t =
Cursor(NEHole(NEHole(Lam("f", Plus(Var("x"), Var("x"))))));
let a: Hazelnut.Action.t = Finish;
let ht: Hazelnut.Htyp.t = Hole;
let given: option(Hazelnut.Zexp.t) = Hazelnut.ana_action(ctx, ze, a, ht);
let expected: option(Hazelnut.Zexp.t) = None;
check(zexp_typ, "same Hazelnut.Zexp.t", given, expected);
};

let ana_action_tests = [
("test_aamove_1", `Quick, test_aamove_1),
("test_aamove_2", `Quick, test_aamove_2),
("test_aamove_3", `Quick, test_aamove_3),
("test_aadel_1", `Quick, test_aadel_1),
("test_aadel_2", `Quick, test_aadel_2),
("test_aaconasc_1", `Quick, test_aaconasc_1),
("test_aaconasc_2", `Quick, test_aaconasc_2),
("test_aaconvar_1", `Quick, test_aaconvar_1),
("test_aaconvar_2", `Quick, test_aaconvar_2),
("test_aaconlam1_1", `Quick, test_aaconlam1_1),
("test_aaconlam1_2", `Quick, test_aaconlam1_2),
("test_aaconlam2_1", `Quick, test_aaconlam2_1),
("test_aaconlam2_2", `Quick, test_aaconlam2_2),
("test_aaconnumlit_1", `Quick, test_aaconnumlit_1),
("test_aaconnumlit_2", `Quick, test_aaconnumlit_2),
("test_aafinish_1", `Quick, test_aafinish_1),
("test_aafinish_2", `Quick, test_aafinish_2),
];
Loading