module author Paolo Masci
 *  date copyright import * as xmlrpc from 'xmlrpc' ; import { PvsProcess , ProcessCode } from "./pvsProcess" ; import { PvsResponse , ParseResult , ShowTCCsResult , PvsError } from "./common/pvs-gui.d" ; import * as fsUtils from './common/fsUtils' ; import * as path from 'path' ; import * as net from 'net' ; import * as crypto from 'crypto' ; import { SimpleConnection , serverEvent , PvsVersionDescriptor , ProofStatus , ProofDescriptor , ProofFile , PvsFormula , ServerMode , TheoryDescriptor , PvsTheory , FormulaDescriptor , PvsFile , PvsContextDescriptor , FileDescriptor , SequentDescriptor , MathObjects , ProofOrigin } from './common/serverInterface' ; import { Parser } from './core/Parser' ; import * as languageserver from 'vscode-languageserver' ; import { ParserDiagnostics } from './core/pvs-parser/javaTarget/pvsParser' ; import { checkPar , CheckParResult , getErrorRange , isQuitCommand , isQuitDontSaveCommand , isSaveThenQuitCommand , isShowHiddenFormulas } from './common/languageUtils' ; import * as languageUtils from './common/languageUtils' ; import { PvsProxyLegacy } from './legacy/pvsProxyLegacy' ; import { PvsErrorManager } from './pvsErrorManager' ; export class PvsProgressInfo { protected progressLevel : number = 0 ; showProgress ( cmd , data ? ) { this . progressLevel ++ ; if ( this . progressLevel > 4 ) { this . progressLevel = 0 ; } return `Executing ${ cmd }${ "." . repeat ( this . progressLevel ) }` ; } } export declare interface FileList { contextFolder : string ; fileNames : string [ ] ; } export class PvsProxy { protected activeParsers : { [ filename ] : boolean ; } = { } ; protected mathObjectsCache : { lemmas : string [ ] ; types : string [ ] ; definitions : string [ ] ; } = { lemmas : [ ] , types : [ ] , definitions : [ ] } ; protected showBanner : boolean = true ; protected debugMode : boolean = false ; protected verbose : boolean = false ; readonly MAXTIME : number = 2000 ; readonly MAX_PORT_ATTEMPTS : number = 200 ; readonly client_methods : string [ ] = [ 'info' , 'warning' , 'debug' , 'buffer' , 'yes-no' , 'dialog' ] ; protected banner : string ; protected handlers : { [ mth ] : ( params : string [ ] ) => string [ ] ; } = { } ; protected serverAddress : string = "0.0.0.0" ; protected serverPort : number ; protected clientAddress : string = "0.0.0.0" ; protected clientPort : number ; protected client : xmlrpc . Client ; protected guiServer : xmlrpc . Server ; protected pvsPath : string ; protected pvsLibPath : string ; protected nasalibPath : string ; protected pvsLibraryPath : string ; protected pvsServer : PvsProcess ; protected connection : SimpleConnection ; protected cliListener : ( data : string ) => void ; protected pvsErrorManager : PvsErrorManager ; protected pvsVersionInfo : PvsVersionDescriptor = null ; protected legacy : PvsProxyLegacy ; protected useLegacy : boolean = true ; protected useNasalib : boolean = false ; protected externalServer : boolean ; protected mode : ServerMode = "lisp" ; protected proverBusy : boolean = false ; /**
     * Parser
     */ parser : Parser ; /** The constructor simply sets various properties in the PvsProxy class. */ constructor ( pvsPath , opt ? ) { opt = opt || { } ; this . pvsPath = pvsPath ; this . pvsLibraryPath = opt . pvsLibraryPath || "" ; this . serverPort = ( ! ! opt . serverPort ) ? opt . serverPort : 22334 ; this . clientPort = ( ! ! opt . clientPort ) ? opt . clientPort : 9092 ; this . client_methods . forEach ( mth => { this . handlers [ mth ] = ( params ) : string [ ] => { return params ; } ; } ) ; this . banner = `XML-RPC GUI Server active at http://${ this . clientAddress }:${ this . clientPort }` ; this . connection = opt . connection ; this . externalServer = ! ! opt . externalServer ; this . cliListener = null ; this . parser = new Parser ( ) ; this . legacy = new PvsProxyLegacy ( pvsPath , opt ) ; } setClientPort ( p ) { if ( p ) { this . clientPort = p ; return true ; } return false ; } setClientAddress ( addr ) { if ( addr ) { this . clientAddress = addr ; return true ; } return false ; } async getMode ( ) { return this . mode ; } async enableExternalServer ( opt ? ) { opt = opt || { } ; if ( opt . enabled === false ) { await this . disableExternalServer ( ) ; } else { console . info ( "[pvs-proxy] Enabling external server..." ) ; await this . killPvsServer ( ) ; this . externalServer = true ; } } async disableExternalServer ( ) { console . info ( "[pvs-proxy] External server disabled" ) ; this . externalServer = false ; } protected normalizeSequent ( res , cmd ) { if ( res ) { const sequent = { path : res [ "path" ] , label : ( res [ "result" ] ) ? "Q.E.D." : res [ "label" ] , commentary : ( res [ "result" ] ) ? [ res [ "result" ] ] : res [ "prover-session-status" ] ? [ "Q.E.D." ] : res [ "commentary" ] , "num-subgoals" : ( res [ "result" ] ) ? 0 : res [ "num-subgoals" ] , sequent : ( res [ "result" ] ) ? { } : res [ "sequent" ] , comment : res [ "comment" ] || "" , "prev-cmd" : ( res [ "prev-cmd" ] && typeof res [ "prev-cmd" ] === "string" ) ? res [ "prev-cmd" ] . replace ( /\s+/g , " " ) : res [ "prev-cmd" ] } ; sequent [ "commentary" ] = sequent [ "commentary" ] || [ ] ; if ( typeof sequent [ "commentary" ] === "string" ) { sequent [ "commentary" ] = [ sequent [ "commentary" ] ] ; } if ( res [ "action" ] ) { sequent [ "commentary" ] . push ( res [ "action" ] ) ; } if ( res [ "num-subgoals" ] && + res [ "num-subgoals" ] > 1 ) { sequent [ "commentary" ] . push ( `this yields ${ res [ "num-subgoals" ] } subgoals:` ) ; } return sequent ; } return null ; } async pvsRequest ( method , params ? ) { params = params || [ ] ; const req = { method : method , params : params , jsonrpc : "2.0" , id : this . get_fresh_id ( ) } ; return new Promise ( async ( resolve , reject ) => { if ( this . proverBusy && req && req . method === "proof-command" ) { console . warn ( `[pvs-proxy] Warning: prover busy, ignoring command ${ req . method }` ) ; return resolve ( { jsonrpc : "2.0" , id : req . id } ) ; } if ( this . client ) { const jsonReq = JSON . stringify ( req , null , " " ) ; if ( ! this . externalServer && req && req . method !== "prover-status" ) { } this . proverBusy = true ; this . client . methodCall ( "pvs.request" , [ jsonReq , `http://${ this . clientAddress }:${ this . clientPort }` ] , ( error , value ) => { this . proverBusy = false ; if ( error ) { console . error ( "[pvs-proxy] Error returned by pvs-server: " ) ; console . error ( error ) ; if ( error [ 'code' ] === 'ECONNREFUSED' ) { console . log ( `[pvs-proxy] Connection refused when launching pvs from ${ this . pvsPath }` ) ; resolve ( { jsonrpc : "2.0" , id : req . id , error } ) ; if ( this . pvsErrorManager ) { const pvs = path . join ( this . pvsPath , "pvs" ) ; const fileExists = fsUtils . fileExists ( pvs ) ; if ( ! fileExists ) { this . pvsErrorManager . notifyPvsNotFound ( this . pvsPath ) ; } else { this . pvsErrorManager . notifyPvsFailure ( { msg : `Error: unable to connect to pvs-server at http://${ this . clientAddress }:${ this . clientPort }` , src : "pvs-server" } ) ; } } } else { if ( this . pvsErrorManager ) { this . pvsErrorManager . notifyPvsFailure ( { method : jsonReq , msg : error . message , src : "pvs-server" } ) ; } resolve ( { jsonrpc : "2.0" , id : req . id , error : { error_string : `xmlrpc method ${ method } failed with error ${ JSON . stringify ( error , null , " " ) }` } } ) ; } } else if ( value ) { try { const resp = JSON . parse ( value ) ; if ( resp && ( resp [ "result" ] === "null" || resp [ "result" ] === "nil" ) ) { resp [ "result" ] = null ; } if ( ( method === "proof-command" || method === "prove-formula" ) && resp . result ) { if ( resp . result ) { if ( resp . result . length ) { for ( let i = 0 ; i < resp . result . length ; i ++ ) { resp . result [ i ] = this . normalizeSequent ( resp . result [ i ] , params [ 0 ] ) ; } } else { resp . result = [ this . normalizeSequent ( resp . result , params [ 0 ] ) ] ; } } } resolve ( resp ) ; } catch ( jsonError ) { console . error ( `[pvs-proxy] Unable to parse pvs-server response :/` , value ) ; resolve ( null ) ; } } else { console . error ( `[pvs-proxy] pvs-server returned error` , error ) ; resolve ( { jsonrpc : "2.0" , id : req . id , error : { code : 'NO_CONTENT' , message : "pvs-server returned null response" } } ) ; } } ) ; } else { console . log ( `[pvs-proxy] Warning: could not invoke method ${ method } (pvs is not installed)` ) ; this . proverBusy = false ; resolve ( { jsonrpc : "2.0" , id : req . id , error : { code : 'PVS_NOT_INSTALLED' , message : "pvs-proxy failed to initialize gui server" } } ) ; } } ) ; } async listMethodsRequest ( ) { return await this . pvsRequest ( 'list-methods' ) ; } async listClientMethods ( ) { return await this . pvsRequest ( 'list-client-methods' ) ; } param diags protected makeDiags ( diags , opt ? ) { opt = opt || { } ; const id = opt . id || this . get_fresh_id ( ) ; let ans = { jsonrpc : "2.0" , id } ; if ( diags ) { ans [ "math-objects" ] = diags [ "math-objects" ] ; ans . contextFolder = diags . contextFolder ; ans . fileName = diags . fileName ; ans . fileExtension = diags . fileExtension ; if ( diags . errors && diags . errors . length > 0 ) { ans . error = { code : 1 , message : 'Errors' , data : diags . errors } ; } } return ans ; } /**
     * Utility function, returns the list of known math objects
     */ listMathObjects ( ) { return this . mathObjectsCache ; } /**
     * Utility function, returns the list of known lemmas
     */ listLemmas ( ) { return this . mathObjectsCache . lemmas ; } /**
     * Utility function, returns the list of known definitions
     */ listDefinitions ( ) { return this . mathObjectsCache . definitions ; } /**
     * Utility function, returns the list of known types
     */ listTypes ( ) { return this . mathObjectsCache . types ; } param desc async parseFile ( desc , opt ? ) { opt = opt || { } ; if ( desc && desc . fileName && desc . fileExtension && desc . contextFolder ) { const fname = path . join ( desc . contextFolder , `${ desc . fileName }${ desc . fileExtension }` ) ; const fileExists = fsUtils . fileExists ( fname ) ; if ( fileExists ) { await this . changeContext ( desc ) ; const content = await fsUtils . readFile ( fname ) ; if ( content ) { if ( desc . fileExtension === ".hpvs" ) { if ( ! this . activeParsers [ fname ] ) { this . activeParsers [ fname ] = true ; const diags = await this . parser . parseFile ( desc ) ; delete this . activeParsers [ fname ] ; return this . makeDiags ( diags ) ; } } else { if ( this . isProtectedFolder ( desc . contextFolder ) ) { this . info ( `${ desc . contextFolder } is already parsed` ) ; return { jsonrpc : "2.0" , id : `parse-${ desc . contextFolder }` , result : `Skipping parsing of ${ desc . contextFolder } (protected pvs folder)` } ; } const startTime = Date . now ( ) ; const res = ( this . useLegacy ) ? await this . legacy ?. parseFile ( fname ) : await this . pvsRequest ( 'parse' , [ fname ] ) ; if ( opt . test ) { return res ; } if ( res ) { let range = null ; let message = `File ${ desc . fileName } parsed successfully` ; let mathObjects = { types : 0 , definitions : 0 , lemmas : 0 } ; if ( res . result ) { const result = res . result ; if ( result && result . length ) { for ( let i = 0 ; i < result . length ; i ++ ) { const theoryStats = result [ i ] ; if ( theoryStats && theoryStats . decls && theoryStats . decls . length ) { theoryStats . decls . forEach ( decl => { switch ( decl . kind ) { case "type" : case "datatype" : mathObjects . types ++ ; this . mathObjectsCache . types . push ( decl . id ) ; break ; case "formula" : case "judgement" : mathObjects . lemmas ++ ; this . mathObjectsCache . lemmas . push ( decl . id ) ; break ; case "expr" : case "conversion" : case "auto-rewrite" : mathObjects . definitions ++ ; this . mathObjectsCache . definitions . push ( decl . id ) ; break ; default : } } ) ; } } } } const diags = { fileName : desc . fileName , fileExtension : desc . fileExtension , contextFolder : desc . contextFolder , "math-objects" : mathObjects , "parse-time" : { ms : Date . now ( ) - startTime } , range , message } ; if ( res . error && res . error . data ) { const errorStart = { line : res . error . data . place [ 0 ] , character : res . error . data . place [ 1 ] } ; const errorEnd = ( res . error . data . place . length > 3 ) ? { line : res . error . data . place [ 2 ] , character : res . error . data . place [ 3 ] } : null ; const txt = await fsUtils . readFile ( fname ) ; const error_range = getErrorRange ( txt , errorStart , errorEnd ) ; const error = { range : error_range , message : res . error . data . error_string , severity : languageserver . DiagnosticSeverity . Error } ; diags . message = `File ${ desc . fileName } contains errors` ; diags . errors = [ error ] ; if ( opt . enableEParser ) { const antlrdiags = await this . parser . parseFile ( desc ) ; if ( antlrdiags && antlrdiags . errors ) { diags . errors = diags . errors . concat ( antlrdiags . errors ) ; if ( antlrdiags [ "parse-time" ] ) { console . log ( `[pvs-parser] antlr completed parsing in ${ antlrdiags [ "parse-time" ] . ms }ms` ) ; } } } } return this . makeDiags ( diags , { id : res . id } ) ; } else { console . error ( `[pvs-proxy] Error: received pvs-server error while parsing file ${ desc . fileName }${ desc . fileExtension }` , res ) ; return null ; } } } else { return this . makeDiags ( { fileName : desc . fileName , fileExtension : desc . fileExtension , contextFolder : desc . contextFolder , "math-objects" : { types : 0 , definitions : 0 , lemmas : 0 } , "parse-time" : { ms : 0 } , range : null , message : `File ${ desc . fileName } is empty` } ) ; } } else { const message = `File ${ fname } does not exist or is not readable` ; const error = { range : { start : { line : 0 , character : 0 } , end : { line : 0 , character : 0 } } , message , severity : languageserver . DiagnosticSeverity . Error } ; return this . makeDiags ( { fileName : desc . fileName , fileExtension : desc . fileExtension , contextFolder : desc . contextFolder , "math-objects" : { types : 0 , definitions : 0 , lemmas : 0 } , "parse-time" : { ms : 0 } , range : null , message , errors : [ error ] } ) ; } } return null ; } async prettyPrintDdl ( desc ) { if ( desc && desc . expr ) { return await this . parser . prettyPrintDdl ( desc ) ; } return null ; } param desc async hp2pvs ( desc ) { if ( desc ) { const id = this . get_fresh_id ( ) ; let ans = { jsonrpc : "2.0" , id } ; const diags = await this . parser . hp2pvs ( desc ) ; if ( diags ) { ans [ "math-objects" ] = diags [ "math-objects" ] ; ans . contextFolder = diags . contextFolder ; ans . fileName = diags . fileName ; ans . fileExtension = diags . fileExtension ; if ( diags . errors && diags . errors . length > 0 ) { const msg = `PVS file could not be generated (${ desc . fileName }.hpvs contains errors)` ; ans . error = { code : 1 , message : msg , data : diags . errors } ; } } return ans ; } return null ; } param desc async getImportChain ( desc ) { let importChain = [ ] ; if ( desc && desc . theoryName ) { await this . changeContext ( desc ) ; const res = await this . legacy ?. lisp ( `
		(let ((theoryname "${ desc . theoryName }"))
				(let ((usings (remove-if #'(lambda (th)
				(or (from-prelude? th)
					(lib-datatype-or-theory? th)))
			(collect-theory-usings theoryname nil))))
				(mapcar (lambda (theory) (cons (format nil "|~a|" (id theory)) (shortname (make-specpath (filename theory))))) (reverse usings))))
			` ) ; console . log ( res . result ) ; if ( res && res . result ) { const regex = /\"\|(\w+)\|\"\s*\.\s*\"([^\|]+)\"\)/g ; let match = null ; while ( match = regex . exec ( res . result ) ) { if ( match && match . length > 2 ) { const fname = match [ 2 ] . trim ( ) ; if ( fname ) { const pvsTheory = { theoryName : match [ 1 ] . trim ( ) , fileName : fsUtils . getFileName ( fname ) , contextFolder : fsUtils . getContextFolder ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) } ; importChain . push ( pvsTheory ) ; } } } } } return importChain ; } param desc async getTheorems ( desc , opt ? ) { opt = opt || { } ; let ans = [ ] ; if ( desc ) { let theories = ( opt . includeImportChain ) ? await this . getImportChain ( desc ) : [ desc ] ; if ( theories && theories . length ) { for ( let i = 0 ; i < theories . length ; i ++ ) { if ( ! opt . tccsOnly ) { const formulaDescriptors = await fsUtils . listTheoremsInFile ( fsUtils . desc2fname ( theories [ i ] ) ) ; if ( formulaDescriptors && formulaDescriptors . length ) { const theorems = formulaDescriptors . filter ( formula => { return formula . theoryName === desc . theoryName ; } ) ; if ( theorems && theorems . length ) { ans = ans . concat ( theorems ) ; } } } const tccsResponse = await this . generateTccsFile ( theories [ i ] ) ; if ( tccsResponse && tccsResponse . result ) { const tccsResult = < ShowTCCsResult > tccsResponse . result ; for ( let j = 0 ; j < tccsResult . length ; j ++ ) { if ( tccsResult [ j ] . id ) { ans . push ( { formulaName : tccsResult [ j ] . id , theoryName : theories [ i ] . theoryName , fileName : theories [ i ] . fileName , contextFolder : theories [ i ] . contextFolder , fileExtension : ".tccs" } ) ; } } } } } } return ans ; } param desc async generateTccs ( desc ) { desc = fsUtils . decodeURIComponents ( desc ) ; if ( desc && desc . contextFolder && desc . fileName && desc . fileExtension ) { try { const fname = fsUtils . desc2fname ( { contextFolder : desc . contextFolder , fileName : desc . fileName , fileExtension : ".pvs" } ) ; const res = { contextFolder : desc . contextFolder , fileDescriptors : { } } ; res . fileDescriptors [ fname ] = { fileName : desc . fileName , fileExtension : ".pvs" , contextFolder : desc . contextFolder , theories : [ ] } ; fsUtils . deleteFile ( fsUtils . desc2fname ( { fileName : desc . fileName , fileExtension : ".tccs" , contextFolder : desc . contextFolder } ) ) ; const theories = await fsUtils . listTheoriesInFile ( fname ) ; const TCC_START_OFFSET = 5 ; if ( theories ) { for ( let i = 0 ; i < theories . length ; i ++ ) { const theoryName = theories [ i ] . theoryName ; const response = await this . generateTccsFile ( { fileName : desc . fileName , fileExtension : ".pvs" , contextFolder : desc . contextFolder , theoryName } ) ; if ( response && ! response . error ) { if ( response . result ) { const tccResult = < ShowTCCsResult > response . result ; let line = TCC_START_OFFSET ; const tccs = ( tccResult ) ? tccResult . map ( tcc => { line += ( tcc . comment && tcc . comment . length ) ? tcc . comment [ 0 ] . split ( "\n" ) . length + 1 : tcc [ "subsumed-tccs" ] ? tcc [ "subsumed-tccs" ] . split ( "\n" ) . length + 1 : 1 ; const res = { fileName : desc . fileName , fileExtension : ".tccs" , contextFolder : desc . contextFolder , theoryName , formulaName : tcc . id , position : { line , character : 0 } , status : tcc [ "status" ] , isTcc : true } ; line += ( tcc . definition ) ? tcc . definition . split ( "\n" ) . length + 2 : 2 ; return res ; } ) : null ; res . fileDescriptors [ fname ] . theories . push ( { fileName : desc . fileName , fileExtension : ".pvs" , contextFolder : desc . contextFolder , theoryName , position : null , theorems : tccs } ) ; } else { console . info ( `[pvs-language-server.showTccs] No TCCs generated` , response ) ; } } else { this . pvsErrorManager . handleShowTccsError ( { response : < PvsError > response } ) ; } } } return res ; } catch ( ex ) { console . error ( '[pvs-language-server.showTccs] Error: pvsProxy has thrown an exception' , ex ) ; return null ; } } return null ; } param desc async typecheckFile ( desc , opt ? ) { opt = opt || { } ; if ( desc && desc . fileName && desc . fileExtension && desc . contextFolder ) { let fname = fsUtils . desc2fname ( desc ) ; if ( this . isProtectedFolder ( desc . contextFolder ) ) { this . info ( `${ desc . fileName }${ desc . fileExtension } is already typechecked` ) ; return { jsonrpc : "2.0" , id : `parse-${ desc . contextFolder }` , result : `Skipping typechecking of ${ desc . contextFolder } (protected pvs folder)` } ; } if ( desc . fileExtension === ".hpvs" ) { await this . hp2pvs ( desc ) ; fname = path . join ( desc . contextFolder , `${ desc . fileName }.pvs` ) ; } await this . getPvsLibraryPath ( ) ; await this . getPvsTemporaryFolder ( ) ; await this . changeContext ( desc ) ; const res = await this . legacy ?. typecheckFile ( fname ) ; if ( res && ( res . error && res . error . data ) || res . result ) { if ( res . error ) { fname = ( res . error && res . error . data && res . error . data . file_name ) ? res . error . data . file_name : fname ; if ( res . error && res . error . data ) { if ( res . error . data ?. error_string ?. includes ( "Error: the assertion" ) ) { this . pvsErrorManager . notifyPvsFailure ( { src : "pvs-proxy.typecheck-file" , msg : res . error . data . error_string } ) ; } return { jsonrpc : "2.0" , id : this . get_fresh_id ( ) , error : { data : res . error . data } } ; } } } else { const msg = `Typechecker was unable to process file ${ desc . fileName }${ desc . fileExtension }: ${ JSON . stringify ( res , null , " " ) }` ; console . error ( `[pvs-proxy] Error: ${ msg }` ) ; if ( typeof res === "string" ) { const error = { range : { start : { line : 1 , character : 0 } , end : { line : 1 , character : 100 } } , message : res , severity : languageserver . DiagnosticSeverity . Error } ; return { jsonrpc : "2.0" , id : this . get_fresh_id ( ) , error } ; } } return res ; } return null ; } param desc deprecated protected async proveFile ( desc ) { if ( desc && desc . fileName && desc . fileExtension && desc . contextFolder ) { if ( this . isProtectedFolder ( desc . contextFolder ) ) { this . info ( `${ desc . contextFolder } is already proved` ) ; return null ; } const fname = path . join ( desc . contextFolder , `${ desc . fileName }${ desc . fileExtension }` ) ; const res = await this . pvsRequest ( 'lisp' , [ `(prove-pvs-file "${ fname }" nil)` ] ) ; return res ; } return null ; } /**
     * The status-proofchain command provides a proof chain analysis of the
     * formula at the cursor and displays it in the PVS Status buffer.  The
     * proof chain analysis indicates whether the formula has been proved, and
     * analyses the formulas used in the proof to insure that the proof is
     * complete; lemmas used in the proof are proved, and sound, i.e. there are
     * no circularities.
     * Example invocation: (proofchain-status-at "/test/helloworld/helloworld.pvs" nil 12 "pvs")
     */ async statusProofChain ( desc ) { const res = await this . legacy . statusProofChain ( desc ) ; return res ; } param formula protected async proofStatus ( formula ) { if ( formula && formula . fileName && formula . fileExtension && formula . contextFolder && formula . theoryName && formula . formulaName ) { await this . changeContext ( formula . contextFolder ) ; const fullName = path . join ( formula . contextFolder , formula . fileName + ".pvs" + "#" + formula . theoryName ) ; const ans = await this . pvsRequest ( "proof-status" , [ fullName , formula . formulaName ] ) ; return ans ; } return null ; } param formula async getProofStatus ( formula ) { if ( formula ) { const response = await this . proofStatus ( formula ) ; if ( response && response . result ) { switch ( response . result ) { case "subsumed" : case "simplified" : case "proved" : return "proved" ; case "unfinished" : return "unfinished" ; case "unchecked" : return "unchecked" ; case "unproved" : case "untried" : return "untried" ; } } } return "untried" ; } param formula async proveFormula ( formula , opt ? ) { if ( formula && formula . fileName && formula . fileExtension && formula . contextFolder && formula . theoryName && formula . formulaName ) { opt = opt || { } ; await this . changeContext ( formula . contextFolder ) ; const fullName = path . join ( formula . contextFolder , formula . fileName + ".pvs" + "#" + formula . theoryName ) ; let ans = await this . pvsRequest ( "prove-formula" , [ formula . formulaName , fullName ] ) ; if ( ans ?. error ?. data ?. error_string === "Must exit the prover first" ) { await this . quitProof ( { force : true } ) ; ans = await this . pvsRequest ( "prove-formula" , [ formula . formulaName , fullName ] ) ; } if ( ans && ans . result && ans . result [ "length" ] === undefined ) { ans . result = [ ans . result ] ; } if ( ans && ! ans . error ) { this . mode = "in-checker" ; } return ans ; } return null ; } /**
     * Clears the list of theories and theorems known to pvs
     */ async clearTheories ( ) { console . log ( `[pvs-proxy] Resetting cache of theory names` ) ; await this . lisp ( "(clear-theories t)" ) ; } param desc param desc param desc async statusProofTheory ( desc ) { if ( desc && desc . fileName && desc . fileExtension && desc . contextFolder && desc . theoryName ) { await this . changeContext ( desc . contextFolder ) ; const res = await this . pvsRequest ( 'lisp' , [ `(status-proof-theory "${ desc . theoryName }")` ] ) ; return res ; } return null ; } param contextFolder async changeContext ( desc , opt ? ) { if ( desc ) { opt = opt || { } ; const ctx = ( typeof desc === "string" ) ? desc : desc . contextFolder ; const externalServer = opt . externalServer === undefined ? this . externalServer : ! ! opt . externalServer ; if ( externalServer ) { return await this . pvsRequest ( 'change-context' , [ ctx ] ) ; } return await this . legacy ?. changeContext ( ctx ) ; } return null ; } /**
     * Returns the current context
     */ async currentContext ( ) { const res = await this . legacy ?. lisp ( '(pvs-current-directory)' ) ; if ( res && res . result && typeof res . result === "string" ) { res . result = res . result . replace ( /"/g , "" ) ; } return res ; } param cmd async lisp ( cmd , opt ? ) { opt = opt || { } ; if ( this . useLegacy && ! opt . externalServer ) { return await this . legacy ?. lisp ( cmd ) ; } return await this . pvsRequest ( 'lisp' , [ cmd ] ) ; } async getServerMode ( ) { const proverStatus = await this . getProverStatus ( ) ; if ( proverStatus === undefined ) { console . warn ( `[pvs-language-server] Warning: prover status is undefined` ) ; } const mode = ( proverStatus && proverStatus . result !== "inactive" ) ? "in-checker" : "lisp" ; return mode ; } /**
     * Quits the prover
     */ async quitProof ( opt ? ) { const mode = await this . getMode ( ) ; if ( mode === "in-checker" || opt ?. force ) { const useLispInterface = true ; const response = await this . proofCommand ( { cmd : "(quit)" } , { useLispInterface } ) ; if ( response && response . error ) { if ( response . error . data && ! response . error . data . error_string . includes ( "Prover is not running" ) ) { console . warn ( `[pvs-proxy] Warning: Unable to quit proof` , response . error . data . error_string ) ; } } } this . mode = "lisp" ; } param symbolName async findDeclaration ( symbolName , opt ? ) { opt = opt || { } ; return await this . legacy ?. findDeclaration ( symbolName ) ; } async findTheory ( theoryName ) { const ans = await this . lisp ( `(let ((th (get-theory "${ theoryName }")))
(when th
(format nil "~a~a.pvs" (context-path th) (filename th))))` ) ; return ans ; } SAM param desc async termAt ( desc ) { const fname = fsUtils . desc2fname ( desc ) ; const ans = await this . pvsRequest ( "term-at" , [ fname , `(${ desc . line } ${ desc . character })` , 't' ] ) ; return ans ; } /**
     * Returns the help message for a given command
     */ async showHelpBang ( cmd ) { const match = new RegExp ( languageUtils . helpBangCommandRegexp ) . exec ( cmd ) ; if ( match && match . length > 1 && match [ 1 ] ) { this . pvsServer . clearLispInterfaceOutput ( ) ; const helpCmd = `(help ${ match [ 1 ] })` ; const ans = await this . pvsRequest ( 'proof-command' , [ helpCmd ] ) ; if ( ans && ans . result && ans . result . length ) { let help = this . pvsServer . getLispInterfaceOutput ( ) ; this . pvsServer . clearLispInterfaceOutput ( ) ; if ( languageUtils . isInvalidCommand ( { commentary : help } ) ) { const metaHelp = languageUtils . PROOF_COMMANDS [ match [ 1 ] ] ? `(${ match [ 1 ] })    ${ languageUtils . PROOF_COMMANDS [ match [ 1 ] ] . description }` : null ; help = metaHelp || `Help not available for ${ match [ 1 ] }` ; } else { help = help . substring ( help . indexOf ( `(${ match [ 1 ] }` ) , help . indexOf ( "No change on" ) ) ; } ans . result [ ans . result . length - 1 ] . action = "" ; ans . result [ ans . result . length - 1 ] . commentary = [ help . trim ( ) ] ; } return ans ; } return null ; } param desc async proofCommand ( desc , opt ? ) { if ( desc ) { opt = opt || { } ; const test = checkPar ( desc . cmd ) ; let res = { jsonrpc : "2.0" , id : "" } ; if ( test . success ) { const showHidden = isShowHiddenFormulas ( desc . cmd ) ; const cmd = showHidden ? "(skip)" : desc . cmd ; if ( ! this . externalServer ) { console . log ( cmd ) ; } res = languageUtils . isHelpBangCommand ( cmd ) ? await this . showHelpBang ( cmd ) : await this . pvsRequest ( 'proof-command' , [ cmd ] ) ; if ( res && res . result ) { const proofStates = res . result ; if ( showHidden ) { for ( let i = 0 ; i < proofStates . length ; i ++ ) { const result = proofStates [ i ] ; if ( result ) { result . label = "hidden formulas in " + result . label ; result . action = "Showing list of hidden formulas" ; result . commentary = "Showing list of hidden formulas" ; result . sequent = { antecedents : result . sequent ? result . sequent [ 'hidden-antecedents' ] : null , succedents : result . sequent ? result . sequent [ 'hidden-succedents' ] : null } ; } } } for ( let i = 0 ; i < proofStates . length ; i ++ ) { const result = proofStates [ i ] ; if ( languageUtils . QED ( result ) ) { this . mode = "lisp" ; } } if ( isQuitCommand ( desc . cmd ) || isQuitDontSaveCommand ( desc . cmd ) || isSaveThenQuitCommand ( desc . cmd ) ) { this . mode = "lisp" ; } } } if ( res . error || ! test . success ) { res . result = res . result || [ { "prev-cmd" : desc . cmd } ] ; const error_msg = ( test . success ) ? ( res . error && res . error . message ) ? res . error . message . replace ( /\\\\"/g , "" ) : null : test . msg ; const i = res . result . length - 1 ; res . result [ i ] . commentary = res . result [ i ] . commentary || [ ] ; res . result [ i ] . commentary . push ( `No change on: ${ desc . cmd }` ) ; res . result [ i ] . commentary . push ( "Error: " + error_msg ) ; } return res ; } return null ; } /**
     * Returns the prover status
     */ async getProverStatus ( ) { const ans1 = await this . pvsRequest ( 'prover-status' ) ; const ans2 = await this . legacy ?. getProverStatus ( ) ; if ( ans1 && ans1 . result && ans2 && ans2 . result ) { return ans1 ; } else { console . warn ( `[pvs-proxy] Warning: pvs is not returning a correct prover status` ) ; console . dir ( ans1 ) ; console . dir ( ans2 ) ; } return ( ans1 && ans1 . result ) ? ans1 : ans2 ; } /**
     * Returns the pvs proof script for a given formula
     */ async getDefaultProofScript ( formula , opt ? ) { if ( formula ) { opt = opt || { } ; formula = fsUtils . decodeURIComponents ( formula ) ; const fname = fsUtils . desc2fname ( { contextFolder : formula . contextFolder , fileName : formula . fileName , fileExtension : ".pvs" } ) ; if ( this . useLegacy && ! opt . externalServer ) { return await this . legacy ?. getDefaultProofScript ( formula ) ; } return await this . pvsRequest ( 'proof-script' , [ fname , formula . formulaName ] ) ; } return null ; } param desc param formula returns async openProofFile ( desc , formula , opt ? ) { let origin = ".prf" ; if ( desc && desc . fileName && desc . fileExtension && desc . contextFolder && formula && formula . fileName && formula . fileExtension && formula . theoryName && formula . formulaName ) { let pdesc = null ; try { const isTcc = languageUtils . isTccFormula ( formula ) ; switch ( desc . fileExtension ) { case ".prf" : { const response = await this . getDefaultProofScript ( formula ) ; if ( response && response . result ) { const pvsVersionDescriptor = this . getPvsVersionInfo ( ) ; const shasum = await fsUtils . shasumFile ( formula ) ; const jpdesc = await fsUtils . getProofDescriptor ( formula ) ; pdesc = languageUtils . prf2jprf ( { prf : response . result , theoryName : formula . theoryName , formulaName : formula . formulaName , version : pvsVersionDescriptor , shasum , status : jpdesc ?. info ?. status || "untried" } ) ; } if ( ! languageUtils . isEmptyProof ( pdesc ) ) { break ; } } case ".jprf" : { const fname = fsUtils . desc2fname ( { fileName : desc . fileName , fileExtension : ".jprf" , contextFolder : desc . contextFolder } ) ; const proofFile = await fsUtils . readJprfProofFile ( fname , opt ) ; const key = `${ formula . theoryName }.${ formula . formulaName }` ; if ( proofFile && proofFile [ key ] && proofFile [ key ] . length > 0 ) { origin = ".jprf" ; pdesc = new ProofDescriptor ( proofFile [ key ] [ 0 ] . info , origin , proofFile [ key ] [ 0 ] . proofTree ) ; } break ; } case ".prl" : { const fname = fsUtils . desc2fname ( desc ) ; const prl = await fsUtils . readProoflite ( fname , formula . formulaName ) ; if ( prl ) { const pvsResponse = await this . installProofliteScript ( formula , prl ) ; if ( pvsResponse && pvsResponse . result ) { const response = await this . getDefaultProofScript ( formula ) ; if ( response && response . result ) { const pvsVersionDescriptor = this . getPvsVersionInfo ( ) ; const shasum = await fsUtils . shasumFile ( formula ) ; pdesc = languageUtils . prf2jprf ( { prf : response . result , theoryName : formula . theoryName , formulaName : formula . formulaName , version : pvsVersionDescriptor , shasum } ) ; origin = ".prl" ; } else { let msg = `Error: Unable to associate prooflite script to ${ formula . formulaName }` ; const error_msg = ( response && response . error && response . error . data && response . error . data . error_string ) ? response . error . data . error_string : "" ; if ( error_msg ) { msg += ` (${ error_msg })` ; } this . connection . sendNotification ( "server.status.error" , msg ) ; } } } break ; } default : { console . warn ( `[proof-explorer] Warning: trying to load unrecognized proof format ${ desc . fileExtension }` ) ; break ; } } } catch ( err ) { console . error ( `[pvs-server] Error while fetching proof information.` , err ) ; } finally { if ( ! pdesc ) { const shasum = await fsUtils . shasumFile ( formula ) ; const pvsVersionDescriptor = this . getPvsVersionInfo ( ) ; pdesc = new ProofDescriptor ( { theory : formula . theoryName , formula : formula . formulaName , status : "untried" , prover : languageUtils . pvsVersionToString ( pvsVersionDescriptor ) || "PVS 7.x" , shasum } , origin ) ; } return pdesc ; } } return null ; } async newProof ( formula ) { formula = fsUtils . decodeURIComponents ( formula ) ; const shasum = await fsUtils . shasumFile ( formula ) ; const pvsVersionDescriptor = this . getPvsVersionInfo ( ) ; const status = await this . getProofStatus ( formula ) ; const empty_pdesc = new ProofDescriptor ( { theory : formula . theoryName , formula : formula . formulaName , status , prover : languageUtils . pvsVersionToString ( pvsVersionDescriptor ) || "PVS 7.x" , shasum } , ".prf" ) ; return empty_pdesc ; } param formula param formula async storeLastAttemptedProof ( formula ) { if ( formula && formula . fileName && formula . contextFolder && formula . formulaName && formula . theoryName ) { const fullTheoryName = path . join ( formula . contextFolder , formula . fileName + ".pvs" + "#" + formula . theoryName ) ; const response = await this . pvsRequest ( "store-last-attempted-proof" , [ formula . formulaName , fullTheoryName , 't' ] ) ; if ( response && response . result ) { await this . pvsRequest ( "change-context" , [ formula . contextFolder ] ) ; await this . pvsRequest ( "save-all-proofs" , [ fullTheoryName ] ) ; } return response ; } console . error ( "[pvs-language-server] Warning: save-proof invoked with null or incomplete descriptor" , formula ) ; return null ; } param desc async saveProoflite ( desc , opt ? ) { opt = opt || { } ; opt . usePvsBinFolder = opt . usePvsBinFolder === undefined ? true : ! ! opt . usePvsBinFolder ; const contextFolder = opt . usePvsBinFolder ? path . join ( desc . contextFolder , "pvsbin" ) : desc . contextFolder ; const prlFile = { contextFolder , fileName : desc . theoryName , fileExtension : ".prl" } ; const content = languageUtils . proofDescriptor2ProofLite ( desc . proofDescriptor ) ; if ( content && content . length ) { const header = languageUtils . makeProofliteHeader ( `${ desc . fileName }.pvs` , desc . formulaName , desc . theoryName , desc . proofDescriptor . info . status ) ; const proofLite = content . join ( "\n" ) ; const success = await fsUtils . saveProoflite ( fsUtils . desc2fname ( prlFile ) , desc . formulaName , header + proofLite ) ; if ( success ) { prlFile . fileContent = proofLite ; return prlFile ; } } return null ; } param desc param desc /**
     * Returns the prooflite script for the given formula -- FIXME: display-prooflite-script is not working, we need to use languageUtils.proofTree2ProofLite()
     */ async proofLiteScript ( desc ) { if ( desc ) { const fname = fsUtils . desc2fname ( { contextFolder : desc . contextFolder , fileName : desc . fileName , fileExtension : ".pvs" } ) ; const res = await this . lisp ( `(display-prooflite-script "${ fname }#${ desc . theoryName }" "${ desc . formulaName }")` ) ; return res ; } return null ; } param desc async generateTccsFile ( desc ) { desc . fileExtension = ".pvs" ; desc = fsUtils . decodeURIComponents ( desc ) ; const res = await this . showTccs ( desc ) ; try { if ( res && res . result ) { const result = res . result ; const keys = Object . keys ( result ) ; let content = "" ; for ( let i = 0 ; i < keys . length ; i ++ ) { if ( result [ i ] [ "subsumed-tccs" ] ) { content += result [ i ] [ "subsumed-tccs" ] + "\n\n" ; } else { content += result [ i ] . comment ; if ( result [ i ] . id ) { const formulaName = result [ i ] . id ; const lastKnownStatus = await fsUtils . getProofStatus ( { fileName : desc . fileName , fileExtension : ".tccs" , contextFolder : desc . contextFolder , theoryName : desc . theoryName , formulaName } ) ; result [ i ] [ "status" ] = result [ i ] . proved ? "proved" : lastKnownStatus || "unfinished" ; const status = result [ i ] [ "status" ] ; content += `\n  % ${ status }\n` ; content += `${ formulaName }: OBLIGATION\n${ result [ i ] . definition }\n\n` ; } } } if ( content . trim ( ) ) { content = "\n\t" + content . split ( "\n" ) . map ( line => { return `\t${ line }` ; } ) . join ( "\n" ) . trim ( ) + "\n" ; } else { content = `%-- No TCC was generated for theory ${ desc . theoryName }` ; } content = `${ desc . theoryName }_TCCS: THEORY BEGIN\n` + content + `\nEND ${ desc . theoryName }_TCCS` ; const header = `%% TCCs associated with theory ${ desc . theoryName }\n%% This file was automatically generated by PVS, please **do not modify** by hand.\n` ; const fname = path . join ( desc . contextFolder , `${ desc . fileName }.tccs` ) ; await fsUtils . writeFile ( fname , header + content , { append : true } ) ; } } catch ( error ) { console . warn ( `[pvs-language-server] Warning: something when wrong while writing the TCCs file` , error ) ; } finally { return res ; } } protected async showTccs ( desc , opt ? ) { if ( desc ) { opt = opt || { } ; await this . changeContext ( desc . contextFolder ) ; const fullName = path . join ( desc . contextFolder , desc . fileName + ".pvs" + "#" + desc . theoryName ) ; if ( this . useLegacy && ! opt . externalServer ) { return await this . legacy ?. showTccs ( fsUtils . desc2fname ( desc ) , desc . theoryName ) ; } return await this . pvsRequest ( 'show-tccs' , [ fullName ] ) ; } return null ; } param desc /**
     * Returns pvs version information
     */ getPvsVersionInfo ( ) { return this . pvsVersionInfo ; } async loadPvsLibraryPathAndPatches ( ) { await this . setNasalibPath ( ) ; await this . pushPvsLibraryPath ( { useLisp : true } ) ; await this . loadPvsPatches ( ) ; } /**
     * Loads pvs version information
     */ async loadPvsVersionInfo ( ) { let res = null ; if ( this . externalServer ) { res = await this . lisp ( `(get-pvs-version-information)` ) ; } else { await this . loadPvsLibraryPathAndPatches ( ) ; res = await this . legacy ?. lisp ( `(get-pvs-version-information)` ) ; } const nasalib = await this . getNasalibVersionInfo ( ) ; if ( res && res . result ) { const regexp = /\(\"?(\d+(?:.?\d+)*)\"?[\s|nil]*\"?([\w\s\d\.]*)\"?/g ; const info = regexp . exec ( res . result ) ; if ( info && info . length > 2 ) { this . pvsVersionInfo = { "pvs-version" : info [ 1 ] . trim ( ) , "lisp-version" : info [ 2 ] . replace ( "International" , "" ) . trim ( ) , "nasalib-version" : nasalib ? "NASALib" : null } ; return this . pvsVersionInfo ; } } return null ; } /**
     * Returns pvs version information
     */ async getNasalibVersionInfo ( ) { const nasalibPresent = await this . NasalibPresent ( ) ; if ( nasalibPresent ) { const nasalibVersion = this . externalServer ? await this . lisp ( `*nasalib-version*` ) : await this . legacy ?. lisp ( `*nasalib-version*` ) ; const regexp = /(\d+(?:.?\d+)*)/g ; const info = regexp . exec ( nasalibVersion . result ) ; if ( info && info . length > 1 ) { this . useNasalib = true ; if ( this . connection ) { this . connection . sendNotification ( serverEvent . profilerData , `Profiling: xmlrpc-server\n` ) ; } return info [ 1 ] ; } } return null ; } protected info ( ... data ) { if ( this . debugMode ) { console . info ( data ) ; } if ( this . cliListener ) { this . cliListener ( data ) ; } } /**
     * Checks availability of the port. Returns true if the port is available, false otherwise.
     * The check works as follows. A dummy server is created at port p; if the creation of the server succeeds, an event 'listening' is triggered, otherwise an event 'error' is triggered.
     * The server is turned off as soon as an answer is available.
     */ protected checkPort ( port , retry ) { return new Promise ( ( resolve , reject ) => { if ( this . showBanner ) { console . log ( `[pvs-proxy] Checking port ${ port }...` ) ; } const socket = net . createConnection ( { host : this . clientAddress , port } ) ; socket . once ( 'error' , ( error ) => { console . log ( `[pvs-proxy] port ${ port } is available :)` ) ; resolve ( true ) ; } ) ; socket . once ( 'connect' , ( ) => { console . error ( `[pvs-proxy] port ${ port } is not available :/` ) ; resolve ( false ) ; } ) ; } ) ; } /**
     * Checks if pvs-server accepts connection
     */ async testServerConnectivity ( ) { const client = xmlrpc . createClient ( { host : "0.0.0.0" , port : this . clientPort , path : "/RPC2" } ) ; return new Promise ( ( resolve , reject ) => { client . methodCall ( 'request' , [ ] , ( error , value ) => { if ( error ) { console . log ( "[pvs-proxy] server-test error:" , error ) ; return resolve ( false ) ; } return resolve ( true ) ; } ) ; } ) ; } /**
     * Callback function called from activate, when gui-server is ready
     */ protected serverReadyCallBack ( ) { this . guiServer . on ( 'request' , ( error , params , callback ) => { if ( error ) { console . log ( "[pvs-proxy] Error" , error ) ; } if ( params && params . length > 0 ) { try { for ( let i = 0 ; i < params . length ; i ++ ) { const json = JSON . parse ( params [ i ] ) ; if ( json && json . method && this . handlers [ json . method ] ) { this . handlers [ json . method ] ( json . params ) ; } } } catch ( jsonError ) { console . log ( "[pvs-proxy] Error" , jsonError ) ; } } callback ( error , params ) ; } ) ; this . guiServer . on ( "error" , ( error ) => { console . log ( `[pvs-proxy] GUI-Server Error` , error ) ; } ) ; this . guiServer . on ( "connect" , ( error , params , callback ) => { if ( error ) { console . log ( "[pvs-proxy] connection error" , error ) ; } if ( params ) { console . info ( "[pvs-proxy] connection params" , params ) ; } } ) ; } /**
     * Utility function, creates a new pvs-server
     */ protected async createPvsServer ( opt ? ) { opt = opt || { } ; const externalServer = opt . externalServer === undefined ? this . externalServer : ! ! opt . externalServer ; if ( externalServer ) { console . log ( `[pvs-proxy] +-- EXTERNAL SERVER CONFIGURATION --` ) ; console . log ( `[pvs-proxy] |  Address: ${ this . serverAddress }` ) ; console . log ( `[pvs-proxy] |  Port: ${ this . serverPort }` ) ; console . log ( `[pvs-proxy] +-----------------------------------` ) ; return ProcessCode . SUCCESS ; } const connection = ( opt . enableNotifications ) ? this . connection : null ; const proc = new PvsProcess ( this . pvsPath , { connection , pvsErrorManager : this . pvsErrorManager } ) ; let portIsAvailable = false ; for ( let i = 0 ; ! portIsAvailable && i < this . MAX_PORT_ATTEMPTS ; i ++ ) { const success = await proc . activate ( { enableNotifications : opt . enableNotifications , serverPort : this . serverPort , externalServer : opt . externalServer , verbose : opt . verbose } ) ; if ( success === ProcessCode . PVSNOTFOUND ) { return ProcessCode . PVSNOTFOUND ; } if ( success === ProcessCode . UNSUPPORTEDPLATFORM ) { return ProcessCode . UNSUPPORTEDPLATFORM ; } portIsAvailable = success === ProcessCode . SUCCESS ; if ( portIsAvailable === false ) { this . serverPort ++ ; await proc . kill ( ) ; } } if ( portIsAvailable ) { if ( ! opt . externalServer ) { if ( connection ) { connection . console . info ( `[pvs-proxy] pvs-server active at http://${ this . serverAddress }:${ this . serverPort }` ) ; } else { console . info ( `[pvs-proxy] pvs-server active at http://${ this . serverAddress }:${ this . serverPort }` ) ; } } else { console . info ( `[pvs-proxy] using external pvs-server on port ${ this . serverPort }` ) ; } this . pvsServer = proc ; return ProcessCode . SUCCESS ; } console . log ( `[pvs-proxy] Failed to activate pvs-server at http://${ this . serverAddress }:${ this . serverPort }` ) ; return ProcessCode . ADDRINUSE ; } killParser ( ) { if ( this . parser ) { this . parser . killParser ( ) ; } } /**
     * Kill pvs process
     */ async killPvsServer ( ) { if ( this . pvsServer ) { await this . interruptProver ( ) ; await this . pvsServer . kill ( ) ; if ( this . debugMode ) { console . info ( "[pvs-proxy] Killed pvs-server" ) ; } } } /**
     * Kill pvs-gui server
     */ async killPvsProxy ( ) { return new Promise ( ( resolve , reject ) => { if ( this . guiServer ) { this . guiServer . httpServer . once ( "close" , ( ) => { if ( this . debugMode ) { console . log ( "[pvs-proxy] Closed pvs-proxy" ) ; } this . guiServer = null ; this . client = null ; resolve ( ) ; } ) ; this . guiServer . httpServer . close ( ) ; } else { resolve ( ) ; } } ) ; } async listSystemMethods ( ) { return new Promise ( ( resolve , reject ) => { if ( this . client ) { this . client . methodCall ( "system.listMethods" , [ ] , ( error , value ) => { resolve ( { error , result : value } ) ; } ) ; } else { console . log ( '[pvs-proxy] Warning: client is null :/' ) ; resolve ( null ) ; } } ) ; } async rebootPvsServer ( desc ) { this . pvsPath = desc ?. pvsPath || "" ; console . log ( `[pvs-proxy] New PVS path: ${ this . pvsPath }` ) ; await this . killPvsServer ( ) ; await this . restartPvsServer ( ) ; } protected async sendWorkspaceInfo ( ) { const res = await this . 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 } ) ; } } /**
     * Utility function, sets the current mode to 'lisp'
     */ lispMode ( ) { this . mode = "lisp" ; } param opt async restartPvsServer ( opt ? ) { opt = opt || { } ; this . mode = "lisp" ; if ( opt ) { if ( opt . pvsPath ) { this . pvsPath = opt . pvsPath ; console . log ( `[pvs-proxy] PVS path: ${ this . pvsPath }` ) ; } if ( opt . pvsLibraryPath ) { this . pvsLibraryPath = opt . pvsLibraryPath ; console . log ( `[pvs-proxy] PVS library path: ${ this . pvsLibraryPath }` ) ; } } console . info ( "[pvs-proxy] Rebooting pvs-server..." ) ; const serverPort = this . serverPort ; const serverAddress = this . serverAddress ; const pvsProcessActive = await this . createPvsServer ( { enableNotifications : true , externalServer : this . externalServer , verbose : this . verbose } ) ; if ( pvsProcessActive !== ProcessCode . SUCCESS ) { this . pvsErrorManager . handleStartPvsServerError ( pvsProcessActive ) ; } await this . legacy ?. activate ( this . pvsServer , { pvsErrorManager : this . pvsErrorManager } ) ; if ( this . client && ( this . serverPort !== serverPort || this . serverAddress !== serverAddress ) ) { this . client = xmlrpc . createClient ( { host : this . serverAddress , port : this . serverPort , path : "/RPC2" } ) ; if ( ! this . client ) { console . error ( `[pvs-proxy] Error: could not create client necessary to connect to pvs-server` ) ; this . pvsErrorManager . handleStartPvsServerError ( ProcessCode . COMMFAILURE ) ; } } const success = await this . createGuiServer ( ) ; if ( success ) { console . info ( "[pvs-proxy] Reboot complete!" ) ; } return success ; } /**
     * Internal function, returns a unique ID
    */ protected get_fresh_id ( ) { return crypto . createHash ( 'sha256' ) . update ( Math . random ( ) . toString ( 36 ) ) . digest ( 'hex' ) ; } param contextFolder isProtectedFolder ( contextFolder ) { return contextFolder === this . pvsPath || contextFolder === path . join ( this . pvsPath , "lib" ) ; } /**
     * Other internal methods
     */ protected async disableGcPrintout ( ) { return await this . pvsRequest ( 'lisp' , [ '(setq *disable-gc-printout* t)' ] ) ; } protected async namesInfo ( fileName ) { return await this . pvsRequest ( 'names-info' , [ fileName ] ) ; } protected async xmlrcpReset ( ) { return await this . pvsRequest ( 'reset' ) ; } async getPvsTemporaryFolder ( opt ? ) { const ans = [ ] ; let response = await this . lisp ( `uiop:*temporary-directory*` ) ; ans . push ( response ?. result ) ; response = await this . lisp ( `(uiop:default-temporary-directory)` ) ; ans . push ( response ?. result ) ; response = await this . lisp ( `(uiop:temporary-directory)` ) ; ans . push ( response ?. result ) ; return ans ; } async getPvsLibraryPath ( opt ? ) { const response = await this . lisp ( `*pvs-library-path*` , opt ) ; if ( response && response . result ) { const match = /\(([\w\W\s]+)\)/g . exec ( response . result ) ; if ( match && match . length > 1 && match [ 1 ] ) { const pvsLibraries = match [ 1 ] . replace ( /\s+/g , " " ) . split ( `"` ) . filter ( ( elem ) => { return elem . trim ( ) ; } ) ; return pvsLibraries ; } } return [ ] ; } getNasalibPath ( ) { return fsUtils . tildeExpansion ( path . join ( this . pvsPath , "nasalib/" ) ) ; } async setNasalibPath ( opt ? ) { const present = await this . NasalibPresent ( ) ; if ( ! present ) { const pvsLibraries = await this . getPvsLibraryPath ( opt ) ; const nasalibPath = this . getNasalibPath ( ) ; if ( ! pvsLibraries . includes ( nasalibPath ) && fsUtils . folderExists ( nasalibPath ) ) { console . log ( `[pvs-proxy] Setting nasalib path to ${ nasalibPath }` ) ; return await this . pushPvsLibraryPath ( { pvsLibraryPath : nasalibPath , useLisp : true } ) ; } } return null ; } async NasalibPresent ( ) { const response = this . externalServer ? await this . lisp ( `(boundp '*nasalib-version*)` ) : await this . legacy ?. lisp ( `(boundp '*nasalib-version*)` ) ; return response && response . result === "t" ; } async installProofliteScript ( desc , proofLiteScript ) { const nasalibPresent = await this . NasalibPresent ( ) ; if ( nasalibPresent ) { if ( this . externalServer ) { return null ; } return await this . legacy ?. installProofliteScript ( desc , proofLiteScript ) ; } return null ; } param pvsLibraryPath async pushPvsLibraryPath ( opt ? ) { opt = opt || { } ; const lp = opt . pvsLibraryPath || this . pvsLibraryPath ; const libs = ( lp ) ? lp . split ( ":" ) . map ( ( elem ) => { elem = elem . trim ( ) ; elem = fsUtils . tildeExpansion ( elem ) ; return elem . endsWith ( "/" ) ? elem : `${ elem }/` ; } ) : [ ] ; if ( libs && libs . length ) { const pvsLibraries = await this . getPvsLibraryPath ( opt ) ; let res = null ; for ( let i = 0 ; i < libs . length ; i ++ ) { let path = libs [ i ] . endsWith ( "/" ) ? libs [ i ] : `${ libs [ i ] }/` ; path = fsUtils . tildeExpansion ( path ) ; if ( ! pvsLibraries . includes ( path ) ) { res = ( opt . useLisp ) ? await this . legacy ?. lisp ( `(push "${ path }" *pvs-library-path*)` ) : await this . pvsRequest ( 'add-pvs-library' , [ path ] ) ; } } return res ; } return null ; } async patchesLoaded ( ) { const response = await this . legacy ?. lisp ( `(boundp '*pvs-patches*)` ) ; return response && response . result === "t" ; } async loadPvsPatches ( opt ? ) { const alreadyLoaded = await this . patchesLoaded ( ) ; if ( ! alreadyLoaded ) { return await this . lisp ( `(load-pvs-patches)` , opt ) ; } return null ; } param opt async activate ( opt ? ) { opt = opt || { } ; console . log ( `[pvs-proxy] Starting pvs-proxy...` ) ; this . showBanner = ( opt . showBanner === undefined ) ? true : opt . showBanner ; this . debugMode = ! ! opt . debugMode ; this . verbose = ! ! opt . verbose ; this . pvsErrorManager = opt . pvsErrorManager ; if ( this . pvsServer ) { return Promise . resolve ( true ) ; } const success = await this . restartPvsServer ( ) ; if ( success ) { console . log ( `[pvs-proxy] Ready!` ) ; } else { console . error ( `[pvs-proxy] Failed to start proxy :/` ) ; } return success ; } async createGuiServer ( opt ? ) { opt = opt || { } ; if ( this . client ) { return Promise . resolve ( true ) ; } return new Promise ( async ( resolve , reject ) => { let portIsAvailable = ( this . guiServer ) ? true : false ; for ( let i = 0 ; ! portIsAvailable && i < this . MAX_PORT_ATTEMPTS ; i ++ ) { portIsAvailable = await this . checkPort ( this . clientPort , true ) ; if ( portIsAvailable === false ) { this . clientPort ++ ; } } if ( portIsAvailable ) { this . banner = `GUI Server active at http://${ this . clientAddress }:${ this . clientPort }` ; console . log ( `[pvs-proxy] Starting GUI Server on http://${ this . clientAddress }:${ this . clientPort }` ) ; this . client = xmlrpc . createClient ( { host : this . serverAddress , port : this . serverPort , path : "/RPC2" } ) ; if ( ! this . client ) { console . error ( `[pvs-proxy] Error: could not create client necessary to connect to pvs-server` ) ; resolve ( false ) ; } if ( ! this . guiServer ) { try { this . guiServer = xmlrpc . createServer ( { host : this . clientAddress , port : this . clientPort , path : "/RPC2" } , ( ) => { this . serverReadyCallBack ( ) ; if ( opt . showBanner ) { console . log ( "[pvs-proxy] " + this . banner ) ; } resolve ( true ) ; } ) ; this . guiServer . once ( 'error' , ( error ) => { console . error ( error ) ; if ( error [ "code" ] === 'EADDRINUSE' ) { console . log ( `[pvs-proxy] port ${ this . clientPort } busy` ) ; } } ) ; } catch ( gui_server_error ) { console . error ( `[pvs-proxy]` , gui_server_error ) ; resolve ( false ) ; } } } else { console . error ( `[pvs-proxy] Error: could not start GUI-server` ) ; resolve ( false ) ; } } ) ; } /**
     * interrupts the prover
     */ async interruptProver ( ) { return await this . pvsRequest ( 'interrupt' ) ; } }