diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index cd909cc..99cd309 100644 --- a/compiler/lib/eval.ml +++ b/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 diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index f40d8d1..99b42d7 100644 --- a/compiler/lib/typecheck.ml +++ b/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] ---- *) diff --git a/compiler/test/test_typecheck.ml b/compiler/test/test_typecheck.ml index c7fc4cc..d448e8f 100644 --- a/compiler/test/test_typecheck.ml +++ b/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 diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 9e71d40..d190ca8 100755 --- a/scripts/check-corpus.sh +++ b/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 )