curry.backends.py.eval.rts_constraints module

Implements RuntimeState methods related to constraints. This module is not intended to be imported except by rts.py.

curry.backends.py.eval.rts_constraints.constrain_equal(rts, arg0, arg1, constraint_type=STRICT_CONSTRAINT, config=None, guards=None)

Constrain the given arguments to be equal in the specified context. This implements the equational constraints (=:=) and (=:<=). For strict constraints, both arguments must be choices or both free variables, and, in the latter case, the free variables must represent values of the same type (as is guaranteed by the type system). For non-strict constraints, the first argument must be a free variable, and the second is any expression. This implements the “binding” part of (=:<=). When the left-hand side is not a variable, ordinary pull-tabbing computations will proceed until the term is evaluated or this function is called.

Recursive constraints arise from interleaving the rules of (=:=) or (=:<=) with narrowing steps. Suppose x =:= y is first evaluated, then x and y are subsequently narrowed to (x0:x1) and (y0:y1), resp. The recursive constraints over subvariables, x0 =:= y0 and x1 =:= y1, must then be evaluated. The timing of this differs slightly for the two constraint types. With strict constraints, the subvariables are immediately equated. For non-strict constraints this that would give incorrect semantics. Instead, this function creates a binding. When (and if) the binding is later applied, the recursive non-strict constraints between subvariables are evaluated.

Parameters:

• arg0 –

  The arguments to constrain. Each must be a choice or free variable

  node, or ID. The associated IDs must refer to free variables.

  constraint_type:

  The constraint type. Must be STRICT_CONSTRAINT or NONSTRICT_CONSTRAINT.

  config:

  The configuration to use as context.

  guards:

  A list that takes the pairs of bindings (dropped, kept) of the unions that merge two bound classes (update_binding; decision D26 of 2026-10-12), or None: such a merge then fails the step. The constraint step at the root (fairscheme.D) puts the strict equality of each pair above its result.

• arg1 –

  The arguments to constrain. Each must be a choice or free variable

  node, or ID. The associated IDs must refer to free variables.

  constraint_type:

  The constraint type. Must be STRICT_CONSTRAINT or NONSTRICT_CONSTRAINT.

  config:

  The configuration to use as context.

  guards:

  A list that takes the pairs of bindings (dropped, kept) of the unions that merge two bound classes (update_binding; decision D26 of 2026-10-12), or None: such a merge then fails the step. The constraint step at the root (fairscheme.D) puts the strict equality of each pair above its result.

Returns:

A Boolean indicating whether the resulting configuration remains consistent.

curry.backends.py.eval.rts_constraints.constraint_type(rts, arg=None, config=None)

Indicates the constraint type.

curry.backends.py.eval.rts_constraints.lift_constraint(rts, var, rewrite=None)

Similar to a pull-tab step, lift the constraint at var.target above var.root.

curry.backends.py.eval.rts_constraints.occurs(rts, i, j, ri, rj, config=None)

The occurs check at the union of two classes of free variables (the decision of 2026-10-12 on the Fair Scheme). i and j are the two variables of the constraint, just united; ri and rj are the roots of their classes before the union. Returns True when the merged class has a cycle: a member whose generator instance, as created so far, contains another member of the class. Such a class has no finite instance (x = S x has no term), so the step fails.

The test is local to the union. It walks the generator instance of each side (the generator of the variable or of its old root; a side without one, undecided or fresh, has no instance): the choice nodes along the decided path, the constructor cells, through forward cells, down to the inner free variables. An inner variable of the merged class is the cycle. An inner variable of another decided class is bound through that class (Def 2.74), so the walk continues into the generator of that class, once per class. A choice the configuration has not decided ends the walk there: the variable is not narrowed here, and its generator is no instance of it. The C++ runtime has the same test (occurs in state/rts_constraints.cpp), and the checker verifies the invariant (D15 (occurs check)).