More

src/type_checker.cpp

@@ -940,7 +940,13 @@ Expr TypeChecker::evaluateProgramInternal(
         bool matchSuccess = true;
         for (size_t i=1; i<nargs; i++)
         {
-          // TODO: should we abort here?
+          // Note we abort here, which changed in Ethos versions >=0.1.2.
+          // The motivation is to disallow unintuitive behaviors of Ethos,
+          // which includes:
+          // - Passing (unapplied) user programs, user oracles or builtin
+          // operators, which we do not support in this current version.
+          // - Passing stuck terms, where we chose to propagate the failure,
+          // e.g. (<program> t) is also stuck if t is stuck.
           if (children[i]->isEvaluatable())
           {
             return d_null;

user_manual.md

@@ -1438,6 +1438,10 @@ If no such term can be found, then the application does not evaluate.
 > __Note:__ If a case is provided `(si ri)` in the definition of program `f` where `si` is not an application of `f`, an error is thrown.
 Furthermore, if `si` contains any computational operators (i.e. those with `eo::` prefix), then an error is thrown.
 
+> __Note:__ Programs are *not* evaluated on terms that fail to evaluate. For example, if a function `f : Int -> Int` is applied to `(eo::add "A" "B")`, we return `(f (eo::add "A" "B"))`.
+
+> __Note:__ Programs cannot be passed as arguments to other programs in this version of Ethos. For example, calling a function `f : (Int -> Int) -> Int` on another user defined program `g : Int -> Int`, the result will be unevaluated, i.e. `(f g)`.
+
 ### Example: Finding a child in an `or` term
 
 The following program (recursively) computes whether a formula `l` is contained as the direct child of an application of `or`: