feat(jtv): the add{} injection island — Harvard data expressions (#94)

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

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       (** + *)

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)
 

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 =

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 }

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:

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 ")"