コミット: f89591928cda9053c1baaa0ff6252d2465c40a95 - cammy (git)

A categorical programming language

コミットメタ情報

• リビジョン: f89591928cda9053c1baaa0ff6252d2465c40a95 (tree)
• 日時: 2022-02-27 13:21:36
• 作者: Corbin <cds@corb...>
• コミッター: Corbin

ログメッセージ

Get the typechecker to emit reasonable output.

変更サマリ

• modified: cammy-rpy/cammylib/arrows.py
• modified: cammy-rpy/cammylib/hive.py
• modified: cammy-rpy/cammylib/types.py
• modified: cammy-rpy/repl.py
• modified: cammy-rpy/weave.py

差分

--- a/cammy-rpy/cammylib/arrows.py
+++ b/cammy-rpy/cammylib/arrows.py
@@ -192,7 +192,7 @@ class Case(Arrow):
         fdom, fcod = self.f.types(cs)
         gdom, gcod = self.g.types(cs)
         cs.unify(fcod, gcod)
-        return fdom, cs.functor("sum", [fdom, gdom])
+        return cs.functor("sum", [fdom, gdom]), fdom
 
 class Curry(Arrow):
     _immutable_ = True
@@ -519,16 +519,12 @@ def buildCompound(name, args):
         raise BuildProblem("Invalid compound functor: " + name)
 
 def buildArrow(sexp):
-    try:
-        if isinstance(sexp, Atom):
-            return buildUnary(sexp.symbol)
-        elif isinstance(sexp, Functor):
-            args = [buildArrow(arg) for arg in sexp.arguments]
-            return buildCompound(sexp.constructor, args)
-        elif isinstance(sexp, Hole):
-            raise BuildProblem("Holes cannot become arrows")
-        else:
-            assert False, "inconceivable"
-    except BuildProblem as bp:
-        print "Couldn't build Cammy expression:", bp.message
-        raise
+    if isinstance(sexp, Atom):
+        return buildUnary(sexp.symbol)
+    elif isinstance(sexp, Functor):
+        args = [buildArrow(arg) for arg in sexp.arguments]
+        return buildCompound(sexp.constructor, args)
+    elif isinstance(sexp, Hole):
+        raise BuildProblem("Holes cannot become arrows")
+    else:
+        assert False, "inconceivable"

--- a/cammy-rpy/cammylib/hive.py
+++ b/cammy-rpy/cammylib/hive.py
@@ -18,15 +18,18 @@ class Hive(object):
         self.exprs = {}
 
     def load(self, atom):
+        if atom in self.exprs:
+            return self.exprs[atom]
+
         # print("Loading", atom)
         filename = atom + ".cammy"
         fullpath = os.path.join(self.hivepath, filename)
-        with open(fullpath, "r") as handle:
-            try:
+        try:
+            with open(fullpath, "r") as handle:
                 sexp, trail = parse(handle.read())
                 sexp = sexp.canonicalize(self)
                 self.exprs[atom] = sexp
                 # print("Loaded", atom, sexp)
                 return sexp
-            except IOError:
-                raise MissingAtom(atom)
+        except IOError:
+            raise MissingAtom(atom)

--- a/cammy-rpy/cammylib/types.py
+++ b/cammy-rpy/cammylib/types.py
@@ -4,6 +4,29 @@ class UnificationFailed(Exception):
     def __init__(self, message):
         self.message = message
 
+def occurs(index, var):
+    if isinstance(var, Hole):
+        return var.index == index
+    elif isinstance(var, Atom):
+        return False
+    elif isinstance(var, Functor):
+        for arg in var.arguments:
+            if occurs(index, arg):
+                return True
+        return False
+    else:
+        assert False, "impossible"
+
+def occursCheck(index, var):
+    "If an index occurs in a variable, raise an error."
+    if occurs(index, var):
+        raise UnificationFailed("Occurs check: %d in %s" %
+                (index, var.asStr()))
+
+def unhole(sexp):
+    assert isinstance(sexp, Hole), "implementation error"
+    return sexp.index
+
 class ConstraintStore(object):
     "A Kanren-style constraint store."
 
@@ -30,31 +53,24 @@ class ConstraintStore(object):
         self.constraints.append(Functor(constructor, args))
         return rv
 
-    def walkArg(self, var):
-        if isinstance(var, Atom):
-            return var
-        elif isinstance(var, Functor):
-            return Functor(var.constructor,
-                    [self.walkArg(arg) for arg in var.arguments])
-        elif isinstance(var, Hole):
-            return self.walk(var.index)
-        assert False, "impossible"
-
     def walk(self, i):
         var = self.constraints[i]
-        if isinstance(var, Hole) and var.index == i:
-            return var
+        if isinstance(var, Hole) and var.index != i:
+            return self.walk(var.index)
         else:
-            return self.walkArg(var)
+            return var
 
     def unify(self, i, j):
-        return self.unifyArg(self.walk(i), self.walk(j))
-
-    def unifyArg(self, vi, vj):
-        print "unifying", vi.asStr(), vj.asStr()
+        vi = self.walk(i)
+        vj = self.walk(j)
+        # print "unifying", vi.asStr(), vj.asStr()
         if isinstance(vi, Hole):
+            if isinstance(vj, Hole) and vi.index == vj.index:
+                return
+            occursCheck(vi.index, vj)
             self.constraints[vi.index] = vj
         elif isinstance(vj, Hole):
+            occursCheck(vj.index, vi)
             self.constraints[vj.index] = vi
         elif isinstance(vi, Atom) and isinstance(vj, Atom):
             if vi.symbol != vj.symbol:
@@ -69,29 +85,40 @@ class ConstraintStore(object):
             if len(vi.arguments) != len(vj.arguments):
                 raise UnificationFailed("Compound types have different arity?")
             for i, argi in enumerate(vi.arguments):
-                self.unifyArg(argi, vj.arguments[i])
+                self.unify(unhole(argi), unhole(vj.arguments[i]))
         else:
             raise UnificationFailed("Quite different types: %s. vs %s" %
                     (vi.asStr(), vj.asStr()))
 
-def formatType(sexp):
-    if isinstance(sexp, Hole):
-        return "_%d" % sexp.index
-    elif isinstance(sexp, Atom):
-        return sexp.symbol
-    elif isinstance(sexp, Functor):
-        if sexp.constructor == "hom":
-            return "[%s, %s]" % (formatType(sexp.arguments[0]),
-                    formatType(sexp.arguments[1]))
-        elif sexp.constructor == "pair":
-            return "(%s x %s)" % (formatType(sexp.arguments[0]),
-                    formatType(sexp.arguments[1]))
-        elif sexp.constructor == "sum":
-            return "(%s + %s)" % (formatType(sexp.arguments[0]),
-                    formatType(sexp.arguments[1]))
-        elif sexp.constructor == "list":
-            return "[%s]" % formatType(sexp.arguments[0])
+
+LETTERS = "XYZWSTPQ"
+
+class TypeExtractor(object):
+    def __init__(self):
+        self.d = {}
+
+    def addTypeAlias(self, index):
+        self.d[index] = LETTERS[len(self.d)]
+
+    def extractType(self, cs, var):
+        sexp = cs.walk(var)
+        if isinstance(sexp, Hole):
+            if sexp.index not in self.d:
+                self.addTypeAlias(sexp.index)
+            return self.d[sexp.index]
+        elif isinstance(sexp, Atom):
+            return sexp.symbol
+        elif isinstance(sexp, Functor):
+            args = [self.extractType(cs, unhole(arg)) for arg in sexp.arguments]
+            if sexp.constructor == "hom":
+                return "[%s, %s]" % (args[0], args[1])
+            elif sexp.constructor == "pair":
+                return "(%s x %s)" % (args[0], args[1])
+            elif sexp.constructor == "sum":
+                return "(%s + %s)" % (args[0], args[1])
+            elif sexp.constructor == "list":
+                return "[%s]" % args[0]
+            else:
+                assert False, "whoops"
         else:
-            assert False, "whoops"
-    else:
-        assert False, "not whoops"
+            assert False, "not whoops"

--- a/cammy-rpy/repl.py
+++ b/cammy-rpy/repl.py
@@ -8,7 +8,7 @@ from rpython.rlib.rfile import create_stdio
 from cammylib.arrows import buildArrow, BuildProblem
 from cammylib.hive import Hive, MissingAtom
 from cammylib.parser import parse
-from cammylib.types import ConstraintStore, formatType, UnificationFailed
+from cammylib.types import ConstraintStore, TypeExtractor, UnificationFailed
 
 LINE_BUFFER_LENGTH = 1024
 
@@ -42,7 +42,8 @@ def repl(hive, stdin, stdout):
             print "Arrow:", arrow
             cs = ConstraintStore()
             domain, codomain = arrow.types(cs)
-            print "Type:", formatType(cs.walk(domain)), "->", formatType(cs.walk(codomain))
+            extractor = TypeExtractor()
+            print "Type:", extractor.extractType(cs, domain), "->", extractor.extractType(cs, codomain)
         except BuildProblem as bp:
             print "Couldn't build arrow:", bp.message
         except UnificationFailed as uf:

--- a/cammy-rpy/weave.py
+++ b/cammy-rpy/weave.py
@@ -1,7 +1,10 @@
 import os
 import os.path
 
+from cammylib.arrows import buildArrow, BuildProblem
+from cammylib.hive import Hive, MissingAtom
 from cammylib.parser import parse
+from cammylib.types import ConstraintStore, TypeExtractor, UnificationFailed
 
 
 def codeblock(code):
@@ -9,6 +12,7 @@ def codeblock(code):
 
 def main(argv):
     hivepath = argv[-1]
+    hive = Hive(hivepath)
     if not hivepath.endswith(os.sep):
         hivepath += os.sep
     prefix = len(hivepath)
@@ -29,6 +33,22 @@ def main(argv):
 
             doc.append("## " + atom)
             doc.append(codeblock(sexp.asStr()))
+            try:
+                sexp = sexp.canonicalize(hive)
+                arrow = buildArrow(sexp)
+                cs = ConstraintStore()
+                domain, codomain = arrow.types(cs)
+                extractor = TypeExtractor()
+                doc.append("Type: %s -> %s" % (extractor.extractType(cs, domain),
+                        extractor.extractType(cs, codomain)))
+            except MissingAtom as ma:
+                doc.append(
+                    "(Couldn't canonicalize due to missing expression %s)" %
+                    ma.atom)
+            except BuildProblem:
+                doc.append("(Couldn't build arrow)")
+            except UnificationFailed as uf:
+                doc.append("(Couldn't typecheck: %s)" % uf.message)
             if trail:
                 doc.append(trail)
     print "\n\n".join(doc)