Merge pull request #8 from hazelgrove/feature-test

#7: Proof of concept for the test suite
hazelgrove · Feb 22, 2024 · 6f271ea · 6f271ea
2 parents fbc3018 + 79c4a21
commit 6f271ea
Show file tree

Hide file tree

Showing 10 changed files with 560 additions and 169 deletions.
diff --git a/Makefile b/Makefile
@@ -18,3 +18,7 @@ clean:
 
 deps:
 	opam install dune reason incr_dom ocaml-lsp-server
+
+.PHONY: test
+test:
+	dune test
diff --git a/README.md b/README.md
@@ -71,6 +71,11 @@ To erase the build:
 make clean
 ```
 
+To test your implementation:
+```sh
+make test
+```
+
 ## Implementing Hazelnut
 
 Now it's your turn to implement Hazelnut!
@@ -112,6 +117,7 @@ If anything unexpected happens, a warning will appear at the bottom. Here's what
 | Unimplemented     | You called upon an operation that you haven't implemented yet.                                                                                         |
 | Theorem violation | Your implementation has a bug that caused it to violate a Hazelnut metatheorem. Note: This won't catch every metatheorem violation, only some of them. |
 
+
 ## Using the Maybe Monad
 
 Have you ever written code that looks like this?

diff --git a/hazelnut/hazelnut.re b/hazelnut/hazelnut.re
@@ -4,84 +4,100 @@ open Sexplib.Std;
 let compare_string = String.compare;
 let compare_int = Int.compare;
 
-[@deriving (sexp, compare)]
-type htyp =
-  | Arrow(htyp, htyp)
-  | Num
-  | Hole;
-
-[@deriving (sexp, compare)]
-type hexp =
-  | Var(string)
-  | Lam(string, hexp)
-  | Ap(hexp, hexp)
-  | Lit(int)
-  | Plus(hexp, hexp)
-  | Asc(hexp, htyp)
-  | EHole
-  | NEHole(hexp);
-
-[@deriving (sexp, compare)]
-type ztyp =
-  | Cursor(htyp)
-  | LArrow(ztyp, htyp)
-  | RArrow(htyp, ztyp);
-
-[@deriving (sexp, compare)]
-type zexp =
-  | Cursor(hexp)
-  | Lam(string, zexp)
-  | LAp(zexp, hexp)
-  | RAp(hexp, zexp)
-  | LPlus(zexp, hexp)
-  | RPlus(hexp, zexp)
-  | LAsc(zexp, htyp)
-  | RAsc(hexp, ztyp)
-  | NEHole(zexp);
-
-[@deriving (sexp, compare)]
-type child =
-  | One
-  | Two;
-
-[@deriving (sexp, compare)]
-type dir =
-  | Child(child)
-  | Parent;
-
-[@deriving (sexp, compare)]
-type shape =
-  | Arrow
-  | Num
-  | Asc
-  | Var(string)
-  | Lam(string)
-  | Ap
-  | Lit(int)
-  | Plus
-  | NEHole;
-
-[@deriving (sexp, compare)]
-type action =
-  | Move(dir)
-  | Construct(shape)
-  | Del
-  | Finish;
+module Htyp = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Arrow(t, t)
+    | Num
+    | Hole;
+};
+
+module Hexp = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Var(string)
+    | Lam(string, t)
+    | Ap(t, t)
+    | Lit(int)
+    | Plus(t, t)
+    | Asc(t, Htyp.t)
+    | EHole
+    | NEHole(t);
+};
+
+module Ztyp = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Cursor(Htyp.t)
+    | LArrow(t, Htyp.t)
+    | RArrow(Htyp.t, t);
+};
+
+module Zexp = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Cursor(Hexp.t)
+    | Lam(string, t)
+    | LAp(t, Hexp.t)
+    | RAp(Hexp.t, t)
+    | LPlus(t, Hexp.t)
+    | RPlus(Hexp.t, t)
+    | LAsc(t, Htyp.t)
+    | RAsc(Hexp.t, Ztyp.t)
+    | NEHole(t);
+};
+
+module Child = {
+  [@deriving (sexp, compare)]
+  type t =
+    | One
+    | Two;
+};
+
+module Dir = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Child(Child.t)
+    | Parent;
+};
+
+module Shape = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Arrow
+    | Num
+    | Asc
+    | Var(string)
+    | Lam(string)
+    | Ap
+    | Lit(int)
+    | Plus
+    | NEHole;
+};
+
+module Action = {
+  [@deriving (sexp, compare)]
+  type t =
+    | Move(Dir.t)
+    | Construct(Shape.t)
+    | Del
+    | Finish;
+};
 
 module TypCtx = Map.Make(String);
-type typctx = TypCtx.t(htyp);
+type typctx = TypCtx.t(Htyp.t);
 
 exception Unimplemented;
 
-let erase_exp = (e: zexp): hexp => {
+let erase_exp = (e: Zexp.t): Hexp.t => {
   // Used to suppress unused variable warnings
   // Okay to remove
   let _ = e;
 
   raise(Unimplemented);
 };
 
-let syn = (ctx: typctx, e: hexp): option(htyp) => {
+let syn = (ctx: typctx, e: Hexp.t): option(Htyp.t) => {
   // Used to suppress unused variable warnings
   // Okay to remove
   let _ = ctx;
@@ -90,7 +106,7 @@ let syn = (ctx: typctx, e: hexp): option(htyp) => {
   raise(Unimplemented);
 }
 
-and ana = (ctx: typctx, e: hexp, t: htyp): bool => {
+and ana = (ctx: typctx, e: Hexp.t, t: Htyp.t): bool => {
   // Used to suppress unused variable warnings
   // Okay to remove
   let _ = ctx;
@@ -101,7 +117,8 @@ and ana = (ctx: typctx, e: hexp, t: htyp): bool => {
 };
 
 let syn_action =
-    (ctx: typctx, (e: zexp, t: htyp), a: action): option((zexp, htyp)) => {
+    (ctx: typctx, (e: Zexp.t, t: Htyp.t), a: Action.t)
+    : option((Zexp.t, Htyp.t)) => {
   // Used to suppress unused variable warnings
   // Okay to remove
   let _ = ctx;
@@ -112,7 +129,8 @@ let syn_action =
   raise(Unimplemented);
 }
 
-and ana_action = (ctx: typctx, e: zexp, a: action, t: htyp): option(zexp) => {
+and ana_action =
+    (ctx: typctx, e: Zexp.t, a: Action.t, t: Htyp.t): option(Zexp.t) => {
   // Used to suppress unused variable warnings
   // Okay to remove
   let _ = ctx;

diff --git a/hazelnut/hazelnut.rei b/hazelnut/hazelnut.rei
@@ -1,73 +1,91 @@
-[@deriving (sexp, compare)]
-type htyp =
-  | Arrow(htyp, htyp)
-  | Num
-  | Hole;
+module Htyp: {
+  [@deriving (sexp, compare)]
+  type t =
+    | Arrow(t, t)
+    | Num
+    | Hole;
+};
 
-[@deriving compare]
-type hexp =
-  | Var(string)
-  | Lam(string, hexp)
-  | Ap(hexp, hexp)
-  | Lit(int)
-  | Plus(hexp, hexp)
-  | Asc(hexp, htyp)
-  | EHole
-  | NEHole(hexp);
+module Hexp: {
+  [@deriving (sexp, compare)]
+  type t =
+    | Var(string)
+    | Lam(string, t)
+    | Ap(t, t)
+    | Lit(int)
+    | Plus(t, t)
+    | Asc(t, Htyp.t)
+    | EHole
+    | NEHole(t);
+};
 
-type ztyp =
-  | Cursor(htyp)
-  | LArrow(ztyp, htyp)
-  | RArrow(htyp, ztyp);
+module Ztyp: {
+  [@deriving (sexp, compare)]
+  type t =
+    | Cursor(Htyp.t)
+    | LArrow(t, Htyp.t)
+    | RArrow(Htyp.t, t);
+};
 
-[@deriving (sexp, compare)]
-type zexp =
-  | Cursor(hexp)
-  | Lam(string, zexp)
-  | LAp(zexp, hexp)
-  | RAp(hexp, zexp)
-  | LPlus(zexp, hexp)
-  | RPlus(hexp, zexp)
-  | LAsc(zexp, htyp)
-  | RAsc(hexp, ztyp)
-  | NEHole(zexp);
+module Zexp: {
+  [@deriving (sexp, compare)]
+  type t =
+    | Cursor(Hexp.t)
+    | Lam(string, t)
+    | LAp(t, Hexp.t)
+    | RAp(Hexp.t, t)
+    | LPlus(t, Hexp.t)
+    | RPlus(Hexp.t, t)
+    | LAsc(t, Htyp.t)
+    | RAsc(Hexp.t, Ztyp.t)
+    | NEHole(t);
+};
 
-type child =
-  | One
-  | Two;
+module Child: {
+  type t =
+    | One
+    | Two;
+};
 
-type dir =
-  | Child(child)
-  | Parent;
+module Dir: {
+  type t =
+    | Child(Child.t)
+    | Parent;
+};
 
-type shape =
-  | Arrow
-  | Num
-  | Asc
-  | Var(string)
-  | Lam(string)
-  | Ap
-  | Lit(int)
-  | Plus
-  | NEHole;
+module Shape: {
+  type t =
+    | Arrow
+    | Num
+    | Asc
+    | Var(string)
+    | Lam(string)
+    | Ap
+    | Lit(int)
+    | Plus
+    | NEHole;
+};
 
-[@deriving (sexp, compare)]
-type action =
-  | Move(dir)
-  | Construct(shape)
-  | Del
-  | Finish;
+module Action: {
+  [@deriving (sexp, compare)]
+  type t =
+    | Move(Dir.t)
+    | Construct(Shape.t)
+    | Del
+    | Finish;
+};
 
 module TypCtx: {
   type t('a) = Map.Make(String).t('a);
   let empty: t('a);
 };
-type typctx = TypCtx.t(htyp);
+type typctx = TypCtx.t(Htyp.t);
 
 exception Unimplemented;
 
-let erase_exp: zexp => hexp;
-let syn: (typctx, hexp) => option(htyp);
-let ana: (typctx, hexp, htyp) => bool;
-let syn_action: (typctx, (zexp, htyp), action) => option((zexp, htyp));
-let ana_action: (typctx, zexp, action, htyp) => option(zexp);
+let erase_exp: Zexp.t => Hexp.t;
+let syn: (typctx, Hexp.t) => option(Htyp.t);
+let ana: (typctx, Hexp.t, Htyp.t) => bool;
+let syn_action:
+  (typctx, (Zexp.t, Htyp.t), Action.t) => option((Zexp.t, Htyp.t));
+let ana_action: (typctx, Zexp.t, Action.t, Htyp.t) => option(Zexp.t);