Merge pull request #969 from creusot-rs/remove-impure-term

Remove notion of 'purity' in logic

creusot/src/backend/clone_map/elaborator.rs

@@ -18,7 +18,7 @@ use crate::{
         dependency::HackedId,
         logic::{lower_logical_defn, lower_pure_defn, sigs, spec_axiom},
         signature::sig_to_why3,
-        term::{lower_impure, lower_pure},
+        term::lower_pure,
         ty_inv::InvariantElaborator,
         TransId, Why3Generator,
     },
@@ -183,7 +183,7 @@ impl<'tcx> SymbolElaborator<'tcx> {
 
             let span = ctx.def_span(def_id);
             let res = crate::constant::from_ty_const(&mut ctx.ctx, constant, param_env, span);
-            let res = lower_impure(ctx, names, &res);
+            let res = lower_pure(ctx, names, &res);
 
             vec![Decl::Let(LetDecl {
                 kind: Some(LetKind::Constant),

creusot/src/backend/constant.rs

@@ -6,7 +6,7 @@ use crate::{ctx::TranslatedItem, translation::constant::from_ty_const};
 use super::{
     clone_map::{CloneMap, CloneSummary},
     signature::signature_of,
-    term::lower_impure,
+    term::lower_pure,
     CloneDepth, Why3Generator,
 };
 
@@ -27,7 +27,7 @@ impl<'tcx> Why3Generator<'tcx> {
         let span = self.def_span(def_id);
         let res = from_ty_const(&mut self.ctx, constant, param_env, span);
         let mut names = CloneMap::new(self.tcx, def_id.into());
-        let _ = lower_impure(self, &mut names, &res);
+        let _ = lower_pure(self, &mut names, &res);
         let _ = signature_of(self, &mut names, def_id);
         let (_, summary) = names.to_clones(self, CloneDepth::Shallow);
 

creusot/src/backend/logic.rs

@@ -82,9 +82,9 @@ fn builtin_body<'tcx>(
     // Program symbol (for proofs)
     let mut val_sig = sig.clone();
 
-    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::pure_var(id)).collect();
+    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::var(id)).collect();
     val_sig.contract.ensures =
-        vec![Exp::pure_var("result").eq(Exp::pure_var(val_sig.name.clone()).app(val_args.clone()))];
+        vec![Exp::var("result").eq(Exp::var(val_sig.name.clone()).app(val_args.clone()))];
 
     if util::is_predicate(ctx.tcx, def_id) {
         sig.retty = None;
@@ -101,7 +101,7 @@ fn builtin_body<'tcx>(
 
     decls.extend(clones);
     if !builtin.module.is_empty() {
-        let body = Exp::pure_qvar(builtin.without_search_path()).app(val_args);
+        let body = Exp::qvar(builtin.without_search_path()).app(val_args);
 
         if util::is_predicate(ctx.tcx, def_id) {
             decls.push(Decl::PredDecl(Predicate { sig, body }));
@@ -127,12 +127,12 @@ pub(crate) fn val_decl<'tcx, N: Namer<'tcx>>(
     sig.contract.variant = Vec::new();
 
     let (val_args, val_binders) = binders_to_args(ctx, sig.args);
-    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::pure_var(id)).collect();
+    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::var(id)).collect();
 
     sig.contract
         .ensures
         // = vec!(Exp::pure_var("result".into()).eq(Exp::pure_var(sig.name.clone()).app(val_args)));
-        .push(Exp::pure_var("result").eq(Exp::pure_var(sig.name.clone()).app(val_args)));
+        .push(Exp::var("result").eq(Exp::var(sig.name.clone()).app(val_args)));
     sig.args = val_binders;
     Decl::ValDecl(ValDecl { sig, ghost: false, val: true, kind: None })
 }
@@ -255,12 +255,12 @@ pub fn sigs<'tcx>(ctx: &mut Why3Generator<'tcx>, mut sig: Signature) -> (Signatu
     contract.variant = Vec::new();
     prog_sig.contract = contract;
     let (val_args, val_binders) = binders_to_args(ctx, prog_sig.args);
-    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::pure_var(id)).collect();
+    let val_args: Vec<_> = val_args.into_iter().map(|id| Exp::var(id)).collect();
 
     prog_sig.args = val_binders;
 
     prog_sig.contract.ensures =
-        vec![Exp::pure_var("result").eq(Exp::pure_var(sig.name.clone()).app(val_args))];
+        vec![Exp::var("result").eq(Exp::var(sig.name.clone()).app(val_args))];
 
     (sig, prog_sig)
 }
@@ -281,8 +281,8 @@ fn subst_qname(body: &mut Exp, name: &Ident, lim_name: &Ident) {
     impl<'a> ExpMutVisitor for QNameSubst<'a> {
         fn visit_mut(&mut self, exp: &mut Exp) {
             match exp {
-                Exp::QVar(qname, _) if qname.module.is_empty() && &qname.name == self.0 => {
-                    *exp = Exp::pure_var(self.1.clone())
+                Exp::QVar(qname) if qname.module.is_empty() && &qname.name == self.0 => {
+                    *exp = Exp::var(self.1.clone())
                 }
                 _ => super_visit_mut(self, exp),
             }
@@ -420,13 +420,13 @@ fn function_call(sig: &Signature) -> Exp {
         .cloned()
         .flat_map(|b| b.var_type_pairs())
         .filter(|arg| &*arg.0 != "_")
-        .map(|arg| Exp::pure_var(arg.0))
+        .map(|arg| Exp::var(arg.0))
         .collect();
     if args.is_empty() {
         args = vec![Exp::Tuple(vec![])];
     }
 
-    Exp::pure_var(sig.name.clone()).app(args)
+    Exp::var(sig.name.clone()).app(args)
 }
 
 fn definition_axiom(sig: &Signature, body: Exp, suffix: &str) -> Axiom {

creusot/src/backend/logic/vcgen.rs

@@ -6,7 +6,7 @@ use std::{
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::{EarlyBinder, GenericArgsRef, ParamEnv, Ty, TyKind};
 use rustc_span::{Span, Symbol};
-use why3::{declaration::Signature, exp::Purity, ty::Type, Exp, Ident, QName};
+use why3::{declaration::Signature, ty::Type, Exp, Ident, QName};
 
 use crate::{
     backend::{
@@ -216,7 +216,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
         use crate::pearlite::*;
         match &t.kind {
             // VC(v, Q) = Q(v)
-            TermKind::Var(v) => k(Exp::pure_var(util::ident_of(*v))),
+            TermKind::Var(v) => k(Exp::var(util::ident_of(*v))),
             // VC(l, Q) = Q(l)
             TermKind::Lit(l) => k(self.lower_literal(l)),
             // Items are just global names so
@@ -227,9 +227,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
 
                 if get_builtin(self.ctx.borrow().tcx, *id).is_some() {
                     // Builtins can leverage Why3 polymorphism and sometimes can cause typeck errors in why3 due to ambiguous type variables so lets fix the type now.
-                    k(Exp::pure_qvar(item_name).ascribe(self.ty(t.ty)))
+                    k(Exp::qvar(item_name).ascribe(self.ty(t.ty)))
                 } else {
-                    k(Exp::pure_qvar(item_name))
+                    k(Exp::qvar(item_name))
                 }
             }
             // VC(assert { C }, Q) => VC(C, |c| c && Q(()))
@@ -259,7 +259,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
                 let variant =
                     if *id == self.self_id { self.build_variant(&args)? } else { Exp::mk_true() };
 
-                let call = Exp::pure_qvar(fname).app(args);
+                let call = Exp::qvar(fname).app(args);
                 sig.contract.subst(&[("result".into(), call.clone())].into_iter().collect());
 
                 let inner = k(call)?;
@@ -283,15 +283,11 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
                 //     Ok(Exp::if_(lhs, k(Exp::mk_true())?, self.build_vc(rhs, k)?,))
                 // }),
                 BinOp::Div => self.build_vc(&lhs, &|lhs| {
-                    self.build_vc(rhs, &|rhs| k(Exp::pure_var("div").app(vec![lhs.clone(), rhs])))
+                    self.build_vc(rhs, &|rhs| k(Exp::var("div").app(vec![lhs.clone(), rhs])))
                 }),
                 _ => self.build_vc(&lhs, &|lhs| {
                     self.build_vc(rhs, &|rhs| {
-                        k(Exp::BinaryOp(
-                            binop_to_binop(*op, Purity::Logic),
-                            Box::new(lhs.clone()),
-                            Box::new(rhs),
-                        ))
+                        k(Exp::BinaryOp(binop_to_binop(*op), Box::new(lhs.clone()), Box::new(rhs)))
                     })
                 }),
             },
@@ -383,7 +379,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
                     k => unreachable!("Projection from {k:?}"),
                 };
 
-                self.build_vc(lhs, &|lhs| k(Exp::pure_qvar(accessor.clone()).app(vec![lhs])))
+                self.build_vc(lhs, &|lhs| k(Exp::qvar(accessor.clone()).app(vec![lhs])))
             }
             // TODO: lol
             TermKind::Absurd => todo!("absrd"),

creusot/src/backend/place.rs

@@ -103,8 +103,7 @@ fn create_assign_rec<'tcx>(
 
                 let varnames = freshvars.take(variant.fields.len()).collect::<Vec<Ident>>();
                 let field_pats = varnames.clone().into_iter().map(|x| VarP(x)).collect();
-                let mut varexps: Vec<Exp> =
-                    varnames.into_iter().map(|x| Exp::impure_var(x)).collect();
+                let mut varexps: Vec<Exp> = varnames.into_iter().map(|x| Exp::var(x)).collect();
 
                 varexps[ix.as_usize()] = inner;
 
@@ -118,8 +117,7 @@ fn create_assign_rec<'tcx>(
             TyKind::Tuple(fields) => {
                 let varnames = freshvars.take(fields.len()).collect::<Vec<Ident>>();
                 let field_pats = varnames.clone().into_iter().map(|x| VarP(x.into())).collect();
-                let mut varexps: Vec<Exp> =
-                    varnames.into_iter().map(|x| Exp::impure_var(x.into())).collect();
+                let mut varexps: Vec<Exp> = varnames.into_iter().map(|x| Exp::var(x)).collect();
 
                 varexps[ix.as_usize()] = inner;
 
@@ -133,8 +131,7 @@ fn create_assign_rec<'tcx>(
                 let varnames =
                     freshvars.take(subst.as_closure().upvar_tys().len()).collect::<Vec<Ident>>();
                 let field_pats = varnames.clone().into_iter().map(|x| VarP(x.into())).collect();
-                let mut varexps: Vec<Exp> =
-                    varnames.into_iter().map(|x| Exp::impure_var(x.into())).collect();
+                let mut varexps: Vec<Exp> = varnames.into_iter().map(|x| Exp::var(x)).collect();
 
                 varexps[ix.as_usize()] = inner;
                 let cons = names.constructor(*id, subst);
@@ -149,8 +146,8 @@ fn create_assign_rec<'tcx>(
         },
         Downcast(_, _) => inner,
         Index(ix) => {
-            let set = Exp::impure_qvar(QName::from_string("Slice.set").unwrap());
-            let ix_exp = Exp::impure_var(Ident::build(ix.as_str()));
+            let set = Exp::qvar(QName::from_string("Slice.set").unwrap());
+            let ix_exp = Exp::var(Ident::build(ix.as_str()));
 
             Call(
                 Box::new(set),
@@ -174,7 +171,7 @@ pub(crate) fn translate_rplace<'tcx, N: Namer<'tcx>>(
     loc: Symbol,
     proj: &[mir::ProjectionElem<Symbol, Ty<'tcx>>],
 ) -> Exp {
-    let mut inner = Exp::impure_var(Ident::build(loc.as_str()));
+    let mut inner = Exp::var(Ident::build(loc.as_str()));
     if proj.is_empty() {
         return inner;
     }
@@ -199,7 +196,7 @@ pub(crate) fn translate_rplace<'tcx, N: Namer<'tcx>>(
                     ctx.translate_accessor(def.variants()[variant_id].fields[*ix].did);
 
                     let acc = names.accessor(def.did(), subst, variant_id.as_usize(), *ix);
-                    inner = Call(Box::new(Exp::impure_qvar(acc)), vec![inner]);
+                    inner = Call(Box::new(Exp::qvar(acc)), vec![inner]);
                 }
                 TyKind::Tuple(fields) => {
                     let mut pat = vec![Wildcard; fields.len()];
@@ -208,23 +205,21 @@ pub(crate) fn translate_rplace<'tcx, N: Namer<'tcx>>(
                     inner = Let {
                         pattern: TupleP(pat),
                         arg: Box::new(inner),
-                        body: Box::new(Exp::impure_var("a".into())),
+                        body: Box::new(Exp::var("a")),
                     }
                 }
                 TyKind::Closure(id, subst) => {
-                    inner = Call(
-                        Box::new(Exp::impure_qvar(names.accessor(*id, subst, 0, *ix))),
-                        vec![inner],
-                    );
+                    inner =
+                        Call(Box::new(Exp::qvar(names.accessor(*id, subst, 0, *ix))), vec![inner]);
                 }
                 e => unreachable!("{:?}", e),
             },
             Downcast(_, _) => {}
             Index(ix) => {
                 // TODO: Use [_] syntax
-                let ix_exp = Exp::impure_var(Ident::build(ix.as_str()));
+                let ix_exp = Exp::var(Ident::build(ix.as_str()));
                 inner = Call(
-                    Box::new(Exp::impure_qvar(QName::from_string("Slice.get").unwrap())),
+                    Box::new(Exp::qvar(QName::from_string("Slice.get").unwrap())),
                     vec![inner, ix_exp],
                 )
             }