|
|
from fastapi import APIRouter, Depends, HTTPException
|
|
|
from sqlalchemy.orm import Session
|
|
|
from backend.db.session import SessionLocal
|
|
|
from backend.db.models import Universe, Axiom, Theorem
|
|
|
from backend.api.auth import get_api_key
|
|
|
from backend.core.logging_config import get_logger
|
|
|
|
|
|
router = APIRouter()
|
|
|
logger = get_logger("query_routes")
|
|
|
|
|
|
def get_db():
|
|
|
db = SessionLocal()
|
|
|
try:
|
|
|
yield db
|
|
|
finally:
|
|
|
db.close()
|
|
|
|
|
|
@router.get("/query/universe_summary/{universe_id}")
|
|
|
def get_universe_summary(universe_id: int, db: Session = Depends(get_db), api_key: str = Depends(get_api_key)):
|
|
|
try:
|
|
|
universe = db.query(Universe).filter(Universe.id == universe_id).first()
|
|
|
axioms = db.query(Axiom).filter(Axiom.universe_id == universe_id).all()
|
|
|
theorems = db.query(Theorem).filter(Theorem.universe_id == universe_id).all()
|
|
|
logger.info(f"Universe summary for {universe_id} generated.")
|
|
|
return {
|
|
|
"universe": {"id": universe.id, "name": universe.name, "type": universe.universe_type},
|
|
|
"axioms": [ax.statement for ax in axioms],
|
|
|
"theorems": [th.statement for th in theorems],
|
|
|
"axiom_count": len(axioms),
|
|
|
"theorem_count": len(theorems)
|
|
|
}
|
|
|
except Exception as e:
|
|
|
logger.error(f"Query error: {e}")
|
|
|
raise HTTPException(status_code=500, detail=str(e))
|
|
|
|
|
|
@router.get("/query/axiom_usage/{axiom_id}")
|
|
|
def get_axiom_usage(axiom_id: int, db: Session = Depends(get_db), api_key: str = Depends(get_api_key)):
|
|
|
try:
|
|
|
axiom = db.query(Axiom).filter(Axiom.id == axiom_id).first()
|
|
|
theorems = db.query(Theorem).filter(Theorem.universe_id == axiom.universe_id).all()
|
|
|
used_in = [th.statement for th in theorems if axiom.statement in th.proof]
|
|
|
logger.info(f"Axiom usage for {axiom_id} generated.")
|
|
|
return {
|
|
|
"axiom": axiom.statement,
|
|
|
"used_in_theorems": used_in,
|
|
|
"usage_count": len(used_in)
|
|
|
}
|
|
|
except Exception as e:
|
|
|
logger.error(f"Query error: {e}")
|
|
|
raise HTTPException(status_code=500, detail=str(e))
|
|
|
|
