diff --git a/api.meta.json b/api.meta.json index 180b16a3019..953b76c6088 100644 --- a/api.meta.json +++ b/api.meta.json @@ -10,11 +10,13 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -51,19 +53,23 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "category", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "scriptCommandName", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -87,7 +93,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "SetTraceParams" } ] @@ -97,7 +103,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "ProofId" } ], @@ -112,11 +118,11 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "proof", "type": "ProofId" }, { - "name": "arg1", + "name": "nodeId", "type": "TreeNodeId" } ], @@ -134,11 +140,11 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "proof", "type": "ProofId" }, { - "name": "arg1", + "name": "nodeId", "type": "TreeNodeId" } ], @@ -156,11 +162,11 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "NodeId" }, { - "name": "arg1", + "name": "options", "type": "PrintOptions" } ], @@ -169,11 +175,13 @@ "fields": [ { "name": "id", - "type": "NodeTextId" + "type": "NodeTextId", + "documentation": "" }, { "name": "result", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -184,11 +192,11 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "NodeTextId" }, { - "name": "arg1", + "name": "pos", "type": "INT" } ], @@ -198,23 +206,28 @@ "fields": [ { "name": "commandId", - "type": "TermActionId" + "type": "TermActionId", + "documentation": "" }, { "name": "displayName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "category", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "kind", - "type": "TermActionKind" + "type": "TermActionKind", + "documentation": "" } ], "documentation": "" @@ -227,7 +240,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "TermActionId" } ], @@ -237,23 +250,28 @@ "fields": [ { "name": "commandId", - "type": "TermActionId" + "type": "TermActionId", + "documentation": "" }, { "name": "displayName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "category", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "kind", - "type": "TermActionKind" + "type": "TermActionKind", + "documentation": "" } ], "documentation": "" @@ -266,7 +284,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "NodeTextId" } ] @@ -276,7 +294,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "env", "type": "EnvironmentId" } ], @@ -286,31 +304,38 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "sort", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "retSort", - "type": "SortDesc" + "type": "SortDesc", + "documentation": "" }, { "name": "argSorts", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "rigid", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "unique", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "skolemConstant", - "type": "BOOL" + "type": "BOOL", + "documentation": "" } ], "documentation": "" @@ -323,7 +348,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "env", "type": "EnvironmentId" } ], @@ -333,23 +358,28 @@ "fields": [ { "name": "string", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "documentation", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "extendsSorts", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "anAbstract", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "s", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -362,7 +392,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "env", "type": "EnvironmentId" } ], @@ -372,27 +402,33 @@ "fields": [ { "name": "contractId", - "type": "ContractId" + "type": "ContractId", + "documentation": "" }, { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "displayName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "typeName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "htmlText", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "plainText", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -405,7 +441,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "contractId", "type": "ContractId" } ], @@ -414,11 +450,13 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -429,7 +467,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "LoadParams" } ], @@ -439,7 +477,8 @@ "fields": [ { "name": "envId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -449,11 +488,13 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -462,11 +503,11 @@ } }, { - "name": "loading/loadKey", + "name": "loading/loadExample", "documentation": "", "args": [ { - "name": "arg0", + "name": "id", "type": "STRING" } ], @@ -475,23 +516,25 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" } }, { - "name": "loading/loadExample", + "name": "loading/loadProblem", "documentation": "", "args": [ { - "name": "arg0", - "type": "STRING" + "name": "problem", + "type": "ProblemDefinition" } ], "returnType": { @@ -499,23 +542,25 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" } }, { - "name": "loading/loadProblem", + "name": "loading/loadKey", "documentation": "", "args": [ { - "name": "arg0", - "type": "ProblemDefinition" + "name": "content", + "type": "STRING" } ], "returnType": { @@ -523,11 +568,13 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -538,7 +585,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "term", "type": "STRING" } ], @@ -547,11 +594,13 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -562,7 +611,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "e", "type": "STRING" } ] @@ -572,7 +621,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "LogTraceParams" } ] @@ -582,7 +631,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "ShowMessageParams" } ] @@ -592,7 +641,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "ShowMessageRequestParams" } ], @@ -601,7 +650,8 @@ "fields": [ { "name": "title", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -612,7 +662,7 @@ "documentation": "", "args": [ { - "name": "arg0", + "name": "params", "type": "ShowDocumentParams" } ], @@ -621,7 +671,8 @@ "fields": [ { "name": "success", - "type": "BOOL" + "type": "BOOL", + "documentation": "" } ], "documentation": "" @@ -634,11 +685,13 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -653,19 +706,23 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "category", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "scriptCommandName", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -684,7 +741,8 @@ "fields": [ { "name": "value", - "type": "TraceValue" + "type": "TraceValue", + "documentation": "" } ], "documentation": "" @@ -694,7 +752,8 @@ "fields": [ { "name": "envId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -704,11 +763,13 @@ "fields": [ { "name": "env", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "proofId", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -723,7 +784,8 @@ "fields": [ { "name": "id", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -733,11 +795,13 @@ "fields": [ { "name": "proofId", - "type": "ProofId" + "type": "ProofId", + "documentation": "" }, { "name": "nodeId", - "type": "INT" + "type": "INT", + "documentation": "" } ], "documentation": "" @@ -747,23 +811,28 @@ "fields": [ { "name": "unicode", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "width", - "type": "INT" + "type": "INT", + "documentation": "" }, { "name": "indentation", - "type": "INT" + "type": "INT", + "documentation": "" }, { "name": "pure", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "termLabels", - "type": "BOOL" + "type": "BOOL", + "documentation": "" } ], "documentation": "" @@ -773,11 +842,13 @@ "fields": [ { "name": "nodeId", - "type": "NodeId" + "type": "NodeId", + "documentation": "" }, { "name": "nodeTextId", - "type": "INT" + "type": "INT", + "documentation": "" } ], "documentation": "" @@ -787,11 +858,13 @@ "fields": [ { "name": "id", - "type": "NodeTextId" + "type": "NodeTextId", + "documentation": "" }, { "name": "result", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -801,15 +874,18 @@ "fields": [ { "name": "nodeId", - "type": "NodeId" + "type": "NodeId", + "documentation": "" }, { "name": "pio", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "id", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -829,23 +905,28 @@ "fields": [ { "name": "commandId", - "type": "TermActionId" + "type": "TermActionId", + "documentation": "" }, { "name": "displayName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "description", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "category", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "kind", - "type": "TermActionKind" + "type": "TermActionKind", + "documentation": "" } ], "documentation": "" @@ -860,23 +941,28 @@ "fields": [ { "name": "string", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "documentation", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "extendsSorts", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "anAbstract", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "s", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -886,31 +972,38 @@ "fields": [ { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "sort", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "retSort", - "type": "SortDesc" + "type": "SortDesc", + "documentation": "" }, { "name": "argSorts", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "rigid", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "unique", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "skolemConstant", - "type": "BOOL" + "type": "BOOL", + "documentation": "" } ], "documentation": "" @@ -920,11 +1013,13 @@ "fields": [ { "name": "envId", - "type": "EnvironmentId" + "type": "EnvironmentId", + "documentation": "" }, { "name": "contractId", - "type": "INT" + "type": "INT", + "documentation": "" } ], "documentation": "" @@ -934,27 +1029,33 @@ "fields": [ { "name": "contractId", - "type": "ContractId" + "type": "ContractId", + "documentation": "" }, { "name": "name", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "displayName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "typeName", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "htmlText", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "plainText", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -964,23 +1065,28 @@ "fields": [ { "name": "keyFile", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "javaFile", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "classPath", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "bootClassPath", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "includes", - "type": "List" + "type": "List", + "documentation": "" } ], "documentation": "" @@ -990,23 +1096,28 @@ "fields": [ { "name": "sorts", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "functions", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "predicates", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "antecTerms", - "type": "List" + "type": "List", + "documentation": "" }, { "name": "succTerms", - "type": "List" + "type": "List", + "documentation": "" } ], "documentation": "" @@ -1016,11 +1127,13 @@ "fields": [ { "name": "messag", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "verbose", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -1042,34 +1155,34 @@ "fields": [ { "name": "type", - "type": "MessageType" + "type": "MessageType", + "documentation": "" }, { "name": "message", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" }, - { - "typeName": "MessageActionItem[]", - "fields": [], - "documentation": "" - }, { "typeName": "ShowMessageRequestParams", "fields": [ { "name": "type", - "type": "MessageType" + "type": "MessageType", + "documentation": "" }, { "name": "message", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "actions", - "type": "MessageActionItem[]" + "type": "List", + "documentation": "" } ], "documentation": "" @@ -1079,7 +1192,8 @@ "fields": [ { "name": "title", - "type": "STRING" + "type": "STRING", + "documentation": "" } ], "documentation": "" @@ -1089,11 +1203,13 @@ "fields": [ { "name": "start", - "type": "INT" + "type": "INT", + "documentation": "" }, { "name": "end", - "type": "INT" + "type": "INT", + "documentation": "" } ], "documentation": "" @@ -1103,19 +1219,23 @@ "fields": [ { "name": "uri", - "type": "STRING" + "type": "STRING", + "documentation": "" }, { "name": "external", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "takeFocus", - "type": "BOOL" + "type": "BOOL", + "documentation": "" }, { "name": "selection", - "type": "Range" + "type": "Range", + "documentation": "" } ], "documentation": "" @@ -1125,7 +1245,8 @@ "fields": [ { "name": "success", - "type": "BOOL" + "type": "BOOL", + "documentation": "" } ], "documentation": "" diff --git a/api.meta.md b/api.meta.md index f53d88619f3..f6d7a29c764 100644 --- a/api.meta.md +++ b/api.meta.md @@ -80,13 +80,6 @@ type MessageActionItem { } ``` -### Type: MessageActionItem[] -``` -type MessageActionItem[] { - -} -``` - ### Type: MessageType ``` enum MessageType { Unused, Error, Warning, Info, Log, Debug } @@ -206,7 +199,7 @@ type ShowMessageParams { ### Type: ShowMessageRequestParams ``` type ShowMessageRequestParams { - actions : MessageActionItem[] + actions : List message : STRING type : MessageType } @@ -285,63 +278,63 @@ type TreeNodeId { ### client/logTrace (`server ~~> client`) ``` -Client.client/logTrace( arg0 : LogTraceParams ) **async** +Client.client/logTrace( params : LogTraceParams ) **async** ``` ### client/sayHello (`server ~~> client`) ``` -Client.client/sayHello( arg0 : STRING ) **async** +Client.client/sayHello( e : STRING ) **async** ``` ### client/showDocument (`server -> client`) ``` -Client.client/showDocument( arg0 : ShowDocumentParams ) -> ShowDocumentResult +Client.client/showDocument( params : ShowDocumentParams ) -> ShowDocumentResult ``` ### client/sm (`server ~~> client`) ``` -Client.client/sm( arg0 : ShowMessageParams ) **async** +Client.client/sm( params : ShowMessageParams ) **async** ``` ### client/userResponse (`server -> client`) ``` -Client.client/userResponse( arg0 : ShowMessageRequestParams ) -> MessageActionItem +Client.client/userResponse( params : ShowMessageRequestParams ) -> MessageActionItem ``` ### env/contracts (`client -> server`) ``` -Server.env/contracts( arg0 : EnvironmentId ) -> ContractDesc[] +Server.env/contracts( env : EnvironmentId ) -> ContractDesc[] ``` ### env/functions (`client -> server`) ``` -Server.env/functions( arg0 : EnvironmentId ) -> FunctionDesc[] +Server.env/functions( env : EnvironmentId ) -> FunctionDesc[] ``` ### env/openContract (`client -> server`) ``` -Server.env/openContract( arg0 : ContractId ) -> ProofId +Server.env/openContract( contractId : ContractId ) -> ProofId ``` ### env/sorts (`client -> server`) ``` -Server.env/sorts( arg0 : EnvironmentId ) -> SortDesc[] +Server.env/sorts( env : EnvironmentId ) -> SortDesc[] ``` @@ -355,63 +348,63 @@ Server.examples/list( ) -> ExampleDesc[] ### goal/actions (`client -> server`) ``` -Server.goal/actions( arg0 : NodeTextId, arg1 : INT ) -> TermActionDesc[] +Server.goal/actions( id : NodeTextId, pos : INT ) -> TermActionDesc[] ``` ### goal/apply_action (`client -> server`) ``` -Server.goal/apply_action( arg0 : TermActionId ) -> TermActionDesc[] +Server.goal/apply_action( id : TermActionId ) -> TermActionDesc[] ``` ### goal/free (`client ~~> server`) ``` -Server.goal/free( arg0 : NodeTextId ) **async** +Server.goal/free( id : NodeTextId ) **async** ``` ### goal/print (`client -> server`) ``` -Server.goal/print( arg0 : NodeId, arg1 : PrintOptions ) -> NodeTextDesc +Server.goal/print( id : NodeId, options : PrintOptions ) -> NodeTextDesc ``` ### loading/load (`client -> server`) ``` -Server.loading/load( arg0 : LoadParams ) -> either +Server.loading/load( params : LoadParams ) -> either ``` ### loading/loadExample (`client -> server`) ``` -Server.loading/loadExample( arg0 : STRING ) -> ProofId +Server.loading/loadExample( id : STRING ) -> ProofId ``` ### loading/loadKey (`client -> server`) ``` -Server.loading/loadKey( arg0 : STRING ) -> ProofId +Server.loading/loadKey( content : STRING ) -> ProofId ``` ### loading/loadProblem (`client -> server`) ``` -Server.loading/loadProblem( arg0 : ProblemDefinition ) -> ProofId +Server.loading/loadProblem( problem : ProblemDefinition ) -> ProofId ``` ### loading/loadTerm (`client -> server`) ``` -Server.loading/loadTerm( arg0 : STRING ) -> ProofId +Server.loading/loadTerm( term : STRING ) -> ProofId ``` @@ -439,21 +432,21 @@ Server.meta/version( ) -> STRING ### proofTree/children (`client -> server`) ``` -Server.proofTree/children( arg0 : ProofId, arg1 : TreeNodeId ) -> TreeNodeDesc[] +Server.proofTree/children( proof : ProofId, nodeId : TreeNodeId ) -> TreeNodeDesc[] ``` ### proofTree/root (`client -> server`) ``` -Server.proofTree/root( arg0 : ProofId ) -> TreeNodeDesc +Server.proofTree/root( id : ProofId ) -> TreeNodeDesc ``` ### proofTree/subtree (`client -> server`) ``` -Server.proofTree/subtree( arg0 : ProofId, arg1 : TreeNodeId ) -> TreeNodeDesc[] +Server.proofTree/subtree( proof : ProofId, nodeId : TreeNodeId ) -> TreeNodeDesc[] ``` @@ -467,7 +460,7 @@ Server.server/exit( ) **async** ### server/setTrace (`client ~~> server`) ``` -Server.server/setTrace( arg0 : SetTraceParams ) **async** +Server.server/setTrace( params : SetTraceParams ) **async** ``` diff --git a/api.py b/api.py deleted file mode 100644 index c83050a763e..00000000000 --- a/api.py +++ /dev/null @@ -1,374 +0,0 @@ -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/keydata.py b/keydata.py new file mode 100644 index 00000000000..59511c2a7a8 --- /dev/null +++ b/keydata.py @@ -0,0 +1,493 @@ +from __future__ import annotations +import enum +import abc +import typing +from abc import abstractmethod, ABCMeta + +class ExampleDesc: + """""" + + name : str + """""" + + description : str + """""" + + def __init__(self, name, description): + self.name = name + self.description = description + +class ProofScriptCommandDesc: + """""" + + def __init__(self, ): + pass + + +class ProofMacroDesc: + """""" + + name : str + """""" + + category : str + """""" + + description : str + """""" + + scriptCommandName : str + """""" + + def __init__(self, name, category, description, scriptCommandName): + self.name = name + self.category = category + self.description = description + self.scriptCommandName = scriptCommandName + +class TraceValue(enum.Enum): + """""" + + Off = None + Message = None + All = None + +class SetTraceParams: + """""" + + value : TraceValue + """""" + + def __init__(self, value): + self.value = value + +class EnvironmentId: + """""" + + envId : str + """""" + + def __init__(self, envId): + self.envId = envId + +class ProofId: + """""" + + env : EnvironmentId + """""" + + proofId : str + """""" + + def __init__(self, env, proofId): + self.env = env + self.proofId = proofId + +class TreeNodeDesc: + """""" + + def __init__(self, ): + pass + + +class TreeNodeId: + """""" + + id : str + """""" + + def __init__(self, id): + self.id = id + +class NodeId: + """""" + + proofId : ProofId + """""" + + nodeId : int + """""" + + def __init__(self, proofId, nodeId): + self.proofId = proofId + self.nodeId = nodeId + +class PrintOptions: + """""" + + unicode : bool + """""" + + width : int + """""" + + indentation : int + """""" + + pure : bool + """""" + + termLabels : bool + """""" + + def __init__(self, unicode, width, indentation, pure, termLabels): + self.unicode = unicode + self.width = width + self.indentation = indentation + self.pure = pure + self.termLabels = termLabels + +class NodeTextId: + """""" + + nodeId : NodeId + """""" + + nodeTextId : int + """""" + + def __init__(self, nodeId, nodeTextId): + self.nodeId = nodeId + self.nodeTextId = nodeTextId + +class NodeTextDesc: + """""" + + id : NodeTextId + """""" + + result : str + """""" + + def __init__(self, id, result): + self.id = id + self.result = result + +class TermActionId: + """""" + + nodeId : NodeId + """""" + + pio : str + """""" + + id : str + """""" + + def __init__(self, nodeId, pio, id): + self.nodeId = nodeId + self.pio = pio + self.id = id + +class TermActionKind(enum.Enum): + """""" + + BuiltIn = None + Script = None + Macro = None + Taclet = None + +class TermActionDesc: + """""" + + commandId : TermActionId + """""" + + displayName : str + """""" + + description : str + """""" + + category : str + """""" + + kind : TermActionKind + """""" + + def __init__(self, commandId, displayName, description, category, kind): + self.commandId = commandId + self.displayName = displayName + self.description = description + self.category = category + self.kind = kind + +class List: + """""" + + def __init__(self, ): + pass + + +class SortDesc: + """""" + + string : str + """""" + + documentation : str + """""" + + extendsSorts : List + """""" + + anAbstract : bool + """""" + + s : str + """""" + + def __init__(self, string, documentation, extendsSorts, anAbstract, s): + self.string = string + self.documentation = documentation + self.extendsSorts = extendsSorts + self.anAbstract = anAbstract + self.s = s + +class FunctionDesc: + """""" + + name : str + """""" + + sort : str + """""" + + retSort : SortDesc + """""" + + argSorts : List + """""" + + rigid : bool + """""" + + unique : bool + """""" + + skolemConstant : bool + """""" + + def __init__(self, name, sort, retSort, argSorts, rigid, unique, skolemConstant): + self.name = name + self.sort = sort + self.retSort = retSort + self.argSorts = argSorts + self.rigid = rigid + self.unique = unique + self.skolemConstant = skolemConstant + +class ContractId: + """""" + + envId : EnvironmentId + """""" + + contractId : int + """""" + + def __init__(self, envId, contractId): + self.envId = envId + self.contractId = contractId + +class ContractDesc: + """""" + + contractId : ContractId + """""" + + name : str + """""" + + displayName : str + """""" + + typeName : str + """""" + + htmlText : str + """""" + + plainText : str + """""" + + def __init__(self, contractId, name, displayName, typeName, htmlText, plainText): + self.contractId = contractId + self.name = name + self.displayName = displayName + self.typeName = typeName + self.htmlText = htmlText + self.plainText = plainText + +class LoadParams: + """""" + + keyFile : str + """""" + + javaFile : str + """""" + + classPath : List + """""" + + bootClassPath : str + """""" + + includes : List + """""" + + def __init__(self, keyFile, javaFile, classPath, bootClassPath, includes): + self.keyFile = keyFile + self.javaFile = javaFile + self.classPath = classPath + self.bootClassPath = bootClassPath + self.includes = includes + +class ProblemDefinition: + """""" + + sorts : List + """""" + + functions : List + """""" + + predicates : List + """""" + + antecTerms : List + """""" + + succTerms : List + """""" + + def __init__(self, sorts, functions, predicates, antecTerms, succTerms): + self.sorts = sorts + self.functions = functions + self.predicates = predicates + self.antecTerms = antecTerms + self.succTerms = succTerms + +class LogTraceParams: + """""" + + messag : str + """""" + + verbose : str + """""" + + def __init__(self, messag, verbose): + self.messag = messag + self.verbose = verbose + +class MessageType(enum.Enum): + """""" + + Unused = None + Error = None + Warning = None + Info = None + Log = None + Debug = None + +class ShowMessageParams: + """""" + + type : MessageType + """""" + + message : str + """""" + + def __init__(self, type, message): + self.type = type + self.message = message + +class ShowMessageRequestParams: + """""" + + type : MessageType + """""" + + message : str + """""" + + actions : List + """""" + + def __init__(self, type, message, actions): + self.type = type + self.message = message + self.actions = actions + +class MessageActionItem: + """""" + + title : str + """""" + + def __init__(self, title): + self.title = title + +class Range: + """""" + + start : int + """""" + + end : int + """""" + + def __init__(self, start, end): + self.start = start + self.end = end + +class ShowDocumentParams: + """""" + + uri : str + """""" + + external : bool + """""" + + takeFocus : bool + """""" + + selection : Range + """""" + + def __init__(self, uri, external, takeFocus, selection): + self.uri = uri + self.external = external + self.takeFocus = takeFocus + self.selection = selection + +class ShowDocumentResult: + """""" + + success : bool + """""" + + def __init__(self, success): + self.success = success + +class TaskFinishedInfo: + """""" + + def __init__(self, ): + pass + + +class TaskStartedInfo: + """""" + + def __init__(self, ): + pass + + +KEY_DATA_CLASSES = { "ExampleDesc": ExampleDesc,"ProofScriptCommandDesc": ProofScriptCommandDesc,"ProofMacroDesc": ProofMacroDesc,"TraceValue": TraceValue,"SetTraceParams": SetTraceParams,"EnvironmentId": EnvironmentId,"ProofId": ProofId,"TreeNodeDesc": TreeNodeDesc,"TreeNodeId": TreeNodeId,"NodeId": NodeId,"PrintOptions": PrintOptions,"NodeTextId": NodeTextId,"NodeTextDesc": NodeTextDesc,"TermActionId": TermActionId,"TermActionKind": TermActionKind,"TermActionDesc": TermActionDesc,"List": List,"SortDesc": SortDesc,"FunctionDesc": FunctionDesc,"ContractId": ContractId,"ContractDesc": ContractDesc,"LoadParams": LoadParams,"ProblemDefinition": ProblemDefinition,"LogTraceParams": LogTraceParams,"MessageType": MessageType,"ShowMessageParams": ShowMessageParams,"ShowMessageRequestParams": ShowMessageRequestParams,"MessageActionItem": MessageActionItem,"Range": Range,"ShowDocumentParams": ShowDocumentParams,"ShowDocumentResult": ShowDocumentResult,"TaskFinishedInfo": TaskFinishedInfo,"TaskStartedInfo": TaskStartedInfo } + diff --git a/keyext.api.doc/src/main/java/ExtractMetaData.java b/keyext.api.doc/src/main/java/ExtractMetaData.java index 2855e390f75..1c6c904553e 100644 --- a/keyext.api.doc/src/main/java/ExtractMetaData.java +++ b/keyext.api.doc/src/main/java/ExtractMetaData.java @@ -22,6 +22,8 @@ import java.nio.file.Paths; import java.util.*; import java.util.concurrent.CompletableFuture; +import java.util.function.Function; +import java.util.function.Supplier; /** * @author Alexander Weigl @@ -43,21 +45,16 @@ public static void main(String[] args) { addClientEndpoint(method); } - try { - Files.writeString(Paths.get("api.meta.json"), getGson().toJson(keyApi)); - } catch (IOException e) { - e.printStackTrace(); - } + runGenerator("api.meta.json", (a) -> () -> getGson().toJson(a)); + runGenerator("api.meta.md", DocGen::new); + runGenerator("keydata.py", PythionGenerator.PyDataGen::new); + runGenerator("server.py", PythionGenerator.PyApiGen::new); + } + private static void runGenerator(String target, Function> api) { 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()); + var n = api.apply(keyApi); + Files.writeString(Paths.get(target), n.get()); } catch (IOException e) { e.printStackTrace(); } @@ -124,7 +121,7 @@ private static List translate(Parameter[] parameters) { } private static Metamodel.Argument translate(Parameter parameter) { - var type = getOrFindType(parameter.getType()).name(); + var type = getOrFindType(parameter.getType()).name(); return new Metamodel.Argument(parameter.getName(), type); } diff --git a/keyext.api.doc/src/main/java/Metamodel.java b/keyext.api.doc/src/main/java/Metamodel.java index 833699cfe0c..1a868f49a06 100644 --- a/keyext.api.doc/src/main/java/Metamodel.java +++ b/keyext.api.doc/src/main/java/Metamodel.java @@ -41,10 +41,13 @@ record ClientRequest(String name, String documentation, List args, Typ record ClientNotification(String name, String documentation, List args) implements Endpoint { } - record Field(String name, /*Type*/ String type) { + record Field(String name, /*Type*/ String type, String documentation) { + Field(String name, String type) { + this(name, type, ""); + } } - sealed interface Type { + public sealed interface Type { default String kind() { return getClass().getSimpleName(); } diff --git a/keyext.api.doc/src/main/java/PyGen.java b/keyext.api.doc/src/main/java/PyGen.java deleted file mode 100644 index 357c2f51e8d..00000000000 --- a/keyext.api.doc/src/main/java/PyGen.java +++ /dev/null @@ -1,136 +0,0 @@ -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.doc/src/main/java/PythionGenerator.java b/keyext.api.doc/src/main/java/PythionGenerator.java new file mode 100644 index 00000000000..a4d2018c328 --- /dev/null +++ b/keyext.api.doc/src/main/java/PythionGenerator.java @@ -0,0 +1,223 @@ +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 abstract class PythionGenerator implements Supplier { + protected final Metamodel.KeyApi metamodel; + protected PrintWriter out; + protected final StringWriter target = new StringWriter(); + + public PythionGenerator(Metamodel.KeyApi metamodel) { + this.metamodel = metamodel; + } + + @Override + public String get() { + try (var out = new PrintWriter(target)) { + this.out = out; + run(); + } + return target.toString(); + } + + protected abstract void run(); + + protected 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); + } + }; + } + + protected 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()) + "]"; + } + + if (t instanceof Metamodel.BuiltinType bt) { + return switch (bt) { + case INT -> "int"; + case LONG -> "int"; + case STRING -> "str"; + case BOOL -> "bool"; + case DOUBLE -> "float"; + }; + } + return t.name(); + } + + protected 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)); + } + + + public static class PyApiGen extends PythionGenerator { + public PyApiGen(Metamodel.KeyApi metamodel) { + super(metamodel); + } + + @Override + protected void run() { + out.format(""" + from __future__ import annotations + from .keydata import * + from .rpc import ServerBase, LspEndpoint + + import enum + import abc + import typing + from abc import abstractmethod + """); + 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))); + } + + + 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(ServerBase):%n + def __init__(self, endpoint : LspEndpoint): + super().__init__(endpoint) + + """); + 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(", ")); + + var params = "[]"; + if (!endpoint.args().isEmpty()) { + params = endpoint.args().stream() + .map(Metamodel.Argument::name) + .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._call_sync(\"%s\", %s)".formatted(endpoint.name(), params)); + } else { + out.format(" def %s(self, %s):%n", endpoint.name().replace("/", "_"), args); + out.format(" \"\"\"%s\"\"\"%n%n", endpoint.documentation()); + out.format(" return self._call_async(\"%s\", %s)".formatted(endpoint.name(), params)); + } + out.println(); + out.println(); + } + + } + + + public static class PyDataGen extends PythionGenerator { + public PyDataGen(Metamodel.KeyApi metamodel) { + super(metamodel); + } + + @Override + public String get() { + try (var out = new PrintWriter(target)) { + this.out = out; + run(); + } + return target.toString(); + } + + protected void run() { + out.format(""" + from __future__ import annotations + import enum + import abc + import typing + from abc import abstractmethod, ABCMeta + + """); + metamodel.types().forEach(this::printType); + + var names = metamodel.types().stream().map(it -> "\"%s\": %s".formatted(it.name(), it.name())) + .collect(Collectors.joining(",")); + out.format("KEY_DATA_CLASSES = { %s }%n%n", names); + } + + private void printType(Metamodel.Type type) { + if (type instanceof Metamodel.ObjectType ot) { + out.format("class %s:%n".formatted(type.name())); + out.format(" \"\"\"%s\"\"\"%n", type.documentation()); + ot.fields().forEach(it -> out.format("%n %s : %s%n \"\"\"%s\"\"\"%n" + .formatted(it.name(), asPython(it.type()), it.documentation()))); + + out.format("\n def __init__(self%s):%n".formatted( + ot.fields().stream() + .map(Metamodel.Field::name) + .collect(Collectors.joining(", ", ", ", "")) + )); + + if (ot.fields().isEmpty()) + out.format(" pass%n%n"); + + for (Metamodel.Field field : ot.fields()) { + out.format(" self.%s = %s%n", field.name(), field.name()); + } + + } 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(); + } + } +} \ No newline at end of file diff --git a/keyext.api/build.gradle b/keyext.api/build.gradle index fbbbac93898..71e79884c3d 100644 --- a/keyext.api/build.gradle +++ b/keyext.api/build.gradle @@ -27,5 +27,6 @@ dependencies { compileJava { // for GraalVM options.compilerArgs += ["-Aproject=${project.group}/${project.name}"] + options.compilerArgs += ["-parameters"] // for having parameter name in reflection } diff --git a/keyext.api/src/main/java/org/keyproject/key/api/GenericSerializer.java b/keyext.api/src/main/java/org/keyproject/key/api/GenericSerializer.java new file mode 100644 index 00000000000..b8f61b62272 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/GenericSerializer.java @@ -0,0 +1,56 @@ +package org.keyproject.key.api; + +import com.google.gson.*; + +import java.lang.reflect.Type; + +/** + * Stackoverflow post + */ +public class GenericSerializer implements JsonSerializer /*, JsonDeserializer*/ { + + private static final String CLASS_PROPERTY_NAME = "$type"; + private final Gson gson; + + public GenericSerializer() { + gson = new Gson(); + } + + public GenericSerializer(Gson gson) { + this.gson = gson; + } + + /* + @Override + public Object deserialize(JsonElement json, Type typeOfT, + JsonDeserializationContext context) throws JsonParseException { + + Class actualClass; + if (json.isJsonObject()) { + JsonObject jsonObject = json.getAsJsonObject(); + String className = jsonObject.get(CLASS_PROPERTY_NAME).getAsString(); + try { + actualClass = Class.forName(className); + } catch (ClassNotFoundException e) { + e.printStackTrace(); + throw new JsonParseException(e.getMessage()); + } + } else { + actualClass = typeOfT.getClass(); + } + + return gson.fromJson(json, actualClass); + } + */ + + @Override + public JsonElement serialize(Object src, Type typeOfSrc, + JsonSerializationContext context) { + JsonElement retValue = gson.toJsonTree(src); + if (retValue.isJsonObject()) { + retValue.getAsJsonObject().addProperty(CLASS_PROPERTY_NAME, src.getClass().getName()); + } + return retValue; + } + +} 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 7ff86ae2c09..f2a28731d3a 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 @@ -75,7 +75,8 @@ public KeyApiImpl() { @JsonRequest public CompletableFuture> examples() { return CompletableFutures.computeAsync((c) -> - ExampleChooser.listExamples(ExampleChooser.lookForExamples()).stream().map(it -> ExampleDesc.from(it)).toList()); + ExampleChooser.listExamples(ExampleChooser.lookForExamples()) + .stream().map(ExampleDesc::from).toList()); } @Override diff --git a/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java b/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java index b95ae6eebe2..26981875aef 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java @@ -26,8 +26,6 @@ public class StartServer implements Runnable { private static final Logger LOGGER = LoggerFactory.getLogger(StartServer.class); - private static KeyAdapter adapter; - //region CLI arguments @Option(names = "--std", description = "use stdout and stdin for communication") boolean stdStreams; @@ -146,7 +144,9 @@ public void run() { public static void configureJson(GsonBuilder gsonBuilder) { - adapter = new KeyAdapter(gsonBuilder); + gsonBuilder.registerTypeHierarchyAdapter(Object.class, new GenericSerializer()); + gsonBuilder.registerTypeAdapter(File.class, new KeyAdapter.FileTypeAdapter()); + } public static Launcher launch(OutputStream out, InputStream in, KeyApiImpl keyApi) { @@ -167,3 +167,4 @@ public static Launcher launch(OutputStream out, InputStream in, KeyAp return launcherBuilder.create(); } } + diff --git a/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java b/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java index 68b330491fc..c17647c9e4f 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java @@ -48,7 +48,7 @@ public JsonElement serialize(ProofMacro src, Type typeOfSrc, JsonSerializationCo } } - static class FileTypeAdapter extends TypeAdapter { + public static class FileTypeAdapter extends TypeAdapter { @Override public void write(JsonWriter out, File value) throws IOException { out.value(value.toString()); diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java index 5e5f4f1410b..49e662c6524 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java @@ -1,5 +1,7 @@ package org.keyproject.key.api.remoteclient; +import java.util.List; + public record ShowMessageRequestParams( /** * The message type. See {@link MessageType} @@ -15,6 +17,6 @@ public record ShowMessageRequestParams( * The message action items to present. * */ - MessageActionItem[] actions + List actions ) { } \ No newline at end of file diff --git a/keyext.client.python/keyapi/__init__.py b/keyext.client.python/keyapi/__init__.py index 4a913b39b2e..4807ec5ee59 100644 --- a/keyext.client.python/keyapi/__init__.py +++ b/keyext.client.python/keyapi/__init__.py @@ -1,8 +1,8 @@ -from keyapi.rpc import * +import abc +from abc import abstractmethod, ABCMeta + +from keyapi.keydata import * +from keyapi.rpc import LspEndpoint + -class KeyStub(JsonRPCHandler): - def __init__(self, input, output): - super().__init__(input, output) - def list_examples(self): - return self._send("examples/list", []) diff --git a/keyext.client.python/keyapi/keydata.py b/keyext.client.python/keyapi/keydata.py new file mode 100644 index 00000000000..dfeaf76f7c7 --- /dev/null +++ b/keyext.client.python/keyapi/keydata.py @@ -0,0 +1,533 @@ +from __future__ import annotations +import enum +import abc +import typing +from abc import abstractmethod, ABCMeta + + +class ExampleDesc: + """""" + + name: str + """""" + + description: str + """""" + + def __init__(self, name, description): + self.name = name + self.description = description + + +class ProofScriptCommandDesc: + """""" + + def __init__(self, ): + pass + + +class ProofMacroDesc: + """""" + + name: str + """""" + + category: str + """""" + + description: str + """""" + + scriptCommandName: str + """""" + + def __init__(self, name, category, description, scriptCommandName): + self.name = name + self.category = category + self.description = description + self.scriptCommandName = scriptCommandName + + +class TraceValue(enum.Enum): + """""" + + Off = None + Message = None + All = None + + +class SetTraceParams: + """""" + + value: TraceValue + """""" + + def __init__(self, value): + self.value = value + + +class EnvironmentId: + """""" + + envId: str + """""" + + def __init__(self, envId): + self.envId = envId + + +class ProofId: + """""" + + env: EnvironmentId + """""" + + proofId: str + """""" + + def __init__(self, env, proofId): + self.env = env + self.proofId = proofId + + +class TreeNodeDesc: + """""" + + def __init__(self, ): + pass + + +class TreeNodeId: + """""" + + id: str + """""" + + def __init__(self, id): + self.id = id + + +class NodeId: + """""" + + proofId: ProofId + """""" + + nodeId: int + """""" + + def __init__(self, proofId, nodeId): + self.proofId = proofId + self.nodeId = nodeId + + +class PrintOptions: + """""" + + unicode: bool + """""" + + width: int + """""" + + indentation: int + """""" + + pure: bool + """""" + + termLabels: bool + """""" + + def __init__(self, unicode, width, indentation, pure, termLabels): + self.unicode = unicode + self.width = width + self.indentation = indentation + self.pure = pure + self.termLabels = termLabels + + +class NodeTextId: + """""" + + nodeId: NodeId + """""" + + nodeTextId: int + """""" + + def __init__(self, nodeId, nodeTextId): + self.nodeId = nodeId + self.nodeTextId = nodeTextId + + +class NodeTextDesc: + """""" + + id: NodeTextId + """""" + + result: str + """""" + + def __init__(self, id, result): + self.id = id + self.result = result + + +class TermActionId: + """""" + + nodeId: NodeId + """""" + + pio: str + """""" + + id: str + """""" + + def __init__(self, nodeId, pio, id): + self.nodeId = nodeId + self.pio = pio + self.id = id + + +class TermActionKind(enum.Enum): + """""" + + BuiltIn = None + Script = None + Macro = None + Taclet = None + + +class TermActionDesc: + """""" + + commandId: TermActionId + """""" + + displayName: str + """""" + + description: str + """""" + + category: str + """""" + + kind: TermActionKind + """""" + + def __init__(self, commandId, displayName, description, category, kind): + self.commandId = commandId + self.displayName = displayName + self.description = description + self.category = category + self.kind = kind + + +class List: + """""" + + def __init__(self, ): + pass + + +class SortDesc: + """""" + + string: str + """""" + + documentation: str + """""" + + extendsSorts: List + """""" + + anAbstract: bool + """""" + + s: str + """""" + + def __init__(self, string, documentation, extendsSorts, anAbstract, s): + self.string = string + self.documentation = documentation + self.extendsSorts = extendsSorts + self.anAbstract = anAbstract + self.s = s + + +class FunctionDesc: + """""" + + name: str + """""" + + sort: str + """""" + + retSort: SortDesc + """""" + + argSorts: List + """""" + + rigid: bool + """""" + + unique: bool + """""" + + skolemConstant: bool + """""" + + def __init__(self, name, sort, retSort, argSorts, rigid, unique, skolemConstant): + self.name = name + self.sort = sort + self.retSort = retSort + self.argSorts = argSorts + self.rigid = rigid + self.unique = unique + self.skolemConstant = skolemConstant + + +class ContractId: + """""" + + envId: EnvironmentId + """""" + + contractId: int + """""" + + def __init__(self, envId, contractId): + self.envId = envId + self.contractId = contractId + + +class ContractDesc: + """""" + + contractId: ContractId + """""" + + name: str + """""" + + displayName: str + """""" + + typeName: str + """""" + + htmlText: str + """""" + + plainText: str + """""" + + def __init__(self, contractId, name, displayName, typeName, htmlText, plainText): + self.contractId = contractId + self.name = name + self.displayName = displayName + self.typeName = typeName + self.htmlText = htmlText + self.plainText = plainText + + +class LoadParams: + """""" + + keyFile: str + """""" + + javaFile: str + """""" + + classPath: List + """""" + + bootClassPath: str + """""" + + includes: List + """""" + + def __init__(self, keyFile, javaFile, classPath, bootClassPath, includes): + self.keyFile = keyFile + self.javaFile = javaFile + self.classPath = classPath + self.bootClassPath = bootClassPath + self.includes = includes + + + +class ProblemDefinition: + """""" + + sorts: List + """""" + + functions: List + """""" + + predicates: List + """""" + + antecTerms: List + """""" + + succTerms: List + """""" + + def __init__(self, sorts, functions, predicates, antecTerms, succTerms): + self.sorts = sorts + self.functions = functions + self.predicates = predicates + self.antecTerms = antecTerms + self.succTerms = succTerms + + +class LogTraceParams: + """""" + + messag: str + """""" + + verbose: str + """""" + + def __init__(self, messag, verbose): + self.messag = messag + self.verbose = verbose + + +class MessageType(enum.Enum): + """""" + + Unused = None + Error = None + Warning = None + Info = None + Log = None + Debug = None + + +class ShowMessageParams: + """""" + + type: MessageType + """""" + + message: str + """""" + + def __init__(self, type, message): + self.type = type + self.message = message + + +class ShowMessageRequestParams: + """""" + + type: MessageType + """""" + + message: str + """""" + + actions: List + """""" + + def __init__(self, type, message, actions): + self.type = type + self.message = message + self.actions = actions + + +class MessageActionItem: + """""" + + title: str + """""" + + def __init__(self, title): + self.title = title + + +class Range: + """""" + + start: int + """""" + + end: int + """""" + + def __init__(self, start, end): + self.start = start + self.end = end + + +class ShowDocumentParams: + """""" + + uri: str + """""" + + external: bool + """""" + + takeFocus: bool + """""" + + selection: Range + """""" + + def __init__(self, uri, external, takeFocus, selection): + self.uri = uri + self.external = external + self.takeFocus = takeFocus + self.selection = selection + + +class ShowDocumentResult: + """""" + + success: bool + """""" + + def __init__(self, success): + self.success = success + + +class TaskFinishedInfo: + """""" + + def __init__(self, ): + pass + + +class TaskStartedInfo: + """""" + + def __init__(self, ): + pass + + +KEY_DATA_CLASSES = {"ExampleDesc": ExampleDesc, "ProofScriptCommandDesc": ProofScriptCommandDesc, + "ProofMacroDesc": ProofMacroDesc, "TraceValue": TraceValue, "SetTraceParams": SetTraceParams, + "EnvironmentId": EnvironmentId, "ProofId": ProofId, "TreeNodeDesc": TreeNodeDesc, + "TreeNodeId": TreeNodeId, "NodeId": NodeId, "PrintOptions": PrintOptions, "NodeTextId": NodeTextId, + "NodeTextDesc": NodeTextDesc, "TermActionId": TermActionId, "TermActionKind": TermActionKind, + "TermActionDesc": TermActionDesc, "List": List, "SortDesc": SortDesc, "FunctionDesc": FunctionDesc, + "ContractId": ContractId, "ContractDesc": ContractDesc, "LoadParams": LoadParams, + "ProblemDefinition": ProblemDefinition, "LogTraceParams": LogTraceParams, + "MessageType": MessageType, "ShowMessageParams": ShowMessageParams, + "ShowMessageRequestParams": ShowMessageRequestParams, "MessageActionItem": MessageActionItem, + "Range": Range, "ShowDocumentParams": ShowDocumentParams, "ShowDocumentResult": ShowDocumentResult, + "TaskFinishedInfo": TaskFinishedInfo, "TaskStartedInfo": TaskStartedInfo} diff --git a/keyext.client.python/keyapi/rpc.py b/keyext.client.python/keyapi/rpc.py index 02ba2be474b..c112055e006 100644 --- a/keyext.client.python/keyapi/rpc.py +++ b/keyext.client.python/keyapi/rpc.py @@ -1,10 +1,11 @@ import enum import json -import sys import threading -from io import TextIOWrapper +import typing from typing import Dict +from keyapi import KEY_DATA_CLASSES + JSON_RPC_REQ_FORMAT = "Content-Length: {json_string_len}\r\n\r\n{json_string}" LEN_HEADER = "Content-Length: " TYPE_HEADER = "Content-Type: " @@ -16,16 +17,20 @@ class MyEncoder(json.JSONEncoder): """ def default(self, o): # pylint: disable=E0202 - return o.__dict__ + d = dict(o.__dict__) + d['$type'] = type(o).__name__ + return d class ResponseError(Exception): - def __init__(self, error_code, message): + def __init__(self, error_code, message, data=None): super().__init__(message) self.error_code = error_code + self.data = data class ErrorCodes(enum.Enum): + MethodNotFound = None ParseError = 1 @@ -57,27 +62,27 @@ def send_request(self, message): :param dict message: The message to send. ''' - json_string = json.dumps(message, cls=MyEncoder) + 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() + self.stdout.write(jsonrpc_req) + self.stdout.flush() - def recv_response(self): + def recv_response(self) -> object: ''' Recives a message. :return: a message ''' - with self.read_lock: + with (self.read_lock): message_size = None while True: # read header - line = self.stdout.readline() + line = self.stdin.readline() if not line: # server quit return None - line = line.decode("utf-8") + # line = line.decode("utf-8") if not line.endswith("\r\n"): raise ResponseError(ErrorCodes.ParseError, "Bad header: missing newline") # remove the "\r\n" @@ -99,12 +104,18 @@ def recv_response(self): 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) + jsonrpc_res = self.stdin.read(message_size) # .decode("utf-8") + return json.loads(jsonrpc_res, object_hook=object_decoder) + + +def object_decoder(obj): + if '$type' in obj: + return KEY_DATA_CLASSES[obj["$type"]](**obj) + return obj class LspEndpoint(threading.Thread): - def __init__(self, json_rpc_endpoint: JsonRpcEndpoint, method_callbacks=None, notify_callbacks=None, timeout=2): + def __init__(self, json_rpc_endpoint: JsonRpcEndpoint, method_callbacks=None, notify_callbacks=None, timeout=2000): super().__init__() self.json_rpc_endpoint: JsonRpcEndpoint = json_rpc_endpoint self.notify_callbacks: Dict = notify_callbacks or {} @@ -126,6 +137,7 @@ def stop(self): self.shutdown_flag = True def run(self): + rpc_id = None while not self.shutdown_flag: try: jsonrpc_message = self.json_rpc_endpoint.recv_response() @@ -175,14 +187,14 @@ def send_message(self, method_name, params, id=None): message_dict["params"] = params self.json_rpc_endpoint.send_request(message_dict) - def call_method(self, method_name, **kwargs): + def call_method(self, method_name, args): 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) + self.send_message(method_name, args, current_id) if self.shutdown_flag: return None @@ -196,5 +208,17 @@ def call_method(self, method_name, **kwargs): raise ResponseError(error.get("code"), error.get("message"), error.get("data")) return result - def send_notification(self, method_name, **kwargs): + def send_notification(self, method_name, kwargs): self.send_message(method_name, kwargs) + + +class ServerBase: + def __init__(self, endpoint: LspEndpoint): + self.endpoint = endpoint + + def _call_sync(self, method_name: str, param: typing.List[object]) -> object: + resp = self.endpoint.call_method(method_name, param) + return resp + + def _call_async(self, method_name: str, param: typing.List[object]): + self.endpoint.send_notification(method_name, param) diff --git a/keyext.client.python/keyapi/server.py b/keyext.client.python/keyapi/server.py new file mode 100644 index 00000000000..2940363e1c2 --- /dev/null +++ b/keyext.client.python/keyapi/server.py @@ -0,0 +1,161 @@ +from __future__ import annotations + +import abc +from abc import abstractmethod + +from .keydata import * +from .rpc import ServerBase, LspEndpoint + + +# noinspection PyTypeChecker +class KeyServer(ServerBase): + + def __init__(self, endpoint: LspEndpoint): + super().__init__(endpoint) + + def env_contracts(self, env: EnvironmentId) -> typing.List[ContractDesc]: + """""" + + return self._call_sync("env/contracts", [env]) + + def env_functions(self, env: EnvironmentId) -> typing.List[FunctionDesc]: + """""" + + return self._call_sync("env/functions", [env]) + + def env_openContract(self, contractId: ContractId) -> ProofId: + """""" + + return self._call_sync("env/openContract", [contractId]) + + def env_sorts(self, env: EnvironmentId) -> typing.List[SortDesc]: + """""" + + return self._call_sync("env/sorts", [env]) + + def examples_list(self, ) -> typing.List[ExampleDesc]: + """""" + + return self._call_sync("examples/list", []) + + def goal_actions(self, id: NodeTextId, pos: int) -> typing.List[TermActionDesc]: + """""" + + return self._call_sync("goal/actions", [id, pos]) + + def goal_apply_action(self, id: TermActionId) -> typing.List[TermActionDesc]: + """""" + + return self._call_sync("goal/apply_action", [id]) + + def goal_free(self, id: NodeTextId): + """""" + + return self._call_async("goal/free", [id]) + + def goal_print(self, id: NodeId, options: PrintOptions) -> NodeTextDesc: + """""" + + return self._call_sync("goal/print", [id, options]) + + def loading_load(self, params: LoadParams) -> typing.Union[EnvironmentId, ProofId]: + """""" + + return self._call_sync("loading/load", [params]) + + def loading_loadExample(self, id: str) -> ProofId: + """""" + + return self._call_sync("loading/loadExample", [id]) + + def loading_loadKey(self, content: str) -> ProofId: + """""" + + return self._call_sync("loading/loadKey", [content]) + + def loading_loadProblem(self, problem: ProblemDefinition) -> ProofId: + """""" + + return self._call_sync("loading/loadProblem", [problem]) + + def loading_loadTerm(self, term: str) -> ProofId: + """""" + + return self._call_sync("loading/loadTerm", [term]) + + def meta_available_macros(self, ) -> typing.List[ProofMacroDesc]: + """""" + + return self._call_sync("meta/available_macros", []) + + def meta_available_script_commands(self, ) -> typing.List[ProofScriptCommandDesc]: + """""" + + return self._call_sync("meta/available_script_commands", []) + + def meta_version(self, ) -> str: + """""" + + return self._call_sync("meta/version", []) + + def proofTree_children(self, proof: ProofId, nodeId: TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self._call_sync("proofTree/children", [proof, nodeId]) + + def proofTree_root(self, id: ProofId) -> TreeNodeDesc: + """""" + + return self._call_sync("proofTree/root", [id]) + + def proofTree_subtree(self, proof: ProofId, nodeId: TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self._call_sync("proofTree/subtree", [proof, nodeId]) + + def server_exit(self, ): + """""" + + return self._call_async("server/exit", []) + + def server_setTrace(self, params: SetTraceParams): + """""" + + return self._call_async("server/setTrace", [params]) + + def server_shutdown(self, ) -> bool: + """""" + + return self._call_sync("server/shutdown", []) + + +class Client(abc.ABCMeta): + @abstractmethod + def client_logTrace(self, params: LogTraceParams): + """""" + + pass + + @abstractmethod + def client_sayHello(self, e: str): + """""" + + pass + + @abstractmethod + def client_showDocument(self, params: ShowDocumentParams) -> ShowDocumentResult: + """""" + + pass + + @abstractmethod + def client_sm(self, params: ShowMessageParams): + """""" + + pass + + @abstractmethod + def client_userResponse(self, params: ShowMessageRequestParams) -> MessageActionItem: + """""" + + pass diff --git a/keyext.client.python/main.py b/keyext.client.python/main.py index a5cb45321d8..d12fadea42a 100644 --- a/keyext.client.python/main.py +++ b/keyext.client.python/main.py @@ -1,5 +1,7 @@ import socket -from keyapi import KeyStub, KeyClient +from keyapi import LspEndpoint, LoadParams +from keyapi.server import KeyServer +from keyapi.rpc import JsonRpcEndpoint if __name__ == "__main__": target = ("localhost", 5151) @@ -8,6 +10,18 @@ s.connect(target) input = s.makefile("r", newline="\r\n") output = s.makefile("w", newline="\r\n") - stub = KeyStub(input, output) - stub.client = KeyClient() - print(stub.list_examples()) + + rpc_endpoint = JsonRpcEndpoint(input, output) + endpoint = LspEndpoint(rpc_endpoint) + endpoint.start() + + key = KeyServer(endpoint) + print(key.meta_version()) + ex = key.examples_list() + print(ex) + + proofHandle = key.loading_load( + LoadParams("/home/weigl/work/key/key.ui/examples/standard_key/prop_log/contraposition.key", + None, None, None, None)) + + print(proofHandle) diff --git a/keyext.client.python/rwtest.py b/keyext.client.python/rwtest.py deleted file mode 100644 index 312532192dc..00000000000 --- a/keyext.client.python/rwtest.py +++ /dev/null @@ -1,402 +0,0 @@ -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 diff --git a/server.py b/server.py new file mode 100644 index 00000000000..7ad103297fe --- /dev/null +++ b/server.py @@ -0,0 +1,159 @@ +from __future__ import annotations +from .keydata import * +from .rpc import ServerBase + +import enum +import abc +import typing +from abc import abstractmethod +class KeyServer(ServerBase): + + def __init__(self, endpoint : LspEndpoint): + super().__init__(endpoint) + + def env_contracts(self, env : EnvironmentId) -> typing.List[ContractDesc]: + """""" + + return self._call_sync("env/contracts", [env]) + + def env_functions(self, env : EnvironmentId) -> typing.List[FunctionDesc]: + """""" + + return self._call_sync("env/functions", [env]) + + def env_openContract(self, contractId : ContractId) -> ProofId: + """""" + + return self._call_sync("env/openContract", [contractId]) + + def env_sorts(self, env : EnvironmentId) -> typing.List[SortDesc]: + """""" + + return self._call_sync("env/sorts", [env]) + + def examples_list(self, ) -> typing.List[ExampleDesc]: + """""" + + return self._call_sync("examples/list", []) + + def goal_actions(self, id : NodeTextId, pos : int) -> typing.List[TermActionDesc]: + """""" + + return self._call_sync("goal/actions", [id , pos]) + + def goal_apply_action(self, id : TermActionId) -> typing.List[TermActionDesc]: + """""" + + return self._call_sync("goal/apply_action", [id]) + + def goal_free(self, id : NodeTextId): + """""" + + return self._call_async("goal/free", [id]) + + def goal_print(self, id : NodeId, options : PrintOptions) -> NodeTextDesc: + """""" + + return self._call_sync("goal/print", [id , options]) + + def loading_load(self, params : LoadParams) -> typing.Union[EnvironmentId, ProofId]: + """""" + + return self._call_sync("loading/load", [params]) + + def loading_loadExample(self, id : str) -> ProofId: + """""" + + return self._call_sync("loading/loadExample", [id]) + + def loading_loadKey(self, content : str) -> ProofId: + """""" + + return self._call_sync("loading/loadKey", [content]) + + def loading_loadProblem(self, problem : ProblemDefinition) -> ProofId: + """""" + + return self._call_sync("loading/loadProblem", [problem]) + + def loading_loadTerm(self, term : str) -> ProofId: + """""" + + return self._call_sync("loading/loadTerm", [term]) + + def meta_available_macros(self, ) -> typing.List[ProofMacroDesc]: + """""" + + return self._call_sync("meta/available_macros", []) + + def meta_available_script_commands(self, ) -> typing.List[ProofScriptCommandDesc]: + """""" + + return self._call_sync("meta/available_script_commands", []) + + def meta_version(self, ) -> str: + """""" + + return self._call_sync("meta/version", []) + + def proofTree_children(self, proof : ProofId, nodeId : TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self._call_sync("proofTree/children", [proof , nodeId]) + + def proofTree_root(self, id : ProofId) -> TreeNodeDesc: + """""" + + return self._call_sync("proofTree/root", [id]) + + def proofTree_subtree(self, proof : ProofId, nodeId : TreeNodeId) -> typing.List[TreeNodeDesc]: + """""" + + return self._call_sync("proofTree/subtree", [proof , nodeId]) + + def server_exit(self, ): + """""" + + return self._call_async("server/exit", []) + + def server_setTrace(self, params : SetTraceParams): + """""" + + return self._call_async("server/setTrace", [params]) + + def server_shutdown(self, ) -> bool: + """""" + + return self._call_sync("server/shutdown", []) + +class Client(abc.ABCMeta): + @abstractmethod + def client_logTrace(self, params : LogTraceParams): + """""" + + pass + + @abstractmethod + def client_sayHello(self, e : str): + """""" + + pass + + @abstractmethod + def client_showDocument(self, params : ShowDocumentParams) -> ShowDocumentResult: + """""" + + pass + + @abstractmethod + def client_sm(self, params : ShowMessageParams): + """""" + + pass + + @abstractmethod + def client_userResponse(self, params : ShowMessageRequestParams) -> MessageActionItem: + """""" + + pass +