diff options
| -rw-r--r-- | docs/language-specification.org | 26 | ||||
| -rw-r--r-- | docs/sakura-RNT-integration.org | 49 | ||||
| -rw-r--r-- | docs/states.org | 8 | ||||
| -rw-r--r-- | lib/ast.ml | 1 | ||||
| -rw-r--r-- | lib/branch.ml | 2 | ||||
| -rw-r--r-- | lib/branch.mli | 2 | ||||
| -rw-r--r-- | lib/lexer.mll | 1 | ||||
| -rw-r--r-- | lib/parser.mly | 2 | ||||
| -rw-r--r-- | lib/pattern.ml | 11 | ||||
| -rw-r--r-- | lib/pattern.mli | 1 | ||||
| -rw-r--r-- | lib/term.ml | 15 | ||||
| -rw-r--r-- | lib/term.mli | 9 | ||||
| -rw-r--r-- | lib/world.ml | 3 | ||||
| -rw-r--r-- | test/test_branch.ml | 30 | ||||
| -rw-r--r-- | test/test_term.ml | 14 |
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 @@ -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; ] ); ] |