diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md index 1ab64a3..b6d404c 100644 --- a/ASSUMPTIONS.md +++ b/ASSUMPTIONS.md @@ -33,6 +33,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here. | A-TG-6.2 | DESIGN | Source semantics has no floating-point non-determinism (Tangle has only `Int` currently) | TG-6 | `Tangle.lean::Ty` lacks `.float` | | A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ | | A-TG-7.2 | IMPL | `braidEquiv` (`proofs/Tangle.lean`) and `braid_equiv.ml` implement Dehornoy handle reduction **correctly**, and agree with each other. Since the 2026-07-29 ruling (#50) routed `==` through them, this is **load-bearing for the semantics of `==`**: the Step relation's metatheory is proven only *relative to* `braidEquiv`, never that it decides braid-group equality. Evidenced by testing (2220 + 8 assertions), not proof. Retired by the mechanised Garside/Dehornoy proof (#51, research-grade). The Lean port is additionally **fuel-bounded**, so termination is assumed rather than proven. | TG-7 | `compiler/lib/braid_equiv.ml`; `proofs/Tangle.lean` §BRAID-GROUP EQUIVALENCE; `compiler/test/tg7` | +| A-TG-92.1 | MATH | Comparing braid words of different widths is decided in B_max(n,m) via the standard embedding Bn -> Bn+1 (adjoin a strand no generator touches). Used to justify widening `T-Eq-Word` (#92) and the match-arm width join. The embedding is standard mathematics but is **asserted in prose, not mechanised** — no Lean lemma states it. What IS machine-checked is that the metatheory (Progress/Preservation/Determinism/TypeSafety, infer_sound/complete) holds under the widened rule, and that OCaml `infer_expr` still agrees with Lean `infer` on the corpus (TG-3, 496 obligations). | TG-7 / #92 | `proofs/Tangle.lean` (`tEqWord`, `infer`); `compiler/lib/typecheck.ml` | | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` | | A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec | | A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` | diff --git a/compiler/bin/main.ml b/compiler/bin/main.ml index c0199f8..81ce622 100644 --- a/compiler/bin/main.ml +++ b/compiler/bin/main.ml @@ -49,12 +49,23 @@ let parse_file_recovering (filename : string) : Tangle.Ast.program * parse_diagn Lexing.pos_lnum = 1; }; let diagnostics = ref [] in - let stmts = ref [] in + (* Accumulate SEGMENTS (each a statement list from one parser run), newest + first, and flatten in order at the end. + The previous code did `stmts := prog @ !stmts` and then `List.rev !stmts`. + That reversal is correct for an accumulator built by prepending single + items — as `diagnostics` is — but here whole segments are prepended, so + reversing the FLATTENED list reversed the statements themselves. On the + normal path (one successful parse) every program came out backwards: + `def x; def y; def z` parsed to [z; y; x], so any program whose statements + depend on order failed at evaluation with "Unbound variable". + The test suites never caught it because they call Tangle.Parser.program + directly; only the CLI goes through this recovering path. *) + let segments = ref [] in let at_eof = ref false in while not !at_eof do (try let prog = Tangle.Parser.program Tangle.Lexer.token lexbuf in - stmts := prog @ !stmts; + segments := prog :: !segments; at_eof := true with | Tangle.Lexer.Lexer_error msg -> @@ -76,7 +87,8 @@ let parse_file_recovering (filename : string) : Tangle.Ast.program * parse_diagn } :: !diagnostics; at_eof := synchronize_tangle_lexer lexbuf) done; - (List.rev !stmts, List.rev !diagnostics) + (* Flatten oldest-segment-first, preserving order WITHIN each segment. *) + (List.concat (List.rev !segments), List.rev !diagnostics) (** Parse a TANGLE source file into a program AST. *) let parse_file (filename : string) : Tangle.Ast.program = diff --git a/compiler/lib/parser.mly b/compiler/lib/parser.mly index 969a2f9..1197d2c 100644 --- a/compiler/lib/parser.mly +++ b/compiler/lib/parser.mly @@ -90,6 +90,18 @@ definition: { { def_name = name; def_params = ps; def_body = body; def_line = $startpos(name).Lexing.pos_lnum } } | DEF name = IDENT EQ body = expr { { def_name = name; def_params = []; def_body = body; def_line = $startpos(name).Lexing.pos_lnum } } + (* Weave as a DEFINITION BODY specifically, rather than as a general + primary_expr. Admitting it into primary_expr made the grammar ambiguous: + inside a comma context such as `pair(weave ... yield strands a, b)` the + parser cannot tell whether the comma continues the strand list or + separates arguments, and menhir resolved that arbitrarily. Definition + bodies are not comma-delimited, so this position is unambiguous — and it + is the only position the construct is actually used in + (conformance/valid/v02, v08, v09, v12). *) + | DEF name = IDENT EQ w = weave_block + { { def_name = name; def_params = []; def_body = Weave w; def_line = $startpos(name).Lexing.pos_lnum } } + | DEF name = IDENT LPAREN ps = param_list RPAREN EQ w = weave_block + { { def_name = name; def_params = ps; def_body = Weave w; def_line = $startpos(name).Lexing.pos_lnum } } ; param_list: @@ -321,8 +333,6 @@ primary_expr: { e } | LBRACE e = expr RBRACE { e } - | w = weave_block - { Weave w } ; (* ---- Crossings: (a > b) or (a < b) ---- *) diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 8ed563b..32c1047 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -399,13 +399,38 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = env_bind_val g name ty) gamma bindings in infer_expr gamma' sigma arm.arm_body ) arms in - let result_ty = List.hd arm_types in - List.iteri (fun i ty -> - if ty <> result_ty then - type_error "Match arm %d has type %s but arm 0 has type %s" - i (pp_ty ty) (pp_ty result_ty) - ) arm_types; - result_ty + (* Arms must agree — but for WORDS, "agree" means agree up to width (#92), + consistent with `.` (compose) widening to max and with `==` no longer + requiring equal widths. Arms at Word[0] and Word[2] describe the same + kind of thing at different strand counts; the join is the wider. + Everything else must still match exactly. *) + let join_ty a b = + match a, b with + | TWord n, TWord m -> Some (TWord (max n m)) + | x, y when x = y -> Some x + | _ -> None + in + let result_ty = + List.fold_left (fun acc ty -> + match acc with + | None -> None + | Some a -> join_ty a ty + ) (Some (List.hd arm_types)) arm_types + in + begin match result_ty with + | Some t -> t + | None -> + (* Report against arm 0, as before, so the message stays familiar. *) + let t0 = List.hd arm_types in + let i, bad = + let rec find i = function + | [] -> (0, t0) + | ty :: rest -> if join_ty t0 ty = None then (i, ty) else find (i+1) rest + in find 0 arm_types + in + type_error "Match arm %d has type %s but arm 0 has type %s" + i (pp_ty bad) (pp_ty t0) + end (* ---- Echo types (structured loss) ---- * Mirror the HasType rules in proofs/Tangle.lean: @@ -571,9 +596,13 @@ and infer_binop (op : binop) (t1 : ty) (t2 : ty) : ty = * PROOF-NEEDS.md. *) | Eq -> begin match t1, t2 with - | TWord n, TWord m when n = m -> TBool - | TWord n, TWord m -> - type_error "Cannot compare words of differing width: Word[%d] == Word[%d]" n m + (* Widths need not agree (#92). Braid groups embed Bn -> Bn+1 by adding a + strand nothing touches, so a Word[n] IS a Word[max n m]; the comparison + is decided in the larger group. That is already what + [Braid_equiv.equiv] computes — it takes two generator lists and has no + width parameter — and it is what `~` has always accepted. Mirrors the + widened [tEqWord] in proofs/Tangle.lean. *) + | TWord _, TWord _ -> TBool | TNum, TNum -> TBool | TStr, TStr -> TBool | TBool, TBool -> TBool diff --git a/compiler/test/test_check.ml b/compiler/test/test_check.ml index 895a5ab..83a929c 100644 --- a/compiler/test/test_check.ml +++ b/compiler/test/test_check.ml @@ -43,11 +43,16 @@ let () = not (has_error (check_source "def b = true == false\n"))); Printf.printf "\n=== Type errors are reported ===\n"; - test "unequal-width word eq is rejected" (fun () -> - let ds = check_source "def bad = braid[s1] == braid[s1, s2]\n" in - has_error ds && mentions "width" ds); + (* #92: unequal-width `==` is now WELL-TYPED, so it is no longer a source of + type errors. Adding a word to a number still is. *) + test "unequal-width word eq is ACCEPTED (#92)" (fun () -> + not (has_error (check_source "def ok = braid[s1] == braid[s1, s2]\n"))); test "add of word and num is rejected" (fun () -> - has_error (check_source "def bad = braid[s1] + 3\n")); + let ds = check_source "def bad = braid[s1] + 3\n" in + (* Also check the message is the specific one, not just that something + failed — `mentions` was left unused when #92 made width mismatches + legal, and an unused assertion helper is a smell. *) + has_error ds && mentions "add" ds); Printf.printf "\n=== Parse errors are reported ===\n"; test "empty body is a parse error" (fun () -> @@ -61,11 +66,11 @@ let () = List.exists (fun d -> d.level = Error && d.line >= 1) ds); test "type error is located at the def line, not the file top" (fun () -> (* `def bad` is on line 2; the diagnostic must point there, not line 1. *) - let src = "def a = braid[s1]\ndef bad = braid[s1] == braid[s1, s2]\n" in + let src = "def a = braid[s1]\ndef bad = braid[s1] + 3\n" in let ds = check_source src in List.exists (fun d -> d.level = Error && d.line = 2) ds); test "a single type error yields exactly one diagnostic (no duplicate)" (fun () -> - let ds = check_source "def bad = braid[s1] == braid[s1, s2]\n" in + let ds = check_source "def bad = braid[s1] + 3\n" in List.length (List.filter (fun d -> d.level = Error) ds) = 1); test "format_diag is tab-separated with 4 fields" (fun () -> let line = format_diag { level = Error; line = 3; col = 5; message = "boom" } in diff --git a/compiler/test/test_typecheck.ml b/compiler/test/test_typecheck.ml index 09e7113..a78d663 100644 --- a/compiler/test/test_typecheck.ml +++ b/compiler/test/test_typecheck.ml @@ -1062,8 +1062,39 @@ let test_echo_types () = infer [] (BinOp (Eq, BraidLit [sigma 1], BraidLit [sigma 1])) = TBool); test "Eq: Bool == Bool ok (extra-core)" (fun () -> infer [] (BinOp (Eq, BoolLit true, BoolLit false)) = TBool); - test "Eq: unequal-width words rejected" (fun () -> - raises (fun () -> infer [] (BinOp (Eq, BraidLit [sigma 1], BraidLit [sigma 1; sigma 2])))) + (* #92: unequal widths are now WELL-TYPED. Bn embeds in Bn+1, the comparison + is decided in the larger group, and `Braid_equiv.equiv` has no width + parameter — it is only the typing rule that used to forbid this. *) + test "#92 Eq: unequal-width words are accepted" (fun () -> + infer [] (BinOp (Eq, BraidLit [sigma 1], BraidLit [sigma 1; sigma 2])) = TBool); + + test "#92 Eq: identity == braid is accepted (the 'is it trivial?' shape)" (fun () -> + infer [] (BinOp (Eq, Identity, BraidLit [sigma 1])) = TBool); + + test "#92 Eq: == and ~ now agree on what they accept" (fun () -> + (* They evaluate through the same Braid_equiv.equiv since TG-7; before #92 + the typechecker accepted one and rejected the other. *) + let a = BraidLit [sigma 1] and b = BraidLit [sigma 2] in + infer [] (BinOp (Eq, a, b)) = infer [] (BinOp (Isotopy, a, b))); + + test "#92 Eq: genuinely mismatched types are STILL rejected" (fun () -> + (* Widening must not become "anything compares to anything". *) + raises (fun () -> infer [] (BinOp (Eq, IntLit 1, BraidLit [sigma 1])))); + + test "#92 match arms join on width instead of failing" (fun () -> + (* turing_complete.tangle's shape: arms at Word[0] and Word[2]. *) + let arms = [ + { arm_pattern = PatIdentity; arm_body = Identity }; + { arm_pattern = PatWildcard; arm_body = BraidLit [sigma 1] }; + ] in + infer [] (Match (BraidLit [sigma 1], arms)) = TWord 2); + + test "#92 match arms of genuinely different KINDS still fail" (fun () -> + let arms = [ + { arm_pattern = PatIdentity; arm_body = IntLit 1 }; + { arm_pattern = PatWildcard; arm_body = BraidLit [sigma 1] }; + ] in + raises (fun () -> infer [] (Match (BraidLit [sigma 1], arms)))) (* ================================================================== *) (* Main: run all test groups *) diff --git a/compiler/test/tg3/tg3_emit.ml b/compiler/test/tg3/tg3_emit.ml index 1ac2ae7..f04cce9 100644 --- a/compiler/test/tg3/tg3_emit.ml +++ b/compiler/test/tg3/tg3_emit.ml @@ -357,11 +357,15 @@ let check () = pin "let shadowing inner" (Let (x, IntLit 1, Let (x, BraidLit [s 2], BinOp (Compose, Var x, Var x)))) (TWord 3); pin "nested pair fst.fst" (Fst (Fst (Pair (Pair (IntLit 1, StringLit "a"), BoolLit true)))) TNum; + (* #92: widths need not agree, so this is now WELL-TYPED rather than + rejected. It is the `identity == braid` shape the Lean step relation has + always had rules for (eqIdBraid / eqBraidId). *) + pin "eq diff-width word" (BinOp (Eq, BraidLit [s 1], Identity)) TBool; (* 3. Reject pins — these must raise Type_error. *) let rejects name e = ok name (infer_opt e = None) in rejects "add word+num" (BinOp (Add, BraidLit [], IntLit 1)); - rejects "eq diff-width word" (BinOp (Eq, BraidLit [s 1], Identity)); + rejects "eq num vs str" (BinOp (Eq, IntLit 1, StringLit "a")); rejects "lower non-echo" (Lower (IntLit 1)); rejects "fst non-prod" (Fst (IntLit 1)); diff --git a/examples/trefoil.tangle b/examples/trefoil.tangle index 01c3da4..3c97bdd 100644 --- a/examples/trefoil.tangle +++ b/examples/trefoil.tangle @@ -66,7 +66,15 @@ assert length(double_trefoil) == 6 # --- Reverse --- def reversed = reverse(trefoil) -assert reversed == braid[s1, s1, s1] + +# `reverse` reverses the word AND negates each exponent, so it yields the +# INVERSE braid: reverse(s1 s1 s1) = s1^-1 s1^-1 s1^-1. +# +# This file previously asserted `reversed == braid[s1, s1, s1]`, which is false +# — writhe(trefoil) = 3 but writhe(reversed) = -3, and writhe is invariant +# under the braid relations, so they cannot be the same element. The assertion +# had been wrong since it was written; nothing ran the examples until #89. +assert reversed == braid[s1^-1, s1^-1, s1^-1] # --- Close to form a knot --- diff --git a/proofs/TG3Differential.lean b/proofs/TG3Differential.lean index 66deb86..f1606d5 100644 --- a/proofs/TG3Differential.lean +++ b/proofs/TG3Differential.lean @@ -265,66 +265,66 @@ example : infer [] (.eq (.str "knot") (.str "ab")) = some .bool := by decide -- example : infer [] (.eq (.str "knot") (.str "knot")) = some .bool := by decide -- 250/490 example : infer [] (.eq .identity .identity) = some .bool := by decide -- 251/490 example : infer [] (.eq .identity (.braidLit [])) = some .bool := by decide -- 252/490 -example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩])) = none := by decide -- 253/490 -example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩])) = none := by decide -- 254/490 -example : infer [] (.eq .identity (.braidLit [⟨1, (-1)⟩])) = none := by decide -- 255/490 -example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide -- 256/490 -example : infer [] (.eq .identity (.braidLit [⟨2, 1⟩])) = none := by decide -- 257/490 -example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 258/490 +example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 253/490 +example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 254/490 +example : infer [] (.eq .identity (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 255/490 +example : infer [] (.eq .identity (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 256/490 +example : infer [] (.eq .identity (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 257/490 +example : infer [] (.eq .identity (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 258/490 example : infer [] (.eq (.braidLit []) .identity) = some .bool := by decide -- 259/490 example : infer [] (.eq (.braidLit []) (.braidLit [])) = some .bool := by decide -- 260/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩])) = none := by decide -- 261/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩])) = none := by decide -- 262/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = none := by decide -- 263/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide -- 264/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨2, 1⟩])) = none := by decide -- 265/490 -example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 266/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) .identity) = none := by decide -- 267/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [])) = none := by decide -- 268/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 261/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 262/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 263/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 264/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 265/490 +example : infer [] (.eq (.braidLit []) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 266/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) .identity) = some .bool := by decide -- 267/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [])) = some .bool := by decide -- 268/490 example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 269/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide -- 270/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide -- 271/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide -- 272/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide -- 273/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 274/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩]) .identity) = none := by decide -- 275/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [])) = none := by decide -- 276/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide -- 277/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 270/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 271/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 272/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 273/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 274/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩]) .identity) = some .bool := by decide -- 275/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [])) = some .bool := by decide -- 276/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 277/490 example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 278/490 example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 279/490 example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 280/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide -- 281/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 282/490 -example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) .identity) = none := by decide -- 283/490 -example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = none := by decide -- 284/490 -example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide -- 285/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 281/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 282/490 +example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) .identity) = some .bool := by decide -- 283/490 +example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [])) = some .bool := by decide -- 284/490 +example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 285/490 example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 286/490 example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 287/490 example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 288/490 -example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide -- 289/490 -example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 290/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = none := by decide -- 291/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = none := by decide -- 292/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide -- 293/490 +example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 289/490 +example : infer [] (.eq (.braidLit [⟨1, (-1)⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 290/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) .identity) = some .bool := by decide -- 291/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [])) = some .bool := by decide -- 292/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 293/490 example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 294/490 example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 295/490 example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 296/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = none := by decide -- 297/490 -example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = none := by decide -- 298/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) .identity) = none := by decide -- 299/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [])) = none := by decide -- 300/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide -- 301/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide -- 302/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide -- 303/490 -example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide -- 304/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 297/490 +example : infer [] (.eq (.braidLit [⟨0, 1⟩, ⟨1, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 298/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) .identity) = some .bool := by decide -- 299/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [])) = some .bool := by decide -- 300/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 301/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 302/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 303/490 +example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 304/490 example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 305/490 example : infer [] (.eq (.braidLit [⟨2, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 306/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = none := by decide -- 307/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = none := by decide -- 308/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = none := by decide -- 309/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = none := by decide -- 310/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = none := by decide -- 311/490 -example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = none := by decide -- 312/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) .identity) = some .bool := by decide -- 307/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [])) = some .bool := by decide -- 308/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩])) = some .bool := by decide -- 309/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩])) = some .bool := by decide -- 310/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, (-1)⟩])) = some .bool := by decide -- 311/490 +example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨0, 1⟩, ⟨1, 1⟩])) = some .bool := by decide -- 312/490 example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨2, 1⟩])) = some .bool := by decide -- 313/490 example : infer [] (.eq (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩]) (.braidLit [⟨1, 1⟩, ⟨2, (-1)⟩, ⟨0, 1⟩])) = some .bool := by decide -- 314/490 example : infer [] (.echoClose .identity) = some (.echo (.word 0) (.word 0)) := by decide -- 315/490 diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 8f7195a..2e202df 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -374,9 +374,26 @@ inductive HasType : Ctx → Expr → Ty → Prop where HasType Γ e₁ .num → HasType Γ e₂ .num → HasType Γ (.add e₁ e₂) .num - | tEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n : Nat) : -- [T-Eq-Word] + -- [T-Eq-Word]. The two operands need NOT have the same width (#92). + -- + -- Braid groups embed: Bₙ ↪ Bₙ₊₁ by adding a strand nothing touches. A word + -- on n strands IS a word on max(n,m) strands, so the comparison is asked in + -- the larger group — which is exactly what `braidEquiv` already computes: it + -- takes two generator lists and has no width parameter at all. + -- + -- Requiring n = n was inconsistent with the rest of the language: + -- * `tComposeWord` (below) already WIDENS to max n m, so a program could + -- compose two braids it was then forbidden to compare; + -- * `~` (isotopy) accepted differing widths in OCaml and, since TG-7, + -- evaluates through the SAME `braidEquiv` — identical operands and + -- identical answer, one rejected by the typechecker and one not; + -- * `eqIdBraid`/`eqBraidId` below decide "is this braid trivial?" against + -- `identity : word 0`, which under the old rule could only ever type + -- when the braid was empty. The step relation had rules for a question + -- the typing rule forbade asking. + | tEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n m : Nat) : -- [T-Eq-Word] HasType Γ e₁ (.word n) → - HasType Γ e₂ (.word n) → + HasType Γ e₂ (.word m) → HasType Γ (.eq e₁ e₂) .bool | tEqNum (Γ : Ctx) (e₁ e₂ : Expr) : -- [T-Eq-Num] HasType Γ e₁ .num → @@ -687,7 +704,7 @@ theorem weakening {Γ₁ Γ₂ : Ctx} {e : Expr} {τ σ : Ty} : cases h; rename_i h₁ h₂; simp only [shift]; exact .tAddNum _ _ _ (iha h₁) (ihb h₂) | eq a b iha ihb => cases h <;> simp only [shift] - · rename_i n h₁ h₂; exact .tEqWord _ _ _ n (iha h₁) (ihb h₂) + · rename_i n m h₁ h₂; exact .tEqWord _ _ _ n m (iha h₁) (ihb h₂) · rename_i h₁ h₂; exact .tEqNum _ _ _ (iha h₁) (ihb h₂) · rename_i h₁ h₂; exact .tEqStr _ _ _ (iha h₁) (ihb h₂) | echoClose a iha => @@ -765,7 +782,7 @@ theorem subst_preserves {Γ₁ Γ₂ : Ctx} {e s : Expr} {τ σ : Ty} : cases h; rename_i h₁ h₂; simp only [subst]; exact .tAddNum _ _ _ (iha h₁ hs) (ihb h₂ hs) | eq a b iha ihb => cases h <;> simp only [subst] - · rename_i n h₁ h₂; exact .tEqWord _ _ _ n (iha h₁ hs) (ihb h₂ hs) + · rename_i n m h₁ h₂; exact .tEqWord _ _ _ n m (iha h₁ hs) (ihb h₂ hs) · rename_i h₁ h₂; exact .tEqNum _ _ _ (iha h₁ hs) (ihb h₂ hs) · rename_i h₁ h₂; exact .tEqStr _ _ _ (iha h₁ hs) (ihb h₂ hs) | echoClose a iha => @@ -1052,21 +1069,21 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by | addNums => cases ht with | tAddNum => exact .tNum _ _ | eqLeft hs ih => cases ht with - | tEqWord _ _ _ n h₁ h₂ => exact .tEqWord _ _ _ n (ih h₁) h₂ + | tEqWord _ _ _ n m h₁ h₂ => exact .tEqWord _ _ _ n m (ih h₁) h₂ | tEqNum _ _ _ h₁ h₂ => exact .tEqNum _ _ _ (ih h₁) h₂ | tEqStr _ _ _ h₁ h₂ => exact .tEqStr _ _ _ (ih h₁) h₂ | eqRight _ hs ih => cases ht with - | tEqWord _ _ _ n h₁ h₂ => exact .tEqWord _ _ _ n h₁ (ih h₂) + | tEqWord _ _ _ n m h₁ h₂ => exact .tEqWord _ _ _ n m h₁ (ih h₂) | tEqNum _ _ _ h₁ h₂ => exact .tEqNum _ _ _ h₁ (ih h₂) | tEqStr _ _ _ h₁ h₂ => exact .tEqStr _ _ _ h₁ (ih h₂) | eqNums => cases ht with | tEqNum => exact .tBool _ _ - | tEqWord _ _ _ _ _ h₁ => cases h₁ + | tEqWord _ _ _ _ _ _ h₁ => cases h₁ | tEqStr _ _ _ _ h₁ => cases h₁ | eqStrs => cases ht with | tEqStr => exact .tBool _ _ - | tEqWord _ _ _ _ _ h₁ => cases h₁ + | tEqWord _ _ _ _ _ _ h₁ => cases h₁ | tEqNum _ _ _ _ h₁ => cases h₁ | eqBraids => cases ht with | tEqWord => exact .tBool _ _ @@ -1569,7 +1586,9 @@ def infer (Γ : Ctx) : Expr → Option Ty | _, _ => none | .eq e₁ e₂ => match infer Γ e₁, infer Γ e₂ with - | some (.word n), some (.word m) => if n = m then some .bool else none + -- Widths need not agree (#92): Bₙ ↪ Bₙ₊₁, so the comparison is decided + -- in the larger group. Mirrors the widened `tEqWord`. + | some (.word _), some (.word _) => some .bool | some .num, some .num => some .bool | some .str, some .str => some .bool | _, _ => none @@ -1658,12 +1677,11 @@ theorem infer_sound {Γ : Ctx} {e : Expr} {τ : Ty} : all_goals simp at h | eq e₁ e₂ ih₁ ih₂ => intro h; simp only [infer] at h; split at h + -- No inner `split`: with widths free (#92) there is no `if n = m` + -- condition left to case on, so the word branch is now direct. next n m he₁ he₂ => - split at h - next hnm => - injection h with h; subst h; subst hnm - exact .tEqWord _ _ _ _ (ih₁ he₁) (ih₂ he₂) - next => simp at h + injection h with h; subst h + exact .tEqWord _ _ _ n m (ih₁ he₁) (ih₂ he₂) next he₁ he₂ => injection h with h; subst h; exact .tEqNum _ _ _ (ih₁ he₁) (ih₂ he₂) next he₁ he₂ => injection h with h; subst h; exact .tEqStr _ _ _ (ih₁ he₁) (ih₂ he₂) all_goals simp at h diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 5946766..7f8dd2c 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -43,25 +43,22 @@ fi # ── MANIFEST ─────────────────────────────────────────────────────────────── # Examples that must fully TYPECHECK and EVALUATE (all their asserts hold). EXAMPLES_MUST_RUN=( - echo_pd.tangle - isotopy.tangle # the TG-7 witness — see header -) - -# Examples that PARSE but do not yet TYPECHECK. Cause is recorded per entry so -# the list cannot quietly become a dumping ground. Tracked in #88. -# braids_as_data / trefoil : recursive fn returning Num — `1 + length(rest)` -# infers the recursive call as Word[0], not Num -# compositional_pd / tensor_product : `identity == braid[...]` is a width -# mismatch (Word[0] vs Word[n]) under T-Eq-Word -# turing_complete : match arms disagree in width (Word[0] vs Word[2]) -EXAMPLES_KNOWN_UNTYPED=( braids_as_data.tangle compositional_pd.tangle + echo_pd.tangle + isotopy.tangle # the TG-7 witness — see header tensor_product.tangle trefoil.tangle turing_complete.tangle ) +# Examples that parse but do not yet typecheck. EMPTY as of #92 + the +# statement-order fix: all seven examples now typecheck AND evaluate, so they +# are all in EXAMPLES_MUST_RUN above. Keep this list empty — an entry here is +# debt, and the ratchet fails the build if a listed file starts working. +EXAMPLES_KNOWN_UNTYPED=( +) + # conformance/valid programs the parser does not yet accept. # v11 : `add{ ... }` — the Harvard DATA SUB-LANGUAGE, not a parse rule. It has # its own expression grammar, type system (Int/Float/Rational/Hex/