"""
example_usage.py - Test local or remote nanoGentzen pipeline
"""
import torch
from transformers import AutoModel, AutoTokenizer
from kernel import Sequent, Imp, And, Var, verify_proof_tree
from search import NeuralProofSearch

device = "cuda" if torch.cuda.is_available() else "cpu"

print("[*] Loading nanoGentzen model & tokenizer...")
model = AutoModel.from_pretrained("./hf_model", trust_remote_code=True).to(device)
tokenizer = AutoTokenizer.from_pretrained("./hf_model", trust_remote_code=True)

searcher = NeuralProofSearch(model, tokenizer, device=device)

# Modus Ponens: P, (P => Q) |- Q
P, Q = Var("P"), Var("Q")
goal = Sequent((P, Imp(P, Q)), (Q,))

print(f"[*] Proving goal: {goal.to_str()}")
proof_tree = searcher.prove(goal, max_depth=8)

if proof_tree:
    print("[✓] PROOF FOUND & VERIFIED:")
    print(f"    Sound: {verify_proof_tree(proof_tree)}")
    print(f"    Tree : {proof_tree}")
else:
    print("[✗] Proof failed or timed out.")