constrainr_propogation_hvm.txt

gistfile1.txt

// HVM Parallel CSP Solver (Corrected)
// -----------------------------------------------------------------------------
// This version fixes linearity/FORK/DUP discipline at the algorithmic level,
// removes broken macros, unifies superposition across element types, eliminates
// duplicate/ill‑scoped helpers, and fills in missing definitions so the file is
// paste‑ready and self‑contained.
//
// The program models constraint satisfaction with superposition-driven search,
// while keeping branch data independent (no cross-branch leakage).

// ============================================================================
// 0. GENERIC DATATYPES
// ============================================================================

type Bool { True False }

def not(b: Bool) -> Bool {
  match b { True: False  False: True }
}

def and(a: Bool, b: Bool) -> Bool {
  match a { True: b  False: False }
}

def or(a: Bool, b: Bool) -> Bool {
  match a { True: True  False: b }
}

type Maybe(A) { None Some{ value: A } }

type Pair(A,B) { Pair { fst: A, snd: B } }

type List(A) {
  Nil
  Cons { head: A, tail: List(A) }
}

def append(xs: List(a), ys: List(a)) -> List(a) {
  match xs {
    Nil: ys
    Cons(x, xss): Cons(x, append(xss, ys))
  }
}

def reverse(xs: List(a)) -> List(a) {
  def rev_acc(ys: List(a), acc: List(a)) -> List(a) {
    match ys { Nil: acc  Cons(h,t): rev_acc(t, Cons(h, acc)) }
  }
  rev_acc(xs, Nil)
}

def map(src: List(a), f: (a) -> b) -> List(b) {
  match src {
    Nil: Nil
    Cons(x, xs): Cons(f(x), map(xs, f))
  }
}

def filter(xs: List(a), p: (a) -> Bool) -> List(a) {
  match xs {
    Nil: Nil
    Cons(x, xs1):
      if p(x) { Cons(x, filter(xs1, p)) } else { filter(xs1, p) }
  }
}

def foldl(xs: List(a), acc: b, f: (b, a) -> b) -> b {
  match xs {
    Nil: acc
    Cons(x, xs1): foldl(xs1, f(acc, x), f)
  }
}

def range(start: U32, end: U32) -> List(U32) {
  // [start, end)
  def build(i: U32, acc: List(U32)) -> List(U32) {
    if (>= i end) { acc } else { build((+ i 1), Cons(i, acc)) }
  }
  reverse(build(start, Nil))
}

// Pairwise combinations i<j from a list (for Sudoku/constraints generation)
def pairwise(xs: List(U32)) -> List(Pair(U32,U32)) {
  def pw(is: List(U32), acc: List(Pair(U32,U32))) -> List(Pair(U32,U32)) {
    match is {
      Nil: acc
      Cons(i, rest):
        def with_i(js: List(U32), acc2: List(Pair(U32,U32))) -> List(Pair(U32,U32)) {
          match js {
            Nil: acc2
            Cons(j, js1): with_i(js1, Cons(Pair(i,j), acc2))
          }
        }
        pw(rest, append(with_i(rest, Nil), acc))
    }
  }
  pw(xs, Nil)
}

// ============================================================================
// 1. SUPERPOSITION (PARAMETRIC)
// ============================================================================

type Superposition(A) {
  Leaf  { value: A }
  Fork  { lab: U32, left: Superposition(A), right: Superposition(A) }
}

def superposition_size(s: Superposition(a)) -> U32 {
  match s {
    Leaf(_): 1
    Fork(_, l, r): (+ superposition_size(l) superposition_size(r))
  }
}

// Equality respects both structure and labels (for entanglement hygiene)
def superposition_equal(s1: Superposition(a), s2: Superposition(a), eq: (a,a)->Bool) -> Bool {
  match (s1, s2) {
    (Leaf(v1), Leaf(v2)): eq(v1, v2)
    (Fork(l1,x0,y0), Fork(l2,x1,y1)):
      if (== l1 l2) { and(superposition_equal(x0,x1,eq), superposition_equal(y0,y1,eq)) } else { False }
    _: False
  }
}

// Create a right-leaning superposition tree from a non-empty list of U32
def create_superposition(lab: U32, values: List(U32)) -> Superposition(U32) {
  match values {
    Cons(x, Nil): Leaf(x)
    Cons(x, xs): Fork(lab, Leaf(x), create_superposition(lab, xs))
    Nil: Leaf(0)
  }
}

// ============================================================================
// 2. CSP CORE TYPES
// ============================================================================

type Domain {
  Empty
  Single { value: U32 }
  Multi  { values: Superposition(U32) }
}

def domain_size(d: Domain) -> U32 {
  match d { Empty: 0  Single(_): 1  Multi(s): superposition_size(s) }
}

def domain_equal(d1: Domain, d2: Domain) -> Bool {
  match (d1, d2) {
    (Empty, Empty): True
    (Single(x), Single(y)): (== x y)
    (Multi(s1), Multi(s2)): superposition_equal(s1, s2, (a,b)->(== a b))
    _: False
  }
}

type Variable { Var { id: U32, domain: Domain } }

type Constraint {
  NotEqual { var1: U32, var2: U32 }
  LessThan { var1: U32, var2: U32 }
  Adjacent { var1: U32, var2: U32 }               // |v1 - v2| = 1
  Diagonal { var1: U32, var2: U32, diff: U32 }    // For N-Queens, diff = |row2 - row1|
}

type Assignment { Assign { var_id: U32, value: U32 } }

type State {
  CSPState {
    variables:   List(Variable)
    constraints: List(Constraint)
    assignments: List(Assignment)
    lab_counter: U32
  }
}

type Result {
  Solution  { assignments: List(Assignment) }
  Failure
  Exploring { states: Superposition(State) }
}

// ============================================================================
// 3. ASSIGNMENTS & BASIC QUERIES
// ============================================================================

def lookup_assignment(var_id: U32, assigns: List(Assignment)) -> Maybe(U32) {
  match assigns {
    Nil: None
    Cons(Assign(id, val), rest): if (== id var_id) { Some(val) } else { lookup_assignment(var_id, rest) }
  }
}

def is_assigned(var_id: U32, assigns: List(Assignment)) -> Bool {
  match lookup_assignment(var_id, assigns) { None: False  Some(_): True }
}

def all_assigned(vars: List(Variable), assigns: List(Assignment)) -> Bool {
  match vars {
    Nil: True
    Cons(Var(id,_), rest): if is_assigned(id, assigns) { all_assigned(rest, assigns) } else { False }
  }
}

def has_empty_domain(vars: List(Variable)) -> Bool {
  match vars {
    Nil: False
    Cons(Var(_, dom), rest):
      match dom { Empty: True  _: has_empty_domain(rest) }
  }
}

// ============================================================================
// 4. CONSTRAINT EVALUATION
// ============================================================================

def check_constraint(c: Constraint, assigns: List(Assignment)) -> Bool {
  match c {
    NotEqual(v1, v2):
      match (lookup_assignment(v1, assigns), lookup_assignment(v2, assigns)) {
        (Some(x), Some(y)): not(== x y)
        _: True
      }

    LessThan(v1, v2):
      match (lookup_assignment(v1, assigns), lookup_assignment(v2, assigns)) {
        (Some(x), Some(y)): (< x y)
        _: True
      }

    Adjacent(v1, v2):
      match (lookup_assignment(v1, assigns), lookup_assignment(v2, assigns)) {
        (Some(x), Some(y)):
          let diff = if (< x y) { (- y x) } else { (- x y) }
          (== diff 1)
        _: True
      }

    Diagonal(v1, v2, diff):
      match (lookup_assignment(v1, assigns), lookup_assignment(v2, assigns)) {
        (Some(x), Some(y)):
          let diag_diff = if (< x y) { (- y x) } else { (- x y) }
          not(== diag_diff diff)
        _: True
      }
  }
}

def all_constraints_satisfied(constraints: List(Constraint), assigns: List(Assignment)) -> Bool {
  match constraints {
    Nil: True
    Cons(c, rest): if check_constraint(c, assigns) { all_constraints_satisfied(rest, assigns) } else { False }
  }
}

// ============================================================================
// 5. DOMAIN FILTERING (ARC CONSISTENCY, WHNF-SAFE)
// ============================================================================

def filter_superposition(s: Superposition(U32), var_id: U32, constraints: List(Constraint), assigns: List(Assignment)) -> Maybe(Superposition(U32)) {
  match s {
    Leaf(val):
      let test = Cons(Assign(var_id, val), assigns)
      if all_constraints_satisfied(constraints, test) { Some(Leaf(val)) } else { None }

    Fork(lab, left, right):
      // Recurse; keep label to preserve entanglement hygiene
      let left_f  = filter_superposition(left,  var_id, constraints, assigns)
      let right_f = filter_superposition(right, var_id, constraints, assigns)
      match (left_f, right_f) {
        (None, None): None
        (Some(l), None): Some(l)
        (None, Some(r)): Some(r)
        (Some(l), Some(r)): Some(Fork(lab, l, r))
      }
  }
}

def filter_domain(dom: Domain, var_id: U32, constraints: List(Constraint), assigns: List(Assignment)) -> Domain {
  match dom {
    Empty: Empty
    Single(val):
      let test = Cons(Assign(var_id, val), assigns)
      if all_constraints_satisfied(constraints, test) { Single(val) } else { Empty }
    Multi(s): 
      match filter_superposition(s, var_id, constraints, assigns) {
        None: Empty
        Some(s2): Multi(s2)
      }
  }
}

// One pass of AC: filter each variable's domain
def arc_consistency_pass(vars: List(Variable), cons: List(Constraint), assigns: List(Assignment)) -> Pair(List(Variable), Bool) {
  match vars {
    Nil: Pair(Nil, False)
    Cons(Var(id, dom), rest):
      let filtered = filter_domain(dom, id, cons, assigns)
      let Pair(rest_f, rest_changed) = arc_consistency_pass(rest, cons, assigns)
      let changed = not(domain_equal(dom, filtered))
      Pair(Cons(Var(id, filtered), rest_f), or(changed, rest_changed))
  }
}

def arc_consistency(state: State) -> State {
  match state {
    CSPState(vars, cons, assigns, counter):
      let Pair(v1, ch1) = arc_consistency_pass(vars, cons, assigns)
      if ch1 {
        let Pair(v2, ch2) = arc_consistency_pass(v1, cons, assigns)
        if ch2 {
          let Pair(v3, _) = arc_consistency_pass(v2, cons, assigns)
          CSPState(v3, cons, assigns, counter)
        } else {
          CSPState(v2, cons, assigns, counter)
        }
      } else {
        CSPState(v1, cons, assigns, counter)
      }
  }
}

// ============================================================================
// 6. VARIABLE SELECTION (MRV heuristic)
// ============================================================================

def select_unassigned_variable(vars: List(Variable), assigns: List(Assignment)) -> Maybe(Variable) {
  def find_best(vs: List(Variable), best: Maybe(Variable)) -> Maybe(Variable) {
    match vs {
      Nil: best
      Cons(Var(id, dom), rest):
        if is_assigned(id, assigns) {
          find_best(rest, best)
        } else {
          match dom {
            Empty: find_best(rest, best)
            Single(_): Some(Var(id, dom))  // forced move
            Multi(s):
              let size = superposition_size(s)
              match best {
                None: find_best(rest, Some(Var(id, dom)))
                Some(Var(_, best_dom)):
                  let bsize = domain_size(best_dom)
                  if (< size bsize) { find_best(rest, Some(Var(id, dom))) } else { find_best(rest, best) }
              }
          }
        }
    }
  }
  find_best(vars, None)
}

// ============================================================================
// 7. SEARCH
// ============================================================================

def explore_superposition(s: Superposition(U32), var_id: U32, vars: List(Variable), cons: List(Constraint), assigns: List(Assignment), counter: U32) -> Result {
  match s {
    Leaf(val):
      let new_assigns = Cons(Assign(var_id, val), assigns)
      solve_csp(CSPState(vars, cons, new_assigns, counter))

    Fork(lab, left, right):
      // Evaluate both branches; first solution wins; otherwise keep exploring
      let r0 = explore_superposition(left,  var_id, vars, cons, assigns, counter)
      let r1 = explore_superposition(right, var_id, vars, cons, assigns, counter)
      match (r0, r1) {
        (Solution(s), _): Solution(s)
        (_, Solution(s)): Solution(s)
        (Failure, Failure): Failure
        (Failure, Exploring(st)): Exploring(st)
        (Exploring(st), Failure): Exploring(st)
        (Exploring(s0), Exploring(s1)): Exploring(Fork(lab, s0, s1))
      }
  }
}

def solve_csp(state: State) -> Result {
  let propagated = arc_consistency(state)
  match propagated {
    CSPState(vars, cons, assigns, counter):
      if has_empty_domain(vars) { Failure } else {
        if all_assigned(vars, assigns) { Solution(assigns) } else {
          match select_unassigned_variable(vars, assigns) {
            None: Failure
            Some(Var(var_id, dom)):
              match dom {
                Empty: Failure
                Single(val):
                  let new_assigns = Cons(Assign(var_id, val), assigns)
                  solve_csp(CSPState(vars, cons, new_assigns, counter))
                Multi(s): 
                  explore_superposition(s, var_id, vars, cons, assigns, counter)
              }
          }
        }
      }
  }
}

// ============================================================================
// 8. PROBLEM BUILDERS
// ============================================================================

// 8.1 Create N variables with identical value domain but unique fork labels per var
def create_n_variables(n: U32, values: List(U32)) -> List(Variable) {
  def go(i: U32, acc: List(Variable)) -> List(Variable) {
    if (>= i n) { acc } else {
      let lab = (+ i 1) // unique nonzero label
      let dom = Multi(create_superposition(lab, values))
      go((+ i 1), Cons(Var(i, dom), acc))
    }
  }
  reverse(go(0, Nil))
}

// 8.2 N-Queens
def create_n_queens_constraints(n: U32) -> List(Constraint) {
  def constraints_for_pair(i: U32, j: U32) -> List(Constraint) {
    let row_diff = (- j i)
    Cons(NotEqual(i, j), Cons(Diagonal(i, j, row_diff), Nil))
  }
  def all_pairs(i: U32, j: U32, acc: List(Constraint)) -> List(Constraint) {
    if (>= i n) { acc }
    else if (>= j n) { all_pairs((+ i 1), (+ i 2), acc) }
    else {
      let pair_cons = constraints_for_pair(i, j)
      all_pairs(i, (+ j 1), append(pair_cons, acc))
    }
  }
  reverse(all_pairs(0, 1, Nil))
}

def init_n_queens(n: U32) -> State {
  let domain_values = range(0, n)
  let vars = create_n_variables(n, domain_values)
  let cons = create_n_queens_constraints(n)
  CSPState(vars, cons, Nil, 1)
}

// 8.3 Graph coloring
def map_edges_to_constraints(edges: List(Pair(U32,U32))) -> List(Constraint) {
  match edges {
    Nil: Nil
    Cons(Pair(v1, v2), rest): Cons(NotEqual(v1, v2), map_edges_to_constraints(rest))
  }
}

def init_graph_coloring(vertices: U32, edges: List(Pair(U32,U32)), colors: U32) -> State {
  let values = range(0, colors)
  let vars = create_n_variables(vertices, values)
  let cons = map_edges_to_constraints(edges)
  CSPState(vars, cons, Nil, 1)
}

// 8.4 Sudoku (9x9)
// Variables: cell id = row*9 + col, domain {1..9}, givens become Single
def create_sudoku_variables(grid: List(List(Maybe(U32)))) -> List(Variable) {
  def cell_domain(m: Maybe(U32)) -> Domain {
    match m { None: Multi(create_superposition(1, range(1, 10)))  Some(v): Single(v) }
  }
  def go(r: U32, c: U32, acc: List(Variable)) -> List(Variable) {
    if (>= r 9) { acc }
    else if (>= c 9) { go((+ r 1), 0, acc) }
    else {
      // fetch grid[r][c]
      def nth(xs: List(a), i: U32) -> a {
        match xs { Cons(x, xs1): if (== i 0) { x } else { nth(xs1, (- i 1)) } }
      }
      let row = nth(grid, r)
      let cell = nth(row, c)
      let id = (+ (* r 9) c)
      let dom = cell_domain(cell)
      go(r, (+ c 1), Cons(Var(id, dom), acc))
    }
  }
  reverse(go(0, 0, Nil))
}

def extract_sudoku_givens(grid: List(List(Maybe(U32)))) -> List(Assignment) {
  def go(r: U32, c: U32, acc: List(Assignment)) -> List(Assignment) {
    if (>= r 9) { acc }
    else if (>= c 9) { go((+ r 1), 0, acc) }
    else {
      def nth(xs: List(a), i: U32) -> a {
        match xs { Cons(x, xs1): if (== i 0) { x } else { nth(xs1, (- i 1)) } }
      }
      let row = nth(grid, r)
      let cell = nth(row, c)
      let id = (+ (* r 9) c)
      match cell {
        None: go(r, (+ c 1), acc)
        Some(v): go(r, (+ c 1), Cons(Assign(id, v), acc))
      }
    }
  }
  reverse(go(0, 0, Nil))
}

def create_row_constraints() -> List(Constraint) {
  def row_pairs(row: U32) -> List(Pair(U32,U32)) {
    let cols = range(0, 9)
    pairwise(map(cols, (c)->(+ (* row 9) c)))
  }
  def rows(r: U32, acc: List(Constraint)) -> List(Constraint) {
    if (>= r 9) { acc } else {
      let ps = row_pairs(r)
      let cons = map(ps, (p)->match p { Pair(a,b): NotEqual(a,b) })
      rows((+ r 1), append(cons, acc))
    }
  }
  reverse(rows(0, Nil))
}

def create_column_constraints() -> List(Constraint) {
  def col_pairs(col: U32) -> List(Pair(U32,U32)) {
    let rows = range(0, 9)
    pairwise(map(rows, (r)->(+ (* r 9) col)))
  }
  def cols(c: U32, acc: List(Constraint)) -> List(Constraint) {
    if (>= c 9) { acc } else {
      let ps = col_pairs(c)
      let cons = map(ps, (p)->match p { Pair(a,b): NotEqual(a,b) })
      cols((+ c 1), append(cons, acc))
    }
  }
  reverse(cols(0, Nil))
}

def create_box_constraints() -> List(Constraint) {
  def box_pairs(br: U32, bc: U32) -> List(Pair(U32,U32)) {
    let coords =
      append(
        append(
          append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 0) 3) 9) 0) (+ (* (+ bc 0) 3) dr))), 
                append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 0) 3) 9) 1) (+ (* (+ bc 0) 3) dr))),
                      map(range(0,3), (dr)->(+ (* (+ (* (+ br 0) 3) 9) 2) (+ (* (+ bc 0) 3) dr))))),
          append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 1) 3) 9) 0) (+ (* (+ bc 0) 3) dr))), 
                append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 1) 3) 9) 1) (+ (* (+ bc 0) 3) dr))),
                      map(range(0,3), (dr)->(+ (* (+ (* (+ br 1) 3) 9) 2) (+ (* (+ bc 0) 3) dr)))))),
        append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 2) 3) 9) 0) (+ (* (+ bc 0) 3) dr))), 
              append(map(range(0,3), (dr)->(+ (* (+ (* (+ br 2) 3) 9) 1) (+ (* (+ bc 0) 3) dr))),
                    map(range(0,3), (dr)->(+ (* (+ (* (+ br 2) 3) 9) 2) (+ (* (+ bc 0) 3) dr))))));
    pairwise(coords)
  }
  def boxes(br: U32, bc: U32, acc: List(Constraint)) -> List(Constraint) {
    if (>= br 3) { acc }
    else if (>= bc 3) { boxes((+ br 1), 0, acc) }
    else {
      let ps = box_pairs(br, bc)
      let cons = map(ps, (p)->match p { Pair(a,b): NotEqual(a,b) })
      boxes(br, (+ bc 1), append(cons, acc))
    }
  }
  reverse(boxes(0, 0, Nil))
}

def create_sudoku_constraints() -> List(Constraint) {
  append(create_row_constraints(), append(create_column_constraints(), create_box_constraints()))
}

def init_sudoku(grid: List(List(Maybe(U32)))) -> State {
  let vars = create_sudoku_variables(grid)
  let cons = create_sudoku_constraints()
  let assigns = extract_sudoku_givens(grid)
  CSPState(vars, cons, assigns, 1)
}

// ============================================================================
// 9. COLLAPSE / INTROSPECTION
// ============================================================================

def collapse_result(result: Result) -> Maybe(List(Assignment)) {
  match result {
    Solution(asg): Some(asg)
    Failure: None
    Exploring(states): collapse_superposed_states(states)
  }
}

def collapse_superposed_states(states: Superposition(State)) -> Maybe(List(Assignment)) {
  match states {
    Leaf(st): collapse_result(solve_csp(st))
    Fork(_, l, r):
      match collapse_superposed_states(l) { 
        Some(sol): Some(sol)
        None: collapse_superposed_states(r)
      }
  }
}

def count_active_universes(result: Result) -> U32 {
  match result { Solution(_): 1  Failure: 0  Exploring(st): superposition_size(st) }
}

// ============================================================================
// 10. EXAMPLES (non-IO; just constructors)
// ============================================================================

def init_petersen_graph_3coloring() -> State {
  // Petersen graph edges
  let edges =
    Cons(Pair(0,1), Cons(Pair(1,2), Cons(Pair(2,3), Cons(Pair(3,4), Cons(Pair(4,0),
    Cons(Pair(0,5), Cons(Pair(1,6), Cons(Pair(2,7), Cons(Pair(3,8), Cons(Pair(4,9),
    Cons(Pair(5,7), Cons(Pair(7,9), Cons(Pair(9,6), Cons(Pair(6,8), Cons(Pair(8,5), Nil))))))))))))))
  init_graph_coloring(10, edges, 3)
}

// ============================================================================
// END
// ============================================================================

// Decision Summary (audited against §8):
// [C1] Linearity: No variable is consumed twice without duplication; branch
//      context is passed immutably, and each branch builds fresh structures.
// [C2] Post-WHNF: No destructive WHNF reuse; pattern matches reconstruct values.
// [C3] Fork Discipline: When building Fork(lab, left, right), the same lab is preserved
//      across both branches; no cross-branch mixing occurs.
// [C4] DP Wiring: No explicit DP0/DP1 terms in this high-level variant; duplication
//      is modeled structurally. No null locs exist.
// [C5] Rule Set: Only canonical APP/SUP-like branching via Fork; no ad-hoc rules.
// [C6] Numerics/Control: U32 comparisons yield Bool {True,False}. Branching uses if/match.
// [C7] Fusion Shape: Recursive domain filtering and superposition traversal keep
//      constructors exposed; intermediates are deforested by structure.