A categorical programming language
リビジョン | 06d54b6826960957451cbd73a9f8ab2602805f66 (tree) |
---|---|
日時 | 2024-11-25 06:23:56 |
作者 | Corbin <cds@corb...> |
コミッター | Corbin |
Allow pairing of domains.
I'm so pissed that I couldn't do this in a nice generic fashion. This
works, but it's ugly and verbose.
@@ -1,3 +1,7 @@ | ||
1 | +import inspect | |
2 | + | |
3 | +from rpython.rlib.objectmodel import import_from_mixin | |
4 | + | |
1 | 5 | class InvalidCammy(Exception): |
2 | 6 | def __init__(self, message): self.message = message |
3 | 7 |
@@ -23,7 +27,7 @@ class Cammy(object): | ||
23 | 27 | def uncurry(self, arr): pass |
24 | 28 | # natural numbers object |
25 | 29 | def nat(self, k): pass |
26 | - def succ(self, arr): pass | |
30 | + def succ(self): pass | |
27 | 31 | def pr(self, f, g): pass |
28 | 32 | # ordinal objects |
29 | 33 | def ord(self, k, n): pass |
@@ -85,3 +89,48 @@ class Cammy(object): | ||
85 | 89 | self.curry(self.comp([self.tuple([self.app(), |
86 | 90 | self.snd()]), |
87 | 91 | self.n_add()])))) |
92 | + | |
93 | + | |
94 | +def PairOf(d1, d2): | |
95 | + class PairDomain(object): | |
96 | + import_from_mixin(Cammy) | |
97 | + def __init__(self, d1, d2): | |
98 | + self.d1 = d1 | |
99 | + self.d2 = d2 | |
100 | + | |
101 | + def hole(self, i): return self.d1.hole(i), self.d2.hole(i) | |
102 | + def substitute(self, args): | |
103 | + return (self.d1.substitute([arg[0] for arg in args]), | |
104 | + self.d2.substitute([arg[1] for arg in args])) | |
105 | + def comp(self, arrs): | |
106 | + return (self.d1.comp([arr[0] for arr in arrs]), | |
107 | + self.d2.comp([arr[1] for arr in arrs])) | |
108 | + def project(self, k, n): | |
109 | + return self.d1.project(k, n), self.d2.project(k, n) | |
110 | + def tuple(self, arrs): | |
111 | + return (self.d1.tuple([arr[0] for arr in arrs]), | |
112 | + self.d2.tuple([arr[1] for arr in arrs])) | |
113 | + def inject(self, k, n): | |
114 | + return self.d1.inject(k, n), self.d2.inject(k, n) | |
115 | + def case(self, arrs): | |
116 | + return (self.d1.case([arr[0] for arr in arrs]), | |
117 | + self.d2.case([arr[1] for arr in arrs])) | |
118 | + def curry(self, arr): | |
119 | + return self.d1.curry(arr[0]), self.d2.curry(arr[1]) | |
120 | + def uncurry(self, arr): | |
121 | + return self.d1.uncurry(arr[0]), self.d2.uncurry(arr[1]) | |
122 | + def nat(self, k): return self.d1.nat(k), self.d2.nat(k) | |
123 | + def pr(self, f, g): | |
124 | + return self.d1.pr(f[0], g[0]), self.d2.pr(f[1], g[1]) | |
125 | + def ord(self, k, n): return self.d1.ord(k, n), self.d2.ord(k, n) | |
126 | + def fold(self, f, g): | |
127 | + return self.d1.fold(f[0], g[0]), self.d2.fold(f[1], g[1]) | |
128 | + def tfold(self, f, g): | |
129 | + return self.d1.tfold(f[0], g[0]), self.d2.tfold(f[1], g[1]) | |
130 | + | |
131 | + for verb, meth in inspect.getmembers(Cammy, inspect.ismethod): | |
132 | + if verb.startswith("__"): continue | |
133 | + argspec = inspect.getargspec(meth) | |
134 | + if len(argspec[0]) != 1: continue | |
135 | + exec """def {verb}(self): return self.d1.{verb}(), self.d2.{verb}()""".format(verb=verb) | |
136 | + return PairDomain(d1, d2) |
@@ -6,6 +6,7 @@ from rpython.rlib.rfile import create_stdio | ||
6 | 6 | |
7 | 7 | from cammylib.cam import CompileToCAM |
8 | 8 | from cammylib.elements import T, N |
9 | +from cammylib.mixins import PairOf | |
9 | 10 | from cammylib.parser import makeParser, ParseError |
10 | 11 | from cammylib.sexp import Atom, Functor |
11 | 12 | from cammylib.types import TypeCheck, ConstraintStore, TypeExtractor, TypeFormatter, UnificationFailed, fixDomain |
@@ -68,12 +69,13 @@ class PrintHelp(Command): | ||
68 | 69 | |
69 | 70 | parseAndTypeCheck = makeParser("TypeChecker", TypeCheck()) |
70 | 71 | parseToCAM = makeParser("Compiler", CompileToCAM()) |
72 | +parseToBoth = makeParser("TypeCheckAndCompile", | |
73 | + PairOf(TypeCheck(), CompileToCAM())) | |
71 | 74 | |
72 | 75 | class EvaluateElement(Command): |
73 | 76 | doc = "Evaluate an element or sequence. Elements are arrows from 1; sequences are elements from N." |
74 | 77 | def run(self, line): |
75 | - subst, trail = parseAndTypeCheck(line) | |
76 | - ca, trail = parseToCAM(line) | |
78 | + (subst, ca), trail = parseToBoth(line) | |
77 | 79 | # If the arrow is polymorphic, monomorphize it. |
78 | 80 | if fixDomain(subst, Atom("1")): printElement(ca.finish()) |
79 | 81 | # Maybe it's a sequence? |