| 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"]
|
|
|
