relation references as a term kind, written #Name

10 files changed, 42 insertions, 5 deletions

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