diff options
| -rw-r--r-- | docs/virtual-machine-specification.org | 7 | ||||
| -rw-r--r-- | docs/vm.org | 29 | ||||
| -rw-r--r-- | lib/vm.ml | 195 | ||||
| -rw-r--r-- | test/test_vm.ml | 32 |
4 files changed, 242 insertions, 21 deletions
diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index c44b666..828bc3c 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -131,9 +131,10 @@ whole or not at all. Specified, not yet implemented; each grows admission or planning without changing admitted semantics: -- constraint propagation: residuated constraints today wait and - return; a store that actively narrows domains and detects - unsatisfiable residue early is the next strength; +- richer propagation: the interval store today reads domains and + one-sided comparisons; difference constraints between variables, + arithmetic relations, and propagation through record structure + are the next strengths; - symbolic discharge: algebraic evidence for universals over infinite domains, and arithmetic decrease measures for recursion that structural containment cannot see; diff --git a/docs/vm.org b/docs/vm.org index 87c0ca0..446cee2 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -59,14 +59,27 @@ decidable wait. So conjunction stays commutative in fact, not just in doctrine: the page order of =:and= operands never matters, and the tests assert it. -When goals remain that cannot run, two things can happen. If every -one of them is pure membership, decidable the moment its variables -ground, the answer comes back with those goals as residual -constraints: =[Integer value: X]= alone answers =X= conditioned on -=[Integer value: X]=, which is exactly what the expression means. -Constraining is not searching. If any remaining goal is a stalled -search, an unbounded recursion or an infinite universal, the plan is -rejected as non total. Membership is never generation either way. +When goals remain that cannot run, the engine first propagates over +the waiting membership constraints as one interval store. Bounds +with an empty intersection fail the branch outright: =X > 5= with +=X < 3= answers no, not a conditioned maybe, and so does asking one +value to be both an integer and a string. An integer variable +squeezed into a finite range converts to bounded generation: +=[Natural value: X] :and [LessThan left: X right: 4]= enumerates 0 +through 3, the same admissible enumeration =Between= performs +explicitly, because the combination of constraints is a finite +relation. This is Sakura's cardinality analysis working inside the +engine. + +If propagation finds neither a contradiction nor a finite range, two +things can happen. If every waiting goal is pure membership, +decidable the moment its variables ground, the answer comes back +with those goals as residual constraints: =[Integer value: X]= alone +answers =X= conditioned on =[Integer value: X]=, which is exactly +what the expression means. Constraining is not searching. If any +remaining goal is a stalled search, an unbounded recursion or an +infinite universal, the plan is rejected as non total. Membership is +never generation either way. Recursive rules unfold only when their witness argument is ground, so the admission proof becomes a runtime termination measure: the @@ -97,6 +97,145 @@ module Make (W : World.WORLD) = struct let proven solutions = List.exists (fun (_, residue) -> residue = []) solutions + (* Interval propagation over waiting membership constraints. What + residuation returns inert, this looks at together: bounds with + an empty intersection fail the branch outright, and an integer + variable squeezed into a finite range converts to bounded + generation, the same admissible enumeration Between performs + explicitly. Sakura's cardinality analysis, inside the engine. *) + module Propagate = struct + 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" + + type bound = { value : Q.t; strict : bool } + + type info = { + integer : bool; + stringy : bool; + lower : bound option; + upper : bound option; + } + + let no_info = { integer = false; stringy = false; lower = None; upper = None } + + module M = Map.Make (String) + + let note var f store = + M.update var + (fun info -> Some (f (Option.value ~default:no_info info))) + store + + let stronger_lower a b = + if Q.gt a.value b.value then a + else if Q.lt a.value b.value then b + else { a with strict = a.strict || b.strict } + + let stronger_upper a b = + if Q.lt a.value b.value then a + else if Q.gt a.value b.value then b + else { a with strict = a.strict || b.strict } + + let add_lower bound info = + { + info with + lower = + Some + (match info.lower with + | None -> bound + | Some existing -> stronger_lower bound existing); + } + + let add_upper bound info = + { + info with + upper = + Some + (match info.upper with + | None -> bound + | Some existing -> stronger_upper bound existing); + } + + let numeric_value = function + | Pattern.Integer z -> Some (Q.of_bigint z) + | Pattern.Rational q -> Some q + | _ -> None + + (* Read one waiting builtin goal into the store. Bindings arrive + already resolved, so a variable here is genuinely unbound. *) + let gather store (name, bindings) = + let value = Label.Map.find_opt value_l bindings + and left = Label.Map.find_opt left_l bindings + and right = Label.Map.find_opt right_l bindings in + match (name, value, left, right) with + | ("Integer" | "Natural"), Some (Pattern.Var x), _, _ -> + let store = note x (fun i -> { i with integer = true }) store in + if String.equal name "Natural" then + note x (add_lower { value = Q.zero; strict = false }) store + else store + | "String", Some (Pattern.Var x), _, _ -> + note x (fun i -> { i with stringy = true }) store + | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"), + _, + Some left, + Some right ) -> ( + let strict = + String.equal name "LessThan" || String.equal name "GreaterThan" + in + let less = String.equal name "LessThan" || String.equal name "LessThanEqual" in + match (left, right) with + | Pattern.Var x, ground when Option.is_some (numeric_value ground) -> + let bound = { value = Option.get (numeric_value ground); strict } in + note x (if less then add_upper bound else add_lower bound) store + | ground, Pattern.Var x when Option.is_some (numeric_value ground) -> + let bound = { value = Option.get (numeric_value ground); strict } in + note x (if less then add_lower bound else add_upper bound) store + | _ -> store) + | _ -> store + + (* Integer endpoints of a rational interval. *) + let lower_int { value; strict } = + let n = Q.num value and d = Q.den value in + if strict then Z.add (Z.fdiv n d) Z.one else Z.cdiv n d + + let upper_int { value; strict } = + let n = Q.num value and d = Q.den value in + if strict then Z.sub (Z.cdiv n d) Z.one else Z.fdiv n d + + type verdict = Fail | Enumerate of string * Z.t * Z.t | Unknown + + let analyze constraints = + let store = List.fold_left gather M.empty constraints in + let contradictory _ info = + (info.stringy && (info.integer || info.lower <> None || info.upper <> None)) + || + match (info.lower, info.upper) with + | Some lo, Some hi -> + Q.gt lo.value hi.value + || (Q.equal lo.value hi.value && (lo.strict || hi.strict)) + || (info.integer && Z.gt (lower_int lo) (upper_int hi)) + | _ -> false + in + if M.exists contradictory store then Fail + else + match + M.choose_opt + (M.filter + (fun _ info -> + info.integer && info.lower <> None && info.upper <> None) + store) + with + | Some (var, info) -> + Enumerate + ( var, + lower_int (Option.get info.lower), + upper_int (Option.get info.upper) ) + | None -> Unknown + end + let rec try_goal world subst goal = match goal with | Negated denial -> @@ -200,16 +339,52 @@ module Make (W : World.WORLD) = struct List.concat_map (fun (subst, extra) -> search world subst (extra @ remaining)) branches - | None -> - if - List.for_all - (fun goal -> - match try_goal world subst goal with - | Wait { residuatable } -> residuatable - | Run _ -> false) - goals - then [ (subst, goals) ] - else raise (Stuck (List.map goal_name goals))) + | None -> ( + (* Everything waits. Propagate over the waiting + membership constraints before residuating or + rejecting: they may be jointly unsatisfiable, or may + pin a variable into a finite range that unblocks the + rest. *) + let attempts = List.map (fun g -> (g, try_goal world subst g)) goals in + let membership = + List.filter_map + (fun (goal, attempt) -> + match (goal, attempt) with + | ( Positive (World.Apply (name, bindings)), + Wait { residuatable = true } ) -> + Some + ( name, + Label.Map.map (Pattern.Subst.resolve subst) bindings ) + | _ -> None) + attempts + in + match Propagate.analyze membership with + | Propagate.Fail -> [] + | Propagate.Enumerate (var, lo, hi) -> + let rec enumerate v acc = + if Z.gt v hi then acc + else + let branch = + match + Pattern.Subst.unify subst (Pattern.Var var) + (Pattern.Integer v) + with + | Some subst -> search world subst goals + | None -> [] + in + enumerate (Z.succ v) (acc @ branch) + in + enumerate lo [] + | Propagate.Unknown -> + if + List.for_all + (fun (_, attempt) -> + match attempt with + | Wait { residuatable } -> residuatable + | Run _ -> false) + attempts + then [ (subst, goals) ] + else raise (Stuck (List.map goal_name goals)))) (* Solution variables: the free variables of the query. Whatever occurs only under a universal is bound per quantifier solution diff --git a/test/test_vm.ml b/test/test_vm.ml index ad58720..f3d8484 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -278,6 +278,27 @@ let test_exists () = ^ {| Query expression: [Exists variable: P quantifier: [Person name: P age: B] body: [GreaterThan left: B right: 60]] |}) "B=70" +(* Constraint propagation over residue. *) + +let test_contradictory_residue_fails () = + check_answers "an empty interval is no, not a conditioned answer" + {| Query expression: [GreaterThan left: X right: 5] :and [LessThan left: X right: 3] |} + "" + +let test_kind_conflict_fails () = + check_answers "no value is both an integer and a string" + {| Query expression: [Integer value: X] :and [String value: X] |} "" + +let test_finite_narrowing_enumerates () = + check_answers "a pinned natural enumerates like Between" + {| Query expression: [Natural value: X] :and [LessThan left: X right: 4] |} + "X=0; X=1; X=2; X=3" + +let test_rational_bounds_narrow_integers () = + check_answers "strict rational bounds squeeze to integers" + {| Query expression: [Integer value: X] :and [GreaterThan left: X right: 1/2] :and [LessThanEqual left: X right: 5/2] |} + "X=1; X=2" + (* Integrity control at loading: facts must satisfy their schema. *) let test_fact_domain_violation () = @@ -400,6 +421,17 @@ let () = Alcotest.test_case "fact domain violation" `Quick test_fact_domain_violation; ] ); + ( "propagation", + [ + Alcotest.test_case "contradictory residue fails" `Quick + test_contradictory_residue_fails; + Alcotest.test_case "kind conflict fails" `Quick + test_kind_conflict_fails; + Alcotest.test_case "finite narrowing enumerates" `Quick + test_finite_narrowing_enumerates; + Alcotest.test_case "rational bounds narrow integers" `Quick + test_rational_bounds_narrow_integers; + ] ); ( "negation", [ Alcotest.test_case "not adults" `Quick test_negation; |