From ea033d842f5af531e5a48403167a4dac88ced590 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Wed, 13 Nov 2024 15:44:07 +0800 Subject: [PATCH] [ new ] Store Agda version information for testing --- lib/js/src/State.bs.js | 5 +- lib/js/src/State/State__Command.bs.js | 12 +- lib/js/test/tests/Test__Auto.bs.js | 159 ++++++++++++++++++++------ src/State.res | 10 +- src/State/State__Command.res | 2 + src/State/State__Type.res | 1 + test/tests/Test__Auto.res | 131 +++++++++++++-------- 7 files changed, 227 insertions(+), 93 deletions(-) diff --git a/lib/js/src/State.bs.js b/lib/js/src/State.bs.js index 56546e3c..1123e8f9 100644 --- a/lib/js/src/State.bs.js +++ b/lib/js/src/State.bs.js @@ -57,7 +57,9 @@ function sendRequest(state, handleResponse, request) { return onDownload(state, extra); }), Config$AgdaModeVscode.Connection.getUseAgdaLanguageServer(), state.document, request, onResponse).then(async function (result) { if (result.TAG === "Ok") { - await State__View$AgdaModeVscode.Panel.displayConnectionStatus(state, result._0); + var status = result._0; + await State__View$AgdaModeVscode.Panel.displayConnectionStatus(state, status); + state.agdaVersion = status._0; } else { await State__View$AgdaModeVscode.Panel.displayConnectionError(state, result._0); } @@ -81,6 +83,7 @@ function destroy(state, alsoRemoveFromRegistry) { function make(channels, globalStoragePath, extensionPath, editor) { return { + agdaVersion: undefined, editor: editor, document: editor.document, panelCache: State__Type$AgdaModeVscode.ViewCache.make(), diff --git a/lib/js/src/State/State__Command.bs.js b/lib/js/src/State/State__Command.bs.js index 2a96e389..87afd25b 100644 --- a/lib/js/src/State/State__Command.bs.js +++ b/lib/js/src/State/State__Command.bs.js @@ -241,11 +241,13 @@ async function dispatchCommand(state, command) { } var version = match._0; await State__View$AgdaModeVscode.Panel.displayStatus(state, "Emacs v" + version); - return await State__View$AgdaModeVscode.Panel.display(state, { - TAG: "Success", - _0: "Switched to version '" + version + "'", - [Symbol.for("name")]: "Success" - }, [Item$AgdaModeVscode.plainText("Found '" + newAgdaVersion + "' at: " + match._1)]); + await State__View$AgdaModeVscode.Panel.display(state, { + TAG: "Success", + _0: "Switched to version '" + version + "'", + [Symbol.for("name")]: "Success" + }, [Item$AgdaModeVscode.plainText("Found '" + newAgdaVersion + "' at: " + match._1)]); + state.agdaVersion = version; + return ; } var match$1 = Connection__Error$AgdaModeVscode.toString(error._0); var header = { diff --git a/lib/js/test/tests/Test__Auto.bs.js b/lib/js/test/tests/Test__Auto.bs.js index ab9a6597..9279ac66 100644 --- a/lib/js/test/tests/Test__Auto.bs.js +++ b/lib/js/test/tests/Test__Auto.bs.js @@ -3,6 +3,7 @@ var Curry = require("rescript/lib/js/curry.js"); var Assert = require("assert"); +var Util$AgdaModeVscode = require("../../src/Util/Util.bs.js"); var State$AgdaModeVscode = require("../../src/State.bs.js"); var Test__Util$AgdaModeVscode = require("./Test__Util.bs.js"); @@ -29,24 +30,67 @@ function run(normalization) { } else { Assert.fail("No goals found"); } - return Curry._3(Assert.deepEqual, responses.contents, [ - { - TAG: "GiveAction", - _0: 0, - _1: { - TAG: "GiveString", - _0: "n", - [Symbol.for("name")]: "GiveString" - }, - [Symbol.for("name")]: "GiveAction" - }, - "CompleteHighlightingAndMakePromptReappear", - { - TAG: "InteractionPoints", - _0: [1], - [Symbol.for("name")]: "InteractionPoints" - } - ], undefined); + var version = state.agdaVersion; + if (version !== undefined) { + if (Util$AgdaModeVscode.Version.gte(version, "2.7.0")) { + return Curry._3(Assert.deepEqual, responses.contents, [ + { + TAG: "GiveAction", + _0: 0, + _1: { + TAG: "GiveString", + _0: "n", + [Symbol.for("name")]: "GiveString" + }, + [Symbol.for("name")]: "GiveAction" + }, + "CompleteHighlightingAndMakePromptReappear", + { + TAG: "InteractionPoints", + _0: [1], + [Symbol.for("name")]: "InteractionPoints" + } + ], undefined); + } else { + return Curry._3(Assert.deepEqual, responses.contents, [ + { + TAG: "GiveAction", + _0: 0, + _1: { + TAG: "GiveString", + _0: "n", + [Symbol.for("name")]: "GiveString" + }, + [Symbol.for("name")]: "GiveAction" + }, + { + TAG: "Status", + _0: false, + _1: false, + [Symbol.for("name")]: "Status" + }, + { + TAG: "DisplayInfo", + _0: { + TAG: "AllGoalsWarnings", + _0: "*All Goals*", + _1: "?1 : ℕ\n", + [Symbol.for("name")]: "AllGoalsWarnings" + }, + [Symbol.for("name")]: "DisplayInfo" + }, + "CompleteHighlightingAndMakePromptReappear", + { + TAG: "InteractionPoints", + _0: [1], + [Symbol.for("name")]: "InteractionPoints" + } + ], undefined); + } + } else { + Assert.fail("No Agda version found"); + return ; + } })); it("should be responded with the correct answer 2", (async function () { var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "Auto.agda"); @@ -68,24 +112,67 @@ function run(normalization) { } else { Assert.fail("No goals found"); } - return Curry._3(Assert.deepEqual, responses.contents, [ - { - TAG: "GiveAction", - _0: 1, - _1: { - TAG: "GiveString", - _0: "n", - [Symbol.for("name")]: "GiveString" - }, - [Symbol.for("name")]: "GiveAction" - }, - "CompleteHighlightingAndMakePromptReappear", - { - TAG: "InteractionPoints", - _0: [0], - [Symbol.for("name")]: "InteractionPoints" - } - ], undefined); + var version = state.agdaVersion; + if (version !== undefined) { + if (Util$AgdaModeVscode.Version.gte(version, "2.7.0")) { + return Curry._3(Assert.deepEqual, responses.contents, [ + { + TAG: "GiveAction", + _0: 1, + _1: { + TAG: "GiveString", + _0: "n", + [Symbol.for("name")]: "GiveString" + }, + [Symbol.for("name")]: "GiveAction" + }, + "CompleteHighlightingAndMakePromptReappear", + { + TAG: "InteractionPoints", + _0: [0], + [Symbol.for("name")]: "InteractionPoints" + } + ], undefined); + } else { + return Curry._3(Assert.deepEqual, responses.contents, [ + { + TAG: "GiveAction", + _0: 1, + _1: { + TAG: "GiveString", + _0: "m", + [Symbol.for("name")]: "GiveString" + }, + [Symbol.for("name")]: "GiveAction" + }, + { + TAG: "Status", + _0: false, + _1: false, + [Symbol.for("name")]: "Status" + }, + { + TAG: "DisplayInfo", + _0: { + TAG: "AllGoalsWarnings", + _0: "*All Goals*", + _1: "?0 : ℕ\n", + [Symbol.for("name")]: "AllGoalsWarnings" + }, + [Symbol.for("name")]: "DisplayInfo" + }, + "CompleteHighlightingAndMakePromptReappear", + { + TAG: "InteractionPoints", + _0: [0], + [Symbol.for("name")]: "InteractionPoints" + } + ], undefined); + } + } else { + Assert.fail("No Agda version found"); + return ; + } })); })); })); diff --git a/src/State.res b/src/State.res index e66d02c0..0a81cde3 100644 --- a/src/State.res +++ b/src/State.res @@ -63,7 +63,14 @@ let sendRequest = ( )->Promise.then(async result => { switch result { | Error(error) => await View.Panel.displayConnectionError(state, error) - | Ok(status) => await View.Panel.displayConnectionStatus(state, status) + | Ok(status) => + // display the connection status + await View.Panel.displayConnectionStatus(state, status) + // update the Agda version + switch status { + | Emacs(version, _) => state.agdaVersion = Some(version) + | LSP(version, _) => state.agdaVersion = Some(version) + } } await responseHandlerPromise }) @@ -89,6 +96,7 @@ let destroy = (state, alsoRemoveFromRegistry) => { } let make = (channels, globalStoragePath, extensionPath, editor) => { + agdaVersion: None, editor, document: VSCode.TextEditor.document(editor), panelCache: ViewCache.make(), diff --git a/src/State/State__Command.res b/src/State/State__Command.res index b6414ddc..f55bdb49 100644 --- a/src/State/State__Command.res +++ b/src/State/State__Command.res @@ -340,6 +340,8 @@ let rec dispatchCommand = async (state: State.t, command): unit => { View.Header.Success("Switched to version '" ++ version ++ "'"), [Item.plainText("Found '" ++ newAgdaVersion ++ "' at: " ++ path)], ) + // update the state.agdaVersion to the new version + state.agdaVersion = Some(version) | Ok(LSP(version, _)) => // should not happen await State.View.Panel.display( diff --git a/src/State/State__Type.res b/src/State/State__Type.res index 56b146d9..e6e067fd 100644 --- a/src/State/State__Type.res +++ b/src/State/State__Type.res @@ -120,6 +120,7 @@ type channels = { } type t = { + mutable agdaVersion: option, // Agda version is set when connection is established mutable editor: VSCode.TextEditor.t, mutable document: VSCode.TextDocument.t, panelCache: ViewCache.t, diff --git a/test/tests/Test__Auto.res b/test/tests/Test__Auto.res index 93242e93..25028092 100644 --- a/test/tests/Test__Auto.res +++ b/test/tests/Test__Auto.res @@ -1,64 +1,95 @@ open Mocha open Test__Util -let run = (normalization) => { +let run = normalization => { describe("request to Agda", () => { - describe( - "global", - () => { - Async.it( - "should be responded with the correct answer 1", - async () => { - let ctx = await AgdaMode.make("Auto.agda") - let state = await ctx->AgdaMode.load + describe("global", () => { + Async.it( + "should be responded with the correct answer 1", + async () => { + let ctx = await AgdaMode.make("Auto.agda") + let state = await ctx->AgdaMode.load - let responses = ref([]) - let responseHandler = async response => responses.contents->Array.push(response) + let responses = ref([]) + let responseHandler = async response => responses.contents->Array.push(response) - switch state.goals[0] { - | Some(goal) => - await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal)) - | None => Assert.fail("No goals found") + switch state.goals[0] { + | Some(goal) => + await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal)) + | None => Assert.fail("No goals found") + } + + switch state.agdaVersion { + | Some(version) => + if Util.Version.gte(version, "2.7.0") { + Assert.deepEqual( + responses.contents, + [ + GiveAction(0, GiveString("n")), + CompleteHighlightingAndMakePromptReappear, + InteractionPoints([1]), + ], + ) + } else { + Assert.deepEqual( + responses.contents, + [ + GiveAction(0, GiveString("n")), + Status(false, false), + DisplayInfo(AllGoalsWarnings("*All Goals*", "?1 : ℕ\n")), + CompleteHighlightingAndMakePromptReappear, + InteractionPoints([1]), + ], + ) } + | None => Assert.fail("No Agda version found") + } + }, + ) - Assert.deepEqual( - responses.contents, - [ - GiveAction(0, GiveString("n")), - CompleteHighlightingAndMakePromptReappear, - InteractionPoints([1]), - ], - ) - }, - ) + Async.it( + "should be responded with the correct answer 2", + async () => { + let ctx = await AgdaMode.make("Auto.agda") + let state = await ctx->AgdaMode.load - Async.it( - "should be responded with the correct answer 2", - async () => { - let ctx = await AgdaMode.make("Auto.agda") - let state = await ctx->AgdaMode.load + let responses = ref([]) + let responseHandler = async response => responses.contents->Array.push(response) - let responses = ref([]) - let responseHandler = async response => responses.contents->Array.push(response) + switch state.goals[1] { + | Some(goal) => + await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal)) + | None => Assert.fail("No goals found") + } - switch state.goals[1] { - | Some(goal) => - await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal)) - | None => Assert.fail("No goals found") + switch state.agdaVersion { + | Some(version) => + if Util.Version.gte(version, "2.7.0") { + Assert.deepEqual( + responses.contents, + [ + GiveAction(1, GiveString("n")), + CompleteHighlightingAndMakePromptReappear, + InteractionPoints([0]), + ], + ) + } else { + Assert.deepEqual( + responses.contents, + [ + GiveAction(1, GiveString("m")), + Status(false, false), + DisplayInfo(AllGoalsWarnings("*All Goals*", "?0 : ℕ\n")), + CompleteHighlightingAndMakePromptReappear, + InteractionPoints([0]), + ], + ) } - - Assert.deepEqual( - responses.contents, - [ - GiveAction(1, GiveString("n")), - CompleteHighlightingAndMakePromptReappear, - InteractionPoints([0]), - ], - ) - }, - ) - }, - ) + | None => Assert.fail("No Agda version found") + } + }, + ) + }) }) } @@ -76,4 +107,4 @@ describe("agda-mode.auto[Normalised]", () => { describe("agda-mode.auto[HeadNormal]", () => { run(HeadNormal) -}) \ No newline at end of file +})