# curl http://localhost:8000/health
# python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000

# curl -G "http://localhost:8000/recommend" \
#   --data-urlencode "prompt=$(cat prompt.txt)" \
#   --data-urlencode "top_k=3"


curl -X POST http://localhost:8000/recommend \
  -H "Content-Type: application/json" \
  -d '{
    "sequent": "{1}   FORALL (A, B: simple_polygon_2d, j: below(A`num_vertices), i: nat): LET IV = injected_vertices(A, B, A`num_vertices), s = edges_of_polygon(A)(j), L = injected_vertices(A, B, j)`length, Q = injected_edge_seq(s, injected_edge(s, B)) IN i < IV`length AND i >= L AND i < Q`length + L IMPLIES IV`seq(i) = Q`seq(i - L)",
    "prev_commands": ["None", "None", "None"],
    "top_k": 3
  }'