Implement find_witness completion rules

src/v4/extdeps/coercion_widening.dag

@@ -15,21 +15,79 @@ import v4.std.coercion {
   coercion_fold_refinement_widening
 }
 import v4.std.constraints { CanonicalGrounding }
-import v4.std.diagnostic { Outcome }
+import v4.std.diagnostic { Accepted, Outcome, Rejected }
 import v4.std.find_witness {
   PreservationPredicate,
   TargetDeclaredPriority,
   preservation_rule_refinement_widening
 }
-import v4.std.node { Node }
-import v4.std.refinement_widening_predicate { refinement_widening_predicate_algebra }
+import v4.std.integer_value_set {
+  integer_interval_value_set_node,
+  integer_unbounded_value_set_node
+}
+import v4.std.node { Atom, Node, TypeNode }
+import v4.std.node_query { find_named_child }
+import v4.std.refinement_widening_predicate { refinement_widening_predicate_algebra_for_value_sets }
+
+fn coercion_widening_unknown_value_set_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^coercion_widening_unknown_value_set } },
+    children: []
+  }
+}
+
+fn coercion_widening_rust_integer_value_set_from_inhabitant(inhabitant: Node) -> Node {
+  match find_named_child(root: inhabitant, name: ^rust_inhabitant_field_facts) {
+    Accepted { value: facts, diagnostics: None } =>
+      match find_named_child(root: facts, name: ^rust_facts_field_range) {
+        Accepted { value: range, diagnostics: None } =>
+          integer_interval_value_set_node(interval: range)
+        Rejected { diagnostics: _ } => coercion_widening_unknown_value_set_node()
+      }
+    Rejected { diagnostics: _ } => coercion_widening_unknown_value_set_node()
+  }
+}
+
+fn coercion_widening_python_integer_value_set_from_inhabitant(inhabitant: Node) -> Node {
+  match find_named_child(root: inhabitant, name: ^python_inhabitant_field_facts) {
+    Accepted { value: facts, diagnostics: None } =>
+      match find_named_child(root: facts, name: ^python_facts_field_encoding) {
+        Accepted { value: encoding, diagnostics: None } =>
+          if encoding == Node { kind: TypeNode { connective: Atom { identity: ^python_repr_int_arbitrary_precision } }, children: [] } {
+            integer_unbounded_value_set_node()
+          } else {
+            coercion_widening_unknown_value_set_node()
+          }
+        Rejected { diagnostics: _ } => coercion_widening_unknown_value_set_node()
+      }
+    Rejected { diagnostics: _ } => coercion_widening_unknown_value_set_node()
+  }
+}
 
 
 fn mvp_rust_i32_python_int_refinement_widening_predicate() -> PreservationPredicate {
+  let source = rust_inhabitant_i32_node()
+  let candidate = python_int_inhabitant_node()
   PreservationPredicate {
-    algebra: refinement_widening_predicate_algebra(
-      source: rust_inhabitant_i32_node(),
-      candidate: python_int_inhabitant_node()
+    algebra: refinement_widening_predicate_algebra_for_value_sets(
+      source: source,
+      candidate: candidate,
+      source_value_set: coercion_widening_rust_integer_value_set_from_inhabitant(inhabitant: source),
+      candidate_value_set: coercion_widening_python_integer_value_set_from_inhabitant(inhabitant: candidate)
+    ),
+    preservation_rule: preservation_rule_refinement_widening
+  }
+}
+
+fn mvp_python_int_rust_i32_refinement_narrowing_predicate() -> PreservationPredicate {
+  let source = python_int_inhabitant_node()
+  let candidate = rust_inhabitant_i32_node()
+  PreservationPredicate {
+    algebra: refinement_widening_predicate_algebra_for_value_sets(
+      source: source,
+      candidate: candidate,
+      source_value_set: coercion_widening_python_integer_value_set_from_inhabitant(inhabitant: source),
+      candidate_value_set: coercion_widening_rust_integer_value_set_from_inhabitant(inhabitant: candidate)
     ),
     preservation_rule: preservation_rule_refinement_widening
   }
@@ -48,3 +106,16 @@ fn coercion_fold_mvp_rust_i32_to_python_int_widening(
     predicate: mvp_rust_i32_python_int_refinement_widening_predicate()
   )
 }
+
+fn coercion_fold_mvp_python_int_to_rust_i32_narrowing(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  priority: Node,
+) -> Outcome<CoercionResult> {
+  coercion_fold_refinement_widening(
+    source: source,
+    candidates: candidates,
+    policy: TargetDeclaredPriority { priority: priority },
+    predicate: mvp_python_int_rust_i32_refinement_narrowing_predicate()
+  )
+}

src/v4/std/coercion.dag

@@ -40,6 +40,7 @@ import v4.std.find_witness {
   preservation_rule_refinement_widening
 }
 import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed }
+import v4.std.refinement_widening_predicate { refinement_widening_is_strict_coarsening }
 import v4.std.witness { HomomorphismWitness, StructuralPropertyWitness }
 data coercion_property_closed_candidate_set: Symbol = coercion_property_closed_candidate_set
 data coercion_property_candidate_set_closedness: Symbol = coercion_property_candidate_set_closedness
@@ -221,6 +222,26 @@ fn coercion_wrap_find_witness_rejection(
       }
   }
 }
+fn coercion_wrap_find_witness_rejection_with_refinement_algebra(
+  source: CanonicalGrounding,
+  upstream: NonEmptyDiagnostics,
+  refinement_algebra: Node,
+) -> Outcome<NonEmptyDiagnostics> {
+  if refinement_widening_is_strict_coarsening(algebra: refinement_algebra) {
+    Accepted {
+      value: NonEmptyDiagnostics {
+        head: coercion_not_realized_diagnostic(source: source, kind: WouldLoseInformation),
+        tail: list_append(
+          left: list_snoc_item(xs: Empty, item: upstream.head),
+          right: upstream.tail
+        )
+      },
+      diagnostics: None
+    }
+  } else {
+    coercion_wrap_find_witness_rejection(source: source, upstream: upstream)
+  }
+}
 fn coercion_homomorphism_evidence(
   source: CanonicalGrounding,
   fw: FindWitnessResult,
@@ -308,7 +329,11 @@ fn coercion_fold_refinement_widening(
         diagnostics: fw_d
       }
     Rejected { diagnostics: r } =>
-      match coercion_wrap_find_witness_rejection(source: source, upstream: r) {
+      match coercion_wrap_find_witness_rejection_with_refinement_algebra(
+        source: source,
+        upstream: r,
+        refinement_algebra: predicate.algebra
+      ) {
         Accepted { value: wrapped, diagnostics: _ } =>
           Rejected { diagnostics: wrapped }
         Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r }

src/v4/std/find_witness.dag

@@ -8,6 +8,7 @@ module v4.std.find_witness
 
 
 import v4.std.collection { List }
+import v4.std.algebra { contains }
 import v4.std.diagnostic {
   Accepted,
   Diagnostic,
@@ -25,6 +26,9 @@ import v4.std.constraint_satisfaction_predicate {
 import v4.std.exact_structural_equality_zip_fold_predicate {
   exact_structural_equality_zip_fold_preservation_holds
 }
+import v4.std.project_to_core_predicate {
+  project_to_core_preservation_holds
+}
 import v4.std.refinement_widening_predicate { refinement_widening_preservation_holds }
 import v4.std.node { Node, Symbol, well_formed }
 import v4.std.witness { StructuralPropertyWitness }
@@ -35,6 +39,7 @@ data find_witness_reason_invalid_witness: Symbol = find_witness_reason_invalid_w
 data preservation_rule_constraint_satisfaction: Symbol = preservation_rule_constraint_satisfaction
 data preservation_rule_exact_structural_equality_zip_fold: Symbol = preservation_rule_exact_structural_equality_zip_fold
 data preservation_rule_refinement_widening: Symbol = preservation_rule_refinement_widening
+data preservation_rule_project_to_core: Symbol = preservation_rule_project_to_core
 type CandidateSet {
   candidates: List<Node>
   closedness: StructuralPropertyWitness
@@ -62,9 +67,19 @@ type MultiplicityPolicy
   = UniqueOnly
   | TargetSelection { policy: TargetSelectionPolicy }
 fn preservation_rule_is_realized(rule: Symbol) -> Bool {
-  (rule == preservation_rule_constraint_satisfaction)
-    || (rule == preservation_rule_exact_structural_equality_zip_fold)
-    || (rule == preservation_rule_refinement_widening)
+  contains(
+    xs: realized_preservation_rules(),
+    item: rule,
+    eq: fn(left, right) { left == right }
+  )
+}
+fn realized_preservation_rules() -> List<Symbol> {
+  [
+    preservation_rule_constraint_satisfaction,
+    preservation_rule_exact_structural_equality_zip_fold,
+    preservation_rule_refinement_widening,
+    preservation_rule_project_to_core
+  ]
 }
 fn find_witness_no_candidate_diagnostic(source_facts: Node) -> Diagnostic {
   Diagnostic {
@@ -126,6 +141,12 @@ fn preservation_predicate_holds(
       candidate: candidate,
       algebra: predicate.algebra
     )
+  } else if predicate.preservation_rule == preservation_rule_project_to_core {
+    project_to_core_preservation_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      algebra: predicate.algebra
+    )
   } else {
     false
   }
@@ -249,6 +270,89 @@ fn find_witness(
     outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
   }
 }
+fn derivation_predicate_for_rule(
+  source_facts: Node,
+  derivation_algebra: Node,
+  rule: Symbol
+) -> PreservationPredicate {
+  if rule == preservation_rule_project_to_core {
+    PreservationPredicate {
+      algebra: derivation_algebra,
+      preservation_rule: rule
+    }
+  } else {
+    PreservationPredicate {
+      algebra: source_facts,
+      preservation_rule: rule
+    }
+  }
+}
+
+fn find_witness_rejection_priority(reason: Symbol) -> Int {
+  if reason == find_witness_reason_invalid_witness {
+    3
+  } else if reason == find_witness_reason_ambiguous_candidate {
+    2
+  } else if reason == find_witness_reason_not_realized {
+    1
+  } else {
+    0
+  }
+}
+
+fn find_witness_derivation_rejection_better(
+  current: Outcome<FindWitnessResult>,
+  candidate: Outcome<FindWitnessResult>
+) -> Outcome<FindWitnessResult> {
+  match current {
+    Accepted { value: _, diagnostics: _ } => current
+    Rejected { diagnostics: current_diagnostics } =>
+      match candidate {
+        Accepted { value: _, diagnostics: _ } => candidate
+        Rejected { diagnostics: candidate_diagnostics } =>
+          if find_witness_rejection_priority(reason: candidate_diagnostics.head.reason) > find_witness_rejection_priority(reason: current_diagnostics.head.reason) {
+            candidate
+          } else {
+            current
+          }
+      }
+  }
+}
+
+fn find_witness_derives(
+  source_facts: Node,
+  candidates: CandidateSet,
+  derivation_algebra: Node,
+  multiplicity_policy: MultiplicityPolicy
+) -> Outcome<FindWitnessResult> {
+  fold(
+    realized_preservation_rules(),
+    init: outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)),
+    f: fn(acc, rule) {
+	      match acc {
+	        Accepted { value: _, diagnostics: _ } => acc
+	        Rejected { diagnostics: _ } =>
+	          match find_witness(
+	            source_facts: source_facts,
+	            candidates: candidates,
+            predicate: derivation_predicate_for_rule(
+              source_facts: source_facts,
+              derivation_algebra: derivation_algebra,
+              rule: rule
+            ),
+	            multiplicity_policy: multiplicity_policy
+	          ) {
+	            Accepted { value: fw, diagnostics: d } => Accepted { value: fw, diagnostics: d }
+	            Rejected { diagnostics: r } =>
+	              find_witness_derivation_rejection_better(
+	                current: acc,
+	                candidate: Rejected { diagnostics: r }
+	              )
+	          }
+	      }
+	    }
+  )
+}
 fn find_witness_realized(
   source_facts: Node,
   candidates: CandidateSet,