• 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

修订版e21733b4da08158e929ad5321466f3e3cfcd2c36 (tree)
时间2022-06-16 12:51:11
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Add swap and dup to movelist, and enrich jelly.

更改概述

差异

--- /dev/null
+++ b/hive/app-pair-at-point.cammy
@@ -0,0 +1 @@
1+(fun/apppair fstsnd (pair fstfst snd))
\ No newline at end of file
--- /dev/null
+++ b/hive/mogensen-eval.cammy
@@ -0,0 +1 @@
1+(fun/apppair id (comp (fun/const (fun/name id)) dup))
\ No newline at end of file
--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -111,9 +111,14 @@ fn main() -> std::io::Result<()> {
111111
112112 // jet for pair/dup
113113 rw!("pair-dup-jet"; "(pair id id)" => "dup"),
114+ rw!("dup-pair-deopt"; "dup" => "(pair id id)"),
115+ rw!("dup-absorb-swap"; "(comp dup swap)" => "dup"),
116+ rw!("dup-elim-fst"; "(comp dup fst)" => "id"),
117+ rw!("dup-elim-snd"; "(comp dup snd)" => "id"),
114118 // jet for pair/swap
115119 rw!("pair-swap-jet"; "(pair snd fst)" => "swap"),
116- rw!("dup-absorb-swap"; "(comp dup swap)" => "dup"),
120+ rw!("swap-fst"; "(comp swap fst)" => "snd"),
121+ rw!("swap-snd"; "(comp swap snd)" => "fst"),
117122
118123 // This implies the old rule pair-swap-invo: (comp pair/swap pair/swap) => id
119124 // So, like pair-swap-invo, this turns braided products into symmetric products.
@@ -144,6 +149,13 @@ fn main() -> std::io::Result<()> {
144149 // This is a more powerful form of beta when ?x is (uncurry ...)
145150 rw!("beta-fuse"; "(comp (pair ?x ?y) (uncurry ?f))" => "(comp (pair (comp ?x ?f) ?y) (uncurry id))"),
146151
152+ rw!("curry-const"; "(comp ?f (curry (comp fst ?g)))" => "(curry (comp fst (comp ?f ?g)))"),
153+ // curry-const when ?g is id
154+ rw!("curry-const-delay"; "(comp ?f (curry fst))" => "(curry (comp fst ?f))"),
155+ rw!("curry-ignore"; "(comp ?f (curry (comp snd ?g)))" => "(curry (comp snd ?g))"),
156+ // curry-ignore when ?g is id
157+ rw!("curry-ignore-name"; "(comp ?f (curry snd))" => "(curry snd)"),
158+
147159 rw!("nat-elim-pr"; "(pr zero succ)" => "id"),
148160 rw!("nat-unroll-pr-zero"; "(comp zero (pr ?x ?f))" => "?x"),
149161 rw!("nat-unroll-pr-succ-post"; "(comp succ (pr ?x ?f))" => "(comp (pr ?x ?f) ?f)"),
@@ -167,6 +179,20 @@ fn main() -> std::io::Result<()> {
167179 rw!("bool-f-not"; "(comp f not)" => "t"),
168180 rw!("bool-not-invo"; "(comp not not)" => "id"),
169181
182+ // Boolean operations
183+ rw!("conj-comm"; "(comp swap conj)" => "conj"),
184+ rw!("disj-comm"; "(comp swap disj)" => "disj"),
185+
186+ // Some Boolean gates
187+ rw!("bool-conj-f-fst"; "(comp (pair f ?b) conj)" => "f"),
188+ rw!("bool-conj-t-fst"; "(comp (pair t ?b) conj)" => "?b"),
189+ rw!("bool-conj-f-snd"; "(comp (pair ?b f) conj)" => "f"),
190+ rw!("bool-conj-t-snd"; "(comp (pair ?b t) conj)" => "?b"),
191+ rw!("bool-disj-f-fst"; "(comp (pair f ?b) disj)" => "?b"),
192+ rw!("bool-disj-t-fst"; "(comp (pair t ?b) disj)" => "t"),
193+ rw!("bool-disj-f-snd"; "(comp (pair ?b f) disj)" => "?b"),
194+ rw!("bool-disj-t-snd"; "(comp (pair ?b t) disj)" => "t"),
195+
170196 // IEEE 754 addition
171197 rw!("f-add-comm"; "(comp swap f-add)" => "f-add"),
172198 rw!("f-add-unit-left"; "(comp (pair ?f f-zero) f-add)" => "?f"),
--- a/movelist/movelist.scm
+++ b/movelist/movelist.scm
@@ -44,6 +44,9 @@
4444 ; Binary Products
4545 ((== expr 'fst) (fresh (x) (== s (list 'pair t x))))
4646 ((== expr 'snd) (fresh (x) (== s (list 'pair x t))))
47+ ((== expr 'dup) (== t (list 'pair s s)))
48+ ((== expr 'swap) (fresh (x y)
49+ (== s (list 'pair x y)) (== t (list 'pair y x))))
4750 ((fresh (f g p1 p2) (== expr (list 'pair f g))
4851 (== t (list 'pair p1 p2)) (cammyo f s p1) (cammyo g s p2)))
4952 ; Binary Sums
@@ -79,11 +82,6 @@
7982 (fresh (sub1 sub2)
8083 (=/= (list f g) (list 'right (list 'case sub1 sub2))))
8184 (cammyo f s y) (cammyo g y t)))
82- ; Hax: Synthesize swaps.
83- ((fresh (f p1 p2)
84- (== expr (list 'comp '(pair snd fst) f))
85- (== s (list 'pair p1 p2))
86- (cammyo f (list 'pair p2 p1) t)))
8785 )
8886 ; (project (expr s t) (begin (pp (list 'exit expr s t)) succeed))
8987 ))