Start of our own AST.

7 files changed, 57 insertions, 10 deletions

diff --git a/.gitignore b/.gitignore
index 3476910..d8b6d74 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,6 +4,7 @@
 !.builds
 !.envrc
 !.gitignore
+!.ocamlformat
 
 # Nix outputs
 result
diff --git a/discocaml/.ocamlformat b/discocaml/.ocamlformat
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/discocaml/.ocamlformat
diff --git a/discocaml/ast.ml b/discocaml/ast.ml
new file mode 100644
index 0000000..009ea87
--- /dev/null
+++ b/discocaml/ast.ml
@@ -0,0 +1,3 @@
+type expr = Foo [@@deriving show { with_path = false }]
+
+let expr_of_parsetree : Parsetree.expression -> expr = function _ -> Foo
diff --git a/discocaml/dune b/discocaml/dune
index 961fe70..50b12c2 100644
--- a/discocaml/dune
+++ b/discocaml/dune
@@ -2,14 +2,17 @@
  (name discocaml)
  (inline_tests)
  (libraries compiler-libs.common yojson)
- (modules discocaml)
+ (modules ast discocaml eval)
  (package discocaml)
  (preprocess
   (pps ppx_deriving.show ppx_deriving_yojson ppx_expect)))
 
+(env
+ (release
+  (link_flags
+   (:standard -cclib -static -cclib -lm -O3))))
+
 (executable
- (flags
-  (:standard -cclib -static -cclib -lm))
  (libraries discocaml yojson)
  (modules main)
  (name main)
diff --git a/discocaml/eval.ml b/discocaml/eval.ml
new file mode 100644
index 0000000..68bb637
--- /dev/null
+++ b/discocaml/eval.ml
@@ -0,0 +1,7 @@
+open Ast
+
+type path = int list
+(** A path from the root of a term to a subterm. *)
+
+let find_redex_cbv : expr -> path option = function _ -> None
+let find_redex_cbn : expr -> path option = function _ -> None
diff --git a/flake.nix b/flake.nix
index 302362e..7fbde5e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -20,7 +20,10 @@
         };
       in rec {
         devShells.default = pkgs.mkShell {
-          inputsFrom = builtins.attrValues packages;
+          inputsFrom = builtins.attrValues (packages // {
+            discocaml =
+              pkgs.ocaml-ng.ocamlPackages_5_1.callPackage ./discocaml { };
+          });
           nativeBuildInputs = [
             pkgs.bubblewrap
             pkgs.cargo-watch
diff --git a/src/commands/discocaml.rs b/src/commands/discocaml.rs
index 4aaa695..78c2d95 100644
--- a/src/commands/discocaml.rs
+++ b/src/commands/discocaml.rs
@@ -159,13 +159,43 @@ pub async fn run_discocaml(
 
 fn make_response_message(expr: &DiscocamlResponseExpr) -> CreateInteractionResponseMessage {
     // TODO: Real escaping
-    CreateInteractionResponseMessage::new()
+    let mut out = CreateInteractionResponseMessage::new()
         .content(format!("```ocaml\n{}\n```", expr.expr))
-        .button(CreateButton::new("step-cbv").label("Step (CBV)"))
-        .button(CreateButton::new("step-cbn").label("Step (CBN)"))
-        .button(CreateButton::new("run-cbv").label("Run (CBV)"))
-        .button(CreateButton::new("run-cbn").label("Run (CBN)"))
-        .button(CreateButton::new("draw-tree").label("Draw Tree"))
+        .button(
+            CreateButton::new("draw-tree")
+                .label("Draw Tree")
+                .disabled(true),
+        );
+
+    out = out
+        .button(
+            CreateButton::new("step-cbv")
+                .label("Step (CBV)")
+                .disabled(true),
+        )
+        .button(
+            CreateButton::new("step-cbn")
+                .label("Step (CBN)")
+                .disabled(true),
+        )
+        .button(
+            CreateButton::new("run-cbv")
+                .label("Run (CBV)")
+                .disabled(true),
+        )
+        .button(
+            CreateButton::new("run-cbn")
+                .label("Run (CBN)")
+                .disabled(true),
+        );
+
+    out = out.button(
+        CreateButton::new("start-proving")
+            .label("Prove it!")
+            .disabled(true),
+    );
+
+    out
 }
 
 pub async fn handle_command(