module author Paolo Masci
 *  date copyright import { spawn , ChildProcess , execSync } from 'child_process' ; import { PvsVersionDescriptor , SimpleConnection , PvsTheory , EvalExpressionRequest , PvsioEvaluatorCommand , PvsIoMode } from './common/serverInterface' ; import * as path from 'path' ; import * as fsUtils from './common/fsUtils' ; import * as languageUtils from './common/languageUtils' ; import { PvsResponse } from './common/pvs-gui' ; import { forceLocale , isQuitCommand } from './common/languageUtils' ; import { WorkspaceFolder } from 'vscode-languageserver' ; export const pvsioResultRegExp = /(\s*==>)?([\w\W\s]+)/g ; /**
 * Wrapper class for PVSio: spawns a PVSio process, and exposes the PVSio REPL interface as an asyncronous server.
 */ class PvsIoProcess { protected pvsioProcess : ChildProcess = null ; protected pvsVersionInfo : PvsVersionDescriptor ; protected pvsPath : string ; protected pvsLibPath : string ; protected pvsLibraryPath : string ; protected nasalibPath : string ; protected patchesLoaded : boolean = false ; protected ready : boolean = false ; protected data : string = "" ; protected cb : ( data : string , readyPrompt ? : boolean ) => void ; protected errorFlag : boolean = false ; protected externalHandlers : { onExit : ( ) => void ; onError : ( err ? : Error ) => void ; } = null ; protected desc : PvsTheory ; /**
     * Connection to the client
     */ protected connection : SimpleConnection ; param msg protected error ( msg ) { if ( msg ) { if ( this . connection ) { this . connection . sendNotification ( 'pvs-error' , msg ) ; } console . log ( '[pvsio-process] pvs-error' , msg ) ; } } param data protected checkError ( data ) { this . errorFlag = data ?. includes ( "Expecting an expression" ) || data ?. includes ( "does not uniquely resolve" ) || data ?. includes ( "Parser error" ) || data ?. includes ( "Error:" ) || data ?. includes ( "<pvserror msg=" ) || data ?. includes ( "Type mismatch in application" ) || data ?. includes ( "can't be translated to PVS syntax" ) || data ?. includes ( "#<Function" ) ; } /**
     * Returns the error flag, useful to check if the evaluation returned an error
     * TODO: improve the APIs
     */ getErrorFlag ( ) { return this . errorFlag ; } constructor param desc param connection constructor ( desc , opt ? , connection ? ) { this . pvsPath = ( desc && desc . pvsPath ) ? fsUtils . tildeExpansion ( desc . pvsPath ) : __dirname ; this . pvsLibPath = path . join ( this . pvsPath , "lib" ) ; this . nasalibPath = path . join ( this . pvsPath , "nasalib" ) ; opt = opt || { } ; this . pvsLibraryPath = opt . pvsLibraryPath || "" ; this . connection = connection ; } getData ( ) { return this . data ; } resetData ( ) { this . data = "" ; } /**
     * Internal function, loads pvs patches.
     * This command is not exposed in the APIs because it will produce an addional PVSio prompt
     * that can be handled correctly only within the activate method.
     */ protected async loadPvsPatches ( ) { await this . sendText ( `(load-pvs-patches)!` ) ; this . patchesLoaded = true ; } param data async sendText ( data , cb ? ) { return new Promise ( ( resolve , reject ) => { this . cb = ( data ) => { if ( cb ) { cb ( data ) ; } resolve ( data ) ; } ; this . resetData ( ) ; this . pvsioProcess ?. stdin . write ( data + "\n" ) ; } ) ; } /**
     * Sends the quit command (followed by a confirmation) to PVSio
     */ quit ( ) { this . pvsioProcess ?. stdin . write ( "exit; Y" ) ; } param desc returns async activate ( desc , opt ? ) { opt = opt || { } ; this . desc = desc ; this . resetData ( ) ; forceLocale ( ) ; this . externalHandlers = { onError : opt ?. onError , onExit : opt ?. onExit } ; return new Promise ( async ( resolve , reject ) => { if ( this . pvsioProcess ) { return resolve ( true ) ; } const pvsioExecutable = path . join ( this . pvsPath , "pvsio" ) ; const fname = fsUtils . desc2fname ( desc ) ; const args = [ `${ fname }@${ desc . theoryName }` ] ; let libraries = [ ] ; let external = this . pvsLibraryPath ?. split ( ":" ) || [ ] ; if ( opt ?. workspaceFolders ?. length ) { external = external . concat ( opt . workspaceFolders . map ( folder => { return fsUtils . normalizeContextFolder ( folder . uri ) ; } ) ) ; } if ( process . env [ "PVS_LIBRARY_PATH" ] ) { external = external . concat ( process . env [ "PVS_LIBRARY_PATH" ] . split ( ":" ) ) ; } for ( let i = 0 ; i < external . length ; i ++ ) { let lib = external [ i ] . trim ( ) ; if ( lib ) { lib = lib . endsWith ( "/" ) ? lib : `${ lib }/` ; if ( fsUtils . folderExists ( lib ) ) { libraries . push ( fsUtils . tildeExpansion ( lib ) ) ; } } } if ( this . nasalibPath && fsUtils . folderExists ( this . nasalibPath ) ) { let lib = this . nasalibPath . endsWith ( "/" ) ? this . nasalibPath : `${ this . nasalibPath }/` ; libraries . push ( fsUtils . tildeExpansion ( lib ) ) ; } process . env [ "PVS_LIBRARY_PATH" ] = ( libraries ?. length ) ? libraries . join ( ":" ) : "" ; console . log ( `\nPVS_LIBRARY_PATH=${ process . env [ "PVS_LIBRARY_PATH" ] }\n` ) ; const fileExists = fsUtils . fileExists ( pvsioExecutable ) ; let bootData = "" ; if ( fileExists && ! this . pvsioProcess ) { console . log ( pvsioExecutable + " " + args . join ( " " ) ) ; this . pvsioProcess = spawn ( pvsioExecutable , args ) ; this . pvsioProcess . stdout . setEncoding ( "utf8" ) ; this . pvsioProcess . stderr . setEncoding ( "utf8" ) ; this . pvsioProcess . stdout . on ( "data" , ( data ) => { if ( this . connection ) { this . connection . console . log ( data ) ; } else { console . log ( data ) ; } this . data += data ; this . checkError ( data ) ; const readyPrompt = data . trim ( ) . endsWith ( languageUtils . pvsioPrompt ) ; if ( this . cb && typeof this . cb === "function" ) { if ( readyPrompt ) { this . data = this . data . replace ( languageUtils . pvsioPrompt , "" ) . trim ( ) ; if ( this . data . includes ( "+----" ) && ! opt . showBanner ) { this . cb ( "" , readyPrompt ) ; } else { this . cb ( this . data , readyPrompt ) ; } } } if ( readyPrompt ) { if ( ! this . patchesLoaded ) { this . loadPvsPatches ( ) ; } else { if ( ! this . ready ) { bootData = data ; this . ready = true ; resolve ( true ) ; } } } } ) ; this . pvsioProcess ?. stdin . on ( "data" , ( data ) => { console . log ( "stdin" , data ) ; } ) ; this . pvsioProcess . stderr . on ( "data" , ( data ) => { console . log ( "[pvsio-process] Error: " + data ) ; this . error ( data ) ; } ) ; this . pvsioProcess . on ( "error" , ( err ) => { console . log ( "[pvsio-process] Process error" , err ) ; if ( this . externalHandlers . onError && typeof this . externalHandlers . onError === "function" ) { this . externalHandlers . onError ( err ) ; } } ) ; this . pvsioProcess . on ( "exit" , async ( code , signal ) => { this . pvsioProcess = null ; this . patchesLoaded = false ; if ( ! this . ready ) { this . error ( bootData ) ; console . log ( "[pvsio-process] Process exited with code " , code ) ; resolve ( false ) ; return ; } if ( this . errorFlag ) { this . cb ( this . data , true ) ; console . error ( "[pvsio-process] Evaluation error " , this . data ) ; console . log ( `[pvsio-process] Re-activating pvsio...` ) ; this . resetData ( ) ; this . ready = false ; const success = await this . activate ( this . desc , { showBanner : false } ) ; console . log ( success ) ; if ( this . externalHandlers ?. onExit && typeof this . externalHandlers . onExit === "function" ) { this . externalHandlers . onExit ( ) ; } return ; } } ) ; this . pvsioProcess . on ( "message" , ( message ) => { console . log ( "[pvsio-process] Process message" ) ; } ) ; } else { console . log ( `\n>>> PVSio executable not found at ${ pvsioExecutable } <<<\n` ) ; resolve ( false ) ; } } ) ; } returns protected getProcessID ( ) { if ( this . pvsioProcess && ! isNaN ( this . pvsioProcess . pid ) ) { return this . pvsioProcess . pid . toString ( ) ; } return null ; } returns async kill ( ) { return new Promise ( ( resolve , reject ) => { if ( this . pvsioProcess ) { const pvs_shell = this . getProcessID ( ) ; this . pvsioProcess ?. stdin . destroy ( ) ; try { execSync ( `kill -9 ${ pvs_shell }` ) ; this . pvsioProcess . on ( "close" , ( code , signal ) => { console . log ( "[pvs-process] Process terminated" ) ; if ( this . externalHandlers ?. onExit && typeof this . externalHandlers . onExit === "function" ) { this . externalHandlers . onExit ( ) ; } resolve ( true ) ; } ) ; } catch ( kill_error ) { console . log ( `[pvsProcess] Warning: Could not kill process id ${ pvs_shell }.` ) ; resolve ( false ) ; } finally { this . pvsioProcess = null ; } } else { resolve ( true ) ; } } ) ; } } export class PvsIoProxy { /**
     * pvs path
     */ protected pvsPath : string ; /**
     * path to the internal pvs libraries
     */ protected pvsLibPath : string ; /**
     * path to external pvs libraries
     */ protected pvsLibraryPath : string ; /**
     * connection to the client
     */ protected connection : SimpleConnection ; /**
     * pvsio process map, key is given by utils.desc2id(theory), see also startEvaluator
     */ protected processRegistry : { [ key ] : PvsIoProcess ; } = { } ; /**
     * queue for incoming command requests
     */ protected queue : Promise < void > = Promise . resolve ( null ) ; /**
     * attributes used when in "state-machine" mode
     */ protected initialState : string = "" ; protected lastState : string = "" ; /**
     * Constructor
     */ constructor ( pvsPath , opt ? ) { opt = opt || { } ; this . pvsPath = pvsPath ; this . pvsLibraryPath = opt . pvsLibraryPath || "" ; this . pvsLibPath = path . join ( pvsPath , "lib" ) ; this . connection = opt . connection ; } /**
     * Utility function, clears the process cache
     */ clearCache ( ) { for ( let i in this . processRegistry ) { this . processRegistry [ i ] . kill ( ) ; } this . processRegistry = { } ; } /**
     * start pvsio programmatically
     */ async startEvaluator ( desc , opt ? ) { const processId = languageUtils . desc2id ( desc ) ; if ( processId ) { opt = opt || { } ; const pvsioProcess = opt ?. reuseProcess && this . processRegistry [ processId ] ? this . processRegistry [ processId ] : new PvsIoProcess ( { pvsPath : this . pvsPath } , opt , this . connection ) ; const success = await pvsioProcess . activate ( { fileName : desc . fileName , fileExtension : desc . fileExtension , contextFolder : desc . contextFolder , theoryName : desc . theoryName } , { onExit : ( ) => { console . error ( "[pvsio-proxy] PVSio process exited." ) ; if ( this . processRegistry [ processId ] ) { delete this . processRegistry [ processId ] ; } } , onError : ( err ? ) => { console . error ( "[pvsio-proxy] PVSio process exited with error" , err ) ; if ( this . processRegistry [ processId ] ) { delete this . processRegistry [ processId ] ; } } , ... opt } ) ; if ( success ) { this . processRegistry [ processId ] = pvsioProcess ; const data = pvsioProcess . getData ( ) ; return { jsonrpc : "2.0" , id : processId , result : data } ; } } return { jsonrpc : "2.0" , id : processId , error : "Failed to start PVSio" } ; } /**
     * Set the initial state
     */ setInitialState ( state ) { this . initialState = state || this . initialState ; } /**
     * Terminates the pvsio session for the given theory
     */ async quitEvaluator ( desc ) { const processId = languageUtils . desc2id ( desc ) ; const pvsio = this . processRegistry ? this . processRegistry [ processId ] : null ; await pvsio ?. kill ( ) ; this . lastState = this . initialState ; } /**
     * Evaluate a pvs command in a pvsio evaluator session (unbuffered version)
     * Requires an evaluator session already started.
     */ protected async evalCmd ( desc , opt ? ) { opt = opt || { } ; const processId = languageUtils . desc2id ( desc ) ; const res = { jsonrpc : "2.0" , id : processId , result : null } ; const pvsio = this . processRegistry ? this . processRegistry [ processId ] : null ; if ( pvsio && desc && desc . contextFolder && desc . fileName && desc . fileExtension ) { if ( desc . cmd ) { const cmdSeq = desc . cmd ?. split ( ";" ) . filter ( cmd => { return cmd . trim ( ) !== "" ; } ) . map ( cmd => { return cmd + ";" ; } ) ; let data = "" ; for ( let i = 0 ; i < cmdSeq . length ; i ++ ) { let cmd = cmdSeq [ i ] ; if ( isQuitCommand ( cmd ) ) { await pvsio . kill ( ) ; if ( opt ?. cb && i === cmdSeq . length - 1 ) { opt . cb ( "bye!" , null ) ; } return res ; } if ( desc . initialState ) { this . initialState = desc . initialState ; this . lastState = this . initialState ; } if ( desc . mode === "state-machine" && this . lastState && this . initialState ) { cmd = cmd . substring ( 0 , cmd . length - 1 ) ; cmd = `LET st = ${ this . lastState } IN ${ cmd }(st);` ; } res . result = res . result || "" ; res . result += "\n" + await pvsio . sendText ( cmd , ( state ) => { const match = new RegExp ( pvsioResultRegExp ) . exec ( state ) ; if ( match && match . length > 2 ) { state = match [ 2 ] ?. trim ( ) ; } if ( ! pvsio . getErrorFlag ( ) ) { this . initialState = this . initialState || state ; this . lastState = state ; } data = data !== "" ? data + "\n" : data ; data += desc . showCommandInTerminal ? `${ cmd }\n==>\n${ state }` : `==>\n${ state }` ; if ( opt ?. cb && i === cmdSeq . length - 1 ) { opt . cb ( data , state ) ; } } ) ; } } return res ; } res . result = "Error: PVSio could not be started. Please check pvs-server log for details." ; return res ; } /**
     * Evaluate a pvs command in a pvsio evaluator session. Requires an evaluator session already started.
     */ async evalCommand ( desc , opt ? ) { return new Promise ( ( resolve , reject ) => { this . queue = this . queue . then ( async ( ) => { const res = await this . evalCmd ( desc , opt ) ; resolve ( res ) ; } ) ; } ) ; } param req async evalExpression ( req , opt ? ) { opt = opt || { } ; let response = await this . startEvaluator ( req , { ... opt , reuseProcess : true } ) ; if ( response && ! response . error ) { response = await this . evalCommand ( { contextFolder : req . contextFolder , fileName : req . fileName , fileExtension : req . fileExtension , theoryName : req . theoryName , cmd : req . expr + ";" } ) ; if ( response ?. result ?. startsWith ( "\n==>\n" ) ) { response . result = response . result . replace ( "\n==>\n" , "" ) ; } } return response ; } }