File size: 1,898 Bytes
b657fcc |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 |
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):
# basic auth header check
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"]
|