Add relevant devTasks for Juvix dev commads, fixes, and snippets

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,30 +113,33 @@ 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;
 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.

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"
           }
         }
       }

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"
+  }
+}

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"
   }
 }

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)

test/A.juvix

@@ -3,4 +3,5 @@ open import B;
 axiom a : A;
 axiom b : A;
 end;
--- DEBUG: Internal-Arity
+
+{- DEBUG: All -}