More

src/state.cpp

@@ -1417,13 +1417,13 @@ Plugin* State::getPlugin()
   return d_plugin;
 }
 
-void State::bindBuiltin(const std::string& name, Kind k, Attr ac)
+Expr State::bindBuiltin(const std::string& name, Kind k, Attr ac)
 {
   // type is irrelevant, assign abstract
-  bindBuiltin(name, k, ac, d_absType);
+  return bindBuiltin(name, k, ac, d_absType);
 }
 
-void State::bindBuiltin(const std::string& name, Kind k, Attr ac, const Expr& t)
+Expr State::bindBuiltin(const std::string& name, Kind k, Attr ac, const Expr& t)
 {
   Expr c = mkSymbol(Kind::CONST, name, t);
   bind(name, c);
@@ -1434,11 +1434,15 @@ void State::bindBuiltin(const std::string& name, Kind k, Attr ac, const Expr& t)
     ai.d_kind = k;
     ai.d_attrCons = ac;
   }
+  return c;
 }
 
-void State::bindBuiltinEval(const std::string& name, Kind k, Attr ac)
+Expr State::bindBuiltinEval(const std::string& name, Kind k, Attr ac)
 {
-  bindBuiltin("eo::"+name, k, ac);
+  Expr c = bindBuiltin("eo::"+name, k, ac);
+  c.getValue()->setFlag(ExprValue::Flag::IS_FLAGS_COMPUTED, true);
+  c.getValue()->setFlag(ExprValue::Flag::IS_EVAL, true);
+  return c;
 }
 
 void State::defineProgram(const Expr& v, const Expr& prog)

src/state.h

@@ -254,11 +254,11 @@ class State
   AppInfo* getAppInfo(const ExprValue* e);
   const AppInfo* getAppInfo(const ExprValue* e) const;
   /** Bind builtin */
-  void bindBuiltin(const std::string& name, Kind k, Attr ac = Attr::NONE);
+  Expr bindBuiltin(const std::string& name, Kind k, Attr ac = Attr::NONE);
   /** Bind builtin */
-  void bindBuiltin(const std::string& name, Kind k, Attr ac, const Expr& t);
+  Expr bindBuiltin(const std::string& name, Kind k, Attr ac, const Expr& t);
   /** Bind builtin eval */
-  void bindBuiltinEval(const std::string& name, Kind k, Attr ac = Attr::NONE);
+  Expr bindBuiltinEval(const std::string& name, Kind k, Attr ac = Attr::NONE);
   //--------------------- parsing state
   /** The symbol table, mapping symbols */
   std::map<std::string, Expr> d_symTable;

src/type_checker.cpp

@@ -940,6 +940,7 @@ Expr TypeChecker::evaluateProgramInternal(
         bool matchSuccess = true;
         for (size_t i=1; i<nargs; i++)
         {
+          // TODO: should we abort here?
           if (children[i]->isEvaluatable())
           {
             return d_null;

tests/CMakeLists.txt

@@ -133,6 +133,7 @@ set(ethos_test_file_list
     simul-overload.eo
     bang-lex.eo
     segfault-98.eo
+    eo-add-non-first-class.eo
 )
 
 if(ENABLE_ORACLES)

tests/eo-add-non-first-class.eo

@@ -0,0 +1,34 @@
+(declare-type Int ())
+(declare-consts <numeral> Int)
+
+(declare-const g (-> Int Int Int))
+
+(program dummy ((f (-> Int Int Int)) (n1 Int) (n2 Int))
+    (Int Int (-> Int Int Int)) Int
+
+    (((dummy n1 n2 f) (f n1 n2)))
+)
+
+; this should work
+(define tmp1 () (dummy 1 1 g))
+(declare-const c1 (eo::requires tmp1 (g 1 1) Int))
+(define test1 () c1 :type Int)
+
+
+(program foo ((n1 Int) (n2 Int))
+    (Int Int) Int
+
+    (((foo n1 n2) n1))
+)
+
+
+; this should not work
+;(define tmp2 () (dummy 1 1 foo))
+;(declare-const c2 (eo::requires tmp2 1 Int))
+;(define test1 () c2 :type Int)
+
+
+; this should not work
+;(define tmp3 () (dummy 1 1 eo::add))
+;(declare-const c3 (eo::requires tmp3 2 Int))
+;(define test2 () c3 :type Int)