diff options
| -rw-r--r-- | lib/evaluators/Lambda.ml | 90 | ||||
| -rw-r--r-- | test/test_rnt.ml | 1 | ||||
| -rw-r--r-- | test/unit/evaluators/Lambda.ml | 142 |
3 files changed, 233 insertions, 0 deletions
diff --git a/lib/evaluators/Lambda.ml b/lib/evaluators/Lambda.ml new file mode 100644 index 0000000..7cb0248 --- /dev/null +++ b/lib/evaluators/Lambda.ml @@ -0,0 +1,90 @@ +module Error = struct + open Concepts.Condition + + let unknown_name name = + condition "unknown-name" + "A term named neither a bound variable nor a relation existing under this snapshot" + ("name" |=| Concepts.Value.String name) + let not_applicable () = + condition "not-applicable" + "A term was applied to an argument, but it denotes a relation rather than an abstraction" + empty + let unapplied_abstraction () = + condition "unapplied-abstraction" + "A program reduced to an abstraction, which names no relation to enumerate" empty + let cancelled () = + condition "evaluation-cancelled" "An evaluation was stopped before it produced its result" empty +end + +(* A dummy untyped lambda calculus where constants are relations. We + look for a name in the environment first and resolved through the + context otherwise, so the relations reachable under the snapshot + are the outer environment every program is evaluated on *) +type term = + | Name of string + | Abstract of string * term + | Apply of term * term + +module Program = Protocols.Program.Make (struct + type t = term +end) + +type value = + | Relation of Protocols.Handle.t + | Closure of string * term * environment +and environment = value BatMap.String.t + +let reduce context ~acquire term = + let open Utilities.Result in + let rec eval environment term = + match context.Protocols.Context.status () with + | `Cancelled | `Exhausted -> Error (Error.cancelled ()) + | `Live -> + match term with + | Name name -> + begin match BatMap.String.find_opt name environment with + | Some value -> Ok value + | None -> + let* found = Runtime.Context.resolve context name in + let* handle = Option.to_result ~none:(Error.unknown_name name) found in + Ok (Relation (acquire handle)) + end + | Abstract (binder, body) -> Ok (Closure (binder, body, environment)) + | Apply (operator, operand) -> + let* operator = eval environment operator in + match operator with + | Relation _ -> Error (Error.not_applicable ()) + | Closure (binder, body, closed) -> + let* argument = eval environment operand in + eval (BatMap.String.add binder argument closed) body + in + eval BatMap.String.empty term + +(* Every handle resolved during reduction is released once the result + has been enumerated and we keep a closure free to carry a relation + it did not resolve itself *) +let execute context term = + let open Utilities.Result in + let acquired = ref [] in + let acquire handle = + acquired := handle :: !acquired; + handle + in + Fun.protect + ~finally:(fun () -> List.iter Protocols.Handle.release !acquired) + (fun () -> + let* value = reduce context ~acquire term in + match value with + | Closure _ -> Error (Error.unapplied_abstraction ()) + | Relation handle -> + let* enumerable = Protocols.Enumerable.require handle in + Protocols.Enumerable.enumerate enumerable context) + +class evaluator = object (self) + inherit Kernel.Lifecycle.null + inherit Kernel.Identity.of_id + method invoke ~program context = execute context program + method protocols : Protocols.Handle.protocol list = [Program.make self] +end + +let make () = new evaluator |> Protocols.Handle.make diff --git a/test/test_rnt.ml b/test/test_rnt.ml index 784689d..d9936ea 100644 --- a/test/test_rnt.ml +++ b/test/test_rnt.ml @@ -3,6 +3,7 @@ let all_suites = @ Unit.Kernel.Merkle.suites () @ Unit.Kernel.SubstantialRelation.suites () @ Unit.Evaluators.FOL.suites () + @ Unit.Evaluators.Lambda.suites () @ Integration.Registration.suites () let () = Alcotest.run "RNT" all_suites diff --git a/test/unit/evaluators/Lambda.ml b/test/unit/evaluators/Lambda.ml new file mode 100644 index 0000000..c1098cf --- /dev/null +++ b/test/unit/evaluators/Lambda.ml @@ -0,0 +1,142 @@ +open Rnt + +module Make (S : Abstract.Storage.STORAGE) (C : Helpers.Storage.CONFIGURATOR) = struct + open Alcotest + + module H = Helpers.Storage.Make (S) (C) + module SR = Rnt.Kernel.SubstantialRelation.Make (S) + + let hash s = + Concepts.Blob.blob_of_bytes (Bytes.of_string s) |> Concepts.Hash.hash_of_blob + + let datum = + { Concepts.Tuple.type_ = "noun"; + attributes = + BatMap.String.empty + |> BatMap.String.add "lemma" (Concepts.Value.String "datum") } + + let reticulare = + { Concepts.Tuple.type_ = "verb"; + attributes = + BatMap.String.empty + |> BatMap.String.add "lemma" (Concepts.Value.String "rēticulāre") } + + let not_a_program () = + Concepts.Condition.condition "not-a-program" + "A handle was expected to carry the program protocol and did not" Concepts.Condition.empty + + (* Sets up the relations "noun" and "verb", each holding one Latin + lemma, hands [term] to the lambda evaluator, and drains the cursor + it returns. Change [term] in the cases below to play with the + calculus *) + let evaluate conn term = + let open Utilities.Result in + let* tx = S.start conn in + let singleton tuple = + let* relation = SR.empty tx ~schematics:(hash "schema") () in + SR.assert_tuple tx relation (Concepts.Tuple.Representation.to_blob tuple) + in + let* noun = singleton datum in + let* verb = singleton reticulare in + let* () = S.commit tx in + let* noun = SR.wrap conn noun in + let* verb = SR.wrap conn verb in + let root = + Kernel.Prototype.mixture + [ Kernel.Prototype.Directory.of_properties + ["noun", noun; "verb", verb; "lambda", Rnt.Evaluators.Lambda.make ()] ] + in + let context = Runtime.Context.over ~snapshot:(hash "snapshot") ~root () in + let* found = Runtime.Context.resolve context "lambda" in + let* evaluator = Option.to_result ~none:(not_a_program ()) found in + let* interpreter = + Rnt.Evaluators.Lambda.Program.from evaluator + |> Option.to_result ~none:(not_a_program ()) + in + let* cursor = Rnt.Evaluators.Lambda.Program.invoke interpreter ~program:term context in + let* scan = Protocols.Cursor.require cursor in + let* tuples = Protocols.Cursor.drain scan () in + Protocols.Handle.release cursor; + Ok (BatFingerTree.to_list tuples) + + let is lemma tuple = + Concepts.Hash.hash_equals (Concepts.Tuple.hash tuple) (Concepts.Tuple.hash lemma) + + (* A bare name resolves through the context, so the relations under + the snapshot are the outer environment *) + let a_name_is_a_relation conn = + let scanned = + evaluate conn (Rnt.Evaluators.Lambda.Name "noun") |> Helpers.condition_as_failure + in + check int "one tuple scanned" 1 (List.length scanned); + check bool "the tuple that was asserted" true (List.for_all (is datum) scanned) + + (* (\x. x) noun *) + let identity_applied_to_a_relation conn = + let open Rnt.Evaluators.Lambda in + let scanned = + evaluate conn (Apply (Abstract ("x", Name "x"), Name "noun")) + |> Helpers.condition_as_failure + in + check int "one tuple scanned" 1 (List.length scanned); + check bool "the tuple that was asserted" true (List.for_all (is datum) scanned) + + (* (\x. \y. x) noun (\z. z), so the argument that wins is the one + the closure kept *) + let a_closure_keeps_its_binding conn = + let open Rnt.Evaluators.Lambda in + let scanned = + evaluate conn + (Apply + ( Apply (Abstract ("x", Abstract ("y", Name "x")), Name "noun"), + Abstract ("z", Name "z") )) + |> Helpers.condition_as_failure + in + check int "one tuple scanned" 1 (List.length scanned); + check bool "the tuple that was asserted" true (List.for_all (is datum) scanned) + + (* The classic conditional, with no conditional in the calculus. A + boolean is the choice it makes, so [if] is application and both + branches are relations *) + let church_conditional conn = + let open Rnt.Evaluators.Lambda in + let true_ = Abstract ("then", Abstract ("else", Name "then")) in + let false_ = Abstract ("then", Abstract ("else", Name "else")) in + let if_ condition then_ else_ = Apply (Apply (condition, then_), else_) in + let declining = if_ true_ (Name "noun") (Name "verb") in + let conjugating = if_ false_ (Name "noun") (Name "verb") in + let declined = evaluate conn declining |> Helpers.condition_as_failure in + let conjugated = evaluate conn conjugating |> Helpers.condition_as_failure in + check int "one tuple on the then branch" 1 (List.length declined); + check bool "the then branch is the noun" true (List.for_all (is datum) declined); + check int "one tuple on the else branch" 1 (List.length conjugated); + check bool "the else branch is the verb" true (List.for_all (is reticulare) conjugated) + + (* A program reducing to an abstraction names nothing to + enumerate *) + let an_abstraction_is_not_a_result conn = + let open Rnt.Evaluators.Lambda in + match evaluate conn (Abstract ("x", Name "x")) with + | Error condition -> + check bool "unapplied abstraction" true + (String.starts_with ~prefix:"unapplied-abstraction" + (Concepts.Condition.to_string_hum condition)) + | Ok _ -> fail "an abstraction was enumerated" + + let suite prefix = + ( "lambda/" ^ prefix, + [ test_case "a-name-is-a-relation" `Quick + (H.with_connection a_name_is_a_relation "lambda-name"); + test_case "identity-applied-to-a-relation" `Quick + (H.with_connection identity_applied_to_a_relation "lambda-identity"); + test_case "a-closure-keeps-its-binding" `Quick + (H.with_connection a_closure_keeps_its_binding "lambda-closure"); + test_case "church-conditional" `Quick + (H.with_connection church_conditional "lambda-conditional"); + test_case "an-abstraction-is-not-a-result" `Quick + (H.with_connection an_abstraction_is_not_a_result "lambda-abstraction") ] ) +end + +module LMDB = Make (Rnt.Backend.Storage.LMDB) (Helpers.Storage.LMDB_Configurator) + +let suites () = [LMDB.suite "lmdb"] |