Commit: 97a7a3ed2f25a148e138e7dedb43af9b84a405b4 - cammy (git)

A categorical programming language

Commit MetaInfo

• Revision: 97a7a3ed2f25a148e138e7dedb43af9b84a405b4 (tree)
• Time: 2024-05-24 14:09:14
• Author: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

jelly: Fix the problematic rule.

Change Summary

• modified: jelly/src/main.rs

Incremental Difference

--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -54,13 +54,6 @@ impl CostFunction<SymbolLang> for CAMCostModel {
     }
 }
 
-// XXX doesn't typecheck!?
-// fn isNotNil<L, N>(var :&'static str) -> impl Fn(&mut EGraph<L, N>, Id, &Subst) -> bool {
-//     let v = var.parse().unwrap();
-//     let nil = "nil".parse().unwrap();
-//     move |egraph, _, subst| !egraph[subst[v]].nodes.contains(&nil)
-// }
-
 // Hagino 1987: https://web.sfc.keio.ac.jp/~hagino/index.html.en
 // Cousineau, Curien, & Mauny 1987: https://doi.org/10.1016/0167-6423(87)90020-7
 // Wadler 1989: https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf
@@ -129,8 +122,7 @@ fn main() -> std::io::Result<()> {
         // pair-precompose when ?g is id
         rw!("pair-factor-snd"; "(pair (comp ?r ?f) ?r)" => "(comp ?r (pair ?f id))"),
         // pair-precompose when ?f and ?g are id
-        // XXX This is not type-correct when ?r is nil.
-        rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r dup)"), // if isNotNil("?r")),
+        rw!("pair-factor-both"; "(comp ?r dup)" => "(pair ?r ?r)"),
 
         // jet for pair/dup
         rw!("pair-dup-jet"; "(pair id id)" => "dup"),