|
|
from pydantic import BaseModel
|
|
|
from .universe import UniverseManager
|
|
|
|
|
|
|
|
|
class AxiomsRequest(BaseModel):
|
|
|
axioms: list[str]
|
|
|
|
|
|
|
|
|
class ProveRequest(BaseModel):
|
|
|
theorem: str
|
|
|
universe_id: str
|
|
|
|
|
|
|
|
|
class PipelineRequest(BaseModel):
|
|
|
axioms: list[str]
|
|
|
theorem: str
|
|
|
|
|
|
|
|
|
def create_app():
|
|
|
"""Create and return the FastAPI app. This is lazy to avoid import-time
|
|
|
collisions with a repo-local `fastapi/` directory when running tests in
|
|
|
this workspace.
|
|
|
"""
|
|
|
from fastapi import FastAPI, HTTPException
|
|
|
from .auth import require_token
|
|
|
from .pipeline import Pipeline
|
|
|
|
|
|
app = FastAPI(title="AlphaGeometry Demo API")
|
|
|
manager = UniverseManager()
|
|
|
pipeline = Pipeline(manager)
|
|
|
|
|
|
@app.post("/generateUniverse")
|
|
|
def generate_universe(req: AxiomsRequest):
|
|
|
uid = manager.create_universe(req.axioms)
|
|
|
return {"universe_id": uid}
|
|
|
|
|
|
@app.post("/prove")
|
|
|
def prove(req: ProveRequest):
|
|
|
try:
|
|
|
result = manager.prove(req.universe_id, req.theorem)
|
|
|
except KeyError:
|
|
|
raise HTTPException(status_code=404, detail="Universe not found")
|
|
|
return {"result": result}
|
|
|
|
|
|
@app.post("/pipeline/generate_and_prove")
|
|
|
def pipeline_generate_and_prove(req: PipelineRequest, x_api_key: str | None = None):
|
|
|
|
|
|
require_token(x_api_key)
|
|
|
res = pipeline.run_generate_and_prove(req.axioms, req.theorem)
|
|
|
return res
|
|
|
|
|
|
@app.get("/compare/{a}/{b}")
|
|
|
def compare(a: str, b: str):
|
|
|
try:
|
|
|
score = manager.compare_universes(a, b)
|
|
|
except KeyError:
|
|
|
raise HTTPException(status_code=404, detail="Universe not found")
|
|
|
return {"similarity": score}
|
|
|
|
|
|
@app.get("/health")
|
|
|
def health():
|
|
|
return {"status": "ok"}
|
|
|
|
|
|
return app
|
|
|
|
|
|
|
|
|
__all__ = ["create_app"]
|
|
|
|
