relation references as a term kind, written #Name

15 files changed, 156 insertions, 18 deletions

diff --git a/docs/language-specification.org b/docs/language-specification.org
index 639e8d6..602d3d4 100644
--- a/docs/language-specification.org
+++ b/docs/language-specification.org
@@ -60,6 +60,7 @@ The core lexical categories are:
 - literals (ground scalars)
 - records (tuple literals)
 - sequences (list literals)
+- references (relation-denoting values, =#Name=)
 - blocks (membership propositions)
 - logical combinator messages as labels
 
@@ -227,6 +228,31 @@ sequence of propositions (e.g. a schema's fact list) also uses
 =#( ... )=: it is honestly a sequence whose elements happen to be
 blocks.
 
+** References
+
+A reference is a first-class value denoting a relation by name,
+written with the Smalltalk symbol notation:
+
+#+BEGIN_SRC sol
+#Person
+#Increment
+#+END_SRC
+
+A reference is a term, not a proposition: it names a relation as
+data, resolved through the catalog of a state. It is deliberately
+distinct from a string (a string is inert; a reference resolves) and
+from a variable (an uppercase bare name in term position stays a
+variable). Wherever a relation must appear as an argument, the
+reference is the value: transition relations
+(=[Insert relation: #Person ...]=), higher-order relations
+(=[Map relation: #Increment ...]=), and the attributes of the
+catalog relations themselves.
+
+Because a reference variable ranges over the catalog, which is
+finite, an unbound reference is boundedly enumerable: the
+higher-order restriction becomes ordinary cardinality analysis
+rather than a prohibition.
+
 ** Blocks
 
 Blocks — square brackets — delimit exactly one thing: membership
diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org
index 8207ee5..2df3892 100644
--- a/docs/sakura-RNT-integration.org
+++ b/docs/sakura-RNT-integration.org
@@ -778,6 +778,55 @@ elaboration (fresh variable plus flat conjunct). The privilege must
 be explicit and queryable, never assumed from position. Until a real
 program hurts without it, it is not built.
 
+* Decision 15: Relation References Are a Term Kind, Written #Name
+
+** The decision
+
+A relation reference is a first-class ground value denoting a
+relation by name, written with the Smalltalk symbol notation:
+
+#+BEGIN_SRC sol
+[Insert relation: #Person tuple: {name: "Ana" age: 12} before: S after: S2]
+#+END_SRC
+
+It is a new lexical kind, distinct from variables, strings, and
+propositions. A reference denotes the *catalog entry* resolved at a
+state, not an extension: two states where =Person= holds different
+tuples share the reference. Wherever a relation must appear as data,
+the reference is the value: transition arguments, higher-order
+arguments (=[Map relation: #Increment ...]=), and the attributes of
+the catalog relations themselves (decision 11).
+
+** The alternatives rejected
+
+- *Strings* (=relation: "Person"=): a conflation. The text and the
+  relation are different things with different semantics; a string
+  is inert, a reference resolves against a catalog at a state.
+  Identity is not representation (decision 12's own diagnosis).
+- *Context-resolved atoms* (=relation: Person= with the loader
+  special-casing certain argument positions): position-dependent
+  meaning of one spelling, the exact dishonesty the delimiter law
+  forbids, over an open set of special positions.
+
+** What it buys
+
+- P1 (honesty). Different semantics get a visibly different form.
+- P2 (decision 11). "You may only insert into a relation that
+  exists" stops being transition machinery and becomes an ordinary
+  foreign key into the catalog, checked at the =before:= state.
+- P3 (higher-order, grounded). A reference variable ranges over the
+  catalog, and the catalog is finite: an unbound relation variable
+  is *bounded generation*, admissible like =Between=. The
+  specification's higher-order restriction becomes ordinary
+  cardinality analysis instead of a prohibition.
+
+** Acknowledged costs
+
+- A new lexical category through the whole pipeline: token, term
+  and pattern kind, checker leaf, printing.
+- The resolution semantics (reference = name resolved through the
+  catalog of a state) must be respected by every world.
+
 * Consequences for the Pending Documents
 
 - =docs/core-design-and-pipeline.org= must treat transition relations
diff --git a/docs/states.org b/docs/states.org
index 7849918..aa5c507 100644
--- a/docs/states.org
+++ b/docs/states.org
@@ -38,16 +38,16 @@ tip, which is the elaboration rule of decision 7 for bare queries.
 =Insert= is a relation between states:
 
 #+BEGIN_SRC sol
-[Insert relation: "Person" tuple: {name: "Ana" age: 12} before: S1 after: S2]
+[Insert relation: #Person tuple: {name: "Ana" age: 12} before: S1 after: S2]
 #+END_SRC
 
 It holds when the successor of =S1= by admitting that tuple is =S2=.
 The tuple must match the relation's schema exactly and satisfy its
 domains, or there is no such transition: integrity is part of the
 relation, not a hook bolted on. Solving computes successor states
-and binds them; nothing moves. The relation name is a string for
-now, a provisional notation until relation references in term
-position get their own decision.
+and binds them; nothing moves. The relation is named by a reference,
+=#Person=, per decision 15: a dangling reference is simply no
+transition.
 
 Sequencing is the chain: =before: S1 after: S2= in one application,
 =before: S2= in the next. Conjunction stays commutative; the order
diff --git a/lib/ast.ml b/lib/ast.ml
index 61ca787..41b2346 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -10,6 +10,7 @@ type node =
   | Int of Z.t
   | Rat of Z.t * Z.t  (** one token, [1/4]; normalized at loading *)
   | Str of string
+  | Ref of string  (** [#Name], a relation reference *)
   | Record of (string * node) list  (** [{l: n ...}], source order *)
   | Seq of node list * node option  (** [#(a b)], optional [| tail] *)
   | Block of string * (string * node) list  (** [[Rel l: n ...]] *)
diff --git a/lib/branch.ml b/lib/branch.ml
index a1382c6..994653e 100644
--- a/lib/branch.ml
+++ b/lib/branch.ml
@@ -83,7 +83,7 @@ let insert world bindings =
     Option.bind (Label.Map.find_opt label bindings) Pattern.to_term
   in
   match (ground relation_l, ground tuple_l, ground before_l) with
-  | Some (Term.String relation), Some (Term.Record tuple), Some (Term.String before)
+  | Some (Term.Reference relation), Some (Term.Record tuple), Some (Term.String before)
     -> (
       match
         (String_map.find_opt relation world.schemas, Hashtbl.find_opt world.states before)
diff --git a/lib/branch.mli b/lib/branch.mli
index a60d91e..82542da 100644
--- a/lib/branch.mli
+++ b/lib/branch.mli
@@ -23,7 +23,7 @@ val find : t -> ?at:Term.t -> string -> World.def option
     REPL elaboration rule of decision 7. *)
 
 val transition : t -> string -> Pattern.t Label.Map.t -> World.transition_result option
-(** [Insert relation: "R" tuple: {...} before: S after: S']: checks
+(** [Insert relation: #R tuple: {...} before: S after: S']: checks
     the tuple against the relation's schema (integrity at the
     transition, decision 3), stores the successor state, and
     returns its digest for the VM to unify with [after:]. Stuck
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 90beacf..18dfee9 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -31,6 +31,7 @@ rule token = parse
   | [' ' '\t' '\r']+          { token lexbuf }
   | '%' [^ '\n']*             { token lexbuf }
   | "#("                      { HASH_LPAREN }
+  | '#' (ident as name)       { REFERENCE name }
   | '('                       { LPAREN }
   | ')'                       { RPAREN }
   | '['                       { LBRACKET }
diff --git a/lib/parser.mly b/lib/parser.mly
index 4bac905..ca6195e 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -7,6 +7,7 @@ open Ast
 %token <string> STR
 %token <string> NAME
 %token <string> LABEL
+%token <string> REFERENCE
 %token LBRACKET RBRACKET LBRACE RBRACE LPAREN RPAREN HASH_LPAREN
 %token BAR AND OR NOT EOF
 
@@ -41,6 +42,7 @@ operand:
   | n = INT                       { Int n }
   | r = RAT                       { Rat (fst r, snd r) }
   | s = STR                       { Str s }
+  | r = REFERENCE                 { Ref r }
   | LBRACE; fields = nonempty_list(binding); RBRACE { Record fields }
   | HASH_LPAREN; items = list(operand); tail = option(seq_tail); RPAREN
       { Seq (items, tail) }
diff --git a/lib/pattern.ml b/lib/pattern.ml
index 5186e04..9c69622 100644
--- a/lib/pattern.ml
+++ b/lib/pattern.ml
@@ -3,6 +3,7 @@ type t =
   | Integer of Z.t
   | Rational of Q.t
   | String of string
+  | Reference of string
   | Nil
   | Record of t Label.Map.t
 
@@ -11,11 +12,13 @@ let rec of_term (term : Term.t) =
   | Term.Integer z -> Integer z
   | Term.Rational q -> Rational q
   | Term.String s -> String s
+  | Term.Reference name -> Reference name
   | Term.Nil -> Nil
   | Term.Record map -> Record (Label.Map.map of_term map)
 
 let rec to_term = function
   | Var _ -> None
+  | Reference name -> Result.to_option (Term.reference name)
   | Integer z -> Some (Term.integer z)
   | Rational q ->
       (* Rebuilding through the smart constructor keeps canonicity a
@@ -40,7 +43,7 @@ let is_ground pattern = Option.is_some (to_term pattern)
 let vars pattern =
   let rec collect acc = function
     | Var v -> if List.mem v acc then acc else v :: acc
-    | Integer _ | Rational _ | String _ | Nil -> acc
+    | Integer _ | Rational _ | String _ | Reference _ | Nil -> acc
     | Record map -> Label.Map.fold (fun _ p acc -> collect acc p) map acc
   in
   List.rev (collect [] pattern)
@@ -60,6 +63,7 @@ let rec equal a b =
   | Integer x, Integer y -> Z.equal x y
   | Rational x, Rational y -> Q.equal x y
   | String x, String y -> String.equal x y
+  | Reference x, Reference y -> String.equal x y
   | Nil, Nil -> true
   | Record x, Record y -> Label.Map.equal equal x y
   | _ -> false
@@ -73,11 +77,12 @@ type checker_leaf =
   | L_int of Z.t
   | L_rat of Q.t
   | L_str of string
+  | L_ref of string
   | L_nil
 
 let checker_leaf_equal a b =
   match (a, b) with
-  | L_var x, L_var y | L_str x, L_str y -> String.equal x y
+  | L_var x, L_var y | L_str x, L_str y | L_ref x, L_ref y -> String.equal x y
   | L_int x, L_int y -> Z.equal x y
   | L_rat x, L_rat y -> Q.equal x y
   | L_nil, L_nil -> true
@@ -88,6 +93,7 @@ let rec to_checker = function
   | Integer z -> Decrease_extracted.Leaf (L_int z)
   | Rational q -> Decrease_extracted.Leaf (L_rat q)
   | String s -> Decrease_extracted.Leaf (L_str s)
+  | Reference name -> Decrease_extracted.Leaf (L_ref name)
   | Nil -> Decrease_extracted.Leaf L_nil
   | Record map ->
       Decrease_extracted.Node
@@ -105,6 +111,7 @@ let rec pp fmt = function
   | Integer z -> Z.pp_print fmt z
   | Rational q -> Q.pp_print fmt q
   | String s -> Format.fprintf fmt "%S" s
+  | Reference name -> Format.fprintf fmt "#%s" name
   | Nil -> Format.pp_print_string fmt "#()"
   | Record map ->
       Format.fprintf fmt "@[<hv 1>{";
diff --git a/lib/pattern.mli b/lib/pattern.mli
index f79dce0..f14a8e5 100644
--- a/lib/pattern.mli
+++ b/lib/pattern.mli
@@ -12,6 +12,7 @@ type t =
   | Integer of Z.t
   | Rational of Q.t
   | String of string
+  | Reference of string  (** a relation reference, [#Name] *)
   | Nil
   | Record of t Label.Map.t
 
diff --git a/lib/term.ml b/lib/term.ml
index a0dc760..fcef6f9 100644
--- a/lib/term.ml
+++ b/lib/term.ml
@@ -2,6 +2,7 @@ type t =
   | Integer of Z.t
   | Rational of Q.t
   | String of string
+  | Reference of string
   | Nil
   | Record of t Label.Map.t
 
@@ -9,6 +10,16 @@ let integer z = Integer z
 let string s = String s
 let nil = Nil
 
+let reference name =
+  let is_letter c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') in
+  let is_body c = is_letter c || (c >= '0' && c <= '9') || c = '_' in
+  if
+    String.length name > 0
+    && is_letter name.[0]
+    && String.for_all is_body name
+  then Ok (Reference name)
+  else Error (`Invalid_reference name)
+
 let rational ~num ~den =
   if Z.equal den Z.zero then Error `Zero_denominator
   else
@@ -52,6 +63,7 @@ let rec compare a b =
   | Integer x, Integer y -> Z.compare x y
   | Rational x, Rational y -> Q.compare x y
   | String x, String y -> String.compare x y
+  | Reference x, Reference y -> String.compare x y
   | Nil, Nil -> 0
   | Record x, Record y -> Label.Map.compare compare x y
   | Integer _, _ -> -1
@@ -60,6 +72,8 @@ let rec compare a b =
   | _, Rational _ -> 1
   | String _, _ -> -1
   | _, String _ -> 1
+  | Reference _, _ -> -1
+  | _, Reference _ -> 1
   | Nil, _ -> -1
   | _, Nil -> 1
 
@@ -81,6 +95,7 @@ let rec pp fmt t =
   | Integer z -> Z.pp_print fmt z
   | Rational q -> Q.pp_print fmt q
   | String s -> Format.fprintf fmt "%S" s
+  | Reference name -> Format.fprintf fmt "#%s" name
   | Nil -> Format.pp_print_string fmt "#()"
   | Record map -> (
       match as_cell t with
diff --git a/lib/term.mli b/lib/term.mli
index cf79d89..8dc201e 100644
--- a/lib/term.mli
+++ b/lib/term.mli
@@ -17,6 +17,11 @@ type t = private
           its minimal shape, so integer membership inclusion holds
           literally. *)
   | String of string
+  | Reference of string
+      (** A relation reference, written [#Name]: a first-class
+          value denoting a relation by name, resolved through the
+          catalog of a state. Distinct from {!String} on purpose;
+          identity is not representation. *)
   | Nil  (** The empty sequence, written [#()]. *)
   | Record of t Label.Map.t
       (** A nonempty labeled tuple. Attribute order is canonical
@@ -30,6 +35,10 @@ val nil : t
 (** The empty sequence, [#()]. The distinguished base every
     {!sequence} chain ends in. *)
 
+val reference : string -> (t, [ `Invalid_reference of string ]) result
+(** A relation reference. Validates the name: a letter, then
+    letters, digits, or underscores. *)
+
 val rational : num:Z.t -> den:Z.t -> (t, [ `Zero_denominator ]) result
 (** Normalizes on entry: reduces by the gcd, moves the sign to the
     numerator, and collapses to {!Integer} when the reduced
diff --git a/lib/world.ml b/lib/world.ml
index 94fa0a9..e1663c5 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -114,6 +114,7 @@ let rec pattern_of_node (node : Ast.node) : (Pattern.t, error) result =
       | Ok t -> Ok (Pattern.of_term t)
       | Error `Zero_denominator -> Error Zero_denominator)
   | Ast.Str s -> Ok (Pattern.String s)
+  | Ast.Ref name -> Ok (Pattern.Reference name)
   | Ast.Record fields ->
       let* map = bindings_to_map ~of_node:pattern_of_node fields in
       Ok (Pattern.Record map)
@@ -195,7 +196,7 @@ let rec expr_of_node (node : Ast.node) : (expr, error) result =
       let* b = expr_of_node b in
       Ok (Not (a, b))
   | Ast.Name n -> Error (Proposition_expected n)
-  | Ast.Int _ | Ast.Rat _ | Ast.Str _ | Ast.Record _ | Ast.Seq _ ->
+  | Ast.Int _ | Ast.Rat _ | Ast.Str _ | Ast.Ref _ | Ast.Record _ | Ast.Seq _ ->
       Error (Proposition_expected "a literal")
 
 let rec expr_free_vars = function
diff --git a/test/test_branch.ml b/test/test_branch.ml
index 2cfabdd..415e1c2 100644
--- a/test/test_branch.ml
+++ b/test/test_branch.ml
@@ -48,8 +48,8 @@ let test_transition_chain () =
   let world = world () in
   let source =
     Printf.sprintf
-      {| [Insert relation: "Person" tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
-         [Insert relation: "Person" tuple: {name: "Ana" age: 12} before: S1 after: S2] :and
+      {| [Insert relation: #Person tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
+         [Insert relation: #Person tuple: {name: "Ana" age: 12} before: S1 after: S2] :and
          [Person name: N age: A at: S2] |}
       (tip_digest world)
   in
@@ -59,7 +59,7 @@ let test_transition_chain () =
      visible at S1. *)
   let mid =
     Printf.sprintf
-      {| [Insert relation: "Person" tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
+      {| [Insert relation: #Person tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
          [Person name: N age: A at: S1] |}
       (tip_digest world)
   in
@@ -73,7 +73,7 @@ let test_tip_unmoved_until_commit () =
     solve world
       (compile
          (Printf.sprintf
-            {| [Insert relation: "Person" tuple: {name: "Rui" age: 70} before: %S after: S1] |}
+            {| [Insert relation: #Person tuple: {name: "Rui" age: 70} before: %S after: S1] |}
             before))
   in
   Alcotest.(check string) "solving commits nothing" before (tip_digest world)
@@ -85,7 +85,7 @@ let test_commit_and_conflict () =
     solve world
       (compile
          (Printf.sprintf
-            {| [Insert relation: "Person" tuple: {name: "Rui" age: 70} before: %S after: S1] |}
+            {| [Insert relation: #Person tuple: {name: "Rui" age: 70} before: %S after: S1] |}
             root))
   in
   let next =
@@ -110,7 +110,7 @@ let test_integrity_at_transition () =
   let world = world () in
   let source =
     Printf.sprintf
-      {| [Insert relation: "Person" tuple: {name: "Ghost" age: "old"} before: %S after: S1] |}
+      {| [Insert relation: #Person tuple: {name: "Ghost" age: "old"} before: %S after: S1] |}
       (tip_digest world)
   in
   Alcotest.(check int) "an ill-typed tuple is no transition" 0
@@ -120,13 +120,25 @@ let test_linearity_rejects_forks () =
   let world = world () in
   ignore world;
   let source =
-    {| [Insert relation: "Person" tuple: {name: "A" age: 1} before: S0 after: S1] :and
-       [Insert relation: "Person" tuple: {name: "B" age: 2} before: S0 after: S2] |}
+    {| [Insert relation: #Person tuple: {name: "A" age: 1} before: S0 after: S1] :and
+       [Insert relation: #Person tuple: {name: "B" age: 2} before: S0 after: S2] |}
   in
   match Sol.Branch.linear (compile source) with
   | Error _ -> ()
   | Ok () -> Alcotest.fail "a fork inside one expression must be rejected"
 
+let test_unknown_relation_is_no_transition () =
+  (* Decision 15: inserting into a relation absent from the catalog
+     is a dangling reference, and there is no such transition. *)
+  let world = world () in
+  let source =
+    Printf.sprintf
+      {| [Insert relation: #Ghost tuple: {name: "X" age: 1} before: %S after: S1] |}
+      (tip_digest world)
+  in
+  Alcotest.(check int) "dangling reference" 0
+    (List.length (solve world (compile source)))
+
 let test_reads_default_to_tip () =
   let world = world () in
   Alcotest.(check int) "the root tip has nobody" 0
@@ -145,6 +157,8 @@ let () =
             test_integrity_at_transition;
           Alcotest.test_case "linearity rejects forks" `Quick
             test_linearity_rejects_forks;
+          Alcotest.test_case "unknown relation is no transition" `Quick
+            test_unknown_relation_is_no_transition;
           Alcotest.test_case "reads default to tip" `Quick
             test_reads_default_to_tip;
         ] );
diff --git a/test/test_term.ml b/test/test_term.ml
index 20b2f1a..3601718 100644
--- a/test/test_term.ml
+++ b/test/test_term.ml
@@ -82,7 +82,17 @@ let test_printing () =
   Alcotest.(check string) "sequence" "#(1 2 3)"
     (print (Sol.Term.sequence [ int 1; int 2; int 3 ]));
   Alcotest.(check string) "record" "{a: 1 b: 2}"
-    (print (record [ (label "b", int 2); (label "a", int 1) ]))
+    (print (record [ (label "b", int 2); (label "a", int 1) ]));
+  Alcotest.(check string) "reference" "#Person"
+    (print (Result.get_ok (Sol.Term.reference "Person")))
+
+let test_reference_validation () =
+  Alcotest.(check bool) "well-formed" true
+    (Result.is_ok (Sol.Term.reference "Person"));
+  Alcotest.(check bool) "empty rejected" false
+    (Result.is_ok (Sol.Term.reference ""));
+  Alcotest.(check bool) "leading digit rejected" false
+    (Result.is_ok (Sol.Term.reference "1st"))
 
 let test_label_validation () =
   let ok s = Result.is_ok (Sol.Label.of_string s) in
@@ -122,5 +132,7 @@ let () =
         [
           Alcotest.test_case "printing" `Quick test_printing;
           Alcotest.test_case "label validation" `Quick test_label_validation;
+          Alcotest.test_case "reference validation" `Quick
+            test_reference_validation;
         ] );
     ]