Skip to content

Commit 32dde34

Browse files
rcosta358rcosta358
committed
Remove Duplicate Tool Logic
1 parent 3ad0743 commit 32dde34

20 files changed

Lines changed: 228 additions & 200 deletions

‎src/main/java/liquidjava/mcp/Main.java‎

Lines changed: 15 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,7 @@
2020
import liquidjava.mcp.tools.context.ContextInspector;
2121
import liquidjava.mcp.tools.fsm.GetStateMachineTool;
2222

23-
public final class Main {
24-
private Main() {}
23+
public class Main {
2524

2625
public static void main(String[] args) {
2726
PrintStream protocolOutput = System.out;
@@ -31,20 +30,20 @@ public static void main(String[] args) {
3130
LiquidJavaVerifier verifier = new LiquidJavaVerifier();
3231
ContextInspector inspector = new ContextInspector();
3332
McpSyncServer server = McpServer.sync(transport)
34-
.serverInfo("liquidjava-mcp", "0.1.0-SNAPSHOT")
35-
.capabilities(ServerCapabilities.builder().tools(false).build())
36-
.validateToolInputs(false)
37-
.tools(
38-
new VerifyTool(verifier, mapper).specification(),
39-
new GetDiagnosticsTool(verifier, mapper).specification(),
40-
new GetLocalsTool(inspector, mapper).specification(),
41-
new GetGlobalsTool(inspector, mapper).specification(),
42-
new GetContractsTool(inspector, mapper).specification(),
43-
new CheckValidityTool(new ValidityChecker()::check, mapper).specification(),
44-
new CheckSatisfiabilityTool(new SmtChecker()::check, mapper).specification(),
45-
new GetStateMachineTool(mapper).specification()
46-
)
47-
.build();
33+
.serverInfo("liquidjava-mcp", "0.1.0-SNAPSHOT")
34+
.capabilities(ServerCapabilities.builder().tools(false).build())
35+
.validateToolInputs(false)
36+
.tools(
37+
new VerifyTool(verifier, mapper).specification(),
38+
new GetDiagnosticsTool(verifier, mapper).specification(),
39+
new GetLocalsTool(inspector, mapper).specification(),
40+
new GetGlobalsTool(inspector, mapper).specification(),
41+
new GetContractsTool(inspector, mapper).specification(),
42+
new CheckValidityTool(new ValidityChecker()::check, mapper).specification(),
43+
new CheckSatisfiabilityTool(new SmtChecker()::check, mapper).specification(),
44+
new GetStateMachineTool(mapper).specification()
45+
)
46+
.build();
4847
Runtime.getRuntime().addShutdownHook(new Thread(server::close, "mcp-shutdown"));
4948
}
5049
}

‎src/main/java/liquidjava/mcp/tools/context/AbstractContextTool.java‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
package liquidjava.mcp.tools.context;
2+
3+
import io.modelcontextprotocol.json.McpJsonMapper;
4+
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5+
import java.util.LinkedHashMap;
6+
import java.util.List;
7+
import java.util.Map;
8+
import java.util.function.Function;
9+
import liquidjava.mcp.tools.AbstractMcpTool;
10+
import liquidjava.mcp.tools.McpError;
11+
12+
abstract class AbstractContextTool<T> extends AbstractMcpTool {
13+
protected final ContextInspector inspector;
14+
15+
protected AbstractContextTool(
16+
String name,
17+
String description,
18+
ContextInspector inspector,
19+
McpJsonMapper jsonMapper
20+
) {
21+
super(name, description, jsonMapper);
22+
this.inspector = inspector;
23+
}
24+
25+
protected final CallToolResult handleContextRequest(
26+
Map<String, Object> arguments,
27+
Function<Map<String, Object>, T> parser,
28+
Function<T, ContextResult> operation,
29+
String... resultNames
30+
) {
31+
return handleRequest(arguments, parser,
32+
request -> toMcpResult(operation.apply(request), resultNames),
33+
message -> toMcpResult(ContextResult.failed(McpError.Code.INVALID_INPUT, message), resultNames)
34+
);
35+
}
36+
37+
private CallToolResult toMcpResult(ContextResult result, String... resultNames) {
38+
Map<String, Object> content = new LinkedHashMap<>();
39+
for (String resultName : resultNames)
40+
content.put(resultName, result.context().getOrDefault(resultName, List.of()));
41+
return result(content, result.error());
42+
}
43+
}

‎src/main/java/liquidjava/mcp/tools/context/ContextInspector.java‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@
77

88
public final class ContextInspector {
99
public ContextResult getLocals(ContextRequest request) {
10-
if (request.line() == null)
11-
return ContextResult.failed(McpError.Code.INVALID_INPUT, "expected path, file, line, and column");
1210
return inspect(request.path(), () -> ContextMapper.locals(request));
1311
}
1412

‎src/main/java/liquidjava/mcp/tools/context/ContractRequest.java‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,6 @@
66
public record ContractRequest(String path, String className, String signature) {
77
public ContractRequest {
88
path = PathUtils.requireExisting(path).toString();
9-
if (className != null && className.isBlank())
10-
throw new IllegalArgumentException("className must be a nonblank string");
11-
if (signature != null && signature.isBlank())
12-
throw new IllegalArgumentException("signature must be a nonblank string");
139
}
1410

1511
public static ContractRequest fromArguments(Map<String, Object> arguments) {

‎src/main/java/liquidjava/mcp/tools/context/GetContractsTool.java‎

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -2,39 +2,29 @@
22

33
import io.modelcontextprotocol.json.McpJsonMapper;
44
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5-
import java.util.LinkedHashMap;
6-
import java.util.List;
75
import java.util.Map;
8-
import liquidjava.mcp.tools.AbstractMcpTool;
9-
import liquidjava.mcp.tools.McpError;
106

117
/**
128
* Exposes registered LiquidJava method and constructor contracts.
139
*/
14-
public final class GetContractsTool extends AbstractMcpTool {
15-
private final ContextInspector inspector;
10+
public final class GetContractsTool extends AbstractContextTool<ContractRequest> {
1611

1712
public GetContractsTool(ContextInspector inspector, McpJsonMapper jsonMapper) {
1813
super("get_contracts", """
1914
Returns contracts for methods and constructors.
2015
Each contract includes fully qualified signature, parameter names, types and refinements, return type and refinement, state transitions, and declaration location.
2116
Optional `className` and `signature` filters use exact matches and can be combined.
2217
The `signature` must be fully qualified, e.g. `com.example.MyClass.myMethod(int, java.lang.String)`.
23-
""", jsonMapper);
24-
this.inspector = inspector;
18+
""", inspector, jsonMapper);
2519
}
2620

2721
@Override
2822
public CallToolResult call(Map<String, Object> arguments) {
29-
return handleRequest(arguments, ContractRequest::fromArguments,
30-
request -> toMcpResult(inspector.getContracts(request)),
31-
message -> toMcpResult(ContextResult.failed(McpError.Code.INVALID_INPUT, message))
23+
return handleContextRequest(
24+
arguments,
25+
ContractRequest::fromArguments,
26+
inspector::getContracts,
27+
"contracts"
3228
);
3329
}
34-
35-
private CallToolResult toMcpResult(ContextResult result) {
36-
Map<String, Object> content = new LinkedHashMap<>();
37-
content.put("contracts", result.context().getOrDefault("contracts", List.of()));
38-
return result(content, result.error());
39-
}
4030
}

‎src/main/java/liquidjava/mcp/tools/context/GetGlobalsTool.java‎

Lines changed: 7 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2,38 +2,26 @@
22

33
import io.modelcontextprotocol.json.McpJsonMapper;
44
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5-
import java.util.LinkedHashMap;
6-
import java.util.List;
75
import java.util.Map;
8-
import liquidjava.mcp.tools.AbstractMcpTool;
9-
import liquidjava.mcp.tools.McpError;
106

117
/**
128
* Exposes aliases, ghost functions, and typestate definitions.
139
*/
14-
public final class GetGlobalsTool extends AbstractMcpTool {
15-
private final ContextInspector inspector;
10+
public final class GetGlobalsTool extends AbstractContextTool<ContextRequest> {
1611

1712
public GetGlobalsTool(ContextInspector inspector, McpJsonMapper jsonMapper) {
1813
super("get_globals", """
1914
Runs LiquidJava on a path and returns available aliases, ghosts, and states, optionally filtering ghosts and states by file.
20-
""", jsonMapper);
21-
this.inspector = inspector;
15+
""", inspector, jsonMapper);
2216
}
2317

2418
@Override
2519
public CallToolResult call(Map<String, Object> arguments) {
26-
return handleRequest(arguments, ContextRequest::fromGlobalArguments,
27-
request -> toMcpResult(inspector.getGlobals(request)),
28-
message -> toMcpResult(ContextResult.failed(McpError.Code.INVALID_INPUT, message))
20+
return handleContextRequest(
21+
arguments,
22+
ContextRequest::fromGlobalArguments,
23+
inspector::getGlobals,
24+
"aliases", "ghosts", "states"
2925
);
3026
}
31-
32-
private CallToolResult toMcpResult(ContextResult result) {
33-
Map<String, Object> content = new LinkedHashMap<>();
34-
content.put("aliases", result.context().getOrDefault("aliases", List.of()));
35-
content.put("ghosts", result.context().getOrDefault("ghosts", List.of()));
36-
content.put("states", result.context().getOrDefault("states", List.of()));
37-
return result(content, result.error());
38-
}
3927
}

‎src/main/java/liquidjava/mcp/tools/context/GetLocalsTool.java‎

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -2,37 +2,27 @@
22

33
import io.modelcontextprotocol.json.McpJsonMapper;
44
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5-
import java.util.LinkedHashMap;
6-
import java.util.List;
75
import java.util.Map;
8-
import liquidjava.mcp.tools.AbstractMcpTool;
9-
import liquidjava.mcp.tools.McpError;
106

117
/**
128
* Exposes refined variables visible at a source position.
139
*/
14-
public final class GetLocalsTool extends AbstractMcpTool {
15-
private final ContextInspector inspector;
10+
public final class GetLocalsTool extends AbstractContextTool<ContextRequest> {
1611

1712
public GetLocalsTool(ContextInspector inspector, McpJsonMapper jsonMapper) {
1813
super("get_locals", """
1914
Runs LiquidJava on a path and returns variables and their refinements filtered by source file, scope, and position.
2015
Locations use one-based lines and columns with inclusive ends.
21-
""", jsonMapper);
22-
this.inspector = inspector;
16+
""", inspector, jsonMapper);
2317
}
2418

2519
@Override
2620
public CallToolResult call(Map<String, Object> arguments) {
27-
return handleRequest(arguments, ContextRequest::fromPositionArguments,
28-
request -> toMcpResult(inspector.getLocals(request)),
29-
message -> toMcpResult(ContextResult.failed(McpError.Code.INVALID_INPUT, message))
21+
return handleContextRequest(
22+
arguments,
23+
ContextRequest::fromPositionArguments,
24+
inspector::getLocals,
25+
"variables"
3026
);
3127
}
32-
33-
private CallToolResult toMcpResult(ContextResult result) {
34-
Map<String, Object> content = new LinkedHashMap<>();
35-
content.put("variables", result.context().getOrDefault("variables", List.of()));
36-
return result(content, result.error());
37-
}
3828
}

‎src/main/java/liquidjava/mcp/tools/context/Range.java‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,12 @@ static Range from(SourcePosition position) {
1010

1111
static Range parse(String scope) {
1212
String[] parts = Regex.RANGE_SEPARATOR.split(scope);
13-
return new Range(Integer.parseInt(parts[0]), Integer.parseInt(parts[1]),
14-
Integer.parseInt(parts[2]), Integer.parseInt(parts[3]));
13+
return new Range(
14+
Integer.parseInt(parts[0]),
15+
Integer.parseInt(parts[1]),
16+
Integer.parseInt(parts[2]),
17+
Integer.parseInt(parts[3])
18+
);
1519
}
1620

1721
static boolean before(int line, int column, int otherLine, int otherColumn) {
@@ -24,6 +28,6 @@ boolean startsBefore(Range other) {
2428

2529
boolean contains(Range other) {
2630
return !before(other.startLine, other.startColumn, startLine, startColumn)
27-
&& !before(endLine, endColumn, other.endLine, other.endColumn);
31+
&& !before(endLine, endColumn, other.endLine, other.endColumn);
2832
}
2933
}

‎src/main/java/liquidjava/mcp/tools/smt/AbstractSmtTool.java‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
package liquidjava.mcp.tools.smt;
2+
3+
import io.modelcontextprotocol.json.McpJsonMapper;
4+
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5+
import java.util.LinkedHashMap;
6+
import java.util.Map;
7+
import java.util.function.Function;
8+
import liquidjava.mcp.tools.AbstractMcpTool;
9+
10+
abstract class AbstractSmtTool<T, R extends SolverResult<?>> extends AbstractMcpTool {
11+
private final Function<T, R> checker;
12+
private final Function<String, R> invalidInput;
13+
14+
protected AbstractSmtTool(
15+
String name,
16+
String description,
17+
Function<T, R> checker,
18+
Function<String, R> invalidInput,
19+
McpJsonMapper jsonMapper
20+
) {
21+
super(name, description, jsonMapper);
22+
this.checker = checker;
23+
this.invalidInput = invalidInput;
24+
}
25+
26+
protected final CallToolResult handleSmtRequest(
27+
Map<String, Object> arguments,
28+
Function<Map<String, Object>, T> parser,
29+
String resultName
30+
) {
31+
return handleRequest(arguments, parser,
32+
request -> solverResult(checker.apply(request), resultName),
33+
message -> solverResult(invalidInput.apply(message), resultName)
34+
);
35+
}
36+
37+
private CallToolResult solverResult(R result, String resultName) {
38+
Map<String, Object> content = new LinkedHashMap<>();
39+
if (result.status() != null) content.put("status", result.statusValue());
40+
if (result.assignments() != null) content.put(resultName, result.assignments());
41+
return result(content, result.error());
42+
}
43+
}

‎src/main/java/liquidjava/mcp/tools/smt/CheckSatisfiabilityTool.java‎

Lines changed: 3 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,12 @@
22

33
import io.modelcontextprotocol.json.McpJsonMapper;
44
import io.modelcontextprotocol.spec.McpSchema.CallToolResult;
5-
import java.util.LinkedHashMap;
65
import java.util.Map;
76
import java.util.function.Function;
8-
import liquidjava.mcp.tools.AbstractMcpTool;
97
import liquidjava.mcp.tools.McpError;
108

119
/** Checks whether a set of refinement predicates has a satisfying assignment. */
12-
public final class CheckSatisfiabilityTool extends AbstractMcpTool {
13-
private final Function<SmtRequest, SmtResult> checker;
10+
public final class CheckSatisfiabilityTool extends AbstractSmtTool<SmtRequest, SmtResult> {
1411

1512
public CheckSatisfiabilityTool(Function<SmtRequest, SmtResult> checker, McpJsonMapper jsonMapper) {
1613
super("check_satisfiability", """
@@ -21,21 +18,10 @@ public CheckSatisfiabilityTool(Function<SmtRequest, SmtResult> checker, McpJsonM
2118
Uses LiquidJava's solver semantics and returns sat, unsat, or unknown.
2219
Sat results include a satisfying assignment when the solver provides one.
2320
Does not support aliases, source constants, or implicit receiver/return/old-state bindings.
24-
""", jsonMapper);
25-
this.checker = checker;
21+
""", checker, message -> SmtResult.failed(McpError.Code.INVALID_INPUT, message), jsonMapper);
2622
}
2723

2824
public CallToolResult call(Map<String, Object> arguments) {
29-
return handleRequest(arguments, SmtRequest::fromArguments,
30-
request -> toMcpResult(checker.apply(request)),
31-
message -> toMcpResult(SmtResult.failed(McpError.Code.INVALID_INPUT, message))
32-
);
33-
}
34-
35-
private CallToolResult toMcpResult(SmtResult result) {
36-
Map<String, Object> content = new LinkedHashMap<>();
37-
if (result.status() != null) content.put("status", result.status().value());
38-
if (result.assignment() != null) content.put("assignment", result.assignment());
39-
return result(content, result.error());
25+
return handleSmtRequest(arguments, SmtRequest::fromArguments, "assignment");
4026
}
4127
}

0 commit comments

Comments
 (0)