Add support for eo::dt_constructors and eo::dt_selectors to inspe…

…ct datatypes and datatype constructors (#87)

This adds a way `eo::dt_constructors` to extract the definition of
datatypes (their corresponding list of constructors) and
`eo::dt_selectors` to extract the definition of datatype constructors
(their corresponding list of selectors). It adds an ordinary type
`eo::List` that is part of the assumed background signature for this
purpose.

Also fixes the parser for `declare-datatype` (the singular form of
datatypes, which had not been tested).

NEWS.md

@@ -10,6 +10,8 @@ ethos 0.1.1 prerelease
 - Fixed the disambiguation of overloaded symbols that are not applied to arguments.
 - Fixed the interpretation of operators that combine opaque and ordinary arguments.
 - Fixed a bug in the evaluation of `eo::cons` for left associative operators, which would construct erroneous terms.
+- Adds support for `eo::dt_constructors` which returns the list of constructors associated with a datatype, and `eo::dt_selectors` which returns the list of selectors associated with a datatype constructor. These operators make use of a type `eo::List`, which is now part of the background signature assumed by Ethos.
+- Fixed parser for the singleton case of `declare-datatype`.
 
 ethos 0.1.0
 ===========

src/cmd_parser.cpp

@@ -239,14 +239,13 @@ bool CmdParser::parseNextCommand()
     {
       bool isCo = (tok==Token::DECLARE_CODATATYPES || tok==Token::DECLARE_CODATATYPE);
       bool isMulti = (tok==Token::DECLARE_CODATATYPES || tok==Token::DECLARE_DATATYPES);
-      //d_state.checkThatLogicIsSet();
-      d_lex.eatToken(Token::LPAREN);
       std::vector<std::string> dnames;
       std::vector<size_t> arities;
       std::map<const ExprValue*, std::vector<Expr>> dts;
       std::map<const ExprValue*, std::vector<Expr>> dtcons;
       if (isMulti)
       {
+        d_lex.eatToken(Token::LPAREN);
         // parse (<sort_dec>^{n+1})
         // while the next token is LPAREN, exit if RPAREN
         while (d_lex.eatTokenChoice(Token::LPAREN, Token::RPAREN))
@@ -278,16 +277,19 @@ bool CmdParser::parseNextCommand()
       for (std::pair<const ExprValue* const, std::vector<Expr>>& d : dts)
       {
         Expr dt = Expr(d.first);
-        Expr ctuple = d_state.mkExpr(Kind::TUPLE, d.second);
+        Expr ctuple = d_state.mkList(d.second);
         d_state.markConstructorKind(dt, attr, ctuple);
       }
       for (std::pair<const ExprValue* const, std::vector<Expr>>& c : dtcons)
       {
         Expr cons = Expr(c.first);
-        Expr stuple = d_state.mkExpr(Kind::TUPLE, c.second);
+        Expr stuple = d_state.mkList(c.second);
         d_state.markConstructorKind(cons, Attr::DATATYPE_CONSTRUCTOR, stuple);
       }
-      d_lex.eatToken(Token::RPAREN);
+      if (isMulti)
+      {
+        d_lex.eatToken(Token::RPAREN);
+      }
     }
     break;
     // (declare-consts <symbol> <sort>)

src/kind.cpp

@@ -92,6 +92,9 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_TO_RAT: o << "EVAL_TO_RAT"; break;
     case Kind::EVAL_TO_BIN: o << "EVAL_TO_BIN"; break;
     case Kind::EVAL_TO_STRING: o << "EVAL_TO_STRING"; break;
+    // datatypes
+    case Kind::EVAL_DT_CONSTRUCTORS: o << "EVAL_DT_CONSTRUCTORS"; break;
+    case Kind::EVAL_DT_SELECTORS: o << "EVAL_DT_SELECTORS"; break;
     default: o << "UnknownKind(" << unsigned(k) << ")"; break;
   }
   return o;
@@ -167,6 +170,9 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_TO_RAT: ss << "to_q";break;
         case Kind::EVAL_TO_BIN: ss << "to_bin";break;
         case Kind::EVAL_TO_STRING: ss << "to_str";break;
+        // datatypes
+        case Kind::EVAL_DT_CONSTRUCTORS: ss << "dt_constructors"; break;
+        case Kind::EVAL_DT_SELECTORS: ss << "dt_selectors"; break;
         default:ss << "[" << k << "]";break;
         }
       }
@@ -256,7 +262,10 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
     case Kind::EVAL_TO_BIN:
-    case Kind::EVAL_TO_STRING:return true; break;
+    case Kind::EVAL_TO_STRING:
+    // datatypes
+    case Kind::EVAL_DT_CONSTRUCTORS:
+    case Kind::EVAL_DT_SELECTORS: return true; break;
     default: break;
   }
   return false;

src/kind.h

@@ -19,16 +19,16 @@ namespace ethos {
 enum class Kind
 {
   NONE = 0,
-  
+
   // types
   TYPE,
   FUNCTION_TYPE,
   PROOF_TYPE,
   ABSTRACT_TYPE,
   BOOL_TYPE,
   QUOTE_TYPE,
-  OPAQUE_TYPE, // an argument marked :opaque, temporary during parsing
-  
+  OPAQUE_TYPE,  // an argument marked :opaque, temporary during parsing
+
   // terms
   APPLY,
   LAMBDA,
@@ -101,7 +101,10 @@ enum class Kind
   EVAL_TO_INT,
   EVAL_TO_RAT,
   EVAL_TO_BIN,
-  EVAL_TO_STRING
+  EVAL_TO_STRING,
+  // datatypes
+  EVAL_DT_CONSTRUCTORS,
+  EVAL_DT_SELECTORS
 };
 
 /** Print a kind to the stream, for debugging */

src/state.cpp

@@ -145,19 +145,12 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("concat", Kind::EVAL_CONCAT);
   bindBuiltinEval("extract", Kind::EVAL_EXTRACT);
   bindBuiltinEval("find", Kind::EVAL_FIND);
+  // datatypes
+  bindBuiltinEval("dt_constructors", Kind::EVAL_DT_CONSTRUCTORS);
+  bindBuiltinEval("dt_selectors", Kind::EVAL_DT_SELECTORS);
 
   // as
   bindBuiltinEval("as", Kind::AS);
-
-  // we do not export eo::null
-  // for now, eo::? is (undocumented) syntax for abstract type
-  bind("eo::?", mkAbstractType());
-  // self is a distinguished parameter
-  d_self = Expr(mkSymbolInternal(Kind::PARAM, "eo::self", mkAbstractType()));
-  bind("eo::self", d_self);
-  d_conclusion = Expr(mkSymbolInternal(Kind::PARAM, "eo::conclusion", mkBoolType()));
-  // eo::conclusion is not globally bound, since it can only appear
-  // in :requires.
 
   // note we don't allow parsing (Proof ...), (Quote ...), or (quote ...).
 
@@ -168,6 +161,31 @@ State::State(Options& opts, Stats& stats)
   bind("true", d_true);
   d_false = Expr(new Literal(false));
   bind("false", d_false);
+
+  // builtin lists
+  d_listType = Expr(mkSymbolInternal(Kind::CONST, "eo::List", d_type));
+  bind("eo::List", d_listType);
+  d_listNil = Expr(mkSymbolInternal(Kind::CONST, "eo::List::nil", d_listType));
+  bind("eo::List::nil", d_listNil);
+  Expr t = Expr(mkSymbolInternal(Kind::PARAM, "T", d_type));
+  std::vector<Expr> argTypes;
+  argTypes.push_back(t);
+  argTypes.push_back(d_listType);
+  Expr consType = mkFunctionType(argTypes, d_listType);
+  d_listCons = Expr(mkSymbolInternal(Kind::CONST, "eo::List::cons", consType));
+  bind("eo::List::cons", d_listCons);
+  markConstructorKind(d_listCons, Attr::RIGHT_ASSOC_NIL, d_listNil);
+
+  // we do not export eo::null
+  // for now, eo::? is (undocumented) syntax for abstract type
+  bind("eo::?", d_absType);
+  // self is a distinguished parameter
+  d_self = Expr(mkSymbolInternal(Kind::PARAM, "eo::self", d_absType));
+  bind("eo::self", d_self);
+  d_conclusion =
+      Expr(mkSymbolInternal(Kind::PARAM, "eo::conclusion", d_boolType));
+  // eo::conclusion is not globally bound, since it can only appear
+  // in :requires.
 }
 
 State::~State() {}
@@ -539,6 +557,9 @@ Expr State::mkBoolType()
 {
   return d_boolType;
 }
+
+Expr State::mkListType() { return d_listType; }
+
 Expr State::mkProofType(const Expr& proven)
 {
   return Expr(mkExprInternal(Kind::PROOF_TYPE, {proven.getValue()}));
@@ -961,6 +982,18 @@ Expr State::mkParameterized(const ExprValue* hd, const std::vector<Expr>& params
   return mkExpr(Kind::PARAMETERIZED, {mkExpr(Kind::TUPLE, params), Expr(hd)});
 }
 
+Expr State::mkList(const std::vector<Expr>& args)
+{
+  if (args.empty())
+  {
+    return d_listNil;
+  }
+  std::vector<Expr> largs;
+  largs.push_back(d_listCons);
+  largs.insert(largs.end(), args.begin(), args.end());
+  return mkExpr(Kind::APPLY, largs);
+}
+
 ExprValue* State::mkLiteralInternal(Literal& l)
 {
   d_stats.d_mkExprCount++;

src/state.h

@@ -103,6 +103,8 @@ class State
   Expr mkAbstractType();
   /** Bool */
   Expr mkBoolType();
+  /** eo::List */
+  Expr mkListType();
   /** (Proof <proven>) */
   Expr mkProofType(const Expr& proven);
   /** (Quote <term>) */
@@ -138,6 +140,11 @@ class State
    * Make parameterized with given parameters
    */
   Expr mkParameterized(const ExprValue* hd, const std::vector<Expr>& params);
+  /**
+   * Make (eo::List::Cons <args>) if args is non-empty or eo::List::nil
+   * otherwise.
+   */
+  Expr mkList(const std::vector<Expr>& args);
   //--------------------------------------
   /** Get the constructor kind for symbol v */
   Attr getConstructorKind(const ExprValue* v) const;
@@ -205,6 +212,9 @@ class State
   Expr d_self;
   Expr d_conclusion;
   Expr d_fail;
+  Expr d_listType;
+  Expr d_listNil;
+  Expr d_listCons;
   /** Get base operator */
   const ExprValue* getBaseOperator(const ExprValue * v) const;
   /** Mark that file s was included */

src/type_checker.cpp

@@ -178,8 +178,8 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_IS_STR:
     case Kind::EVAL_IS_BOOL:
     case Kind::EVAL_IS_VAR:
-      ret = (nargs==1);
-      break;
+    case Kind::EVAL_DT_CONSTRUCTORS:
+    case Kind::EVAL_DT_SELECTORS: ret = (nargs == 1); break;
     case Kind::EVAL_NIL:
       ret = (nargs>=1);
       break;
@@ -1173,6 +1173,23 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       }
     }
     break;
+    case Kind::EVAL_DT_CONSTRUCTORS:
+    case Kind::EVAL_DT_SELECTORS:
+    {
+      AppInfo* ac = d_state.getAppInfo(args[0]);
+      if (ac != nullptr)
+      {
+        Assert(args[0]->isGround());
+        Attr a = ac->d_attrCons;
+        if ((a == Attr::DATATYPE && k == Kind::EVAL_DT_CONSTRUCTORS)
+            || (a == Attr::DATATYPE_CONSTRUCTOR
+                && k == Kind::EVAL_DT_SELECTORS))
+        {
+          return ac->d_attrConsTerm;
+        }
+      }
+    }
+    break;
     default:
       break;
   }
@@ -1445,6 +1462,8 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
       return getOrSetLiteralTypeRule(Kind::STRING);
     case Kind::EVAL_TO_BIN:
       return getOrSetLiteralTypeRule(Kind::BINARY);
+    case Kind::EVAL_DT_CONSTRUCTORS:
+    case Kind::EVAL_DT_SELECTORS: return d_state.mkListType().getValue();
     default:break;
   }
   if (out)

tests/CMakeLists.txt

@@ -128,6 +128,8 @@ set(ethos_test_file_list
     simple-lra-reference.eo
     left-cons.eo
     overload-standalone.eo
+    datatypes-split-rule.eo
+    singular-datatype.eo
     simul-overload.eo
     bang-lex.eo
 )

tests/datatypes-split-rule.eo

@@ -0,0 +1,47 @@
+; (declare-type eo::List ())
+; (declare-const eo::List::nil eo::List)
+; (declare-const eo::List::cons (-> (! Type :var T :implicit) T eo::List eo::List))
+
+(declare-type Int ())
+(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
+
+
+
+
+(declare-const is (-> (! Type :var C :implicit) (! Type :var D :implicit) C D Bool))
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(program $mk_dt_split ((D Type) (x D) (T Type) (c T) (xs eo::List :list))
+  (eo::List D) Bool
+  (
+    (($mk_dt_split eo::List::nil x)          false)
+    (($mk_dt_split (eo::List::cons c xs) x)  (eo::cons or (is c x) ($mk_dt_split xs x)))
+  )
+)
+
+(declare-rule dt-split ((D Type) (x D))
+  :args (x)
+  :conclusion ($mk_dt_split (eo::dt_constructors (eo::typeof x)) x)
+)
+
+(declare-const x Lst)
+
+(step @p0 (or (is cons x) (is nil x)) :rule dt-split :args (x))
+
+
+(program $mk_dt_inst ((D Type) (x D) (T Type) (t T) (S Type) (s S) (xs eo::List :list))
+  (eo::List D T) Bool
+  (
+    (($mk_dt_inst eo::List::nil x t)          t)
+    (($mk_dt_inst (eo::List::cons s xs) x t)  ($mk_dt_inst xs x (t (s x))))
+  )
+)
+
+(declare-rule dt-inst ((D Type) (T Type) (c T) (x D))
+  :args (c x)
+  :conclusion (= (is c x) (= x ($mk_dt_inst (eo::dt_selectors c) x c)))
+)
+
+(step @p1 (= (is cons x) (= x (cons (head x) (tail x)))) :rule dt-inst :args (cons x))
+(step @p1 (= (is nil x) (= x nil)) :rule dt-inst :args (nil x))

tests/singular-datatype.eo

@@ -0,0 +1 @@
+(declare-datatype a ((b)))