doc(library/blast): document action_result

src/library/blast/action_result.h

@@ -9,9 +9,15 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
+/**
+   \brief Result produced by actions, proof-steps and choice-point next method.
+   There are 3 possible results
+   1- Failed:     action/step/next failed.
+   2- NewBranch:  a new branch has been created (or updated) in the current state.
+   3- Solved(pr): the current branch has been closed with proof pr. */
 class action_result {
 public:
-    enum kind { Failed, Solved, NewBranch };
+    enum kind { Failed, NewBranch, Solved };
 private:
     kind m_kind;
     expr m_proof;

src/library/blast/choice_point.h

@@ -23,7 +23,15 @@ public:
     virtual ~choice_point_cell() {}
     /** \brief Update next proof state. This method may
         perform destructive updates, choice points are not shared
-        objects. */
+        objects.
+
+        The next method result can be:
+        1- Failed:    failure
+        2- NewBranch: the current state has been updated, and it contains
+           a new branch to be solved.
+        3- Solved(pr): the current state has been updated, and its current
+           branch has been closed by the next choice.
+    */
     virtual action_result next() = 0;
 };
 

src/library/blast/state.h

@@ -43,17 +43,27 @@ class proof_step_cell {
     void dealloc() { delete this; }
 public:
     virtual ~proof_step_cell() {}
-    /** \brief Every proof-step must provide a resolve method.
+    /** \brief When an action updates the main branch of the proof state,
-        When the branch created by the proof-step is closed,
+        it adds a proof_step object to the proof step stack.
-        a proof pr is provided, and the proof-step can:
+        The proof_step object is responsible for converting a proof for
-        1- setup the next branch, or
+        the new branch into a proof for the original branch.
-        2- fail, or
-        3- finish and return a new proof
 
-        \remark Proof steps may be shared, i.e., they may ocurren the
+        If the action requires multiple branches to be solved,
+        the proof-step object is reponsible for creating the next branch.
+
+        The resolve method result can be:
+        1- Failed
+        2- NewBranch: the current state has been updated with the next branch to
+           be solved.
+        3- Solved(pr): all branches have been processed and pr is the
+           proof for the original branch.
+
+        \remark Proof steps may be shared, i.e., they may occur in the
         proof-step stack of different proof state objects.
         So, resolve must not perform destructive updates.
-        This is why we marked it as const. */
+        We enforce that by marking this method const.
+
+        Proof-steps are usually not used when implementing forward chaining. */
     virtual action_result resolve(expr const & pr) const = 0;
 };