OSDN > Developer > corbin > Chamber > cammy > 提交

Cammy
Fork

(Original repository, No fork origin)

提交

Implement list fusion.

We are fusing both intermediate lists and partially-consumed lists.

--- a/cammy.txt

+++ b/cammy.txt

		@@ -49,9 +49,9 @@ succ : N → N
49	49	Given x : 1 → X and f : X → X, pr(x, f) : N → X
50	50
51	51	nil : 1 → [X]
52		-cons : X × [X] → X
53		-Given f : X → Y, map(f) : [X] → [Y]
	52	+cons : X × [X] → [X]
54	53	Given x : 1 → Y and f : X × Y → Y, fold(x, f) : [X] → Y
	54	+Given f : X → Y, map(f) = fold(nil, comp(pair(comp(fst, f), snd), cons)) : [X] → [Y]
55	55
56	56	Combinators with (*) are provided by OCaml by default; the others are in a
57	57	stub module. Type-checking is achieved by copying the combinators into

--- /dev/null

+++ b/hive/list/gauss.cammy

		@@ -0,0 +1 @@
	1	+(comp list/range nat/sum)

--- a/jelly/src/main.rs

+++ b/jelly/src/main.rs

		@@ -8,8 +8,14 @@ fn load_tree(handle :&mut Read) -> std::io::Result<RecExpr<SymbolLang>> {
8	8	input.parse().map_err(\|e\| std::io::Error::new(std::io::ErrorKind::InvalidData, e))
9	9	}
10	10
	11	+// Wadler 1989: https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf
11	12	// Conal 2013: http://conal.net/blog/posts/optimizing-cccs
12	13
	14	+// Rules with names ending in "-desugar" are directly transcribed from the underlying equality.
	15	+
	16	+// "free for X" means that the polymorphic type of X implies the underlying equality justifying
	17	+// the annotated rule, as in Wadler 1989.
	18	+
13	19	fn main() -> std::io::Result<()> {
14	20	let rules :&[Rewrite<SymbolLang, ()>] = &[
15	21	rw!("comp-id-left"; "(comp id ?x)" => "?x"),

		@@ -18,23 +24,29 @@ fn main() -> std::io::Result<()> {
18	24
19	25	rw!("ignore-absorb-left"; "(comp ?x ignore)" => "ignore"),
20	26
	27	+ // free for fst
21	28	rw!("fst-elim-pair"; "(comp (pair ?f ?g) fst)" => "?f"),
	29	+ // free for snd
22	30	rw!("snd-elim-pair"; "(comp (pair ?f ?g) snd)" => "?g"),
23	31	rw!("pair-fst-snd"; "(pair fst snd)" => "id"),
24	32	// Conal 2013
25	33	rw!("pair-precompose"; "(pair (comp ?r ?f) (comp ?r ?g))" => "(comp ?r (pair ?f ?g))"),
26	34
	35	+ // free for left
27	36	rw!("left-elim-case"; "(comp left (case ?f ?g))" => "?f"),
	37	+ // free for right
28	38	rw!("right-elim-case"; "(comp right (case ?f ?g))" => "?g"),
29	39	rw!("case-left-right"; "(case left right)" => "id"),
30	40
31	41	rw!("assl-assr-cancel"; "(comp assl assr)" => "id"),
32	42	rw!("assr-assl-cancel"; "(comp assr assl)" => "id"),
33	43
	44	+ // free for swap
34	45	rw!("swap-pair"; "(comp (pair ?f ?g) swap)" => "(pair ?g ?f)"),
35	46	rw!("pair-snd-fst"; "(pair snd fst)" => "swap"),
36	47	rw!("swap-twice-cancel"; "(comp swap swap)" => "id"),
37	48
	49	+ // free for dup
38	50	rw!("dup-factor"; "(pair ?f ?f)" => "(comp ?f dup)"),
39	51	rw!("dup-desugar"; "dup" => "(pair id id)"),
40	52

		@@ -52,6 +64,9 @@ fn main() -> std::io::Result<()> {
52	64	rw!("nat-elim-pr"; "(pr zero succ)" => "id"),
53	65
54	66	rw!("list-elim-fold"; "(fold nil cons)" => "id"),
	67	+
	68	+ rw!("map-desugar"; "(map ?f)" => "(fold nil (comp (pair (comp fst ?f) snd) cons))"),
	69	+ rw!("map-fusion"; "(comp (map ?f) (map ?g))" => "(map (comp ?f ?g))"),
55	70	];
56	71
57	72	let tree = load_tree(&mut std::io::stdin())?;

--- a/todo.txt

+++ b/todo.txt