A categorical programming language
| 修订版 | ec83ededb658caa34976ba08e197fb26a396b8c1 (tree) |
|---|---|
| 时间 | 2022-02-28 08:18:51 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Typecheck functors with holes.
It might feel a little hacky to allow non-exectuable arrow subclasses,
but I'm thinking of it this way: execution is only one thing an arrow
can do, and symbolic logic doesn't end after arrows are built.
cammy-rpy/cammylib/arrows.py (diff) cammy-rpy/cammylib/sexp.py (diff) cammy-rpy/cammylib/types.py (diff) cammy-rpy/repl.py (diff) cammy-rpy/weave.py (diff)| @@ -520,6 +520,18 @@ def buildCompound(name, args): | ||
| 520 | 520 | else: |
| 521 | 521 | raise BuildProblem("Invalid compound functor: " + name) |
| 522 | 522 | |
| 523 | + | |
| 524 | +class Given(Arrow): | |
| 525 | + """ | |
| 526 | + A formal parameter for a function. | |
| 527 | + | |
| 528 | + An given arrow is not executable, but it can still be typechecked. | |
| 529 | + """ | |
| 530 | + _immutable_ = True | |
| 531 | + def __init__(self, index): self.index = index | |
| 532 | + def run(self, x): raise BuildProblem("given arrow cannot be run") | |
| 533 | + def types(self, cs): return cs.givens(self.index) | |
| 534 | + | |
| 523 | 535 | def buildArrow(sexp): |
| 524 | 536 | if isinstance(sexp, Atom): |
| 525 | 537 | return buildUnary(sexp.symbol) |
| @@ -527,6 +539,6 @@ def buildArrow(sexp): | ||
| 527 | 539 | args = [buildArrow(arg) for arg in sexp.arguments] |
| 528 | 540 | return buildCompound(sexp.constructor, args) |
| 529 | 541 | elif isinstance(sexp, Hole): |
| 530 | - raise BuildProblem("Holes cannot become arrows") | |
| 542 | + return Given(sexp.index) | |
| 531 | 543 | else: |
| 532 | 544 | assert False, "inconceivable" |
| @@ -38,7 +38,7 @@ class Atom(SExp): | ||
| 38 | 38 | class Functor(SExp): |
| 39 | 39 | "A list of S-expressions with a distinguished head." |
| 40 | 40 | |
| 41 | - _immutable_fields_ = "constructor", "arguments[:]", | |
| 41 | + _immutable_fields_ = "constructor", "arguments[:]" | |
| 42 | 42 | |
| 43 | 43 | def __init__(self, constructor, arguments): |
| 44 | 44 | self.constructor = constructor |
| @@ -33,6 +33,12 @@ class ConstraintStore(object): | ||
| 33 | 33 | def __init__(self): |
| 34 | 34 | self.i = 0 |
| 35 | 35 | self.constraints = [] |
| 36 | + self.knownGivens = [] | |
| 37 | + | |
| 38 | + def givens(self, index): | |
| 39 | + while len(self.knownGivens) <= index: | |
| 40 | + self.knownGivens.append((self.fresh(), self.fresh())) | |
| 41 | + return self.knownGivens[index] | |
| 36 | 42 | |
| 37 | 43 | def fresh(self): |
| 38 | 44 | rv = self.i |
| @@ -43,6 +43,10 @@ def repl(hive, stdin, stdout): | ||
| 43 | 43 | cs = ConstraintStore() |
| 44 | 44 | domain, codomain = arrow.types(cs) |
| 45 | 45 | extractor = TypeExtractor() |
| 46 | + for i, (gdom, gcod) in enumerate(cs.knownGivens): | |
| 47 | + print "Given @%d : %s -> %s" % (i, | |
| 48 | + extractor.extractType(cs, gdom), | |
| 49 | + extractor.extractType(cs, gcod)) | |
| 46 | 50 | print "Type:", extractor.extractType(cs, domain), "->", extractor.extractType(cs, codomain) |
| 47 | 51 | except BuildProblem as bp: |
| 48 | 52 | print "Couldn't build arrow:", bp.message |
| @@ -39,6 +39,10 @@ def main(argv): | ||
| 39 | 39 | cs = ConstraintStore() |
| 40 | 40 | domain, codomain = arrow.types(cs) |
| 41 | 41 | extractor = TypeExtractor() |
| 42 | + for i, (gdom, gcod) in enumerate(cs.knownGivens): | |
| 43 | + doc.append("Given @%d : %s -> %s" % (i, | |
| 44 | + extractor.extractType(cs, gdom), | |
| 45 | + extractor.extractType(cs, gcod))) | |
| 42 | 46 | doc.append("Type: %s -> %s" % (extractor.extractType(cs, domain), |
| 43 | 47 | extractor.extractType(cs, codomain))) |
| 44 | 48 | except MissingAtom as ma: |
Fork