Cannot launch polymorphic functions via lenses

[nickbattle]

If you define a polymorphic function, like this:

functions
        Launch | Debug
        set2seq[@T]: set of @T -> seq of @T
        set2seq(a) == ...

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:

set2seq({4,3,2,1}) = Cannot evaluate set2seq({4,3,2,1}) : Error 3350: Polymorphic function has not been instantiated in 'Set2Seq' (console) at line 1:1

That is because it is launched as set2seq({4,3,2,1}) rather than set2Seq[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.

[nickbattle]

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

[nickbattle]

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

[nickbattle]

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.