module author Paolo Masci
 *  date copyright import { PvsResponse , ShowTCCsResult , PvsResult , FindDeclarationResult } from '../common/pvs-gui' ; import { SimpleConnection , PvsFileDescriptor , TheoryDescriptor , FormulaDescriptor , PvsFormula , SequentDescriptor } from '../common/serverInterface' ; import * as path from 'path' ; import * as fsUtils from '../common/fsUtils' ; import { PvsProcess } from '../pvsProcess' ; import { PvsErrorManager } from '../pvsErrorManager' ; interface ProofSessionStatus { label : string ; "proof-session-status" : string ; } ; export class PvsProxyLegacy { protected pvsPath : string ; protected pvsLibraryPath : string ; protected connection : SimpleConnection ; protected pvsErrorManager : PvsErrorManager ; protected pvsProcess : PvsProcess ; constructor ( pvsPath , opt ? ) { opt = opt || { } ; this . pvsPath = pvsPath ; this . pvsLibraryPath = path . join ( pvsPath , "lib" ) ; this . connection = opt . connection ; } async activate ( pvsProcess , opt ? ) { opt = opt || { } ; this . pvsProcess = pvsProcess ; this . pvsErrorManager = opt . pvsErrorManager ; if ( ! this . pvsProcess ) { console . log ( `[pvs-proxy-legacy] Activating stand-alone pvs process` ) ; this . pvsProcess = new PvsProcess ( this . pvsPath , opt ) ; await this . pvsProcess . activate ( { externalServer : true } ) ; } } async lisp ( cmd , opt ? ) { opt = opt || { } ; let data = ( this . pvsProcess ) ? await this . pvsProcess . sendText ( `(lisp ${ cmd })` ) : "" ; if ( data ) { data = data . split ( "\n" ) . filter ( line => { return ! line . startsWith ( "127.0.0" ) && ! ( line . trim ( ) === "nil" ) && line . trim ( ) ; } ) . join ( "\n" ) ; if ( data && data . startsWith ( `"` ) && data . endsWith ( `"` ) ) { data = data . substring ( 1 , data . length - 1 ) ; } } const matchPvsError = /Error: (.+)/g . exec ( data ) ; const matchInterrupted = /Error: Interrupted by client/gm . exec ( data ) ; if ( matchPvsError && ! matchInterrupted && this . pvsErrorManager ) { const error_string = data ; const msg = ( error_string . includes ( "not find lib-path" ) ) ? error_string + ". Please add external pvs libraries to vscode-pvs settings" : error_string ; if ( ! opt . quiet ) { } return { jsonrpc : "2.0" , id : "pvs-process-legacy" , error : { data : { error_string } } } ; } return { jsonrpc : "2.0" , id : "pvs-process-legacy" , result : data } ; } async getProverStatus ( ) { const inchecker = await this . lisp ( "*in-checker*" ) ; if ( inchecker && inchecker . result === "t" ) { return { jsonrpc : "2.0" , id : "pvs-process-legacy" , result : "active" } ; } return { jsonrpc : "2.0" , id : "pvs-process-legacy" , result : "inactive" } ; } async proofCommand ( cmd ) { const pvsResponse = { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; let data = ( this . pvsProcess ) ? await this . pvsProcess . sendText ( cmd ) : "" ; if ( data . includes ( "Error:" ) ) { const error_string = data . substring ( data . indexOf ( "Error:" ) , data . length + 1 ) ; pvsResponse . error = { message : error_string } ; return pvsResponse ; } if ( data . includes ( "</pvserror>" ) ) { const error_string = data . substring ( data . indexOf ( "</pvserror>" ) + 11 , data . length + 1 ) ; pvsResponse . error = { message : error_string } ; return pvsResponse ; } if ( data . indexOf ( "[" ) !== 0 ) { console . log ( cmd ) ; } data = data . substring ( data . indexOf ( "[" ) , data . lastIndexOf ( "]" ) + 1 ) ; if ( data ) { try { const result = JSON . parse ( data ) ; pvsResponse . result = [ ] ; for ( let i = 0 ; i < result . length ; i ++ ) { if ( result [ i ] [ "prover-session-status" ] ) { pvsResponse . result . push ( { label : result [ i ] . label , commentary : ( result [ i ] . label . includes ( "." ) ) ? [ `This completes the proof in branch ${ result [ i ] . label }` ] : [ `Q.E.D.` ] } ) ; } else { pvsResponse . result . push ( result [ i ] ) ; } } } catch ( jsonerror ) { console . error ( jsonerror ) ; console . error ( data ) ; pvsResponse . error = jsonerror ; return pvsResponse ; } } return pvsResponse ; } async changeContext ( ctx ) { const response = await this . lisp ( `(change-workspace "${ ctx }" t)` ) ; if ( response . result ) { const matchFolder = /\"(.+)\"/g . exec ( response . result ) ; if ( matchFolder && matchFolder . length > 1 ) { return { result : matchFolder [ 1 ] , jsonrpc : "2.0" , id : "pvs-process-legacy" } ; } } return { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; } async proveFormula ( desc ) { const pvsResponse = { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; const response = await this . lisp ( `(prove-formula "${ desc . theoryName }#${ desc . formulaName }")` ) ; const data = response . result . substring ( ( < string > response . result ) . indexOf ( "[" ) , ( < string > response . result ) . lastIndexOf ( "]" ) + 1 ) ; try { pvsResponse . result = < SequentDescriptor [ ] > JSON . parse ( data ) ; } catch ( jsonerror ) { console . error ( data ) ; console . error ( jsonerror ) ; pvsResponse . error = jsonerror ; return pvsResponse ; } return pvsResponse ; } async showTccs ( fname , theoryName ) { const pvsResponse = { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; if ( this . pvsProcess && fsUtils . getFileExtension ( fname ) === ".pvs" ) { const fullName = path . join ( fname + "#" + theoryName ) ; const response = await this . lisp ( `(show-tccs "${ fullName }")` ) ; const result = [ ] ; if ( response && response . result ) { const ans = response . result ; const tccs = ans . split ( ";" ) ; for ( let i = 0 ; i < tccs . length ; i ++ ) { const info = tccs [ i ] ; let comment = "" ; let matchComment = null ; let proved = false ; const regexpComment = /(%\s*.+)/g ; const regexpStatus = /%\s*(?:is\s+)?(subsumed|simplified|proved|unproved|unfinished|unchecked|untried)/g ; while ( matchComment = regexpComment . exec ( info ) ) { const matchStatus = regexpStatus . exec ( matchComment [ 1 ] ) ; if ( matchStatus ) { proved = matchStatus [ 1 ] === "subsumed" || matchStatus [ 1 ] === "simplified" || matchStatus [ 1 ] === "proved" ; } else { comment += "\n" + matchComment [ 1 ] ; } } let id = "" ; const matchId = /(.+): OBLIGATION/g . exec ( info ) ; if ( matchId ?. length > 1 && /^[A-Za-z][\w\?₀₁₂₃₄₅₆₇₈₉]*/g . test ( matchId [ 1 ] ?. trim ( ) ) ) { id = matchId [ 1 ] ; } let definition = "" ; let matchDefinition = null ; const regexpDefinition = /: OBLIGATION\b([\w\W\s]+)/g ; while ( matchDefinition = regexpDefinition . exec ( info ) ) { definition += matchDefinition [ 1 ] + "\n" ; } let subsumed = "" ; let matchSubsumed = null ; const regexpSubsumed = /%\s*The subtype TCC [\w\W\s]* is subsumed by .*\s/g ; while ( matchSubsumed = regexpSubsumed . exec ( tccs [ i ] ) ) { if ( matchSubsumed && matchSubsumed . length > 0 ) { subsumed += matchSubsumed [ 0 ] . trim ( ) ; } } if ( id && comment ) { result . push ( { comment : [ comment . trim ( ) ] , definition : definition . trim ( ) , id , proved , theory : theoryName , "from-decl" : null } ) ; } if ( subsumed ) { result . push ( { "subsumed-tccs" : subsumed , theory : theoryName } ) ; } } } pvsResponse . result = result ; } return pvsResponse ; } async parseFile ( fname ) { const pvsResponse = { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; if ( this . pvsProcess && fsUtils . getFileExtension ( fname ) === ".pvs" ) { const response = await this . lisp ( `(parse-file "${ fname }" nil)` , { quiet : true } ) ; const res = ( response ) ? response . result : "" ; const matchParseError = /\berror\"\>\s*\"([\w\W\s]+)\bIn file\s+([\w\W\s]+)\s+\(line\s+(\d+)\s*,\s*col\s+(\d+)/gm . exec ( res ) ; const matchAssertionError = /\bError:[\w\W\s]+/gm . exec ( res ) ; if ( matchParseError || matchAssertionError ) { const error_string = ( matchParseError && matchParseError . length > 3 ) ? matchParseError [ 1 ] . trim ( ) . replace ( /\\n/g , "\n" ) : matchAssertionError [ 0 ] ; const file_name = ( matchParseError && matchParseError . length > 3 ) ? matchParseError [ 2 ] . trim ( ) : fname ; const line = ( matchParseError && matchParseError . length > 3 ) ? matchParseError [ 3 ] : "1" ; const character = ( matchParseError && matchParseError . length > 3 ) ? matchParseError [ 4 ] : "0" ; pvsResponse . error = { data : { place : [ + line , + character ] , error_string , file_name } } ; } else { pvsResponse . result = [ ] ; } } return pvsResponse ; } /**
     * Typecheck file
     */ async typecheckFile ( fname ) { const pvsResponse = { jsonrpc : "2.0" , id : "pvs-process-legacy" } ; if ( this . pvsProcess && fsUtils . getFileExtension ( fname ) === ".pvs" ) { const response = await this . lisp ( `(typecheck-file "${ fname }" nil nil nil nil t)` , { quiet : true } ) ; if ( response && response . error ) { return response ; } const res = ( response ) ? response . result : "" ; const matchTypecheckError = /\b(?:pvs)?error\"\>\s*\"([\w\W\s]+)\bIn file\s+([\w\W\s]+)\s+\(line\s+(\d+)\s*,\s*col\s+(\d+)\s*\)/gm . exec ( res ) ; const matchTypecheckError2 = /<pvserror msg=\"(?:[\w\W\s]+)\"\>\s*\"([\w\W\s]+)\bIn file\s+([^\()]+)(?:\s+\(line\s+(\d+)\s*,\s*col\s+(\d+)\s*\))?\"/gm . exec ( res ) ; const matchLibraryError = /\bError: ([\w\W\s]+)\b/gm . exec ( res ) ; if ( matchTypecheckError || matchTypecheckError2 || matchLibraryError ) { let error_string = ( matchTypecheckError && matchTypecheckError . length > 3 ) ? matchTypecheckError [ 1 ] . trim ( ) . replace ( /\\n/g , "\n" ) : ( matchTypecheckError2 && matchTypecheckError2 . length > 3 ) ? matchTypecheckError2 [ 1 ] . trim ( ) . replace ( /\\n/g , "\n" ) : `Libraries imported by the theory cannot be found` ; error_string = error_string . replace ( /\n+/g , "\n" ) ; let line = ( matchTypecheckError && matchTypecheckError . length > 3 && ! isNaN ( + matchTypecheckError [ 4 ] ) ) ? matchTypecheckError [ 3 ] : ( matchTypecheckError2 && matchTypecheckError2 . length > 3 && ! isNaN ( + matchTypecheckError2 [ 3 ] ) ) ? matchTypecheckError2 [ 3 ] : "1" ; let character = ( matchTypecheckError && matchTypecheckError . length > 3 && ! isNaN ( + matchTypecheckError [ 4 ] ) ) ? matchTypecheckError [ 4 ] : ( matchTypecheckError2 && matchTypecheckError2 . length > 3 && ! isNaN ( + matchTypecheckError2 [ 3 ] ) ) ? matchTypecheckError2 [ 4 ] : "0" ; let file_name = ( matchTypecheckError && matchTypecheckError . length > 3 ) ? matchTypecheckError [ 2 ] . trim ( ) : ( matchTypecheckError2 && matchTypecheckError2 . length > 3 ) ? matchTypecheckError2 [ 2 ] . trim ( ) : fname ; if ( ! file_name . endsWith ( '.pvs' ) ) { file_name = file_name + ".pvs" ; } if ( ! file_name . includes ( '/' ) ) { const candidate = path . join ( fsUtils . getContextFolder ( fname ) , file_name ) ; if ( fsUtils . fileExists ( candidate ) ) { file_name = candidate ; } else { error_string = `In imported file ${ file_name } (line ${ line }, col ${ character }): ` + error_string ; line = "1" ; character = "0" ; file_name = fname ; } } pvsResponse . error = { data : { place : [ + line , + character ] , error_string , file_name } } ; const fileName = fsUtils . getFileName ( file_name ) ; this . connection ?. sendNotification ( "server.status.info" , { msg : `Typecheck errors in file ${ fileName }` } ) ; return pvsResponse ; } const matchSystemError = /\bRestart actions \(select using \:continue\)\:/g . test ( res ) ; if ( matchSystemError ) { const error_string = `pvs crashed into Lisp.\n To continue, you may need to reboot pvs.\nPlease report the following error log to vscode-pvs developers:\n(typecheck-file "${ fname }" nil nil nil nil t)\n${ res }` ; pvsResponse . error = { data : { place : [ 1 , 0 ] , error_string , file_name : fname } } ; if ( this . pvsErrorManager ) { this . pvsErrorManager . notifyPvsFailure ( { fname , msg : error_string , src : "pvs-proxy-legacy" } ) ; } const fileName = fsUtils . getFileName ( fname ) ; this . connection ?. sendNotification ( "server.status.info" , { msg : `Error while trying to typecheck ${ fileName }` } ) ; return pvsResponse ; } pvsResponse . result = res || `File ${ fname } typechecks successfully` ; } return pvsResponse ; } /**
     * Find symbol declaration
     */ async findDeclaration ( symbolName ) { const data = await this . lisp ( `(find-declaration "${ symbolName }")` ) ; let result = [ ] ; try { if ( data && data . result ) { data . result = data . result . replace ( /\\"/g , '"' ) . replace ( /\\\\\//g , "/" ) ; result = JSON . parse ( data . result ) ; if ( typeof result === "string" ) { result = JSON . parse ( result ) ; } if ( result && result . length ) { for ( let i = 0 ; i < result . length ; i ++ ) { result [ i ] [ "decl-ppstring" ] = result [ i ] [ "decl-ppstring" ] . replace ( /\\n/g , "\n" ) ; } } } } finally { return { jsonrpc : "2.0" , id : "pvs-process-legacy" , result } ; } } async getDefaultProofScript ( formula ) { let result = null ; const error_string = `${ formula . theoryName }.${ formula . formulaName } does not have a proof` ; await this . changeContext ( formula . contextFolder ) ; await this . typecheckFile ( fsUtils . desc2fname ( formula ) ) ; if ( formula && formula . contextFolder && formula . fileExtension && formula . fileName && formula . formulaName ) { const cmd = `(get-default-proof-script "${ formula . theoryName }" "${ formula . formulaName }")` ; const data = await this . lisp ( cmd ) ; if ( data && data . result ) { const matchProof = /(;;; Proof\b[\w\W\s]+)/ . exec ( data . result ) ; if ( matchProof && matchProof . length > 1 ) { result = matchProof [ 1 ] . replace ( /\\"/g , `"` ) ; } } } return ( result ) ? { jsonrpc : "2.0" , id : "pvs-process-legacy" , result } : { jsonrpc : "2.0" , id : "pvs-process-legacy" , error : { data : { error_string } } } ; } async installProofliteScript ( desc , prl ) { const escaped = prl . replace ( /"/g , "\\\"" ) ; const cmd = `(install-script "${ desc . theoryName }" "${ escaped }" (list "${ desc . formulaName }") t)` ; const data = await this . lisp ( cmd ) ; if ( data && data . error ) { console . error ( data . error ) ; } else if ( data && data . result && typeof data . result === "string" && data . result . startsWith ( "Error:" ) ) { console . error ( data . result ) ; } return data ; } /**
     * 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 fname = fsUtils . desc2fname ( { ... desc , fileExtension : ".pvs" } ) ; let res = await this . typecheckFile ( fname ) ; if ( ! res ?. error || ( typeof res ?. result === "string" && ! res ?. result ?. startsWith ( "Error:" ) ) ) { const ext = desc . fileExtension . replace ( "." , "" ) ; const formula = desc . fileExtension === ".pvs" ? `"${ desc . formulaName }"` : "nil" ; const cmd = `(proofchain-status-at "${ desc . fileName }" ${ formula } ${ desc . line } "${ ext }")` ; res = await this . lisp ( cmd ) ; } return res ; } }