From 3002e581c98e11ef5e07b43ee4d01ee90c90a1db Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 23 Dec 2022 22:11:50 +0100 Subject: [PATCH] Add relevant devTasks for Juvix dev commads, fixes, and snippets --- README.md | 26 ++++++---- package.json | 33 +++++++++--- snippets/Debug.code-snippets | 98 ++++++++++++++++++++++++++++++++++++ snippets/Juvix.json | 9 +--- src/dev.ts | 14 +++--- test/A.juvix | 3 +- 6 files changed, 151 insertions(+), 32 deletions(-) create mode 100644 snippets/Debug.code-snippets diff --git a/README.md b/README.md index c968c86..c324cdf 100644 --- a/README.md +++ b/README.md @@ -81,20 +81,23 @@ settings. If you are debugging Juvix programs, you might want to use the extension in development mode. To do so, enable in your configuration the `juvix-mode.enableDevTasks` option. This will enable the extension to open a -panel and run the tasks specified in the active file. +panel and run the tasks specified in the active file. However, you can use +this feature even if it's not a Juvix file. The extension will look for lines in the active file that contain the pattern `DEBUG: nameTASK` where `nameTask` is an entry in the `juvix-mode.devTasks` configuration option. Check the extension configuration to see some examples you -can use or add your own setup. Some strings are expanded in the commands. For -example, `$filename` will be replaced by the name of the +can use or add your own setup. Some strings are expanded in runtime. For +example, `$filename` will be replaced by the name of the active file. The +extension provides autocompletion for the default tasks. To triger this feature, +start typing `debug` somewhere in the file. For example, if you have the following line in your configuration file: -``` +```json + "juvix-mode.enableDevTasks" : true, "juvix-mode.devTasks": { - "Parsed": "$juvix dev parse $filename", - "Scoped": "$juvix dev scope $filename", + "CatFile": "cat $filename" } ``` @@ -110,7 +113,8 @@ end; The extension will run the command for the `Parsed` task in a new tab and update that view when the file changes. If the active file contains multiple `DEBUG` annotations, the extension will run all the commands in separate tabs. For -example, if you have the following lines in your file: +example, if you have the following lines in your file, the extension will open +two tabs, one for the `InternalArity` task and another for the `CoreLifting` ``` module A; @@ -118,22 +122,24 @@ open import B; axiom a : A; axiom b : A; end; --- DEBUG: Internal-Arity +-- DEBUG: InternalArity -- DEBUG: CoreLifting ``` To keep your debug annotations but not run the tasks on save, you can add the `NO-DEBUG!` annotation, somewhere in the file. To run all the available tasks, -include `DEBUG: ALL`. +include `DEBUG: All`. ``` -- NO-DEBUG! --- DEBUG: ALL +-- DEBUG: All module B; axiom A : Type; end; ``` +The aforementioned features are experimental and might change in the future. + ## Features - Command palette with typechecking, compilation, and running Juvix files. diff --git a/package.json b/package.json index 253f851..5cb10e1 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "juvix-mode", - "version": "0.1.10", + "version": "0.1.11", "license": "GPL-3.0", "description": "Juvix IDE support for VSCode", "displayName": "Juvix", @@ -169,6 +169,9 @@ { "language": "Juvix", "path": "./snippets/Juvix.json" + }, + { + "path": "./snippets/Debug.code-snippets" } ], "languages": [ @@ -2329,16 +2332,32 @@ "juvix-mode.devTasks": { "type": "object", "items": { - "description": "Internal commands that run on save. Juvix executable is passed as $juvix, the filename as $filename. Example command: $juvix dev internal pretty $filename" + "description": "Internal commands that run on save. Juvix executable is passed as $juvix, the filename as $filename. " }, "default": { + "CatFile": "cat $filename", "Parsed": "$juvix dev parse $filename", "Scoped": "$juvix dev scope $filename", - "EvalCore": "$juvix dev core-eval $filename", - "Internal-Pretty": "$juvix dev internal pretty $filename", - "Internal-Arity": "$juvix dev internal arity $filename", - "Highlighting": "$juvix dev highlight --format json $filename", - "CoreLifting": "$juvix dev core read -t lifting $filename" + "HighlightJSON": "$juvix dev highlight --format json $filename", + "Highlight": "$juvix dev highlight $filename", + "InternalPretty": "$juvix dev internal pretty $filename", + "InternalArity": "$juvix dev internal arity $filename", + "InternalTypecheck": "$juvix dev internal typecheck $filename", + "InternalCoreEval": "$juvix dev internal core-eval $filename", + "InternalCoreEvalShowDeBruijn": "$juvix dev internal core-eval --show-de-brujin $filename", + "InternalCoreEvalTransformsLifting": "$juvix dev internal core-eval --transforms lifting $filename", + "InternalCoreEvalTransformsMoveApps": "$juvix dev internal core-eval --transforms move-apps $filename", + "InternalCoreEvalTransformsRemoveTypeArgs": "$juvix dev internal core-eval --transforms remove-type-args $filename", + "InternalCoreEvalTransformsRemoveTopEtaExpand": "$juvix dev internal core-eval --transforms top-eta-expand $filename", + "CoreEval": "$juvix dev core eval $filename", + "CoreRead": "$juvix dev core read $filename", + "AsmRun": "$juvix dev asm run $filename", + "AsmValidate": "$juvix dev asm validate $filename", + "AsmCompile": "$juvix dev asm compile $filename", + "RuntimeCompile": "$juvix dev runtime compile $filename", + "Root": "$juvix dev root", + "TerminationCalls": "$juvix dev termination calls -d $filename", + "TerminationGraph": "$juvix dev termination graph $filename" } } } diff --git a/snippets/Debug.code-snippets b/snippets/Debug.code-snippets new file mode 100644 index 0000000..d55f904 --- /dev/null +++ b/snippets/Debug.code-snippets @@ -0,0 +1,98 @@ +{ + "All": { + "prefix": ["debug-all"], + "body": "$BLOCK_COMMENT_START DEBUG: All $BLOCK_COMMENT_END" + }, + "None": { + "prefix": ["debug-none"], + "body": "$BLOCK_COMMENT_START NO-DEBUG! $BLOCK_COMMENT_END" + }, + "Parsed": { + "prefix": ["debug-parse"], + "body": "$BLOCK_COMMENT_START DEBUG: sed $BLOCK_COMMENT_END" + }, + "Scoped": { + "prefix": ["debug-scope"], + "body": "$BLOCK_COMMENT_START DEBUG: Scoped" + }, + "HighlightJSON": { + "prefix": ["debug-highlight-json"], + "body": "$BLOCK_COMMENT_START DEBUG: HighlightJSON $BLOCK_COMMENT_END" + }, + "Highlight": { + "prefix": ["debug-highlight"], + "body": "$BLOCK_COMMENT_START DEBUG: Highlight $BLOCK_COMMENT_END" + }, + "InternalPretty": { + "prefix": ["debug-internal-pretty"], + "body": "$BLOCK_COMMENT_START DEBUG: ernalPretty $BLOCK_COMMENT_END" + }, + "InternalArity": { + "prefix": ["debug-internal-arity"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalArity $BLOCK_COMMENT_END" + }, + "InternalTypecheck": { + "prefix": ["debug-internal-typecheck"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalTypecheck $BLOCK_COMMENT_END" + }, + "InternalCoreEval": { + "prefix": ["debug-internal-core-eval"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEval $BLOCK_COMMENT_END" + }, + "InternalCoreEvalShowDeBruijn": { + "prefix": ["debug-internal-core-eval-show-de-bruijn"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalShowDeBruijn $BLOCK_COMMENT_END" + }, + "InternalCoreEvalTransformsLifting": { + "prefix": ["debug-lifting"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsLifting $BLOCK_COMMENT_END" + }, + "InternalCoreEvalTransformsMoveApps": { + "prefix": ["debug-move-apps"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsMoveApps $BLOCK_COMMENT_END" + }, + "InternalCoreEvalTransformsRemoveTypeArgs": { + "prefix": ["debug-remove-type-args"], + "body": "$BLOCK_COMMENT_START DEBUG: InternalCoreEvalTransformsRemoveTypeArgs $BLOCK_COMMENT_END" + }, + "InternalCoreEvalTransformsRemoveTopEtaExpand": { + "prefix": ["debug-remove-top-eta-expand"], + "body": "$BLOCK_COMMENT_START DEBUG: ernalCoreEvalTransformsRemoveTopEtaExpand $BLOCK_COMMENT_END" + }, + "CoreEval": { + "prefix": ["debug-core-eval"], + "body": "$BLOCK_COMMENT_START DEBUG: CoreEval $BLOCK_COMMENT_END" + }, + "CoreRead": { + "prefix": ["debug-core-read"], + "body": "$BLOCK_COMMENT_START DEBUG: CoreRead $BLOCK_COMMENT_END" + }, + "AsmRun": { + "prefix": ["debug-asm-run"], + "body": "$BLOCK_COMMENT_START DEBUG: AsmRun $BLOCK_COMMENT_END" + }, + "AsmValidate": { + "prefix": ["debug-asm-validate"], + "body": "$BLOCK_COMMENT_START DEBUG: AsmValidate $BLOCK_COMMENT_END" + }, + "AsmCompile": { + "prefix": ["debug-asm-compile"], + "body": "$BLOCK_COMMENT_START DEBUG: AsmCompile $BLOCK_COMMENT_END" + }, + "RuntimeCompile": { + "prefix": ["debug-runtime-compile"], + "body": "$BLOCK_COMMENT_START DEBUG: RuntimeCompile $BLOCK_COMMENT_END" + }, + "Root": { + "prefix": ["debug-root"], + "body": "$BLOCK_COMMENT_START DEBUG: Root $BLOCK_COMMENT_END" + }, + "TerminationCalls": { + "prefix": ["debug-termination-calls"], + "body": "$BLOCK_COMMENT_START DEBUG: TerminationCalls $BLOCK_COMMENT_END" + }, + "TerminationGraph": { + "prefix": ["debug-termination-graph"], + "body": "$BLOCK_COMMENT_START DEBUG: TerminationGraph" + } +} diff --git a/snippets/Juvix.json b/snippets/Juvix.json index c783e42..66a7350 100644 --- a/snippets/Juvix.json +++ b/snippets/Juvix.json @@ -5,8 +5,8 @@ "description": "module type" }, "data types": { - "prefix": ["ind", "data"], - "body": "inductive ${1:typeName ${2:typeParameters?}} {\n ${3:constructorName} : ${4:constructorArgs} -> ${5:returnType}; \n};\n", + "prefix": ["type", "inductive", "data"], + "body": "type ${1:typeName} {\n ${3:constructorName} : ${4:constructorArgs} -> ${5:returnType} |\n ${6:constructorName} : ${7:constructorArgs} -> ${8:returnType} \n};\n", "description": "inductive data type declaration" }, "axiom": { @@ -33,10 +33,5 @@ "prefix": "doc", "body": "--- ${1:documentation}", "description": "documentation" - }, - "set type": { - "prefix": "ty", - "body": "Type", - "description": "The type of all types" } } diff --git a/src/dev.ts b/src/dev.ts index 4ab4631..6c27b5c 100644 --- a/src/dev.ts +++ b/src/dev.ts @@ -42,24 +42,24 @@ class DevEnv { if (this.document) this.makeViews(); const changeEditor = vscode.window.onDidChangeActiveTextEditor(e => { - this.disposables.push(changeEditor); - if (e) { - if (e.document) { - if (e.document !== this.document) this.disposeViews(); + if (e && e.document) { + if (e.document !== this.document) { + this.disposeViews(); this.document = e.document; this.makeViews(); } } + this.disposables.push(changeEditor); }); const closeD = vscode.workspace.onDidCloseTextDocument(doc => { - this.disposables.push(closeD); if (doc === this.document) this.disposeViews(); + this.disposables.push(closeD); }); const saveDoc = vscode.workspace.onDidSaveTextDocument(doc => { - this.disposables.push(saveDoc); if (doc === this.document) this.makeViews(); + this.disposables.push(saveDoc); }); } @@ -70,7 +70,7 @@ class DevEnv { const txt: string = this.document!.getText(); const debug = txt.indexOf(debugStr) > -1; if (!debug || txt.indexOf('NO-DEBUG!') > -1) return; - const all = txt.indexOf(debugStr + ' ALL') > -1; + const all = txt.indexOf(debugStr + ' All') > -1; const views = config.devTasks.get(); Object.entries(views).forEach(([title, cmd], _) => { if (all || txt.indexOf(debugStr + ' ' + title) > -1) diff --git a/test/A.juvix b/test/A.juvix index 0564aba..b5ff148 100644 --- a/test/A.juvix +++ b/test/A.juvix @@ -3,4 +3,5 @@ open import B; axiom a : A; axiom b : A; end; --- DEBUG: Internal-Arity \ No newline at end of file + +{- DEBUG: All -} \ No newline at end of file