From 83bd1e0b181a18dc1c4e8b918a870832f321d050 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 29 Oct 2023 22:44:19 +0100 Subject: [PATCH] more doc and py generation --- api.meta.json | 1144 +++++++++++++++++ api.meta.md | 480 +++++++ api.py | 374 ++++++ .../main/java/de/uka/ilkd/key/proof/Node.java | 5 + keyext.api.doc/build.gradle | 1 + keyext.api.doc/src/main/java/DocGen.java | 189 +++ .../src/main/java/ExtractMetaData.java | 343 +++-- keyext.api.doc/src/main/java/Metamodel.java | 93 ++ keyext.api.doc/src/main/java/PyGen.java | 136 ++ keyext.api/build.gradle | 6 +- .../org/keyproject/key/api/KeyApiImpl.java | 17 +- .../org/keyproject/key/api/NodeTextDesc.java | 8 - .../org/keyproject/key/api/NodeTextId.java | 6 - .../keyproject/key/api/TermActionUtil.java | 3 +- .../key/api/data/KeyIdentifications.java | 8 +- .../org/keyproject/key/api/data/NodeDesc.java | 5 +- .../keyproject/key/api/data/NodeTextDesc.java | 9 + .../key/api/data/ProblemDefinition.java | 3 +- .../keyproject/key/api/data/TermActionId.java | 2 - .../keyproject/key/api/data/TreeNodeId.java | 2 - .../key/api/remoteapi/ExampleApi.java | 2 +- .../key/api/remoteapi/ExampleDesc.java | 13 + .../keyproject/key/api/remoteapi/GoalApi.java | 3 +- .../key/api/remoteapi/ServerManagement.java | 2 +- keyext.api/src/main/python/keyapi/rpc.py | 76 -- .../java/org/keyproject/key/api/TestRpc.java | 6 +- .../keyapi/__init__.py | 11 +- keyext.client.python/keyapi/rpc.py | 200 +++ .../python => keyext.client.python}/main.py | 0 keyext.client.python/rwtest.py | 402 ++++++ 30 files changed, 3306 insertions(+), 243 deletions(-) create mode 100644 api.meta.json create mode 100644 api.meta.md create mode 100644 api.py create mode 100644 keyext.api.doc/src/main/java/DocGen.java create mode 100644 keyext.api.doc/src/main/java/Metamodel.java create mode 100644 keyext.api.doc/src/main/java/PyGen.java delete mode 100644 keyext.api/src/main/java/org/keyproject/key/api/NodeTextDesc.java create mode 100644 keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java delete mode 100644 keyext.api/src/main/java/org/keyproject/key/api/data/TermActionId.java delete mode 100644 keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeId.java create mode 100644 keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleDesc.java delete mode 100644 keyext.api/src/main/python/keyapi/rpc.py rename {keyext.api/src/main/python => keyext.client.python}/keyapi/__init__.py (54%) create mode 100644 keyext.client.python/keyapi/rpc.py rename {keyext.api/src/main/python => keyext.client.python}/main.py (100%) create mode 100644 keyext.client.python/rwtest.py diff --git a/api.meta.json b/api.meta.json new file mode 100644 index 00000000000..180b16a3019 --- /dev/null +++ b/api.meta.json @@ -0,0 +1,1144 @@ +{ + "endpoints": [ + { + "name": "examples/list", + "documentation": "", + "args": [], + "returnType": { + "type": { + "typeName": "ExampleDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "meta/version", + "documentation": "", + "args": [], + "returnType": "STRING" + }, + { + "name": "meta/available_script_commands", + "documentation": "", + "args": [], + "returnType": { + "type": { + "typeName": "ProofScriptCommandDesc", + "fields": [], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "meta/available_macros", + "documentation": "", + "args": [], + "returnType": { + "type": { + "typeName": "ProofMacroDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "category", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + }, + { + "name": "scriptCommandName", + "type": "STRING" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "server/exit", + "documentation": "", + "args": [] + }, + { + "name": "server/shutdown", + "documentation": "", + "args": [], + "returnType": "BOOL" + }, + { + "name": "server/setTrace", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "SetTraceParams" + } + ] + }, + { + "name": "proofTree/root", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ProofId" + } + ], + "returnType": { + "typeName": "TreeNodeDesc", + "fields": [], + "documentation": "" + } + }, + { + "name": "proofTree/children", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ProofId" + }, + { + "name": "arg1", + "type": "TreeNodeId" + } + ], + "returnType": { + "type": { + "typeName": "TreeNodeDesc", + "fields": [], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "proofTree/subtree", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ProofId" + }, + { + "name": "arg1", + "type": "TreeNodeId" + } + ], + "returnType": { + "type": { + "typeName": "TreeNodeDesc", + "fields": [], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "goal/print", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "NodeId" + }, + { + "name": "arg1", + "type": "PrintOptions" + } + ], + "returnType": { + "typeName": "NodeTextDesc", + "fields": [ + { + "name": "id", + "type": "NodeTextId" + }, + { + "name": "result", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "goal/actions", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "NodeTextId" + }, + { + "name": "arg1", + "type": "INT" + } + ], + "returnType": { + "type": { + "typeName": "TermActionDesc", + "fields": [ + { + "name": "commandId", + "type": "TermActionId" + }, + { + "name": "displayName", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + }, + { + "name": "category", + "type": "STRING" + }, + { + "name": "kind", + "type": "TermActionKind" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "goal/apply_action", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "TermActionId" + } + ], + "returnType": { + "type": { + "typeName": "TermActionDesc", + "fields": [ + { + "name": "commandId", + "type": "TermActionId" + }, + { + "name": "displayName", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + }, + { + "name": "category", + "type": "STRING" + }, + { + "name": "kind", + "type": "TermActionKind" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "goal/free", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "NodeTextId" + } + ] + }, + { + "name": "env/functions", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "EnvironmentId" + } + ], + "returnType": { + "type": { + "typeName": "FunctionDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "sort", + "type": "STRING" + }, + { + "name": "retSort", + "type": "SortDesc" + }, + { + "name": "argSorts", + "type": "List" + }, + { + "name": "rigid", + "type": "BOOL" + }, + { + "name": "unique", + "type": "BOOL" + }, + { + "name": "skolemConstant", + "type": "BOOL" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "env/sorts", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "EnvironmentId" + } + ], + "returnType": { + "type": { + "typeName": "SortDesc", + "fields": [ + { + "name": "string", + "type": "STRING" + }, + { + "name": "documentation", + "type": "STRING" + }, + { + "name": "extendsSorts", + "type": "List" + }, + { + "name": "anAbstract", + "type": "BOOL" + }, + { + "name": "s", + "type": "STRING" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "env/contracts", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "EnvironmentId" + } + ], + "returnType": { + "type": { + "typeName": "ContractDesc", + "fields": [ + { + "name": "contractId", + "type": "ContractId" + }, + { + "name": "name", + "type": "STRING" + }, + { + "name": "displayName", + "type": "STRING" + }, + { + "name": "typeName", + "type": "STRING" + }, + { + "name": "htmlText", + "type": "STRING" + }, + { + "name": "plainText", + "type": "STRING" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "env/openContract", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ContractId" + } + ], + "returnType": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "loading/load", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "LoadParams" + } + ], + "returnType": { + "a": { + "typeName": "EnvironmentId", + "fields": [ + { + "name": "envId", + "type": "STRING" + } + ], + "documentation": "" + }, + "b": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + }, + "documentation": "" + } + }, + { + "name": "loading/loadKey", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "STRING" + } + ], + "returnType": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "loading/loadExample", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "STRING" + } + ], + "returnType": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "loading/loadProblem", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ProblemDefinition" + } + ], + "returnType": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "loading/loadTerm", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "STRING" + } + ], + "returnType": { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "client/sayHello", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "STRING" + } + ] + }, + { + "name": "client/logTrace", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "LogTraceParams" + } + ] + }, + { + "name": "client/sm", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ShowMessageParams" + } + ] + }, + { + "name": "client/userResponse", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ShowMessageRequestParams" + } + ], + "returnType": { + "typeName": "MessageActionItem", + "fields": [ + { + "name": "title", + "type": "STRING" + } + ], + "documentation": "" + } + }, + { + "name": "client/showDocument", + "documentation": "", + "args": [ + { + "name": "arg0", + "type": "ShowDocumentParams" + } + ], + "returnType": { + "typeName": "ShowDocumentResult", + "fields": [ + { + "name": "success", + "type": "BOOL" + } + ], + "documentation": "" + } + } + ], + "types": [ + { + "typeName": "ExampleDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "ProofScriptCommandDesc", + "fields": [], + "documentation": "" + }, + { + "typeName": "ProofMacroDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "category", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + }, + { + "name": "scriptCommandName", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "TraceValue", + "values": [ + "Off", + "Message", + "All" + ], + "documentation": "" + }, + { + "typeName": "SetTraceParams", + "fields": [ + { + "name": "value", + "type": "TraceValue" + } + ], + "documentation": "" + }, + { + "typeName": "EnvironmentId", + "fields": [ + { + "name": "envId", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "ProofId", + "fields": [ + { + "name": "env", + "type": "EnvironmentId" + }, + { + "name": "proofId", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "TreeNodeDesc", + "fields": [], + "documentation": "" + }, + { + "typeName": "TreeNodeId", + "fields": [ + { + "name": "id", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "NodeId", + "fields": [ + { + "name": "proofId", + "type": "ProofId" + }, + { + "name": "nodeId", + "type": "INT" + } + ], + "documentation": "" + }, + { + "typeName": "PrintOptions", + "fields": [ + { + "name": "unicode", + "type": "BOOL" + }, + { + "name": "width", + "type": "INT" + }, + { + "name": "indentation", + "type": "INT" + }, + { + "name": "pure", + "type": "BOOL" + }, + { + "name": "termLabels", + "type": "BOOL" + } + ], + "documentation": "" + }, + { + "typeName": "NodeTextId", + "fields": [ + { + "name": "nodeId", + "type": "NodeId" + }, + { + "name": "nodeTextId", + "type": "INT" + } + ], + "documentation": "" + }, + { + "typeName": "NodeTextDesc", + "fields": [ + { + "name": "id", + "type": "NodeTextId" + }, + { + "name": "result", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "TermActionId", + "fields": [ + { + "name": "nodeId", + "type": "NodeId" + }, + { + "name": "pio", + "type": "STRING" + }, + { + "name": "id", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "TermActionKind", + "values": [ + "BuiltIn", + "Script", + "Macro", + "Taclet" + ], + "documentation": "" + }, + { + "typeName": "TermActionDesc", + "fields": [ + { + "name": "commandId", + "type": "TermActionId" + }, + { + "name": "displayName", + "type": "STRING" + }, + { + "name": "description", + "type": "STRING" + }, + { + "name": "category", + "type": "STRING" + }, + { + "name": "kind", + "type": "TermActionKind" + } + ], + "documentation": "" + }, + { + "typeName": "List", + "fields": [], + "documentation": "" + }, + { + "typeName": "SortDesc", + "fields": [ + { + "name": "string", + "type": "STRING" + }, + { + "name": "documentation", + "type": "STRING" + }, + { + "name": "extendsSorts", + "type": "List" + }, + { + "name": "anAbstract", + "type": "BOOL" + }, + { + "name": "s", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "FunctionDesc", + "fields": [ + { + "name": "name", + "type": "STRING" + }, + { + "name": "sort", + "type": "STRING" + }, + { + "name": "retSort", + "type": "SortDesc" + }, + { + "name": "argSorts", + "type": "List" + }, + { + "name": "rigid", + "type": "BOOL" + }, + { + "name": "unique", + "type": "BOOL" + }, + { + "name": "skolemConstant", + "type": "BOOL" + } + ], + "documentation": "" + }, + { + "typeName": "ContractId", + "fields": [ + { + "name": "envId", + "type": "EnvironmentId" + }, + { + "name": "contractId", + "type": "INT" + } + ], + "documentation": "" + }, + { + "typeName": "ContractDesc", + "fields": [ + { + "name": "contractId", + "type": "ContractId" + }, + { + "name": "name", + "type": "STRING" + }, + { + "name": "displayName", + "type": "STRING" + }, + { + "name": "typeName", + "type": "STRING" + }, + { + "name": "htmlText", + "type": "STRING" + }, + { + "name": "plainText", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "LoadParams", + "fields": [ + { + "name": "keyFile", + "type": "STRING" + }, + { + "name": "javaFile", + "type": "STRING" + }, + { + "name": "classPath", + "type": "List" + }, + { + "name": "bootClassPath", + "type": "STRING" + }, + { + "name": "includes", + "type": "List" + } + ], + "documentation": "" + }, + { + "typeName": "ProblemDefinition", + "fields": [ + { + "name": "sorts", + "type": "List" + }, + { + "name": "functions", + "type": "List" + }, + { + "name": "predicates", + "type": "List" + }, + { + "name": "antecTerms", + "type": "List" + }, + { + "name": "succTerms", + "type": "List" + } + ], + "documentation": "" + }, + { + "typeName": "LogTraceParams", + "fields": [ + { + "name": "messag", + "type": "STRING" + }, + { + "name": "verbose", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "MessageType", + "values": [ + "Unused", + "Error", + "Warning", + "Info", + "Log", + "Debug" + ], + "documentation": "" + }, + { + "typeName": "ShowMessageParams", + "fields": [ + { + "name": "type", + "type": "MessageType" + }, + { + "name": "message", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "MessageActionItem[]", + "fields": [], + "documentation": "" + }, + { + "typeName": "ShowMessageRequestParams", + "fields": [ + { + "name": "type", + "type": "MessageType" + }, + { + "name": "message", + "type": "STRING" + }, + { + "name": "actions", + "type": "MessageActionItem[]" + } + ], + "documentation": "" + }, + { + "typeName": "MessageActionItem", + "fields": [ + { + "name": "title", + "type": "STRING" + } + ], + "documentation": "" + }, + { + "typeName": "Range", + "fields": [ + { + "name": "start", + "type": "INT" + }, + { + "name": "end", + "type": "INT" + } + ], + "documentation": "" + }, + { + "typeName": "ShowDocumentParams", + "fields": [ + { + "name": "uri", + "type": "STRING" + }, + { + "name": "external", + "type": "BOOL" + }, + { + "name": "takeFocus", + "type": "BOOL" + }, + { + "name": "selection", + "type": "Range" + } + ], + "documentation": "" + }, + { + "typeName": "ShowDocumentResult", + "fields": [ + { + "name": "success", + "type": "BOOL" + } + ], + "documentation": "" + }, + { + "typeName": "TaskFinishedInfo", + "fields": [], + "documentation": "" + }, + { + "typeName": "TaskStartedInfo", + "fields": [], + "documentation": "" + } + ] +} \ No newline at end of file diff --git a/api.meta.md b/api.meta.md new file mode 100644 index 00000000000..f53d88619f3 --- /dev/null +++ b/api.meta.md @@ -0,0 +1,480 @@ +## Types +### Type: ContractDesc +``` +type ContractDesc { + contractId : ContractId + displayName : STRING + htmlText : STRING + name : STRING + plainText : STRING + typeName : STRING +} +``` + +### Type: ContractId +``` +type ContractId { + contractId : INT + envId : EnvironmentId +} +``` + +### Type: EnvironmentId +``` +type EnvironmentId { + envId : STRING +} +``` + +### Type: ExampleDesc +``` +type ExampleDesc { + description : STRING + name : STRING +} +``` + +### Type: FunctionDesc +``` +type FunctionDesc { + argSorts : List + name : STRING + retSort : SortDesc + rigid : BOOL + skolemConstant : BOOL + sort : STRING + unique : BOOL +} +``` + +### Type: List +``` +type List { + +} +``` + +### Type: LoadParams +``` +type LoadParams { + bootClassPath : STRING + classPath : List + includes : List + javaFile : STRING + keyFile : STRING +} +``` + +### Type: LogTraceParams +``` +type LogTraceParams { + messag : STRING + verbose : STRING +} +``` + +### Type: MessageActionItem +``` +type MessageActionItem { + title : STRING +} +``` + +### Type: MessageActionItem[] +``` +type MessageActionItem[] { + +} +``` + +### Type: MessageType +``` +enum MessageType { Unused, Error, Warning, Info, Log, Debug } +``` + +### Type: NodeId +``` +type NodeId { + nodeId : INT + proofId : ProofId +} +``` + +### Type: NodeTextDesc +``` +type NodeTextDesc { + id : NodeTextId + result : STRING +} +``` + +### Type: NodeTextId +``` +type NodeTextId { + nodeId : NodeId + nodeTextId : INT +} +``` + +### Type: PrintOptions +``` +type PrintOptions { + indentation : INT + pure : BOOL + termLabels : BOOL + unicode : BOOL + width : INT +} +``` + +### Type: ProblemDefinition +``` +type ProblemDefinition { + antecTerms : List + functions : List + predicates : List + sorts : List + succTerms : List +} +``` + +### Type: ProofId +``` +type ProofId { + env : EnvironmentId + proofId : STRING +} +``` + +### Type: ProofMacroDesc +``` +type ProofMacroDesc { + category : STRING + description : STRING + name : STRING + scriptCommandName : STRING +} +``` + +### Type: ProofScriptCommandDesc +``` +type ProofScriptCommandDesc { + +} +``` + +### Type: Range +``` +type Range { + end : INT + start : INT +} +``` + +### Type: SetTraceParams +``` +type SetTraceParams { + value : TraceValue +} +``` + +### Type: ShowDocumentParams +``` +type ShowDocumentParams { + external : BOOL + selection : Range + takeFocus : BOOL + uri : STRING +} +``` + +### Type: ShowDocumentResult +``` +type ShowDocumentResult { + success : BOOL +} +``` + +### Type: ShowMessageParams +``` +type ShowMessageParams { + message : STRING + type : MessageType +} +``` + +### Type: ShowMessageRequestParams +``` +type ShowMessageRequestParams { + actions : MessageActionItem[] + message : STRING + type : MessageType +} +``` + +### Type: SortDesc +``` +type SortDesc { + anAbstract : BOOL + documentation : STRING + extendsSorts : List + s : STRING + string : STRING +} +``` + +### Type: TaskFinishedInfo +``` +type TaskFinishedInfo { + +} +``` + +### Type: TaskStartedInfo +``` +type TaskStartedInfo { + +} +``` + +### Type: TermActionDesc +``` +type TermActionDesc { + category : STRING + commandId : TermActionId + description : STRING + displayName : STRING + kind : TermActionKind +} +``` + +### Type: TermActionId +``` +type TermActionId { + id : STRING + nodeId : NodeId + pio : STRING +} +``` + +### Type: TermActionKind +``` +enum TermActionKind { BuiltIn, Script, Macro, Taclet } +``` + +### Type: TraceValue +``` +enum TraceValue { Off, Message, All } +``` + +### Type: TreeNodeDesc +``` +type TreeNodeDesc { + +} +``` + +### Type: TreeNodeId +``` +type TreeNodeId { + id : STRING +} +``` + +## Endpoints +### client/logTrace (`server ~~> client`) + +``` +Client.client/logTrace( arg0 : LogTraceParams ) **async** +``` + + +### client/sayHello (`server ~~> client`) + +``` +Client.client/sayHello( arg0 : STRING ) **async** +``` + + +### client/showDocument (`server -> client`) + +``` +Client.client/showDocument( arg0 : ShowDocumentParams ) -> ShowDocumentResult +``` + + +### client/sm (`server ~~> client`) + +``` +Client.client/sm( arg0 : ShowMessageParams ) **async** +``` + + +### client/userResponse (`server -> client`) + +``` +Client.client/userResponse( arg0 : ShowMessageRequestParams ) -> MessageActionItem +``` + + +### env/contracts (`client -> server`) + +``` +Server.env/contracts( arg0 : EnvironmentId ) -> ContractDesc[] +``` + + +### env/functions (`client -> server`) + +``` +Server.env/functions( arg0 : EnvironmentId ) -> FunctionDesc[] +``` + + +### env/openContract (`client -> server`) + +``` +Server.env/openContract( arg0 : ContractId ) -> ProofId +``` + + +### env/sorts (`client -> server`) + +``` +Server.env/sorts( arg0 : EnvironmentId ) -> SortDesc[] +``` + + +### examples/list (`client -> server`) + +``` +Server.examples/list( ) -> ExampleDesc[] +``` + + +### goal/actions (`client -> server`) + +``` +Server.goal/actions( arg0 : NodeTextId, arg1 : INT ) -> TermActionDesc[] +``` + + +### goal/apply_action (`client -> server`) + +``` +Server.goal/apply_action( arg0 : TermActionId ) -> TermActionDesc[] +``` + + +### goal/free (`client ~~> server`) + +``` +Server.goal/free( arg0 : NodeTextId ) **async** +``` + + +### goal/print (`client -> server`) + +``` +Server.goal/print( arg0 : NodeId, arg1 : PrintOptions ) -> NodeTextDesc +``` + + +### loading/load (`client -> server`) + +``` +Server.loading/load( arg0 : LoadParams ) -> either +``` + + +### loading/loadExample (`client -> server`) + +``` +Server.loading/loadExample( arg0 : STRING ) -> ProofId +``` + + +### loading/loadKey (`client -> server`) + +``` +Server.loading/loadKey( arg0 : STRING ) -> ProofId +``` + + +### loading/loadProblem (`client -> server`) + +``` +Server.loading/loadProblem( arg0 : ProblemDefinition ) -> ProofId +``` + + +### loading/loadTerm (`client -> server`) + +``` +Server.loading/loadTerm( arg0 : STRING ) -> ProofId +``` + + +### meta/available_macros (`client -> server`) + +``` +Server.meta/available_macros( ) -> ProofMacroDesc[] +``` + + +### meta/available_script_commands (`client -> server`) + +``` +Server.meta/available_script_commands( ) -> ProofScriptCommandDesc[] +``` + + +### meta/version (`client -> server`) + +``` +Server.meta/version( ) -> STRING +``` + + +### proofTree/children (`client -> server`) + +``` +Server.proofTree/children( arg0 : ProofId, arg1 : TreeNodeId ) -> TreeNodeDesc[] +``` + + +### proofTree/root (`client -> server`) + +``` +Server.proofTree/root( arg0 : ProofId ) -> TreeNodeDesc +``` + + +### proofTree/subtree (`client -> server`) + +``` +Server.proofTree/subtree( arg0 : ProofId, arg1 : TreeNodeId ) -> TreeNodeDesc[] +``` + + +### server/exit (`client ~~> server`) + +``` +Server.server/exit( ) **async** +``` + + +### server/setTrace (`client ~~> server`) + +``` +Server.server/setTrace( arg0 : SetTraceParams ) **async** +``` + + +### server/shutdown (`client -> server`) + +``` +Server.server/shutdown( ) -> BOOL +``` + + diff --git a/api.py b/api.py new file mode 100644 index 00000000000..c83050a763e --- /dev/null +++ b/api.py @@ -0,0 +1,374 @@ +import enum +import abc +import typing +class ExampleDesc: + """""" + + name : str + description : str + +class ProofScriptCommandDesc: + """""" + + +class ProofMacroDesc: + """""" + + name : str + category : str + description : str + scriptCommandName : str + +class TraceValue(enum.Enum): + """""" + + Off = None + Message = None + All = None + +class SetTraceParams: + """""" + + value : TraceValue + +class EnvironmentId: + """""" + + envId : str + +class ProofId: + """""" + + env : EnvironmentId + proofId : str + +class TreeNodeDesc: + """""" + + +class TreeNodeId: + """""" + + id : str + +class NodeId: + """""" + + proofId : ProofId + nodeId : int + +class PrintOptions: + """""" + + unicode : bool + width : int + indentation : int + pure : bool + termLabels : bool + +class NodeTextId: + """""" + + nodeId : NodeId + nodeTextId : int + +class NodeTextDesc: + """""" + + id : NodeTextId + result : str + +class TermActionId: + """""" + + nodeId : NodeId + pio : str + id : str + +class TermActionKind(enum.Enum): + """""" + + BuiltIn = None + Script = None + Macro = None + Taclet = None + +class TermActionDesc: + """""" + + commandId : TermActionId + displayName : str + description : str + category : str + kind : TermActionKind + +class List: + """""" + + +class SortDesc: + """""" + + string : str + documentation : str + extendsSorts : List + anAbstract : bool + s : str + +class FunctionDesc: + """""" + + name : str + sort : str + retSort : SortDesc + argSorts : List + rigid : bool + unique : bool + skolemConstant : bool + +class ContractId: + """""" + + envId : EnvironmentId + contractId : int + +class ContractDesc: + """""" + + contractId : ContractId + name : str + displayName : str + typeName : str + htmlText : str + plainText : str + +class LoadParams: + """""" + + keyFile : str + javaFile : str + classPath : List + bootClassPath : str + includes : List + +class ProblemDefinition: + """""" + + sorts : List + functions : List + predicates : List + antecTerms : List + succTerms : List + +class LogTraceParams: + """""" + + messag : str + verbose : str + +class MessageType(enum.Enum): + """""" + + Unused = None + Error = None + Warning = None + Info = None + Log = None + Debug = None + +class ShowMessageParams: + """""" + + type : MessageType + message : str + +class MessageActionItem[]: + """""" + + +class ShowMessageRequestParams: + """""" + + type : MessageType + message : str + actions : MessageActionItem[] + +class MessageActionItem: + """""" + + title : str + +class Range: + """""" + + start : int + end : int + +class ShowDocumentParams: + """""" + + uri : str + external : bool + takeFocus : bool + selection : Range + +class ShowDocumentResult: + """""" + + success : bool + +class TaskFinishedInfo: + """""" + + +class TaskStartedInfo: + """""" + + +class KeyServer(): + def env_contracts(self, arg0 : EnvironmentId) -> typing.List[ContractDesc]: + """""" + + return self.rpc.call_sync("env/contracts", ) + + def env_functions(self, arg0 : EnvironmentId) -> typing.List[FunctionDesc]: + """""" + + return self.rpc.call_sync("env/functions", ) + + def env_openContract(self, arg0 : ContractId) -> ProofId: + """""" + + return self.rpc.call_sync("env/openContract", ) + + def env_sorts(self, arg0 : EnvironmentId) -> typing.List[SortDesc]: + """""" + + return self.rpc.call_sync("env/sorts", ) + + def examples_list(self, ) -> typing.List[ExampleDesc]: + """""" + + return self.rpc.call_sync("examples/list", ) + + def goal_actions(self, arg0 : NodeTextId, arg1 : int) -> typing.List[TermActionDesc]: + """""" + + return self.rpc.call_sync("goal/actions", ) + + def goal_apply_action(self, arg0 : TermActionId) -> typing.List[TermActionDesc]: + """""" + + return self.rpc.call_sync("goal/apply_action", ) + + def goal_free(self, arg0 : NodeTextId): + """""" + + return self.rpc.call_async("goal/free", ) + + def goal_print(self, arg0 : NodeId, arg1 : PrintOptions) -> NodeTextDesc: + """""" + + return self.rpc.call_sync("goal/print", ) + + def loading_load(self, arg0 : LoadParams) -> typing.Union[EnvironmentId, ProofId]: + """""" + + return self.rpc.call_sync("loading/load", ) + + def loading_loadExample(self, arg0 : str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadExample", ) + + def loading_loadKey(self, arg0 : str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadKey", ) + + def loading_loadProblem(self, arg0 : ProblemDefinition) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadProblem", ) + + def loading_loadTerm(self, arg0 : str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadTerm", ) + + def meta_available_macros(self, ) -> typing.List[ProofMacroDesc]: + """""" + + return self.rpc.call_sync("meta/available_macros", ) + + def meta_available_script_commands(self, ) -> typing.List[ProofScriptCommandDesc]: + """""" + + return self.rpc.call_sync("meta/available_script_commands", ) + + def meta_version(self, ) -> STRING: + """""" + + return self.rpc.call_sync("meta/version", ) + + def proofTree_children(self, arg0 : ProofId, arg1 : TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self.rpc.call_sync("proofTree/children", ) + + def proofTree_root(self, arg0 : ProofId) -> TreeNodeDesc: + """""" + + return self.rpc.call_sync("proofTree/root", ) + + def proofTree_subtree(self, arg0 : ProofId, arg1 : TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self.rpc.call_sync("proofTree/subtree", ) + + def server_exit(self, ): + """""" + + return self.rpc.call_async("server/exit", ) + + def server_setTrace(self, arg0 : SetTraceParams): + """""" + + return self.rpc.call_async("server/setTrace", ) + + def server_shutdown(self, ) -> BOOL: + """""" + + return self.rpc.call_sync("server/shutdown", ) + +class Client(abc.AbcMeta): + @abstractmethod + def client_logTrace(self, arg0 : LogTraceParams): + """""" + + pass + + @abstractmethod + def client_sayHello(self, arg0 : str): + """""" + + pass + + @abstractmethod + def client_showDocument(self, arg0 : ShowDocumentParams) -> ShowDocumentResult: + """""" + + pass + + @abstractmethod + def client_sm(self, arg0 : ShowMessageParams): + """""" + + pass + + @abstractmethod + def client_userResponse(self, arg0 : ShowMessageRequestParams) -> MessageActionItem: + """""" + + pass + diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 378cfee9470..ee16ea09a56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -12,6 +12,7 @@ import java.util.LinkedList; import java.util.List; import java.util.ListIterator; +import java.util.stream.Stream; import de.uka.ilkd.key.logic.RenamingTable; import de.uka.ilkd.key.logic.Sequent; @@ -836,4 +837,8 @@ public int getStepIndex() { void setStepIndex(int stepIndex) { this.stepIndex = stepIndex; } + + public Stream childrenStream() { + return children.stream(); + } } diff --git a/keyext.api.doc/build.gradle b/keyext.api.doc/build.gradle index f7aadd6467c..84a1789e01f 100644 --- a/keyext.api.doc/build.gradle +++ b/keyext.api.doc/build.gradle @@ -1,4 +1,5 @@ dependencies { + implementation(project(":keyext.api")) implementation("com.github.javaparser:javaparser-core:3.25.5") implementation("com.github.javaparser:javaparser-symbol-solver-core:3.25.5") } \ No newline at end of file diff --git a/keyext.api.doc/src/main/java/DocGen.java b/keyext.api.doc/src/main/java/DocGen.java new file mode 100644 index 00000000000..36aed393607 --- /dev/null +++ b/keyext.api.doc/src/main/java/DocGen.java @@ -0,0 +1,189 @@ +import java.io.PrintWriter; +import java.io.StringWriter; +import java.util.Comparator; +import java.util.function.Supplier; +import java.util.stream.Collectors; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public class DocGen implements Supplier { + private final Metamodel.KeyApi metamodel; + private PrintWriter out; + private final StringWriter target = new StringWriter(); + + public DocGen(Metamodel.KeyApi metamodel) { + this.metamodel = metamodel; + } + + @Override + public String get() { + try (var out = new PrintWriter(target)) { + this.out = out; + printHeader(); + + out.format("## Types%n"); + metamodel.types() + .stream().sorted(Comparator.comparing(Metamodel.Type::name)) + .forEach(this::printType); + + out.format("## Endpoints%n"); + metamodel.endpoints() + .stream().sorted(Comparator.comparing(Metamodel.Endpoint::name)) + .forEach(this::endpoints); + printFooter(); + } + return target.toString(); + } + + private void printFooter() { + + } + + private void printHeader() { + + + } + + private void endpoints(Metamodel.Endpoint endpoint) { + //out.format("## Group: %s%n%n", getJsonSegment(typeDeclaration)); + //out.println(getJavaDoc(typeDeclaration)); + //out.println("\n"); + + var direction = ""; + if (endpoint instanceof Metamodel.ServerRequest sr) + direction = "client -> server"; + else if (endpoint instanceof Metamodel.ClientRequest sr) + direction = "server -> client"; + else if (endpoint instanceof Metamodel.ServerNotification sr) + direction = "client ~~> server"; + else if (endpoint instanceof Metamodel.ClientNotification sr) + direction = "server ~~> client"; + + out.format("### %s (`%s`) %n%n", endpoint.name(), direction); + out.format("```%n"); + var args = endpoint.args(); + final var a = args.stream() + .map(it -> "%s : %s".formatted(it.name(), it.type())) + .collect(Collectors.joining(", ")); + if (endpoint instanceof Metamodel.ServerRequest sr) { + out.format("Server.%s( %s ) -> %s%n", endpoint.name(), a, sr.returnType().name()); + } else if (endpoint instanceof Metamodel.ClientRequest sr) + out.format("Client.%s( %s ) -> %s%n", endpoint.name(), a, sr.returnType().name()); + else if (endpoint instanceof Metamodel.ServerNotification sr) + out.format("Server.%s( %s ) **async**%n", endpoint.name(), a); + else if (endpoint instanceof Metamodel.ClientNotification sr) + out.format("Client.%s( %s ) **async**%n", endpoint.name(), a); + out.format("```%n"); + + out.println(endpoint.documentation()); + out.println(); + } + + private void printType(Metamodel.Type type) { + out.format("### Type: %s%n", type.name()); + if (type instanceof Metamodel.ObjectType ot) { + out.format(""" + ``` + type %s { + %s + } + ``` + """.formatted(type.name(), + ot.fields().stream().sorted(Comparator.comparing(Metamodel.Field::name)) + .map(it -> "\t%s : %s".formatted(it.name(), it.type())) + .collect(Collectors.joining("\n")))); + } + + if (type instanceof Metamodel.EnumType et) { + out.format(""" + ``` + enum %s { %s } + ``` + """.formatted(type.name(), String.join(", ", et.values()) + )); + out.format(type.documentation()); + } + out.format(type.documentation()); + out.println(); + } + + /* + private static String getCallName (MethodDeclaration m, TypeDeclaration < ?>td){ + var annotationExpr = m.getAnnotationByName("JsonNotification").or( + () -> m.getAnnotationByName("JsonRequest")) + .orElseThrow(); + + var segment = getJsonSegment(td) + "/"; + String name = ""; + + if (annotationExpr.isMarkerAnnotationExpr()) { + name = m.getNameAsString(); + } else if (annotationExpr.isSingleMemberAnnotationExpr()) { + var sma = annotationExpr.asSingleMemberAnnotationExpr(); + name = sma.getMemberValue().asLiteralStringValueExpr().getValue(); + } else { + var ne = annotationExpr.asNormalAnnotationExpr(); + for (MemberValuePair pair : ne.getPairs()) { + switch (pair.getName().asString()) { + case "value": + name = pair.getValue().asLiteralStringValueExpr().getValue(); + break; + case "useSegment": + if (!pair.getValue().asBooleanLiteralExpr().getValue()) { + segment = ""; + } + } + } + } + return segment + name; + } + + @Nonnull + private static String getJavaDoc (NodeWithJavadoc < ? > typeDeclaration){ + if (typeDeclaration.getJavadoc().isPresent()) { + final var javadoc = typeDeclaration.getJavadoc().get(); + return javadoc.getDescription().toText() + + "\n\n" + + javadoc.getBlockTags().stream().map(it -> "* " + it.toText()) + .collect(Collectors.joining("\n")); + } + return ""; + } + + private static String type (MethodDeclaration method){ + if (method.getAnnotationByName("JsonNotification").isPresent()) + return "notification"; + if (method.getAnnotationByName("JsonRequest").isPresent()) + return "request"; + return ""; + } + + private static boolean isExported (MethodDeclaration method){ + return method.getAnnotationByName("JsonNotification").isPresent() + || method.getAnnotationByName("JsonRequest").isPresent(); + } + + private void printHeader () { + out.format("# KeY-API%n%n"); + } + + private void printFooter () { + } + + + /* + private static boolean hasJsonSegment(TypeDeclaration it) { + return it.getAnnotationByName("JsonSegment").isPresent(); + } + + private static String getJsonSegment(TypeDeclaration it) { + var ae = it.getAnnotationByName("JsonSegment").get(); + return ae.asSingleMemberAnnotationExpr().getMemberValue() + .asLiteralStringValueExpr().getValue(); + } + */ + +} + diff --git a/keyext.api.doc/src/main/java/ExtractMetaData.java b/keyext.api.doc/src/main/java/ExtractMetaData.java index a9df59adef8..2855e390f75 100644 --- a/keyext.api.doc/src/main/java/ExtractMetaData.java +++ b/keyext.api.doc/src/main/java/ExtractMetaData.java @@ -1,25 +1,27 @@ -import com.github.javaparser.ParseResult; +import com.github.javaparser.JavaParser; import com.github.javaparser.ParserConfiguration; -import com.github.javaparser.ast.body.MethodDeclaration; -import com.github.javaparser.ast.body.TypeDeclaration; -import com.github.javaparser.ast.expr.MemberValuePair; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.comments.Comment; import com.github.javaparser.ast.nodeTypes.NodeWithJavadoc; -import com.github.javaparser.javadoc.JavadocBlockTag; -import com.github.javaparser.resolution.SymbolResolver; -import com.github.javaparser.resolution.TypeSolver; -import com.github.javaparser.symbolsolver.JavaSymbolSolver; -import com.github.javaparser.symbolsolver.resolution.typesolvers.TypeSolverBuilder; -import com.github.javaparser.utils.SourceRoot; - -import javax.annotation.Nonnull; -import java.io.FileWriter; +import com.google.gson.*; +import de.uka.ilkd.key.proof.Proof; +import org.eclipse.lsp4j.jsonrpc.messages.Either; +import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.remoteapi.KeyApi; +import org.keyproject.key.api.remoteclient.ClientApi; +import sun.misc.Unsafe; + +import java.io.File; import java.io.IOException; import java.io.PrintWriter; +import java.lang.reflect.*; +import java.nio.file.Files; +import java.nio.file.Path; import java.nio.file.Paths; -import java.util.Arrays; -import java.util.Comparator; -import java.util.List; -import java.util.stream.Collectors; +import java.util.*; +import java.util.concurrent.CompletableFuture; /** * @author Alexander Weigl @@ -28,135 +30,250 @@ public class ExtractMetaData { private static PrintWriter out; - public static void main(String[] args) throws IOException { - System.out.println("XXX" + Arrays.toString(args)); - ParserConfiguration config = new ParserConfiguration(); - config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_17_PREVIEW); - /*config.setAttributeComments(true); - config.setLexicalPreservationEnabled(false); - config.setStoreTokens(false); - config.setIgnoreAnnotationsWhenAttributingComments(true); - config.setDoNotAssignCommentsPrecedingEmptyLines(true);*/ - //var root = Paths.get(args[0]); - TypeSolver typeSolver = new TypeSolverBuilder() - .withSourceCode("keyext.api/src/main/java") - .withSourceCode("key.core/src/main/java") - .withSourceCode("key.util/src/main/java") - .withCurrentJRE() - .build(); - SymbolResolver symbolResolver = new JavaSymbolSolver(typeSolver); - config.setSymbolResolver(symbolResolver); - var source = new SourceRoot(Paths.get("keyext.api", "src", "main", "java"), config); - var cu = source.tryToParse(); - var jsonSegment = Comparator.comparing(ExtractMetaData::getJsonSegment); - var segments = cu.stream().filter(ParseResult::isSuccessful) - .filter(it -> it.getResult().get().getPrimaryType().isPresent()) - .map(it -> it.getResult().get().getPrimaryType().get()) - .filter(ExtractMetaData::hasJsonSegment) - .sorted(jsonSegment) - .toList(); + private static final List endpoints = new LinkedList<>(); + private static final List types = new LinkedList<>(); + private static final Metamodel.KeyApi keyApi = new Metamodel.KeyApi(endpoints, types); - try (var out = new PrintWriter(new FileWriter("doc.md"))) { - ExtractMetaData.out = out; - printHeader(segments); - segments.forEach(ExtractMetaData::printDocumentation); - printFooter(segments); + public static void main(String[] args) { + for (Method method : KeyApi.class.getMethods()) { + addServerEndpoint(method); } - // "org.keyproject.key.api.remoteapi.KeyApi"; + for (Method method : ClientApi.class.getMethods()) { + addClientEndpoint(method); + } + + try { + Files.writeString(Paths.get("api.meta.json"), getGson().toJson(keyApi)); + } catch (IOException e) { + e.printStackTrace(); + } + + try { + var n = new DocGen(keyApi); + Files.writeString(Paths.get("api.meta.md"), n.get()); + } catch (IOException e) { + e.printStackTrace(); + } + try { + var n = new PyGen(keyApi); + Files.writeString(Paths.get("api.py"), n.get()); + } catch (IOException e) { + e.printStackTrace(); + } } - private static void printDocumentation(TypeDeclaration typeDeclaration) { - out.format("## Group: %s%n%n", getJsonSegment(typeDeclaration)); - out.println(getJavaDoc(typeDeclaration)); - out.println("\n"); + private static Gson getGson() { + return new GsonBuilder() + .setPrettyPrinting() + .registerTypeAdapter(Type.class, new JsonSerializer() { + @Override + public JsonElement serialize(Metamodel.Type src, Type typeOfSrc, JsonSerializationContext context) { + JsonObject json = (JsonObject) context.serialize(src); + json.addProperty("kind", src.kind()); + return json; + } + }) + .create(); + } - for (MethodDeclaration method : typeDeclaration.getMethods()) { - if (!isExported(method)) continue; + private static void addServerEndpoint(Method method) { + var jsonSegment = method.getDeclaringClass().getAnnotation(JsonSegment.class); + if (jsonSegment == null) return; + var segment = jsonSegment.value(); - String callName = getCallName(method, typeDeclaration); + var req = method.getAnnotation(JsonRequest.class); + var resp = method.getAnnotation(JsonNotification.class); - out.format("### %s (type: %s) %n%n", callName, type(method)); + var args = translate(method.getParameters()); - out.println(getJavaDoc(method)); + if (req != null) { + var mn = callMethodName(method.getName(), segment, req.value(), req.useSegment()); - out.println(); + if (method.getReturnType() == Void.class) { + System.err.println("Found void as return type for a request! " + method); + return; + } + + var retType = getOrFindType(method.getGenericReturnType()); + Objects.requireNonNull(retType, "No retType found " + method.getGenericReturnType()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ServerRequest(mn, documentation, args, retType); + endpoints.add(mm); + return; + } + + if (resp != null) { + var mn = callMethodName(method.getName(), segment, resp.value(), resp.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ServerNotification(mn, documentation, args); + endpoints.add(mm); + return; } + + throw new IllegalStateException(); } - private static String getCallName(MethodDeclaration m, TypeDeclaration td) { - var annotationExpr = m.getAnnotationByName("JsonNotification").or( - () -> m.getAnnotationByName("JsonRequest")) - .orElseThrow(); + private static String findDocumentation(Method method) { + // TODO get compilation, get type, find method, getJavaDocComment() + return ""; + } - var segment = getJsonSegment(td) + "/"; - String name = ""; + private static List translate(Parameter[] parameters) { + return Arrays.stream(parameters).map(ExtractMetaData::translate).toList(); + } - if (annotationExpr.isMarkerAnnotationExpr()) { - name = m.getNameAsString(); - } else if (annotationExpr.isSingleMemberAnnotationExpr()) { - var sma = annotationExpr.asSingleMemberAnnotationExpr(); - name = sma.getMemberValue().asLiteralStringValueExpr().getValue(); - } else { - var ne = annotationExpr.asNormalAnnotationExpr(); - for (MemberValuePair pair : ne.getPairs()) { - switch (pair.getName().asString()) { - case "value": - name = pair.getValue().asLiteralStringValueExpr().getValue(); - break; - case "useSegment": - if (!pair.getValue().asBooleanLiteralExpr().getValue()) { - segment = ""; - } - } - } - } - return segment + name; + private static Metamodel.Argument translate(Parameter parameter) { + var type = getOrFindType(parameter.getType()).name(); + return new Metamodel.Argument(parameter.getName(), type); } + private static Metamodel.Type getOrFindType(Class type) { + System.out.println(type); + if (type == CompletableFuture.class) { + return getOrFindType(type.getTypeParameters()[0].getClass()); + } - @Nonnull - private static String getJavaDoc(NodeWithJavadoc typeDeclaration) { - if (typeDeclaration.getJavadoc().isPresent()) { - final var javadoc = typeDeclaration.getJavadoc().get(); - return javadoc.getDescription().toText() - + "\n\n" - + javadoc.getBlockTags().stream().map(it -> "* " + it.toText()) - .collect(Collectors.joining("\n")); + if (type == Unsafe.class || type == Class.class || type == Constructor.class || type == Proof.class) { + throw new IllegalStateException("Forbidden class reached!"); } - return ""; + + if (type == String.class) return Metamodel.BuiltinType.STRING; + if (type == Integer.class) return Metamodel.BuiltinType.INT; + if (type == Double.class) return Metamodel.BuiltinType.DOUBLE; + if (type == Long.class) return Metamodel.BuiltinType.LONG; + if (type == Character.class) return Metamodel.BuiltinType.LONG; + if (type == File.class) return Metamodel.BuiltinType.STRING; + if (type == Boolean.class) return Metamodel.BuiltinType.BOOL; + if (type == Boolean.TYPE) return Metamodel.BuiltinType.BOOL; + + if (type == Integer.TYPE) return Metamodel.BuiltinType.INT; + if (type == Double.TYPE) return Metamodel.BuiltinType.DOUBLE; + if (type == Long.TYPE) return Metamodel.BuiltinType.LONG; + if (type == Character.TYPE) return Metamodel.BuiltinType.LONG; + + System.out.println(type); + var t = types.stream().filter(it -> it.name().equals(type.getSimpleName())).findFirst(); + if (t.isPresent()) return t.get(); + var a = createType(type); + types.add(a); + return a; } - private static String type(MethodDeclaration method) { - if (method.getAnnotationByName("JsonNotification").isPresent()) - return "notification"; - if (method.getAnnotationByName("JsonRequest").isPresent()) - return "request"; - return ""; + private static Metamodel.Type createType(Class type) { + final var documentation = findDocumentation(type); + if (type.isEnum()) + return new Metamodel.EnumType(type.getSimpleName(), + Arrays.stream(type.getEnumConstants()).map(Object::toString).toList(), + documentation); + + + var obj = new Metamodel.ObjectType(type.getSimpleName(), new ArrayList<>(), documentation); + final var list = Arrays.stream(type.getDeclaredFields()) + .map(it -> new Metamodel.Field(it.getName(), getOrFindType(it.getType()).name())) + .toList(); + obj.fields().addAll(list); + return obj; } - private static boolean isExported(MethodDeclaration method) { - return method.getAnnotationByName("JsonNotification").isPresent() - || method.getAnnotationByName("JsonRequest").isPresent(); + private static String findDocumentation(Class type) { + var parser = initJavaParser(); + var fileName = findFileForType(type); + + if (Files.exists(fileName)) { + try { + return parser.parse(fileName).getResult().flatMap(CompilationUnit::getPrimaryType) + .flatMap(NodeWithJavadoc::getJavadocComment) + .map(Comment::getContent).orElse(""); + } catch (IOException e) { + e.printStackTrace(); + return ""; + } + } else return ""; } - private static void printHeader(List> segments) { - out.format("# KeY-API%n%n"); + private static Path findFileForType(Class type) { + final var folderString = type.getPackageName().replaceAll("\\.", "/"); + var folder = Paths.get("keyext.api", "src", "main", "java", folderString); + final Class declaringClass = type.getDeclaringClass(); + var fileName = (declaringClass != null ? declaringClass : type).getSimpleName() + ".java"; + var file = folder.resolve(fileName); + return file; } - private static void printFooter(List> segments) { + private static void addClientEndpoint(Method method) { + var jsonSegment = method.getDeclaringClass().getAnnotation(JsonSegment.class); + var segment = jsonSegment.value(); + + var req = method.getAnnotation(JsonRequest.class); + var resp = method.getAnnotation(JsonNotification.class); + + var args = translate(method.getParameters()); + + if (req != null) { + var retType = getOrFindType(method.getGenericReturnType()); + Objects.requireNonNull(retType); + var mn = callMethodName(method.getName(), segment, req.value(), req.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ClientRequest(mn, documentation, args, retType); + endpoints.add(mm); + return; + } + + if (resp != null) { + var mn = callMethodName(method.getName(), segment, resp.value(), resp.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ClientNotification(mn, documentation, args); + endpoints.add(mm); + } + } + private static String callMethodName(String method, String segment, String userValue, boolean useSegment) { + if (!useSegment) { + if (userValue == null || userValue.isBlank()) { + return method; + } else { + return userValue; + } + } else { + if (userValue == null || userValue.isBlank()) { + return segment + "/" + method; + } else { + return segment + "/" + userValue; + } + } } + private static Metamodel.Type getOrFindType(Type genericReturnType) { + if (genericReturnType instanceof Class c) return getOrFindType(c); + if (genericReturnType instanceof ParameterizedType pt) { + if (Objects.equals(pt.getRawType().getTypeName(), CompletableFuture.class.getTypeName())) { + return getOrFindType(pt.getActualTypeArguments()[0]); + } + if (Objects.equals(pt.getRawType().getTypeName(), List.class.getTypeName())) { + var base = getOrFindType(pt.getActualTypeArguments()[0]); + return new Metamodel.ListType(base, ""); + } - private static boolean hasJsonSegment(TypeDeclaration it) { - return it.getAnnotationByName("JsonSegment").isPresent(); + if (Objects.equals(pt.getRawType().getTypeName(), Either.class.getTypeName())) { + var base1 = getOrFindType(pt.getActualTypeArguments()[0]); + var base2 = getOrFindType(pt.getActualTypeArguments()[1]); + return new Metamodel.EitherType(base1, base2, ""); + } + } + return null; } - private static String getJsonSegment(TypeDeclaration it) { - var ae = it.getAnnotationByName("JsonSegment").get(); - return ae.asSingleMemberAnnotationExpr().getMemberValue() - .asLiteralStringValueExpr().getValue(); + static JavaParser initJavaParser() { + ParserConfiguration config = new ParserConfiguration(); + config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_17_PREVIEW); + config.setAttributeComments(true); + config.setLexicalPreservationEnabled(false); + config.setStoreTokens(false); + config.setIgnoreAnnotationsWhenAttributingComments(true); + config.setDoNotAssignCommentsPrecedingEmptyLines(true); + return new JavaParser(config); } + } diff --git a/keyext.api.doc/src/main/java/Metamodel.java b/keyext.api.doc/src/main/java/Metamodel.java new file mode 100644 index 00000000000..833699cfe0c --- /dev/null +++ b/keyext.api.doc/src/main/java/Metamodel.java @@ -0,0 +1,93 @@ +import org.jspecify.annotations.NullMarked; + +import java.util.List; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +@NullMarked +public class Metamodel { + public record KeyApi( + List endpoints, + List types + ) { + } + + sealed interface Endpoint { + String name(); + + String documentation(); + + default String kind() { + return getClass().getSimpleName(); + } + + List args(); + } + + public record Argument(String name, String type) { + } + + record ServerRequest(String name, String documentation, List args, Type returnType) implements Endpoint { + } + + record ServerNotification(String name, String documentation, List args) implements Endpoint { + } + + record ClientRequest(String name, String documentation, List args, Type returnType) implements Endpoint { + } + + record ClientNotification(String name, String documentation, List args) implements Endpoint { + } + + record Field(String name, /*Type*/ String type) { + } + + sealed interface Type { + default String kind() { + return getClass().getSimpleName(); + } + + String documentation(); + + String name(); + } + + enum BuiltinType implements Type { + INT, LONG, STRING, BOOL, DOUBLE; + + @Override + public String documentation() { + return "built-in data type"; + } + } + + record ListType(Type type, String documentation) implements Type { + @Override + public String name() { + return type().name() + "[]"; + } + } + + record ObjectType(String typeName, List fields, String documentation) implements Type { + @Override + public String name() { + return typeName; + } + } + + public record EitherType(Type a, Type b, String documentation) implements Type { + @Override + public String name() { + return "either"; + } + } + + public record EnumType(String typeName, List values, String documentation) implements Type { + @Override + public String name() { + return typeName; + } + } +} diff --git a/keyext.api.doc/src/main/java/PyGen.java b/keyext.api.doc/src/main/java/PyGen.java new file mode 100644 index 00000000000..357c2f51e8d --- /dev/null +++ b/keyext.api.doc/src/main/java/PyGen.java @@ -0,0 +1,136 @@ +import java.io.PrintWriter; +import java.io.StringWriter; +import java.util.Comparator; +import java.util.function.Supplier; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public class PyGen implements Supplier { + private final Metamodel.KeyApi metamodel; + private PrintWriter out; + private final StringWriter target = new StringWriter(); + + public PyGen(Metamodel.KeyApi metamodel) { + this.metamodel = metamodel; + } + + @Override + public String get() { + try (var out = new PrintWriter(target)) { + this.out = out; + + out.format(""" + import enum + import abc + import typing + from abc import abstractmethod + """); + + metamodel.types().forEach(this::printType); + server( + metamodel.endpoints() + .stream() + .filter(it -> it instanceof Metamodel.ServerRequest || it instanceof Metamodel.ServerNotification) + .sorted(Comparator.comparing(Metamodel.Endpoint::name))); + + client( + metamodel.endpoints() + .stream() + .filter(it -> it instanceof Metamodel.ClientRequest || it instanceof Metamodel.ClientNotification) + .sorted(Comparator.comparing(Metamodel.Endpoint::name))); + + } + return target.toString(); + } + + private void client(Stream sorted) { + out.format("class Client(abc.AbcMeta):%n"); + sorted.forEach(this::clientEndpoint); + } + + private void clientEndpoint(Metamodel.Endpoint endpoint) { + var args = endpoint.args().stream() + .map(it -> "%s : %s".formatted(it.name(), asPython(it.type()))) + .collect(Collectors.joining(", ")); + out.format(" @abstractmethod%n"); + if (endpoint instanceof Metamodel.ClientRequest sr) { + out.format(" def %s(self, %s) -> %s:%n", endpoint.name().replace("/", "_"), args, asPython(sr.returnType())); + } else { + out.format(" def %s(self, %s):%n", endpoint.name().replace("/", "_"), args); + } + out.format(" \"\"\"%s\"\"\"%n%n", endpoint.documentation()); + out.format(" pass".formatted(endpoint.name(), "")); + out.println(); + out.println(); + } + + private void server(Stream sorted) { + out.format("class KeyServer():%n"); + sorted.forEach(this::serverEndpoint); + } + + private void serverEndpoint(Metamodel.Endpoint endpoint) { + var args = endpoint.args().stream() + .map(it -> "%s : %s".formatted(it.name(), asPython(it.type()))) + .collect(Collectors.joining(", ")); + if (endpoint instanceof Metamodel.ServerRequest sr) { + out.format(" def %s(self, %s) -> %s:%n", endpoint.name().replace("/", "_"), args, + asPython(sr.returnType())); + out.format(" \"\"\"%s\"\"\"%n%n", sr.documentation()); + out.format(" return self.rpc.call_sync(\"%s\", %s)".formatted(endpoint.name(), "")); + } else { + out.format(" def %s(self, %s):%n", endpoint.name().replace("/", "_"), args); + out.format(" \"\"\"%s\"\"\"%n%n", endpoint.documentation()); + out.format(" return self.rpc.call_async(\"%s\", %s)".formatted(endpoint.name(), "")); + } + out.println(); + out.println(); + } + + private void printType(Metamodel.Type type) { + if (type instanceof Metamodel.ObjectType ot) { + out.format("class %s:%n".formatted(type.name())); + out.format(" \"\"\"%s\"\"\"%n%n", type.documentation()); + ot.fields().forEach(it -> out.format(" %s : %s%n".formatted(it.name(), asPython(it.type())))); + } else if (type instanceof Metamodel.EnumType et) { + out.format("class %s(enum.Enum):%n".formatted(type.name())); + out.format(" \"\"\"%s\"\"\"%n%n", type.documentation()); + et.values().forEach(it -> out.format(" %s = None%n".formatted(it))); + } + out.println(); + } + + private String asPython(String typeName) { + return switch (typeName) { + case "INT" -> "int"; + case "LONG" -> "int"; + case "STRING" -> "str"; + case "BOOL" -> "bool"; + case "DOUBLE" -> "float"; + default -> { + var t = findType(typeName); + yield asPython(t); + } + }; + } + + private String asPython(Metamodel.Type t) { + if (t instanceof Metamodel.ListType lt) { + return "typing.List[" + asPython(lt.type()) + "]"; + } + + if (t instanceof Metamodel.EitherType lt) { + return "typing.Union[" + asPython(lt.a()) + ", " + asPython(lt.b()) + "]"; + } + return t.name(); + } + + private Metamodel.Type findType(String typeName) { + return this.metamodel.types().stream().filter(it -> it.name().equals(typeName)).findFirst() + .orElseThrow(() -> new RuntimeException("Could not find type: " + typeName)); + } +} \ No newline at end of file diff --git a/keyext.api/build.gradle b/keyext.api/build.gradle index c2b84249430..fbbbac93898 100644 --- a/keyext.api/build.gradle +++ b/keyext.api/build.gradle @@ -10,10 +10,10 @@ plugins { description "Verification server interface via JSON-RPC" dependencies { - implementation(project(":key.core")) - implementation(project(":key.ui")) + api(project(":key.core")) + api(project(":key.ui")) - implementation("org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.21.1") + api("org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.21.1") implementation("org.eclipse.lsp4j:org.eclipse.lsp4j.websocket.jakarta:0.21.1") implementation("org.eclipse.lsp4j:org.eclipse.lsp4j.websocket.jakarta:0.21.1") implementation("org.eclipse.jetty.websocket:websocket-javax-server:10.0.16") diff --git a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java index fd1b8352356..7ff86ae2c09 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -3,7 +3,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.gui.Example; import de.uka.ilkd.key.gui.ExampleChooser; import de.uka.ilkd.key.macros.ProofMacroFacade; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; @@ -32,6 +31,7 @@ import org.keyproject.key.api.data.*; import org.keyproject.key.api.data.KeyIdentifications.*; import org.keyproject.key.api.internal.NodeText; +import org.keyproject.key.api.remoteapi.ExampleDesc; import org.keyproject.key.api.remoteapi.KeyApi; import org.keyproject.key.api.remoteapi.PrintOptions; import org.keyproject.key.api.remoteclient.ClientApi; @@ -73,13 +73,14 @@ public KeyApiImpl() { @Override @JsonRequest - public CompletableFuture> examples() { - return CompletableFutures.computeAsync((c) -> ExampleChooser.listExamples(ExampleChooser.lookForExamples())); + public CompletableFuture> examples() { + return CompletableFutures.computeAsync((c) -> + ExampleChooser.listExamples(ExampleChooser.lookForExamples()).stream().map(it -> ExampleDesc.from(it)).toList()); } @Override - public CompletableFuture shutdown() { - return CompletableFuture.completedFuture(null); + public CompletableFuture shutdown() { + return CompletableFuture.completedFuture(true); } @Override @@ -192,7 +193,8 @@ private List asNodeDesc(ProofId proofId, Stream nodes) { } private NodeDesc asNodeDesc(ProofId proofId, Node it) { - return new NodeDesc(proofId, it.serialNr(), it.getNodeInfo().getBranchLabel(), it.getNodeInfo().getScriptRuleApplication()); + return new NodeDesc(proofId, it.serialNr(), it.getNodeInfo().getBranchLabel(), + it.getNodeInfo().getScriptRuleApplication()); } @Override @@ -204,10 +206,11 @@ public CompletableFuture tree(ProofId proofId) { } private NodeDesc asNodeDescRecursive(ProofId proofId, Node root) { + final List list = root.childrenStream().map(it -> asNodeDescRecursive(proofId, it)).toList(); return new NodeDesc(new NodeId(proofId, root.serialNr()), root.getNodeInfo().getBranchLabel(), root.getNodeInfo().getScriptRuleApplication(), - root.childrenStream().map(it -> asNodeDescRecursive(proofId, it)).toList() + list ); } diff --git a/keyext.api/src/main/java/org/keyproject/key/api/NodeTextDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/NodeTextDesc.java deleted file mode 100644 index 0a27c633e5a..00000000000 --- a/keyext.api/src/main/java/org/keyproject/key/api/NodeTextDesc.java +++ /dev/null @@ -1,8 +0,0 @@ -package org.keyproject.key.api; - -/** - * @author Alexander Weigl - * @version 1 (29.10.23) - */ -public record NodeTextDesc(NodeTextId id, String result) { -} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/NodeTextId.java b/keyext.api/src/main/java/org/keyproject/key/api/NodeTextId.java index a99bed5fda9..f28001e8c15 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/NodeTextId.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/NodeTextId.java @@ -2,9 +2,3 @@ import org.keyproject.key.api.data.KeyIdentifications.NodeId; -/** - * @author Alexander Weigl - * @version 1 (29.10.23) - */ -public record NodeTextId(NodeId nodeId, int nodeTextId) { -} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java index 51e0053eed6..31714a361d7 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java @@ -9,10 +9,11 @@ import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.*; -import org.checkerframework.checker.nullness.qual.NonNull; +import org.jspecify.annotations.NonNull; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.keyproject.key.api.data.KeyIdentifications; +import org.keyproject.key.api.data.KeyIdentifications.NodeTextId; import org.keyproject.key.api.data.TermActionDesc; import org.keyproject.key.api.data.TermActionKind; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java b/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java index 0698a50a982..6d66823142a 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java @@ -5,8 +5,7 @@ import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import org.checkerframework.checker.nullness.qual.NonNull; -import org.keyproject.key.api.NodeTextId; +import org.jspecify.annotations.NonNull; import org.keyproject.key.api.internal.NodeText; import java.lang.ref.WeakReference; @@ -109,11 +108,12 @@ public record ProofId(EnvironmentId env, String proofId) { /** * @author Alexander Weigl - * @version 1 (13.10.23) + * @version 1 (29.10.23) */ - public record PrintId(String id) { + public record NodeTextId(NodeId nodeId, int nodeTextId) { } + /** * @author Alexander Weigl * @version 1 (13.10.23) diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java index 9e24e0f4cd7..eda5e693f64 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java @@ -1,6 +1,6 @@ package org.keyproject.key.api.data; -import org.checkerframework.checker.nullness.qual.Nullable; +import org.jspecify.annotations.Nullable; import java.util.List; @@ -8,7 +8,8 @@ * @author Alexander Weigl * @version 1 (13.10.23) */ -public record NodeDesc(KeyIdentifications.NodeId nodeid, String branchLabel, +public record NodeDesc(KeyIdentifications.NodeId nodeid, + String branchLabel, boolean scriptRuleApplication, @Nullable List children ) { diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java new file mode 100644 index 00000000000..333b24f1c73 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java @@ -0,0 +1,9 @@ +package org.keyproject.key.api.data; + + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record NodeTextDesc(KeyIdentifications.NodeTextId id, String result) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java index 4e2de0d4010..d952ea3a654 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java @@ -1,6 +1,7 @@ package org.keyproject.key.api.data; -import org.checkerframework.checker.nullness.qual.Nullable; + +import org.jspecify.annotations.Nullable; import java.util.List; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionId.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionId.java deleted file mode 100644 index 96d22acee47..00000000000 --- a/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionId.java +++ /dev/null @@ -1,2 +0,0 @@ -package org.keyproject.key.api.data; - diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeId.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeId.java deleted file mode 100644 index 96d22acee47..00000000000 --- a/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeId.java +++ /dev/null @@ -1,2 +0,0 @@ -package org.keyproject.key.api.data; - diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java index 9ccbb03049f..6c52dfd39aa 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java @@ -10,5 +10,5 @@ @JsonSegment("examples") public interface ExampleApi { @JsonRequest("list") - CompletableFuture> examples(); + CompletableFuture> examples(); } diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleDesc.java new file mode 100644 index 00000000000..c0091943899 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleDesc.java @@ -0,0 +1,13 @@ +package org.keyproject.key.api.remoteapi; + +import de.uka.ilkd.key.gui.Example; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record ExampleDesc(String name, String description) { + public static ExampleDesc from(Example example) { + return new ExampleDesc(example.getName(), example.getDescription()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java index 2f34293f0d5..959ed91570c 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java @@ -3,8 +3,7 @@ import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; -import org.keyproject.key.api.NodeTextDesc; -import org.keyproject.key.api.NodeTextId; +import org.keyproject.key.api.data.NodeTextDesc; import org.keyproject.key.api.data.*; import org.keyproject.key.api.data.KeyIdentifications.*; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java index ddd1fe408e6..00e85b9e021 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java @@ -29,7 +29,7 @@ public interface ServerManagement { * error: code and message set in case an exception happens during shutdown request. */ @JsonRequest - CompletableFuture shutdown(); + CompletableFuture shutdown(); /** * Exit Notification (:arrow_right:) diff --git a/keyext.api/src/main/python/keyapi/rpc.py b/keyext.api/src/main/python/keyapi/rpc.py deleted file mode 100644 index 89dc6f3e041..00000000000 --- a/keyext.api/src/main/python/keyapi/rpc.py +++ /dev/null @@ -1,76 +0,0 @@ -import abc -import json -from abc import abstractmethod -from multiprocessing import Process, SimpleQueue, Lock, Value - - -class Client(abc.ABC): - @abstractmethod - def handle(self, response): - pass - - -class JsonRPCHandler: - client: Client - - def __init__(self, in_stream, out_stream): - self.input = in_stream - self.out = out_stream - self.__id = 0 - self.client: Client - - self._events = dict() - self._responses = dict() - - # t: Process = Process(target=self.__read) - # t.start() - - def read_message(self): - length = 0 - for clength in self.input.readlines(): - if clength.startswith("Content-Length:"): - length = int(clength[14:]) - break - - payload = self.input.read(2 + length) - r = json.loads(payload) - if "id" in r: # JSON response for request - rid = r["id"] - # self._responses[rid] = r - # if rid in self._events: - # self._events[rid].set() - else: # JSON notification - self.client.handle(r) - return r - - def __read(self): - while True: - self.read_message() - - # def __create_event(self, number): - # self._events[number] = Event() - - def _send(self, method, params): - self.__id += 1 - id = self.__id - # self.__create_event(self.__id) - req = {"jsonrpc": "2.0", "method": method, "params": params, "id": self.__id} - - self._write(json.dumps(req)) - # self._wait_for(self.__id) - - r = dict() - while "id" in r and str(r[id]) != str(id): - r = self.read_message() - return r - - def _write(self, msg): - length = len(msg) - self.out.write(f"Content-Length: {length}\r\n") - self.out.write("\r\n") - self.out.write(msg) - self.out.write("\r\n") - self.out.flush() - - # def _wait_for(self, rid): - # self._events[rid].wait() diff --git a/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java b/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java index ae34b339231..5e0c87e06f5 100644 --- a/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java +++ b/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java @@ -5,7 +5,6 @@ import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import org.keyproject.key.api.adapters.KeyAdapter; import org.keyproject.key.api.remoteapi.KeyApi; import org.keyproject.key.api.remoteclient.ClientApi; @@ -16,7 +15,6 @@ import java.util.Collections; import java.util.concurrent.ExecutionException; import java.util.concurrent.Future; -import java.util.concurrent.TimeoutException; import java.util.logging.Level; import java.util.logging.Logger; @@ -34,7 +32,7 @@ void setup() throws IOException { inClient.connect(outServer); outClient.connect(inServer); - KeyApiImpl impl = new KeyApiImpl(new KeyAdapter(null)); + KeyApiImpl impl = new KeyApiImpl(); Launcher serverLauncher = StartServer.launch(outServer, inServer, impl); impl.setClientApi(serverLauncher.getRemoteProxy()); @@ -58,7 +56,7 @@ void setup() throws IOException { } @AfterEach - void teardown() throws ExecutionException, InterruptedException, TimeoutException { + void teardown() { serverListening.cancel(true); clientListening.cancel(true); } diff --git a/keyext.api/src/main/python/keyapi/__init__.py b/keyext.client.python/keyapi/__init__.py similarity index 54% rename from keyext.api/src/main/python/keyapi/__init__.py rename to keyext.client.python/keyapi/__init__.py index 8523f3801f5..4a913b39b2e 100644 --- a/keyext.api/src/main/python/keyapi/__init__.py +++ b/keyext.client.python/keyapi/__init__.py @@ -1,13 +1,4 @@ -from keyapi.rpc import JsonRPCHandler, Client - - -class KeyClient(Client): - def __int__(self): - pass - - def handle(self, res): - print(res) - +from keyapi.rpc import * class KeyStub(JsonRPCHandler): def __init__(self, input, output): diff --git a/keyext.client.python/keyapi/rpc.py b/keyext.client.python/keyapi/rpc.py new file mode 100644 index 00000000000..02ba2be474b --- /dev/null +++ b/keyext.client.python/keyapi/rpc.py @@ -0,0 +1,200 @@ +import enum +import json +import sys +import threading +from io import TextIOWrapper +from typing import Dict + +JSON_RPC_REQ_FORMAT = "Content-Length: {json_string_len}\r\n\r\n{json_string}" +LEN_HEADER = "Content-Length: " +TYPE_HEADER = "Content-Type: " + + +class MyEncoder(json.JSONEncoder): + """ + Encodes an object in JSON + """ + + def default(self, o): # pylint: disable=E0202 + return o.__dict__ + + +class ResponseError(Exception): + def __init__(self, error_code, message): + super().__init__(message) + self.error_code = error_code + + +class ErrorCodes(enum.Enum): + ParseError = 1 + + +class JsonRpcEndpoint(object): + ''' + Thread safe JSON RPC endpoint implementation. Responsible to recieve and send JSON RPC messages, as described in the + protocol. More information can be found: https://www.jsonrpc.org/ + ''' + + def __init__(self, stdin, stdout): + self.stdin = stdin + self.stdout = stdout + self.read_lock = threading.Lock() + self.write_lock = threading.Lock() + + @staticmethod + def __add_header(json_string): + ''' + Adds a header for the given json string + + :param str json_string: The string + :return: the string with the header + ''' + return JSON_RPC_REQ_FORMAT.format(json_string_len=len(json_string), json_string=json_string) + + def send_request(self, message): + ''' + Sends the given message. + + :param dict message: The message to send. + ''' + json_string = json.dumps(message, cls=MyEncoder) + jsonrpc_req = self.__add_header(json_string) + with self.write_lock: + self.stdin.write(jsonrpc_req.encode()) + self.stdin.flush() + + def recv_response(self): + ''' + Recives a message. + + :return: a message + ''' + with self.read_lock: + message_size = None + while True: + # read header + line = self.stdout.readline() + if not line: + # server quit + return None + line = line.decode("utf-8") + if not line.endswith("\r\n"): + raise ResponseError(ErrorCodes.ParseError, "Bad header: missing newline") + # remove the "\r\n" + line = line[:-2] + if line == "": + # done with the headers + break + elif line.startswith(LEN_HEADER): + line = line[len(LEN_HEADER):] + if not line.isdigit(): + raise ResponseError(ErrorCodes.ParseError, + "Bad header: size is not int") + message_size = int(line) + elif line.startswith(TYPE_HEADER): + # nothing todo with type for now. + pass + else: + raise ResponseError(ErrorCodes.ParseError, "Bad header: unkown header") + if not message_size: + raise ResponseError(ErrorCodes.ParseError, "Bad header: missing size") + + jsonrpc_res = self.stdout.read(message_size).decode("utf-8") + return json.loads(jsonrpc_res) + + +class LspEndpoint(threading.Thread): + def __init__(self, json_rpc_endpoint: JsonRpcEndpoint, method_callbacks=None, notify_callbacks=None, timeout=2): + super().__init__() + self.json_rpc_endpoint: JsonRpcEndpoint = json_rpc_endpoint + self.notify_callbacks: Dict = notify_callbacks or {} + self.method_callbacks: Dict = method_callbacks or {} + self.event_dict = {} + self.response_dict = {} + self.next_id = 0 + self._timeout = timeout + self.shutdown_flag = False + + def handle_result(self, rpc_id, result, error): + self.response_dict[rpc_id] = (result, error) + cond = self.event_dict[rpc_id] + cond.acquire() + cond.notify() + cond.release() + + def stop(self): + self.shutdown_flag = True + + def run(self): + while not self.shutdown_flag: + try: + jsonrpc_message = self.json_rpc_endpoint.recv_response() + if jsonrpc_message is None: + print("server quit") + break + method = jsonrpc_message.get("method") + result = jsonrpc_message.get("result") + error = jsonrpc_message.get("error") + rpc_id = jsonrpc_message.get("id") + params = jsonrpc_message.get("params") + + if method: + if rpc_id: + # a call for method + if method not in self.method_callbacks: + raise ResponseError(ErrorCodes.MethodNotFound, + "Method not found: {method}".format(method=method)) + result = self.method_callbacks[method](params) + self.send_response(rpc_id, result, None) + else: + # a call for notify + if method not in self.notify_callbacks: + # Have nothing to do with this. + print("Notify method not found: {method}.".format(method=method)) + else: + self.notify_callbacks[method](params) + else: + self.handle_result(rpc_id, result, error) + except ResponseError as e: + self.send_response(rpc_id, None, e) + + def send_response(self, id, result, error): + message_dict = {"jsonrpc": "2.0", "id": id} + if result: + message_dict["result"] = result + if error: + message_dict["error"] = error + self.json_rpc_endpoint.send_request(message_dict) + + def send_message(self, method_name, params, id=None): + message_dict = {} + message_dict["jsonrpc"] = "2.0" + if id is not None: + message_dict["id"] = id + message_dict["method"] = method_name + message_dict["params"] = params + self.json_rpc_endpoint.send_request(message_dict) + + def call_method(self, method_name, **kwargs): + current_id = self.next_id + self.next_id += 1 + cond = threading.Condition() + self.event_dict[current_id] = cond + + cond.acquire() + self.send_message(method_name, kwargs, current_id) + if self.shutdown_flag: + return None + + if not cond.wait(timeout=self._timeout): + raise TimeoutError() + cond.release() + + self.event_dict.pop(current_id) + result, error = self.response_dict.pop(current_id) + if error: + raise ResponseError(error.get("code"), error.get("message"), error.get("data")) + return result + + def send_notification(self, method_name, **kwargs): + self.send_message(method_name, kwargs) diff --git a/keyext.api/src/main/python/main.py b/keyext.client.python/main.py similarity index 100% rename from keyext.api/src/main/python/main.py rename to keyext.client.python/main.py diff --git a/keyext.client.python/rwtest.py b/keyext.client.python/rwtest.py new file mode 100644 index 00000000000..312532192dc --- /dev/null +++ b/keyext.client.python/rwtest.py @@ -0,0 +1,402 @@ +import enum +import abc +import typing +from abc import abstractmethod + + +class ExampleDesc: + """""" + + name: str + description: str + + +class ProofScriptCommandDesc: + """""" + + +class ProofMacroDesc: + """""" + + name: str + category: str + description: str + scriptCommandName: str + + +class TraceValue(enum.Enum): + """""" + + Off = None + Message = None + All = None + + +class SetTraceParams: + """""" + + value: TraceValue + + +class EnvironmentId: + """""" + + envId: str + + +class ProofId: + """""" + + env: EnvironmentId + proofId: str + + +class TreeNodeDesc: + """""" + + +class TreeNodeId: + """""" + + id: str + + +class NodeId: + """""" + + proofId: ProofId + nodeId: int + + +class PrintOptions: + """""" + + unicode: bool + width: int + indentation: int + pure: bool + termLabels: bool + + +class NodeTextId: + """""" + + nodeId: NodeId + nodeTextId: int + + +class NodeTextDesc: + """""" + + id: NodeTextId + result: str + + +class TermActionId: + """""" + + nodeId: NodeId + pio: str + id: str + + +class TermActionKind(enum.Enum): + """""" + + BuiltIn = None + Script = None + Macro = None + Taclet = None + + +class TermActionDesc: + """""" + + commandId: TermActionId + displayName: str + description: str + category: str + kind: TermActionKind + + +class List: + """""" + + +class SortDesc: + """""" + + string: str + documentation: str + extendsSorts: List + anAbstract: bool + s: str + + +class FunctionDesc: + """""" + + name: str + sort: str + retSort: SortDesc + argSorts: List + rigid: bool + unique: bool + skolemConstant: bool + + +class ContractId: + """""" + + envId: EnvironmentId + contractId: int + + +class ContractDesc: + """""" + + contractId: ContractId + name: str + displayName: str + typeName: str + htmlText: str + plainText: str + + +class LoadParams: + """""" + + keyFile: str + javaFile: str + classPath: List + bootClassPath: str + includes: List + + +class ProblemDefinition: + """""" + + sorts: List + functions: List + predicates: List + antecTerms: List + succTerms: List + + +class LogTraceParams: + """""" + + messag: str + verbose: str + + +class MessageType(enum.Enum): + """""" + + Unused = None + Error = None + Warning = None + Info = None + Log = None + Debug = None + + +class ShowMessageParams: + """""" + + type: MessageType + message: str + + + +class ShowMessageRequestParams: + """""" + + type: MessageType + message: str + actions: typing.List[MessageActionItem] + + +class MessageActionItem: + """""" + + title: str + + +class Range: + """""" + + start: int + end: int + + +class ShowDocumentParams: + """""" + + uri: str + external: bool + takeFocus: bool + selection: Range + + +class ShowDocumentResult: + """""" + + success: bool + + +class TaskFinishedInfo: + """""" + + +class TaskStartedInfo: + """""" + + +class KeyServer(): + def env_contracts(self, arg0: EnvironmentId) -> typing.List[ContractDesc]: + """""" + + return self.rpc.call_sync("env/contracts", ) + + def env_functions(self, arg0: EnvironmentId) -> typing.List[FunctionDesc]: + """""" + + return self.rpc.call_sync("env/functions", ) + + def env_openContract(self, arg0: ContractId) -> ProofId: + """""" + + return self.rpc.call_sync("env/openContract", ) + + def env_sorts(self, arg0: EnvironmentId) -> typing.List[SortDesc]: + """""" + + return self.rpc.call_sync("env/sorts", ) + + def examples_list(self, ) -> typing.List[ExampleDesc]: + """""" + + return self.rpc.call_sync("examples/list", ) + + def goal_actions(self, arg0: NodeTextId, arg1: int) -> typing.List[TermActionDesc]: + """""" + + return self.rpc.call_sync("goal/actions", ) + + def goal_apply_action(self, arg0: TermActionId) -> typing.List[TermActionDesc]: + """""" + + return self.rpc.call_sync("goal/apply_action", ) + + def goal_free(self, arg0: NodeTextId): + """""" + + return self.rpc.call_async("goal/free", ) + + def goal_print(self, arg0: NodeId, arg1: PrintOptions) -> NodeTextDesc: + """""" + + return self.rpc.call_sync("goal/print", ) + + def loading_load(self, arg0: LoadParams) -> typing.Union[EnvironmentId, ProofId]: + """""" + + return self.rpc.call_sync("loading/load", ) + + def loading_loadExample(self, arg0: str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadExample", ) + + def loading_loadKey(self, arg0: str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadKey", ) + + def loading_loadProblem(self, arg0: ProblemDefinition) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadProblem", ) + + def loading_loadTerm(self, arg0: str) -> ProofId: + """""" + + return self.rpc.call_sync("loading/loadTerm", ) + + def meta_available_macros(self, ) -> typing.List[ProofMacroDesc]: + """""" + + return self.rpc.call_sync("meta/available_macros", ) + + def meta_available_script_commands(self, ) -> typing.List[ProofScriptCommandDesc]: + """""" + + return self.rpc.call_sync("meta/available_script_commands", ) + + def meta_version(self, ) -> str: + """""" + + return self.rpc.call_sync("meta/version", ) + + def proofTree_children(self, arg0: ProofId, arg1: TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self.rpc.call_sync("proofTree/children", ) + + def proofTree_root(self, arg0: ProofId) -> TreeNodeDesc: + """""" + + return self.rpc.call_sync("proofTree/root", ) + + def proofTree_subtree(self, arg0: ProofId, arg1: TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self.rpc.call_sync("proofTree/subtree", ) + + def server_exit(self, ): + """""" + + return self.rpc.call_async("server/exit", ) + + def server_setTrace(self, arg0: SetTraceParams): + """""" + + return self.rpc.call_async("server/setTrace", ) + + def server_shutdown(self, ) -> bool: + """""" + + return self.rpc.call_sync("server/shutdown", ) + + +class Client(abc.ABCMeta): + @abstractmethod + def client_logTrace(self, arg0: LogTraceParams): + """""" + + pass + + @abstractmethod + def client_sayHello(self, arg0: str): + """""" + + pass + + @abstractmethod + def client_showDocument(self, arg0: ShowDocumentParams) -> ShowDocumentResult: + """""" + + pass + + @abstractmethod + def client_sm(self, arg0: ShowMessageParams): + """""" + + pass + + @abstractmethod + def client_userResponse(self, arg0: ShowMessageRequestParams) -> MessageActionItem: + """""" + + pass