From 5588808852a2fd379be0e9c01cf67cfdcbcdd4c3 Mon Sep 17 00:00:00 2001 From: Nathan Ringo Date: Thu, 18 Jan 2024 19:02:16 -0600 Subject: Prepare to output non-single-expr messages. --- discocaml/ast.ml | 12 ++ discocaml/discocaml.ml | 72 +++++------ discocaml/eval.ml | 1 + migrations/20240118234708_init_discocaml.sql | 7 ++ src/commands/discocaml.rs | 181 +++++++++++++++++++++------ src/commands/mod.rs | 22 +++- 6 files changed, 218 insertions(+), 77 deletions(-) create mode 100644 migrations/20240118234708_init_discocaml.sql diff --git a/discocaml/ast.ml b/discocaml/ast.ml index 009ea87..22f3790 100644 --- a/discocaml/ast.ml +++ b/discocaml/ast.ml @@ -1,3 +1,15 @@ type expr = Foo [@@deriving show { with_path = false }] let expr_of_parsetree : Parsetree.expression -> expr = function _ -> Foo + +let parsetree_of_expr : expr -> Parsetree.expression = + let expression (pexp_desc : Parsetree.expression_desc) : Parsetree.expression + = + { + pexp_desc; + pexp_loc = Location.none; + pexp_loc_stack = []; + pexp_attributes = []; + } + in + function Foo -> expression (Pexp_constant (Pconst_char '!')) diff --git a/discocaml/discocaml.ml b/discocaml/discocaml.ml index cd99c9a..2140fa5 100644 --- a/discocaml/discocaml.ml +++ b/discocaml/discocaml.ml @@ -1,13 +1,19 @@ -type command = [ `Roundtrip ] +type command = [ `Parse | `DrawTree | `RunCBN | `RunCBV | `StepCBN | `StepCBV ] let command_of_yojson = function - | `String "Roundtrip" -> Ok `Roundtrip + | `String "Parse" -> Ok `Parse + | `String "DrawTree" -> Ok `DrawTree + | `String "RunCBN" -> Ok `RunCBN + | `String "RunCBV" -> Ok `RunCBV + | `String "StepCBN" -> Ok `StepCBN + | `String "StepCBV" -> Ok `StepCBV | _ -> Error "invalid command" type request = { expr : string; command : command } [@@deriving of_yojson { exn = true }] -type response_expr = { expr : string } [@@deriving to_yojson { exn = true }] +type response_expr = { expr : string; has_redex : bool } +[@@deriving to_yojson { exn = true }] type response = [ `Error of string | `Expr of response_expr ] [@@deriving to_yojson { exn = true }] @@ -17,47 +23,37 @@ let%expect_test _ = [%expect {| ["Error","foo"] |}] let%expect_test _ = - Yojson.Safe.to_channel stdout (response_to_yojson (`Expr { expr = "foo" })); - [%expect {| ["Expr",{"expr":"foo"}] |}] -(* -type position = [%import: Lexing.position] [@@deriving show] - -type location = [%import: (Location.t[@with Lexing.position := position])] -[@@deriving show] - -type constant = [%import: Parsetree.constant] [@@deriving show] -type expression_desc = [%import: Parsetree.expression_desc] [@@deriving show] -type expression = [%import: Parsetree.expression] [@@deriving show] - -type structure_item_desc = [%import: Parsetree.structure_item_desc] -[@@deriving show] - -type structure_item = [%import: Parsetree.structure_item] [@@deriving show] -type structure = [%import: Parsetree.structure] [@@deriving show] -type toplevel_phrase = [%import: Parsetree.toplevel_phrase] [@@deriving show] - -let parse ~path (src : string) = - let buf = Lexing.from_string src in - buf.lex_start_p <- { buf.lex_start_p with pos_fname = path }; - buf.lex_curr_p <- { buf.lex_curr_p with pos_fname = path }; - Parse.expression buf - -let () = - parse ~path:"main.ml" " print_endline ((\"Hello, world!\") )" - |> Format.fprintf Format.std_formatter "\n%a\n" Pprintast.expression -*) + Yojson.Safe.to_channel stdout + (response_to_yojson (`Expr { expr = "foo"; has_redex = false })); + [%expect {| ["Expr",{"expr":"foo","has_redex":false}] |}] let handle_request { expr; command } : response = try let buf = Lexing.from_string expr in let expr = Parse.expression buf in + let expr = Ast.expr_of_parsetree expr in + + let expr_response (expr : Ast.expr) : response = + let buf = Buffer.create 16 in + (let fmt = Format.formatter_of_buffer buf in + Pprintast.expression fmt (Ast.parsetree_of_expr expr); + Format.pp_print_flush fmt ()); + let has_redex = Option.is_some (Eval.find_redex_cbn expr) in + `Expr { expr = Buffer.contents buf; has_redex } + in + + let step_with (find_redex : Ast.expr -> Eval.path option) (expr : Ast.expr) + : Ast.expr = + match find_redex expr with + | Some path -> Eval.reduce expr path + | None -> failwith "no redex" + in + match command with - | `Roundtrip -> - let buf = Buffer.create 16 in - (let fmt = Format.formatter_of_buffer buf in - Pprintast.expression fmt expr; - Format.pp_print_flush fmt ()); - `Expr { expr = Buffer.contents buf } + | `Parse -> expr_response expr + | `StepCBN -> expr_response (step_with Eval.find_redex_cbn expr) + | `StepCBV -> expr_response (step_with Eval.find_redex_cbv expr) + | `DrawTree | `RunCBN | `RunCBV -> failwith "not implemented" with | Failure msg -> `Error msg | exn -> `Error ("uncaught exception: " ^ Printexc.to_string exn) diff --git a/discocaml/eval.ml b/discocaml/eval.ml index 68bb637..63dd6f7 100644 --- a/discocaml/eval.ml +++ b/discocaml/eval.ml @@ -5,3 +5,4 @@ type path = int list let find_redex_cbv : expr -> path option = function _ -> None let find_redex_cbn : expr -> path option = function _ -> None +let reduce : expr -> path -> expr = fun e _ -> e diff --git a/migrations/20240118234708_init_discocaml.sql b/migrations/20240118234708_init_discocaml.sql new file mode 100644 index 0000000..adce26a --- /dev/null +++ b/migrations/20240118234708_init_discocaml.sql @@ -0,0 +1,7 @@ +-- We're just storing a map between interaction IDs and the expression at the +-- time. If we ever get theorem proving support, this'll probably need to be +-- extended... That, or we just have another table for the context? +CREATE TABLE IF NOT EXISTS discocaml_exprs + ( interaction_id INTEGER PRIMARY KEY + , expr TEXT NOT NULL + ); diff --git a/src/commands/discocaml.rs b/src/commands/discocaml.rs index 78c2d95..8565c6f 100644 --- a/src/commands/discocaml.rs +++ b/src/commands/discocaml.rs @@ -1,9 +1,12 @@ use anyhow::{anyhow, bail, Context as _, Error, Result}; +use futures::Future; use serde::{Deserialize, Serialize}; use serde_json::de::Deserializer; use serenity::{ all::{ - CommandDataOptionValue, CommandInteraction, CommandOptionType, CommandType, Member, RoleId, + CommandDataOptionValue, CommandInteraction, CommandOptionType, CommandType, + ComponentInteraction, ComponentInteractionDataKind, InteractionId, + InteractionResponseFlags, Member, RoleId, }, builder::{ CreateButton, CreateCommand, CreateCommandOption, CreateInteractionResponse, @@ -33,7 +36,12 @@ pub struct DiscocamlRequest { #[derive(Debug, PartialEq, Serialize)] pub enum DiscocamlCommand { - Roundtrip, + Parse, + DrawTree, + RunCBN, + RunCBV, + StepCBN, + StepCBV, } /// A response outputted by the discocaml subprocess as a JSON string. @@ -46,11 +54,13 @@ pub enum DiscocamlCommand { /// let example = r#" /// [ "Expr" /// , { "expr": "1 + 2" +/// , "has_redex": true /// } /// ] /// "#; /// let expected = DiscocamlResponse::Expr(DiscocamlResponseExpr { /// expr: "1 + 2".to_string(), +/// has_redex: true, /// }); /// /// let mut de = Deserializer::from_str(&example); @@ -70,6 +80,21 @@ pub enum DiscocamlResponse { #[serde(deny_unknown_fields)] pub struct DiscocamlResponseExpr { pub expr: String, + pub has_redex: bool, +} + +impl DiscocamlResponseExpr { + async fn save(&self, db: &SqlitePool, id: InteractionId) -> Result<()> { + let interaction_id = i64::from(id); + sqlx::query!( + "INSERT INTO discocaml_exprs (interaction_id, expr) VALUES (?, ?)", + interaction_id, + self.expr + ) + .execute(db) + .await?; + Ok(()) + } } pub fn command() -> CreateCommand { @@ -88,7 +113,7 @@ pub fn command() -> CreateCommand { ) } -async fn check_permissions(config: &DiscocamlConfig, member: &Option>) -> Result<()> { +async fn check_permissions(config: &DiscocamlConfig, member: Option<&Member>) -> Result<()> { if let Some(member) = member { if !member.roles.contains(&config.role) { bail!("This command can only be used by <@&{}>.", config.role) @@ -99,12 +124,14 @@ async fn check_permissions(config: &DiscocamlConfig, member: &Option } } -async fn respond_with_error(ctx: &Context, command: &CommandInteraction, err: &Error) { - let msg = CreateInteractionResponseMessage::new().content(format!(":no_entry_sign: {}", err)); - if let Err(err) = command - .create_response(ctx, CreateInteractionResponse::Message(msg)) - .await - { +async fn respond_with_error>>( + err: &Error, + send: impl FnOnce(CreateInteractionResponse) -> F, +) { + let msg = CreateInteractionResponseMessage::new() + .content(format!(":no_entry_sign: {}", err)) + .flags(InteractionResponseFlags::EPHEMERAL); + if let Err(err) = send(CreateInteractionResponse::Message(msg)).await { log::error!( "failed to respond to command that failed permissions check: {:?}", err @@ -159,54 +186,40 @@ pub async fn run_discocaml( fn make_response_message(expr: &DiscocamlResponseExpr) -> CreateInteractionResponseMessage { // TODO: Real escaping - let mut out = CreateInteractionResponseMessage::new() + CreateInteractionResponseMessage::new() .content(format!("```ocaml\n{}\n```", expr.expr)) - .button( - CreateButton::new("draw-tree") - .label("Draw Tree") - .disabled(true), - ); - - out = out + .button(CreateButton::new("draw-tree").label("Draw Tree")) .button( CreateButton::new("step-cbv") .label("Step (CBV)") - .disabled(true), + .disabled(!expr.has_redex), ) .button( CreateButton::new("step-cbn") .label("Step (CBN)") - .disabled(true), + .disabled(!expr.has_redex), ) .button( CreateButton::new("run-cbv") .label("Run (CBV)") - .disabled(true), + .disabled(!expr.has_redex), ) .button( CreateButton::new("run-cbn") .label("Run (CBN)") - .disabled(true), - ); - - out = out.button( - CreateButton::new("start-proving") - .label("Prove it!") - .disabled(true), - ); - - out + .disabled(!expr.has_redex), + ) } pub async fn handle_command( ctx: &Context, config: &DiscocamlConfig, - _db: &SqlitePool, + db: &SqlitePool, command: &CommandInteraction, ) -> Result<()> { // Check that the required role was present. - if let Err(err) = check_permissions(config, &command.member).await { - respond_with_error(ctx, command, &err).await; + if let Err(err) = check_permissions(config, command.member.as_deref()).await { + respond_with_error(&err, |res| command.create_response(&ctx, res)).await; return Err(err.context("permissions check failed")); } @@ -217,7 +230,7 @@ pub async fn handle_command( ("expr", CommandDataOptionValue::String(value)) => expr = Some(value), _ => { let err = anyhow!("unknown option {:?}", option); - respond_with_error(ctx, command, &err).await; + respond_with_error(&err, |res| command.create_response(&ctx, res)).await; return Err(err); } } @@ -226,23 +239,33 @@ pub async fn handle_command( expr } else { let err = anyhow!("missing option {:?}", "expr"); - respond_with_error(ctx, command, &err).await; + respond_with_error(&err, |res| command.create_response(&ctx, res)).await; return Err(err); }; // Round-trip the expression through discocaml. let req = DiscocamlRequest { expr: expr.to_string(), - command: DiscocamlCommand::Roundtrip, + command: DiscocamlCommand::Parse, }; let res = match run_discocaml(config, &req).await { Ok(res) => res, Err(err) => { - respond_with_error(ctx, command, &err).await; + respond_with_error(&err, |res| command.create_response(&ctx, res)).await; return Err(err.context("failed to run discocaml")); } }; + // Insert the output expression in the database. + if let Err(err) = res + .save(db, command.id) + .await + .context("failed to save expression to database") + { + respond_with_error(&err, |res| command.create_response(&ctx, res)).await; + return Err(err); + } + // Respond with the expression and the buttons. command .create_response( @@ -252,3 +275,87 @@ pub async fn handle_command( .await .context("failed to respond") } + +pub async fn handle_button( + ctx: &Context, + config: &DiscocamlConfig, + db: &SqlitePool, + component: &ComponentInteraction, +) -> Result<()> { + // Check that the required role was present. + if let Err(err) = check_permissions(config, component.member.as_ref()).await { + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err.context("permissions check failed")); + } + + // Find the interaction ID from the message it was in response to. + let interaction_id = if let Some(interaction) = &component.message.interaction { + i64::from(interaction.id) + } else { + let err = anyhow!( + "button was pressed in response to an unknown message {:?}", + component.message.id + ); + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err); + }; + + // Fetch the expression it was in response to. + let result = sqlx::query!( + "SELECT expr FROM discocaml_exprs WHERE interaction_id = ?", + interaction_id, + ) + .fetch_one(db) + .await + .context("failed to load expression from database"); + let expr = match result { + Ok(expr) => expr.expr, + Err(err) => { + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err); + } + }; + + // Come up with a command for discocaml based on which button it was. + let command = match (&component.data.kind, &component.data.custom_id as &str) { + (ComponentInteractionDataKind::Button, "draw-tree") => DiscocamlCommand::DrawTree, + (ComponentInteractionDataKind::Button, "step-cbv") => DiscocamlCommand::StepCBV, + (ComponentInteractionDataKind::Button, "step-cbn") => DiscocamlCommand::StepCBN, + (ComponentInteractionDataKind::Button, "run-cbv") => DiscocamlCommand::RunCBV, + (ComponentInteractionDataKind::Button, "run-cbn") => DiscocamlCommand::RunCBN, + _ => { + let err = anyhow!("unknown component {:?}", component.data); + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err); + } + }; + + // Send discocaml the request. + let req = DiscocamlRequest { expr, command }; + let res = match run_discocaml(config, &req).await { + Ok(res) => res, + Err(err) => { + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err.context("failed to run discocaml")); + } + }; + + // Insert the output expression in the database. + if let Err(err) = res + .save(db, component.id) + .await + .context("failed to save expression to database") + { + respond_with_error(&err, |res| component.create_response(&ctx, res)).await; + return Err(err); + } + + // Respond with the expression and the buttons. + component + .create_response( + &ctx, + CreateInteractionResponse::Message(make_response_message(&res)), + ) + .await + .context("failed to respond") +} diff --git a/src/commands/mod.rs b/src/commands/mod.rs index 899bb8f..d793c95 100644 --- a/src/commands/mod.rs +++ b/src/commands/mod.rs @@ -34,13 +34,31 @@ pub async fn handle_interaction( .await .context("failed to handle discocaml command"), _ => { - log::warn!("unexpected interaction: {:?}", interaction); + log::warn!("unexpected interaction: {:#?}", interaction); Ok(()) } }, + Interaction::Component(component) => { + match component + .message + .interaction + .as_ref() + .map(|i| &i.name as &str) + { + Some("discocaml") => { + discocaml::handle_button(ctx, &config.discocaml, db, component) + .await + .context("failed to handle discocaml command") + } + _ => { + log::warn!("unexpected interaction: {:#?}", interaction); + Ok(()) + } + } + } _ => { - log::warn!("unexpected interaction: {:?}", interaction); + log::warn!("unexpected interaction: {:#?}", interaction); Ok(()) } } -- cgit v1.2.3