diff --git a/compiler/bin/main.ml b/compiler/bin/main.ml index 07ccaf8..3a234ae 100644 --- a/compiler/bin/main.ml +++ b/compiler/bin/main.ml @@ -189,7 +189,18 @@ let dump_tokens (filename : string) : unit = | ECHOADD -> print_string "ECHOADD" | ECHOEQ -> print_string "ECHOEQ" | WARRANT -> print_string "WARRANT" - | EVIDENCE -> print_string "EVIDENCE"); + | EVIDENCE -> print_string "EVIDENCE" + | ADDBRACE -> print_string "ADDBRACE" + | IF -> print_string "IF" + | THEN -> print_string "THEN" + | ELSE -> print_string "ELSE" + | AMPAMP -> print_string "AMPAMP" + | BARBAR -> print_string "BARBAR" + | BANGEQ -> print_string "BANGEQ" + | LE -> print_string "LE" + | GE -> print_string "GE" + | PERCENT -> print_string "PERCENT" + | BANG -> print_string "BANG"); print_newline (); if tok <> EOF then loop () in diff --git a/compiler/lib/ast.ml b/compiler/lib/ast.ml index f887dc6..08d45d7 100644 --- a/compiler/lib/ast.ml +++ b/compiler/lib/ast.ml @@ -97,6 +97,19 @@ and expr = * proofs/Tangle.lean and epistemic-types' Warrant.agda. * NON-FACTIVE: `Evidence` is the only elimination. There is no * operation taking a warrant to the thing warranted. ---- *) + (* ---- JTV injection island (D2.1) ---- + * `add{ he }` embeds a Harvard DATA expression into TANGLE. + * + * Deliberately a SEPARATE grammar, not more TANGLE expressions: the whole + * point of the island is semantic separation. `+` in TANGLE is connect-sum + * on tangles; `+` inside add{} is arithmetic. Sharing one `expr` type would + * lose exactly the distinction the design exists to make (README-jtv.adoc, + * "Semantic Separation"). + * + * The block is total and pure by construction: no side effects, no loops, no + * assignment, guaranteed terminating (D2.1). *) + | AddBlock of hv_expr (* add{ he } *) + | Warrant of int * expr * expr (* warrant κ claim evidence (redex) *) | EpiVal of int * expr * expr (* formed warrant: standpoint, claim, token *) | Evidence of expr (* project the evidence token (ONLY elimination) *) @@ -128,6 +141,32 @@ and expr = * touches no proof obligation. *) | Weave of weave_block +(** Harvard DATA expressions — the `add{...}` island (spec section 6.2). + Separate from [expr] on purpose; see [AddBlock]. + + Implemented here: the scalar-literal fragment with the full operator + hierarchy and the conditional. NOT implemented, and NOT pretended: + rationals, complex numbers, lists and tuples (spec section 7.1); variables + resolving in the Pi environment and function calls (sections 8.2, 9.5); and + the `harvard{...}` CONTROL block (section 6.3) entirely. *) +and hv_expr = + | HvInt of int + | HvFloat of float + | HvStr of string + | HvBool of bool + | HvUn of hv_unop * hv_expr + | HvBin of hv_binop * hv_expr * hv_expr + | HvIf of hv_expr * hv_expr * hv_expr (* total: both branches required *) + +and hv_unop = + | HvNeg (* - *) + | HvNot (* ! *) + +and hv_binop = + | HvAdd | HvSub | HvMul | HvDiv | HvMod + | HvEq | HvNe | HvLt | HvLe | HvGt | HvGe + | HvAnd | HvOr + (** Binary operator tag. *) and binop = | Add (** + *) diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index 99cd309..7e167b3 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -282,6 +282,85 @@ let gens_of_value (v : value) : gen list = | VTangle tv -> tv.tv_word | _ -> eval_error "Expected a braid or tangle value, got %s" (pp_value v) +(** Harvard data VALUES — the island's own value space, kept separate from + TANGLE's [value] so the two cannot be confused. *) +type hv_value = + | HvVInt of int + | HvVFloat of float + | HvVBool of bool + | HvVStr of string + +(** Evaluate a Harvard data expression. Total by construction (D2.1): no + loops, no assignment, no side effects — every case is structural recursion + on a finite term, so this terminates. Division by zero is the one runtime + error the fragment admits. *) +let rec eval_hv (e : hv_expr) : hv_value = + let num2 f g a b = + match a, b with + | HvVInt x, HvVInt y -> HvVInt (f x y) + | HvVInt x, HvVFloat y -> HvVFloat (g (float_of_int x) y) + | HvVFloat x, HvVInt y -> HvVFloat (g x (float_of_int y)) + | HvVFloat x, HvVFloat y -> HvVFloat (g x y) + | _ -> eval_error "add{}: arithmetic on non-numbers" + in + let cmp2 f g a b = + match a, b with + | HvVInt x, HvVInt y -> HvVBool (f x y) + | HvVInt x, HvVFloat y -> HvVBool (g (float_of_int x) y) + | HvVFloat x, HvVInt y -> HvVBool (g x (float_of_int y)) + | HvVFloat x, HvVFloat y -> HvVBool (g x y) + | _ -> eval_error "add{}: comparison on non-numbers" + in + match e with + | HvInt n -> HvVInt n + | HvFloat f -> HvVFloat f + | HvStr s -> HvVStr s + | HvBool b -> HvVBool b + | HvUn (HvNeg, a) -> + (match eval_hv a with + | HvVInt n -> HvVInt (-n) | HvVFloat f -> HvVFloat (-.f) + | _ -> eval_error "add{}: negation of a non-number") + | HvUn (HvNot, a) -> + (match eval_hv a with + | HvVBool b -> HvVBool (not b) + | _ -> eval_error "add{}: ! of a non-boolean") + | HvBin (op, a, b) -> + let va = eval_hv a and vb = eval_hv b in + begin match op with + | HvAdd -> num2 ( + ) ( +. ) va vb + | HvSub -> num2 ( - ) ( -. ) va vb + | HvMul -> num2 ( * ) ( *. ) va vb + | HvDiv -> + (match va, vb with + | _, HvVInt 0 -> eval_error "add{}: division by zero" + | _, HvVFloat 0.0 -> eval_error "add{}: division by zero" + | _ -> num2 ( / ) ( /. ) va vb) + | HvMod -> + (match va, vb with + | HvVInt _, HvVInt 0 -> eval_error "add{}: modulo by zero" + | HvVInt x, HvVInt y -> HvVInt (x mod y) + | _ -> eval_error "add{}: modulo requires integers") + | HvLt -> cmp2 ( < ) ( < ) va vb + | HvLe -> cmp2 ( <= ) ( <= ) va vb + | HvGt -> cmp2 ( > ) ( > ) va vb + | HvGe -> cmp2 ( >= ) ( >= ) va vb + | HvEq -> HvVBool (va = vb) + | HvNe -> HvVBool (va <> vb) + | HvAnd -> + (match va, vb with + | HvVBool x, HvVBool y -> HvVBool (x && y) + | _ -> eval_error "add{}: && on non-booleans") + | HvOr -> + (match va, vb with + | HvVBool x, HvVBool y -> HvVBool (x || y) + | _ -> eval_error "add{}: || on non-booleans") + end + | HvIf (c, t, e2) -> + (match eval_hv c with + | HvVBool true -> eval_hv t + | HvVBool false -> eval_hv e2 + | _ -> eval_error "add{}: if condition is not a boolean") + (** Evaluate an expression in the given environment. *) let rec eval_expr (env : env) (e : expr) : value = match e with @@ -406,6 +485,16 @@ let rec eval_expr (env : env) (e : expr) : value = (* Epistemic. `warrant` forms the value; `evidence` is the sole projection and yields the TOKEN. There is deliberately no operation returning the claim — holding a warrant is not holding the fact. *) + (* The add{} island evaluates in its own world and crosses back as a TANGLE + value. Total and pure: every case terminates, nothing escapes. *) + | AddBlock he -> + begin match eval_hv he with + | HvVInt n -> VInt n + | HvVFloat f -> VFloat f + | HvVBool b -> VBool b + | HvVStr s -> VString s + end + | Warrant (k, claim, ev) -> VEpi (k, eval_expr env claim, eval_expr env ev) diff --git a/compiler/lib/jeg.ml b/compiler/lib/jeg.ml index 541936b..1296b83 100644 --- a/compiler/lib/jeg.ml +++ b/compiler/lib/jeg.ml @@ -99,6 +99,7 @@ let rec derive (gamma : env) (e : expr) : derivation = (derive gamma scrut :: List.map (fun a -> derive gamma a.arm_body) arms) | Call (f, args) -> node "T-App" gamma [f] e ty (List.map (derive gamma) args) + | AddBlock _ -> leaf "T-Add-Block" | Crossing _ -> leaf "T-Crossing" | Weave _ -> leaf "T-Weave" @@ -225,6 +226,9 @@ let rec check_node (d : derivation) : unit = | "T-Pipeline" | "T-Unary" | "T-Close" | "T-Mirror" | "T-Reverse" | "T-Simplify" | "T-Twist" | "T-Cap" | "T-Cup" | "T-Echo-Add" | "T-Echo-Eq" | "T-Let" | "T-Match" | "T-App" | "T-Crossing" | "T-Weave" -> () + (* T-Add-Block: the island has its own judgement (|-_hd), so re-deriving it + here would mean re-implementing that checker. Deferred, and listed. *) + | "T-Add-Block" -> () | r -> fail r "unknown rule name" c let check (d : derivation) : (unit, check_error list) result = diff --git a/compiler/lib/lexer.mll b/compiler/lib/lexer.mll index ac11be2..d11b9ec 100644 --- a/compiler/lib/lexer.mll +++ b/compiler/lib/lexer.mll @@ -58,6 +58,16 @@ deliberately no keyword that extracts the claim from a warrant. *) | "warrant" -> WARRANT | "evidence" -> EVIDENCE + (* JTV island (D2.1). `if`/`then`/`else` are island-only keywords — TANGLE + has no conditional of its own. + NOTE `add` is deliberately NOT here: it must stay a usable identifier + (`def add(a, b) = a + b` is valid TANGLE and appears in the e2e suite). + The island is entered by the two-character opener `add{`, lexed as a + single ADDBRACE token below — which is exactly the "Delimited Syntax" + principle in README-jtv.adoc: the delimiter is what prevents conflict. *) + | "if" -> IF + | "then" -> THEN + | "else" -> ELSE | "jones" -> JONES | "alexander" -> ALEXANDER | "homfly" -> HOMFLY @@ -100,6 +110,20 @@ rule token = parse | "=>" { ARROW } | "==" { EQEQ } | ">>" { GTGT } + (* JTV island operators. `&&`, `||`, `!=`, `<=`, `>=`, `%` and `!` appear + only inside add{...}: TANGLE has no logical operators and no inequality, + so these cannot collide with core syntax. Multi-char forms must precede + the single-char rules below. *) + (* The island opener, matched as ONE token so `add` alone stays an IDENT. + Must precede the identifier rule. *) + | "add" [' ' '\t']* '{' { ADDBRACE } + | "&&" { AMPAMP } + | "||" { BARBAR } + | "!=" { BANGEQ } + | "<=" { LE } + | ">=" { GE } + | '%' { PERCENT } + | '!' { BANG } (* Single-character operators and punctuation *) | '.' { DOT } diff --git a/compiler/lib/parser.mly b/compiler/lib/parser.mly index 66d2010..4d2bdc9 100644 --- a/compiler/lib/parser.mly +++ b/compiler/lib/parser.mly @@ -35,6 +35,8 @@ (* Echo / product forms — surface syntax mirrors pretty.ml output *) %token ECHOCLOSE LOWER RESIDUE PAIR FST SND ECHOADD ECHOEQ %token WARRANT EVIDENCE +%token ADDBRACE IF THEN ELSE +%token AMPAMP BARBAR BANGEQ LE GE PERCENT BANG (* Invariant names *) %token JONES ALEXANDER HOMFLY KAUFFMAN WRITHE LINKING @@ -302,6 +304,12 @@ unary_expr: { Warrant (k, c, ev) } | EVIDENCE LPAREN e = expr RPAREN { Evidence e } + (* ---- JTV injection island (D2.1) ---- + `add{ he }` switches to the Harvard DATA grammar entirely. The island is + delimited precisely so its operators cannot conflict with TANGLE's: + `+` here is arithmetic, `+` outside is connect-sum. *) + | ADDBRACE he = hv_expr RBRACE + { AddBlock he } | t = twist_expr { t } | MINUS e = primary_expr { UnaryOp (Neg, e) } | e = primary_expr { e } @@ -347,6 +355,66 @@ primary_expr: { e } ; +(* ================================================================== *) +(* JTV Harvard DATA grammar (spec section 6.2) *) +(* ================================================================== *) +(* A SEPARATE hierarchy from TANGLE's. Precedence, loosest to tightest: + if/then/else < || < && < comparison < + - < * / % < unary + Note `if` is total: both branches are required (D2.1). *) + +hv_expr: + | IF c = hv_expr THEN t = hv_expr ELSE e = hv_expr { HvIf (c, t, e) } + | e = hv_or { e } + ; + +hv_or: + | a = hv_or BARBAR b = hv_and { HvBin (HvOr, a, b) } + | e = hv_and { e } + ; + +hv_and: + | a = hv_and AMPAMP b = hv_cmp { HvBin (HvAnd, a, b) } + | e = hv_cmp { e } + ; + +hv_cmp: + | a = hv_sum EQEQ b = hv_sum { HvBin (HvEq, a, b) } + | a = hv_sum BANGEQ b = hv_sum { HvBin (HvNe, a, b) } + | a = hv_sum LT b = hv_sum { HvBin (HvLt, a, b) } + | a = hv_sum LE b = hv_sum { HvBin (HvLe, a, b) } + | a = hv_sum GT b = hv_sum { HvBin (HvGt, a, b) } + | a = hv_sum GE b = hv_sum { HvBin (HvGe, a, b) } + | e = hv_sum { e } + ; + +hv_sum: + | a = hv_sum PLUS b = hv_prod { HvBin (HvAdd, a, b) } + | a = hv_sum MINUS b = hv_prod { HvBin (HvSub, a, b) } + | e = hv_prod { e } + ; + +hv_prod: + | a = hv_prod STAR b = hv_unary { HvBin (HvMul, a, b) } + | a = hv_prod SLASH b = hv_unary { HvBin (HvDiv, a, b) } + | a = hv_prod PERCENT b = hv_unary { HvBin (HvMod, a, b) } + | e = hv_unary { e } + ; + +hv_unary: + | MINUS e = hv_unary { HvUn (HvNeg, e) } + | BANG e = hv_unary { HvUn (HvNot, e) } + | e = hv_atom { e } + ; + +hv_atom: + | n = INT { HvInt n } + | f = FLOAT { HvFloat f } + | s = STRING { HvStr s } + | TRUE { HvBool true } + | FALSE { HvBool false } + | LPAREN e = hv_expr RPAREN { e } + ; + (* ---- Crossings: (a > b) or (a < b) ---- *) crossing: diff --git a/compiler/lib/pretty.ml b/compiler/lib/pretty.ml index 51f4c50..3add593 100644 --- a/compiler/lib/pretty.ml +++ b/compiler/lib/pretty.ml @@ -100,6 +100,28 @@ let pp_strand_list ctx strands = pp_typed_strand ctx s ) strands +(* Harvard data expressions print fully parenthesised: the island has its own + precedence, and re-parsing must not depend on the reader sharing TANGLE's. *) +let rec pp_hv ctx = function + | HvInt n -> emit ctx (string_of_int n) + | HvFloat f -> emit ctx (Printf.sprintf "%g" f) + | HvStr s -> emit ctx (Printf.sprintf "%S" s) + | HvBool b -> emit ctx (if b then "true" else "false") + | HvUn (op, a) -> + emit ctx "("; emit ctx (match op with HvNeg -> "-" | HvNot -> "!"); + pp_hv ctx a; emit ctx ")" + | HvBin (op, a, b) -> + emit ctx "("; pp_hv ctx a; + emit ctx (match op with + | HvAdd -> " + " | HvSub -> " - " | HvMul -> " * " | HvDiv -> " / " + | HvMod -> " % " | HvEq -> " == " | HvNe -> " != " | HvLt -> " < " + | HvLe -> " <= " | HvGt -> " > " | HvGe -> " >= " + | HvAnd -> " && " | HvOr -> " || "); + pp_hv ctx b; emit ctx ")" + | HvIf (c, t, e) -> + emit ctx "(if "; pp_hv ctx c; emit ctx " then "; pp_hv ctx t; + emit ctx " else "; pp_hv ctx e; emit ctx ")" + let rec pp_expr ctx = function | Match (scrut, arms) -> emit ctx "match "; @@ -276,6 +298,9 @@ let rec pp_expr ctx = function emit ctx " yield strands "; pp_strand_list ctx w.weave_outputs + | AddBlock he -> + emit ctx "add{ "; pp_hv ctx he; emit ctx " }" + | Warrant (k, c, ev) -> emit ctx "warrant["; emit ctx (string_of_int k); emit ctx "]("; pp_expr ctx c; emit ctx ", "; pp_expr ctx ev; emit ctx ")" diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 99b42d7..846b053 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -164,6 +164,98 @@ let apply_perm (b : boundary) (gens : generator list) : boundary = (* Type inference for expressions *) (* ================================================================== *) +(* ================================================================== *) +(* Harvard data types and the |-_hd judgement (spec sections 7.1, 9.3) *) +(* ================================================================== *) + +(** Harvard DATA types (spec section 7.1). A separate type language from + TANGLE's [ty] — the island has its own judgement, written |-_hd. + + Implemented: Int, Float, Bool, String. NOT implemented and not pretended: + Rational, Hex, Binary, Symbolic (section 7.1), and the aggregate types. *) +type hv_ty = + | HvTInt + | HvTFloat + | HvTBool + | HvTStr + +let pp_hv_ty = function + | HvTInt -> "Int" | HvTFloat -> "Float" + | HvTBool -> "Bool" | HvTStr -> "String" + +(** Embed (D2.4): Harvard type -> TANGLE type, for an `add{...}` result + entering TANGLE. Spec section 7.2: + Embed(Int) = Embed(Float) = Num, Embed(Bool) = Bool, + Embed(String) = Str *) +let embed : hv_ty -> ty = function + | HvTInt | HvTFloat -> TNum + | HvTBool -> TBool + | HvTStr -> TStr + +(** The |-_hd judgement (spec section 9.3). Total and pure by construction, so + it needs no environment in this fragment: variables resolve in Pi, which is + not yet modelled. *) +let rec infer_hv (e : hv_expr) : hv_ty = + match e with + | HvInt _ -> HvTInt + | HvFloat _ -> HvTFloat + | HvStr _ -> HvTStr + | HvBool _ -> HvTBool + + | HvUn (HvNeg, a) -> + begin match infer_hv a with + | HvTInt -> HvTInt | HvTFloat -> HvTFloat + | t -> type_error "add{}: negation requires a number, got %s" (pp_hv_ty t) + end + | HvUn (HvNot, a) -> + begin match infer_hv a with + | HvTBool -> HvTBool + | t -> type_error "add{}: ! requires Bool, got %s" (pp_hv_ty t) + end + + | HvBin (op, a, b) -> + let ta = infer_hv a and tb = infer_hv b in + begin match op with + | HvAdd | HvSub | HvMul | HvDiv | HvMod -> + begin match ta, tb with + | HvTInt, HvTInt -> HvTInt + | (HvTInt | HvTFloat), (HvTInt | HvTFloat) -> HvTFloat + | _ -> type_error "add{}: arithmetic requires numbers, got %s and %s" + (pp_hv_ty ta) (pp_hv_ty tb) + end + | HvLt | HvLe | HvGt | HvGe -> + begin match ta, tb with + | (HvTInt | HvTFloat), (HvTInt | HvTFloat) -> HvTBool + | _ -> type_error "add{}: comparison requires numbers, got %s and %s" + (pp_hv_ty ta) (pp_hv_ty tb) + end + | HvEq | HvNe -> + (* Equality is homogeneous, and numeric across Int/Float. *) + begin match ta, tb with + | (HvTInt | HvTFloat), (HvTInt | HvTFloat) -> HvTBool + | x, y when x = y -> HvTBool + | _ -> type_error "add{}: cannot compare %s with %s" + (pp_hv_ty ta) (pp_hv_ty tb) + end + | HvAnd | HvOr -> + begin match ta, tb with + | HvTBool, HvTBool -> HvTBool + | _ -> type_error "add{}: logical operators require Bool, got %s and %s" + (pp_hv_ty ta) (pp_hv_ty tb) + end + end + + | HvIf (c, t, e2) -> + begin match infer_hv c with + | HvTBool -> + let tt = infer_hv t and te = infer_hv e2 in + (* TOTAL: both branches required and they must agree (D2.1). *) + if tt = te then tt + else type_error "add{}: if branches disagree — %s vs %s" + (pp_hv_ty tt) (pp_hv_ty te) + | t -> type_error "add{}: if condition must be Bool, got %s" (pp_hv_ty t) + end + (** Infer the type of an expression under environment Gamma. * Optionally takes a strand context Sigma for weave block bodies. * @@ -244,6 +336,11 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = | t -> type_error "evidence requires an Epi[k, rho, tau], got %s" (pp_ty t) end + (* [T-Add-Block] (spec section 9.1): the island's result crosses back into + TANGLE through Embed. The Harvard judgement |-_hd is used inside; the + TANGLE judgement never looks in. *) + | AddBlock he -> embed (infer_hv he) + (* ---- Variables [T-Var] ---- *) | Var name -> @@ -776,6 +873,9 @@ let rec expr_calls (f : string) (e : expr) : bool = | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1 | Evidence e1 -> go e1 | Warrant (_, c, ev) | EpiVal (_, c, ev) -> go c || go ev + (* An add{} island is closed: it cannot call a TANGLE function (Pi/section 9.5 + is not modelled), so it can never contain a recursive call. *) + | AddBlock _ -> false | Weave wb -> go wb.weave_body | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _ | StringLit _ | Var _ | Crossing _ -> false diff --git a/compiler/test/test_eval.ml b/compiler/test/test_eval.ml index 1af7e5e..6cf5ea0 100644 --- a/compiler/test/test_eval.ml +++ b/compiler/test/test_eval.ml @@ -231,6 +231,43 @@ let test_reverse () = eval (Mirror (BraidLit [sigma 1; sigma 2])) = VBraid [rgen 1 (-1); rgen 2 (-1)]); + (* ---------------------------------------------------------------- *) + (* JTV add{} island (#94). The design point is SEMANTIC SEPARATION: *) + (* `+` in TANGLE is connect-sum; `+` inside add{} is arithmetic. *) + (* ---------------------------------------------------------------- *) + + test "#94 add{}: operator precedence is the island's own" (fun () -> + eval (AddBlock (HvBin (HvAdd, HvInt 1, HvBin (HvMul, HvInt 2, HvInt 3)))) + = VInt 7); + + test "#94 add{}: conditional is total (both branches)" (fun () -> + eval (AddBlock (HvIf (HvBin (HvGt, HvInt 5, HvInt 3), HvInt 10, HvInt 20))) + = VInt 10); + + test "#94 add{}: logical operators" (fun () -> + eval (AddBlock (HvBin (HvAnd, HvBool true, + HvBin (HvOr, HvBool false, HvUn (HvNot, HvBool false))))) + = VBool true); + + test "#94 add{}: modulo" (fun () -> + eval (AddBlock (HvBin (HvMod, HvInt 7, HvInt 3))) = VInt 1); + + test "#94 add{}: int division stays integral" (fun () -> + eval (AddBlock (HvBin (HvDiv, HvInt 10, HvInt 4))) = VInt 2); + + test "#94 add{}: mixed int/float promotes" (fun () -> + eval (AddBlock (HvBin (HvAdd, HvInt 1, HvFloat 0.5))) = VFloat 1.5); + + test "#94 add{}: division by zero is caught" (fun () -> + try let _ = eval (AddBlock (HvBin (HvDiv, HvInt 1, HvInt 0))) in false + with Eval_error _ -> true); + + test "#94 add{}: Embed crosses back into TANGLE" (fun () -> + (* Int -> Num, Bool -> Bool, String -> Str (spec 7.2). *) + eval (AddBlock (HvInt 1)) = VInt 1 + && eval (AddBlock (HvBool true)) = VBool true + && eval (AddBlock (HvStr "s")) = VString "s"); + (* Reverse identity is identity *) test "Reverse identity" (fun () -> eval (Reverse Identity) = VBraid []); diff --git a/compiler/test/test_typecheck.ml b/compiler/test/test_typecheck.ml index d448e8f..dd86cdb 100644 --- a/compiler/test/test_typecheck.ml +++ b/compiler/test/test_typecheck.ml @@ -382,6 +382,24 @@ let test_isotopy () = try let _ = infer [] (Twist (StringLit "x")) in false with Type_error _ -> true); + (* #94 JTV island typing: the Harvard judgement |-_hd, then Embed. *) + test "#94 add{} embeds Int as Num" (fun () -> + infer [] (AddBlock (HvBin (HvAdd, HvInt 1, HvInt 2))) = TNum); + + test "#94 add{} embeds Bool as Bool" (fun () -> + infer [] (AddBlock (HvBool true)) = TBool); + + test "#94 add{} comparison yields Bool" (fun () -> + infer [] (AddBlock (HvBin (HvLt, HvInt 1, HvInt 2))) = TBool); + + test "#94 add{} rejects arithmetic on a Bool" (fun () -> + try let _ = infer [] (AddBlock (HvBin (HvAdd, HvBool true, HvInt 1))) in false + with Type_error _ -> true); + + test "#94 add{} rejects if-branches that disagree (totality)" (fun () -> + try let _ = infer [] (AddBlock (HvIf (HvBool true, HvInt 1, HvStr "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/compiler/test/tg3/tg3_emit.ml b/compiler/test/tg3/tg3_emit.ml index 1b4f84b..712240c 100644 --- a/compiler/test/tg3/tg3_emit.ml +++ b/compiler/test/tg3/tg3_emit.ml @@ -142,7 +142,10 @@ let rec lean_expr (scope : string list) (e : expr) : string = (* Non-core: must never appear in the corpus (close is the boundary gateway). *) | FloatLit _ | BinOp ((Sub | Mul | Div | Isotopy), _, _) | UnaryOp _ | Close _ | Mirror _ | Reverse _ | Simplify _ | Cap _ | Cup _ | Twist _ - | Match _ | Call _ | Crossing _ | Weave _ -> + (* add{} is NOT in the mechanised core: the Harvard judgement |-_hd has no + Lean image (0 occurrences in proofs/Tangle.lean), so an island must never + appear in the TG-3 corpus. *) + | Match _ | Call _ | Crossing _ | Weave _ | AddBlock _ -> failwith "TG-3: non-core constructor in corpus term" (* ================================================================== *) diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index d190ca8..00a30d3 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -61,25 +61,14 @@ 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/ -# Binary/Bool/String/Symbolic), environments (Pi), visibility rules, a -# separate typing judgement, Embed/Unembed, and bidirectional calling -# with Tangle — 288 lines of FORMAL-SEMANTICS.md across 12 sections. -# A feature, tracked separately. -# -# v02/v08/v09/v12 were here for `weave ... into ... yield ...` used as a -# DEFINITION BODY. Fixed: weave is now an expression as well as a statement. +# EMPTY as of #94 (the JTV add{} island). All 19 valid programs parse. CONFORMANCE_KNOWN_UNPARSED=( - v11_add_block.tangle ) # conformance/valid programs that PARSE but do not yet TYPECHECK+EVALUATE. -# 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.) +# EMPTY as of #94. All 19 valid programs run. Keep it empty: an entry here is +# debt, and the ratchet fails the build if a listed file starts working. CONFORMANCE_KNOWN_UNRUNNABLE=( - v11_add_block.tangle ) fail=0