Codex/ltl ir discourse

src/app.py

@@ -322,7 +322,7 @@ def ltl_to_english():
         return jsonify({"error": "Missing required query parameter 'formula'."}), 400
     try:
         node = parse_ltl_string(formula)
-        english = ltltoeng.finalize_sentence(node.__to_english__())
+        english = ltltoeng.translate(node, discourse=True)
     except Exception as e:
         return jsonify({"error": "Failed to translate formula.", "details": str(e)}), 400
 
@@ -426,7 +426,7 @@ def ltl_to_english_ui():
         else:
             try:
                 node = parse_ltl_string(input_formula)
-                translation = ltltoeng.finalize_sentence(node.__to_english__())
+                translation = ltltoeng.translate(node, discourse=True)
             except Exception as e:
                 error = f"Failed to translate formula: {e}"
 

src/exercisebuilder.py

@@ -54,7 +54,7 @@ def getLTLFormulaAsString(self, node):
         elif self.syntax == "English":
             ## We should hopefully never get here. However, 
             ## I'm adding it here to suggest a way forward.
-            return node.__to_english__()
+            return ltltoeng.translate(node, discourse=True)
 
         ## Default to classic syntax
         return str(node)
@@ -492,14 +492,14 @@ def formula_choice_metric(formula):
     def gen_nl_question(self, formula):
 
         as_node = ltlnode.parse_ltl_string(formula)
-        formula_eng = as_node.__to_english__()
+        formula_eng = ltltoeng.translate(as_node, discourse=True)
         if formula_eng is None or formula_eng == "":
             return None
 
         formula_eng_corrected = ltltoeng.correct_grammar(formula_eng)
         ### If there are multiple '.' in a row, replace with a single '.'
         formula_eng_corrected = re.sub(r'\.{2,}', '.', formula_eng_corrected)
-        return ltltoeng.finalize_sentence(formula_eng_corrected)
+        return formula_eng_corrected
 
 
     def get_options_with_misconceptions_as_formula(self, answer):

src/ltlir.py

@@ -0,0 +1,25 @@
+from dataclasses import dataclass, field
+from typing import List, Optional
+
+
+@dataclass
+class PlanStep:
+    """Intermediate representation step for discourse planning."""
+    role: str  # "anchor", "lead", "clause"
+    text: str
+    prefix: Optional[str] = None
+
+
+@dataclass
+class TemporalPlan:
+    """Intermediate compiled plan for multi-sentence LTL translations."""
+    steps: List[PlanStep] = field(default_factory=list)
+
+    def add_anchor(self, text: str) -> None:
+        self.steps.append(PlanStep(role="anchor", text=text))
+
+    def add_lead(self, text: str) -> None:
+        self.steps.append(PlanStep(role="lead", text=text))
+
+    def add_clause(self, text: str, prefix: Optional[str] = None) -> None:
+        self.steps.append(PlanStep(role="clause", text=text, prefix=prefix))

src/ltlnode.py

@@ -308,22 +308,17 @@ class FinallyNode(UnaryOperatorNode):
     def __init__(self, operand):
         super().__init__(FinallyNode.symbol, operand)
 
-    def __to_english__(self):
-        x = ltltoeng.apply_special_pattern_if_possible(self)
-        if x is not None:
-            return x
-        op = self.operand.__to_english__().rstrip('.')
-
-        # Provide more natural alternatives
-        if type(self.operand) is LiteralNode:
-            patterns = [
-                f"eventually, {op}",
-                f"{op} will eventually occur",
-                f"at some point, {op} will hold"
-            ]
-            return ltltoeng.choose_best_sentence(patterns)
-
-        return f"eventually, {op}"
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        op = self.operand.__to_english__().rstrip('.')
+
+        # Provide more natural alternatives
+        if type(self.operand) is LiteralNode:
+            return ltltoeng.finally_phrase(op, is_literal=True)
+
+        return ltltoeng.finally_phrase(op, is_literal=False)
 
     def __forge__(self):
         return f"(EVENTUALLY {self.operand.__forge__()})"
@@ -339,23 +334,20 @@ class OrNode(BinaryOperatorNode):
     def __init__(self, left, right):
         super().__init__(OrNode.symbol, left, right)
 
-    def __to_english__(self):
-        x = ltltoeng.apply_special_pattern_if_possible(self)
-        if x is not None:
-            return x
-        lhs = self.left.__to_english__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-
-        # Provide alternatives for simple literals
-        if type(self.left) is LiteralNode and type(self.right) is LiteralNode:
-            patterns = [
-                f"either {lhs} or {rhs}",
-                f"{lhs} or {rhs}",
-                f"at least one of {lhs} or {rhs}"
-            ]
-            return ltltoeng.choose_best_sentence(patterns)
-
-        return f"either {lhs} or {rhs}"
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+
+        # Provide alternatives for simple literals
+        if type(self.left) is LiteralNode and type(self.right) is LiteralNode:
+            return ltltoeng.or_phrase(lhs, rhs)
+
+        if ltltoeng.get_pragmatic_policy().avoid_exclusive_or:
+            return f"either {lhs} or {rhs} (or both)"
+        return f"either {lhs} or {rhs}"
 
 
 
@@ -365,7 +357,7 @@ class AndNode(BinaryOperatorNode):
     def __init__(self, left, right):
         super().__init__(AndNode.symbol, left, right)
 
-    def __to_english__(self):
+    def __to_english__(self):
         x = ltltoeng.apply_special_pattern_if_possible(self)
         if x is not None:
             return x
@@ -423,16 +415,17 @@ def __to_english__(self):
         lhs = ltltoeng.normalize_embedded_clause(lhs)
         rhs = ltltoeng.normalize_embedded_clause(rhs)
 
-        # Potential patterns:
-        patterns = [
-            f"if {lhs}, then {rhs}",
-            f"{lhs} implies {rhs}",
-            f"whenever {lhs}, then {rhs}"
-        ]
-
-        # Choose the most fluent pattern rather than picking randomly
-        english = ltltoeng.choose_best_sentence(patterns)
-        return english
+        # Potential patterns:
+        patterns = [
+            f"if {lhs}, then {rhs}",
+            f"{lhs} implies {rhs}"
+        ]
+        if not ltltoeng.get_pragmatic_policy().avoid_causal:
+            patterns.append(f"whenever {lhs}, {rhs}")
+
+        # Choose the most fluent pattern rather than picking randomly
+        english = ltltoeng.choose_best_sentence(patterns)
+        return english
 
 
 class EquivalenceNode(BinaryOperatorNode):