aya-prover / aya-vscode

~ VSCode extension for Aya Prover
GNU General Public License v3.0
7 stars 2 forks source link

Can't compute-type and compute-nf #12

Closed by-cloud closed 3 years ago

by-cloud commented 3 years ago

After press ctrl+l ctrl+p or ctrl+l ctrl+n, we have error report in debug console:

Error: Invalid arguments
    at new l (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:87:21239)
    at new l (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:87:17220)
    at applyComputedTerm (/Users/claude/Downloads/projects/aya/aya-vscode/out/compute-term.js:21:24)
    at /Users/claude/Downloads/projects/aya/aya-vscode/out/features.js:24:152

I think the result passed to applyComputedTerm(...) is not in the right format, then I have no clue.

ice1000 commented 3 years ago

@by-cloud Can you print result and check it

by-cloud commented 3 years ago

Screen Shot 2021-10-23 at 1 50 34 AM

ice1000 commented 3 years ago

@by-cloud How does it cause the error? What's the expected object structure?

by-cloud commented 3 years ago

result.computed should not be <unknown>, instead it should be type information or normal form of the expression,

and result.range.start should not be the same as result.range.end.

The return value of client.sendRequest<ResultType>(...) is not fit for our expectations.

ice1000 commented 3 years ago

hmmmmmmmmmmmmmmmmmm

ice1000 commented 3 years ago

Why is result.computed <unknown>? Can you check the relevant Java code?

imkiva commented 3 years ago

image

imkiva commented 3 years ago

It might be source pos problem

imkiva commented 3 years ago

image

imkiva commented 3 years ago

image

Fixed

imkiva commented 3 years ago

It seems we didn't fix this problem in some cases.