change yaml spec to + move ast utilities + drop numpy dependency
yaml spec now supports attaching meta data to specs such as pri or stl
This commit is contained in:
parent
8d5a32701c
commit
a414e57162
4 changed files with 60 additions and 62 deletions
|
|
@ -1,4 +1,4 @@
|
||||||
from stl.ast import terms_lens, lineq_lens, walk, tree, and_or_lens
|
from stl.utils import terms_lens, lineq_lens, walk, tree, and_or_lens
|
||||||
from stl.ast import dt_sym, t_sym
|
from stl.ast import dt_sym, t_sym
|
||||||
from stl.ast import LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var
|
from stl.ast import LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var
|
||||||
from stl.parser import parse
|
from stl.parser import parse
|
||||||
|
|
|
||||||
60
ast.py
60
ast.py
|
|
@ -8,10 +8,6 @@ from typing import Union
|
||||||
from enum import Enum
|
from enum import Enum
|
||||||
from sympy import Symbol
|
from sympy import Symbol
|
||||||
|
|
||||||
from lenses import lens
|
|
||||||
|
|
||||||
import funcy as fn
|
|
||||||
|
|
||||||
VarKind = Enum("VarKind", ["x", "u", "w"])
|
VarKind = Enum("VarKind", ["x", "u", "w"])
|
||||||
str_to_varkind = {"x": VarKind.x, "u": VarKind.u, "w": VarKind.w}
|
str_to_varkind = {"x": VarKind.x, "u": VarKind.u, "w": VarKind.w}
|
||||||
dt_sym = Symbol('dt', positive=True)
|
dt_sym = Symbol('dt', positive=True)
|
||||||
|
|
@ -51,7 +47,7 @@ class NaryOpSTL(namedtuple('NaryOp', ['args'])):
|
||||||
if n == 1:
|
if n == 1:
|
||||||
return "{}".format(self.args[0])
|
return "{}".format(self.args[0])
|
||||||
elif self.args:
|
elif self.args:
|
||||||
rep = "({})" + " {op} ({})"*(len(self.args) - 1)
|
rep = " {op} ".join(["({})"]*(len(self.args) - 1))
|
||||||
return rep.format(*self.args, op=self.OP)
|
return rep.format(*self.args, op=self.OP)
|
||||||
else:
|
else:
|
||||||
return ""
|
return ""
|
||||||
|
|
@ -88,57 +84,3 @@ class Neg(namedtuple('Neg', ['arg'])):
|
||||||
|
|
||||||
def children(self):
|
def children(self):
|
||||||
return [self.arg]
|
return [self.arg]
|
||||||
|
|
||||||
|
|
||||||
def walk(stl, bfs=False):
|
|
||||||
"""Walks Ast. Defaults to DFS unless BFS flag is set."""
|
|
||||||
pop = deque.popleft if bfs else deque.pop
|
|
||||||
children = deque([stl])
|
|
||||||
while len(children) != 0:
|
|
||||||
node = pop(children)
|
|
||||||
yield node
|
|
||||||
children.extend(node.children())
|
|
||||||
|
|
||||||
|
|
||||||
def tree(stl):
|
|
||||||
return {x:set(x.children()) for x in walk(stl) if x.children()}
|
|
||||||
|
|
||||||
|
|
||||||
def type_pred(*args):
|
|
||||||
ast_types = set(args)
|
|
||||||
return lambda x: type(x) in ast_types
|
|
||||||
|
|
||||||
|
|
||||||
def _child_lens(psi, focus):
|
|
||||||
if psi is None:
|
|
||||||
return
|
|
||||||
if isinstance(psi, NaryOpSTL):
|
|
||||||
for j, _ in enumerate(psi.args):
|
|
||||||
yield focus.args[j]
|
|
||||||
else:
|
|
||||||
yield focus.arg
|
|
||||||
|
|
||||||
|
|
||||||
def ast_lens(phi:"STL", bind=True, *, pred) -> lens:
|
|
||||||
tls = list(fn.flatten(_ast_lens(phi, pred=pred)))
|
|
||||||
tl = lens().tuple_(*tls).each_()
|
|
||||||
return tl.bind(phi) if bind else tl
|
|
||||||
|
|
||||||
|
|
||||||
def _ast_lens(phi, *, pred, focus=lens()):
|
|
||||||
psi = focus.get(state=phi)
|
|
||||||
ret_lens = [focus] if pred(psi) else []
|
|
||||||
|
|
||||||
if isinstance(psi, LinEq):
|
|
||||||
return ret_lens
|
|
||||||
|
|
||||||
child_lenses = list(_child_lens(psi, focus=focus))
|
|
||||||
ret_lens += [_ast_lens(phi, pred=pred, focus=cl) for cl in child_lenses]
|
|
||||||
return ret_lens
|
|
||||||
|
|
||||||
|
|
||||||
lineq_lens = fn.partial(ast_lens, pred=type_pred(LinEq))
|
|
||||||
and_or_lens = fn.partial(ast_lens, pred=type_pred(And, Or))
|
|
||||||
|
|
||||||
def terms_lens(phi:"STL", bind=True) -> lens:
|
|
||||||
return lineq_lens(phi, bind).terms.each_()
|
|
||||||
|
|
|
||||||
|
|
@ -14,7 +14,6 @@ import operator as op
|
||||||
|
|
||||||
from parsimonious import Grammar, NodeVisitor
|
from parsimonious import Grammar, NodeVisitor
|
||||||
from funcy import flatten
|
from funcy import flatten
|
||||||
import numpy as np
|
|
||||||
from lenses import lens
|
from lenses import lens
|
||||||
|
|
||||||
from sympy import Symbol, Number
|
from sympy import Symbol, Number
|
||||||
|
|
@ -51,7 +50,7 @@ prime = "'"
|
||||||
pm = "+" / "-"
|
pm = "+" / "-"
|
||||||
dt = "dt"
|
dt = "dt"
|
||||||
unbound = "?"
|
unbound = "?"
|
||||||
id = ("x" / "u" / "w") ~r"[a-zA-z\d]*"
|
id = ~r"[a-zA-z\d]*"
|
||||||
const = ~r"[\+\-]?\d*(\.\d+)?"
|
const = ~r"[\+\-]?\d*(\.\d+)?"
|
||||||
op = ">=" / "<=" / "<" / ">" / "="
|
op = ">=" / "<=" / "<" / ">" / "="
|
||||||
_ = ~r"\s"+
|
_ = ~r"\s"+
|
||||||
|
|
|
||||||
57
utils.py
Normal file
57
utils.py
Normal file
|
|
@ -0,0 +1,57 @@
|
||||||
|
from lenses import lens
|
||||||
|
import funcy as fn
|
||||||
|
|
||||||
|
from stl.ast import LinEq, And, Or, NaryOpSTL
|
||||||
|
|
||||||
|
def walk(stl, bfs=False):
|
||||||
|
"""Walks Ast. Defaults to DFS unless BFS flag is set."""
|
||||||
|
pop = deque.popleft if bfs else deque.pop
|
||||||
|
children = deque([stl])
|
||||||
|
while len(children) != 0:
|
||||||
|
node = pop(children)
|
||||||
|
yield node
|
||||||
|
children.extend(node.children())
|
||||||
|
|
||||||
|
|
||||||
|
def tree(stl):
|
||||||
|
return {x:set(x.children()) for x in walk(stl) if x.children()}
|
||||||
|
|
||||||
|
|
||||||
|
def type_pred(*args):
|
||||||
|
ast_types = set(args)
|
||||||
|
return lambda x: type(x) in ast_types
|
||||||
|
|
||||||
|
|
||||||
|
def _child_lens(psi, focus):
|
||||||
|
if psi is None:
|
||||||
|
return
|
||||||
|
if isinstance(psi, NaryOpSTL):
|
||||||
|
for j, _ in enumerate(psi.args):
|
||||||
|
yield focus.args[j]
|
||||||
|
else:
|
||||||
|
yield focus.arg
|
||||||
|
|
||||||
|
|
||||||
|
def ast_lens(phi:"STL", bind=True, *, pred) -> lens:
|
||||||
|
tls = list(fn.flatten(_ast_lens(phi, pred=pred)))
|
||||||
|
tl = lens().tuple_(*tls).each_()
|
||||||
|
return tl.bind(phi) if bind else tl
|
||||||
|
|
||||||
|
|
||||||
|
def _ast_lens(phi, *, pred, focus=lens()):
|
||||||
|
psi = focus.get(state=phi)
|
||||||
|
ret_lens = [focus] if pred(psi) else []
|
||||||
|
|
||||||
|
if isinstance(psi, LinEq):
|
||||||
|
return ret_lens
|
||||||
|
|
||||||
|
child_lenses = list(_child_lens(psi, focus=focus))
|
||||||
|
ret_lens += [_ast_lens(phi, pred=pred, focus=cl) for cl in child_lenses]
|
||||||
|
return ret_lens
|
||||||
|
|
||||||
|
|
||||||
|
lineq_lens = fn.partial(ast_lens, pred=type_pred(LinEq))
|
||||||
|
and_or_lens = fn.partial(ast_lens, pred=type_pred(And, Or))
|
||||||
|
|
||||||
|
def terms_lens(phi:"STL", bind=True) -> lens:
|
||||||
|
return lineq_lens(phi, bind).terms.each_()
|
||||||
Loading…
Add table
Add a link
Reference in a new issue