From c530682030e80ee2de2c263471e5eda7a3392e84 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:07:56 -0300 Subject: working vm: parser, admission with totality checks, solver and repl --- lib/ast.ml | 25 ++++ lib/builtin.ml | 193 ++++++++++++++++++++++++++ lib/builtin.mli | 29 ++++ lib/dune | 5 + lib/front.ml | 14 ++ lib/front.mli | 7 + lib/lexer.mll | 54 ++++++++ lib/parser.mly | 52 +++++++ lib/pattern.ml | 140 +++++++++++++++++++ lib/pattern.mli | 70 ++++++++++ lib/vm.ml | 156 +++++++++++++++++++++ lib/vm.mli | 37 +++++ lib/world.ml | 410 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/world.mli | 67 +++++++++ 14 files changed, 1259 insertions(+) create mode 100644 lib/ast.ml create mode 100644 lib/builtin.ml create mode 100644 lib/builtin.mli create mode 100644 lib/front.ml create mode 100644 lib/front.mli create mode 100644 lib/lexer.mll create mode 100644 lib/parser.mly create mode 100644 lib/pattern.ml create mode 100644 lib/pattern.mli create mode 100644 lib/vm.ml create mode 100644 lib/vm.mli create mode 100644 lib/world.ml create mode 100644 lib/world.mli (limited to 'lib') diff --git a/lib/ast.ml b/lib/ast.ml new file mode 100644 index 0000000..9674664 --- /dev/null +++ b/lib/ast.ml @@ -0,0 +1,25 @@ +(** Surface syntax tree. + + The parser produces one uniform node category. Atoms and + variables share a spelling in Sol and are distinguished by + context, so classification (proposition or term, relation or + variable) belongs to the loader, not the grammar. *) + +type node = + | Name of string (** identifier; variable or relation, by context *) + | Int of Z.t + | Rat of Z.t * Z.t (** one token, [1/4]; normalized at loading *) + | Str of string + | 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 ...]] *) + | And of node * node + | Or of node * node + +(** A program is a list of statements. A bare block asserts a fact; + a directive is a top-level message send such as + [Relation named: ... schema: ...], [Rule name: ... head: ... + body: ...], or [Query expression: ...]. *) +type statement = + | Directive of string * (string * node) list + | Assert of node diff --git a/lib/builtin.ml b/lib/builtin.ml new file mode 100644 index 0000000..694b688 --- /dev/null +++ b/lib/builtin.ml @@ -0,0 +1,193 @@ +type outcome = Solved of Pattern.Subst.t list | Stuck + +let forced_label name = + match Label.of_string name with Ok l -> l | Error _ -> assert false + +let value_l = forced_label "value" +let left_l = forced_label "left" +let right_l = forced_label "right" +let result_l = forced_label "result" +let lower_l = forced_label "lower" +let upper_l = forced_label "upper" + +let names = + [ + "True"; + "Integer"; + "Natural"; + "Rational"; + "String"; + "Equal"; + "Plus"; + "Times"; + "LessThan"; + "LessThanEqual"; + "GreaterThan"; + "GreaterEqual"; + "Between"; + ] + +let is_builtin name = List.mem name names + +let fail = Solved [] +let yes subst = Solved [ subst ] + +(* Numeric view: integers and rationals compute together in Q, and + results come back through Term.rational, which restores the + minimal shape. An integer-valued result is an Integer. *) +let to_q = function + | Pattern.Integer z -> Some (Q.of_bigint z) + | Pattern.Rational q -> Some q + | _ -> None + +let of_q q = + match Term.rational ~num:(Q.num q) ~den:(Q.den q) with + | Ok term -> Pattern.of_term term + | Error `Zero_denominator -> assert false + +let arg subst bindings label = + Option.map (Pattern.Subst.resolve subst) (Label.Map.find_opt label bindings) + +(* Domain membership. Unbound arguments are Stuck, never + enumerated: membership is not generation. The inclusions are the + literal ones of decision 12. *) +let domain_check subst bindings check = + match arg subst bindings value_l with + | None -> Stuck + | Some pattern -> + if Pattern.is_ground pattern then if check pattern then yes subst else fail + else Stuck + +let comparison subst bindings compare = + match (arg subst bindings left_l, arg subst bindings right_l) with + | Some left, Some right -> ( + match (to_q left, to_q right) with + | Some l, Some r -> if compare (Q.compare l r) 0 then yes subst else fail + | _ -> + if Pattern.is_ground left && Pattern.is_ground right then fail + else Stuck) + | _ -> Stuck + +(* Plus and Times solve backwards: any two ground numeric arguments + determine the third by unification. Times through zero cannot + determine the missing factor and stays Stuck rather than guess. *) +let arithmetic subst bindings ~forward ~from_result_left ~from_result_right = + let left = arg subst bindings left_l + and right = arg subst bindings right_l + and result = Label.Map.find_opt result_l bindings in + let unify_result value = + match result with + | Some pattern -> ( + match Pattern.Subst.unify subst pattern value with + | Some subst -> yes subst + | None -> fail) + | None -> yes subst + in + let solve_side binding solved = + match binding with + | Some pattern -> ( + match solved with + | Some value -> ( + match Pattern.Subst.unify subst pattern value with + | Some subst -> yes subst + | None -> fail) + | None -> Stuck) + | None -> Stuck + in + match (Option.bind left to_q, Option.bind right to_q) with + | Some l, Some r -> unify_result (of_q (forward l r)) + | Some l, None -> ( + match Option.bind result (fun p -> to_q (Pattern.Subst.resolve subst p)) with + | Some res -> + solve_side right (Option.map of_q (from_result_left res l)) + | None -> Stuck) + | None, Some r -> ( + match Option.bind result (fun p -> to_q (Pattern.Subst.resolve subst p)) with + | Some res -> + solve_side left (Option.map of_q (from_result_right res r)) + | None -> Stuck) + | None, None -> Stuck + +let between subst bindings = + let value = Label.Map.find_opt value_l bindings + and lower = arg subst bindings lower_l + and upper = arg subst bindings upper_l in + match (lower, upper) with + | Some (Pattern.Integer lo), Some (Pattern.Integer hi) -> ( + match Option.map (Pattern.Subst.resolve subst) value with + | Some (Pattern.Integer v) -> + if Z.geq v lo && Z.leq v hi then yes subst else fail + | Some (Pattern.Var _) | None -> + (* Bounded generation: the one place enumeration is + admitted, because the range is finite by construction. *) + let rec enumerate v acc = + if Z.gt v hi then List.rev acc + else + let acc = + match value with + | Some pattern -> ( + match + Pattern.Subst.unify subst pattern (Pattern.Integer v) + with + | Some subst -> subst :: acc + | None -> acc) + | None -> subst :: acc + in + enumerate (Z.succ v) acc + in + Solved (enumerate lo []) + | Some _ -> fail) + | Some p, Some q when Pattern.is_ground p && Pattern.is_ground q -> fail + | _ -> Stuck + +let run subst name bindings = + match name with + | "True" -> Some (yes subst) + | "Integer" -> + Some + (domain_check subst bindings (function + | Pattern.Integer _ -> true + | _ -> false)) + | "Natural" -> + Some + (domain_check subst bindings (function + | Pattern.Integer z -> Z.geq z Z.zero + | _ -> false)) + | "Rational" -> + Some + (domain_check subst bindings (function + | Pattern.Integer _ | Pattern.Rational _ -> true + | _ -> false)) + | "String" -> + Some + (domain_check subst bindings (function + | Pattern.String _ -> true + | _ -> false)) + | "Equal" -> ( + match + (Label.Map.find_opt left_l bindings, Label.Map.find_opt right_l bindings) + with + | Some left, Some right -> + Some + (match Pattern.Subst.unify subst left right with + | Some subst -> yes subst + | None -> fail) + | _ -> Some Stuck) + | "Plus" -> + Some + (arithmetic subst bindings ~forward:Q.add + ~from_result_left:(fun res l -> Some (Q.sub res l)) + ~from_result_right:(fun res r -> Some (Q.sub res r))) + | "Times" -> + Some + (arithmetic subst bindings ~forward:Q.mul + ~from_result_left:(fun res l -> + if Q.equal l Q.zero then None else Some (Q.div res l)) + ~from_result_right:(fun res r -> + if Q.equal r Q.zero then None else Some (Q.div res r))) + | "LessThan" -> Some (comparison subst bindings ( < )) + | "LessThanEqual" -> Some (comparison subst bindings ( <= )) + | "GreaterThan" -> Some (comparison subst bindings ( > )) + | "GreaterEqual" -> Some (comparison subst bindings ( >= )) + | "Between" -> Some (between subst bindings) + | _ -> None diff --git a/lib/builtin.mli b/lib/builtin.mli new file mode 100644 index 0000000..d7017e3 --- /dev/null +++ b/lib/builtin.mli @@ -0,0 +1,29 @@ +(** The builtin relations every world carries. + + Builtins are relations with operational capabilities beyond + scanning: they check membership against the host (the domain + relations), evaluate and solve (arithmetic), unify (equality), + and generate boundedly (Between). The VM consults this module + before the world. + + A builtin never enumerates an infinite domain. When its + arguments are too unbound to decide, the answer is {!Stuck}, and + the planner tries it again later or rejects the plan; totality + is preserved either way. *) + +type outcome = + | Solved of Pattern.Subst.t list + (** Zero or more ways to satisfy the goal. The empty list is + failure. *) + | Stuck + (** Not decidable at the current bindings; retry once more + variables are ground. *) + +val is_builtin : string -> bool +(** Whether a name is a builtin. The loader uses it for reference + checking, so user relations cannot shadow builtins. *) + +val run : Pattern.Subst.t -> string -> Pattern.t Label.Map.t -> outcome option +(** Executes one builtin goal under the substitution. [None] when + the name is not a builtin, so the VM falls through to the + world. *) diff --git a/lib/dune b/lib/dune index ca7e7b7..2d9154e 100644 --- a/lib/dune +++ b/lib/dune @@ -2,3 +2,8 @@ (name sol) (public_name sol) (libraries zarith)) + +(ocamllex lexer) + +(menhir + (modules parser)) diff --git a/lib/front.ml b/lib/front.ml new file mode 100644 index 0000000..7cacc20 --- /dev/null +++ b/lib/front.ml @@ -0,0 +1,14 @@ +let parse_string source = + let lexbuf = Lexing.from_string source in + match Parser.program Lexer.token lexbuf with + | statements -> Ok statements + | exception Lexer.Error message -> + let position = lexbuf.Lexing.lex_curr_p in + Error + (Printf.sprintf "lexical error at line %d: %s" + position.Lexing.pos_lnum message) + | exception Parser.Error -> + let position = lexbuf.Lexing.lex_curr_p in + Error + (Printf.sprintf "syntax error at line %d, before %S" + position.Lexing.pos_lnum (Lexing.lexeme lexbuf)) diff --git a/lib/front.mli b/lib/front.mli new file mode 100644 index 0000000..00fa65f --- /dev/null +++ b/lib/front.mli @@ -0,0 +1,7 @@ +(** Front door: text to statements. + + Wraps the generated lexer and parser so callers see one total + function from source text to syntax or a positioned message. + The REPL, the file runner, and the tests all enter here. *) + +val parse_string : string -> (Ast.statement list, string) result diff --git a/lib/lexer.mll b/lib/lexer.mll new file mode 100644 index 0000000..53ef04a --- /dev/null +++ b/lib/lexer.mll @@ -0,0 +1,54 @@ +{ +open Parser + +exception Error of string + +let unescape s = + let buffer = Buffer.create (String.length s) in + let rec go i = + if i < String.length s then + match s.[i] with + | '\\' when i + 1 < String.length s -> + (match s.[i + 1] with + | 'n' -> Buffer.add_char buffer '\n' + | 't' -> Buffer.add_char buffer '\t' + | c -> Buffer.add_char buffer c); + go (i + 2) + | c -> + Buffer.add_char buffer c; + go (i + 1) + in + go 0; + Buffer.contents buffer +} + +let digit = ['0'-'9'] +let ident = ['A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* +let string_body = ([^ '"' '\\'] | '\\' _)* + +rule token = parse + | [' ' '\t' '\r' '\n']+ { token lexbuf } + | '%' [^ '\n']* { token lexbuf } + | "#(" { HASH_LPAREN } + | '(' { LPAREN } + | ')' { RPAREN } + | '[' { LBRACKET } + | ']' { RBRACKET } + | '{' { LBRACE } + | '}' { RBRACE } + | '|' { BAR } + | ":and" { AND } + | ":or" { OR } + | '-'? digit+ '/' digit+ as s + { match String.index_opt s '/' with + | Some i -> + RAT + ( Z.of_string (String.sub s 0 i), + Z.of_string (String.sub s (i + 1) (String.length s - i - 1)) ) + | None -> assert false } + | '-'? digit+ as s { INT (Z.of_string s) } + | (ident as name) ':' { LABEL name } + | ident as name { NAME name } + | '"' (string_body as s) '"' { STR (unescape s) } + | eof { EOF } + | _ as c { raise (Error (Printf.sprintf "unexpected character %C" c)) } diff --git a/lib/parser.mly b/lib/parser.mly new file mode 100644 index 0000000..c85eccc --- /dev/null +++ b/lib/parser.mly @@ -0,0 +1,52 @@ +%{ +open Ast +%} + +%token INT +%token RAT +%token STR +%token NAME +%token LABEL +%token LBRACKET RBRACKET LBRACE RBRACE LPAREN RPAREN HASH_LPAREN +%token BAR AND OR EOF + +%start program + +%% + +program: + | statements = list(statement); EOF { statements } + +statement: + | head = NAME; args = nonempty_list(binding) { Directive (head, args) } + | b = block { Assert b } + +binding: + | label = LABEL; value = node { (label, value) } + +(* :or binds looser than :and; both associate to the left. The + grouping form is ordinary parentheses. *) +node: + | left = node; OR; right = conjunction { Or (left, right) } + | conj = conjunction { conj } + +conjunction: + | left = conjunction; AND; right = operand { And (left, right) } + | operand = operand { operand } + +operand: + | b = block { b } + | name = NAME { Name name } + | n = INT { Int n } + | r = RAT { Rat (fst r, snd r) } + | s = STR { Str s } + | LBRACE; fields = nonempty_list(binding); RBRACE { Record fields } + | HASH_LPAREN; items = list(operand); tail = option(seq_tail); RPAREN + { Seq (items, tail) } + | LPAREN; n = node; RPAREN { n } + +seq_tail: + | BAR; tail = operand { tail } + +block: + | LBRACKET; head = NAME; args = list(binding); RBRACKET { Block (head, args) } diff --git a/lib/pattern.ml b/lib/pattern.ml new file mode 100644 index 0000000..823162c --- /dev/null +++ b/lib/pattern.ml @@ -0,0 +1,140 @@ +type t = + | Var of string + | Integer of Z.t + | Rational of Q.t + | String of string + | Nil + | Record of t Label.Map.t + +let rec of_term (term : Term.t) = + match term with + | Term.Integer z -> Integer z + | Term.Rational q -> Rational q + | Term.String s -> String s + | Term.Nil -> Nil + | Term.Record map -> Record (Label.Map.map of_term map) + +let rec to_term = function + | Var _ -> None + | Integer z -> Some (Term.integer z) + | Rational q -> + (* Rebuilding through the smart constructor keeps canonicity a + single-point invariant. The denominator is nonzero by + construction, so this cannot fail. *) + Result.to_option (Term.rational ~num:(Q.num q) ~den:(Q.den q)) + | String s -> Some (Term.string s) + | Nil -> Some Term.nil + | Record map -> + let closed = + Label.Map.fold + (fun label pattern acc -> + match (acc, to_term pattern) with + | Some bindings, Some term -> Some ((label, term) :: bindings) + | _ -> None) + map (Some []) + in + Option.bind closed (fun bindings -> Result.to_option (Term.record bindings)) + +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 + | Record map -> Label.Map.fold (fun _ p acc -> collect acc p) map acc + in + List.rev (collect [] pattern) + +let forced_label name = + match Label.of_string name with Ok l -> l | Error _ -> assert false + +let head_label = forced_label "head" +let tail_label = forced_label "tail" + +let cons ~head ~tail = + Record Label.Map.(empty |> add head_label head |> add tail_label tail) + +let rec equal a b = + match (a, b) with + | Var x, Var y -> String.equal x y + | Integer x, Integer y -> Z.equal x y + | Rational x, Rational y -> Q.equal x y + | String x, String y -> String.equal x y + | Nil, Nil -> true + | Record x, Record y -> Label.Map.equal equal x y + | _ -> false + +let strictly_contains pattern ~sub = + let rec inside p = equal p sub || strictly p + and strictly = function + | Record map -> Label.Map.exists (fun _ p -> inside p) map + | _ -> false + in + strictly pattern + +let rec pp fmt = function + | Var v -> Format.pp_print_string fmt v + | Integer z -> Z.pp_print fmt z + | Rational q -> Q.pp_print fmt q + | String s -> Format.fprintf fmt "%S" s + | Nil -> Format.pp_print_string fmt "#()" + | Record map -> + Format.fprintf fmt "@[{"; + let first = ref true in + Label.Map.iter + (fun label p -> + if not !first then Format.fprintf fmt "@ "; + first := false; + Format.fprintf fmt "%a %a" Label.pp label pp p) + map; + Format.fprintf fmt "}@]" + +module Subst = struct + module M = Map.Make (String) + + type pattern = t + type nonrec t = pattern M.t + + let empty = M.empty + + let rec walk subst pattern = + match pattern with + | Var v -> ( + match M.find_opt v subst with + | Some bound -> walk subst bound + | None -> pattern) + | _ -> pattern + + let rec resolve subst pattern = + match walk subst pattern with + | Record map -> Record (Label.Map.map (resolve subst) map) + | other -> other + + let rec occurs subst v pattern = + match walk subst pattern with + | Var w -> String.equal v w + | Record map -> Label.Map.exists (fun _ p -> occurs subst v p) map + | _ -> false + + let rec unify subst a b = + let a = walk subst a and b = walk subst b in + match (a, b) with + | Var x, Var y when String.equal x y -> Some subst + | Var x, other | other, Var x -> + if occurs subst x other then None else Some (M.add x other subst) + | Integer x, Integer y -> if Z.equal x y then Some subst else None + | Rational x, Rational y -> if Q.equal x y then Some subst else None + | String x, String y -> if String.equal x y then Some subst else None + | Nil, Nil -> Some subst + | Record x, Record y -> + if + Label.Map.cardinal x = Label.Map.cardinal y + && Label.Map.for_all (fun label _ -> Label.Map.mem label y) x + then + Label.Map.fold + (fun label p acc -> + Option.bind acc (fun s -> unify s p (Label.Map.find label y))) + x (Some subst) + else None + | _ -> None +end diff --git a/lib/pattern.mli b/lib/pattern.mli new file mode 100644 index 0000000..5fc16c6 --- /dev/null +++ b/lib/pattern.mli @@ -0,0 +1,70 @@ +(** Open terms and unification. + + A pattern is a {!Term.t} that may contain logic variables. Goals, + rule heads, and rule bodies are made of patterns; solving a query + means finding substitutions that close them back into terms. + Unification here is the join mechanism of the whole language: + shared variables across conjoined propositions unify, and that is + what a join is. *) + +type t = + | Var of string + | Integer of Z.t + | Rational of Q.t + | String of string + | Nil + | Record of t Label.Map.t + +val of_term : Term.t -> t +(** Injects a closed term. Canonicity carries over unchanged. *) + +val to_term : t -> Term.t option +(** Closes a pattern back into a term. [None] if any variable + remains, so [Some] is proof of groundness. *) + +val is_ground : t -> bool + +val vars : t -> string list +(** Free variables, each reported once. The solver reports solutions + for exactly these. *) + +val cons : head:t -> tail:t -> t +(** One sequence cell over open terms, [{head: _ tail: _}]. The + loader elaborates [#( ... )] in rule heads and bodies with + this. *) + +val equal : t -> t -> bool +(** Syntactic equality, variables by name. Used by the totality + checker to compare head and body arguments. *) + +val strictly_contains : t -> sub:t -> bool +(** Whether [sub] occurs strictly inside the pattern, at depth one or + more. This is the structural decrease witness of the admission + checker: a recursive call is safe when its argument is strictly + contained in the head's. *) + +val pp : Format.formatter -> t -> unit + +(** Substitutions bind variables to patterns. They only grow; + unification never revokes a binding. *) +module Subst : sig + type pattern := t + type t + + val empty : t + + val walk : t -> pattern -> pattern + (** Follows variable bindings one level: the result is either a + non-variable or an unbound variable. The solver's view of "what + is this argument right now". *) + + val resolve : t -> pattern -> pattern + (** Applies the substitution everywhere, recursively. Used to read + answers out and to test groundness of arguments. *) + + val unify : t -> pattern -> pattern -> t option + (** Extends the substitution so both sides are equal, or reports + impossibility. Records unify only on identical label sets. + Runs an occurs check: Sol terms are finite, so a solution that + would need an infinite term is a failure, not a loop. *) +end diff --git a/lib/vm.ml b/lib/vm.ml new file mode 100644 index 0000000..bde087a --- /dev/null +++ b/lib/vm.ml @@ -0,0 +1,156 @@ +type error = Non_total_plan of string list + +let pp_error fmt (Non_total_plan goals) = + Format.fprintf fmt + "non-total plan rejected: no decidable goal among %s (bind more arguments or bound the search)" + (String.concat ", " goals) + +type solution = (string * Pattern.t) list + +module Make (W : World.WORLD) = struct + exception Stuck of string list + + let rec flatten = function + | World.And (a, b) -> flatten a @ flatten b + | goal -> [ goal ] + + let rec expr_vars = function + | World.Apply (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] + | World.And (a, b) | World.Or (a, b) -> expr_vars a @ expr_vars b + + let goal_name = function + | World.Apply (name, _) -> name + | World.And _ -> ":and" + | World.Or _ -> ":or" + + (* Rule variables are renamed apart at every unfolding. The suffix + character cannot be lexed, so renamed variables are unforgeable + from source text. *) + let freshen = + let counter = ref 0 in + fun rule -> + incr counter; + let stamp = "@" ^ string_of_int !counter in + let rec rename = function + | Pattern.Var v -> Pattern.Var (v ^ stamp) + | Pattern.Record map -> Pattern.Record (Label.Map.map rename map) + | ground -> ground + in + let rec rename_expr = function + | World.Apply (name, bindings) -> + World.Apply (name, Label.Map.map rename bindings) + | World.And (a, b) -> World.And (rename_expr a, rename_expr b) + | World.Or (a, b) -> World.Or (rename_expr a, rename_expr b) + in + (Label.Map.map rename rule.World.head, rename_expr rule.World.body) + + (* Unify a goal's bindings against a rule head or a stored tuple. + Goal labels absent from the head fail the branch; head labels + absent from the goal are existential. *) + let unify_bindings subst goal_bindings target_bindings = + Label.Map.fold + (fun label pattern acc -> + Option.bind acc (fun subst -> + match Label.Map.find_opt label target_bindings with + | Some target -> Pattern.Subst.unify subst pattern target + | None -> None)) + goal_bindings (Some subst) + + (* Executing one goal yields branches: an extended substitution + and the extra goals it owes (rule bodies, disjuncts). [None] + means not decidable yet. *) + let try_goal world subst goal = + match goal with + | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ] + | World.And _ -> Some [ (subst, flatten goal) ] + | World.Apply (name, bindings) -> ( + match Builtin.run subst name bindings with + | Some (Builtin.Solved substs) -> + Some (List.map (fun s -> (s, [])) substs) + | Some Builtin.Stuck -> None + | None -> ( + match W.find world name with + | Some (World.Table { facts; _ }) -> + Some + (List.filter_map + (fun tuple -> + let target = Label.Map.map Pattern.of_term tuple in + Option.map + (fun s -> (s, [])) + (unify_bindings subst bindings target)) + facts) + | Some (World.Rules rules) -> + let witness_ground rule = + match rule.World.witness with + | None -> true + | Some label -> ( + match Label.Map.find_opt label bindings with + | Some pattern -> + Pattern.is_ground (Pattern.Subst.resolve subst pattern) + | None -> false) + in + if List.for_all witness_ground rules then + Some + (List.filter_map + (fun rule -> + let head, body = freshen rule in + Option.map + (fun s -> (s, flatten body)) + (unify_bindings subst bindings head)) + rules) + else None + | None -> + (* Unreachable on admitted programs: the loader + checks references. An embedded host that lies + about its catalog surfaces here as a stuck goal + rather than a crash. *) + None)) + + let solve world expr = + let rec search subst goals = + match goals with + | [] -> [ subst ] + | _ -> ( + let rec select scanned = function + | [] -> None + | goal :: rest -> ( + match try_goal world subst goal with + | Some branches -> Some (branches, List.rev_append scanned rest) + | None -> select (goal :: scanned) rest) + in + match select [] goals with + | Some (branches, remaining) -> + List.concat_map + (fun (subst, extra) -> search subst (extra @ remaining)) + branches + | None -> raise (Stuck (List.map goal_name goals))) + in + let variables = + List.fold_left + (fun acc v -> if List.mem v acc then acc else acc @ [ v ]) + [] (expr_vars expr) + in + match search Pattern.Subst.empty (flatten expr) with + | exception Stuck goals -> Error (Non_total_plan goals) + | substs -> + let read subst = + List.map + (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v))) + variables + in + let equal_solution a b = + List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a b + in + let solutions = + List.fold_left + (fun acc subst -> + let solution = read subst in + if List.exists (equal_solution solution) acc then acc + else acc @ [ solution ]) + [] substs + in + Ok solutions +end + +module Standalone = Make (World.Standalone) diff --git a/lib/vm.mli b/lib/vm.mli new file mode 100644 index 0000000..6ce3f93 --- /dev/null +++ b/lib/vm.mli @@ -0,0 +1,37 @@ +(** The solver: proof search over an admitted world. + + Functorized over {!World.WORLD} (decision 4): the standalone + binary instantiates it with {!World.Standalone}; RNT instantiates + it with its own catalog and links the same engine in-process. + + Execution is dynamic goal selection: at each step the engine + runs any goal that is decidable at the current bindings, so + conjunction stays honestly commutative and order on the page + means nothing. A conjunction where no goal can ever run (an + unbounded membership, an unbounded recursion) is rejected as a + non-total plan, never attempted. Together with admission-time + rule checking, this is what makes every accepted query + terminate. *) + +type error = + | Non_total_plan of string list + (** No remaining goal is decidable; the relation names of the + stuck goals, for the message. *) + +val pp_error : Format.formatter -> error -> unit + +(** One answer: each free variable of the query, resolved. Ground in + the common case; open exactly when the query admits any value + there. *) +type solution = (string * Pattern.t) list + +module Make (W : World.WORLD) : sig + val solve : W.t -> World.expr -> (solution list, error) result + (** All answers to the query, duplicates collapsed. Total: the + world was admitted, so search terminates; the only failure is + a plan the engine refuses to run. *) +end + +module Standalone : sig + val solve : World.Standalone.t -> World.expr -> (solution list, error) result +end 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 diff --git a/lib/world.mli b/lib/world.mli new file mode 100644 index 0000000..76ad316 --- /dev/null +++ b/lib/world.mli @@ -0,0 +1,67 @@ +(** Worlds: the store of relations, and the loader that builds the + standalone one. + + Decision 4 of the integration document: the VM is parameterized + over a world. This module gives the module type every host + satisfies, the standalone in-memory world, and the loader that + admits a parsed program into it. Admission is where totality is + enforced: a program that gets a world is a program whose queries + terminate. *) + +(** A compiled relational expression: what rule bodies and queries + are made of after names are resolved. *) +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; + (** For a recursive rule, the label whose argument strictly + decreases. The VM requires it ground before unfolding, + which is what turns the admission proof into runtime + termination. [None] on non-recursive rules. *) +} + +(** The builtin domains a schema may constrain an attribute by. *) +type domain = D_integer | D_natural | D_rational | D_string + +(** How a relation is defined. *) +type def = + | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list } + (** Extensional: a schema and finite stored tuples. *) + | Rules of rule list (** Intensional: defined by admitted rules. *) + +(** What a host must answer for the VM to run: which relation lives + under a name. Builtins are the VM's own and are not consulted + here. *) +module type WORLD = sig + type t + + val find : t -> string -> def option +end + +type error + +val pp_error : Format.formatter -> error -> unit + +(** The standalone world: an immutable catalog loaded from program + text. This is Sol as a separate language; there are no branches, + no transitions, only the pure fragment. *) +module Standalone : sig + type t + + val find : t -> string -> def option + + val load : Ast.statement list -> (t * expr list, error) result + (** Admits a program: registers relations, checks every fact + against its schema and domains, compiles rules and queries, + and enforces totality. Rejected, not deferred: a recursive + rule without a structural decrease witness, a mutual + recursion cycle, an unknown relation, or an ill-typed fact is + an [error], and no world exists. Returns the world and the + query expressions in program order. *) +end -- cgit v1.2.3