Get simple int -> int function to have its constraints solved

Author: kennknowles

typelanguage/constraintgen.py

@@ -10,6 +10,13 @@ def __init__(self, subtype, supertype):
         self.subtype = subtype
         self.supertype = supertype
 
+    def __str__(self):
+        return '%s <: %s' % (self.subtype, self.supertype)
+
+    def substitute(self, substitution):
+        return Constraint(subtype = self.subtype.substitute(substitution),
+                          supertype = self.supertype.substitute(substitution))
+
 class ConstrainedType(object):
     def __init__(self, type=None, constraints=None):
         self.type = type
@@ -21,10 +28,15 @@ def __init__(self, env=None, constraints=None, return_type=None):
         self.constraints = constraints or []
         self.return_type = return_type
 
+    def substitute(self, substitution):
+        return ConstrainedEnv(env = dict([(key, ty.substitute(substitution)) for key, ty in self.env.items()]),
+                              constraints = [constraint.substitute(substitution) for constraint in self.constraints],
+                              return_type = None if self.return_type is None else self.return_type.substitute(substitution))
+
     def pretty(self):
         return ("Env:\n\t%(bindings)s\n\nConstraints:\n\t%(constraints)s\n\nResult:\n\t%(result)s" % 
                 dict(bindings    = '\n\t'.join(['%s: %s' % (var, ty) for var, ty in self.env.items()]),
-                     constraints = '\n\t'.join(['%s <: %s' % (c.subtype, c.supertype) for c in self.constraints]),
+                     constraints = '\n\t'.join([str(c) for c in self.constraints]),
                      result      = self.return_type))
 
 def constraints(env, pyast):
@@ -113,7 +125,7 @@ def constraints_expr(env, expr):
             raise Exception('Variable not found in environment: %s' % expr.id)
 
     elif isinstance(expr, ast.Num):
-        return ConstrainedType(type=types.AtomicType('int'))
+        return ConstrainedType(type=types.AtomicType('num'))
 
     elif isinstance(expr, ast.BinOp):
         left = constraints_expr(env, expr.left)

typelanguage/constraintsolve.py

@@ -0,0 +1,84 @@
+import sys
+import ast
+import logging
+import copy
+
+from typelanguage import constraintgen
+from typelanguage.types import *
+
+logger = logging.getLogger(__name__)
+
+class Refutation(object):
+    def __init__(self, reason):
+        self.reason = reason
+
+    def __bool__(self):
+        return False
+
+    def __str__(self):
+        return 'Refutation(reason="%s")' % self.reason
+
+def reconcile(constraint):
+    '''
+    Returns an assignment of type variable names to
+    types that makes this constraint satisfiable, or a Refutation
+    '''
+    
+    if isinstance(constraint.subtype, AtomicType):
+        if isinstance(constraint.supertype, AtomicType):
+            if constraint.subtype.name == constraint.supertype.name:
+                return {}
+            else:
+                return Refutation('Cannot reconcile different atomic types: %s' % constraint)
+        elif isinstance(constraint.supertype, TypeVariable):
+            return {constraint.supertype.name: contraint.subtype}
+        else:
+            return Refutation('Cannot reconcile atomic type with non-atomic type: %s' % constraint)
+
+    elif isinstance(constraint.supertype, AtomicType):
+        if isinstance(constraint.subtype, AtomicType):
+            if constraint.subtype.name == constraint.supertype.name:
+                return {}
+            else:
+                return Refutation('Cannot reconcile different atomic types: %s' % constraint)
+        elif isinstance(constraint.subtype, TypeVariable):
+            return {constraint.subtype.name: constraint.supertype}
+        else:
+            return Refutation('Cannot reconcile non-atomic type with atomic type: %s' % constraint)
+    else:
+        raise NotImplementedError('Reconciliation of %s' % constraint)
+
+def solve(constraints):
+    remaining_constraints = copy.copy(constraints)
+    substitution = {}
+    
+    while len(remaining_constraints) > 0:
+        constraint = remaining_constraints.pop()
+        additional_substitution = reconcile(constraint)
+
+        logger.info('reconcile(%s) ==> %s', constraint, additional_substitution)
+    
+
+        if isinstance(additional_substitution, Refutation):
+            return additional_substitution
+        else:
+            substitution.update(additional_substitution)
+
+        remaining_constraints = [c.substitute(additional_substitution) for c in remaining_constraints]
+        
+    return substitution
+
+if __name__ == '__main__':
+    logging.basicConfig()
+    logging.getLogger('').setLevel(logging.DEBUG)
+    
+    with open(sys.argv[1]) as fh:
+        proggy = ast.parse(fh.read())
+
+    cs = constraintgen.constraints({}, proggy)
+    print cs.pretty()
+
+    substitution = solve(cs.constraints)
+    print substitution
+
+    print cs.substitute(substitution).pretty()

typelanguage/types.py

@@ -1,8 +1,29 @@
 from collections import namedtuple, defaultdict
 
 class Type(object): pass
-class AtomicType(Type, namedtuple('AtomicType', ['name'])): pass
-class TypeVariable(Type, namedtuple('TypeVariable', ['name'])): pass
+
+class AtomicType(Type):
+    def __init__(self, name):
+        self.name = name
+
+    def substitute(self, substitution):
+        return self
+
+    def __str__(self):
+        return self.name
+        
+class TypeVariable(Type):
+    def __init__(self, name):
+        self.name = name
+
+    def substitute(self, substitution):
+        if self.name in substitution:
+            return substitution[self.name]
+        else:
+            return self
+
+    def __str__(self):
+        return '?%s' % self.name
 
 class FunctionType(Type):
     def __init__(self, arg_types, return_type, vararg_type=None, kwonly_arg_types=None, kwarg_type=None):
@@ -12,6 +33,13 @@ def __init__(self, arg_types, return_type, vararg_type=None, kwonly_arg_types=No
         self.kwarg_type = kwarg_type
         self.kwonly_arg_types = kwonly_arg_types
 
+    def substitute(self, substitution):
+        return FunctionType(arg_types = [ty.substitute(substitution) for ty in self.arg_types],
+                            return_type = self.return_type.substitute(substitution),
+                            vararg_type = None if self.vararg_type is None else self.vararg_type.substitute(substitution),
+                            kwonly_arg_types = None if self.kwonly_arg_types is None else [ty.substitute(substitution) for ty in self.kwonly_arg_types],
+                            kwarg_type = None if self.kwarg_type is None else self.kwarg_type.substitute(substitution))
+
     def __str__(self):
         comma_separated_bits = [unicode(v) for v in self.arg_types]
 
@@ -31,15 +59,17 @@ def __init__(self, fn, args):
         self.fn = fn
         self.args = args
 
+    def substitute(self, substitution):
+        return TypeApplication(self.fn.substitute(substitution), [ty.substitute(substitution) for ty in self.args])
+
 class UnionType(Type):
     def __init__(self, types):
         self.types = types
 
-
 used_vars = defaultdict(lambda: 0)
 def fresh(prefix=None):
     global used_vars
-    prefix = prefix or '?X'
+    prefix = prefix or 'X'
     used_vars[prefix] = used_vars[prefix] + 1
-    return prefix + str(used_vars[prefix])
+    return TypeVariable(prefix + str(used_vars[prefix]))