Change names of defeq rewrites

marcusrossel · Mar 6, 2024 · 2ac9661 · 2ac9661
1 parent 12524ed
commit 2ac9661
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 20 deletions.
diff --git a/Lean/Egg/Core/Source.lean b/Lean/Egg/Core/Source.lean
@@ -37,9 +37,9 @@ inductive Source where
 namespace Source
 
 def NatLit.description : Source.NatLit → String
-  | zero   => s!"!z"
-  | toSucc => s!"!t"
-  | ofSucc => s!"!o"
+  | zero   => s!"≡0"
+  | toSucc => s!"≡→S"
+  | ofSucc => s!"≡S→"
 
 def description : Source → String
   | goal                    => "⊢"
@@ -49,8 +49,8 @@ def description : Source → String
   | tcProj src side pos     => s!"{src.description}[{side.description}{pos}]"
   | explosion src idx       => s!"{src.description}<{idx}>"
   | natLit src              => src.description
-  | eta                     => "!η"
-  | beta                    => "!β"
+  | eta                     => "≡β"
+  | beta                    => "≡η"
 
 instance : ToString Source where
   toString := description

diff --git a/Lean/Egg/Tactic/Explanation.lean b/Lean/Egg/Tactic/Explanation.lean
@@ -44,11 +44,11 @@ syntax "<" num ">" : egg_explosion
 
 syntax egg_basic_fwd_rw_src (egg_tc_proj)? (egg_explosion)? : egg_fwd_rw_src
 syntax "⊢" egg_tc_proj                                      : egg_fwd_rw_src
-syntax "!z"                                                 : egg_fwd_rw_src
-syntax "!t"                                                 : egg_fwd_rw_src
-syntax "!o"                                                 : egg_fwd_rw_src
-syntax "!η"                                                 : egg_fwd_rw_src
-syntax "!β"                                                 : egg_fwd_rw_src
+syntax "≡0"                                                 : egg_fwd_rw_src
+syntax "≡→S"                                                : egg_fwd_rw_src
+syntax "≡S→"                                                : egg_fwd_rw_src
+syntax "≡η"                                                 : egg_fwd_rw_src
+syntax "≡β"                                                 : egg_fwd_rw_src
 
 syntax egg_fwd_rw_src (noWs "-rev")? : egg_rw_src
 
@@ -106,11 +106,11 @@ private def parseBasicFwdRwSrc : (TSyntax `egg_basic_fwd_rw_src) → Source
 
 private def parseFwdRwSrc : (TSyntax `egg_fwd_rw_src) → Source
   | `(egg_fwd_rw_src|⊢[$side$pos]) => .tcProj .goal (parseSide side) (parseSubexprPos pos)
-  | `(egg_fwd_rw_src|!z)           => .natLit .zero
-  | `(egg_fwd_rw_src|!t)           => .natLit .toSucc
-  | `(egg_fwd_rw_src|!o)           => .natLit .ofSucc
-  | `(egg_fwd_rw_src|!η)           => .eta
-  | `(egg_fwd_rw_src|!β)           => .beta
+  | `(egg_fwd_rw_src|≡0)           => .natLit .zero
+  | `(egg_fwd_rw_src|≡→S)          => .natLit .toSucc
+  | `(egg_fwd_rw_src|≡S→)          => .natLit .ofSucc
+  | `(egg_fwd_rw_src|≡η)           => .eta
+  | `(egg_fwd_rw_src|≡β)           => .beta
   | `(egg_fwd_rw_src|$src:egg_basic_fwd_rw_src$[[$tcSide?$pos?]]?$[<$exIdx?>]?) => Id.run do
     let mut src := parseBasicFwdRwSrc src
     if let some tcSide := tcSide? then src := .tcProj src (parseSide tcSide) (parseSubexprPos pos?.get!)

diff --git a/Rust/src/beta.rs b/Rust/src/beta.rs
@@ -203,5 +203,5 @@ fn register_node(new_class: &mut Option<Id>, new_node: LeanExpr, egraph: &mut Le
 }
 
 pub fn beta_reduction_rw() -> LeanRewrite {
-    rewrite!("!β"; "(app (λ ?t ?b) ?a)" => { Beta { body : "?b".parse().unwrap(), arg : "?a".parse().unwrap() }})
+    rewrite!("≡β"; "(app (λ ?t ?b) ?a)" => { Beta { body : "?b".parse().unwrap(), arg : "?a".parse().unwrap() }})
 }
diff --git a/Rust/src/eta.rs b/Rust/src/eta.rs
@@ -184,5 +184,5 @@ fn register_node(new_class: &mut Option<Id>, new_node: LeanExpr, egraph: &mut Le
 }
 
 pub fn eta_reduction_rw() -> LeanRewrite {
-    rewrite!("!η"; "(λ ?t (app ?f (bvar 0)))" => { Eta { fun : "?f".parse().unwrap() }})
+    rewrite!("≡η"; "(λ ?t (app ?f (bvar 0)))" => { Eta { fun : "?f".parse().unwrap() }})
 }
diff --git a/Rust/src/nat_lit.rs b/Rust/src/nat_lit.rs
@@ -41,8 +41,8 @@ impl Applier<LeanExpr, LeanAnalysis> for OfSucc {
 
 pub fn nat_lit_rws() -> Vec<LeanRewrite> {
     let mut rws = vec![];
-    rws.append(&mut rewrite!("!z"; "(lit 0)"                         <=> "(const Nat.zero)"));
-    rws.push(       rewrite!("!t"; "(lit ?n)"                        => { ToSucc { nat_val : "?n".parse().unwrap() }}));
-    rws.push(       rewrite!("!o"; "(app (const Nat.succ) (lit ?n))" => { OfSucc { nat_val : "?n".parse().unwrap() }}));
+    rws.append(&mut rewrite!("≡0";  "(lit 0)"                        <=> "(const Nat.zero)"));
+    rws.push(       rewrite!("≡→S"; "(lit ?n)"                        => { ToSucc { nat_val : "?n".parse().unwrap() }}));
+    rws.push(       rewrite!("≡S→"; "(app (const Nat.succ) (lit ?n))" => { OfSucc { nat_val : "?n".parse().unwrap() }}));
     rws
 }