From f3881fdc08486f37d92945ac2b431bdc70390658 Mon Sep 17 00:00:00 2001 From: ainnoot Date: Tue, 14 May 2024 19:41:05 +0200 Subject: [PATCH 1/5] chore(types): mypy --strict now works --- .github/workflows/cicd.yml | 2 +- ltlf2asp/api.py | 3 - ltlf2asp/cli.py | 16 +++-- ltlf2asp/exceptions.py | 6 +- ltlf2asp/parser/__init__.py | 2 +- ltlf2asp/parser/parser.py | 88 +++++++++++++----------- ltlf2asp/parser/reify_as_atoms.py | 43 ++++++------ ltlf2asp/parser/reify_interface.py | 11 +-- ltlf2asp/solve/check_model.py | 7 +- ltlf2asp/solve/decode_model.py | 8 +-- ltlf2asp/solve/incremental_solve_loop.py | 2 +- ltlf2asp/solve/parse_trace.py | 6 +- ltlf2asp/solve/solver_interface.py | 2 +- ltlf2asp/solve/static_solve_loop.py | 4 +- tests/test_parser/reify_as_object.py | 34 +++++---- tests/test_parser/syntax.py | 4 +- tests/test_parser/test_grammar.py | 16 ++--- 17 files changed, 133 insertions(+), 121 deletions(-) delete mode 100644 ltlf2asp/api.py diff --git a/.github/workflows/cicd.yml b/.github/workflows/cicd.yml index 4de225c..908a41b 100644 --- a/.github/workflows/cicd.yml +++ b/.github/workflows/cicd.yml @@ -61,7 +61,7 @@ jobs: run: poetry run ruff check ltlf2asp - name: Typecheck - run: poetry run mypy ltlf2asp + run: poetry run mypy ltlf2asp --strict - name: Install dependencies run: poetry install diff --git a/ltlf2asp/api.py b/ltlf2asp/api.py deleted file mode 100644 index e711fe9..0000000 --- a/ltlf2asp/api.py +++ /dev/null @@ -1,3 +0,0 @@ -from ltlf2asp.solve.solver_interface import Solver # noqa -from ltlf2asp.solve.decode_model import Model, SolveResult, SolveStatus # noqa -from ltlf2asp.parser import parse_formula # noqa diff --git a/ltlf2asp/cli.py b/ltlf2asp/cli.py index 1e2ed6e..fa01c52 100644 --- a/ltlf2asp/cli.py +++ b/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,7 +30,7 @@ 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.") @@ -36,7 +38,7 @@ def __post_init__(self): 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:") diff --git a/ltlf2asp/exceptions.py b/ltlf2asp/exceptions.py index 366a943..0915fc0 100644 --- a/ltlf2asp/exceptions.py +++ b/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 diff --git a/ltlf2asp/parser/__init__.py b/ltlf2asp/parser/__init__.py index 056429f..988284f 100644 --- a/ltlf2asp/parser/__init__.py +++ b/ltlf2asp/parser/__init__.py @@ -1 +1 @@ -from .parser import parse_formula # noqa +from .parser import parse_formula as parse_formula diff --git a/ltlf2asp/parser/parser.py b/ltlf2asp/parser/parser.py index 4b31403..ee3a78f 100644 --- a/ltlf2asp/parser/parser.py +++ b/ltlf2asp/parser/parser.py @@ -1,4 +1,8 @@ -from lark import Lark, Transformer # type: ignore +from typing import TypeVar, Set, Type, Sequence + +import clingo +import lark +from lark import Lark, Transformer from pathlib import Path from ltlf2asp.parser.constants import Constants from ltlf2asp.parser.reify_as_atoms import ReifyFormulaAsFacts @@ -6,20 +10,24 @@ 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) diff --git a/ltlf2asp/parser/reify_as_atoms.py b/ltlf2asp/parser/reify_as_atoms.py index 358525f..8c79042 100644 --- a/ltlf2asp/parser/reify_as_atoms.py +++ b/ltlf2asp/parser/reify_as_atoms.py @@ -1,16 +1,16 @@ from collections import defaultdict -from typing import Set, Dict, Tuple +from typing import Set, Dict, Sequence -import clingo # type: ignore +import clingo from ltlf2asp.parser.constants import Constants from ltlf2asp.parser.reify_interface import Reify -def clingo_symbol(name, args): +def clingo_symbol(name: str, args: Sequence[int]) -> clingo.Symbol: return clingo.Function(name, [clingo.Number(x) for x in args]) -def add_in_backend(b: clingo.Backend, symbol: clingo.Symbol): +def add_in_backend(b: clingo.Backend, symbol: clingo.Symbol) -> None: lit = b.add_atom(symbol) b.add_rule([lit], []) @@ -31,28 +31,29 @@ def id(self, obj: object) -> int: class ReifyFormulaAsFacts(Reify[int, Set[clingo.Symbol]]): def __init__(self) -> None: + super().__init__() self.pool: IDPool = IDPool() self.facts: Set[clingo.Symbol] = set() def result(self) -> Set[clingo.Symbol]: return self.facts - def constant(self, name: str): + def constant(self, name: str) -> int: id = self.pool.id((name,)) self.facts.add(clingo_symbol(name, [id])) return id - def reify_unary(self, f: int, name: str): + def reify_unary(self, f: int, name: str) -> int: id = self.pool.id((name, f)) self.facts.add(clingo_symbol(name, [id, f])) return id - def reify_binary(self, lhs: int, rhs: int, name: str): + def reify_binary(self, lhs: int, rhs: int, name: str) -> int: id = self.pool.id((name, lhs, rhs)) self.facts.add(clingo_symbol(name, [id, lhs, rhs])) return id - def reify_variadic(self, fs: Tuple[int, ...], name: str): + def reify_variadic(self, fs: Sequence[int], name: str) -> int: id = self.pool.id((name, *sorted(fs))) for f in fs: self.facts.add(clingo_symbol(name, [id, f])) @@ -79,48 +80,48 @@ def proposition(self, string: str) -> int: def next(self, f: int) -> int: return self.reify_unary(f, Constants.NEXT) - def weak_next(self, f) -> int: + def weak_next(self, f: int) -> int: # return self.reify_unary(f, Constants.WEAK_NEXT) return self.disjunction((self.last(), self.next(f))) - def until(self, lhs, rhs) -> int: + def until(self, lhs: int, rhs: int) -> int: return self.reify_binary(lhs, rhs, Constants.UNTIL) - def release(self, lhs, rhs) -> int: + def release(self, lhs: int, rhs: int) -> int: return self.reify_binary(lhs, rhs, Constants.RELEASE) - def weak_until(self, lhs, rhs) -> int: + def weak_until(self, lhs: int, rhs: int) -> int: # return self.reify_binary(lhs, rhs, Constants.WEAK_UNTIL) return self.disjunction((self.until(lhs, rhs), self.always(lhs))) - def strong_release(self, lhs, rhs) -> int: + def strong_release(self, lhs: int, rhs: int) -> int: # return self.reify_binary(lhs, rhs, Constants.STRONG_RELEASE) return self.conjunction((self.release(lhs, rhs), self.eventually(lhs))) - def equivalence(self, lhs, rhs) -> int: + def equivalence(self, lhs: int, rhs: int) -> int: # return self.reify_binary(lhs, rhs, Constants.EQUALS) return self.conjunction((self.implies(lhs, rhs), self.implies(rhs, lhs))) - def implies(self, lhs, rhs) -> int: + def implies(self, lhs: int, rhs: int) -> int: # return self.reify_binary(lhs, rhs, Constants.IMPLIES) return self.disjunction((self.negate(lhs), rhs)) - def eventually(self, f) -> int: + def eventually(self, f: int) -> int: # return self.reify_unary(f, Constants.EVENTUALLY) return self.until(self.true(), f) - def always(self, f) -> int: + def always(self, f: int) -> int: # return self.reify_unary(f, Constants.ALWAYS) return self.release(self.false(), f) - def negate(self, f) -> int: + def negate(self, f: int) -> int: return self.reify_unary(f, Constants.NEGATE) - def conjunction(self, fs: Tuple[int, ...]) -> int: + def conjunction(self, fs: Sequence[int]) -> int: return self.reify_variadic(fs, Constants.CONJUNCTION) - def disjunction(self, fs: Tuple[int, ...]) -> int: + def disjunction(self, fs: Sequence[int]) -> int: return self.reify_variadic(fs, Constants.DISJUNCTION) - def mark_as_root(self, f) -> None: + def mark_as_root(self, f: int) -> None: self.facts.add(clingo_symbol(Constants.ROOT, [f])) diff --git a/ltlf2asp/parser/reify_interface.py b/ltlf2asp/parser/reify_interface.py index 10eb64c..9387e3f 100644 --- a/ltlf2asp/parser/reify_interface.py +++ b/ltlf2asp/parser/reify_interface.py @@ -1,12 +1,15 @@ from abc import ABC, abstractmethod -from typing import TypeVar, Generic, Tuple +from typing import TypeVar, Generic, Sequence T = TypeVar("T") G = TypeVar("G") class Reify(Generic[T, G], ABC): + def __init__(self) -> None: + pass + @abstractmethod def result(self) -> G: pass @@ -72,13 +75,13 @@ def negate(self, f: T) -> T: pass @abstractmethod - def conjunction(self, fs: Tuple[T, ...]) -> T: + def conjunction(self, fs: Sequence[T]) -> T: pass @abstractmethod - def disjunction(self, fs: Tuple[T, ...]) -> T: + def disjunction(self, fs: Sequence[T]) -> T: pass @abstractmethod - def mark_as_root(self, f) -> None: + def mark_as_root(self, f: T) -> None: pass diff --git a/ltlf2asp/solve/check_model.py b/ltlf2asp/solve/check_model.py index 530ed7d..c0c56bf 100644 --- a/ltlf2asp/solve/check_model.py +++ b/ltlf2asp/solve/check_model.py @@ -1,16 +1,15 @@ from typing import Tuple, Iterable -import clingo # type: ignore - +import clingo from ltlf2asp.solve.decode_model import State from ltlf2asp.solve import CHECK -def trace_2(t: int, value: str, positive): +def trace_2(t: int, value: str, positive: bool) -> clingo.Symbol: return clingo.Function("trace", [clingo.Number(t), clingo.String(value)], positive) -def time_1(t: int): +def time_1(t: int) -> clingo.Symbol: return clingo.Function("time", [clingo.Number(t)]) diff --git a/ltlf2asp/solve/decode_model.py b/ltlf2asp/solve/decode_model.py index 258b50c..d00cac9 100644 --- a/ltlf2asp/solve/decode_model.py +++ b/ltlf2asp/solve/decode_model.py @@ -1,6 +1,6 @@ from typing import Dict, Tuple, Generator, Optional -import clingo # type: ignore +import clingo from collections import defaultdict from dataclasses import dataclass from enum import StrEnum @@ -17,13 +17,13 @@ class SolveResult: k: int model: Optional["Model"] - def __str__(self): + def __str__(self) -> str: return "{}[{}]".format(self.status.value, self.k) - def __repr__(self): + def __repr__(self) -> str: return self.__repr__() - def json(self): + def json(self) -> str: import json if self.status == SolveStatus.UNSATISFIABLE: diff --git a/ltlf2asp/solve/incremental_solve_loop.py b/ltlf2asp/solve/incremental_solve_loop.py index 558b039..01246ad 100644 --- a/ltlf2asp/solve/incremental_solve_loop.py +++ b/ltlf2asp/solve/incremental_solve_loop.py @@ -1,5 +1,5 @@ from typing import Optional, Tuple, List, Iterable -import clingo # type: ignore +import clingo from ltlf2asp.solve.decode_model import State, SolveResult, SolveStatus, Model from ltlf2asp.solve import SOLVE_INCREMENTAL diff --git a/ltlf2asp/solve/parse_trace.py b/ltlf2asp/solve/parse_trace.py index cf7a95e..d7eb4a7 100644 --- a/ltlf2asp/solve/parse_trace.py +++ b/ltlf2asp/solve/parse_trace.py @@ -1,12 +1,14 @@ +from typing import Dict, Tuple + from ltlf2asp.solve.decode_model import State import json -def parse_state(state_dict): +def parse_state(state_dict: Dict[str, str]) -> State: return State({x: (y.lower() == "true") for x, y in state_dict.items()}) -def parse_trace(file: str): +def parse_trace(file: str) -> Tuple[State, ...]: model = json.loads(file) states = model["model"]["states"] return tuple(parse_state(s) for s in states) diff --git a/ltlf2asp/solve/solver_interface.py b/ltlf2asp/solve/solver_interface.py index 1825346..6a983cb 100644 --- a/ltlf2asp/solve/solver_interface.py +++ b/ltlf2asp/solve/solver_interface.py @@ -3,7 +3,7 @@ from ltlf2asp.solve.decode_model import SolveResult from ltlf2asp.solve.incremental_solve_loop import solve as solve_incremental from ltlf2asp.solve.static_solve_loop import solve as solve_static -import clingo # type: ignore +import clingo class Solver: diff --git a/ltlf2asp/solve/static_solve_loop.py b/ltlf2asp/solve/static_solve_loop.py index f108bc5..da6e210 100644 --- a/ltlf2asp/solve/static_solve_loop.py +++ b/ltlf2asp/solve/static_solve_loop.py @@ -1,6 +1,6 @@ from typing import Optional, Iterable, Tuple from ltlf2asp.solve.decode_model import Model, State, SolveResult, SolveStatus -import clingo # type: ignore +import clingo from ltlf2asp.solve import SOLVE_STATIC @@ -35,7 +35,7 @@ def _solve(f: Iterable[clingo.Symbol], a: int, b: int) -> Optional[Model]: return None -def solve(f: Iterable[clingo.Symbol], max_horizon) -> SolveResult: +def solve(f: Iterable[clingo.Symbol], max_horizon: int) -> SolveResult: a, b = 0, 1 while b <= max_horizon: model = _solve(f, a, b) diff --git a/tests/test_parser/reify_as_object.py b/tests/test_parser/reify_as_object.py index decdba7..a07874d 100644 --- a/tests/test_parser/reify_as_object.py +++ b/tests/test_parser/reify_as_object.py @@ -1,11 +1,13 @@ -from typing import Optional +from typing import Optional, Sequence from ltlf2asp.parser.reify_interface import Reify from tests.test_parser import syntax +from tests.test_parser.syntax import Formula class ReifyFormulaAsObject(Reify[syntax.Formula, Optional[syntax.Formula]]): def __init__(self) -> None: + super().__init__() self.f: Optional[syntax.Formula] = None def result(self) -> Optional[syntax.Formula]: @@ -23,44 +25,46 @@ def last(self) -> syntax.Formula: def proposition(self, string: str) -> syntax.Formula: return syntax.Proposition(string) - def next(self, f) -> syntax.Formula: + def next(self, f: syntax.Formula) -> syntax.Formula: return syntax.Next(f) - def weak_next(self, f) -> syntax.Formula: + def weak_next(self, f: syntax.Formula) -> syntax.Formula: return syntax.WeakNext(f) - def until(self, lhs, rhs) -> syntax.Formula: + def until(self, lhs: syntax.Formula, rhs: syntax.Formula) -> syntax.Formula: return syntax.Until(lhs, rhs) - def release(self, lhs, rhs) -> syntax.Formula: + def release(self, lhs: syntax.Formula, rhs: syntax.Formula) -> syntax.Formula: return syntax.Release(lhs, rhs) - def weak_until(self, lhs, rhs) -> syntax.Formula: + def weak_until(self, lhs: syntax.Formula, rhs: syntax.Formula) -> syntax.Formula: return syntax.WeakUntil(lhs, rhs) - def strong_release(self, lhs, rhs) -> syntax.Formula: + def strong_release( + self, lhs: syntax.Formula, rhs: syntax.Formula + ) -> syntax.Formula: return syntax.StrongRelease(lhs, rhs) - def equivalence(self, lhs, rhs) -> syntax.Formula: + def equivalence(self, lhs: syntax.Formula, rhs: syntax.Formula) -> syntax.Formula: return syntax.Equivalence(lhs, rhs) - def implies(self, lhs, rhs) -> syntax.Formula: + def implies(self, lhs: syntax.Formula, rhs: syntax.Formula) -> syntax.Formula: return syntax.Implication(lhs, rhs) - def eventually(self, f) -> syntax.Formula: + def eventually(self, f: syntax.Formula) -> syntax.Formula: return syntax.Eventually(f) - def always(self, f) -> syntax.Formula: + def always(self, f: syntax.Formula) -> syntax.Formula: return syntax.Always(f) - def negate(self, f) -> syntax.Formula: + def negate(self, f: syntax.Formula) -> syntax.Formula: return syntax.Negate(f) - def conjunction(self, fs) -> syntax.Formula: + def conjunction(self, fs: Sequence[Formula]) -> syntax.Formula: return syntax.Conjunction(fs) - def disjunction(self, fs) -> syntax.Formula: + def disjunction(self, fs: Sequence[Formula]) -> syntax.Formula: return syntax.Disjunction(fs) - def mark_as_root(self, f) -> None: + def mark_as_root(self, f: Formula) -> None: self.f = f diff --git a/tests/test_parser/syntax.py b/tests/test_parser/syntax.py index a426bd2..5e6f51b 100644 --- a/tests/test_parser/syntax.py +++ b/tests/test_parser/syntax.py @@ -1,6 +1,6 @@ from dataclasses import dataclass from abc import ABC, abstractmethod -from typing import Tuple +from typing import Sequence @dataclass(frozen=True) @@ -131,7 +131,7 @@ def symbol(self) -> str: @dataclass(frozen=True) class Variadic(Formula, ABC): - fs: Tuple[Formula, ...] + fs: Sequence[Formula] def __str__(self) -> str: return "({})".format((" " + self.symbol() + " ").join(str(x) for x in self.fs)) diff --git a/tests/test_parser/test_grammar.py b/tests/test_parser/test_grammar.py index e2adf28..af7546b 100644 --- a/tests/test_parser/test_grammar.py +++ b/tests/test_parser/test_grammar.py @@ -13,42 +13,42 @@ class TestAtomicTokens: @pytest.mark.parametrize("token", ("true", "True", "TRUE")) def test_parse_true(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Truth() @pytest.mark.parametrize("token", ("false", "False", "FALSE")) def test_parse_false(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Faux() @pytest.mark.parametrize("token", ("last", "Last", "LAST", "end", "END", "End")) def test_parse_last(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Last() @pytest.mark.parametrize("token", ("Abc", "Ab2", "A23_xyzXW")) def test_uppercase_symbol(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Proposition(token) @pytest.mark.parametrize("token", ('"Abc"', '"Ab2"', '"A23_xyzXW"')) def test_quoted_symbol(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Proposition(token) @pytest.mark.parametrize("token", ("abc", "ab2", "a23_xyzXW")) def test_clingo_symbol(self, token): - dag = _parse_formula(token, "start", ReifyFormulaAsObject()) + dag = _parse_formula(token, "start", ReifyFormulaAsObject) assert dag == Proposition(token) class TestUnaryTokens: @pytest.mark.parametrize("token", ("a", "Abc", "x12_23")) def test_weak_next(self, token): - dag = _parse_formula("WX {}".format(token), "start", ReifyFormulaAsObject()) + dag = _parse_formula("WX {}".format(token), "start", ReifyFormulaAsObject) assert dag == WeakNext(Proposition(token)) @pytest.mark.parametrize("token", ("a",)) def test_weak_next_wrapped(self, token): - dag = _parse_formula("WX ({})".format(token), "start", ReifyFormulaAsObject()) + dag = _parse_formula("WX ({})".format(token), "start", ReifyFormulaAsObject) assert dag == WeakNext(Proposition(token)) From 3dc680c414ee2e7816e0bd33e7c4c70ce009a53e Mon Sep 17 00:00:00 2001 From: ainnoot Date: Tue, 14 May 2024 19:44:13 +0200 Subject: [PATCH 2/5] fix(ci): missing --install-types on mypy --- .github/workflows/cicd.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cicd.yml b/.github/workflows/cicd.yml index 908a41b..66a78b9 100644 --- a/.github/workflows/cicd.yml +++ b/.github/workflows/cicd.yml @@ -61,7 +61,9 @@ jobs: run: poetry run ruff check ltlf2asp - name: Typecheck - run: poetry run mypy ltlf2asp --strict + run: | + poetry run mypy --install-types + poetry run mypy ltlf2asp --strict - name: Install dependencies run: poetry install From 3d75876fed8d4e52da73bc5745cb4550e991a27d Mon Sep 17 00:00:00 2001 From: ainnoot Date: Tue, 14 May 2024 19:46:06 +0200 Subject: [PATCH 3/5] fix(ci): --install-types on mypy before checking --- .github/workflows/cicd.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/cicd.yml b/.github/workflows/cicd.yml index 66a78b9..83805d5 100644 --- a/.github/workflows/cicd.yml +++ b/.github/workflows/cicd.yml @@ -62,8 +62,7 @@ jobs: - name: Typecheck run: | - poetry run mypy --install-types - poetry run mypy ltlf2asp --strict + poetry run mypy ltlf2asp --strict --install-types - name: Install dependencies run: poetry install From f6ddda1b635feec50cc55cfe1fca62977d256c01 Mon Sep 17 00:00:00 2001 From: ainnoot Date: Tue, 14 May 2024 19:47:12 +0200 Subject: [PATCH 4/5] ci: clingo does not have types on GHA --- .github/workflows/cicd.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/cicd.yml b/.github/workflows/cicd.yml index 83805d5..e0914f9 100644 --- a/.github/workflows/cicd.yml +++ b/.github/workflows/cicd.yml @@ -62,7 +62,7 @@ jobs: - name: Typecheck run: | - poetry run mypy ltlf2asp --strict --install-types + poetry run mypy ltlf2asp - name: Install dependencies run: poetry install From 4c632dbfa8ca136140108a3720e5266237be0f1d Mon Sep 17 00:00:00 2001 From: ainnoot Date: Tue, 14 May 2024 19:49:19 +0200 Subject: [PATCH 5/5] chore(ci): added type ignore to clingo for CI --- ltlf2asp/parser/parser.py | 4 ++-- ltlf2asp/parser/reify_as_atoms.py | 2 +- ltlf2asp/solve/check_model.py | 2 +- ltlf2asp/solve/decode_model.py | 2 +- ltlf2asp/solve/incremental_solve_loop.py | 2 +- ltlf2asp/solve/solver_interface.py | 2 +- ltlf2asp/solve/static_solve_loop.py | 2 +- 7 files changed, 8 insertions(+), 8 deletions(-) diff --git a/ltlf2asp/parser/parser.py b/ltlf2asp/parser/parser.py index ee3a78f..b8725a7 100644 --- a/ltlf2asp/parser/parser.py +++ b/ltlf2asp/parser/parser.py @@ -1,7 +1,7 @@ from typing import TypeVar, Set, Type, Sequence -import clingo -import lark +import clingo # type: ignore +import lark # type: ignore from lark import Lark, Transformer from pathlib import Path from ltlf2asp.parser.constants import Constants diff --git a/ltlf2asp/parser/reify_as_atoms.py b/ltlf2asp/parser/reify_as_atoms.py index 8c79042..fecbcfd 100644 --- a/ltlf2asp/parser/reify_as_atoms.py +++ b/ltlf2asp/parser/reify_as_atoms.py @@ -1,7 +1,7 @@ from collections import defaultdict from typing import Set, Dict, Sequence -import clingo +import clingo # type: ignore from ltlf2asp.parser.constants import Constants from ltlf2asp.parser.reify_interface import Reify diff --git a/ltlf2asp/solve/check_model.py b/ltlf2asp/solve/check_model.py index c0c56bf..3aadf31 100644 --- a/ltlf2asp/solve/check_model.py +++ b/ltlf2asp/solve/check_model.py @@ -1,6 +1,6 @@ from typing import Tuple, Iterable -import clingo +import clingo # type: ignore from ltlf2asp.solve.decode_model import State from ltlf2asp.solve import CHECK diff --git a/ltlf2asp/solve/decode_model.py b/ltlf2asp/solve/decode_model.py index d00cac9..3958658 100644 --- a/ltlf2asp/solve/decode_model.py +++ b/ltlf2asp/solve/decode_model.py @@ -1,6 +1,6 @@ from typing import Dict, Tuple, Generator, Optional -import clingo +import clingo # type: ignore from collections import defaultdict from dataclasses import dataclass from enum import StrEnum diff --git a/ltlf2asp/solve/incremental_solve_loop.py b/ltlf2asp/solve/incremental_solve_loop.py index 01246ad..558b039 100644 --- a/ltlf2asp/solve/incremental_solve_loop.py +++ b/ltlf2asp/solve/incremental_solve_loop.py @@ -1,5 +1,5 @@ from typing import Optional, Tuple, List, Iterable -import clingo +import clingo # type: ignore from ltlf2asp.solve.decode_model import State, SolveResult, SolveStatus, Model from ltlf2asp.solve import SOLVE_INCREMENTAL diff --git a/ltlf2asp/solve/solver_interface.py b/ltlf2asp/solve/solver_interface.py index 6a983cb..1825346 100644 --- a/ltlf2asp/solve/solver_interface.py +++ b/ltlf2asp/solve/solver_interface.py @@ -3,7 +3,7 @@ from ltlf2asp.solve.decode_model import SolveResult from ltlf2asp.solve.incremental_solve_loop import solve as solve_incremental from ltlf2asp.solve.static_solve_loop import solve as solve_static -import clingo +import clingo # type: ignore class Solver: diff --git a/ltlf2asp/solve/static_solve_loop.py b/ltlf2asp/solve/static_solve_loop.py index da6e210..68f16dc 100644 --- a/ltlf2asp/solve/static_solve_loop.py +++ b/ltlf2asp/solve/static_solve_loop.py @@ -1,6 +1,6 @@ from typing import Optional, Iterable, Tuple from ltlf2asp.solve.decode_model import Model, State, SolveResult, SolveStatus -import clingo +import clingo # type: ignore from ltlf2asp.solve import SOLVE_STATIC