fix(typecheck): implement [T-Twist-Strand] — (~a) on a named strand (#96)

compiler/lib/eval.ml

@@ -428,6 +428,18 @@ let rec eval_expr (env : env) (e : expr) : value =
        cup/cap pair.  Represented as an empty closed tangle. *)
     VTangle { tv_word = []; tv_closed = true }
 
+  (* [T-Twist-Strand]: `(~a)` on a NAMED STRAND inside a weave.  Treated as
+     structural, exactly as `Crossing` is below — weave bodies describe a
+     morphism, and the interpreter carries no strand context at runtime.
+     A single-strand twist is in any case invisible to the braid WORD: it is a
+     framing change (Reidemeister I), which the braid group does not see.
+
+     Safe to detect by "a Var the environment does not bind": the typechecker
+     runs first and accepts `Twist (Var a)` ONLY when `a` is in the strand
+     context, so a genuinely unbound variable never reaches here. *)
+  | Twist (Var a) when env_lookup env a = None ->
+    ignore a; VBraid []
+
   | Twist e1 ->
     let v = eval_expr env e1 in
     begin match v with

compiler/lib/typecheck.ml

@@ -373,11 +373,32 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
 
   (* [T-Twist-Word], [T-Twist-Tangle] (D1.18) *)
   | Twist e1 ->
-    let t = infer_expr gamma sigma e1 in
-    begin match t with
-    | TWord n        -> TWord n
-    | TTangle (a, b) -> TTangle (a, b)
-    | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t)
+    (* [T-Twist-Strand] (D1.18, spec section 3.10) must be tried FIRST:
+     *
+     *     Sigma(a) = (i, T)
+     *     ---------------------------------
+     *     Gamma; Sigma |- (~a) : Tangle[[T], [T]]
+     *
+     * `(~a)` on a NAMED STRAND inside a weave twists that strand.  Falling
+     * through to the general case would infer `a` as an ordinary expression,
+     * and the Var rule rejects strand names outright ("cannot be used as a
+     * standalone expression") — which is why conformance/valid/v09_twist.tangle
+     * never typechecked despite the spec licensing it.
+     *
+     * Exactly parallel to [T-Self-Cross] below, which types `(a > a)` the same
+     * way; the spec presents them as a pair. *)
+    begin match e1 with
+    | Var a when strand_lookup sigma a <> None ->
+      let ea = Option.get (strand_lookup sigma a) in
+      TTangle ([strand_to_type ea.strand_ty], [strand_to_type ea.strand_ty])
+    | _ ->
+      (* [T-Twist-Word] / [T-Twist-Tangle]: the standalone forms. *)
+      let t = infer_expr gamma sigma e1 in
+      begin match t with
+      | TWord n        -> TWord n
+      | TTangle (a, b) -> TTangle (a, b)
+      | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t)
+      end
     end
 
   (* ---- Crossings in weave context [T-Cross-Over], [T-Cross-Under] ---- *)

compiler/test/test_typecheck.ml

@@ -357,6 +357,31 @@ let test_isotopy () =
     infer gamma (BinOp (Isotopy, Var "t1", Var "t2")) = TBool);
 
   (* Isotopy: non-topological types -> error *)
+  (* #96 [T-Twist-Strand] (D1.18): `(~a)` on a NAMED STRAND inside a weave.
+     Specified in FORMAL-SEMANTICS section 3.10 and in spec/grammar.ebnf, but
+     infer_expr rejected any strand name used as an expression, so the
+     construct was licensed by the spec and unimplemented.  Parallel to
+     [T-Self-Cross], which the spec presents alongside it. *)
+  test "#96 T-Twist-Strand: (~a) on a strand is Tangle[[T],[T]]" (fun () ->
+    let sigma = [("a", { strand_pos = 1; strand_ty = StrandNamed "Q" })] in
+    infer_expr [] sigma (Twist (Var "a"))
+      = TTangle ([StrandNamed "Q"], [StrandNamed "Q"]));
+
+  test "#96 twist agrees with the self-crossing rule it parallels" (fun () ->
+    (* [T-Self-Cross] types (a > a) the same way; the two must not diverge. *)
+    let sigma = [("a", { strand_pos = 1; strand_ty = StrandNamed "Q" })] in
+    infer_expr [] sigma (Twist (Var "a"))
+      = infer_expr [] sigma (Crossing ("a", Over, "a")));
+
+  test "#96 standalone twist on a Word is unchanged" (fun () ->
+    (* Regression guard: [T-Twist-Word] must still apply outside a weave. *)
+    infer [] (Twist (BraidLit [sigma 1])) = TWord 2);
+
+  test "#96 twist of a non-strand, non-word is still rejected" (fun () ->
+    (* `raises` is defined in a later group; inline it here. *)
+    try let _ = infer [] (Twist (StringLit "x")) in false
+    with Type_error _ -> true);
+
   test "T-Isotopy (type error)" (fun () ->
     try
       let _ = infer [] (BinOp (Isotopy, IntLit 1, IntLit 2)) in

scripts/check-corpus.sh

@@ -75,14 +75,10 @@ CONFORMANCE_KNOWN_UNPARSED=(
 )
 
 # conformance/valid programs that PARSE but do not yet TYPECHECK+EVALUATE.
-#   v09_twist : `(~a)` — twisting a named strand inside a weave. spec/grammar.ebnf
-#               says "In weave context: (~a) twists named strand a", but
-#               infer_expr rejects any strand name used as an expression, so the
-#               construct is specified and unimplemented. Tracked in #96.
-#   v11       : does not parse at all (see above); listed here too so the eval
-#               loop does not double-report it.
+#   v11 : does not parse at all (see above); listed here too so the eval loop
+#         does not double-report it.
+# (v09_twist was listed here for [T-Twist-Strand] until #96 implemented it.)
 CONFORMANCE_KNOWN_UNRUNNABLE=(
-  v09_twist.tangle
   v11_add_block.tangle
 )