done merge
This commit is contained in:
parent
4776e559fa
commit
4c18b1c10b
|
@ -1,5 +1,5 @@
|
||||||
"""
|
"""
|
||||||
Data structures for expressions and goals
|
Data structuers for expressions and goals
|
||||||
"""
|
"""
|
||||||
from dataclasses import dataclass
|
from dataclasses import dataclass
|
||||||
from typing import Optional, Union
|
from typing import Optional, Union
|
||||||
|
@ -33,7 +33,7 @@ class Variable:
|
||||||
|
|
||||||
@dataclass(frozen=True)
|
@dataclass(frozen=True)
|
||||||
class Goal:
|
class Goal:
|
||||||
variables: List[Variable]
|
variables: list[Variable]
|
||||||
target: Expr
|
target: Expr
|
||||||
name: Optional[str] = None
|
name: Optional[str] = None
|
||||||
is_conversion: bool = False
|
is_conversion: bool = False
|
||||||
|
@ -43,26 +43,22 @@ class Goal:
|
||||||
return Goal(variables=[], target=target)
|
return Goal(variables=[], target=target)
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def parse(payload: dict) -> Self:
|
def parse(payload: dict):
|
||||||
name = payload.get("userName")
|
name = payload.get("userName")
|
||||||
variables = [Variable.parse(v) for v in payload["vars"]]
|
variables = [Variable.parse(v) for v in payload["vars"]]
|
||||||
target = parse_expr(payload["target"])
|
target = parse_expr(payload["target"])
|
||||||
is_conversion = payload.get("isConversion", False) # Handle missing keys
|
is_conversion = payload["isConversion"]
|
||||||
return Goal(variables, target, name, is_conversion)
|
return Goal(variables, target, name, is_conversion)
|
||||||
|
|
||||||
def __str__(self):
|
def __str__(self):
|
||||||
front = "|" if self.is_conversion else "⊢"
|
front = "|" if self.is_conversion else "⊢"
|
||||||
return "\n".join(str(v) for v in self.variables) + f"\n{front} {self.target}"
|
return "\n".join(str(v) for v in self.variables) + \
|
||||||
|
f"\n{front} {self.target}"
|
||||||
|
|
||||||
@dataclass(frozen=True)
|
@dataclass(frozen=True)
|
||||||
class GoalState:
|
class GoalState:
|
||||||
state_id: int
|
state_id: int
|
||||||
goals: List[Goal]
|
goals: list[Goal]
|
||||||
|
|
||||||
_sentinel: list[int]
|
|
||||||
|
|
||||||
def __del__(self):
|
|
||||||
self._sentinel.append(self.state_id)
|
|
||||||
|
|
||||||
_sentinel: list[int]
|
_sentinel: list[int]
|
||||||
|
|
||||||
|
@ -85,7 +81,6 @@ class GoalState:
|
||||||
@dataclass(frozen=True)
|
@dataclass(frozen=True)
|
||||||
class TacticHave:
|
class TacticHave:
|
||||||
branch: str
|
branch: str
|
||||||
|
|
||||||
@dataclass(frozen=True)
|
@dataclass(frozen=True)
|
||||||
class TacticCalc:
|
class TacticCalc:
|
||||||
step: str
|
step: str
|
||||||
|
|
2
src
2
src
|
@ -1 +1 @@
|
||||||
Subproject commit b9b16ba0e9d99279837527bcb40176277d11e725
|
Subproject commit f20ee8dc87ae3fa9c0f13040e1b4f097f1a40503
|
Loading…
Reference in New Issue