Split assume op in two operators

src/error.rs

@@ -875,7 +875,10 @@ impl ToDiagnostic<FileId> for EvalError {
                     // point to the builtin implementation contract like `func` or `record`, so
                     // there's no good reason to show it. Note than even in that case, the
                     // information contained in the argument thunk can still be useful.
-                    if contract_id.map(|ctrs_id| arg_pos.src_id != ctrs_id).unwrap_or(true)  {
+                    if contract_id
+                        .map(|ctrs_id| arg_pos.src_id != ctrs_id)
+                        .unwrap_or(true)
+                    {
                         labels.push(primary(&arg_pos).with_message("applied to this expression"));
                     }
                 }

src/merge.rs

@@ -54,7 +54,7 @@
 use crate::error::EvalError;
 use crate::eval::{Closure, Environment};
 use crate::position::TermPos;
-use crate::term::{BinaryOp, Contract, MetaValue, RichTerm, Term, make as mk_term};
+use crate::term::{make as mk_term, BinaryOp, Contract, MetaValue, RichTerm, Term};
 use crate::transformations::Closurizable;
 use std::collections::HashMap;
 

src/operation.rs

@@ -226,6 +226,34 @@ fn process_unary_operation(
                 ))
             }
         }
+        UnaryOp::ToCtrFun() => {
+            match *t {
+                Term::Fun(..) => Ok(Closure {
+                    body: RichTerm { term: t, pos },
+                    env,
+                }),
+                Term::Record(..) => {
+                    let mut new_env = Environment::new();
+                    let closurized = RichTerm { term: t, pos }.closurize(&mut new_env, env);
+
+                    // Convert the record to the function `fun l x => contract & x`.
+                    let body = mk_fun!(
+                        "_l",
+                        "x",
+                        mk_term::op2(BinaryOp::Merge(), closurized, mk_term::var("x"))
+                    )
+                    .with_pos(pos.into_inherited());
+
+                    Ok(Closure { body, env: new_env })
+                }
+                _ => Err(EvalError::TypeError(
+                    String::from("Function or record"),
+                    String::from("contract application, 1st argument"),
+                    arg_pos,
+                    RichTerm { term: t, pos },
+                )),
+            }
+        }
         UnaryOp::Blame() => {
             if let Term::Lbl(label) = *t {
                 Err(EvalError::BlameError(
@@ -888,8 +916,6 @@ fn process_binary_operation(
                 l.arg_pos = thunk.borrow().body.pos;
                 l.arg_thunk = Some(thunk);
 
-                println!("After setting label pos: types {:?}; tag {:?}; span {:?}; arg_pos {:?}; pol {:?}", l.types, l.tag, l.span, l.arg_pos, l.polarity);
-
                 stack.push_arg(
                     Closure::atomic_closure(RichTerm::new(Term::Lbl(l), pos2.into_inherited())),
                     pos2.into_inherited(),
@@ -903,27 +929,9 @@ fn process_binary_operation(
                         },
                         env: env1,
                     }),
-                    Term::Record(..) => {
-                        let mut new_env = Environment::new();
-                        let closurized = RichTerm {
-                            term: t1,
-                            pos: pos1,
-                        }
-                        .closurize(&mut new_env, env1);
-
-                        // Convert the record to the function `fun l x => contract & x`.
-                        let body = mk_fun!(
-                            "l",
-                            "x",
-                            mk_term::op2(BinaryOp::Merge(), closurized, mk_term::var("x"))
-                        )
-                        .with_pos(pos1.into_inherited());
-
-                        Ok(Closure { body, env: new_env })
-                    }
                     _ => Err(EvalError::TypeError(
-                        String::from("Function or record"),
+                        String::from("Function"),
-                        String::from("contract application, 1st argument"),
+                        String::from("assume, 1st argument"),
                         fst_pos,
                         RichTerm {
                             term: t1,
@@ -934,7 +942,7 @@ fn process_binary_operation(
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
-                    String::from("contract application, 2nd argument"),
+                    String::from("assume, 2nd argument"),
                     snd_pos,
                     RichTerm {
                         term: t2,

src/stack.rs

@@ -267,9 +267,7 @@ impl Stack {
     /// corresponding thunk, or `None` if the top element wasn't an argument.
     pub fn track_arg(&mut self) -> Option<Thunk> {
         match self.0.last_mut() {
-            Some(Marker::TrackedArg(thunk, _)) => {
+            Some(Marker::TrackedArg(thunk, _)) => Some(thunk.clone()),
-                Some(thunk.clone())
-            }
             Some(Marker::Arg(..)) => {
                 let (closure, pos) = self.pop_arg().unwrap();
                 let thunk = Thunk::new(closure, IdentKind::Lam());

src/term.rs

@@ -518,6 +518,12 @@ pub enum UnaryOp {
 
     /// Raise a blame, which stops the execution and prints an error according to the label argument.
     Blame(),
+    /// Convert a flat contract, specified as an expression like `#SomeContract`, to a function of
+    /// two arguments (a label and the value to be tested) suitable to be passed to [`Assume`]().
+    /// This operator's purpose is to accept more terms than just functions as a contract: it is
+    /// the identity on functions, but it also accepts contracts as records, which are translated
+    /// to a function that performs a merge operation with its argument.
+    ToCtrFun(),
 
     /// Typecast an enum to a larger enum type.
     ///
@@ -632,9 +638,7 @@ pub enum BinaryOp {
     ///
     /// Apply a contract to a label and a value. The label and the value are stored on the stack,
     /// unevaluated, while the contract is the strict argument to this operator.  This operator
-    /// additionally marks the location of the tested value for better error reporting. It also
+    /// additionally marks the location of the tested value for better error reporting.
-    /// accepts contracts as records, which are translated to a merge operation instead of function
-    /// application.
     Assume(),
     /// Unwrap a tagged term.
     ///

src/typecheck.rs

@@ -814,7 +814,7 @@ pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType {
     match t {
         Term::Promise(ty, _, _)
         | Term::MetaValue(MetaValue {
-            types: Some(Contract {types: ty, ..}),
+            types: Some(Contract { types: ty, .. }),
             ..
         }) => ApparentType::Annotated(ty.clone()),
         // For metavalues, if there's no type annotation, choose the first contract appearing.
@@ -1528,6 +1528,8 @@ pub fn get_uop_type(state: &mut State, op: &UnaryOp) -> Result<TypeWrapper, Type
         }
         // Bool -> Bool
         UnaryOp::BoolNot() => mk_tyw_arrow!(AbsType::Bool(), AbsType::Bool()),
+        // This should not happen, as ToCtrFun() is only produced during evaluation.
+        UnaryOp::ToCtrFun() => panic!("cannot typecheck ToCtrFun()"),
         // forall a. Dyn -> a
         UnaryOp::Blame() => {
             let res = TypeWrapper::Ptr(new_var(state.table));

src/types.rs

@@ -53,7 +53,7 @@
 //! untyped parts.
 use crate::identifier::Ident;
 use crate::term::make as mk_term;
-use crate::term::{RichTerm, Term, UnaryOp, BinaryOp};
+use crate::term::{BinaryOp, RichTerm, Term, UnaryOp};
 use crate::{mk_app, mk_fun};
 use std::collections::HashMap;
 use std::fmt;
@@ -180,7 +180,7 @@ impl Types {
     ) -> RichTerm {
         use crate::stdlib::contracts;
 
-        let ctr = match self.0 {
+        match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
@@ -189,19 +189,17 @@ impl Types {
             //always successful contract on each element.
             AbsType::List(ref ty) => mk_app!(contracts::list(), ty.contract_open(h, pol, sy)),
             AbsType::Sym() => panic!("Are you trying to check a Sym at runtime?"),
-            AbsType::Arrow(ref s, ref t) => {
+            AbsType::Arrow(ref s, ref t) => mk_app!(
-                let res = mk_app!(
                 contracts::func(),
                 s.contract_open(h.clone(), !pol, sy),
                 t.contract_open(h, pol, sy)
-            );
+            ),
-                println!("Resulting contract: {:#?}", res);
-                res
-            }
             AbsType::Flat(ref t) => {
-                // The assume primive op being strict in the label, we need to map the contract in
+                // As contracts may be specified either as function or records, we apply the ToCtrFun
-                // a function first.
+                // operator, specifically to generate a uniform function of the label and the value to be
-                mk_fun!("l", mk_term::op2(BinaryOp::Assume(), t.clone(), mk_term::var("l")))
+                // tested.
+                let pos = t.pos;
+                mk_term::op1(UnaryOp::ToCtrFun(), t.clone()).with_pos(pos.into_inherited())
             }
             AbsType::Var(ref i) => {
                 let (rt, _) = h
@@ -294,12 +292,7 @@ impl Types {
             AbsType::DynRecord(ref ty) => {
                 mk_app!(contracts::dyn_record(), ty.contract_open(h, pol, sy))
             }
-        };
+        }
-
-        // The assume primive op being strict in the label, we need to map contracts as a lazy
-        // function.
-        let pos = ctr.pos;
-        mk_fun!("l", mk_term::op2(BinaryOp::Assume(), ctr, mk_term::var("l"))).with_pos(pos.into_inherited())
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type