module author Paolo Masci
 *  date copyright import { PvsDefinition , ProofStatus , TheoryDescriptor , PvsTheory } from '../common/serverInterface' ; import * as language from "../common/languageKeywords" ; import { Connection , Position , Range , CancellationToken , TextDocuments , TextDocumentPositionParams , Definition , TextDocument , Location } from 'vscode-languageserver' ; import { getWordRange } from '../common/languageUtils' ; import * as fsUtils from '../common/fsUtils' ; import { PvsProxy } from '../pvsProxy' ; import { FindDeclarationResult , Place , PvsResponse } from '../common/pvs-gui' ; import * as path from 'path' ; import * as utils from '../common/languageUtils' ; export class PvsDefinitionProvider { connection : Connection ; protected pvsProxy : PvsProxy ; protected documents : TextDocuments ; constructor ( pvsProxy , documents ) { this . pvsProxy = pvsProxy ; this . documents = documents ; } param msg protected printWarning ( msg ) { if ( this . connection ) { this . connection . console . warn ( `[pvs-definition-provider] ${ msg }` ) ; } } param msg protected printInfo ( msg ) { if ( this . connection ) { this . connection . console . info ( `[pvs-definition-provider] ${ msg }` ) ; } } isProtectedFolder ( contextFolder ) { if ( this . pvsProxy ) { return this . pvsProxy . isProtectedFolder ( contextFolder ) ; } return false ; } param fname param symbolName param position async findSymbolDefinition ( fname , symbolName , position ) { if ( fname ) { if ( fname . endsWith ( ".tccs" ) ) { const theoryName = fsUtils . getFileName ( fname ) ; const theory = { ... fsUtils . fname2desc ( fname ) , theoryName } ; return await this . findSymbolDefinitionInTheory ( theory , symbolName , position ) ; } const content = await fsUtils . readFile ( fname ) ; const theoryName = fsUtils . findTheoryName ( content , position ?. line ) ; if ( theoryName ) { const theory = { ... fsUtils . fname2desc ( fname ) , theoryName } ; return await this . findSymbolDefinitionInTheory ( theory , symbolName , position ) ; } } return null ; } param fname param symbolName param position async findSymbolDefinitionInTheory ( theory , symbolName , position ? ) { if ( ! theory || ! symbolName ) { return null ; } let response = { file : fsUtils . desc2fname ( theory ) , theory : theory . theoryName , line : position ?. line || 0 , character : position ?. character || 0 , symbolName : symbolName , symbolTheory : null , symbolDeclaration : null , symbolDeclarationRange : null , symbolDeclarationFile : null , symbolDoc : null , comment : null , error : null } ; symbolName = ( symbolName . toUpperCase ( ) === "TRUE" || symbolName . toUpperCase ( ) === "FALSE" ) ? symbolName . toUpperCase ( ) : symbolName ; const isNumber = new RegExp ( language . PVS_NUMBER_REGEXP_SOURCE ) . test ( symbolName ) ; if ( isNumber ) { this . printInfo ( `Number ${ symbolName }` ) ; response . comment = `Number ${ symbolName }` ; return [ response ] ; } const isString = new RegExp ( language . PVS_STRING_REGEXP_SOURCE ) . test ( symbolName ) ; if ( isString ) { this . printInfo ( `String ${ symbolName }` ) ; response . comment = `String ${ symbolName }` ; return [ response ] ; } const isKeyword = new RegExp ( language . PVS_RESERVED_WORDS_REGEXP_SOURCE , "gi" ) . test ( symbolName ) ; if ( isKeyword ) { symbolName = symbolName ; this . printInfo ( `Keyword ${ symbolName }` ) ; response . comment = symbolName === 'o' ? `Keyword ${ symbolName }` : `Keyword ${ symbolName . toUpperCase ( ) }` ; return [ response ] ; } const ans = await this . pvsProxy . findDeclaration ( symbolName ) ; const candidates = [ ] ; if ( ans && ans . result ) { const declarations = ans . result ; if ( declarations && typeof declarations === "object" && declarations . length > 0 ) { for ( let i = 0 ; i < declarations . length ; i ++ ) { const info = declarations [ i ] ; if ( info ) { let fname = info . filename ; if ( fname && fname . indexOf ( "/" ) < 0 ) { let contextFolder = theory . contextFolder ; if ( contextFolder . endsWith ( "/pvsbin" ) || contextFolder . endsWith ( "pvsbin/" ) ) { contextFolder = contextFolder . split ( "/" ) . slice ( 0 , - 1 ) . join ( "/" ) ; } fname = path . join ( contextFolder , fname ) ; } let comment = "" ; if ( fname && info . type === "theorem" || info . type === "lemma" ) { const proofStatus = await fsUtils . getProofStatus ( { contextFolder : fsUtils . getContextFolder ( fname ) , fileName : fsUtils . getFileName ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) , theoryName : info . theoryid , formulaName : info . declname } ) ; comment += `Formula ${ info . declname } (${ utils . getIcon ( proofStatus ) }${ proofStatus })` ; const date = await fsUtils . getProofDate ( { contextFolder : fsUtils . getContextFolder ( fname ) , fileName : fsUtils . getFileName ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) , theoryName : info . theoryid , formulaName : info . declname } ) ; if ( date ) { comment += ` (${ new Date ( date ) . toLocaleString ( ) })` ; } } const def = { theory : theory . theoryName , line : ( position ) ? position . line : null , character : ( position ) ? position . character : null , file : fsUtils . desc2fname ( theory ) , symbolName : symbolName , symbolTheory : ( info ) ? info . theoryid : null , symbolDeclaration : ( info ) ? info [ "decl-ppstring" ] : null , symbolDeclarationRange : ( info && info . place && info . place . length > 1 ) ? { start : { line : info . place [ 0 ] , character : info . place [ 1 ] } , end : ( info . place . length === 4 ) ? { line : info . place [ 2 ] , character : info . place [ 3 ] } : undefined } : null , symbolDeclarationFile : fname , symbolDoc : null , comment , error : null } ; candidates . push ( def ) ; } } } } else { const importedTheory = await this . pvsProxy . findTheory ( symbolName ) ; if ( importedTheory && importedTheory . result ) { const fname = importedTheory . result ; let desc = await fsUtils . listTheoriesInFile ( fname ) ; desc = desc ?. filter ( tdesc => { return tdesc . theoryName = symbolName ; } ) ; const start = ( desc && desc . length ) ? desc [ 0 ] . position : { line : 0 , character : 0 } ; let decl = "" ; if ( desc && desc . length ) { decl = await fsUtils . readFile ( fname ) ; decl = decl . split ( "\n" ) . slice ( start . line - 1 ) . join ( "\n" ) ; } const def = { theory : symbolName , line : null , character : null , file : fname , symbolName : symbolName , symbolTheory : symbolName , symbolDeclaration : decl , symbolDeclarationRange : { start , end : start } , symbolDeclarationFile : fname , symbolDoc : null , comment : `Imported theory ${ symbolName }` , error : null } ; candidates . push ( def ) ; } } if ( candidates . length === 0 ) { this . printWarning ( "Warning: Could not find declaration :/" ) ; return null ; } if ( candidates . length === 1 ) { response = candidates [ 0 ] ; const isBuiltinType = new RegExp ( language . PVS_BUILTIN_TYPE_REGEXP_SOURCE , "g" ) . test ( symbolName ) ; const isTrueFalse = new RegExp ( language . PVS_TRUE_FALSE_REGEXP_SOURCE , "gi" ) . test ( symbolName ) ; if ( isBuiltinType ) { response . comment = `Builtin type ${ symbolName }` ; } else if ( isTrueFalse ) { response . comment = `Builtin constant ${ symbolName }` ; } else if ( ! response . comment ) { response . comment = `User-defined symbol ${ symbolName }` ; } return [ response ] ; } else { const currentFile = candidates . filter ( elem => { return fsUtils . getContextFolder ( elem . symbolDeclarationFile ) === theory . contextFolder && fsUtils . getFileName ( elem . symbolDeclarationFile ) === theory . fileName ; } ) || [ ] ; if ( currentFile && currentFile . length ) { return currentFile . concat ( candidates . filter ( elem => { return ! ( fsUtils . getContextFolder ( elem . symbolDeclarationFile ) === theory . contextFolder && fsUtils . getFileName ( elem . symbolDeclarationFile ) === theory . fileName ) ; } ) ) ; } } return candidates ; } param document param position param token async getDefinition ( document , token ? ) { if ( document && document . uri && document . txt && document . position ) { const symbolRange = getWordRange ( document . txt , document . position ) ; if ( symbolRange && symbolRange . end && symbolRange . start && symbolRange . end . character > document . position . character ) { const symbolName = fsUtils . getText ( document . txt , symbolRange ) ; if ( symbolName ) { const line = symbolRange . start . line + 1 ; const character = symbolRange . start . character ; const definitions = await this . findSymbolDefinition ( document . uri , symbolName , { line : line , character : character } ) ; return { symbolName , definitions } ; } } } return null ; } async provideDefinition ( desc ) { if ( desc && desc . uri && fsUtils . isPvsFile ( desc . uri ) ) { if ( desc . txt ) { const position = desc . position ; const info = await this . getDefinition ( { txt : desc . txt , uri : desc . uri , position } ) ; if ( info ) { const pvsDefinitions = info . definitions ; if ( pvsDefinitions ) { const ans = [ ] ; for ( let i = 0 ; i < pvsDefinitions . length ; i ++ ) { const def = pvsDefinitions [ i ] ; if ( def ?. symbolDeclarationRange ) { const uri = def . symbolDeclarationFile ; const range = { start : { line : def . symbolDeclarationRange . start . line - 1 , character : def . symbolDeclarationRange . start . character } , end : { line : def . symbolDeclarationRange . end . line - 1 , character : def . symbolDeclarationRange . end . character } } ; const location = { uri : "file://" + uri , range : range } ; ans . push ( location ) ; } } return ans . reverse ( ) ; } } } } return null ; } }