
trusted := "tools/email/trusted"
prove := "uv run clauz3 prove --trusted-root " + trusted
# Proves each case in one process: *_pass.py must prove, *_fail.py must not.
prove-cases := "uv run python -m clauz3._prove_cases --trusted-root " + trusted
policy-check := "uv run clauz3 policy-check --policy approval-policy.json --trusted-root " + trusted + " --import-root ."

test: lint cases policy

lint:
    uv run clauz3 lint {{trusted}}/effects.py

# alias_import_fail.py:
#   Issue #129: the guarantee is spelled through an import alias. Before the fix
#   the decorator was dropped and this printed "proved!".
cases: while-loop-skip aug-assign-fail aug-assign-rewritten-fail
    {{prove-cases}} cases/*_pass.py cases/*_fail.py

policy: policy-auto-pass policy-auto-reject policy-ask

policy-auto-pass:
    {{policy-check}} --expect auto_approved cases/only_bob_pass.py

policy-auto-reject:
    {{policy-check}} --expect auto_rejected cases/policy_reject.py

policy-ask:
    {{policy-check}} --expect ask cases/policy_ask.py

case1:
    {{prove}} cases/only_bob_pass.py

case1-fail:
    if {{prove}} cases/only_bob_fail.py; then exit 1; fi

# Distinguish unsupported syntax from a refuted guarantee.
while-loop-skip:
    out=$({{prove}} cases/while_loop_skip.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: skipped unsupported program body"

# `+=` on a str is proved like its desugaring: a refuted guarantee, not a skip.
aug-assign-fail:
    out=$({{prove}} cases/aug_assign_fail.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: failed guarantee"

aug-assign-rewritten-fail:
    out=$({{prove}} cases/aug_assign_rewritten_fail.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: failed guarantee"
