A categorical programming language
| 修订版 | 8a2fcd2fb7eaf9e75cfad177db7844632eaeac5d (tree) |
|---|---|
| 时间 | 2022-03-25 14:46:16 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Add basic acceptance tests for jelly.
Maybe these should be moved to jelly/ instead?
accept-jelly.py (diff)
default.nix (diff) hive/fifo/about.md (diff) hive/fifo/is_empty.cammy (diff) hive/fifo/nil.cammy (diff) hive/fifo/pop.cammy (diff) hive/fifo/push.cammy (diff) hive/fifo/refill.cammy (diff) hive/fun/depsum.cammy (diff) hive/fun/inv-img.cammy (diff) hive/list/head.cammy (diff) hive/list/is_empty.cammy (diff) hive/list/uncons.cammy (diff) hive/monads/cont/bind.cammy (diff) hive/monads/cont/join.cammy (diff) hive/monads/cont/run.cammy (diff) jelly/src/main.rs (diff) test_canonical.json (diff)| @@ -0,0 +1,30 @@ | ||
| 1 | +import json | |
| 2 | +import subprocess | |
| 3 | +import sys | |
| 4 | + | |
| 5 | +movelist = sys.argv[-2] | |
| 6 | +jelly = sys.argv[-1] | |
| 7 | +timeout = 5 | |
| 8 | +difficulty = 10 | |
| 9 | + | |
| 10 | +with open("test_canonical.json", "rb") as handle: | |
| 11 | + testCases = json.load(handle) | |
| 12 | + | |
| 13 | +rv = 0 | |
| 14 | +for it, ot, nfs in testCases: | |
| 15 | + print("Ensuring jelly can outwit djinn for all", it, "→", ot) | |
| 16 | + for diff in range(1, difficulty): | |
| 17 | + try: | |
| 18 | + sexp = subprocess.check_output([movelist, it, ot, str(diff)], timeout=timeout) | |
| 19 | + 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() | |
| 22 | + if jellied not in nfs: | |
| 23 | + rv = 1 | |
| 24 | + print("Unacceptable jelly was insufficiently smart;", jellied, | |
| 25 | + "not in", nfs) | |
| 26 | + except subprocess.TimeoutExpired: | |
| 27 | + rv = 1 | |
| 28 | + print("Movelist djinn was too creative with", it, "→", ot) | |
| 29 | + | |
| 30 | +sys.exit(rv) |
| @@ -17,6 +17,11 @@ in pkgs.stdenv.mkDerivation { | ||
| 17 | 17 | |
| 18 | 18 | buildInputs = [ pkgs.makeWrapper ]; |
| 19 | 19 | |
| 20 | + doCheck = true; | |
| 21 | + checkPhase = '' | |
| 22 | + ${pkgs.python3}/bin/python accept-jelly.py ${movelist}/bin/movelist ${jelly}/bin/jelly | |
| 23 | + ''; | |
| 24 | + | |
| 20 | 25 | installPhase = '' |
| 21 | 26 | mkdir -p $out/bin/ |
| 22 | 27 |
| @@ -0,0 +1,5 @@ | ||
| 1 | +For any type $X$, the type $[X] \times [X]$ can be interpreted as a | |
| 2 | +[first-in, first-out (FIFO) | |
| 3 | +queue](https://en.wikipedia.org/wiki/Queue_(abstract_data_type)). This type is | |
| 4 | +studied in ["Purely Functional Data Structures", Okasaki | |
| 5 | +1998](https://doc.lagout.org/programmation/Functional%20Programming/Chris_Okasaki-Purely_Functional_Data_Structures-Cambridge_University_Press%281998%29.pdf). |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(pair/of conj (comp fst list/is_empty) (comp snd list/is_empty)) | |
| 2 | + | |
| 3 | +Whether a queue is empty. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(pair nil nil) | |
| 2 | + | |
| 3 | +An empty queue. |
| @@ -0,0 +1,8 @@ | ||
| 1 | +(comp | |
| 2 | + (comp fifo/refill (pair/mapsnd list/uncons)) | |
| 3 | + (comp fun/distribr (case | |
| 4 | + (comp (pair (comp snd fst) (pair fst (comp snd snd))) left) | |
| 5 | + (comp snd right)))) | |
| 6 | + | |
| 7 | +Pop an item from a queue, returning it in the left-hand component. The | |
| 8 | +right-hand component is used to signal an empty queue. |
| @@ -0,0 +1,5 @@ | ||
| 1 | +(pair | |
| 2 | + (comp (pair snd (comp fst fst)) cons) | |
| 3 | + (comp fst snd)) | |
| 4 | + | |
| 5 | +Push a value onto a queue. |
| @@ -0,0 +1,7 @@ | ||
| 1 | +(comp | |
| 2 | + (pair (comp snd list/is_empty) id) | |
| 3 | + (uncurry (bool/if | |
| 4 | + (pair (fun/const nil) (comp fst list/reverse)) | |
| 5 | + id))) | |
| 6 | + | |
| 7 | +Prepare a queue for a pop by refilling the pop stack. |
| @@ -0,0 +1,4 @@ | ||
| 1 | +(comp @1 (pair id @0)) | |
| 2 | + | |
| 3 | +Given a first arrow, give the dependent sum of the second arrow over the | |
| 4 | +first. The dependent sum is merely postcomposition. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(curry (fun/apppair fst (comp snd @0))) | |
| 2 | + | |
| 3 | +The inverse-image functor for an arbitrary classifier. |
| @@ -1 +1,3 @@ | ||
| 1 | -(fold (fun/const right) (comp fst left)) | |
| 1 | +(fold right (comp fst left)) | |
| 2 | + | |
| 3 | +The most exterior constructed value in a list, if it exists. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(fold t (fun/const f)) | |
| 2 | + | |
| 3 | +Whether a list is nil. |
| @@ -0,0 +1,8 @@ | ||
| 1 | +(fold right | |
| 2 | + (comp | |
| 3 | + (pair/mapsnd (comp (case cons nil) left)) | |
| 4 | + (comp fun/distribr (sum/mapright ignore)))) | |
| 5 | + | |
| 6 | +[X] -> (X x [X]) + 1 | |
| 7 | + | |
| 8 | +Try to decompose a list at its extremal cell. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(fun/apppair snd (comp fst monads/cont/run)) | |
| 2 | + | |
| 3 | +Chain continuations together. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(curry (fun/apppair fst (comp snd monads/cont/unit))) | |
| 2 | + | |
| 3 | +Collapse two layers of continuations into one. |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(fun/apppair id (fun/const (fun/name id))) | |
| 2 | + | |
| 3 | +Run a computation with continuations. |
| @@ -117,6 +117,11 @@ fn main() -> std::io::Result<()> { | ||
| 117 | 117 | // IEEE 754 odd functions |
| 118 | 118 | rw!("f-sin-odd-ana"; "(comp f-negate f-sin)" => "(comp f-sin f-negate)"), |
| 119 | 119 | rw!("f-sin-odd-kata"; "(comp f-sin f-negate)" => "(comp f-negate f-sin)"), |
| 120 | + | |
| 121 | + // IEEE 754 constants | |
| 122 | + rw!("f-one-sign"; "(comp f-one f-sign)" => "t"), | |
| 123 | + rw!("f-zero-sign"; "(comp f-zero f-sign)" => "t"), | |
| 124 | + rw!("f-pi-sign"; "(comp f-pi f-sign)" => "t"), | |
| 120 | 125 | ]; |
| 121 | 126 | |
| 122 | 127 | let tree = load_tree(&mut std::io::stdin())?; |
| @@ -0,0 +1,8 @@ | ||
| 1 | +[ | |
| 2 | + ["X", "X", ["id"]], | |
| 3 | + ["(pair X Y)", "X", ["fst"]], | |
| 4 | + ["X", "(pair X X)", ["(pair id id)"]], | |
| 5 | + ["(pair X Y)", "(pair Y X)", ["(pair snd fst)"]], | |
| 6 | + ["(pair (hom X Y) X)", "Y", ["(uncurry id)"]], | |
| 7 | + ["1", "2", ["t", "f"]] | |
| 8 | +] |
Fork