From 5251752b9cfcc27b895a180e9a9203313cded9f0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Nov 2015 17:29:01 -0800 Subject: [PATCH] chore(library/blast/state): document branch extension methods --- src/library/blast/state.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 7811260fc..2b0e33b23 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -103,12 +103,21 @@ class branch_extension { void dealloc() { delete this; } public: virtual ~branch_extension() {} + /** \brief Return a copy of this object */ virtual branch_extension * clone() = 0; + /** \brief This method is invoked the first time an extension is used in a branch + The system guarantees this object is not shared, and destructive updates are allowed. */ virtual void initialized() {} + /** \brief This method is invoked when the given hypothesis is initialized in the current branch. + The system guarantees this object is not shared, and destructive updates are allowed. */ virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) {} + /** \brief This method is invoked when the given hypothesis is deleted from the current branch. + The system guarantees this object is not shared, and destructive updates are allowed. */ virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) {} }; +/** \brief This procedure must be invoke at Lean initialization time for each branch extension. + The unique id returned should be used to retrieve the branch extension associated with the current state */ unsigned register_branch_extension(branch_extension * initial); /** \brief Information associated with the current branch of the proof state.