comments + pending goals in env

Author: nikomatsakis

crates/formality-prove/src/prove/constraints.rs

@@ -5,10 +5,27 @@ use formality_types::{
     rust::Visit,
 };
 
+/// Captures the conditions under which something is true.
+///
+/// Examples:
+///
+/// * The `substitution` indicates equality constraints for existential (inference) variables.
+///   E.g. if you try to prove `Vec<?A> = Vec<u32>`, the result will be "True; [?A => u32]".
+///   This substitution is then to be applied to any future goals/terms that may reference `?A`.
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
 pub struct Constraints {
+    /// The environment in which future goals should be proven.
+    /// This is an extension of the original environment; it may contain
+    /// new variables and new pending proof obligations.
     pub env: Env,
+
+    /// If this is false, it indicates that the result is actually *ambiguous* and not known to be true.
+    /// This occurs when e.g. we hit overflow or some other condition in which we can neither prove the
+    /// result true nor false.
     pub known_true: bool,
+
+    /// Maps an existential variable to the value which it must be equal to.
+    /// For example `Vec<?A> = Vec<u32>` would result in a substitution `[?A => u32]`.`
     pub substitution: Substitution,
 }
 
@@ -31,9 +48,10 @@ impl Constraints {
     }
 
     pub fn unconditionally_true(&self) -> bool {
-        self.known_true && self.substitution.is_empty()
+        self.known_true && self.substitution.is_empty() && self.env.pending().is_empty()
     }
 
+    /// Construct a set of constraints from a set of substitutions and the previous environment.
     pub fn from(
         env: impl Upcast<Env>,
         iter: impl IntoIterator<Item = (impl Upcast<Variable>, impl Upcast<Parameter>)>,

crates/formality-prove/src/prove/env.rs

@@ -3,6 +3,7 @@ use formality_macros::term;
 use formality_types::{
     grammar::{
         Binder, ExistentialVar, ParameterKind, UniversalVar, VarIndex, VarSubstitution, Variable,
+        Wc,
     },
     rust::{Fold, Visit},
 };
@@ -39,15 +40,31 @@ pub enum Bias {
 
 #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)]
 pub struct Env {
+    /// The set of variables that are in scope (universal and existential).
+    /// All terms should only reference free variables found in this set.
     variables: Vec<Variable>,
+
+    /// XXX this needs to be explained
     bias: Bias,
+
+    /// Pending goals that have not yet been proven.
+    /// When we prove a conjunction `(A && B)`, proving `A` may result in
+    /// some pending items (e.g., subtype constraints).
+    ///
+    /// These are then added into the env when we prove `B` so that if `B`
+    /// winds up constraining an inference varibale, it can also try to prove
+    /// the pending constraints that are now unlocked.
+    ///
+    /// Whenever a "successful" proof results, the pending obligations
+    pending: Vec<Wc>,
 }
 
 impl Env {
     pub fn new_with_bias(bias: Bias) -> Self {
         Env {
             variables: Default::default(),
             bias,
+            pending: vec![],
         }
     }
 
@@ -132,6 +149,11 @@ impl Env {
         }
     }
 
+    /// Pending goals that must still be proven
+    pub fn pending(&self) -> &[Wc] {
+        &self.pending
+    }
+
     /// An env A *encloses* a term `v` if all free variables in `v`
     /// are defined in A.
     pub fn encloses(&self, v: impl Visit) -> bool {
@@ -246,6 +268,7 @@ impl Env {
                 .map(|&v| vs.map_var(v).unwrap_or(v))
                 .collect(),
             bias: self.bias,
+            pending: vs.apply(&self.pending),
         }
     }
 

crates/formality-prove/src/prove/prove_wc.rs

@@ -19,6 +19,8 @@ use super::constraints::Constraints;
 use formality_types::grammar::Parameter::Ty;
 
 judgment_fn! {
+    /// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
+    /// If successful, returns the constraints under which the where-clause holds.
     pub fn prove_wc(
         _decls: Decls,
         env: Env,