提交: f877dbc0f85c6e12ed2f9fbadabbcf4037ddb240 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: f877dbc0f85c6e12ed2f9fbadabbcf4037ddb240 (tree)
• 时间: 2022-03-15 14:29:41
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Generalize an optimization for pair/case.

更改概述

• delete: hive/fun/app-10.cammy
• delete: hive/fun/app-20.cammy
• delete: hive/fun/app-40.cammy
• delete: hive/fun/app-5.cammy
• delete: hive/fun/app-80.cammy
• delete: hive/fun/app-thrice.cammy
• delete: hive/fun/app-twice.cammy
• add: hive/int/abs.cammy
• modified: jelly/src/main.rs

差异

--- a/hive/fun/app-10.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app-5) fun/app-5)

--- a/hive/fun/app-20.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app-10) fun/app-10)

--- a/hive/fun/app-40.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app-20) fun/app-20)

--- a/hive/fun/app-5.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app-twice) fun/app-thrice)

--- a/hive/fun/app-80.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app-40) fun/app-40)

--- a/hive/fun/app-thrice.cammy
+++ /dev/null
@@ -1,2 +0,0 @@
-(comp (pair fst fun/app-twice) fun/app)
-

--- a/hive/fun/app-twice.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(comp (pair fst fun/app) fun/app)

--- /dev/null
+++ b/hive/int/abs.cammy
@@ -0,0 +1,3 @@
+(case id id)
+
+The absolute value of an integer.

--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -58,8 +58,9 @@ fn main() -> std::io::Result<()> {
         // pair-precompose when ?f and ?g are id
         rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r (pair id id))"),
 
-        // Turn braided products into symmetric products.
-        rw!("pair-swap-invo"; "(comp (pair snd fst) (pair snd fst))" => "id"),
+        // This implies the old rule pair-swap-invo: (comp pair/swap pair/swap) => id
+        // So, like pair-swap-invo, this turns braided products into symmetric products.
+        rw!("pair-swap-pair"; "(comp (pair ?f ?g) (pair snd fst))" => "(pair ?g ?f)"),
 
         // free for left
         rw!("left-elim-case"; "(comp left (case ?f ?g))" => "?f"),
@@ -67,6 +68,10 @@ fn main() -> std::io::Result<()> {
         rw!("right-elim-case"; "(comp right (case ?f ?g))" => "?g"),
         rw!("case-left-right"; "(case left right)" => "id"),
 
+        // dual of pair-swap-pair
+        // By abstract nonsense, this turns braided sums into symmetric sums.
+        rw!("case-swap-case"; "(comp (case right left) (case ?f ?g))" => "(case ?g ?f)"),
+
         // dual of Elliott 2013
         rw!("case-postcompose"; "(case (comp ?f ?r) (comp ?g ?r))" => "(comp (case ?f ?g) ?r)"),
         rw!("case-factor"; "(case ?r ?r)" => "(comp (case id id) ?r)"),