working vm: parser, admission with totality checks, solver and repl

1 files changed, 410 insertions, 0 deletions

diff --git a/lib/world.ml b/lib/world.ml
new file mode 100644
index 0000000..c3d3ef2
--- /dev/null
+++ b/lib/world.ml
@@ -0,0 +1,410 @@
+type expr =
+  | Apply of string * Pattern.t Label.Map.t
+  | And of expr * expr
+  | Or of expr * expr
+
+type rule = {
+  rule_name : string;
+  head : Pattern.t Label.Map.t;
+  body : expr;
+  witness : Label.t option;
+}
+
+type domain = D_integer | D_natural | D_rational | D_string
+
+type def =
+  | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
+  | Rules of rule list
+
+module type WORLD = sig
+  type t
+
+  val find : t -> string -> def option
+end
+
+type error =
+  | Invalid_label of string
+  | Duplicate_label of string
+  | Zero_denominator
+  | Lowercase_name of string
+  | Term_expected of string
+  | Proposition_expected of string
+  | Malformed_directive of string
+  | Unknown_domain of string
+  | Unknown_relation of string
+  | Already_defined of string
+  | Fact_not_ground of string
+  | Schema_mismatch of { relation : string; detail : string }
+  | Domain_violation of { relation : string; label : string }
+  | Non_total_rule of string
+  | Mutual_recursion of string list
+
+let pp_error fmt = function
+  | Invalid_label l -> Format.fprintf fmt "invalid label: %s" l
+  | Duplicate_label l -> Format.fprintf fmt "duplicate label: %s:" l
+  | Zero_denominator -> Format.fprintf fmt "rational literal with zero denominator"
+  | Lowercase_name n ->
+      Format.fprintf fmt "lowercase name %s cannot be a variable or relation here" n
+  | Term_expected d -> Format.fprintf fmt "a term was expected: %s" d
+  | Proposition_expected d -> Format.fprintf fmt "a proposition was expected: %s" d
+  | Malformed_directive d -> Format.fprintf fmt "malformed directive: %s" d
+  | Unknown_domain d -> Format.fprintf fmt "unknown domain: %s" d
+  | Unknown_relation r -> Format.fprintf fmt "unknown relation: %s" r
+  | Already_defined r -> Format.fprintf fmt "relation already defined: %s" r
+  | Fact_not_ground r -> Format.fprintf fmt "fact for %s is not ground" r
+  | Schema_mismatch { relation; detail } ->
+      Format.fprintf fmt "schema mismatch on %s: %s" relation detail
+  | Domain_violation { relation; label } ->
+      Format.fprintf fmt "domain violation on %s at %s:" relation label
+  | Non_total_rule name ->
+      Format.fprintf fmt
+        "rule %S rejected: no structurally decreasing argument in its recursive call"
+        name
+  | Mutual_recursion cycle ->
+      Format.fprintf fmt "mutual recursion rejected: %s"
+        (String.concat " -> " cycle)
+
+let ( let* ) = Result.bind
+
+let is_uppercase s = String.length s > 0 && s.[0] >= 'A' && s.[0] <= 'Z'
+
+let label_of_string s =
+  match Label.of_string s with
+  | Ok l -> Ok l
+  | Error (`Invalid_label l) -> Error (Invalid_label l)
+
+let bindings_to_map ~of_node bindings =
+  List.fold_left
+    (fun acc (name, node) ->
+      let* map = acc in
+      let* label = label_of_string name in
+      if Label.Map.mem label map then Error (Duplicate_label name)
+      else
+        let* value = of_node node in
+        Ok (Label.Map.add label value map))
+    (Ok Label.Map.empty) bindings
+
+(* Term position: uppercase names are variables. Blocks and
+   combinators are propositions and cannot appear here. *)
+let rec pattern_of_node (node : Ast.node) : (Pattern.t, error) result =
+  match node with
+  | Ast.Name n ->
+      if is_uppercase n then Ok (Pattern.Var n) else Error (Lowercase_name n)
+  | Ast.Int z -> Ok (Pattern.Integer z)
+  | Ast.Rat (num, den) -> (
+      match Term.rational ~num ~den with
+      | Ok t -> Ok (Pattern.of_term t)
+      | Error `Zero_denominator -> Error Zero_denominator)
+  | Ast.Str s -> Ok (Pattern.String s)
+  | Ast.Record fields ->
+      let* map = bindings_to_map ~of_node:pattern_of_node fields in
+      Ok (Pattern.Record map)
+  | Ast.Seq (items, tail) ->
+      let* tail =
+        match tail with
+        | None -> Ok Pattern.Nil
+        | Some node -> pattern_of_node node
+      in
+      List.fold_right
+        (fun item acc ->
+          let* acc = acc in
+          let* head = pattern_of_node item in
+          Ok (Pattern.cons ~head ~tail:acc))
+        items (Ok tail)
+  | Ast.Block (head, _) -> Error (Term_expected ("[" ^ head ^ " ...]"))
+  | Ast.And _ -> Error (Term_expected ":and")
+  | Ast.Or _ -> Error (Term_expected ":or")
+
+(* Proposition position: blocks apply relations, combinators
+   compose. Terms cannot appear here. *)
+let rec expr_of_node (node : Ast.node) : (expr, error) result =
+  match node with
+  | Ast.Block (head, bindings) ->
+      let* map = bindings_to_map ~of_node:pattern_of_node bindings in
+      Ok (Apply (head, map))
+  | Ast.And (a, b) ->
+      let* a = expr_of_node a in
+      let* b = expr_of_node b in
+      Ok (And (a, b))
+  | Ast.Or (a, b) ->
+      let* a = expr_of_node a in
+      let* b = expr_of_node b in
+      Ok (Or (a, b))
+  | Ast.Name n -> Error (Proposition_expected n)
+  | Ast.Int _ | Ast.Rat _ | Ast.Str _ | Ast.Record _ | Ast.Seq _ ->
+      Error (Proposition_expected "a literal")
+
+let domain_of_name = function
+  | "Integer" -> Ok D_integer
+  | "Natural" -> Ok D_natural
+  | "Rational" -> Ok D_rational
+  | "String" -> Ok D_string
+  | other -> Error (Unknown_domain other)
+
+(* Membership of a ground term in a builtin domain. Note the
+   inclusions of decision 12: a Natural is an Integer, an Integer is
+   a Rational, all literally. *)
+let member_of_domain (term : Term.t) = function
+  | D_integer -> ( match term with Term.Integer _ -> true | _ -> false)
+  | D_natural -> (
+      match term with Term.Integer z -> Z.geq z Z.zero | _ -> false)
+  | D_rational -> (
+      match term with Term.Integer _ | Term.Rational _ -> true | _ -> false)
+  | D_string -> ( match term with Term.String _ -> true | _ -> false)
+
+let rec applications = function
+  | Apply (name, bindings) -> [ (name, bindings) ]
+  | And (a, b) | Or (a, b) -> applications a @ applications b
+
+module String_map = Map.Make (String)
+
+module Standalone = struct
+  type t = def String_map.t
+
+  let find world name = String_map.find_opt name world
+
+  let schema_of_node = function
+    | Ast.Seq (entries, None) ->
+        List.fold_left
+          (fun acc entry ->
+            let* schema = acc in
+            match entry with
+            | Ast.Block (attr, [ ("domain", Ast.Name domain_name) ]) ->
+                let* label = label_of_string attr in
+                let* domain = domain_of_name domain_name in
+                Ok ((label, domain) :: schema)
+            | _ -> Error (Malformed_directive "schema entries are [attr domain: Name]"))
+          (Ok []) entries
+        |> Result.map List.rev
+    | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries")
+
+  (* The structural decrease check of decision 10, rung one. Every
+     self-recursive application must have an argument strictly
+     contained in the head's argument at the same label; that label
+     is kept as the runtime witness. *)
+  let admit_rule ~relation rule_name head body =
+    let recursive =
+      applications body |> List.filter (fun (name, _) -> String.equal name relation)
+    in
+    match recursive with
+    | [] -> Ok { rule_name; head; body; witness = None }
+    | _ ->
+        let witness_for (_, call_bindings) =
+          Label.Map.fold
+            (fun label head_arg found ->
+              match found with
+              | Some _ -> found
+              | None -> (
+                  match Label.Map.find_opt label call_bindings with
+                  | Some call_arg
+                    when Pattern.strictly_contains head_arg ~sub:call_arg ->
+                      Some label
+                  | _ -> None))
+            head None
+        in
+        let witnesses = List.map witness_for recursive in
+        if List.for_all Option.is_some witnesses then
+          (* All recursive calls decrease; any common witness works
+             at runtime, and per-call witnesses agree by label here
+             because they are all drawn from the same head. *)
+          Ok { rule_name; head; body; witness = List.nth witnesses 0 }
+        else Error (Non_total_rule rule_name)
+
+  let load statements =
+    (* First pass: declare tables, collect raw material. *)
+    let* world, raw_facts, raw_rules, raw_queries =
+      List.fold_left
+        (fun acc statement ->
+          let* world, facts, rules, queries = acc in
+          match (statement : Ast.statement) with
+          | Ast.Directive ("Relation", [ ("named", Ast.Name name); ("schema", schema) ])
+            ->
+              if String_map.mem name world then Error (Already_defined name)
+              else
+                let* schema = schema_of_node schema in
+                Ok
+                  ( String_map.add name (Table { schema; facts = [] }) world,
+                    facts,
+                    rules,
+                    queries )
+          | Ast.Directive ("Relation", _) ->
+              Error (Malformed_directive "Relation named: Name schema: #( ... )")
+          | Ast.Directive
+              ("Rule", [ ("name", Ast.Str rule_name); ("head", head); ("body", body) ])
+            ->
+              Ok (world, facts, (rule_name, head, body) :: rules, queries)
+          | Ast.Directive ("Rule", _) ->
+              Error (Malformed_directive "Rule name: \"...\" head: [...] body: ...")
+          | Ast.Directive ("Query", [ ("expression", body) ]) ->
+              Ok (world, facts, rules, body :: queries)
+          | Ast.Directive ("Query", _) ->
+              Error (Malformed_directive "Query expression: ...")
+          | Ast.Directive (name, _) -> Error (Malformed_directive name)
+          | Ast.Assert node -> Ok (world, node :: facts, rules, queries))
+        (Ok (String_map.empty, [], [], []))
+        statements
+    in
+    let raw_facts = List.rev raw_facts
+    and raw_rules = List.rev raw_rules
+    and raw_queries = List.rev raw_queries in
+    (* Second pass: compile rules, group them by head relation, admit
+       each with the totality check. *)
+    let* compiled_rules =
+      List.fold_left
+        (fun acc (rule_name, head_node, body_node) ->
+          let* grouped = acc in
+          let* head_expr = expr_of_node head_node in
+          let* relation, head =
+            match head_expr with
+            | Apply (name, bindings) -> Ok (name, bindings)
+            | _ -> Error (Malformed_directive "a rule head is a single [...] block")
+          in
+          let* body = expr_of_node body_node in
+          let* rule = admit_rule ~relation rule_name head body in
+          let existing =
+            Option.value ~default:[] (String_map.find_opt relation grouped)
+          in
+          Ok (String_map.add relation (existing @ [ rule ]) grouped))
+        (Ok String_map.empty) raw_rules
+    in
+    let* world =
+      String_map.fold
+        (fun relation rules acc ->
+          let* world = acc in
+          if String_map.mem relation world then Error (Already_defined relation)
+          else Ok (String_map.add relation (Rules rules) world))
+        compiled_rules (Ok world)
+    in
+    (* Third pass: admit facts against schemas and domains. This is
+       integrity control at loading, the same check membership always
+       is. *)
+    let* world =
+      List.fold_left
+        (fun acc node ->
+          let* world = acc in
+          let* expr = expr_of_node node in
+          let* relation, bindings =
+            match expr with
+            | Apply (name, bindings) -> Ok (name, bindings)
+            | _ -> Error (Malformed_directive "a fact is a single [...] block")
+          in
+          match String_map.find_opt relation world with
+          | Some (Table { schema; facts }) ->
+              let* tuple =
+                Label.Map.fold
+                  (fun label pattern acc ->
+                    let* tuple = acc in
+                    match Pattern.to_term pattern with
+                    | Some term -> Ok (Label.Map.add label term tuple)
+                    | None -> Error (Fact_not_ground relation))
+                  bindings (Ok Label.Map.empty)
+              in
+              let* () =
+                if
+                  List.length schema = Label.Map.cardinal tuple
+                  && List.for_all
+                       (fun (label, _) -> Label.Map.mem label tuple)
+                       schema
+                then Ok ()
+                else
+                  Error
+                    (Schema_mismatch
+                       { relation; detail = "fact labels must match the schema" })
+              in
+              let* () =
+                List.fold_left
+                  (fun acc (label, domain) ->
+                    let* () = acc in
+                    if member_of_domain (Label.Map.find label tuple) domain then Ok ()
+                    else
+                      Error
+                        (Domain_violation
+                           { relation; label = Label.to_string label }))
+                  (Ok ()) schema
+              in
+              Ok
+                (String_map.add relation
+                   (Table { schema; facts = facts @ [ tuple ] })
+                   world)
+          | Some (Rules _) ->
+              Error
+                (Schema_mismatch
+                   { relation; detail = "facts cannot be asserted on a rule-defined relation" })
+          | None -> Error (Unknown_relation relation))
+        (Ok world) raw_facts
+    in
+    (* Fourth pass: reference checking and the mutual recursion cut.
+       Self recursion is admitted with a witness; longer cycles are
+       rejected outright. *)
+    let known name =
+      Builtin.is_builtin name || String_map.mem name world
+    in
+    let check_refs body =
+      List.fold_left
+        (fun acc (name, _) ->
+          let* () = acc in
+          if known name then Ok () else Error (Unknown_relation name))
+        (Ok ()) (applications body)
+    in
+    let* () =
+      String_map.fold
+        (fun _ def acc ->
+          let* () = acc in
+          match def with
+          | Table _ -> Ok ()
+          | Rules rules ->
+              List.fold_left
+                (fun acc rule ->
+                  let* () = acc in
+                  check_refs rule.body)
+                (Ok ()) rules)
+        world (Ok ())
+    in
+    let dependencies relation =
+      match String_map.find_opt relation world with
+      | Some (Rules rules) ->
+          List.concat_map
+            (fun rule ->
+              applications rule.body
+              |> List.filter_map (fun (name, _) ->
+                     if
+                       (not (String.equal name relation))
+                       && (match String_map.find_opt name world with
+                          | Some (Rules _) -> true
+                          | _ -> false)
+                     then Some name
+                     else None))
+            rules
+      | _ -> []
+    in
+    let* () =
+      let rec visit path relation =
+        if List.mem relation path then
+          Error (Mutual_recursion (List.rev (relation :: path)))
+        else
+          List.fold_left
+            (fun acc dep ->
+              let* () = acc in
+              visit (relation :: path) dep)
+            (Ok ())
+            (dependencies relation)
+      in
+      String_map.fold
+        (fun relation def acc ->
+          let* () = acc in
+          match def with Rules _ -> visit [] relation | Table _ -> Ok ())
+        world (Ok ())
+    in
+    (* Queries compile last, against the full catalog. *)
+    let* queries =
+      List.fold_left
+        (fun acc node ->
+          let* queries = acc in
+          let* expr = expr_of_node node in
+          let* () = check_refs expr in
+          Ok (expr :: queries))
+        (Ok []) raw_queries
+      |> Result.map List.rev
+    in
+    Ok (world, queries)
+end