lambda latin

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"]