diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-09-23 02:51:31 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-09-23 02:51:31 -0300 |
| commit | 71e0bb9ffe0a049bf69296d3a6719e8956752014 (patch) | |
| tree | 760cd813aa484e5b327ecbd789adef69464d6a42 /lib | |
| parent | c16240023545677548d254eecbfef608ebb2dee6 (diff) | |
| download | RNT-71e0bb9ffe0a049bf69296d3a6719e8956752014.tar.gz RNT-71e0bb9ffe0a049bf69296d3a6719e8956752014.zip | |
generate and contains ignoring declared enumeration mode
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/kernel/EphemeralRelation.ml | 35 |
1 files changed, 31 insertions, 4 deletions
diff --git a/lib/kernel/EphemeralRelation.ml b/lib/kernel/EphemeralRelation.ml index 54454fb..3fb8e72 100644 --- a/lib/kernel/EphemeralRelation.ml +++ b/lib/kernel/EphemeralRelation.ml @@ -15,6 +15,22 @@ module type DERIVATION = sig end module Make (D : DERIVATION) = struct + module Error = struct + open Concepts.Condition + + let attributes bound = Concepts.Value.String (String.concat ", " (BatSet.String.elements bound)) + + let ungenerable bound = + condition "ungenerable-binding" + "The derivation declares no mode that generates under the attributes bound." + ("bound" |=| attributes bound) + + let undecidable bound = + condition "undecidable-membership" + "The derivation declares no mode that decides membership under the attributes of the tuple." + ("bound" |=| attributes bound) + end + let pinned_tag = "rnt/pinned/1" let identity ?pinned plan = @@ -26,11 +42,14 @@ module Make (D : DERIVATION) = struct |> Bytes.of_string |> Concepts.Hash.hash_of_bytes - let exhaustible declaration = - match Concepts.Mode.generation declaration BatSet.String.empty with + let exhaustible declaration bound = + match Concepts.Mode.generation declaration bound with | Some cardinality -> Concepts.Cardinality.exhaustible cardinality | None -> false + let decides declaration bound = + Concepts.Mode.decision declaration bound || exhaustible declaration bound + (* A cursor holds a reference to its relation, so the edges it reads outlive a release of the relation that produced it. *) class retaining scan release_owner = @@ -57,6 +76,11 @@ module Make (D : DERIVATION) = struct method private retained binding = let open Utilities.Result in + let bound = Protocols.Generative.bound binding in + let* () = + if Option.is_some (Concepts.Mode.generation declaration bound) then Ok () + else Error (Error.ungenerable bound) + in let* cursor = D.generate plan binding in match Protocols.Cursor.require cursor with | Error c -> @@ -77,7 +101,10 @@ module Make (D : DERIVATION) = struct binding the tuple itself fixes. *) method contains (tuple : Concepts.Tuple.t) = let open Utilities.Result in - let* cursor = D.generate plan tuple.Concepts.Tuple.attributes in + let binding = tuple.Concepts.Tuple.attributes in + let bound = Protocols.Generative.bound binding in + let* () = if decides declaration bound then Ok () else Error (Error.undecidable bound) in + let* cursor = D.generate plan binding in Fun.protect ~finally:(fun () -> Protocols.Handle.release cursor) (fun () -> @@ -100,6 +127,6 @@ module Make (D : DERIVATION) = struct let open Utilities.Result in let* declaration = D.modes plan in Ok - ( new ephemeral plan (identity ?pinned plan) declaration (exhaustible declaration) edges + ( new ephemeral plan (identity ?pinned plan) declaration (exhaustible declaration BatSet.String.empty) edges |> Protocols.Handle.make ) end |
