Control.Solve

The Solve effect: a metavariable solver as an effect.

A solver owns three concerns that otherwise thread through every rule as parameters: allocating fresh metavariable classes, looking a class up in the current substitution, and joining classes in a union-find. Solve(d) bundles the three as ops over classes carrying a descriptor of type d (a solution, a rank, a binding level), so solver rules read as direct style and never name the forest. run_solve discharges the effect through a private payload-carrying forest (Data.UnionFind.Payload) scoped to the run; the combine policy it installs is the one place a join’s descriptors meet, so swapping the handler swaps the solver strategy without touching a rule.

Class keys are minted only by sv_fresh, which is what keeps the ops total: sv_find answers None for a key that was never minted, and sv_assign/sv_union on such a key are inert. Every clause resumes exactly once in tail position, so the compiler is free to lower the whole run to direct state updates. Opt-in: not in Base.

Effects

Solve

effect Solve(d)
  sv_fresh(d) : Int
  sv_find(Int) : Option((Int, d))
  sv_assign(Int, d) : Unit
  sv_union(Int, Int) : Unit

Allocate (sv_fresh), look up (sv_find), solve (sv_assign), and join (sv_union) metavariable classes with descriptors of type d.

Functions and Values

run_solve

run_solve : forall e0 a b. ((a, a) -> a, () -> b ! {Control.Solve.Solve(a), Var@forest@48, Var@next@49, e0}) -> (b, Data.UnionFind.Payload.UnionFind(Int, a)) ! {e0}

Run action against a fresh solver, discharging Solve(d); returns the result paired with the final forest. combine is the join policy: on sv_union it receives the kept root’s descriptor first and the absorbed root’s second, exactly once per join that changes the partition.

import Data.UnionFind.Payload (ufp_roots)

let (_r, forest) = run_solve(concat, \() -> sv_union(sv_fresh("a"), sv_fresh("b")))
ufp_roots(forest)

[(0, ab)]

eval_solve

eval_solve : forall e0 a b. ((a, a) -> a, () -> b ! {Control.Solve.Solve(a), Var@forest@48, Var@next@49, e0}) -> b ! {e0}

Run action for its result only, discarding the final forest.

eval_solve(concat, \() -> sv_find(sv_fresh("root")))

Some((0, root))

sv_root

sv_root : forall a. (Int) -> Int ! {Control.Solve.Solve(a)}

The canonical root of x’s class; a key that was never minted is its own root.

sv_solution

sv_solution : forall a. (Int) -> Option(a) ! {Control.Solve.Solve(a)}

The descriptor at x’s root: the substitution lookup.

eval_solve(concat, \() -> sv_solution(sv_fresh("solved")))

Some(solved)

sv_equiv

sv_equiv : forall a. (Int, Int) -> Bool ! {Control.Solve.Solve(a)}

True when x and y belong to the same class.