@@ -1395,3 +1395,211 @@ def test_first_export_used_when_no_main(self) -> None:
13951395 assert "main" not in result .exports
13961396 exec_result = execute (result ) # no fn_name specified
13971397 assert exec_result .value == 99
1398+
1399+
1400+ # =====================================================================
1401+ # 6d: State<T> host imports
1402+ # =====================================================================
1403+
1404+ def _run_state (
1405+ source : str ,
1406+ fn : str | None = None ,
1407+ args : list [int | float ] | None = None ,
1408+ initial_state : dict [str , int | float ] | None = None ,
1409+ ) -> ExecuteResult :
1410+ """Compile, execute, and return the full ExecuteResult."""
1411+ result = _compile_ok (source )
1412+ return execute (result , fn_name = fn , args = args , initial_state = initial_state )
1413+
1414+
1415+ class TestStateEffect :
1416+
1417+ def test_state_int_get_default (self ) -> None :
1418+ """get(()) returns 0 by default for State<Int>."""
1419+ source = """\
1420+
1421+ requires(true) ensures(true) effects(<State<Int>>)
1422+ { get(()) }
1423+ """
1424+ exec_result = _run_state (source , fn = "f" )
1425+ assert exec_result .value == 0
1426+
1427+ def test_state_int_put_then_get (self ) -> None :
1428+ """put(42) then get(()) returns 42."""
1429+ source = """\
1430+
1431+ requires(true) ensures(true) effects(<State<Int>>)
1432+ {
1433+ put(42);
1434+ get(())
1435+ }
1436+ """
1437+ exec_result = _run_state (source , fn = "f" )
1438+ assert exec_result .value == 42
1439+
1440+ def test_increment_pattern (self ) -> None :
1441+ """Classic increment: get, add 1, put — state goes from 0 to 1."""
1442+ source = """\
1443+
1444+ requires(true) ensures(true) effects(<State<Int>>)
1445+ {
1446+ let @Int = get(());
1447+ put(@Int.0 + 1);
1448+ ()
1449+ }
1450+ """
1451+ exec_result = _run_state (source , fn = "increment" )
1452+ assert exec_result .value is None # Unit return
1453+ assert exec_result .state ["State_Int" ] == 1
1454+
1455+ def test_increment_example_file (self ) -> None :
1456+ """examples/increment.vera compiles and executes."""
1457+ from pathlib import Path
1458+ path = Path (__file__ ).parent .parent / "examples" / "increment.vera"
1459+ source = path .read_text ()
1460+ tree = parse_file (str (path ))
1461+ program = transform (tree )
1462+ result = compile (program , source = source , file = str (path ))
1463+ assert result .ok
1464+ assert "increment" in result .exports
1465+ exec_result = execute (result , fn_name = "increment" )
1466+ assert exec_result .state ["State_Int" ] == 1
1467+
1468+ def test_state_bool_get_default (self ) -> None :
1469+ """Bool state defaults to 0 (false)."""
1470+ source = """\
1471+
1472+ requires(true) ensures(true) effects(<State<Bool>>)
1473+ { get(()) }
1474+ """
1475+ exec_result = _run_state (source , fn = "f" )
1476+ assert exec_result .value == 0
1477+
1478+ def test_state_bool_put_get (self ) -> None :
1479+ """put(true) then get(()) returns 1."""
1480+ source = """\
1481+
1482+ requires(true) ensures(true) effects(<State<Bool>>)
1483+ {
1484+ put(true);
1485+ get(())
1486+ }
1487+ """
1488+ exec_result = _run_state (source , fn = "f" )
1489+ assert exec_result .value == 1
1490+
1491+ def test_state_float64_get_default (self ) -> None :
1492+ """Float64 state defaults to 0.0."""
1493+ source = """\
1494+
1495+ requires(true) ensures(true) effects(<State<Float64>>)
1496+ { get(()) }
1497+ """
1498+ exec_result = _run_state (source , fn = "f" )
1499+ assert exec_result .value == 0.0
1500+
1501+ def test_state_nat_compiles (self ) -> None :
1502+ """State<Nat> compiles (Nat maps to i64)."""
1503+ source = """\
1504+
1505+ requires(true) ensures(true) effects(<State<Nat>>)
1506+ { get(()) }
1507+ """
1508+ exec_result = _run_state (source , fn = "f" )
1509+ assert exec_result .value == 0
1510+
1511+ def test_state_string_rejected (self ) -> None :
1512+ """State<String> is unsupported — function skipped with warning."""
1513+ source = """\
1514+
1515+ requires(true) ensures(true) effects(<State<String>>)
1516+ { 42 }
1517+ """
1518+ result = _compile (source )
1519+ warnings = [d for d in result .diagnostics if d .severity == "warning" ]
1520+ assert any ("unsupported" in w .description .lower () for w in warnings )
1521+ assert "f" not in result .exports
1522+
1523+ def test_state_with_io (self ) -> None :
1524+ """Mixed effects(<State<Int>, IO>) compiles and both work."""
1525+ source = """\
1526+
1527+ requires(true) ensures(true) effects(<State<Int>, IO>)
1528+ {
1529+ put(42);
1530+ IO.print("done");
1531+ ()
1532+ }
1533+ """
1534+ exec_result = _run_state (source , fn = "f" )
1535+ assert exec_result .state ["State_Int" ] == 42
1536+ assert exec_result .stdout == "done"
1537+
1538+ def test_state_wat_has_imports (self ) -> None :
1539+ """WAT output contains State import declarations."""
1540+ source = """\
1541+
1542+ requires(true) ensures(true) effects(<State<Int>>)
1543+ { get(()) }
1544+ """
1545+ result = _compile_ok (source )
1546+ assert 'import "vera" "state_get_Int"' in result .wat
1547+ assert 'import "vera" "state_put_Int"' in result .wat
1548+
1549+ def test_multiple_state_types (self ) -> None :
1550+ """Multiple State types emit all imports."""
1551+ source = """\
1552+
1553+ requires(true) ensures(true) effects(<State<Int>, State<Bool>>)
1554+ {
1555+ put(@Int.0);
1556+ ()
1557+ }
1558+ """
1559+ result = _compile_ok (source )
1560+ assert 'import "vera" "state_get_Int"' in result .wat
1561+ assert 'import "vera" "state_put_Int"' in result .wat
1562+ assert 'import "vera" "state_get_Bool"' in result .wat
1563+ assert 'import "vera" "state_put_Bool"' in result .wat
1564+ assert len (result .state_types ) == 2
1565+
1566+ def test_put_void_no_drop (self ) -> None :
1567+ """put(x) in ExprStmt does not emit a drop instruction."""
1568+ source = """\
1569+
1570+ requires(true) ensures(true) effects(<State<Int>>)
1571+ {
1572+ put(42);
1573+ ()
1574+ }
1575+ """
1576+ result = _compile_ok (source )
1577+ # The function body should NOT contain 'drop' after the put call
1578+ fn_start = result .wat .index ("(func $f" )
1579+ fn_body = result .wat [fn_start :]
1580+ # put call should be present, drop should not follow it
1581+ assert "call $vera.state_put_Int" in fn_body
1582+ assert "drop" not in fn_body
1583+
1584+ def test_state_initial_value (self ) -> None :
1585+ """Initial state override: get(()) returns the initial value."""
1586+ source = """\
1587+
1588+ requires(true) ensures(true) effects(<State<Int>>)
1589+ { get(()) }
1590+ """
1591+ exec_result = _run_state (
1592+ source , fn = "f" , initial_state = {"State_Int" : 10 }
1593+ )
1594+ assert exec_result .value == 10
1595+
1596+ def test_pure_no_state_imports (self ) -> None :
1597+ """Pure functions don't produce State imports."""
1598+ source = """\
1599+
1600+ requires(true) ensures(true) effects(pure)
1601+ { 42 }
1602+ """
1603+ result = _compile_ok (source )
1604+ assert "state_get" not in result .wat
1605+ assert "state_put" not in result .wat
0 commit comments