aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--lib/ast.ml1
-rw-r--r--lib/branch.ml2
-rw-r--r--lib/branch.mli2
-rw-r--r--lib/lexer.mll1
-rw-r--r--lib/parser.mly2
-rw-r--r--lib/pattern.ml11
-rw-r--r--lib/pattern.mli1
-rw-r--r--lib/term.ml15
-rw-r--r--lib/term.mli9
-rw-r--r--lib/world.ml3
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 05:43:11 +0000