Open nickbattle opened 1 year ago
The current lens arguments are as follows:
"command":
{
"title": "Launch",
"command": "vdm-vscode.addLensRunConfiguration",
"arguments":
[
{
"name": "Launch set2seq",
"defaultName": "Set2Seq",
"type": "vdm",
"request": "launch",
"noDebug": true,
"remoteControl": null,
"applyName": "set2seq",
"applyArgs":
[
{
"name": "a",
"type": "set of (@T)"
}
]
}
]
}
I suggest we add an (optional) applyTypes
section, with just a list of type name strings like @T
in this example. The UI would then prompt for these and add them after the function name in the launch.
...
applyTypes
[
{
"name": "@T"
}
]
...
This is now available in the "development" branch of VDMJ...
{
"title": "Debug",
"command": "vdm-vscode.addLensRunConfiguration",
"arguments":
[
{
"name": "Debug set2seq",
"defaultName": "Set2Seq",
"type": "vdm",
"request": "launch",
"noDebug": false,
"remoteControl": null,
"applyName": "set2seq",
"applyTypes":
[
"@T"
],
"applyArgs":
[
{
"name": "a",
"type": "set of (@T)"
}
]
}
]
}
Obviously this only applies to explicit functions with type parameters. Implicit functions or operations do not have the applyTypes
value in the lens argument returned.
If you define a polymorphic function, like this:
You get the
Launch | Debug
lenses above it as usual, but since the launch selection (at the Client) does not prompt for the@T
type parameter, you get an error when the launch is performed:That is because it is launched as
set2seq({4,3,2,1})
rather thanset2Seq[nat]({4,3,2,1})
.The Launch and Debug lens commands need to be sensitive to polymorphic functions and prompt for the type parameter(s) as well as the arguments. That probably requires the type names to be sent in the JSON arguments from the lens.