提交: 876b22629fa5fb390cc8631027af540dc08c734b - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 876b22629fa5fb390cc8631027af540dc08c734b (tree)
• 时间: 2022-03-09 10:16:42
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Clean up pretty-printing for types.

更改概述

• modified: cammy-rpy/cammylib/sexp.py
• modified: cammy-rpy/cammylib/types.py
• modified: cammy-rpy/repl.py
• modified: cammy-rpy/weave.py
• add: hive/baire/add.cammy
• add: hive/baire/omega.cammy
• modified: hive/int/is_zero.cammy
• modified: hive/int/neg.cammy
• modified: hive/int/succ.cammy
• modified: hive/int/zero.cammy
• add: hive/nat/1.cammy
• modified: hive/nat/eq.cammy
• add: hive/nat/pred-maybe.cammy
• modified: hive/nat/pred.cammy
• add: hive/scott/bool/false.cammy
• add: hive/sum/swap.cammy

差异

--- a/cammy-rpy/cammylib/sexp.py
+++ b/cammy-rpy/cammylib/sexp.py
@@ -39,12 +39,18 @@ class Atom(SExp):
     def occurs(self, index):
         return False
 
-    def extractType(self, extractor):
+    def extractType(self, extractor, formatter, outerPrecedence):
         return self.symbol
 
     def buildArrow(self):
         return buildUnary(self.symbol)
 
+# Precedence levels for operator-style notation.
+PRECEDENCE = {
+    "hom": 3,
+    "pair": 2,
+    "sum": 1,
+}
 
 class Functor(SExp):
     "A list of S-expressions with a distinguished head."
@@ -77,18 +83,26 @@ class Functor(SExp):
                 return True
         return False
 
-    def extractType(self, extractor):
-        args = [extractor.extract(unhole(arg)) for arg in self.arguments]
+    def extractType(self, extractor, formatter, outerPrecedence):
+        innerPrecedence = PRECEDENCE.get(self.constructor, 0)
+        args = [extractor.extractWithPrecedence(unhole(arg), innerPrecedence)
+                for arg in self.arguments]
         if self.constructor == "hom":
-            return "[%s, %s]" % (args[0], args[1])
+            rv = formatter.formatHom(args[0], args[1])
         elif self.constructor == "pair":
-            return "(%s x %s)" % (args[0], args[1])
+            rv = formatter.formatPair(args[0], args[1])
         elif self.constructor == "sum":
-            return "(%s + %s)" % (args[0], args[1])
+            rv = formatter.formatSum(args[0], args[1])
         elif self.constructor == "list":
-            return "[%s]" % args[0]
+            rv = formatter.formatList(args[0])
         else:
-            assert False, "whoops"
+            assert False, "whoopsie-doodle"
+        # NB: This is traditionally >, not >=
+        # but that forgets required strictness and would be confusing to read
+        if (outerPrecedence >= innerPrecedence and
+            not formatter.resetsBracketsFor(self.constructor)):
+            rv = formatter.parenthesize(rv)
+        return rv
 
     def buildArrow(self):
         args = [arg.buildArrow() for arg in self.arguments]
@@ -115,7 +129,7 @@ class Hole(SExp):
     def occurs(self, index):
         return self.index == index
 
-    def extractType(self, extractor):
+    def extractType(self, extractor, formatter, outerPrecedence):
         return extractor.findTypeAlias(self.index)
 
     def buildArrow(self):

--- a/cammy-rpy/cammylib/types.py
+++ b/cammy-rpy/cammylib/types.py
@@ -80,11 +80,17 @@ class ConstraintStore(object):
                     (vi.asStr(), vj.asStr()))
 
 
+class TypeFormatter(object):
+    """
+    Customize the output of a type-extraction operation.
+    """
+
 LETTERS = "XYZWSTPQ"
 
 class TypeExtractor(object):
-    def __init__(self, cs):
+    def __init__(self, cs, formatter):
         self.cs = cs
+        self.formatter = formatter
         self.d = {}
         self.seen = []
 
@@ -97,13 +103,16 @@ class TypeExtractor(object):
         return self.d[index]
 
     def extract(self, var):
+        return self.extractWithPrecedence(var, 0)
+
+    def extractWithPrecedence(self, var, precedence):
         if var in self.seen:
             # XXX split exceptions?
             raise UnificationFailed("tried to extract infinite type")
         self.seen.append(var)
 
         sexp = self.cs.walk(var)
-        rv = sexp.extractType(self)
+        rv = sexp.extractType(self, self.formatter, precedence)
 
         self.seen.pop()
         return rv

--- a/cammy-rpy/repl.py
+++ b/cammy-rpy/repl.py
@@ -8,10 +8,29 @@ from cammylib.arrows import BuildProblem, T
 from cammylib.hive import Hive, MissingAtom
 from cammylib.jelly import jellify
 from cammylib.parser import parse
-from cammylib.types import ConstraintStore, TypeExtractor, UnificationFailed
+from cammylib.types import ConstraintStore, TypeExtractor, TypeFormatter, UnificationFailed
 
 LINE_BUFFER_LENGTH = 1024
 
+class PlaintextTypeFormatter(TypeFormatter):
+    def resetsBracketsFor(self, constructor):
+        return constructor in ("hom", "list")
+
+    def parenthesize(self, x):
+        return "(%s)" % x
+
+    def formatHom(self, x, y):
+        return "[%s, %s]" % (x, y)
+
+    def formatPair(self, x, y):
+        return "%s x %s" % (x, y)
+
+    def formatSum(self, x, y):
+        return "%s + %s" % (x, y)
+
+    def formatList(self, x):
+        return "[%s]" % x
+
 def command(hive, code, line):
     # XXX code e: Edit a file
     # os.system("$EDITOR")
@@ -51,7 +70,7 @@ def repl(hive, stdin, stdout):
             print "Arrow:", arrow
             cs = ConstraintStore()
             domain, codomain = arrow.types(cs)
-            extractor = TypeExtractor(cs)
+            extractor = TypeExtractor(cs, PlaintextTypeFormatter())
             for i, (gdom, gcod) in enumerate(cs.knownGivens):
                 print "Given @%d : %s -> %s" % (i,
                         extractor.extract(gdom),

--- a/cammy-rpy/weave.py
+++ b/cammy-rpy/weave.py
@@ -7,11 +7,31 @@ from rpython.rlib.listsort import make_timsort_class
 from cammylib.arrows import BuildProblem
 from cammylib.hive import Hive, MissingAtom
 from cammylib.parser import parse
-from cammylib.types import ConstraintStore, TypeExtractor, UnificationFailed
+from cammylib.types import ConstraintStore, TypeExtractor, TypeFormatter, UnificationFailed
 
 
 SortFileNames = make_timsort_class()
 
+class LatexTypeFormatter(TypeFormatter):
+    def resetsBracketsFor(self, constructor):
+        return constructor == "list"
+
+    def parenthesize(self, x):
+        return "( %s )" % x
+
+    def formatHom(self, x, y):
+        return "{ %s }^{ %s }" % (y, x)
+
+    def formatPair(self, x, y):
+        return r"%s \times %s" % (x, y)
+
+    def formatSum(self, x, y):
+        return r"%s + %s" % (x, y)
+
+    def formatList(self, x):
+        return "[ %s ]" % x
+
+
 def codeblock(code):
     return "```\n" + code + "\n```"
 
@@ -45,12 +65,12 @@ def main(argv):
                 arrow = sexp.buildArrow()
                 cs = ConstraintStore()
                 domain, codomain = arrow.types(cs)
-                extractor = TypeExtractor(cs)
+                extractor = TypeExtractor(cs, LatexTypeFormatter())
                 for i, (gdom, gcod) in enumerate(cs.knownGivens):
-                    doc.append("Given @%d : %s -> %s" % (i,
+                    doc.append(r"Given @%d : $%s \to %s$" % (i,
                             extractor.extract(gdom),
                             extractor.extract(gcod)))
-                doc.append("Type: %s -> %s" % (extractor.extract(domain),
+                doc.append(r"Type: $%s \to %s$" % (extractor.extract(domain),
                         extractor.extract(codomain)))
             except MissingAtom as ma:
                 doc.append(

--- /dev/null
+++ b/hive/baire/add.cammy
@@ -0,0 +1,8 @@
+(curry
+  (comp
+    (pair
+      (fun/apppair (comp fst fst) snd)
+      (fun/apppair (comp fst snd) snd))
+    nat/add))
+
+Addition of non-standard natural numbers in Baire space.

--- /dev/null
+++ b/hive/baire/omega.cammy
@@ -0,0 +1,4 @@
+id
+
+As a non-standard natural number, $\omega$ is the smallest natural number
+greater than all standard natural numbers.

--- a/hive/int/is_zero.cammy
+++ b/hive/int/is_zero.cammy
@@ -1 +1,3 @@
-(uncurry nat/eq)
+(case nat/is_zero nat/is_zero)
+
+Whether an integer is zero.

--- a/hive/int/neg.cammy
+++ b/hive/int/neg.cammy
@@ -1 +1,3 @@
-fun/swap
+sum/swap
+
+The negation of an integer.

--- a/hive/int/succ.cammy
+++ b/hive/int/succ.cammy
@@ -1 +1,3 @@
-(pair (comp fst succ) snd)
+(case (comp succ left) (comp nat/pred-maybe (case right (comp nat/1 left))))
+
+The successor of an integer.

--- a/hive/int/zero.cammy
+++ b/hive/int/zero.cammy
@@ -1 +1,3 @@
-(pair zero zero)
+(comp zero left)
+
+The integer zero. For no particular reason, we choose positive zero.

--- /dev/null
+++ b/hive/nat/1.cammy
@@ -0,0 +1,3 @@
+(comp zero succ)
+
+One.

--- a/hive/nat/eq.cammy
+++ b/hive/nat/eq.cammy
@@ -1,3 +1,5 @@
-(pr (curry (comp snd nat/is_zero)) (curry (comp (pair fst (comp snd nat/pred)) fun/app)))
+(uncurry (pr
+  (curry (comp snd nat/is_zero))
+  (curry (comp (pair fst (comp snd nat/pred)) fun/app))))
 
 Equality on natural numbers is decidable.

--- /dev/null
+++ b/hive/nat/pred-maybe.cammy
@@ -0,0 +1,5 @@
+(pr
+  right
+  (comp (case succ zero) left))
+
+The predecessor of a natural number, or a distinguished point for zero.

--- a/hive/nat/pred.cammy
+++ b/hive/nat/pred.cammy
@@ -1 +1,3 @@
 (comp (pr (comp zero fun/dup) (comp fst (pair succ id))) snd)
+
+The predecessor of a natural number. Zero is mapped to itself.

--- /dev/null
+++ b/hive/scott/bool/false.cammy
@@ -0,0 +1 @@
+(curry snd)

--- /dev/null
+++ b/hive/sum/swap.cammy
@@ -0,0 +1,3 @@
+(case right left)
+
+Swap the two cases of a sum.