Simplify Term::Call

The `Term::Call` node was always this weird hybrid between first-order
and higher-order. This just commits to being first-order making our
lives way simpler.

creusot/src/backend/term.rs

@@ -128,13 +128,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 };
                 Exp::UnaryOp(op, Box::new(self.lower_term(arg)))
             }
-            TermKind::Call {
-                id,
-                subst,
-                // fun: box Term { kind: TermKind::Item(id, subst), .. },
-                args,
-                ..
-            } => {
+            TermKind::Call { id, subst, args, .. } => {
                 let mut args: Vec<_> = args.into_iter().map(|arg| self.lower_term(arg)).collect();
 
                 if args.is_empty() {

creusot/src/translation/function.rs

@@ -677,12 +677,7 @@ fn closure_resolve<'tcx>(
         if let Some((id, subst)) = resolve_predicate_of(ctx, param_env, ty) {
             resolve = Term {
                 ty: ctx.types.bool,
-                kind: TermKind::Call {
-                    id: id.into(),
-                    subst,
-                    fun: Box::new(Term::item(ctx.tcx, id, subst)),
-                    args: vec![proj],
-                },
+                kind: TermKind::Call { id: id.into(), subst, args: vec![proj] },
                 span: DUMMY_SP,
             }
             .conj(resolve);

creusot/src/translation/pearlite.rs

@@ -104,7 +104,7 @@ pub enum TermKind<'tcx> {
     Call {
         id: DefId,
         subst: GenericArgsRef<'tcx>,
-        fun: Box<Term<'tcx>>,
+        // fun: Box<Term<'tcx>>,
         args: Vec<Term<'tcx>>,
     },
     Constructor {
@@ -388,7 +388,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                 };
                 Ok(Term { ty, span, kind: TermKind::Lit(lit) })
             }
-            ExprKind::Call { ty: f_ty, fun, ref args, .. } => {
+            ExprKind::Call { ty: f_ty, ref args, .. } => {
                 use Stub::*;
                 match pearlite_stub(self.ctx.tcx, f_ty) {
                     Some(Forall) => {
@@ -473,7 +473,6 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                     }
                     Some(Absurd) => Ok(Term { ty, span, kind: TermKind::Absurd }),
                     None => {
-                        let fun = self.expr_term(fun)?;
                         let args = args
                             .iter()
                             .map(|arg| self.expr_term(*arg))
@@ -484,11 +483,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                             unreachable!("Call on non-function type");
                         };
 
-                        Ok(Term {
-                            ty,
-                            span,
-                            kind: TermKind::Call { id, subst, fun: Box::new(fun), args },
-                        })
+                        Ok(Term { ty, span, kind: TermKind::Call { id, subst, args } })
                     }
                 }
             }
@@ -1004,16 +999,10 @@ pub(crate) fn type_invariant_term<'tcx>(
     let inv_fn_ty = ctx.type_of(inv_fn_did).instantiate(ctx.tcx, inv_fn_substs);
     assert!(matches!(inv_fn_ty.kind(), TyKind::FnDef(id, _) if id == &inv_fn_did));
 
-    let fun = Term { ty: inv_fn_ty, span, kind: TermKind::Item(inv_fn_did, inv_fn_substs) };
     Some(Term {
         ty: ctx.fn_sig(inv_fn_did).skip_binder().output().skip_binder(),
         span,
-        kind: TermKind::Call {
-            id: inv_fn_did,
-            subst: inv_fn_substs,
-            fun: Box::new(fun),
-            args: vec![arg],
-        },
+        kind: TermKind::Call { id: inv_fn_did, subst: inv_fn_substs, args: vec![arg] },
     })
 }
 
@@ -1153,8 +1142,7 @@ pub fn super_visit_term<'tcx, V: TermVisitor<'tcx>>(term: &Term<'tcx>, visitor:
         TermKind::Unary { op: _, arg } => visitor.visit_term(&*arg),
         TermKind::Forall { binder: _, body } => visitor.visit_term(&*body),
         TermKind::Exists { binder: _, body } => visitor.visit_term(&*body),
-        TermKind::Call { id: _, subst: _, fun, args } => {
-            visitor.visit_term(&*fun);
+        TermKind::Call { id: _, subst: _, args } => {
             args.iter().for_each(|a| visitor.visit_term(&*a))
         }
         TermKind::Constructor { typ: _, variant: _, fields } => {
@@ -1208,8 +1196,7 @@ pub(crate) fn super_visit_mut_term<'tcx, V: TermVisitorMut<'tcx>>(
         TermKind::Unary { op: _, arg } => visitor.visit_mut_term(&mut *arg),
         TermKind::Forall { binder: _, body } => visitor.visit_mut_term(&mut *body),
         TermKind::Exists { binder: _, body } => visitor.visit_mut_term(&mut *body),
-        TermKind::Call { id: _, subst: _, fun, args } => {
-            visitor.visit_mut_term(&mut *fun);
+        TermKind::Call { id: _, subst: _, args } => {
             args.iter_mut().for_each(|a| visitor.visit_mut_term(&mut *a))
         }
         TermKind::Constructor { typ: _, variant: _, fields } => {
@@ -1263,17 +1250,8 @@ impl<'tcx> Term<'tcx> {
     ) -> Self {
         let ty = tcx.type_of(def_id).instantiate(tcx, subst);
         let result = ty.fn_sig(tcx).skip_binder().output();
-        let fun = Term {
-            ty: tcx.type_of(def_id).instantiate(tcx, subst),
-            kind: TermKind::Item(def_id, subst),
-            span: DUMMY_SP,
-        };
 
-        Term {
-            ty: result,
-            span: DUMMY_SP,
-            kind: TermKind::Call { id: def_id, subst, fun: Box::new(fun.clone()), args },
-        }
+        Term { ty: result, span: DUMMY_SP, kind: TermKind::Call { id: def_id, subst, args } }
     }
 
     pub(crate) fn var(sym: Symbol, ty: Ty<'tcx>) -> Self {
@@ -1324,14 +1302,6 @@ impl<'tcx> Term<'tcx> {
         }
     }
 
-    pub(crate) fn item(tcx: TyCtxt<'tcx>, id: DefId, subst: GenericArgsRef<'tcx>) -> Self {
-        Term {
-            ty: tcx.type_of(id).instantiate(tcx, subst),
-            kind: TermKind::Item(id, subst),
-            span: DUMMY_SP,
-        }
-    }
-
     pub(crate) fn bin_op(self, tcx: TyCtxt<'tcx>, op: BinOp, rhs: Self) -> Self {
         Term {
             ty: tcx.types.bool,
@@ -1477,8 +1447,7 @@ impl<'tcx> Term<'tcx> {
 
                 body.subst_with_inner(&bound, inv_subst);
             }
-            TermKind::Call { fun, args, .. } => {
-                fun.subst_with_inner(bound, inv_subst);
+            TermKind::Call { args, .. } => {
                 args.iter_mut().for_each(|f| f.subst_with_inner(bound, inv_subst))
             }
             TermKind::Constructor { fields, .. } => {
@@ -1556,8 +1525,7 @@ impl<'tcx> Term<'tcx> {
 
                 body.free_vars_inner(&bound, free);
             }
-            TermKind::Call { fun, args, .. } => {
-                fun.free_vars_inner(bound, free);
+            TermKind::Call { args, .. } => {
                 for arg in args {
                     arg.free_vars_inner(bound, free);
                 }

creusot/src/translation/pearlite/normalize.rs

@@ -22,15 +22,17 @@ impl<'tcx> TermVisitorMut<'tcx> for NormalizeTerm<'tcx> {
     fn visit_mut_term(&mut self, term: &mut Term<'tcx>) {
         super_visit_mut_term(term, self);
         match &mut term.kind {
-            TermKind::Call {
-                id,
-                subst,
-                fun: box Term { kind: TermKind::Item(fid, fsubst), .. },
-                args,
-            } => {
-                *id = *fid;
-                *subst = fsubst;
-
+            TermKind::Call { id, subst, args } => {
+                let method = if self.tcx.trait_of_item(*id).is_some() {
+                    resolve_opt(self.tcx, self.param_env, *id, subst).unwrap_or_else(|| {
+                        panic!("could not resolve trait instance {:?}", (*id, *subst))
+                    })
+                } else {
+                    // TODO dont' do this
+                    (*id, *subst)
+                };
+                *id = method.0;
+                *subst = method.1;
                 *subst = self.tcx.normalize_erasing_regions(self.param_env, *subst);
 
                 if self.tcx.def_path_str(*id) == "std::boxed::Box::<T>::new" {