Merge pull request #418 from oflatt/oflatt-remove-declare

Remove declare and calc

src/ast/desugar.rs

@@ -182,63 +182,6 @@ fn desugar_simplify(desugar: &mut Desugar, expr: &Expr, schedule: &Schedule) ->
     res
 }
 
-pub(crate) fn desugar_calc(
-    desugar: &mut Desugar,
-    span: Span,
-    idents: Vec<IdentSort>,
-    exprs: Vec<Expr>,
-    seminaive_transform: bool,
-) -> Result<Vec<NCommand>, Error> {
-    let mut res = vec![];
-
-    // first, push all the idents
-    for IdentSort { ident, sort } in idents {
-        res.push(Command::Declare {
-            span: span.clone(),
-            name: ident,
-            sort,
-        });
-    }
-
-    // now, for every pair of exprs we need to prove them equal
-    for expr1and2 in exprs.windows(2) {
-        let expr1 = &expr1and2[0];
-        let expr2 = &expr1and2[1];
-        res.push(Command::Push(1));
-
-        // add the two exprs only when they are calls (consts and vars don't need to be populated).
-        if let Expr::Call(..) = expr1 {
-            res.push(Command::Action(Action::Expr(expr1.span(), expr1.clone())));
-        }
-        if let Expr::Call(..) = expr2 {
-            res.push(Command::Action(Action::Expr(expr2.span(), expr2.clone())));
-        }
-
-        res.push(Command::RunSchedule(Schedule::Saturate(
-            span.clone(),
-            Box::new(Schedule::Run(
-                span.clone(),
-                RunConfig {
-                    ruleset: "".into(),
-                    until: Some(vec![Fact::Eq(
-                        span.clone(),
-                        vec![expr1.clone(), expr2.clone()],
-                    )]),
-                },
-            )),
-        )));
-
-        res.push(Command::Check(
-            span.clone(),
-            vec![Fact::Eq(span.clone(), vec![expr1.clone(), expr2.clone()])],
-        ));
-
-        res.push(Command::Pop(1));
-    }
-
-    desugar_commands(res, desugar, false, seminaive_transform)
-}
-
 pub(crate) fn rewrite_name(rewrite: &Rewrite) -> String {
     rewrite.to_string().replace('\"', "'")
 }
@@ -261,7 +204,6 @@ pub(crate) fn desugar_command(
             constructor,
             inputs,
         } => desugar.desugar_function(&FunctionDecl::relation(constructor, inputs)),
-        Command::Declare { span, name, sort } => desugar.declare(span, name, sort),
         Command::Datatype { name, variants } => desugar_datatype(name, variants),
         Command::Rewrite(ruleset, rewrite, subsume) => {
             desugar_rewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite, subsume)
@@ -313,9 +255,6 @@ pub(crate) fn desugar_command(
         }
         Command::Action(action) => vec![NCommand::CoreAction(action)],
         Command::Simplify { expr, schedule } => desugar_simplify(desugar, &expr, &schedule),
-        Command::Calc(span, idents, exprs) => {
-            desugar_calc(desugar, span, idents, exprs, seminaive_transform)?
-        }
         Command::RunSchedule(sched) => {
             vec![NCommand::RunSchedule(sched.clone())]
         }

src/ast/mod.rs

@@ -382,26 +382,6 @@ where
         name: Symbol,
         variants: Vec<Variant>,
     },
-    /// `declare` is syntactic sugar allowing for the declaration of constants.
-    /// For example, the following program:
-    /// ```text
-    /// (sort Bool)
-    /// (declare True Bool)
-    /// ```
-    /// Desugars to:
-    /// ```text
-    /// (sort Bool)
-    /// (function True_table () Bool)
-    /// (let True (True_table))
-    /// ```
-
-    /// Note that declare inserts the constant into the database,
-    /// so rules can use the constant directly as a variable.
-    Declare {
-        span: Span,
-        name: Symbol,
-        sort: Symbol,
-    },
     /// Create a new user-defined sort, which can then
     /// be used in new [`Command::Function`] declarations.
     /// The [`Command::Datatype`] command desugars directly to this command, with one [`Command::Function`]
@@ -626,8 +606,6 @@ where
         expr: GenericExpr<Head, Leaf>,
         schedule: GenericSchedule<Head, Leaf>,
     },
-    // TODO provide calc docs
-    Calc(Span, Vec<IdentSort>, Vec<GenericExpr<Head, Leaf>>),
     /// The `query-extract` command runs a query,
     /// extracting the result for each match that it finds.
     /// For a simpler extraction command, use [`Action::Extract`] instead.
@@ -691,10 +669,7 @@ where
     /// Print out the number of rows in a function or all functions.
     PrintSize(Option<Symbol>),
     /// Input a CSV file directly into a function.
-    Input {
-        name: Symbol,
-        file: String,
-    },
+    Input { name: Symbol, file: String },
     /// Extract and output a set of expressions to a file.
     Output {
         file: String,
@@ -725,11 +700,6 @@ where
             }
             GenericCommand::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true, false),
             GenericCommand::Datatype { name, variants } => list!("datatype", name, ++ variants),
-            GenericCommand::Declare {
-                span: _,
-                name,
-                sort,
-            } => list!("declare", name, sort),
             GenericCommand::Action(a) => a.to_sexp(),
             GenericCommand::Sort(name, None) => list!("sort", name),
             GenericCommand::Sort(name, Some((name2, args))) => {
@@ -751,7 +721,6 @@ where
             } => rule.to_sexp(*ruleset, *name),
             GenericCommand::RunSchedule(sched) => list!("run-schedule", sched),
             GenericCommand::PrintOverallStatistics => list!("print-stats"),
-            GenericCommand::Calc(_ann, args, exprs) => list!("calc", list!(++ args), ++ exprs),
             GenericCommand::QueryExtract { variants, expr } => {
                 list!("query-extract", ":variants", variants, expr)
             }

src/ast/parse.lalrpop

@@ -55,7 +55,6 @@ Command: Command = {
         <merge:(":merge" <Expr>)?> <default:(":default" <Expr>)?> RParen => {
         Command::Function(FunctionDecl { name, schema, merge, merge_action: Actions::new(merge_action.unwrap_or_default()), default, cost, unextractable: unextractable.is_some(), ignore_viz: false })
     },
-    <lo:LParen> "declare" <name:Ident> <sort:Ident> <hi:RParen> => Command::Declare{span: Span(srcfile.clone(), lo, hi), name, sort},
     LParen "relation" <constructor:Ident> <inputs:List<Type>> RParen => Command::Relation{constructor, inputs},
     LParen "ruleset" <name:Ident> RParen => Command::AddRuleset(name),
     LParen "unstable-combined-ruleset" <name:Ident> <subrulesets:Ident*> RParen => Command::UnstableCombinedRuleset(name, subrulesets),
@@ -82,7 +81,6 @@ Command: Command = {
             Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset, until })))),
     LParen "simplify"  <schedule:Schedule> <expr:Expr> RParen
         => Command::Simplify { expr, schedule },
-    <lo:LParen> "calc" LParen <idents:IdentSort*> RParen <exprs:Expr+> <hi:RParen> => Command::Calc(Span(srcfile.clone(), lo, hi), idents, exprs),
     LParen "query-extract" <variants:(":variants" <UNum>)?> <expr:Expr> RParen => Command::QueryExtract { expr, variants: variants.unwrap_or(0) },
     <lo:LParen> "check" <facts:(Fact)*> <hi:RParen> => Command::Check(Span(srcfile.clone(), lo, hi), facts),
     LParen "check-proof" RParen => Command::CheckProof,

tests/bdd.egg

@@ -9,8 +9,10 @@
 (datatype BDD
     (ITE i64 BDD BDD) ; variables labelled by number
 )
-(declare True BDD)
-(declare False BDD)
+(function TrueConst () BDD)
+(let True (TrueConst))
+(function FalseConst () BDD)
+(let False (FalseConst))
 
 ; compress unneeded nodes
 (rewrite (ITE n a a) a)

tests/calc.egg

@@ -1,7 +1,10 @@
 (datatype G)
-(declare I G)
-(declare A G)
-(declare B G)
+(function IConst () G)
+(let I (IConst))
+(function AConst () G)
+(let A (AConst))
+(function BConst () G)
+(let B (BConst))
 (function g* (G G) G)
 (function inv (G) G)
 (birewrite (g* (g* a b) c) (g* a (g* b c))) ; assoc
@@ -18,15 +21,41 @@
 (let A8 (g* A4 A4))
 
 
-(calc ()
-    (g* A4 A4)
-    (g* (g* A2 A2) (g* A2 A2))
-    (g* A2 (g* A2 (g* A2 A2)))
-)
+(push)
+(g* A4 A4)
 
-; Note that (calc ((I G) (b G)) ...) will fail because names must be unused
-(calc ((a G) (b G))
-    (g* (g* b (g* (inv a) a)) (inv b))
-    (g* b (inv b))
-    I
-)
+(run 10000 :until (= (g* A4 A4) (g* (g* A2 A2) (g* A2 A2))))
+
+(check (= (g* A4 A4) (g* (g* A2 A2) (g* A2 A2))))
+(pop)
+
+(push)
+(g* (g* A2 A2) (g* A2 A2))
+
+(run 10000 :until (= (g* (g* A2 A2) (g* A2 A2))
+(g* A2 (g* A2 (g* A2 A2)))))
+(check (= (g* (g* A2 A2) (g* A2 A2))
+(g* A2 (g* A2 (g* A2 A2)))))
+(pop)
+
+
+(function aConst () G)
+(function bConst () G)
+(let a (aConst))
+(let b (bConst))
+(push)
+
+(g* (g* b (g* (inv a) a)) (inv b))
+
+(run 100000 :until (= (g* (g* b (g* (inv a) a)) (inv b)) (g* b (inv b))))
+
+(check (= (g* (g* b (g* (inv a) a)) (inv b)) (g* b (inv b))))
+
+(pop)
+
+(push)
+(g* b (inv b))
+(run 100000 :until (= (g* b (inv b)) I))
+(check (= (g* b (inv b)) I))
+
+(pop)

tests/combinators.egg

@@ -12,8 +12,10 @@
     (N i64)
     (Add Expr Expr)
     (App Expr Expr))
-(declare T Expr)
-(declare F Expr)
+(function TConst () Expr)
+(let T (TConst))
+(function FConst () Expr)
+(let F (FConst))
 
 
 ; (\x. (if x then 0 else 1) + 2) false
@@ -26,13 +28,20 @@
     (CAbs String CExpr :cost 10000) ; (abstractions that haven't been eliminated yet)
     (CN i64)
     (CApp CExpr CExpr))
-(declare CT CExpr)
-(declare CF CExpr)
-(declare CIf CExpr)
-(declare CAdd CExpr)
-(declare S CExpr)
-(declare K CExpr)
-(declare I CExpr)
+(function CTConst () CExpr)
+(let CT (CTConst))
+(function CFConst () CExpr)
+(let CF (CFConst))
+(function CIfConst () CExpr)
+(let CIf (CIfConst))
+(function CAddConst () CExpr)
+(let CAdd (CAddConst))
+(function SConst () CExpr)
+(let S (SConst))
+(function KConst () CExpr)
+(let K (KConst))
+(function IConst () CExpr)
+(let I (IConst))
 
 ;;;; Conversion functions
 (function Comb (Expr) CExpr :cost 1000000)

tests/fusion.egg

@@ -8,7 +8,8 @@
     (Num i64)
     (CaseSplit Term Term Term)
     (Cons Term Term))
-(declare Nil Term)
+(function NilConst () Term)
+(let Nil (NilConst))
 
 (function V (String) Var) 
 (function From (Term) Var)

tests/integration_test.rs

@@ -334,7 +334,8 @@ fn test_subsume() {
             None,
             r#"
         ;; add something equal to x that can be extracted:
-        (declare other Math)
+        (function otherConst () Math)
+        (let other (otherConst))
         (union x other)
         (extract x 10)
         "#,

tests/knapsack.egg

@@ -8,7 +8,8 @@
 ; List of (weight, value) pairs
 (datatype objects
     (Cons i64 i64 objects))
-(declare Nil objects)
+(function NilConst () objects)
+(let Nil (NilConst))
 
 ; Given a capacity and a list of objects, finds the maximum value of a
 ; collection of objects whose total weight does not exceed the capacity.

tests/lambda.egg

@@ -1,7 +1,9 @@
 ;; NOTE: This file contains several unsafe operations
 (datatype Value (Num i64))
-(declare True Value)
-(declare False Value)
+(function TrueConst () Value)
+(let True (TrueConst))
+(function FalseConst () Value)
+(let False (FalseConst))
 (datatype VarType)
 (datatype Term
     (Val Value)

tests/levenshtein-distance.egg

@@ -10,7 +10,8 @@
 ; `String` supports limited operations, let's just use it as a char type
 (datatype str
     (Cons String str))
-(declare Empty str)
+(function EmptyConst () str)
+(let Empty (EmptyConst))
 
 ; Length function
 

tests/repro-define.egg

@@ -1,6 +1,7 @@
 (datatype Nat
   (S Nat))
-(declare Zero Nat)
+(function ZeroConst () Nat)
+(let Zero (ZeroConst))
 
 (let two (S (S Zero)))
 

tests/repro-querybug.egg

@@ -1,6 +1,7 @@
 (datatype list
     (Cons i64 list))
-(declare Empty list)
+(function EmptyConst () list)
+(let Empty (EmptyConst))
 
 (relation eq (list list))
 

tests/repro-silly-panic.egg

@@ -1,7 +1,8 @@
 (datatype KAT
     (par KAT KAT)
 )
-(declare A KAT)
+(function AConst () KAT)
+(let A (AConst))
 
 (rewrite (par p p) p)
 (rule ((= r (par q r)) (= q (par q r))) ((union r q)))

tests/resolution.egg

@@ -27,8 +27,10 @@
 ; This encoding as it stands really only supports ground atoms modulo equality
 
 (datatype Bool)
-(declare True Bool)
-(declare False Bool)
+(function TrueConst () Bool)
+(let True (TrueConst))
+(function FalseConst () Bool)
+(let False (FalseConst))
 (function myor (Bool Bool) Bool)
 (function negate (Bool) Bool)