module author Paolo Masci
 *  date copyright import { Connection , TextDocuments , TextDocument , CompletionItem , createConnection , ProposedFeatures , InitializeParams , TextDocumentPositionParams , Hover , CodeLens , CodeLensParams , Diagnostic , Position , Range , DiagnosticSeverity , Definition , Location , TextDocumentChangeEvent , TextDocumentSyncKind , RenameParams , WorkspaceEdit , WorkspaceFolder } from 'vscode-languageserver' ; import { PvsDefinition , FileList , TheoryDescriptor , PvsContextDescriptor , serverEvent , serverRequest , PvsDownloadDescriptor , PvsFileDescriptor , PvsVersionDescriptor , ProofDescriptor , ServerMode , PvsFormula , ProofEditCommand , ProofExecCommand , PvsFile , ContextFolder , PvsTheory , PvsProofCommand , FormulaDescriptor , FileDescriptor , PvsioEvaluatorCommand , EvalExpressionRequest , SearchRequest , SearchResponse , SearchResult , FindSymbolDeclarationRequest , FindSymbolDeclarationResponse , ProveFormulaResponse , ProveFormulaRequest , EvaluatorCommandResponse , SequentDescriptor , DownloadWithProgressRequest , DownloadWithProgressResponse , InstallWithProgressRequest , InstallWithProgressResponse , RebootPvsServerRequest , NASALibDownloader , NASALibDownloaderRequest , NASALibDownloaderResponse , ListVersionsWithProgressRequest , ListVersionsWithProgressResponse , StatusProofChain } from './common/serverInterface' ; import { PvsCompletionProvider } from './providers/pvsCompletionProvider' ; import { PvsDefinitionProvider } from './providers/pvsDefinitionProvider' ; import { PvsHoverProvider } from './providers/pvsHoverProvider' ; import { PvsCodeLensProvider } from './providers/pvsCodeLensProvider' ; import { PvsLinter } from './providers/pvsLinter' ; import { getErrorRange } from './common/languageUtils' ; import * as utils from './common/languageUtils' ; import * as fsUtils from './common/fsUtils' ; import * as path from 'path' ; import { PvsProxy } from './pvsProxy' ; import { PvsResponse , PvsError , ImportingDecl , TypedDecl , FormulaDecl , PvsResult } from './common/pvs-gui' ; import { PvsPackageManager } from './providers/pvsPackageManager' ; import { PvsIoProxy } from './pvsioProxy' ; import { PvsErrorManager } from './pvsErrorManager' ; import { ProcessCode } from './pvsProcess' ; import { PvsProofExplorer } from './providers/pvsProofExplorer' ; import { PvsRenameProvider } from './providers/pvsRenameProvider' ; import { PvsSearchEngine } from './providers/pvsSearchEngine' ; import { getOs } from './common/fsUtils' ; export declare interface PvsTheoryDescriptor { id ? : string ; /**
     * an array of declarations in the given theory
     */ decls ? : ( ImportingDecl | TypedDecl | FormulaDecl ) [ ] ; } export declare interface ContextDiagnostics { [ fileName ] : { pvsResponse : PvsResponse ; isTypecheckError : boolean ; } ; } ; interface Settings { maxNumberOfProblems : number ; } export class PvsLanguageServer { protected MAX_PARALLEL_PROCESSES : number = 1 ; readonly MIN_PVS_VERSION : number = 7.1 ; protected diags : ContextDiagnostics = { } ; protected pvsPath : string ; protected pvsLibraryPath : string ; protected pvsVersionDescriptor : PvsVersionDescriptor ; protected timers : { [ key ] : NodeJS . Timer ; } = { } ; protected pvsProxy : PvsProxy ; protected pvsioProxy : PvsIoProxy ; protected connection : Connection ; protected documents : TextDocuments ; protected clientCapabilities : { hasConfigurationCapability : boolean ; hasWorkspaceFolderCapability : boolean ; hasDiagnosticRelatedInformationCapability : boolean ; } ; protected settings : { global : Settings ; documents : Map < string , Thenable < Settings > > ; } ; /**
     * Service providers necessary to support the language server APIs
     */ protected completionProvider : PvsCompletionProvider ; protected definitionProvider : PvsDefinitionProvider ; protected hoverProvider : PvsHoverProvider ; protected codeLensProvider : PvsCodeLensProvider ; protected renameProvider : PvsRenameProvider ; protected linter : PvsLinter ; protected proofExplorer : PvsProofExplorer ; protected pvsSearchEngine : PvsSearchEngine ; pvsErrorManager : PvsErrorManager ; /**
     * Data structures used for performance improvements
     */ protected lastParsedContext : string = "" ; constructor constructor ( ) { this . settings = { global : { maxNumberOfProblems : 1000 } , documents : new Map ( ) } ; this . clientCapabilities = { hasConfigurationCapability : false , hasWorkspaceFolderCapability : false , hasDiagnosticRelatedInformationCapability : false } ; try { this . connection = createConnection ( ProposedFeatures . all ) ; this . setupConnectionManager ( ) ; this . setupDocumentsManager ( this . connection ) ; this . connection ?. listen ( ) ; } catch ( connectionError ) { console . warn ( `[pvs-server] Warning: Unable to create LSP connection with client front-end` ) ; } finally { this . pvsErrorManager = new PvsErrorManager ( this . connection ) ; } } getPvsProxy ( ) { return this . pvsProxy ; } getPvsPath ( ) { return this . pvsPath ? `${ this . pvsPath }` : "" ; } getNasalibPath ( ) { return this . pvsPath ? path . join ( this . pvsPath , "nasalib" ) : "" ; } protected notifyStartExecution ( desc ) { this . connection ?. sendNotification ( "server.status.progress" , desc ) ; } protected notifyEndExecution ( desc ? ) { this . connection ?. sendNotification ( "server.status.info" , desc ) ; } protected notifyStartImportantTask ( desc ) { this . connection ?. sendNotification ( `server.status.start-important-task` , desc ) ; } protected notifyProgressImportantTask ( desc ) { this . connection ?. sendNotification ( `server.status.progress-important-task-${ desc . id }` , desc ) ; } protected notifyEndImportantTask ( desc ) { this . connection ?. sendNotification ( `server.status.end-important-task-${ desc . id }` , desc ) ; } notifyEndImportantTaskWithErrors ( desc ) { this . connection ?. sendNotification ( `server.status.end-important-task-${ desc . id }-with-errors` , desc ) ; } protected notifyMessage ( desc ) { this . connection ?. sendNotification ( "server.status.warning" , desc ) ; } param contextFolder protected isSameWorkspace ( contextFolder ) { if ( this . lastParsedContext ) { return contextFolder === this . lastParsedContext || contextFolder === path . join ( this . lastParsedContext , "pvsbin" ) ; } return false ; } getConnection ( ) { return this . connection ; } param args async startProof ( args ) { return await this . proveFormula ( args ) ; } async proveFormula ( formula ) { if ( formula && formula . fileName && formula . formulaName && formula . fileExtension && formula . contextFolder && formula . theoryName ) { const mode = await this . getMode ( ) ; if ( mode !== "lisp" ) { await this . quitProof ( ) ; } try { formula = fsUtils . decodeURIComponents ( formula ) ; const useLispInterface = true ; const response = await this . pvsProxy ?. proveFormula ( formula , { useLispInterface } ) ; this . connection ?. sendNotification ( serverEvent . profilerData , `(prove-formula "${ path . join ( formula . contextFolder , formula . fileName + ".pvs" + "#" + formula . theoryName ) }")` ) ; return response ; } catch ( ex ) { console . error ( '[pvs-language-server.proveFormula] Error: pvsProxy has thrown an exception' , ex ) ; return null ; } } return null ; } async getMode ( ) { return await this . pvsProxy ?. getMode ( ) ; } async getImportChainTheoremsRequest ( theory ) { if ( this . pvsProxy ) { const res = await this . typecheckFile ( theory ) ; if ( res && ! res . error ) { const theorems = await this . pvsProxy ?. getTheorems ( theory , { includeImportChain : true } ) ; this . connection ?. sendRequest ( serverEvent . getImportChainTheoremsResponse , { theorems } ) ; } else { this . connection ?. sendRequest ( serverEvent . getImportChainTheoremsResponse , null ) ; } } } async getTheoremsRequest ( theory ) { if ( this . pvsProxy ) { const res = await this . typecheckFile ( theory ) ; if ( res && ! res . error ) { const theorems = await this . pvsProxy ?. getTheorems ( theory ) ; this . connection ?. sendRequest ( serverEvent . getTheoremsResponse , { theorems } ) ; } else { if ( res && res . error && res . error . data ) { const fname = ( res . error . data . file_name ) ? res . error . data . file_name : fsUtils . desc2fname ( theory ) ; const msg = `Typecheck errors in ${ fname }${ res . error . data . error_string ? ":" + res . error . data . error_string : "" }` ; this . connection ?. sendRequest ( serverEvent . getTheoremsResponse , { error : msg } ) ; } } } } async getTccsRequest ( theory ) { if ( this . pvsProxy ) { const res = await this . typecheckFile ( theory ) ; if ( res && ! res . error ) { const theorems = await this . pvsProxy ?. getTheorems ( theory , { tccsOnly : true } ) ; this . connection ?. sendRequest ( serverEvent . getTccsResponse , { theorems } ) ; } else { if ( res && res . error && res . error . data ) { const fname = ( res . error . data . file_name ) ? res . error . data . file_name : fsUtils . desc2fname ( theory ) ; const msg = `Typecheck errors in ${ fname }${ res . error . data . error_string ? ":" + res . error . data . error_string : "" }` ; this . connection ?. sendRequest ( serverEvent . getTccsResponse , { error : msg } ) ; } } } } /**
     * Handler for prove formula requests
     */ async proveFormulaRequest ( desc , opt ? ) { opt = opt || { } ; if ( desc && desc . formulaName && desc . theoryName && desc . fileName && desc . contextFolder ) { desc = fsUtils . decodeURIComponents ( desc ) ; const mode = await this . getMode ( ) ; if ( mode !== "lisp" ) { if ( this . proofExplorer ?. proofIsDirty ( ) && ! opt . autorun && ! opt . skipSave ) { await this . proofExplorer ?. quitProofAndSave ( ) ; } else { await this . quitProof ( ) ; } } const fname = fsUtils . desc2fname ( desc ) ; if ( desc . fileExtension === ".pvs" && desc . origin !== "prooflite" && ! fsUtils . fileExists ( fname ) ) { this . notifyMessage ( { msg : `Warning: file ${ fname } does not exist. (source: Prover)` } ) ; return ; } const taskId = `typecheck-${ desc . formulaName }` ; if ( ! opt . autorun ) { this . proofExplorer ?. resetFlags ( ) ; this . notifyStartImportantTask ( { id : taskId , msg : `Starting prover session for formula '${ desc . formulaName }'` } ) ; } if ( desc . fileExtension ) { const response = await this . typecheckFile ( { contextFolder : desc . contextFolder , fileName : desc . fileName , fileExtension : ".pvs" } , opt ) ; if ( response && response . error ) { const fname = ( response . error . data . file_name ) ? response . error . data . file_name : fsUtils . desc2fname ( desc ) ; this . diags [ fname ] = { pvsResponse : response , isTypecheckError : true } ; this . sendDiagnostics ( "Typecheck" ) ; if ( this . pvsErrorManager ) { this . pvsErrorManager ?. handleTypecheckError ( { request : desc , response : < PvsError > response , taskId } ) ; this . pvsErrorManager ?. handleProveFormulaError ( { request : desc , response : < PvsError > response , taskId } ) ; } return ; } } await this . proofExplorer ?. loadProofRequest ( desc , opt ) ; const response = await this . proveFormula ( desc ) ; if ( response ?. result ) { const result = response . result ; if ( result && result . length ) { this . notifyServerMode ( "in-checker" ) ; this . proofExplorer ?. loadInitialSequent ( result [ 0 ] ) ; this . proofExplorer ?. startProof ( { autorun : ! ! opt . autorun } ) ; if ( result . length > 1 ) { for ( let i = 1 ; i < response . result . length ; i ++ ) { const proofState = response . result [ i ] ; await this . proofExplorer ?. onStepExecutedNew ( { proofState , lastSequent : i === response . result . length - 1 } , { feedbackToTerminal : true } ) ; } } if ( ! opt . autorun ) { this . notifyEndImportantTask ( { id : taskId } ) ; const ans = { res : result [ 0 ] , req : desc , mathObjects : this . pvsProxy ?. listMathObjects ( ) } ; this . connection ?. sendRequest ( serverEvent . proveFormulaResponse , ans ) ; } else { const msg = opt . useJprf ? `Re-running J-PRF proof for ${ desc . formulaName }` : `Re-running proof for ${ desc . formulaName }` ; this . connection ?. sendNotification ( "pvs.progress-info" , msg ) ; } } } else { if ( this . pvsErrorManager ) { this . pvsErrorManager ?. handleProveFormulaError ( { request : desc , response : < PvsError > response , taskId , autorun : opt . autorun } ) ; } else { console . error ( response ) ; } } } else { if ( this . pvsErrorManager ) { this . pvsErrorManager ?. handleProveFormulaError ( { request : desc , response : null , taskId : null , autorun : opt . autorun } ) ; } else { console . error ( `[pvs-language-server] Warning: Unable to prove formula` , desc ) ; } } } /**
     * Eval expression request handler -- this is used for one-shot evaluation requests in pvsio
     */ async evalExpressionRequest ( req ) { req = fsUtils . decodeURIComponents ( req ) ; const workspaceFolders = await this . connection ?. workspace ?. getWorkspaceFolders ( ) ; const res = await this . pvsioProxy ?. evalExpression ( req , { workspaceFolders , pvsLibraryPath : this . pvsLibraryPath } ) ; this . connection ?. sendNotification ( serverRequest . evalExpression , { req , res } ) ; } /**
     * Evaluator command handler -- this is used during interactive pvsio sessions
     */ async pvsioEvaluatorCommandRequest ( req ) { req = fsUtils . decodeURIComponents ( req ) ; const response = await this . pvsioProxy ?. evalCommand ( req , { cb : ( res , state ) => { const data = { req , res , state } ; this . connection . sendRequest ( serverEvent . evaluatorCommandResponse , data ) ; } } ) ; if ( response && response . error ) { this . pvsErrorManager ?. handleEvaluationError ( { request : req , response : < PvsError > response } ) ; } } /**
     * Quit pvsio evaluator request handler
     */ async quitEvaluatorRequest ( theory ) { await this . pvsioProxy ?. quitEvaluator ( theory ) ; } /**
     * Start pvsio evaluator request handler
     */ async startEvaluatorRequest ( theory ) { theory . fileExtension = ".pvs" ; const mode = await this . getMode ( ) ; if ( mode !== "lisp" ) { return ; } theory = fsUtils . decodeURIComponents ( theory ) ; const taskId = `pvsio-${ theory . fileName }@${ theory . theoryName }` ; this . notifyStartImportantTask ( { id : taskId , msg : `Loading files necessary to evaluate theory ${ theory . theoryName }` } ) ; const response = await this . typecheckFile ( theory ) ; if ( response && response . result ) { let pvsioResponse = await this . pvsioProxy ?. startEvaluator ( theory , { pvsLibraryPath : this . pvsLibraryPath } ) ; this . connection ?. sendRequest ( serverEvent . startEvaluatorResponse , { response : pvsioResponse , args : theory } ) ; this . notifyEndImportantTask ( { id : taskId , msg : "PVSio evaluator session ready!" } ) ; this . notifyServerMode ( "pvsio" ) ; } else { this . connection ?. sendRequest ( serverEvent . startEvaluatorResponse , { error : response ?. error ?. data ?. error_string , args : theory } ) ; this . pvsErrorManager ?. handleEvaluationError ( { request : theory , response : < PvsError > response , taskId } ) ; } } /**
     * Sends to the client the prooflite script associated with the formula indicated in the request
     */ async showProofLiteRequest ( formula ) { if ( formula && this . connection ) { formula = fsUtils . decodeURIComponents ( formula ) ; const pdesc = await this . openProof ( formula ) ; const proofFile = await this . pvsProxy ?. saveProoflite ( { fileName : formula . fileName , fileExtension : ".prl" , contextFolder : formula . contextFolder , theoryName : formula . theoryName , formulaName : formula . formulaName , proofDescriptor : pdesc } ) ; this . connection ?. sendNotification ( serverRequest . showProofLite , { response : { proofFile } , args : formula } ) ; } } /**
     * Internal function, loads the proof script for the formula indicated in the request
     */ protected async openProof ( formula ) { if ( this . pvsProxy ) { return await this . pvsProxy ?. openProofFile ( { fileName : formula . fileName , fileExtension : ".prf" , contextFolder : formula . contextFolder } , formula ) ; } console . error ( `[pvs-language-server] Error: Could not load proof script (pvs-proxy is null)` ) ; return null ; } /**
     * Typecheck file
     */ async typecheckFile ( args , opt ? ) { opt = opt || { } ; if ( args && args . fileName && args . fileExtension && args . contextFolder ) { try { args = fsUtils . decodeURIComponents ( args ) ; const response = await this . pvsProxy ?. typecheckFile ( args , opt ) ; if ( response ) { if ( response . result ) { const fname = fsUtils . desc2fname ( args ) ; this . diags [ fname ] = { pvsResponse : response , isTypecheckError : true } ; if ( ! opt ?. quiet ) { this . sendDiagnostics ( "Typecheck" ) ; } } else { if ( response . error ?. data ) { const fname = ( response . error . data . file_name ) ? response . error . data . file_name : fsUtils . desc2fname ( args ) ; this . diags [ fname ] = { pvsResponse : response , isTypecheckError : true } ; this . sendDiagnostics ( "Typecheck" ) ; } } } this . pvsioProxy . clearCache ( ) ; return response ; } catch ( ex ) { console . error ( '[pvs-language-server.typecheckFile] Error: pvsProxy has thrown an exception' , ex ) ; return null ; } } return null ; } /**
     * Typecheck file request handler
     */ async typecheckFileRequest ( request ) { const mode = await this . getMode ( ) ; if ( mode !== "lisp" ) { return ; } if ( request ) { request = fsUtils . decodeURIComponents ( request ) ; if ( request ) { request . fileExtension = ".pvs" ; const fname = fsUtils . desc2fname ( request ) ; if ( ! fsUtils . fileExists ( fname ) ) { this . notifyMessage ( { msg : `Warning: file ${ fname } does not exist. (source: Typechecker)` } ) ; return ; } const taskId = `typecheck-${ fname }` ; this . notifyStartImportantTask ( { id : taskId , msg : `Typechecking ${ fname }` } ) ; const response = await this . typecheckFile ( request ) ; this . connection ?. sendRequest ( serverEvent . typecheckFileResponse , { response , args : request } ) ; if ( response ) { if ( response . result ) { this . notifyEndImportantTask ( { id : taskId , msg : `${ request . fileName }${ request . fileExtension } typechecks successfully!` } ) ; const cdesc = await this . getContextDescriptor ( { contextFolder : request . contextFolder } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; } else { this . pvsErrorManager ?. handleTypecheckError ( { response : < PvsError > response , taskId , request } ) ; } } } else { console . error ( "[pvs-language-server] Warning: pvs.typecheck-file is unable to identify filename for " , request ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.typecheck-file invoked with null request" ) ; } } /**
     * Generate theory summary file request handler
     */ async generateTheorySummaryRequest ( request , opt ? ) { opt = opt || { } ; if ( request ) { const fileContent = request . fileContent || "" ; const contextFolder = request . contextFolder ; const fileName = request . fileName ; const fileExtension = ".summary" ; await fsUtils . deleteFile ( fsUtils . desc2fname ( { contextFolder , fileName , fileExtension } ) ) ; await fsUtils . saveSummary ( fsUtils . desc2fname ( { contextFolder , fileName , fileExtension } ) , request . theoryName , fileContent ) ; if ( opt . showSummaryRequest ) { this . connection ?. sendRequest ( serverEvent . showTheorySummaryResponse , { response : { contextFolder , fileName , fileExtension , fileContent } , args : request } ) ; } } } /**
     * Generate workspace summary file request handler
     */ async generateWorkspaceSummaryRequest ( req , opt ? ) { opt = opt || { } ; if ( req ) { const fileContent = req . fileContent || "" ; const contextFolder = req . contextFolder ; const fileName = req . fileName ; const fileExtension = ".workspace.summary" ; await fsUtils . writeFile ( fsUtils . desc2fname ( { contextFolder , fileName , fileExtension } ) , fileContent ) ; if ( opt . showSummaryRequest ) { const res = { contextFolder , fileName , fileExtension , fileContent } ; this . connection ?. sendNotification ( serverRequest . showWorkspaceSummary , { res , req } ) ; } } } /**
     * Generate tccs file request handler
     */ async generateTccsRequest ( request , opt ? ) { request = fsUtils . decodeURIComponents ( request ) ; if ( request && this . pvsProxy ) { opt = opt || { } ; const desc = ( typeof request === "string" ) ? fsUtils . fname2desc ( request ) : request ; if ( desc ) { const fname = fsUtils . desc2fname ( { contextFolder : desc . contextFolder , fileName : desc . fileName , fileExtension : ".pvs" } ) ; const shortName = `${ desc . fileName }.pvs` ; const taskId = `generate-tcc-for-${ fname }` ; if ( ! opt . quiet ) { this . notifyStartImportantTask ( { id : taskId , msg : `Generating typecheck conditions for ${ shortName }` } ) ; } const response = await this . pvsProxy ?. generateTccs ( desc ) ; this . connection ?. sendRequest ( ( opt . showTccsRequest ) ? serverEvent . showTccsResponse : serverEvent . generateTccsResponse , { response , args : request } ) ; let nTccs = 0 ; let nProved = 0 ; if ( response && response . fileDescriptors && response . fileDescriptors [ fname ] && response . fileDescriptors [ fname ] . theories ) { const theories = response . fileDescriptors [ fname ] . theories ; for ( let i = 0 ; i < theories . length ; i ++ ) { if ( theories [ i ] . theorems && theories [ i ] . theorems . length ) { nTccs += theories [ i ] . theorems . filter ( ( elem ) => { return elem . formulaName ; } ) . length ; for ( let j = 0 ; j < theories [ i ] . theorems . length ; j ++ ) { if ( utils . isProved ( theories [ i ] . theorems [ j ] . status ) ) { nProved ++ ; } } } } const cdesc = await this . getContextDescriptor ( { contextFolder : request . contextFolder } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; } else { console . warn ( "[pvs-language-server] Warning: generate-tccs-request returned error" , response ) ; } if ( ! opt . quiet ) { const msg = `${ nTccs } tccs generated for ${ shortName } (${ nProved } proved, ${ nTccs - nProved } to be proved)` ; this . notifyEndImportantTask ( { id : taskId , msg } ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.generate-tccs is unable to identify filename for " , request ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.generate-tccs invoked with null request" ) ; } } /**
     * Parse file
     */ async parseFile ( args ) { args = fsUtils . decodeURIComponents ( args ) ; if ( args && args . fileName && args . fileExtension && args . contextFolder ) { const enableEParser = ! ! ( this . connection && await this . connection ?. workspace . getConfiguration ( "pvs.xtras.enableAntlrParser" ) ) ; try { return await this . pvsProxy ?. parseFile ( args , { enableEParser } ) ; } catch ( ex ) { console . error ( '[pvs-language-server.parseFile] Error: pvsProxy has thrown an exception' , ex ) ; return null ; } } return null ; } /**
     * Parse file request handler
     */ async statusProofChainRequest ( req ) { await this . typecheckFile ( req ) ; await this . generateTccsRequest ( req ) ; const ans = await this . pvsProxy ?. statusProofChain ( req ) ; const res = { message : ans ?. result || ans ?. error ?. message } ; this . connection ?. sendNotification ( serverRequest . statusProofChain , { req , res } ) ; } /**
     * Parse file request handler
     */ async parseFileRequest ( request , opt ? ) { const mode = await this . getMode ( ) ; if ( mode !== "lisp" ) { return ; } request = fsUtils . decodeURIComponents ( request ) ; if ( request ) { opt = opt || { } ; if ( request ) { if ( fsUtils . isPvsFile ( request ) && ! fsUtils . isSummaryFile ( request ) && ! fsUtils . isProofliteFile ( request ) && ! this . isPreludeFile ( request ) ) { if ( request . contextFolder === path . join ( this . lastParsedContext , "pvsbin" ) ) { return ; } request . fileExtension = ".pvs" ; this . lastParsedContext = request . contextFolder ; const cdesc = await this . getContextDescriptor ( { contextFolder : request . contextFolder } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; const fname = fsUtils . desc2fname ( request ) ; if ( ! fsUtils . fileExists ( fname ) ) { this . notifyMessage ( { msg : `Warning: file ${ fname } does not exist. (source: Parser)` } ) ; return ; } const taskId = `parse-${ fname }` ; if ( opt . withFeedback ) { this . notifyStartImportantTask ( { id : taskId , msg : `Parsing file ${ fname }` } ) ; } const contextFiles = await fsUtils . listPvsFiles ( request . contextFolder ) ; if ( contextFiles && contextFiles . fileNames ) { const nfiles = contextFiles . fileNames . length ; this . connection ?. sendRequest ( serverEvent . workspaceStats , { contextFolder : request . contextFolder , files : nfiles } ) ; } const response = await this . parseFile ( request ) ; let source = "Parse" ; if ( response ) { this . connection ?. sendRequest ( serverEvent . parseFileResponse , response ) ; if ( this . diags [ fname ] && this . diags [ fname ] . isTypecheckError ) { source = "Typecheck" ; } else { this . diags [ fname ] = { pvsResponse : response , isTypecheckError : false } ; } if ( opt . withFeedback ) { if ( response . error ) { this . notifyEndImportantTaskWithErrors ( { id : taskId , msg : `${ source } errors in ${ request . fileName }${ request . fileExtension }` } ) ; } else { this . notifyEndImportantTask ( { id : taskId , msg : `${ request . fileName }${ request . fileExtension } parsed successfully!` } ) ; } } } this . sendDiagnostics ( source ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.parse-file is unable to identify filename for " , request ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.parse-file invoked with null request" ) ; } } /**
     * Internal function, implements common code for workspace actions request handlers (parse-workspace, typecheck-workspace)
     */ protected async workspaceActionRequest ( action , request , opt ? ) { opt = opt || { } ; return new Promise ( async ( resolve , reject ) => { request = fsUtils . decodeURIComponents ( request ) ; if ( action === "typecheck-workspace" ) { this . diags = { } ; } if ( request ) { const actionId = opt . actionId || action ; const contextFolder = ( typeof request === "string" ) ? request : request . contextFolder ; let success = true ; const taskId = `${ actionId }-${ contextFolder }` ; const workspaceName = fsUtils . getContextFolderName ( contextFolder ) ; const actionFriendlyName = action === "parse-workspace" ? "Parse" : "Typecheck" ; const actionFriendlyNamePast = action === "parse-workspace" ? "Parsed" : "Typechecked" ; const actionFriendlyNameContinuous = action === "parse-workspace" ? "Parsing" : "Typechecking" ; if ( opt . withFeedback ) { const msg = opt . msg || `${ actionFriendlyNameContinuous } workspace ${ workspaceName }` ; if ( ! opt . suppressDialogCreation ) { this . notifyStartImportantTask ( { id : taskId , msg } ) ; } else { this . notifyProgressImportantTask ( { id : taskId , msg , increment : - 1 } ) ; } } if ( contextFolder ) { if ( ! this . isSameWorkspace ( contextFolder ) ) { this . lastParsedContext = contextFolder ; } const cdesc = await this . getContextDescriptor ( { contextFolder } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; const contextFiles = await fsUtils . listPvsFiles ( contextFolder ) ; if ( contextFiles && contextFiles . fileNames && contextFiles . fileNames . length ) { const nfiles = contextFiles . fileNames . length ; let completed = 0 ; const msg = opt . msg || `${ actionFriendlyNameContinuous } workspace ${ workspaceName } (0/${ nfiles } files processed)` ; this . notifyProgressImportantTask ( { id : taskId , msg , increment : - 1 } ) ; console . log ( msg ) ; this . connection ?. sendRequest ( serverEvent . workspaceStats , { contextFolder , files : nfiles } ) ; let next_file_index = this . MAX_PARALLEL_PROCESSES ; let completed_tasks = 0 ; let errors = [ ] ; const actionFunction = ( action === "parse-workspace" ) ? "parseFile" : "typecheckFile" ; const workspaceActionAux = async ( actionName , desc ) => { const response = await this [ actionName ] ( desc ) ; completed_tasks ++ ; if ( response && response . error ) { if ( response . error . message ) { errors . push ( `${ actionFriendlyName } error in file ${ desc . fileName }${ desc . fileExtension }: ${ response . error . message }` ) ; } else if ( response . error . data && response . error . data . error_string ) { let error_msg = `${ actionFriendlyName } error in file ${ desc . fileName }${ desc . fileExtension }` ; if ( response . error . data . place && response . error . data . place . length > 1 ) { error_msg += ` (Ln ${ response . error . data . place [ 0 ] }, Col ${ response . error . data . place [ 1 ] })` ; } error_msg += ": " + response . error . data . error_string ; errors . push ( error_msg ) ; } } if ( response ) { if ( opt . generateTCCs ) { await this . pvsProxy . generateTccs ( desc ) ; } completed ++ ; if ( opt . withFeedback ) { const msg = opt . msg || `${ actionFriendlyNameContinuous } workspace ${ workspaceName } (${ completed }/${ nfiles } files processed)` ; console . log ( msg ) ; if ( opt . keepDialogOpen ) { this . notifyProgressImportantTask ( { id : taskId , msg , increment : - 1 } ) ; } else { this . notifyProgressImportantTask ( { id : taskId , msg , increment : 1 / nfiles * 100 } ) ; } } this . connection ?. sendRequest ( serverEvent . workspaceStats , { contextFolder : response . contextFolder , fileName : response . fileName , fileExtension : response . fileExtension , files : nfiles , "math-objects" : response [ "math-objects" ] } ) ; } const fname = fsUtils . desc2fname ( desc ) ; const diag_fname = ( response && response . error && response . error . data && response . error . data . file_name ) ? response . error . data . file_name : fname ; let source = actionFriendlyName ; if ( action === "typecheck-workspace" ) { this . diags [ diag_fname ] = { pvsResponse : response , isTypecheckError : true } ; } else if ( action === "parse-workspace" ) { if ( this . diags [ diag_fname ] && this . diags [ fname ] . isTypecheckError ) { source = "Typecheck" ; } else { this . diags [ diag_fname ] = { pvsResponse : response , isTypecheckError : false } ; } } this . sendDiagnostics ( source ) ; if ( completed_tasks >= contextFiles . fileNames . length ) { if ( opt . withFeedback ) { if ( errors . length ) { success = false ; let msg = ( opt . suppressFinalMessage ) ? "" : ( opt . msg ) ? opt . msg : ( errors . length === 1 ) ? errors [ 0 ] : `Workspace ${ workspaceName } contains ${ actionFriendlyName . toLocaleLowerCase ( ) } errors` ; this . notifyEndImportantTaskWithErrors ( { id : taskId , msg } ) ; } else { if ( ! opt . keepDialogOpen ) { const msg = ( opt . suppressFinalMessage ) ? "" : opt . msg || `Workspace ${ workspaceName } ${ actionFriendlyNamePast . toLocaleLowerCase ( ) } successfully (${ completed } files processed)` ; this . notifyEndImportantTask ( { id : taskId , msg } ) ; } } } resolve ( success ) ; } else { if ( next_file_index < contextFiles . fileNames . length ) { const fname = path . join ( contextFolder , contextFiles . fileNames [ next_file_index ++ ] ) ; const fileName = fsUtils . getFileName ( fname ) ; const fileExtension = fsUtils . getFileExtension ( fname ) ; await workspaceActionAux ( actionName , { fileName , fileExtension , contextFolder } ) ; } } } ; if ( contextFiles . fileNames . length ) { for ( let i = 0 ; i < this . MAX_PARALLEL_PROCESSES && i < contextFiles . fileNames . length ; i ++ ) { const fname = path . join ( contextFolder , contextFiles . fileNames [ i ] ) ; const fileName = fsUtils . getFileName ( fname ) ; const fileExtension = fsUtils . getFileExtension ( fname ) ; workspaceActionAux ( actionFunction , { fileName , fileExtension , contextFolder } ) ; } } else { resolve ( success ) ; } } else { console . log ( `[pvs-language-server] Workspace ${ workspaceName } does not contain pvs files` ) ; if ( ! opt . keepDialogOpen ) { const msg = ( opt . suppressFinalMessage ) ? "" : ( opt . msg ) ? opt . msg : `Workspace ${ workspaceName } ${ actionFriendlyNamePast . toLocaleLowerCase ( ) } (0 files processed)` ; this . notifyEndImportantTask ( { id : taskId , msg } ) ; } resolve ( success ) ; } } else { console . warn ( `[pvs-language-server] Warning: workspace name is null` ) ; resolve ( false ) ; } } else { console . error ( `[pvs-language-server] Warning: pvs.${ action } invoked with null request` ) ; resolve ( false ) ; } } ) ; } /**
     * Parse workspace request handler
     */ async parseWorkspaceRequest ( request , opt ? ) { request = fsUtils . decodeURIComponents ( request ) ; await this . workspaceActionRequest ( "parse-workspace" , request , opt ) ; } /**
     * Typecheck workspace request handler
     */ async typecheckWorkspaceRequest ( request , opt ? ) { request = fsUtils . decodeURIComponents ( request ) ; const success = await this . workspaceActionRequest ( "typecheck-workspace" , request , opt ) ; this . connection . sendRequest ( serverEvent . typecheckWorkspaceResponse , { args : request , success } ) ; } /**
     * Utility function, returns the list of pvs files in a given context folder
     */ async listContextFiles ( args ) { args = fsUtils . decodeURIComponents ( args ) ; if ( args && args . contextFolder ) { return await fsUtils . listPvsFiles ( args . contextFolder ) ; } return null ; } /**
     * List context files request handler
     */ async listContextFilesRequest ( request ) { request = fsUtils . decodeURIComponents ( request ) ; const args = ( typeof request === "string" ) ? { contextFolder : request } : request ; if ( args && args . contextFolder ) { const response = await this . listContextFiles ( args ) ; this . connection ?. sendRequest ( serverEvent . listContextResponse , response ) ; } } /**
     * Utility function, returns the proof status for all theorems in a given theory
     */ async statusProofTheory ( args ) { args = fsUtils . decodeURIComponents ( args ) ; return await this . pvsProxy ?. statusProofTheory ( args ) ; } /**
     * Utility function, returns the proof status for all theorems in a given file
     */ async statusProof ( args ) { args = fsUtils . decodeURIComponents ( args ) ; let res = { } ; const fname = fsUtils . desc2fname ( args ) ; const theories = await fsUtils . listTheoriesInFile ( fname ) ; for ( let i = 0 ; i < theories . length ; i ++ ) { const proofStatus = await this . statusProofTheory ( { contextFolder : args . contextFolder , fileName : args . fileName , fileExtension : args . fileExtension , theoryName : theories [ i ] . theoryName } ) ; if ( proofStatus && proofStatus . response ) { res [ fname ] = proofStatus ; } else { console . error ( "[pvs-language-server] Warning: status proof indicates error for theory " , theories [ i ] . theoryName ) ; } } return res ; } /**
     * Returns a descriptor containing information about theories in the prelude
     */ async getPreludeDescriptor ( ) { return await this . cachePreludeDescriptor ( ) ; } /**
     * Returns a descriptor with information on all theories in a given context folder
     */ async getContextDescriptor ( args ) { if ( args && args . contextFolder ) { args = fsUtils . decodeURIComponents ( args ) ; if ( this . pvsProxy ) { if ( this . pvsProxy ?. isProtectedFolder ( args . contextFolder ) ) { return await this . getPreludeDescriptor ( ) ; } const contextFolder = ( args . contextFolder . endsWith ( "pvsbin" ) || args . contextFolder . endsWith ( "pvsbin/" ) ) ? path . join ( args . contextFolder , ".." ) : args . contextFolder ; const desc = await fsUtils . getContextDescriptor ( contextFolder , { listTheorems : true , includeTccs : true } ) ; return desc ; } else { console . error ( '[pvs-language-server.listTheories] Error: pvs proxy is null' ) ; } } else { console . warn ( '[pvs-language-server.listTheories] Warning: getContextDescriptor invoked with null descriptor' ) ; } return null ; } /**
     * Returns a descriptor with information on all theories in a given file
     */ async getFileDescriptor ( desc , opt ? ) { if ( desc ) { desc = fsUtils . decodeURIComponents ( desc ) ; opt = opt || { } ; if ( this . pvsProxy ) { if ( this . pvsProxy ?. isProtectedFolder ( desc . contextFolder ) ) { const cdesc = await this . getPreludeDescriptor ( ) ; if ( cdesc ) { return cdesc [ fsUtils . desc2fname ( desc ) ] ; } else { console . error ( '[pvs-language-server.listTheories] Error: could not read file descriptor for protected file ' , desc ) ; return null ; } } const fname = fsUtils . desc2fname ( desc ) ; return await fsUtils . getFileDescriptor ( fname , { ... opt , prelude : this . isPreludeFile ( fname ) } ) ; } else { console . error ( '[pvs-language-server.listTheories] Error: pvs proxy is null' ) ; } } else { console . error ( '[pvs-language-server.listTheories] Error: getContextDescriptor invoked with null descriptor' ) ; } return null ; } async hp2pvs ( args ) { args = fsUtils . decodeURIComponents ( args ) ; if ( args && args . fileName && args . fileExtension && args . contextFolder ) { try { return await this . pvsProxy ?. hp2pvs ( args ) ; } catch ( ex ) { console . error ( '[pvs-language-server.generatePvsFile] Error: pvsProxy has thrown an exception' , ex ) ; return null ; } } return null ; } async prettyPrintDdlRequest ( args ) { args = fsUtils . decodeURIComponents ( args ) ; if ( args && args . expr ) { const res = await this . pvsProxy ?. prettyPrintDdl ( args ) ; } } async hp2pvsRequest ( request ) { request = fsUtils . decodeURIComponents ( request ) ; if ( request ) { const desc = ( typeof request === "string" ) ? fsUtils . fname2desc ( request ) : request ; if ( desc ) { const taskId = `typecheck-${ desc . fileName }${ desc . fileExtension }` ; this . notifyStartImportantTask ( { id : taskId , msg : `Translating hybrid program ${ desc . fileName }${ desc . fileExtension } to PVS` } ) ; const response = await this . hp2pvs ( desc ) ; const fname = fsUtils . desc2fname ( desc ) ; if ( response ) { this . connection ?. sendRequest ( serverEvent . parseFileResponse , response ) ; this . diags [ fname ] = { pvsResponse : response , isTypecheckError : false } ; } this . sendDiagnostics ( "Parse" ) ; if ( response && response . error ) { this . pvsErrorManager ?. notifyEndImportantTaskWithErrors ( { id : taskId , msg : `Error: ${ desc . fileName }.pvs could not be generated -- please check pvs-server output to view errors.` } ) ; } else { this . notifyEndImportantTask ( { id : taskId , msg : `PVS file ${ desc . fileName }.pvs generated successfully!` } ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.parse-file is unable to identify filename for " , request ) ; } } else { console . error ( "[pvs-language-server] Warning: pvs.parse-file invoked with null request" ) ; } } param connection protected setupDocumentsManager ( connection ) { this . documents = new TextDocuments ( ) ; this . documents . onDidClose ( ( close ) => { } ) ; this . documents . onDidSave ( async ( save ) => { if ( save && save . document && save . document . uri && fsUtils . isPvsFile ( save . document . uri ) ) { const contextFolder = fsUtils . getContextFolder ( save . document . uri ) ; const fileName = fsUtils . getFileName ( save . document . uri ) ; const fileExtension = fsUtils . getFileExtension ( save . document . uri ) ; const fname = fsUtils . desc2fname ( { contextFolder , fileName , fileExtension } ) ; delete this . diags [ fname ] ; await this . parseFileRequest ( { fileName , fileExtension , contextFolder } ) ; } } ) ; this . documents . listen ( connection ) ; } /**
     * Internal function, used by restartPvs
     */ protected createServiceProviders ( ) { this . definitionProvider = new PvsDefinitionProvider ( this . pvsProxy , this . documents ) ; this . completionProvider = new PvsCompletionProvider ( this . definitionProvider ) ; this . codeLensProvider = new PvsCodeLensProvider ( this ) ; this . renameProvider = new PvsRenameProvider ( this . connection ) ; this . hoverProvider = new PvsHoverProvider ( this . definitionProvider ) ; this . linter = new PvsLinter ( ) ; this . proofExplorer = new PvsProofExplorer ( this . connection , this . pvsProxy , this ) ; this . pvsSearchEngine = new PvsSearchEngine ( this . connection , this ) ; } /**
     * Utility function, returns the proof explorer instance
     */ getProofExplorer ( ) { return this . proofExplorer ; } /**
     * Internal function, sends diagnostics to the client
     */ protected async sendDiagnostics ( source ? ) { source = source || "" ; const fnames = Object . keys ( this . diags ) ; if ( fnames && fnames . length > 0 ) { for ( let i = 0 ; i < fnames . length ; i ++ ) { let fname = fnames [ i ] ; const response = ( this . diags && this . diags [ fname ] ) ? this . diags [ fname ] . pvsResponse : null ; if ( response && response [ "error" ] ) { const info = < PvsError > response ; if ( info . error && info . error . data && info . error . data . place && info . error . data . place . length >= 2 ) { const errorStart = { line : info . error . data . place [ 0 ] , character : info . error . data . place [ 1 ] } ; const errorEnd = ( info . error . data . place . length > 3 ) ? { line : info . error . data . place [ 2 ] , character : info . error . data . place [ 3 ] } : errorStart ; const txt = await fsUtils . readFile ( fname ) ; if ( txt ) { const errorRange = getErrorRange ( txt , errorStart , errorEnd ) ; const diag = { severity : DiagnosticSeverity . Error , range : { start : { line : errorRange . start . line - 1 , character : errorRange . start . character } , end : { line : errorRange . end . line - 1 , character : errorRange . end . character } , } , message : info . error . data . error_string , source : `\n${ source } error` } ; this . connection ?. sendDiagnostics ( { uri : `file://${ fname }` , diagnostics : [ diag ] } ) ; } else { console . error ( `[pvs-language-server] Warning: unable to send error diagnostics for file ${ fname }` ) ; } } else if ( info . error && info . error . data && info . error . data . length > 0 ) { const diagnostics = < Diagnostic [ ] > info . error . data . map ( diag => { return { range : { start : { line : diag . range . start . line - 1 , character : diag . range . start . character } , end : { line : diag . range . end . line - 1 , character : diag . range . end . character } } , message : diag . message , severity : diag . severity } ; } ) ; this . connection ?. sendDiagnostics ( { uri : `file://${ fname }` , diagnostics } ) ; } } else { this . connection ?. sendDiagnostics ( { uri : `file://${ fname }` , diagnostics : [ ] } ) ; } } } } /**
     * Internal function, reads the content of fileName from disk
     */ protected async readFile ( fileName ) { if ( fileName ) { fileName = decodeURIComponent ( fileName ) ; fileName = fileName . startsWith ( "file://" ) ? fileName = fileName . replace ( "file://" , "" ) : fileName ; const doc = this . documents . get ( "file://" + fileName ) ; if ( doc ) { return doc . getText ( ) ; } try { return fsUtils . readFile ( fileName ) ; } catch ( readError ) { console . error ( `[pvs-language-server] Warning: Error while reading file ${ fileName } (${ readError . message })` ) ; this . connection ?. sendNotification ( "pvs-error" , `Error while reading file ${ fileName } (${ readError . message })` ) ; } } else { console . error ( "[pvs-language-server] Warning: trying to read null filename" ) ; } return null ; } /**
     * Internal function, creates a cache to speed up the creation of the prelude descriptor
     */ protected async cachePreludeDescriptor ( ) { const libPath = path . join ( this . pvsPath , "lib" ) ; const preludeCache = path . join ( libPath , "prelude.cache.json" ) ; const cache = await fsUtils . readFile ( preludeCache ) ; if ( cache ) { try { const res = JSON . parse ( cache ) ; if ( res && res . fileDescriptors ) { for ( let i in res . fileDescriptors ) { const theories = res . fileDescriptors [ i ] . theories ; for ( let t = 0 ; t < theories ?. length ; t ++ ) { const theorems = theories [ t ] . theorems ; for ( let tt = 0 ; tt < theorems ?. length ; tt ++ ) { theorems [ tt ] . status = "proved" ; } } } return res ; } } catch ( jsonError ) { console . warn ( "[pvs-language-server] Warning: unable to parse prelude cache, trying to re-create the file." ) ; } } const cdesc = await fsUtils . getContextDescriptor ( libPath , { prelude : true } ) ; await fsUtils . writeFile ( preludeCache , JSON . stringify ( cdesc , null , " " ) ) ; return cdesc ; } /**
     * Internal function, sends workspace info to the client
     */ protected async sendWorkspaceInfo ( ) { const res = await this . pvsProxy ?. currentContext ( ) ; if ( res && res . result ) { const contextFolder = res . result ; const contextFiles = await fsUtils . listPvsFiles ( contextFolder ) ; const nfiles = contextFiles . fileNames . length ; this . connection ?. sendRequest ( serverEvent . workspaceStats , { contextFolder , files : nfiles } ) ; } } /**
     * Internal function, sends pvs-ready event to the client
     */ protected async sendPvsServerReadyEvent ( ) { const desc = await this . pvsProxy ?. loadPvsVersionInfo ( ) ; if ( desc ) { const pvsVersion = parseFloat ( desc [ "pvs-version" ] ) ; if ( pvsVersion >= this . MIN_PVS_VERSION ) { await this . sendWorkspaceInfo ( ) ; this . pvsVersionDescriptor = desc ; this . connection ?. sendRequest ( serverEvent . pvsServerReady , desc ) ; this . connection ?. sendRequest ( serverEvent . pvsVersionInfo , desc ) ; return true ; } else { console . error ( `[pvs-language-server] Error: incompatible pvs version ${ desc [ "pvs-version" ] }` ) ; this . connection ?. sendRequest ( serverEvent . pvsIncorrectVersion , `Incorrect PVS version ${ desc [ "pvs-version" ] } (vscode-pvs requires pvs ver >= ${ this . MIN_PVS_VERSION })` ) ; } } else { const msg = `PVS executable not found at ${ this . pvsPath }` ; console . error ( msg ) ; this . connection ?. sendRequest ( serverEvent . pvsNotFound , msg ) ; } return false ; } /**
     * Internal function, checks that all dependencies necessary to run pvs are installed
     */ async checkDependencies ( ) { console . log ( `[pvs-server] Checking dependencies...` ) ; const osVersion = getOs ( ) ; if ( osVersion && ( osVersion . version !== "Linux" && osVersion . version !== "MacOSX" ) ) { let msg = `VSCode-PVS currently runs only under Linux or MacOSX.\nPlease use a virtual machine to run VSCode-PVS under ${ osVersion . version }.` ; console . error ( msg ) ; this . pvsErrorManager ?. notifyPvsFailure ( { msg , error_type : "dependency" , src : "pvs-language-server" } ) ; return false ; } if ( ! osVersion || osVersion . error ) { console . error ( osVersion . error ) ; this . pvsErrorManager ?. notifyPvsFailure ( { msg : osVersion . error , error_type : "dependency" , src : "pvs-language-server" } ) ; return false ; } return true ; } /**
     * Utility function, starts pvs-server
     */ async startPvsServer ( desc , opt ? ) { if ( desc ) { opt = opt || { } ; desc = fsUtils . decodeURIComponents ( desc ) ; if ( desc . pvsPath !== this . pvsPath && this . pvsProxy ) { await this . pvsProxy ?. killPvsServer ( ) ; } this . pvsPath = desc . pvsPath || this . pvsPath ; this . pvsLibraryPath = desc . pvsLibraryPath || this . pvsLibraryPath ; const externalServer = ! ! desc . externalServer ; if ( this . pvsPath ) { console . log ( `[pvs-language-server] Rebooting PVS (installation folder is ${ this . pvsPath })` ) ; if ( this . pvsProxy ) { await this . pvsProxy ?. enableExternalServer ( { enabled : externalServer } ) ; await this . pvsProxy ?. restartPvsServer ( { pvsPath : this . pvsPath , pvsLibraryPath : this . pvsLibraryPath , externalServer } ) ; } else { this . pvsProxy = new PvsProxy ( this . pvsPath , { connection : this . connection , pvsLibraryPath : this . pvsLibraryPath , externalServer } ) ; this . pvsioProxy = new PvsIoProxy ( this . pvsPath , { connection : this . connection , pvsLibraryPath : this . pvsLibraryPath } ) ; this . createServiceProviders ( ) ; const success = await this . pvsProxy ?. activate ( { debugMode : opt . debugMode , verbose : opt . debugMode !== false , pvsErrorManager : this . pvsErrorManager } ) ; if ( ! success ) { console . error ( "[pvs-language-server] Error: failed to activate pvs-proxy" ) ; this . connection ?. sendRequest ( serverEvent . pvsNotFound ) ; return false ; } } this . notifyServerMode ( "lisp" ) ; return true ; } else { console . error ( "[pvs-language-server] Error: failed to identify PVS path" ) ; this . connection ?. sendRequest ( serverEvent . pvsNotFound ) ; } } return false ; } param desc protected async startPvsServerRequest ( desc ) { this . checkDependencies ( ) ; await PvsPackageManager . installPvsPatches ( desc ) ; const success = await this . startPvsServer ( desc ) ; if ( success ) { await this . sendPvsServerReadyEvent ( ) ; return true ; } return false ; } /**
     * Internal function, reboots pvs-server
     */ protected async rebootPvsServer ( desc ? ) { desc = desc || { } ; desc . pvsPath = desc . pvsPath || this . pvsPath ; this . checkDependencies ( ) ; if ( this . pvsProxy ) { await this . pvsProxy . rebootPvsServer ( desc ) ; this . notifyServerMode ( "lisp" ) ; await this . sendPvsServerReadyEvent ( ) ; return true ; } else { console . error ( "[pvs-language-server] Error: pvs-proxy is null" ) ; this . connection ?. sendRequest ( serverEvent . pvsNotFound ) ; } return false ; } /**
     * Utility function, quits the prover
     */ async quitProof ( ) { if ( this . pvsProxy ) { await this . pvsProxy ?. quitProof ( ) ; } } param mode notifyServerMode ( mode ) { this . connection ?. sendRequest ( serverEvent . serverModeUpdateEvent , { mode } ) ; } /**
     * Handler for quit proof requests
     */ async quitProofRequest ( ) { await this . quitProof ( ) ; this . connection ?. sendRequest ( serverEvent . quitProofResponse ) ; } /**
     * Utility function, return the file name of the prelude
     */ getPreludeFileName ( ) { return { contextFolder : path . join ( this . pvsPath , "lib" ) , fileName : "prelude" , fileExtension : ".pvs" } ; } /**
     * Utility function, checks if the given file name is the prelude file
     */ isPreludeFile ( desc ) { if ( desc ) { let fname = typeof desc === "string" ? desc : fsUtils . desc2fname ( desc ) ; fname = fname . replace ( "file://" , "" ) ; fname = fsUtils . tildeExpansion ( fname ) ; const prelude = fsUtils . desc2fname ( this . getPreludeFileName ( ) ) ; return fname === prelude ; } return false ; } /**
     * Internal function, used to setup LSP event listeners
     */ protected setupConnectionManager ( ) { this . connection ?. onInitialize ( ( params ) => { const capabilities = params . capabilities ; this . clientCapabilities = { hasConfigurationCapability : capabilities . workspace && ! ! capabilities . workspace . configuration , hasWorkspaceFolderCapability : capabilities . workspace && ! ! capabilities . workspace . workspaceFolders , hasDiagnosticRelatedInformationCapability : capabilities . textDocument && capabilities . textDocument . publishDiagnostics && capabilities . textDocument . publishDiagnostics . relatedInformation } ; return { capabilities : { textDocumentSync : TextDocumentSyncKind . Full , completionProvider : { resolveProvider : true , triggerCharacters : [ '`' , '#' , `\\` , ' ' ] } , hoverProvider : true , codeLensProvider : { resolveProvider : true } , definitionProvider : true , workspaceSymbolProvider : true , renameProvider : true , } } ; } ) ; this . connection ?. onInitialized ( async ( ) => { this . connection ?. onRequest ( serverRequest . cancelOperation , ( ) => { console . log ( `[pvs-server] Operation cancelled by the user` ) ; this . proofExplorer ?. interruptProofCommand ( ) ; } ) ; this . connection ?. onRequest ( serverRequest . getContextDescriptor , ( request ) => { if ( request && request . contextFolder ) { this . getContextDescriptor ( request ) . then ( ( cdesc ) => { this . connection ?. sendRequest ( serverEvent . getContextDescriptorResponse , cdesc ) ; } ) ; } } ) ; this . connection ?. onRequest ( serverRequest . getFileDescriptor , ( request ) => { if ( request && request . contextFolder ) { this . getFileDescriptor ( request ) . then ( ( fdesc ) => { this . connection ?. sendRequest ( serverEvent . getFileDescriptorResponse , fdesc ) ; } ) ; } } ) ; this . connection ?. onRequest ( serverRequest . stopPvsServer , async ( ) => { if ( this . pvsProxy ) { await this . pvsProxy ?. killPvsServer ( ) ; } } ) ; this . connection ?. onRequest ( serverRequest . startPvsServer , async ( request ) => { const success = await this . startPvsServerRequest ( request ) ; if ( success ) { const contextFolder = request . contextFolder ; if ( contextFolder ) { if ( ! this . isSameWorkspace ( contextFolder ) ) { this . lastParsedContext = contextFolder ; } const cdesc = await this . getContextDescriptor ( { contextFolder } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; } } else { console . error ( `[pvs-server] Error: failed to start pvs-server` ) ; this . pvsErrorManager ?. handleStartPvsServerError ( ProcessCode . PVSSTARTFAIL ) ; } } ) ; this . connection ?. onRequest ( serverRequest . rebootPvsServer , async ( req ? ) => { this . rebootPvsServer ( req ) ; } ) ; this . connection ?. onRequest ( serverRequest . clearTheories , async ( ) => { await this . pvsProxy ?. clearTheories ( ) ; } ) ; this . connection ?. onRequest ( serverRequest . parseFile , async ( request ) => { this . parseFileRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . parseFileWithFeedback , async ( request ) => { this . parseFileRequest ( request , { withFeedback : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . parseWorkspace , async ( request ) => { this . parseWorkspaceRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . parseWorkspaceWithFeedback , async ( request ) => { this . parseWorkspaceRequest ( request , { withFeedback : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . typecheckWorkspaceWithFeedback , async ( request ) => { this . typecheckWorkspaceRequest ( request , { withFeedback : true , generateTCCs : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . typecheckWorkspace , async ( request ) => { this . typecheckWorkspaceRequest ( request , { generateTCCs : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . statusProofChain , async ( req ) => { this . statusProofChainRequest ( req ) ; } ) ; this . connection ?. onRequest ( serverRequest . hp2pvs , async ( request ) => { this . hp2pvsRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . typecheckFile , async ( request ) => { this . typecheckFileRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . showTccs , async ( request ) => { this . generateTccsRequest ( request , { quiet : request && request . quiet , showTccsRequest : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . generateTccs , async ( request ) => { this . generateTccsRequest ( request , { quiet : request && request . quiet } ) ; } ) ; this . connection ?. onRequest ( serverRequest . generateTheorySummary , async ( request ) => { this . generateTheorySummaryRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . showTheorySummary , async ( request ) => { this . generateTheorySummaryRequest ( request , { showSummaryRequest : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . generateWorkspaceSummary , async ( request ) => { this . generateWorkspaceSummaryRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . showWorkspaceSummary , async ( request ) => { this . generateWorkspaceSummaryRequest ( request , { showSummaryRequest : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . listContext , async ( request ) => { await this . listContextFilesRequest ( request ) ; } ) ; this . connection ?. onRequest ( serverRequest . proveFormula , async ( req ) => { await this . proveFormulaRequest ( req ) ; } ) ; this . connection ?. onRequest ( serverRequest . getImportChainTheorems , async ( args ) => { await this . getImportChainTheoremsRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . getTheorems , async ( args ) => { await this . getTheoremsRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . getTccs , async ( args ) => { await this . getTccsRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . autorunFormula , async ( req ) => { await this . proveFormulaRequest ( req , { autorun : true , quiet : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . autorunFormulaFromJprf , async ( req ) => { await this . proveFormulaRequest ( req , { autorun : true , useJprf : true , quiet : true } ) ; } ) ; this . connection ?. onRequest ( serverRequest . showProofLite , async ( args ) => { await this . showProofLiteRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . proofCommand , async ( args ) => { await this . proofExplorer ?. proofCommandRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . getGatewayConfig , async ( ) => { this . connection ?. sendRequest ( serverEvent . getGatewayConfigResponse , { port : 0 } ) ; } ) ; this . connection ?. onRequest ( serverRequest . viewPreludeFile , async ( ) => { this . connection ?. sendRequest ( serverEvent . viewPreludeFileResponse , this . getPreludeFileName ( ) ) ; } ) ; this . connection ?. onRequest ( serverRequest . quitProof , async ( ) => { this . quitProofRequest ( ) ; } ) ; this . connection ?. onRequest ( serverRequest . getNasalibDownloader , async ( req ) => { const downloader = await PvsPackageManager . getNasalibDownloader ( req ) ; const res = { downloader } ; this . connection ?. sendNotification ( serverRequest . getNasalibDownloader , { req , res } ) ; } ) ; this . connection ?. onRequest ( serverRequest . listVersionsWithProgress , async ( req ) => { const res = await PvsPackageManager . listDownloadableVersionsWithProgress ( this . connection , req ) ; this . connection ?. sendNotification ( serverRequest . listVersionsWithProgress , { req , res } ) ; } ) ; this . connection ?. onRequest ( serverRequest . installWithProgress , async ( req ) => { const res = await PvsPackageManager . installWithProgress ( this . connection , req ) ; this . connection ?. sendNotification ( serverRequest . installWithProgress , { req , res } ) ; } ) ; this . connection ?. onRequest ( serverRequest . downloadWithProgress , async ( req ) => { const res = await PvsPackageManager . downloadWithProgress ( this . connection , req ) ; this . connection ?. sendNotification ( serverRequest . downloadWithProgress , { req , res } ) ; } ) ; this . connection ?. onRequest ( serverRequest . downloadLicensePage , async ( ) => { const licensePage = await PvsPackageManager . downloadPvsLicensePage ( ) ; this . connection ?. sendRequest ( serverEvent . downloadLicensePageResponse , { response : licensePage } ) ; } ) ; this . connection ?. onRequest ( serverRequest . startEvaluator , async ( args ) => { await this . startEvaluatorRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . quitEvaluator , async ( args ) => { await this . quitEvaluatorRequest ( args ) ; this . connection . sendRequest ( serverEvent . quitEvaluatorResponse ) ; } ) ; this . connection ?. onRequest ( serverRequest . evaluatorCommand , async ( args ) => { await this . pvsioEvaluatorCommandRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . evalExpression , async ( args ) => { await this . evalExpressionRequest ( args ) ; } ) ; this . connection ?. onRequest ( serverRequest . search , async ( req ) => { const ans = await this . pvsSearchEngine ?. searchNasalib ( req . searchString ) ; const res = { req , ans } ; this . connection ?. sendNotification ( serverEvent . searchResponse , res ) ; } ) ; this . connection ?. onRequest ( serverRequest . findSymbolDeclaration , async ( req ) => { const ans = await this . definitionProvider . findSymbolDefinitionInTheory ( req ?. theory , req ?. symbolName ) ; const res = { req , ans } ; this . connection ?. sendRequest ( serverEvent . findSymbolDeclarationResponse , res ) ; } ) ; this . connection ?. onRequest ( serverRequest . proverCommand , async ( desc ) => { if ( desc ) { switch ( desc . action ) { case "forward" : { this . proofExplorer ?. forward ( ) ; break ; } case "back" : { this . proofExplorer ?. back ( ) ; break ; } case "fast-forward" : { this . proofExplorer ?. fastForwardToNodeX ( desc ) ; break ; } case "rewind" : { this . proofExplorer ?. rewindToNodeX ( desc ) ; break ; } case "run-subtree" : { this . proofExplorer ?. runSubtreeX ( desc ) ; break ; } case "run" : { await this . proofExplorer ?. run ( { feedbackToTerminal : true } ) ; break ; } case "quit-proof" : { await this . proofExplorer ?. quitProof ( { notifyClient : true } ) ; break ; } case "quit-proof-and-save" : { await this . proofExplorer ?. quitProofAndSave ( { notifyClient : true } ) ; break ; } case "append-node" : { this . proofExplorer ?. appendNodeX ( desc ) ; break ; } case "copy-node" : { this . proofExplorer ?. copyNodeX ( desc ) ; break ; } case "paste-node" : { this . proofExplorer ?. pasteNodeX ( desc , { rebase : true } ) ; break ; } case "copy-tree" : { this . proofExplorer ?. copyTreeX ( desc ) ; break ; } case "paste-tree" : { this . proofExplorer ?. pasteTreeX ( desc , { rebase : true } ) ; break ; } case "delete-node" : { this . proofExplorer ?. deleteNodeX ( desc ) ; break ; } case "append-branch" : { this . proofExplorer ?. appendBranchX ( desc ) ; break ; } case "cut-node" : { this . proofExplorer ?. cutNodeX ( desc ) ; break ; } case "cut-tree" : { this . proofExplorer ?. cutTreeX ( desc ) ; break ; } case "jump-here" : { this . proofExplorer ?. jumpHereX ( desc ) ; break ; } case "delete-tree" : { this . proofExplorer ?. deleteTreeX ( desc ) ; break ; } case "trim-node" : { this . proofExplorer ?. trimNodeX ( desc ) ; break ; } case "trim-unused" : { this . proofExplorer ?. removeNotVisitedX ( desc ) ; break ; } case "rename-node" : { this . proofExplorer ?. renameNodeX ( desc ) ; break ; } case "open-proof" : { if ( desc ?. opt ?. restartProof ) { await this . proveFormulaRequest ( { contextFolder : desc . formula . contextFolder , fileName : desc . formula . fileName , fileExtension : desc . formula . fileExtension , theoryName : desc . formula . theoryName , formulaName : desc . formula . formulaName , proofFile : desc . proofFile } , { skipSave : true } ) ; } else { await this . proofExplorer ?. openProofRequest ( desc . proofFile , desc . formula ) ; } break ; } case "import-proof" : { await this . proofExplorer ?. importProofRequest ( desc . proofFile , desc . formula ) ; break ; } case "export-proof" : { await this . proofExplorer ?. exportProof ( desc . proofFile ) ; break ; } case "start-new-proof" : { await this . proveFormulaRequest ( desc . formula , { newProof : true } ) ; break ; } case "interrupt-prover" : { await this . proofExplorer ?. interruptProofCommand ( ) ; break ; } case "interrupt-and-quit-prover" : { await this . proofExplorer ?. interruptAndQuitProof ( ) ; break ; } default : { console . warn ( `[pvs-server] Warning: unhandled prover command ${ JSON . stringify ( desc ) }` ) ; break ; } } } } ) ; } ) ; this . connection ?. onCompletion ( async ( tpp ) : Promise < CompletionItem [ ] > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.autocompletion" ) ) ; if ( this . completionProvider && isEnabled ) { const uri = tpp . textDocument . uri ; if ( uri . endsWith ( ".pvs" ) && this . completionProvider ) { const document = this . documents ?. get ( tpp ?. textDocument . uri ) ; const txt = document ?. getText ( ) ; const completionItems = await this . completionProvider . provideCompletionItems ( { txt , fname : uri } , tpp . position ) ; return completionItems ; } } return null ; } ) ; this . connection ?. onCompletionResolve ( async ( item ) : Promise < CompletionItem > => { return item ; } ) ; this . connection ?. onHover ( async ( args ) : Promise < Hover > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.hover" ) ) ; if ( this . hoverProvider && isEnabled ) { const uri = args . textDocument . uri ; if ( fsUtils . isPvsFile ( uri ) && this . hoverProvider ) { const document = this . documents ?. get ( args ?. textDocument . uri ) ; const txt = document ?. getText ( ) || await this . readFile ( uri ) ; const hover = await this . hoverProvider . provideHover ( { txt , uri , position : args . position } ) ; return hover ; } } return null ; } ) ; this . connection ?. onCodeLens ( async ( args ) : Promise < CodeLens [ ] > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.codelens" ) ) ; if ( this . codeLensProvider && isEnabled ) { const uri = args ?. textDocument ?. uri ; if ( fsUtils . isPvsFile ( uri ) && this . codeLensProvider ) { const document = this . documents ?. get ( args ?. textDocument . uri ) ; const txt = document ?. getText ( ) || await this . readFile ( uri ) ; const codelens = await this . codeLensProvider . provideCodeLens ( { txt , uri } ) ; return codelens ; } } return null ; } ) ; this . connection ?. onCodeLensResolve ( async ( args ) : Promise < CodeLens > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.autocompletion" ) ) ; if ( this . codeLensProvider && isEnabled ) { return this . codeLensProvider . resolveCodeLens ( args ) ; } return null ; } ) ; this . connection ?. onDefinition ( async ( args ) : Promise < Definition > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.definitions" ) ) ; if ( this . definitionProvider && isEnabled ) { const uri = args . textDocument . uri ; if ( fsUtils . isPvsFile ( uri ) && this . codeLensProvider ) { const document = this . documents ?. get ( args ?. textDocument . uri ) ; const txt = document ?. getText ( ) || await this . readFile ( uri ) ; const def = await this . definitionProvider . provideDefinition ( { uri , position : args . position , txt } ) ; return def ; } } return null ; } ) ; this . connection ?. onRenameRequest ( async ( args ) : Promise < WorkspaceEdit > => { const isEnabled = ! ! ( await this . connection ?. workspace . getConfiguration ( "pvs.serviceProvider.rename" ) ) ; if ( this . renameProvider && isEnabled ) { const uri = args . textDocument . uri ; if ( fsUtils . isPvsFile ( uri ) && this . codeLensProvider ) { const document = this . documents ?. get ( args ?. textDocument . uri ) ; const txt = document ?. getText ( ) || await this . readFile ( uri ) ; const wsEdit = await this . renameProvider . provideRename ( { txt , uri , position : args . position , newName : args . newName } ) ; if ( wsEdit && wsEdit . changes && Object . keys ( wsEdit . changes ) && Object . keys ( wsEdit . changes ) . length ) { const cdesc = await this . getContextDescriptor ( { contextFolder : fsUtils . getContextFolder ( uri ) } ) ; this . connection ?. sendRequest ( serverEvent . contextUpdate , cdesc ) ; } return { } ; } } return null ; } ) ; } } new PvsLanguageServer ( ) ;