ISCC wrapper and projection

diff --git a/polyp.py b/polyp.py
index b73814e..9058c08 100644 (file)
--- a/polyp.py
+++ b/polyp.py
@@ -16,19 +16,65 @@ __all__ = [
 ]
 
 
-_iscc_debug = False
+def _strsymbol(symbol):
+    if isinstance(symbol, str):
+        return symbol
+    elif isinstance(symbol, Expression) and symbol.issymbol():
+        return str(symbol)
+    else:
+        raise TypeError('symbol must be a string or a symbol')
+
+def _strsymbols(symbols):
+    if isinstance(symbols, str):
+        return symbols.replace(',', ' ').split()
+    else:
+        return [_strsymbol(symbol) for symbol in symbols]
+
+
+class _ISCC:
+
+    command =['iscc']
+    debug = False
+
+    @classmethod
+    def eval(cls, input):
+        if not input.endswith(';'):
+            input += ';'
+        proc = subprocess.Popen(cls.command,
+                stdin=subprocess.PIPE, stdout=subprocess.PIPE,
+                universal_newlines=True)
+        output, error = proc.communicate(input=input)
+        output = output.strip()
+        if cls.debug:
+            print('iscc: {!r} -> {!r}'.format(input, output))
+        return output
+
+    @classmethod
+    def symbols(cls, symbols):
+        symbols = _strsymbols(symbols)
+        return '[{}]'.format(', '.join(symbols))
+
+    @classmethod
+    def constraints(cls, equalities, inequalities):
+        strings = []
+        for equality in equalities:
+            strings.append('{} = 0'.format(equality))
+        for inequality in inequalities:
+            strings.append('{} <= 0'.format(inequality))
+        return ' and '.join(strings)
 
-def _iscc(input):
-    if not input.endswith(';'):
-        input += ';'
-    proc = subprocess.Popen(['iscc'],
-            stdin=subprocess.PIPE, stdout=subprocess.PIPE,
-            universal_newlines=True)
-    output, error = proc.communicate(input=input)
-    output = output.strip()
-    if _iscc_debug:
-        print('ISCC({!r}) = {!r}'.format(input, output))
-    return output
+    @classmethod
+    def set(cls, symbols, equalities, inequalities):
+        return '{{ {} : {} }}'.format(cls.symbols(symbols),
+                cls.constraints(equalities, inequalities))
+
+    @classmethod
+    def map(cls, lsymbols, rsymbols, equalities, inequalities):
+        return '{{ {} -> {} : {} }}'.format(
+                cls.symbols(lsymbols), cls.symbols(rsymbols),
+                cls.constraints(equalities, inequalities))
+
+_iscc = _ISCC()
 
 
 def _polymorphic_method(func):
@@ -68,10 +114,7 @@ class Expression:
             coefficients = coefficients.items()
         if coefficients is not None:
             for symbol, coefficient in coefficients:
-                if isinstance(symbol, Expression) and symbol.issymbol():
-                    symbol = str(symbol)
-                elif not isinstance(symbol, str):
-                    raise TypeError('symbols must be strings')
+                symbol = _strsymbol(symbol)
                 if not isinstance(coefficient, numbers.Rational):
                     raise TypeError('coefficients must be rational numbers')
                 if coefficient != 0:
@@ -83,6 +126,7 @@ class Expression:
 
     @classmethod
     def _fromiscc(cls, symbols, string):
+        symbols = _strsymbols(symbols)
         string = re.sub(r'(\d+)\s*([a-zA-Z_]\w*)',
                 lambda m: '{}*{}'.format(m.group(1), m.group(2)),
                 string)
@@ -99,10 +143,7 @@ class Expression:
         return len(list(self.symbols()))
 
     def coefficient(self, symbol):
-        if isinstance(symbol, Expression) and symbol.issymbol():
-            symbol = str(symbol)
-        elif not isinstance(symbol, str):
-            raise TypeError('symbol must be a string')
+        symbol = _strsymbol(symbol)
         try:
             return self._coefficients[symbol]
         except KeyError:
@@ -270,13 +311,11 @@ def Constant(numerator=0, denominator=None):
         return Expression(constant=Fraction(numerator, denominator))
 
 def Symbol(name):
-    if not isinstance(name, str):
-        raise TypeError('name must be a string')
+    name = _strsymbol(name)
     return Expression(coefficients={name: 1})
 
 def symbols(names):
-    if isinstance(names, str):
-        names = names.replace(',', ' ').split()
+    names = _strsymbols(names)
     return (Symbol(name) for name in names)
 
 
@@ -317,29 +356,19 @@ class Polyhedron:
         for inequality in inequalities:
             symbols.update(inequality.symbols())
         symbols = sorted(symbols)
-        string = cls._isccpoly(symbols, equalities, inequalities)
-        string = _iscc(string)
+        string = _iscc.set(symbols, equalities, inequalities)
+        string = _iscc.eval(string)
         return cls._fromiscc(symbols, string)
 
-    @classmethod
-    def _isccpoly(cls, symbols, equalities, inequalities):
-        strings = []
-        for equality in equalities:
-            strings.append('{} = 0'.format(equality))
-        for inequality in inequalities:
-            strings.append('{} <= 0'.format(inequality))
-        string = '{{ [{}] : {} }}'.format(', '.join(symbols), ' and '.join(strings))
-        return string
-
     def _toiscc(self, symbols):
-        return self._isccpoly(symbols, self.equalities, self.inequalities)
+        return _iscc.set(symbols, self.equalities, self.inequalities)
 
     @classmethod
     def _fromiscc(cls, symbols, string):
         if re.match(r'^\s*\{\s*\}\s*$', string):
             return empty
         self = super().__new__(cls)
-        self._symbols = symbols
+        self._symbols = _strsymbols(symbols)
         self._equalities = []
         self._inequalities = []
         string = re.sub(r'^\s*\{\s*(.*?)\s*\}\s*$', lambda m: m.group(1), string)
@@ -399,7 +428,7 @@ class Polyhedron:
     def __eq__(self, other):
         symbols = set(self.symbols()) | set(other.symbols())
         string = '{} = {}'.format(self._toiscc(symbols), other._toiscc(symbols))
-        string = _iscc(string)
+        string = _iscc.eval(string)
         return string == 'True'
 
     def isempty(self):
@@ -415,7 +444,7 @@ class Polyhedron:
     def issubset(self, other):
         symbols = set(self.symbols()) | set(other.symbols())
         string = '{} <= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
-        string = _iscc(string)
+        string = _iscc.eval(string)
         return string == 'True'
 
     def __le__(self, other):
@@ -424,14 +453,14 @@ class Polyhedron:
     def __lt__(self, other):
         symbols = set(self.symbols()) | set(other.symbols())
         string = '{} < {}'.format(self._toiscc(symbols), other._toiscc(symbols))
-        string = _iscc(string)
+        string = _iscc.eval(string)
         return string == 'True'
 
     def issuperset(self, other):
         # test whether every element in other is in the polyhedron
         symbols = set(self.symbols()) | set(other.symbols())
         string = '{} >= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
-        string = _iscc(string)
+        string = _iscc.eval(string)
         return string == 'True'
 
     def __ge__(self, other):
@@ -440,7 +469,7 @@ class Polyhedron:
     def __gt__(self, other):
         symbols = set(self.symbols() + other.symbols())
         string = '{} > {}'.format(self._toiscc(symbols), other._toiscc(symbols))
-        string = _iscc(string)
+        string = _iscc.eval(string)
         return string == 'True'
 
     def union(self, *others):
@@ -454,7 +483,7 @@ class Polyhedron:
         for other in others:
             strings.append(other._toiscc(symbols))
         string = ' + '.join(strings)
-        string = _iscc('poly ({})'.format(string))
+        string = _iscc.eval('poly ({})'.format(string))
         return Polyhedron._fromiscc(symbols, string)
 
     def __or__(self, other):
@@ -469,7 +498,7 @@ class Polyhedron:
         for other in others:
             strings.append(other._toiscc(symbols))
         string = ' * '.join(strings)
-        string = _iscc('poly ({})'.format(string))
+        string = _iscc.eval('poly ({})'.format(string))
         return Polyhedron._fromiscc(symbols, string)
 
     def __and__(self, other):
@@ -486,12 +515,22 @@ class Polyhedron:
         for other in others:
             strings.append(other._toiscc(symbols))
         string = ' - '.join(strings)
-        string = _iscc('poly ({})'.format(string))
+        string = _iscc.eval('poly ({})'.format(string))
         return Polyhedron._fromiscc(symbols, string)
 
     def __sub__(self, other):
         return self.difference(other)
 
+    def projection(self, symbols):
+        symbols = _strsymbols(symbols)
+        string = _iscc.map(symbols, self.symbols(),
+                self.equalities, self.inequalities)
+        string = _iscc.eval('poly (dom ({}))'.format(string))
+        return Polyhedron._fromiscc(symbols, string)
+
+    def __getitem__(self, symbol):
+        return self.projection([symbol])
+
     def __repr__(self):
         constraints = []
         for constraint in self.equalities:
@@ -510,3 +549,12 @@ class Polyhedron:
 empty = Eq(1, 0)
 
 universe = Polyhedron()
+
+
+if __name__ == '__main__':
+    x, y, z = symbols('x y z')
+    sq0 = (0 <= x) & (x <= 1) & (0 <= y) & (y <= 1)
+    sq1 = (1 <= x) & (x <= 2) & (1 <= y) & (y <= 2)
+    print('sq0 ∪ sq1 =', sq0 | sq1)
+    print('sq0 ∩ sq1 =', sq0 & sq1)
+    print('sq0[x] =', sq0[x])