Add test, fix bugs

egraphs-good · Oct 29, 2024 · 7262571 · 7262571
1 parent 5eb6dfc
commit 7262571
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 9 deletions.
diff --git a/src/sort/bigint.rs b/src/sort/bigint.rs
@@ -28,6 +28,8 @@ impl Sort for BigIntSort {
     fn register_primitives(self: Arc<Self>, eg: &mut TypeInfo) {
         type Opt<T=()> = Option<T>;
 
+        add_primitives!(eg, "bigint" = |a: i64| -> Z { a.into() });
+
         add_primitives!(eg, "+" = |a: Z, b: Z| -> Z { a + b });
         add_primitives!(eg, "-" = |a: Z, b: Z| -> Z { a - b });
         add_primitives!(eg, "*" = |a: Z, b: Z| -> Z { a * b });
@@ -58,7 +60,7 @@ impl Sort for BigIntSort {
         add_primitives!(eg, "max" = |a: Z, b: Z| -> Z { a.max(b) });
 
         add_primitives!(eg, "to-string" = |a: Z| -> Symbol { a.to_string().into() });
-        add_primitives!(eg, "from-string" = |a: Symbol| -> Opt<Z> { a.as_str().parse::<Z>().ok() })
+        add_primitives!(eg, "from-string" = |a: Symbol| -> Opt<Z> { a.as_str().parse::<Z>().ok() });
    }
 
     fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) {

diff --git a/src/sort/bigrat.rs b/src/sort/bigrat.rs
@@ -9,7 +9,7 @@ use crate::{ast::Literal, util::IndexSet};
 use super::*;
 
 lazy_static! {
-    static ref BIG_RAT_SORT_NAME: Symbol = "Rational".into();
+    static ref BIG_RAT_SORT_NAME: Symbol = "BigRat".into();
     static ref RATS: Mutex<IndexSet<Q>> = Default::default();
 }
 
@@ -41,7 +41,7 @@ impl Sort for BigRatSort {
         add_primitives!(eg, "floor" = |a: Q| -> Q { a.floor() });
         add_primitives!(eg, "ceil" = |a: Q| -> Q { a.ceil() });
         add_primitives!(eg, "round" = |a: Q| -> Q { a.round() });
-        add_primitives!(eg, "rational" = |a: Z, b: Z| -> Q { Q::new(a, b) });
+        add_primitives!(eg, "bigrat" = |a: Z, b: Z| -> Q { Q::new(a, b) });
         add_primitives!(eg, "numer" = |a: Q| -> Z { a.numer().clone() });
         add_primitives!(eg, "denom" = |a: Q| -> Z { a.denom().clone() });
 
@@ -114,13 +114,19 @@ impl Sort for BigRatSort {
             Expr::call_no_span(
                 "bigrat",
                 vec![
-                    Expr::Lit(
-                        DUMMY_SPAN.clone(),
-                        Literal::String(numer.to_string().into()),
+                    Expr::call_no_span(
+                        "from-string",
+                        vec![GenericExpr::Lit(
+                            DUMMY_SPAN.clone(),
+                            Literal::String(numer.to_string().into()),
+                        )],
                     ),
-                    Expr::Lit(
-                        DUMMY_SPAN.clone(),
-                        Literal::String(denom.to_string().into()),
+                    Expr::call_no_span(
+                        "from-string",
+                        vec![GenericExpr::Lit(
+                            DUMMY_SPAN.clone(),
+                            Literal::String(denom.to_string().into()),
+                        )],
                     ),
                 ],
             ),

diff --git a/src/typechecking.rs b/src/typechecking.rs
@@ -42,6 +42,8 @@ impl Default for TypeInfo {
         res.add_sort(I64Sort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(F64Sort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(RationalSort, DUMMY_SPAN.clone()).unwrap();
+        res.add_sort(BigIntSort, DUMMY_SPAN.clone()).unwrap();
+        res.add_sort(BigRatSort, DUMMY_SPAN.clone()).unwrap();
 
         res.add_presort::<MapSort>(DUMMY_SPAN.clone()).unwrap();
         res.add_presort::<SetSort>(DUMMY_SPAN.clone()).unwrap();

diff --git a/tests/bignum.egg b/tests/bignum.egg
@@ -0,0 +1,5 @@
+
+(let x (bigint -1234))
+(let y (from-string "2"))
+(let z (bigrat x y))
+(check (= (to-string (numer z)) "-617"))