Merge branch 'ethosEoc2' of https://github.com/ajreynol/AletheLF-tc into ethosEoc2

Author: ajreynol

plugins/desugar/desugar_checker.h

@@ -19,21 +19,36 @@ namespace ethos {
 class State;
 
 /**
+ * Helper for generating the desugared executable proof checker.
+ *
+ * `DesugarChecker` is used by the main desugar plugin when VC generation is
+ * disabled.  It inspects each proof-rule declaration, emits an embedded rule
+ * constant for it, and generates checker invocation cases that translate
+ * checker commands into calls to the corresponding desugared proof-rule
+ * program.  The accumulated fragments are finally spliced into
+ * `eo_desugar_checker.eo` by output().
  */
 class DesugarChecker : public StdPlugin
 {
  public:
+  /** Construct the checker generator and initialize common constants. */
   DesugarChecker(State& s);
+  /** Destroy the checker generator. */
   ~DesugarChecker();
+  /** Generate embedded rule and invocation cases for proof rule v. */
   void finalizeRule(const Expr& v);
 
+  /** Write the generated checker EO fragment to out. */
   void output(std::ostream& out);
 
  private:
+  /** Common true literal used to recognize assumption rules. */
   Expr d_true;
-  // the rules
+  /** Generated embedded rule declarations. */
   std::stringstream d_rules;
+  /** Generated checker invocations for ordinary proof-rule steps. */
   std::stringstream d_ruleInvokes;
+  /** Generated checker invocations for assumption-pop proof-rule steps. */
   std::stringstream d_ruleInvokesPop;
 };
 

plugins/linear_patterns/linear_patterns.h

@@ -22,12 +22,24 @@ class State;
 class TypeChecker;
 
 /**
- * Provides utilities for linearizing patterns
+ * Utility for rewriting non-linear EO program patterns into linear patterns.
+ *
+ * Some target encodings, including Lean pattern matching, require each pattern
+ * variable to occur at most once.  `LinearPattern` rewrites repeated variables
+ * by replacing later occurrences with fresh parameters and collecting equality
+ * guards that enforce the original sharing.  When a guarded case is followed
+ * by later cases, linearization may split the original program into helper
+ * programs so the old fall-through behavior is preserved.
+ *
+ * The utility is exposed as static methods because callers typically need a
+ * one-shot transformation of an already-built program definition.
  */
 class LinearPattern : public StdPlugin
 {
  public:
+  /** Construct the linear-pattern utility plugin. */
   LinearPattern(State& s);
+  /** Destroy the linear-pattern utility plugin. */
   ~LinearPattern();
   /**
    * Linearize patterns in prog whose definition is progDef.
@@ -44,6 +56,7 @@ class LinearPattern : public StdPlugin
    * If condition is null, then no linearization was necessary.
    */
   static std::pair<Expr, Expr> linearizePattern(State& s, const Expr& pat);
+  /** Recursively replace repeated parameters and collect equality guards. */
   static Expr linearizeRec(State& s,
                            const Expr& pat,
                            std::map<Expr, size_t>& params,