module author Paolo Masci
 *  date copyright import { CompletionItem , CompletionItemKind , Position , TextEdit , Range } from 'vscode-languageserver' ; import { PVS_BUILTIN_TYPES , PVS_KEYWORDS , INNER_DECLARATION_KEYWORDS , PVS_TRUE_FALSE , PVS_LIBRARY_FUNCTIONS } from "../common/languageKeywords" ; import { PvsDefinitionProvider } from './pvsDefinitionProvider' ; import * as utils from "../common/languageUtils" ; import { PvsDefinition } from '../common/serverInterface' ; import * as fsUtils from '../common/fsUtils' ; import * as path from 'path' ; export class PvsCompletionProvider { protected definitionProvider : PvsDefinitionProvider ; protected coreCompletionItems : CompletionItem [ ] = [ ] ; protected declarationCompletionItems : CompletionItem [ ] = [ ] ; protected mathSymbols : { description : string ; prefix : string ; scope : string ; body : string [ ] ; } [ ] ; protected lowerAndUpperCase ( elems , kind ) { if ( elems ) { return elems . map ( keyword => { return { label : keyword !== "o" ? keyword . toLocaleUpperCase ( ) : keyword , insertText : keyword . toLocaleUpperCase ( ) , commitCharacters : [ '\n' ] , kind } ; } ) . concat ( elems . map ( keyword => { return { label : keyword . toLocaleLowerCase ( ) , insertText : keyword . toLocaleUpperCase ( ) , commitCharacters : [ '\n' ] , kind } ; } ) ) ; } return [ ] ; } constructor param declarationProvider constructor ( declarationProvider ) { this . definitionProvider = declarationProvider ; const types = PVS_BUILTIN_TYPES . map ( ( tp ) => { return { label : tp , insertText : tp , commitCharacters : [ '\n' ] , kind : CompletionItemKind . Constant } ; } ) ; const keywords = this . lowerAndUpperCase ( PVS_KEYWORDS , CompletionItemKind . Keyword ) ; const declarationKeywords = this . lowerAndUpperCase ( INNER_DECLARATION_KEYWORDS , CompletionItemKind . Keyword ) ; const truefalse = this . lowerAndUpperCase ( PVS_TRUE_FALSE , CompletionItemKind . Constant ) ; const functions = PVS_LIBRARY_FUNCTIONS . map ( ( x ) => { return { label : x , insertText : x , commitCharacters : [ '\n' ] , kind : CompletionItemKind . Function } ; } ) ; this . coreCompletionItems = keywords . concat ( truefalse ) . concat ( functions ) ; this . declarationCompletionItems = types . concat ( declarationKeywords ) ; this . loadMathSymbols ( ) ; } /**
     * Loads mathematical symbols from symbols.json
     */ protected async loadMathSymbols ( ) { const symbolsFileName = path . join ( __dirname , "../../../symbols.json" ) ; const symbols = await fsUtils . readFile ( symbolsFileName ) ; try { this . mathSymbols = JSON . parse ( symbols ) ; } catch ( jsonError ) { console . error ( "[pvs-completion-provider] Warning: error while parsing symbols file " , symbolsFileName ) ; } } param document param position param token async provideCompletionItems ( document , position ) { if ( document && document . txt ) { const lastCharacter = fsUtils . getText ( document . txt , { start : { line : position . line , character : ( position . character > 0 ) ? position . character - 1 : 0 } , end : position } ) ; if ( lastCharacter === "\\" && this . mathSymbols ) { const lines = document . txt . split ( "\n" ) ; if ( lines && lines . length > position . line ) { const lineText = lines [ position . line ] ; const currentInput = lineText . substr ( 0 , position . character ) . trim ( ) ; const match = new RegExp ( /\\[^\s]*/g ) . exec ( currentInput ) ; const range = { start : { line : position . line , character : position . character - match [ 0 ] . length } , end : { line : position . line , character : position . character } } ; const items = this . mathSymbols . map ( elem => { return { label : elem . prefix , documentation : elem . description , insertText : elem . body [ 0 ] , additionalTextEdits : [ TextEdit . replace ( range , "" ) ] } ; } ) ; return items ; } } else if ( this . definitionProvider && lastCharacter . trim ( ) ) { const lines = document . txt . split ( "\n" ) ; if ( lines && lines . length > position . line ) { let ans = [ ] ; const lineText = lines [ position . line ] ; const currentLine = lineText . substr ( 0 , position . character ) . trim ( ) ; let currentInput = currentLine . substr ( currentLine . lastIndexOf ( " " ) + 1 ) ; currentInput = ( currentInput . includes ( ":" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( ":" ) + 1 ) . trim ( ) : currentInput ; currentInput = ( currentInput . includes ( "`" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( "`" ) + 1 ) . trim ( ) : currentInput ; currentInput = ( currentInput . includes ( "(" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( "(" ) + 1 ) . trim ( ) : currentInput ; currentInput = ( currentInput . includes ( ")" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( ")" ) + 1 ) . trim ( ) : currentInput ; currentInput = ( currentInput . includes ( "[" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( "[" ) + 1 ) . trim ( ) : currentInput ; currentInput = ( currentInput . includes ( "]" ) ) ? currentInput . substr ( currentInput . lastIndexOf ( "]" ) + 1 ) . trim ( ) : currentInput ; const start = ( position . line - 20 ) > 0 ? position . line - 20 : 0 ; let chunk = lines . slice ( start , position . line ) . join ( "\n" ) . replace ( utils . commentRegexp , "" ) ; chunk += " " + currentLine . replace ( currentInput , "" ) ; const localSymbols = utils . listSymbols ( chunk ) ; for ( let i = 0 ; i < localSymbols . length ; i ++ ) { const term = localSymbols [ i ] ; if ( term . startsWith ( currentInput ) ) { ans . push ( { label : term , insertText : term , commitCharacters : [ '\n' ] , kind : CompletionItemKind . Variable } ) ; } } const theoryDeclared = new RegExp ( utils . isense . theoryDeclaration ) . test ( document . txt ) ; if ( ! theoryDeclared ) { if ( "THEORY" . startsWith ( currentInput . toUpperCase ( ) ) ) { return Promise . resolve ( [ { label : "THEORY" , insertText : "THEORY" , commitCharacters : [ '\n' ] , kind : CompletionItemKind . Keyword } ] ) ; } } const datatypeDeclared = new RegExp ( utils . isense . datatypeDeclaration ) . test ( document . txt ) ; if ( ! datatypeDeclared ) { if ( "DATATYPE" . startsWith ( currentInput . toUpperCase ( ) ) ) { return Promise . resolve ( [ { label : "DATATYPE" , insertText : "DATATYPE" , commitCharacters : [ '\n' ] , kind : CompletionItemKind . Keyword } ] ) ; } } const declarationLine = new RegExp ( utils . isense . declaration ) . test ( currentLine ) ; const formulaDeclared = new RegExp ( utils . isense . formulaDeclaration ) . test ( currentLine ) ; if ( declarationLine && ! formulaDeclared ) { if ( this . declarationCompletionItems ) { ans = ans . concat ( this . declarationCompletionItems . filter ( ( item ) => { return item . label . toUpperCase ( ) . startsWith ( currentInput . toUpperCase ( ) ) ; } ) ) ; } } let match = null ; if ( match = ( new RegExp ( utils . isense . recordExpression ) . exec ( currentLine ) || new RegExp ( utils . isense . recordAccessor ) . exec ( currentLine ) ) ) { if ( ! currentLine . endsWith ( ":=" ) ) { const symbolName = match [ 1 ] ; let declarations = await this . definitionProvider . findSymbolDefinition ( document . fname , symbolName , position ) ; if ( declarations && declarations . length === 1 && declarations [ 0 ] . symbolDeclaration ) { let decl = declarations [ 0 ] ; let tmp = utils . RECORD . declaration . exec ( decl . symbolDeclaration ) ; utils . RECORD . declaration . lastIndex = 0 ; const isTypeDeclaration = tmp [ 2 ] . toUpperCase ( ) === "TYPE" ; if ( ! isTypeDeclaration ) { const typeName = tmp [ 2 ] ; let definitions = await this . definitionProvider . findSymbolDefinition ( document . fname , typeName , position ) ; decl = ( definitions && definitions . length === 1 ) ? definitions [ 0 ] : null ; } if ( decl ) { tmp = utils . RECORD . accessors . exec ( decl . symbolDeclaration ) ; utils . RECORD . accessors . lastIndex = 0 ; if ( tmp && tmp . length > 1 ) { const recordFields = tmp [ 1 ] ; if ( recordFields ) { const fields = recordFields . split ( "," ) ; if ( fields ) { const fieldNames = fields . map ( ( decl ) => { const insertText = decl . split ( ":" ) [ 0 ] . trim ( ) ; return { label : decl . trim ( ) , insertText : insertText , kind : CompletionItemKind . Field } ; } ) ; return Promise . resolve ( fieldNames ) ; } } } } } return Promise . resolve ( [ ] ) ; } else { } } if ( this . coreCompletionItems ) { ans = ans . concat ( this . coreCompletionItems . filter ( ( item ) => { return item . label . startsWith ( currentInput ) ; } ) ) ; } return Promise . resolve ( ans ) ; } } } return null ; } }