• R/O
  • HTTP
  • SSH
  • HTTPS

提交

标签
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#objective-cqtwindows誰得cocoapythonphprubygameguibathyscaphec翻訳omegat計画中(planning stage)frameworktwittertestdomvb.netdirectxbtronarduinopreviewerゲームエンジン

A categorical programming language


Commit MetaInfo

修订版aafb1ba08e8b9fac42290dfa12fde188c2813671 (tree)
时间2022-06-20 03:50:32
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Apply jelly to itself to test its quality.

The idea is similar to the Knuth-Bendix algorithm, but including the
possibility that, after E-matching, the source expression is the best
expression; this means that the rule is intentionally explosive and
meant to expose further rewrite opportunities.

更改概述

差异

--- a/accept-jelly.py
+++ b/accept-jelly.py
@@ -1,4 +1,5 @@
11 import json
2+import re
23 import subprocess
34 import sys
45
@@ -7,24 +8,52 @@ jelly = sys.argv[-1]
78 timeout = 5
89 difficulty = 15
910
10-with open("test_canonical.json", "rb") as handle:
11+def jellify(expr):
12+ return subprocess.run([jelly], input=expr.encode("utf-8"),
13+ capture_output=True).stdout.decode("utf-8").strip()
14+
15+# Whether any tests have failed
16+rv = False
17+
18+# Outwit the djinn
19+with open("accept-jelly.json", "rb") as handle:
1120 testCases = json.load(handle)
1221
13-rv = 0
22+print("Asking jelly to solve", len(testCases), "riddles from djinn")
1423 for it, ot, nfs in testCases:
15- print("Ensuring jelly can outwit djinn for all", it, "→", ot)
1624 for diff in range(1, difficulty):
1725 try:
1826 sexp = subprocess.check_output([movelist, it, ot, str(diff)], timeout=timeout)
1927 text = sexp.decode("utf-8").strip()
20- jellied = subprocess.run([jelly], input=text.encode("utf-8"),
21- capture_output=True).stdout.decode("utf-8").strip()
28+ jellied = jellify(text)
2229 if jellied not in nfs:
23- rv = 1
24- print("Unacceptable jelly was insufficiently smart;", jellied,
25- "not in", nfs)
30+ rv = True
31+ print("Unacceptable jelly was insufficiently smart on the topic of",
32+ it, "→", ot, ":", jellied, "not in", nfs)
2633 except subprocess.TimeoutExpired:
27- rv = 1
34+ rv = True
2835 print("Movelist djinn was too creative with", it, "→", ot)
2936
37+# Self-clarify
38+stringPatt = r'"(.*)"'
39+patt = re.compile(r'rw!\(%s; %s => %s\),' % (stringPatt, stringPatt, stringPatt))
40+rules = []
41+with open("jelly/src/main.rs", "r") as handle:
42+ for line in handle:
43+ match = patt.search(line)
44+ if match is not None:
45+ rules.append((match[1], match[2], match[3]))
46+
47+print("Asking jelly whether", len(rules), "rules are sufficiently clear")
48+explosiveRules = 0
49+for name, source, target in rules:
50+ jellied = jellify(source)
51+ if jellied == source:
52+ explosiveRules += 1
53+ elif jellied != target:
54+ print("Unacceptable jelly could improve itself:", source, "→", target,
55+ "→", jellied)
56+ rv = True
57+print(explosiveRules, "rules were explosive")
58+
3059 sys.exit(rv)
--- a/cammy-rpy/repl.py
+++ b/cammy-rpy/repl.py
@@ -71,7 +71,10 @@ def command(hive, code, line, context):
7171 elif code == "n":
7272 # Normalize an arrow.
7373 sexp, trail = parse(line)
74- sexp = sexp.canonicalize(hive)
74+ try:
75+ sexp = sexp.canonicalize(hive)
76+ except MissingAtom as ma:
77+ print "Warning: Atom %s not found; jellifying anyway." % ma.atom
7578 sexp = jellify(sexp)
7679 print sexp.asStr()
7780 elif code == "d":
--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -159,7 +159,7 @@ fn main() -> std::io::Result<()> {
159159 rw!("nat-elim-pr"; "(pr zero succ)" => "id"),
160160 rw!("nat-unroll-pr-zero"; "(comp zero (pr ?x ?f))" => "?x"),
161161 rw!("nat-unroll-pr-succ-post"; "(comp succ (pr ?x ?f))" => "(comp (pr ?x ?f) ?f)"),
162- rw!("nat-unroll-pr-succ-pre"; "(comp succ (pr ?x ?f))" => "(pr (comp ?x ?f) ?f)"),
162+ rw!("nat-shift-pr-endo"; "(comp (pr ?x ?f) ?f)" => "(pr (comp ?x ?f) ?f)"),
163163
164164 // jet for nat/add
165165 rw!("nat-add-jet"; "(pr (curry snd) (curry (comp (uncurry id) succ)))" => "(curry n-add)"),