• 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

修订版57f59678c0c295d584d39e2e6cf13ea7ea9a19fa (tree)
时间2022-07-12 09:35:51
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Teach movelist about app, and improve jelly in tandem.

更改概述

差异

--- /dev/null
+++ b/hive/bits/morton-fst.cammy
@@ -0,0 +1 @@
1+(comp list/every-other snd)
\ No newline at end of file
--- /dev/null
+++ b/hive/list/every-other.cammy
@@ -0,0 +1 @@
1+(fold (pair f nil) (comp pair/rotl (uncurry (bool/if (pair (fun/const f) snd) (pair (fun/const t) cons)))))
\ No newline at end of file
--- /dev/null
+++ b/hive/morton-spread.cammy
@@ -0,0 +1 @@
1+(fold nil (comp cons (pair/of cons (fun/const f) id)))
\ No newline at end of file
--- /dev/null
+++ b/hive/pair/rotl.cammy
@@ -0,0 +1 @@
1+(comp pair/assl (comp (pair/mapfst swap) pair/assr))
\ No newline at end of file
--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -66,6 +66,7 @@ impl CostFunction<SymbolLang> for CAMCostModel {
6666 // opportunities.
6767
6868 // "jet for X" means that expression X in the hive should be replaced by the annotated rule.
69+// "implied by jet R" means that rule R introduces new critical pairs which need reduction.
6970
7071 // Rules marked "associative!" can cause explosions.
7172
@@ -143,6 +144,8 @@ fn main() -> std::io::Result<()> {
143144
144145 // jet for app
145146 rw!("app-jet"; "(uncurry id)" => "app"),
147+ // Implied by jet app-jet
148+ rw!("curry-app"; "(curry app)" => "id"),
146149 rw!("beta-full"; "(comp (pair (comp ?x (curry ?f)) ?y) app)" => "(comp (pair ?x ?y) ?f)"),
147150 // Cousineau, Curien, & Mauny 1987
148151 // beta-full when ?x is id
--- a/movelist/movelist.scm
+++ b/movelist/movelist.scm
@@ -32,6 +32,8 @@
3232 ((== expr 'f-sqrt) (== s 'F) (== t (list 'sum 'F '1)))
3333 ((== expr 'f-floor) (== s 'F) (== t (list 'sum 'F '1)))
3434 ((== expr 'f-atan2) (== s (list 'pair 'F 'F)) (== t 'F))
35+ ((== expr 'f-exp) (== s 'F) (== t 'F))
36+ ((== expr 'f-log1p) (== s 'F) (== t (list 'sum 'F '1)))
3537 ; Cartesian Closed Categories
3638 ((fresh (f y z) (== expr (list 'curry f))
3739 ; NF: disallow (curry (uncurry ...))
@@ -41,6 +43,7 @@
4143 ; NF: disallow (curry (uncurry ...))
4244 (fresh (sub) (=/= f (list 'curry sub)))
4345 (== s (list 'pair x y)) (cammyo f x (list 'hom y t))))
46+ ((== expr 'app) (fresh (x) (== s (list 'pair (list 'hom x t) x))))
4447 ; Binary Products
4548 ((== expr 'fst) (fresh (x) (== s (list 'pair t x))))
4649 ((== expr 'snd) (fresh (x) (== s (list 'pair x t))))
@@ -59,6 +62,8 @@
5962 ((== expr 'zero) (== s '1) (== t 'N))
6063 ((fresh (x f) (== expr (list 'pr x f))
6164 (== s 'N) (cammyo x '1 t) (cammyo f t t)))
65+ ((== expr 'n-pred-maybe) (== s 'N) (== t (list 'sum 'N '1)))
66+ ((== expr 'n-add) (== s (list 'pair 'N 'N)) (== t 'N))
6267 ; Free Monoids
6368 ((== expr 'cons) (fresh (l) (== s (list 'pair l t)) (== t (list 'list l))))
6469 ((== expr 'nil) (== s '1) (fresh (l) (== t (list 'list l))))
--- a/todo.txt
+++ b/todo.txt
@@ -87,8 +87,6 @@
8787 * Would not be fast enough for raytracing, but could generate various
8888 computable real constants
8989 * Extraction to floats would hopefully require n < 100
90-* Dual numbers: like complex numbers, but different units, multiplication
91- * started a folder, haven't done AD yet
9290 * CI: automatic generation of demo images
9391 * Would be nice to know how long it takes, too
9492 * Parameterize by number of iterations?
@@ -201,3 +199,5 @@
201199 * S-exprs -> RPython
202200 * Missing optimization
203201 * (comp f-log1p f-exp) => (comp (pair (fun/const f-one) id) f/add)
202+* Lentz's algorithm
203+ * https://en.wikipedia.org/wiki/Lentz's_algorithm