doc: autodocs for expr and data

docs/_toc.yml

@@ -11,3 +11,5 @@ parts:
   chapters:
   - file: api-server
   - file: api-search
+  - file: api-expr
+  - file: api-data

docs/api-data.rst

@@ -0,0 +1,5 @@
+Data
+=============
+
+.. automodule:: pantograph.compiler
+    :members:

docs/api-expr.rst

@@ -0,0 +1,8 @@
+Expr
+=============
+
+.. automodule:: pantograph.expr
+    :members:
+
+.. autodata:: pantograph.expr.Expr
+.. autodata:: pantograph.expr.Tactic

pantograph/compiler.py

@@ -2,6 +2,10 @@
 
 @dataclass(frozen=True)
 class TacticInvocation:
+    """
+    One tactic invocation with the before/after goals extracted from Lean source
+    code.
+    """
     before: str
     after: str
     tactic: str

pantograph/expr.py

@@ -2,11 +2,14 @@
 Data structuers for expressions and goals
 """
 from dataclasses import dataclass, field
-from typing import Optional, Union
+from typing import Optional, TypeAlias
 
-Expr = str
+Expr: TypeAlias = str
 
 def parse_expr(payload: dict) -> Expr:
+    """
+    :meta private:
+    """
     return payload["pp"]
 
 @dataclass(frozen=True)
@@ -25,6 +28,9 @@ def parse(payload: dict):
         return Variable(t, v, name)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         result = self.name if self.name else "_"
         result += f" : {self.t}"
         if self.v:
@@ -41,6 +47,9 @@ class Goal:
 
     @staticmethod
     def sentence(target: Expr):
+        """
+        :meta public:
+        """
         return Goal(variables=[], target=target)
 
     @staticmethod
@@ -56,6 +65,9 @@ def parse(payload: dict, sibling_map: dict[str, int]):
         return Goal(variables, target, sibling_dep, name, is_conversion)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         front = "|" if self.is_conversion else "⊢"
         return "\n".join(str(v) for v in self.variables) + \
             f"\n{front} {self.target}"
@@ -74,6 +86,8 @@ def __del__(self):
     def is_solved(self) -> bool:
         """
         WARNING: Does not handle dormant goals.
+
+        :meta public:
         """
         return not self.goals
 
@@ -87,6 +101,9 @@ def parse(payload: dict, _sentinel: list[int]):
         return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         return "\n".join([str(g) for g in self.goals])
 
 @dataclass(frozen=True)
@@ -102,7 +119,7 @@ class TacticHave:
 @dataclass(frozen=True)
 class TacticLet:
     """
-    The `have` tactic, equivalent to
+    The `let` tactic, equivalent to
     ```lean
     let {binder_name} : {branch} := ...
     ```
@@ -126,4 +143,4 @@ class TacticExpr:
     """
     expr: str
 
-Tactic = Union[str, TacticHave, TacticLet, TacticCalc, TacticExpr]
+Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr

pantograph/server.py

@@ -100,6 +100,8 @@ def restart(self):
     def run(self, cmd, payload):
         """
         Runs a raw JSON command. Preferably use one of the commands below.
+
+        :meta private:
         """
         assert self.proc
         s = json.dumps(payload)
@@ -123,9 +125,7 @@ def run(self, cmd, payload):
 
     def gc(self):
         """
-        Garbage collect deleted goal states.
-
-        Must be called periodically.
+        Garbage collect deleted goal states to free up memory.
         """
         if not self.to_remove_goal_states:
             return
@@ -145,13 +145,19 @@ def expr_type(self, expr: Expr) -> Expr:
         return parse_expr(result["type"])
 
     def goal_start(self, expr: Expr) -> GoalState:
+        """
+        Create a goal state with one root goal, whose target is `expr`
+        """
         result = self.run('goal.start', {"expr": str(expr)})
         if "error" in result:
             print(f"Cannot start goal: {expr}")
             raise ServerError(result["desc"])
         return GoalState(state_id=result["stateId"], goals=[Goal.sentence(expr)], _sentinel=self.to_remove_goal_states)
 
     def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalState:
+        """
+        Execute a tactic on `goal_id` of `state`
+        """
         args = {"stateId": state.state_id, "goalId": goal_id}
         if isinstance(tactic, str):
             args["tactic"] = tactic