overturetool / vdm-vscode

Visual Studio Code extension for VDM language support
GNU General Public License v3.0
21 stars 6 forks source link

Unable to debug functions with type parameters #203

Closed mortenhaahr closed 1 year ago

mortenhaahr commented 1 year ago

It appears that it is impossible to use the VSCode lens to debug a function with type parameters. Please see the simple identity function below followed by steps to reproduce it:

class A
functions

public identity[@T]: @T -> @T
identity(t) == t;

end A

Steps to reproduce:

  1. Copy and paste the content of the code snippet above into a .vdmpp file and open it in VSCode.
  2. The option Launch | Debug should be shown above the function.
  3. Press either Launch or Debug.
  4. Enter the value 1 in the text field.

Actual result: An error occurs in the terminal: identity(1) = Cannot evaluate identity(1) : Error 3350: Polymorphic function has not been instantiated in 'A' (console) at line 1:1

Workaround: Open the launch.json file. On the line where it says "command": "p identity(1)" change this to "command": "p identity[nat](1)". Manually debug the function by opening the "Run and Debug" panel (ctrl+shift+D). Press the green button to debug.

Expected result: I propose two suggestions:

  1. The type can be inferred.
  2. Step 3.5 should be introduced where the user is prompted to provide the type of T.
nickbattle commented 1 year ago

Yes, this is a duplicate of #188 . The type data is now sent to the Client (VSCode) from VDMJ, but it is not (yet) prompted for or added to the launch configuration. As a workaround, you can edit the launch.json entry to include the [type] part.

I will close this as a duplicate.