Name: Python代码转译工具
Author: py2many

使用说明

mcp-server-py2many

一个模型上下文协议（MCP）服务器，提供将Python代码转换为多种编程语言的工具，使用 py2many.

概述

此MCP服务器公开了允许LLM将Python代码转换为各种目标语言的工具，包括C++、Rust、Go、Kotlin、Dart、Julia、Nim、V、Mojo、D、SMT和Zig。

安装

使用紫外线（推荐）

# Clone the repository
git clone <repository-url>
cd mcp-server-py2many

# Install dependencies
uv sync

# Run the server
uv run mcp-server-py2many

使用pip

pip install mcp-server-py2many

配置

将此服务器添加到MCP客户端配置中：

Claude桌面配置

添加到您的 claude_desktop_config.json:

{
  "mcpServers": {
    "py2many": {
      "command": "uvx",
      "args": ["mcp-server-py2many"]
    }
  }
}

或者使用本地安装：

{
  "mcpServers": {
    "py2many": {
      "command": "uv",
      "args": ["run", "--directory", "/path/to/mcp-server-py2many", "mcp-server-py2many"]
    }
  }
}

可用工具

1. `transpile_python`

使用基于确定性规则的翻译将Python代码转换为另一种编程语言。

参数：

python_code （string，必填）：要转换的Python代码
target_language （字符串，必填）：目标语言（cpp、rust、go、kotlin、dart、julia、nim、vlang、mojo、dlang、smt、zig）

2. `transpile_python_with_llm`

在LLM的帮助下，使用py2many转换Python代码，以更好地处理复杂的习惯用法。

参数：

python_code （string，必填）：要转换的Python代码
target_language （字符串，必填）：目标语言（cpp、rust、go、kotlin、dart、julia、nim、vlang、mojo、dlang、smt、zig）

3. `list_supported_languages`

列出所有支持转译的目标语言。

4. `verify_python`

使用SMT和z3求解器验证Python代码。此工具使用 --smt 然后通过z3进行验证，以检查前/后条件的逆是否不饱和。

参数：

python_code （string，必填）：要验证的Python代码

它是如何工作的：

使用以下命令将Python代码转换为SMT-LIB格式 py2many --smt
从生成的SMT中提取先决条件（函数以结尾 -pre)
构造一个验证查询，检查是否存在反例，其中：
- 前提条件成立（有效输入）
- 实现与规范不同
在验证查询上运行z3
如果发现错误/反例，则返回SAT，如果验证，则返回UNSAT

示例：三角形分类错误检测

此示例使用 triangle_buggy.py py2many的测试用例，用于检测三角形分类实现中的错误：

from adt import adt as sealed

from py2many.smt import check_sat, default_value, get_model
from py2many.smt import pre as smt_pre


@sealed
class TriangleType:
    EQUILATERAL: int
    ISOSCELES: int
    RIGHT: int
    ACUTE: int
    OBTUSE: int
    ILLEGAL: int


a: int = default_value(int)
b: int = default_value(int)
c: int = default_value(int)


def classify_triangle_correct(a: int, b: int, c: int) -> TriangleType:
    """Correct implementation that properly sorts sides before classification"""
    if a == b and b == c:
        return TriangleType.EQUILATERAL
    elif a == b or b == c or a == c:
        return TriangleType.ISOSCELES
    else:
        if a >= b and a >= c:
            if a * a == b * b + c * c:
                return TriangleType.RIGHT
            elif a * a < b * b + c * c:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE
        elif b >= a and b >= c:
            if b * b == a * a + c * c:
                return TriangleType.RIGHT
            elif b * b < a * a + c * c:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE
        else:
            if c * c == a * a + b * b:
                return TriangleType.RIGHT
            elif c * c < a * a + b * b:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE


def classify_triangle(a: int, b: int, c: int) -> TriangleType:
    """Buggy implementation - assumes a >= b >= c without sorting"""
    # Pre-condition: all sides must be positive and satisfy triangle inequality
    if smt_pre:
        assert a > 0
        assert b > 0
        assert c > 0
        assert a < (b + c)

    if a >= b and b >= c:
        if a == c or b == c:
            if a == b and a == c:
                return TriangleType.EQUILATERAL
            else:
                return TriangleType.ISOSCELES
        else:
            # BUG: Not sorting sides, assuming a is largest
            if a * a != b * b + c * c:
                if a * a < b * b + c * c:
                    return TriangleType.ACUTE
                else:
                    return TriangleType.OBTUSE
            else:
                return TriangleType.RIGHT
    else:
        return TriangleType.ILLEGAL


# Assert that the buggy version differs from correct version
assert not classify_triangle_correct(a, b, c) == classify_triangle(a, b, c)
check_sat()
get_model()

验证结果：

=== z3 verification result ===
sat
(
  (define-fun a () Int
    1)
  (define-fun c () Int
    2)
  (define-fun b () Int
    2)
)

=== VERIFICATION FAILED ===
SAT means a counterexample was found where the implementation differs from the spec.

反例发现： a=1, b=2, c=2 -这满足了前提条件（全部为正，a<b+c），但有缺陷的实现返回非法，而正确的实现返回ISOSCELES。

使用案例：

通过与参考实现进行比较来检测实现中的错误
验证功能是否符合其规格
前/后条件的正式验证
寻找错误算法的反例

何时使用确定性翻译与法学硕士辅助翻译

使用确定性翻译 (`transpile_python`)何时：

✅ 简单、地道的Python代码

基本控制流（if/else、for/while循环）
具有直接等效项的标准库函数
数据结构（列表、字典、集合）
简单的函数和类

✅ 经过充分测试的模式

数学计算
字符串操作
文件I/O操作
算法实现

✅ 当再现性很重要时

相同的输入总是产生相同的输出
没有外部依赖项或API调用
明确、确定的行为

确定性示例案例：

# Simple functions
def factorial(n):
    if n <= 1:
        return 1
    return n * factorial(n - 1)

# Data processing
def sum_even_numbers(numbers):
    return sum(n for n in numbers if n % 2 == 0)

# Basic algorithms
def binary_search(arr, target):
    left, right = 0, len(arr) - 1
    while left <= right:
        mid = (left + right) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

使用 LLM辅助翻译 (`transpile_python_with_llm`)何时：

🧠 复杂的Python习惯用法

装饰器和元类
包含多个子句的复杂理解
生成器表达式和协程
动态打字模式

🧠 特定语言的功能需要翻译

Python专用库（numpy、pandas模式）
鸭子类型和协议实现
Monkey补丁和运行时修改
具有复杂行为的上下文管理器

🧠 确定性翻译失败或产生非惯用代码

需要语义理解的类型错误
目标语言中的非惯用输出
缺少导入或依赖项
复杂的继承模式

🧠 目标语言的最佳实践存在显著差异

Rust所有权和借用模式
C++内存管理
采用并发模式
目标语言函数式编程

LLM辅助的示例案例：

# Complex decorators
def memoize(func):
    cache = {}
    def wrapper(*args):
        if args not in cache:
            cache[args] = func(*args)
        return cache[args]
    return wrapper

# Complex data transformations
def process_data(data):
    return [
        {
            'name': item['name'].upper(),
            'values': [x * 2 for x in item['values'] if x > 0]
        }
        for item in data
        if item.get('active') and len(item.get('values', [])) > 5
    ]

# Dynamic behavior
class DynamicClass:
    def __getattr__(self, name):
        return lambda *args: f"Called {name} with {args}"

决策流程图

Is your Python code...
│
├─ Simple functions/algorithms?
│  └─ Yes → Use deterministic ✓
│
├─ Standard data structures and control flow?
│  └─ Yes → Use deterministic ✓
│
├─ Complex decorators, metaclasses, dynamic behavior?
│  └─ Yes → Use LLM-assisted 🧠
│
├─ Heavy use of Python-specific idioms?
│  └─ Yes → Use LLM-assisted 🧠
│
├─ Did deterministic translation fail?
│  └─ Yes → Try LLM-assisted 🧠
│
└─ Need idiomatic target language output?
   └─ Yes → Use LLM-assisted 🧠

支持的语言

语言	代码	注释
C `cpp`	完全支持STL容器
生锈	`rust`	所有权意识翻译
去吧	`go`	成语Go代码生成
Kotlin	`kotlin`	JVM兼容输出
飞镖	`dart`	颤振友好
朱莉娅	`julia`	科学计算重点
尼姆	`nim`	系统编程
五、 `vlang`	简单、快速的编译
Mojo	`mojo`	AI/ML性能计算
D `dlang`	系统编程
齐格	`zig`	现代系统编程

与SMT签订合同设计

py2many支持SMT（满意模理论） 契约式设计 编程——编写可以使用Z3或其他SMT求解器进行形式验证的规范。与其他目标语言不同，SMT输出不是一种直接的终端用户编程语言，而是一种用于验证的规范语言。

关键概念：

前置条件：函数执行前必须满足的约束
岗位条件：函数执行后必须保持的约束
细化类型：具有附加约束的类型（例如。， int 哪里 1 < x < 1000)

示例：带约束的数学方程

带先决条件的Python源代码：

from py2many.smt import check_sat, default_value, get_value
from py2many.smt import pre as smt_pre

x: int = default_value(int)
y: int = default_value(int)
z: float = default_value(float)


def equation(x: int, y: int) -> bool:
    if smt_pre:
        assert x > 2        # pre-condition
        assert y < 10       # pre-condition
        assert x + 2 * y == 7  # constraint equation
    True


def fequation(z: float) -> bool:
    if smt_pre:
        assert 9.8 + 2 * z == z + 9.11
    True


assert equation(x, y)
assert fequation(z)
check_sat()
get_value((x, y, z))

生成的SMT-LIB 2.0输出：

(declare-const x Int)
(declare-const y Int)
(declare-const z Real)

(define-fun equation-pre ((x Int) (y Int)) Bool
  (and
    (> x 2)
    (< y 10)
    (= (+ x (* 2 y)) 7)))

(define-fun equation ((x Int) (y Int))  Bool
  true)

(assert (and
          (equation-pre  x y)
          (equation x y)))

(check-sat)
(get-value (x y z))

跑步时 z3 -smt2 equations.smt，求解器证明约束是可满足的，并返回值： x = 7, y = 0, z = -0.69.

使用案例：

静态验证：部署前证明正确性
细化类型：对整数强制范围约束（例如。， UserId 必须 0 < id < 1000)
协议验证：确保状态机遵循有效的转换
安全属性：验证输入消毒前提条件

进一步阅读：

PySMT：Python中的契约式设计 -py2many如何实现细化类型和形式验证
代理转发器 -带验证的多级转译架构
方程式.py来源 -Python测试用例
方程式.smt输出 -生成的SMT-LIB

示例

示例1：简单函数（确定性）

# Python input
def greet(name):
    return f"Hello, {name}!"

# C++ output (via transpile_python)
#include <iostream>
#include <string>

std::string greet(std::string name) {
    return "Hello, " + name + "!";
}

示例2：复杂数据处理（LLM辅助）

# Python input with complex comprehensions
def analyze_sales(data):
    return {
        region: {
            'total': sum(s['amount'] for s in sales),
            'count': len(sales),
            'avg': sum(s['amount'] for s in sales) / len(sales)
        }
        for region, sales in data.items()
        if any(s['amount'] > 1000 for s in sales)
    }

# Better results with LLM-assisted translation for idiomatic target language

发展

# Install development dependencies
uv sync

# Run the server
uv run mcp-server-py2many

# Test the server manually
uv run python -m mcp_server_py2many

运作原理

MCP服务器接收包含Python代码和目标语言的请求
使用代码创建一个临时Python文件
跑 py2many --{language} （或与 --llm 标志）在文件上
捕获生成的输出和任何错误
将转换后的代码返回给LLM客户端

局限性

并非所有目标语言都支持所有Python功能
一些Python标准库函数可能没有直接的等价物
复杂的动态Python代码在转译后可能需要手动调整
LLM辅助模式需要为py2many配置LLM API密钥

许可证

MIT许可证-有关详细信息，请参阅许可证文件。

贡献

欢迎投稿！请在存储库中打开问题并拉取请求。

使用说明

mcp-server-py2many

概述

安装

使用紫外线（推荐）

使用pip

配置

Claude桌面配置

可用工具

1. transpile_python

2. transpile_python_with_llm

3. list_supported_languages

4. verify_python

何时使用确定性翻译与法学硕士辅助翻译

使用 确定性翻译 (transpile_python)何时：

使用 LLM辅助翻译 (transpile_python_with_llm)何时：

决策流程图

支持的语言

与SMT签订合同设计

示例

示例1：简单函数（确定性）

示例2：复杂数据处理（LLM辅助）

发展

运作原理

局限性

许可证

贡献

相关项目

相关 MCP

PowerPoint操作服务器

代码索引分析工具

YouTube字幕提取服务

EPICS PV管理服务器

代码运行服务

代码分析服务器

1. `transpile_python`

2. `transpile_python_with_llm`

3. `list_supported_languages`

4. `verify_python`

使用确定性翻译 (`transpile_python`)何时：

使用 LLM辅助翻译 (`transpile_python_with_llm`)何时：