• 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

修订版2d67de7b841230fd479af17b157b577d6a9af4b4 (tree)
时间2022-06-14 13:06:20
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Jet (pair id id) to dup.

更改概述

差异

--- a/cammy-rpy/cammylib/arrows.py
+++ b/cammy-rpy/cammylib/arrows.py
@@ -51,6 +51,14 @@ class Second(Arrow):
5151 pair = cs.functor("pair", [cs.fresh(), right])
5252 return pair, right
5353
54+class Dup(Arrow):
55+ _immutable_ = True
56+ def compile(self, compiler): compiler.dup()
57+ def types(self, cs):
58+ x = cs.fresh()
59+ pair = cs.functor("pair", [x, x])
60+ return x, pair
61+
5462 class Pair(Arrow):
5563 _immutable_ = True
5664 def __init__(self, f, g):
@@ -409,6 +417,7 @@ unaryFunctors = {
409417 "ignore": Ignore(),
410418 "fst": First(),
411419 "snd": Second(),
420+ "dup": Dup(),
412421 "left": Left(),
413422 "right": Right(),
414423 "either": Either(),
--- a/hive/dup.cammy
+++ /dev/null
@@ -1 +0,0 @@
1-pair/dup
\ No newline at end of file
--- a/hive/pair/dup.cammy
+++ b/hive/pair/dup.cammy
@@ -1,3 +1,3 @@
1-(pair id id)
1+dup
22
33 The [diagonal map](https://ncatlab.org/nlab/show/diagonal+morphism).
--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -31,6 +31,7 @@ impl CostFunction<SymbolLang> for CAMCostModel {
3131 // Term ops which the JIT can elide
3232 "fst" => 3,
3333 "snd" => 3,
34+ "dup" => 3,
3435 "left" => 3,
3536 "right" => 3,
3637 // Stack-allocating operations
@@ -106,7 +107,10 @@ fn main() -> std::io::Result<()> {
106107 // pair-precompose when ?g is id
107108 rw!("pair-factor-snd"; "(pair (comp ?r ?f) ?r)" => "(comp ?r (pair ?f id))"),
108109 // pair-precompose when ?f and ?g are id
109- rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r (pair id id))"),
110+ rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r dup)"),
111+
112+ // jet for pair/dup
113+ rw!("pair-dup-jet"; "(pair id id)" => "dup"),
110114
111115 // This implies the old rule pair-swap-invo: (comp pair/swap pair/swap) => id
112116 // So, like pair-swap-invo, this turns braided products into symmetric products.
--- a/test_canonical.json
+++ b/test_canonical.json
@@ -1,7 +1,7 @@
11 [
22 ["X", "X", ["id"]],
33 ["(pair X Y)", "X", ["fst"]],
4- ["X", "(pair X X)", ["(pair id id)"]],
4+ ["X", "(pair X X)", ["dup"]],
55 ["(pair X Y)", "(pair Y X)", ["(pair snd fst)"]],
66 ["(pair (hom X Y) X)", "Y", ["(uncurry id)"]],
77 ["1", "2", ["t", "f"]],