From e8f3ed5db26981d2b5417a9de1d16f33770d8ff4 Mon Sep 17 00:00:00 2001
From: scalexm <martin.alex32@hotmail.fr>
Date: Wed, 14 Mar 2018 15:19:17 +0100
Subject: [PATCH] Add documentation

---
 src/librustc/traits/mod.rs      | 12 ++++++++++++
 src/librustc_traits/lowering.rs | 12 ++++++++++++
 2 files changed, 24 insertions(+)

diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs
index dce1a89d142..8c5c36c3699 100644
--- a/src/librustc/traits/mod.rs
+++ b/src/librustc/traits/mod.rs
@@ -245,6 +245,14 @@ pub type Obligations<'tcx, O> = Vec<Obligation<'tcx, O>>;
 pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
 pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
 
+/// The following types:
+/// * `WhereClauseAtom`
+/// * `DomainGoal`
+/// * `Goal`
+/// * `Clause`
+/// are used for representing the trait system in the form of
+/// logic programming clauses. They are part of the interface
+/// for the chalk SLG solver.
 #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
 pub enum WhereClauseAtom<'tcx> {
     Implemented(ty::TraitPredicate<'tcx>),
@@ -270,6 +278,7 @@ pub enum QuantifierKind {
 
 #[derive(Clone, PartialEq, Eq, Hash, Debug)]
 pub enum Goal<'tcx> {
+    // FIXME: use interned refs instead of `Box`
     Implies(Vec<Clause<'tcx>>, Box<Goal<'tcx>>),
     And(Box<Goal<'tcx>>, Box<Goal<'tcx>>),
     Not(Box<Goal<'tcx>>),
@@ -289,8 +298,11 @@ impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
     }
 }
 
+/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
+/// Harrop Formulas".
 #[derive(Clone, PartialEq, Eq, Hash, Debug)]
 pub enum Clause<'tcx> {
+    // FIXME: again, use interned refs instead of `Box`
     Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
     DomainGoal(DomainGoal<'tcx>),
     ForAll(Box<ty::Binder<Clause<'tcx>>>),
diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs
index b69d97b67e8..296ad18c480 100644
--- a/src/librustc_traits/lowering.rs
+++ b/src/librustc_traits/lowering.rs
@@ -17,6 +17,7 @@ use syntax::ast;
 use rustc_data_structures::sync::Lrc;
 
 trait Lower<T> {
+    /// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
     fn lower(&self) -> T;
 }
 
@@ -56,6 +57,15 @@ impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
     }
 }
 
+/// `ty::Binder` is used for wrapping a rustc construction possibly containing generic
+/// lifetimes, e.g. `for<'a> T: Fn(&'a i32)`. Instead of representing higher-ranked things
+/// in that leaf-form (i.e. `Holds(Implemented(Binder<TraitPredicate>))` in the previous
+/// example), we model them with quantified goals, e.g. as for the previous example:
+/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
+/// `Binder<Holds(Implemented(TraitPredicate))>`.
+///
+/// Also, if `self` does not contain generic lifetimes, we can safely drop the binder and we
+/// can directly lower to a leaf goal instead of a quantified goal.
 impl<'tcx, T> Lower<Goal<'tcx>> for ty::Binder<T>
     where T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx> + Copy
 {
@@ -95,6 +105,8 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
     let item = tcx.hir.expect_item(node_id);
     match item.node {
         hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
+
+        // FIXME: other constructions e.g. traits, associated types...
         _ => Lrc::new(vec![]),
     }
 }