From a414e57162772c8aa6afa5abda8c0b61e56a6209 Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Wed, 27 Jul 2016 23:25:16 -0700 Subject: [PATCH] change yaml spec to + move ast utilities + drop numpy dependency yaml spec now supports attaching meta data to specs such as pri or stl --- __init__.py | 2 +- ast.py | 60 +---------------------------------------------------- parser.py | 3 +-- utils.py | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 60 insertions(+), 62 deletions(-) create mode 100644 utils.py diff --git a/__init__.py b/__init__.py index 7fc2bf3..35eb67a 100644 --- a/__init__.py +++ b/__init__.py @@ -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 LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var from stl.parser import parse diff --git a/ast.py b/ast.py index 2e6f660..ef6569c 100644 --- a/ast.py +++ b/ast.py @@ -8,10 +8,6 @@ from typing import Union from enum import Enum from sympy import Symbol -from lenses import lens - -import funcy as fn - VarKind = Enum("VarKind", ["x", "u", "w"]) str_to_varkind = {"x": VarKind.x, "u": VarKind.u, "w": VarKind.w} dt_sym = Symbol('dt', positive=True) @@ -51,7 +47,7 @@ class NaryOpSTL(namedtuple('NaryOp', ['args'])): if n == 1: return "{}".format(self.args[0]) elif self.args: - rep = "({})" + " {op} ({})"*(len(self.args) - 1) + rep = " {op} ".join(["({})"]*(len(self.args) - 1)) return rep.format(*self.args, op=self.OP) else: return "" @@ -88,57 +84,3 @@ class Neg(namedtuple('Neg', ['arg'])): def children(self): 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_() diff --git a/parser.py b/parser.py index 9902c18..c45f9dc 100644 --- a/parser.py +++ b/parser.py @@ -14,7 +14,6 @@ import operator as op from parsimonious import Grammar, NodeVisitor from funcy import flatten -import numpy as np from lenses import lens from sympy import Symbol, Number @@ -51,7 +50,7 @@ prime = "'" pm = "+" / "-" dt = "dt" unbound = "?" -id = ("x" / "u" / "w") ~r"[a-zA-z\d]*" +id = ~r"[a-zA-z\d]*" const = ~r"[\+\-]?\d*(\.\d+)?" op = ">=" / "<=" / "<" / ">" / "=" _ = ~r"\s"+ diff --git a/utils.py b/utils.py new file mode 100644 index 0000000..dd705ea --- /dev/null +++ b/utils.py @@ -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_()