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))