Fix MOV memoization safety and add repro tests

clang/hvm4.c

@@ -92,6 +92,7 @@ typedef struct {
 #define MOV 47  // Mov(v, b): move binding
 #define GOT 48  // Got(n): linked mov variable
 
+
 // LAM Ext Flags
 // =============
 #define LAM_ERA_MASK 0x800000  // binder unused in lambda body
@@ -223,6 +224,7 @@ static u32 FRESH = 1;
 #include "wnf/tid.c"
 
 static int   DEBUG = 0;
+static int   SAFE_MOV  = 1;
 
 // Nick Alphabet
 // =============
@@ -321,6 +323,17 @@ static int    PARSE_FORK_SIDE = -1;      // -1 = off, 0 = left branch (DP0), 1 =
 #include "term/new/num.c"
 #include "term/clone.c"
 
+fn void safe_mov_init_from_env(void) {
+  const char *val = getenv("HVM4_SAFE_MOV");
+  if (val != NULL && val[0] != '\0') {
+    if (val[0] == '0' && val[1] == '\0') {
+      SAFE_MOV = 0;
+    } else {
+      SAFE_MOV = 1;
+    }
+  }
+}
+
 // Heap Substitution
 // =================
 
@@ -421,9 +434,11 @@ static int    PARSE_FORK_SIDE = -1;      // -1 = off, 0 = left branch (DP0), 1 =
 #include "wnf/app_mat_ctr.c"
 #include "wnf/mat_inc.c"
 #include "wnf/dup_nam.c"
+#include "wnf/dup_got.c"
 #include "wnf/dup_dry.c"
 #include "wnf/dup_red.c"
 #include "wnf/dup_lam.c"
+#include "wnf/dup_mov.c"
 #include "wnf/dup_sup.c"
 #include "wnf/dup_nod.c"
 #include "wnf/mov_nam.c"

clang/main.c

@@ -109,6 +109,7 @@ int main(int argc, char **argv) {
 
   // Set debug mode
   DEBUG = opts.debug;
+  safe_mov_init_from_env();
 
   // Parse prelude
   PState ps = {

clang/parse/term/mov.c

@@ -1,5 +1,93 @@
 fn Term parse_term(PState *s, u32 depth);
 
+fn u32 mov_region_count_go(u64 loc, u32 lvl, u8 tgt, u32 ext, int *viol);
+fn void mov_rebind_bjm_to_bjv_go(u64 loc, u32 lvl);
+fn Term mov_rebind_bjm_to_bjv_term(Term t, u32 lvl);
+
+fn u32 mov_region_count_term(Term t, u32 lvl, u8 tgt, u32 ext, int *viol) {
+  if (*viol) {
+    return 0;
+  }
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+
+  if (tg == tgt && vl == lvl && (tgt == BJV || term_ext(t) == ext)) {
+    return 1;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return 0;
+  }
+
+  if (tg == LAM) {
+    u32 cnt = mov_region_count_go(vl, lvl, tgt, ext, viol);
+    if (cnt > 1) {
+      *viol = 1;
+    }
+    return 0;
+  }
+
+  u32 sum = 0;
+  for (u32 i = 0; i < ari; i++) {
+    sum += mov_region_count_go(vl + i, lvl, tgt, ext, viol);
+  }
+  return sum;
+}
+
+fn u32 mov_region_count_go(u64 loc, u32 lvl, u8 tgt, u32 ext, int *viol) {
+  return mov_region_count_term(HEAP[loc], lvl, tgt, ext, viol);
+}
+
+fn int mov_region_violates(Term body, u32 lvl, u8 tgt, u32 ext) {
+  int viol = 0;
+  u32 cnt = mov_region_count_term(body, lvl, tgt, ext, &viol);
+  return viol || cnt > 1;
+}
+
+fn void mov_rebind_bjm_to_bjv_go(u64 loc, u32 lvl) {
+  Term t = HEAP[loc];
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == BJM && vl == lvl) {
+    Term v = term_new(0, BJV, 0, vl);
+    HEAP[loc] = sub ? term_sub_set(v, 1) : v;
+    return;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return;
+  }
+
+  for (u32 i = 0; i < ari; i++) {
+    mov_rebind_bjm_to_bjv_go(vl + i, lvl);
+  }
+}
+
+fn Term mov_rebind_bjm_to_bjv_term(Term t, u32 lvl) {
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == BJM && vl == lvl) {
+    Term v = term_new(0, BJV, 0, vl);
+    return sub ? term_sub_set(v, 1) : v;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return t;
+  }
+
+  for (u32 i = 0; i < ari; i++) {
+    mov_rebind_bjm_to_bjv_go(vl + i, lvl);
+  }
+  return t;
+}
+
 fn Term parse_term_mov(PState *s, u32 depth) {
   parse_skip(s);
   u32 nam = parse_name(s);
@@ -11,9 +99,24 @@ fn Term parse_term_mov(PState *s, u32 depth) {
   parse_skip(s);
   parse_bind_push(nam, depth, 0, PBIND_MOV, 0);
   Term body = parse_term(s, depth + 1);
+  u32 uses = parse_bind_get_uses();
   parse_bind_pop();
+  u32 lvl = depth + 1;
+  int viol = mov_region_violates(body, lvl, BJM, 0);
+  if (viol) {
+    body = mov_rebind_bjm_to_bjv_term(body, lvl);
+    body = parse_auto_dup(body, lvl, lvl, BJV, 0);
+    u64 lam_loc = heap_alloc(1);
+    HEAP[lam_loc] = body;
+    Term lam = term_new(0, LAM, lvl, lam_loc);
+    return term_new_app(lam, val);
+  }
   u64 loc = heap_alloc(2);
   HEAP[loc + 0] = val;
   HEAP[loc + 1] = body;
+  if (uses > 2) {
+    body = parse_auto_dup(body, lvl, lvl, BJM, 0);
+    HEAP[loc + 1] = body;
+  }
   return term_new(0, MOV, 0, loc);
 }

clang/wnf/_.c

@@ -639,6 +639,14 @@ __attribute__((hot)) fn Term wnf(Term term) {
               whnf = wnf_dup_lam(lab, loc, side, whnf);
               continue;
             }
+            case MOV: {
+              whnf = wnf_dup_mov(lab, loc, side, whnf);
+              continue;
+            }
+            case GOT: {
+              whnf = wnf_dup_got(lab, loc, side, whnf);
+              continue;
+            }
             case SUP: {
               next = wnf_dup_sup(lab, loc, side, whnf);
               goto enter;
@@ -708,6 +716,7 @@ __attribute__((hot)) fn Term wnf(Term term) {
               next = wnf_mov_sup(loc, whnf);
               goto enter;
             }
+            case VAR:
             case ERA:
             case ANY:
             case NUM: {

clang/wnf/app_lam.c

@@ -1,7 +1,3 @@
-// (λx.f a)
-// -------- APP-LAM
-// x ← a
-// f
 fn Term wnf_app_lam(Term lam, Term arg) {
   ITRS++;
   u32  loc     = term_val(lam);

clang/wnf/dup_got.c

@@ -0,0 +1,21 @@
+// ! X &L = x
+// --------- DUP-GOT
+// ! A &L = v
+// X₀ ← A₀
+// X₁ ← A₁
+fn Term wnf_dup_got(u32 lab, u32 loc, u8 side, Term got) {
+  ITRS++;
+  u32  got_loc = term_val(got);
+  u32  got_ext = term_ext(got);
+  Term val     = heap_read(got_loc);
+  Copy V       = term_clone(lab, val);
+
+  u64  loc0 = heap_alloc(1);
+  u64  loc1 = heap_alloc(1);
+  heap_write(loc0, V.k0);
+  heap_write(loc1, V.k1);
+
+  Term g0 = term_new(0, GOT, got_ext, (u32)loc0);
+  Term g1 = term_new(0, GOT, got_ext, (u32)loc1);
+  return heap_subst_cop(side, loc, g0, g1);
+}

clang/wnf/dup_mov.c

@@ -0,0 +1,55 @@
+// ! X &L = % Y = v; b
+// -------------------- DUP-MOV
+// ! A &L = v
+// X₀ ← % Y0 = A₀; b[Y:=Y0]
+// X₁ ← % Y1 = A₁; b[Y:=Y1]
+fn Term mov_clone_rebind_got(Term t, u32 old_loc, u32 new_loc) {
+  u8  tg  = term_tag(t);
+  u32 vl  = term_val(t);
+  u32 ext = term_ext(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == GOT && vl == old_loc) {
+    Term v = term_new_got(new_loc);
+    return sub ? term_sub_set(v, 1) : v;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return t;
+  }
+
+  u64 loc = heap_alloc(ari);
+  for (u32 i = 0; i < ari; i++) {
+    Term child = heap_read(vl + i);
+    Term repl  = mov_clone_rebind_got(child, old_loc, new_loc);
+    heap_write(loc + i, repl);
+  }
+
+  Term res = term_new(0, tg, ext, (u32)loc);
+  return sub ? term_sub_set(res, 1) : res;
+}
+
+fn Term wnf_dup_mov(u32 lab, u32 loc, u8 side, Term mov) {
+  ITRS++;
+  u32  mov_loc = term_val(mov);
+  u32  mov_ext = term_ext(mov);
+  Term val     = heap_read(mov_loc + 0);
+  Term bod     = heap_read(mov_loc + 1);
+
+  Copy V = term_clone(lab, val);
+
+  u64  loc0 = heap_alloc(2);
+  u64  loc1 = heap_alloc(2);
+  Term bod0 = mov_clone_rebind_got(bod, mov_loc, (u32)loc0);
+  Term bod1 = mov_clone_rebind_got(bod, mov_loc, (u32)loc1);
+
+  heap_write(loc0 + 0, V.k0);
+  heap_write(loc0 + 1, bod0);
+  heap_write(loc1 + 0, V.k1);
+  heap_write(loc1 + 1, bod1);
+
+  Term m0 = term_new(0, MOV, mov_ext, (u32)loc0);
+  Term m1 = term_new(0, MOV, mov_ext, (u32)loc1);
+  return heap_subst_cop(side, loc, m0, m1);
+}

clang/wnf/mov_lam.c

@@ -8,13 +8,15 @@ fn Term wnf_mov_lam(u32 loc, Term lam) {
   u32  lam_ext = term_ext(lam);
   Term bod     = heap_read(lam_loc);
 
-  u64  base    = heap_alloc(2);
-  u32  g_loc   = (u32)base;
-  u32  x_loc   = g_loc + 1;
+  u64 base  = heap_alloc(2);
+  u32 g_loc = (u32)base;
+  u32 x_loc = g_loc + 1;
   heap_write(g_loc, bod);
   heap_write(x_loc, term_new_got(g_loc));
   heap_subst_var(lam_loc, term_new(0, VAR, 0, x_loc));
-  Term res     = term_new(0, LAM, lam_ext, x_loc);
-  heap_subst_var(loc, res);
+  Term res = term_new(0, LAM, lam_ext, x_loc);
+  if (!SAFE_MOV || (lam_ext & LAM_ERA_MASK)) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }

clang/wnf/mov_nod.c

@@ -8,7 +8,9 @@ fn Term wnf_mov_nod(u32 loc, Term term) {
   ITRS++;
   u32 ari = term_arity(term);
   if (ari == 0) {
-    heap_subst_var(loc, term);
+    if (!SAFE_MOV) {
+      heap_subst_var(loc, term);
+    }
     return term;
   }
   u32  t_loc = term_val(term);
@@ -22,6 +24,8 @@ fn Term wnf_mov_nod(u32 loc, Term term) {
     heap_write(nod_loc + i, term_new_got(got_loc + i));
   }
   Term res = term_new(0, t_tag, t_ext, nod_loc);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }

clang/wnf/mov_red.c

@@ -13,6 +13,8 @@ fn Term wnf_mov_red(u32 loc, Term red) {
   Term f     = term_new_got(at + 0);
   Term g     = term_new_got(at + 1);
   Term res   = term_new_red_at(at + 2, f, g);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }

clang/wnf/mov_sup.c

@@ -14,6 +14,8 @@ fn Term wnf_mov_sup(u32 loc, Term sup) {
   Term a     = term_new_got(at + 0);
   Term b     = term_new_got(at + 1);
   Term res   = term_new_sup_at(at + 2, s_lab, a, b);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }

test/dup_basic.hvm4

@@ -0,0 +1,4 @@
+@main =
+  !x&A = 1;
+  x₀
+//1