chore(types): mypy --strict now works

.github/workflows/cicd.yml

@@ -61,7 +61,8 @@ jobs:
       run: poetry run ruff check ltlf2asp
 
     - name: Typecheck
-      run: poetry run mypy ltlf2asp
+      run: |
+        poetry run mypy ltlf2asp
 
     - name: Install dependencies
       run: poetry install

ltlf2asp/cli.py

@@ -1,6 +1,8 @@
 import sys
 from argparse import ArgumentParser
 from pathlib import Path
+from typing import Sequence
+
 from ltlf2asp.solve.solver_interface import Solver
 from ltlf2asp.parser import parse_formula
 from dataclasses import dataclass
@@ -15,7 +17,7 @@ class SolveArguments:
     quiet: bool
     search_horizon: int
 
-    def __post_init__(self):
+    def __post_init__(self) -> None:
         if not self.formula.is_file():
             raise RuntimeError("Formula does not exist.")
 
@@ -28,15 +30,15 @@ class CheckArguments:
     formula: Path
     trace: Path
 
-    def __post_init__(self):
+    def __post_init__(self) -> None:
         if not self.formula.is_file():
             raise RuntimeError("Formula file does not exist.")
 
         if not self.trace.is_file():
             raise RuntimeError("Trace file does not exist.")
 
 
-def parse_check_args(argv) -> CheckArguments:
+def parse_check_args(argv: Sequence[str]) -> CheckArguments:
     p = ArgumentParser()
     p.add_argument("trace", type=Path)
     p.add_argument("formula", type=Path)
@@ -45,7 +47,7 @@ def parse_check_args(argv) -> CheckArguments:
     return CheckArguments(**args.__dict__)
 
 
-def parse_solve_args(argv) -> SolveArguments:
+def parse_solve_args(argv: Sequence[str]) -> SolveArguments:
     p = ArgumentParser()
     p.add_argument("formula", type=Path)
     p.add_argument("search_horizon", type=int)
@@ -57,7 +59,7 @@ def parse_solve_args(argv) -> SolveArguments:
     return SolveArguments(**args.__dict__)
 
 
-def solve(args: SolveArguments):
+def solve(args: SolveArguments) -> int:
     formula = parse_formula(args.formula.read_text())
     solver = Solver(args.incremental, args.search_horizon)
     result = solver.solve(formula)
@@ -70,7 +72,7 @@ def solve(args: SolveArguments):
     return 0
 
 
-def check(args: CheckArguments):
+def check(args: CheckArguments) -> int:
     formula = parse_formula(args.formula.read_text())
     trace = parse_trace(args.trace.read_text())
 
@@ -79,7 +81,7 @@ def check(args: CheckArguments):
     return 0
 
 
-def run():
+def run() -> int:
     argv = sys.argv[1:]
     if len(argv) <= 2:
         print("Usage:")

ltlf2asp/exceptions.py

@@ -3,8 +3,8 @@ class ParsingError(Exception):
 
 
 class UnsupportedOperator(Exception):
-    def __init__(self, string):
-        self.string = string
+    def __init__(self, string: str) -> None:
+        self.string: str = string
 
-    def message(self):
+    def message(self) -> str:
         return self.string

ltlf2asp/parser/__init__.py

@@ -1 +1 @@
-from .parser import parse_formula  # noqa
+from .parser import parse_formula as parse_formula

ltlf2asp/parser/parser.py

@@ -1,25 +1,33 @@
-from lark import Lark, Transformer  # type: ignore
+from typing import TypeVar, Set, Type, Sequence
+
+import clingo  # type: ignore
+import lark  # type: ignore
+from lark import Lark, Transformer
 from pathlib import Path
 from ltlf2asp.parser.constants import Constants
 from ltlf2asp.parser.reify_as_atoms import ReifyFormulaAsFacts
 from ltlf2asp.exceptions import ParsingError, UnsupportedOperator
 from ltlf2asp.parser.reify_interface import Reify
 
 
-class LTLfFlatTransformer(Transformer):
-    def __init__(self, reification_cls: Reify):
-        """Initialize."""
+T = TypeVar("T")
+G = TypeVar("G")
+
+
+class LTLfFlatTransformer(Transformer[T]):
+    def __init__(self, reification_cls: Type[Reify[T, G]]) -> None:
+        """Initiaflize."""
         super().__init__()
-        self.reify: Reify = reification_cls
+        self.reify: Reify[T, G] = reification_cls()
 
-    def start(self, args):
+    def start(self, args: Sequence[T]) -> G:  # type: ignore
         self.reify.mark_as_root(args[0])
         return self.reify.result()
 
-    def ltlf_formula(self, args):
+    def ltlf_formula(self, args: Sequence[T]) -> T:
         return args[0]
 
-    def ltlf_equivalence(self, args):
+    def ltlf_equivalence(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -33,7 +41,7 @@ def ltlf_equivalence(self, args):
 
         raise ParsingError
 
-    def ltlf_implication(self, args):
+    def ltlf_implication(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -46,7 +54,7 @@ def ltlf_implication(self, args):
 
         raise ParsingError
 
-    def ltlf_or(self, args):
+    def ltlf_or(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -56,7 +64,7 @@ def ltlf_or(self, args):
 
         raise ParsingError
 
-    def ltlf_and(self, args):
+    def ltlf_and(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -66,7 +74,7 @@ def ltlf_and(self, args):
 
         raise ParsingError
 
-    def ltlf_until(self, args):
+    def ltlf_until(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -79,7 +87,7 @@ def ltlf_until(self, args):
 
         raise ParsingError
 
-    def ltlf_weak_until(self, args):
+    def ltlf_weak_until(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -92,7 +100,7 @@ def ltlf_weak_until(self, args):
 
         raise ParsingError
 
-    def ltlf_release(self, args):
+    def ltlf_release(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -105,7 +113,7 @@ def ltlf_release(self, args):
 
         raise ParsingError
 
-    def ltlf_strong_release(self, args):
+    def ltlf_strong_release(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
@@ -118,80 +126,76 @@ def ltlf_strong_release(self, args):
 
         raise ParsingError
 
-    def ltlf_always(self, args):
+    def ltlf_always(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
         return self.reify.always(args[1])
 
-    def ltlf_eventually(self, args):
+    def ltlf_eventually(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
         return self.reify.eventually(args[1])
 
-    def ltlf_next(self, args):
+    def ltlf_next(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
         return self.reify.next(args[1])
 
-    def ltlf_weak_next(self, args):
+    def ltlf_weak_next(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
         return self.reify.weak_next(args[1])
 
-    def ltlf_not(self, args):
+    def ltlf_not(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
 
         return self.reify.negate(args[1])
 
-    def ltlf_wrapped(self, args):
+    def ltlf_wrapped(self, args: Sequence[T]) -> T:
         if len(args) == 1:
             return args[0]
         return args[1]
 
-    def symbol(self, args):
+    def symbol(self, args: Sequence[lark.Token]) -> str:
         string = "".join(x.value for x in args)
         return string.replace("'", '"')
 
-    def ltlf_atom(self, args):
-        if isinstance(args[0], int):
-            return args[0]
+    def ltlf_atom(self, args: Sequence[str]) -> T:
+        print("Got:", args, type(args[0]))
+        if args[0].lower() == Constants.TRUE:
+            return self.ltlf_true(args)
 
-        if isinstance(args[0], str):
-            if args[0].lower() == Constants.TRUE:
-                return self.ltlf_true(args)
+        elif args[0].lower() == Constants.FALSE:
+            return self.ltlf_false(args)
 
-            elif args[0].lower() == Constants.FALSE:
-                return self.ltlf_false(args)
-
-            elif args[0].lower() in (Constants.LAST, Constants.END):
-                return self.ltlf_last(args)
+        elif args[0].lower() in (Constants.LAST, Constants.END):
+            return self.ltlf_last(args)
 
+        else:
             return self.reify.proposition(args[0])
 
-        raise ParsingError
-
-    def ltlf_true(self, _args):
+    def ltlf_true(self, _args: Sequence[str]) -> T:
         return self.reify.true()
 
-    def ltlf_false(self, _args):
+    def ltlf_false(self, _args: Sequence[str]) -> T:
         return self.reify.false()
 
-    def ltlf_last(self, _args):
+    def ltlf_last(self, _args: Sequence[str]) -> T:
         return self.reify.last()
 
 
-def _parse_formula(formula_string: str, start_rule: str, reify: Reify):
+def _parse_formula(formula_string: str, start_rule: str, reify: Type[Reify[T, G]]) -> G:
     GRAMMAR = Path(__file__).parent / "grammar.lark"
     parser = Lark(GRAMMAR.read_text(), parser="lalr", start=start_rule)
     transformer = LTLfFlatTransformer(reify)
     tree = parser.parse(formula_string)
-    return transformer.transform(tree)
+    return transformer.transform(tree)  # type: ignore
 
 
-def parse_formula(formula_string: str):
-    return _parse_formula(formula_string, "start", ReifyFormulaAsFacts())
+def parse_formula(formula_string: str) -> Set[clingo.Symbol]:
+    return _parse_formula(formula_string, "start", ReifyFormulaAsFacts)