Drafting parametric datatypes

cvc5 · Jan 15, 2025 · 2cab579 · 2cab579
1 parent 7b9ea06
commit 2cab579
Show file tree

Hide file tree

Showing 5 changed files with 26 additions and 4 deletions.
diff --git a/src/attr.h b/src/attr.h
@@ -53,6 +53,7 @@ enum class Attr
   // datatypes
   DATATYPE,
   DATATYPE_CONSTRUCTOR,
+  PARAM_DATATYPE_CONSTRUCTOR,
   CODATATYPE
 };
 

diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
@@ -282,9 +282,10 @@ bool CmdParser::parseNextCommand()
       }
       for (std::pair<const ExprValue* const, std::vector<Expr>>& c : dtcons)
       {
+        Attr ac = Attr::DATATYPE_CONSTRUCTOR;
         Expr cons = Expr(c.first);
         Expr stuple = d_state.mkList(c.second);
-        d_state.markConstructorKind(cons, Attr::DATATYPE_CONSTRUCTOR, stuple);
+        d_state.markConstructorKind(cons, ac, stuple);
       }
       if (isMulti)
       {

diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -962,7 +962,8 @@ bool ExprParser::parseDatatypesDef(
       dti = d_state.mkExpr(Kind::APPLY, dapp);
     }
     std::vector<std::pair<std::string, Expr>> toBind;
-    parseConstructorDefinitionList(dti, dts[dt.getValue()], dtcons, toBind);
+    std::vector<Expr>& clist = dts[dt.getValue()];
+    parseConstructorDefinitionList(dti, clist, dtcons, toBind, params);
     if (pushedScope)
     {
       d_lex.eatToken(Token::RPAREN);
@@ -990,7 +991,8 @@ void ExprParser::parseConstructorDefinitionList(
     Expr& dt,
     std::vector<Expr>& conslist,
     std::map<const ExprValue*, std::vector<Expr>>& dtcons,
-    std::vector<std::pair<std::string, Expr>>& toBind)
+    std::vector<std::pair<std::string, Expr>>& toBind,
+    const std::vector<Expr>& params)
 {
   d_lex.eatToken(Token::LPAREN);
   Expr boolType = d_state.mkBoolType();
@@ -1000,6 +1002,12 @@ void ExprParser::parseConstructorDefinitionList(
     std::string name = parseSymbol();
     std::vector<Expr> typelist;
     std::vector<Expr> sels;
+    if (!params.empty())
+    {
+      Expr odt = d_state.mkQuoteType(dt);
+      odt = d_state.mkExpr(Kind::OPAQUE_TYPE, {odt});
+      typelist.push_back(odt);
+    }
     // parse another selector or close the current constructor
     while (d_lex.eatTokenChoice(Token::LPAREN, Token::RPAREN))
     {

diff --git a/src/expr_parser.h b/src/expr_parser.h
@@ -164,7 +164,8 @@ class ExprParser
       Expr& dt,
       std::vector<Expr>& conslist,
       std::map<const ExprValue*, std::vector<Expr>>& dtcons,
-      std::vector<std::pair<std::string, Expr>>& toBind);
+      std::vector<std::pair<std::string, Expr>>& toBind,
+      const std::vector<Expr>& params);
   /** Return the unsigned for the current token string. */
   uint32_t tokenStrToUnsigned();
   /**

diff --git a/src/state.cpp b/src/state.cpp
@@ -1494,13 +1494,24 @@ Expr State::getOverloadInternal(const std::vector<Expr>& overloads,
     vchildren.push_back(c.getValue());
   }
   // try overloads in order until one is found
+  Expr tmp;
   for (size_t i=0, noverloads = overloads.size(); i<noverloads; i++)
   {
     // search in reverse order, i.e. the last bound symbol takes precendence
     size_t ii = (noverloads-1)-i;
     vchildren[0] = overloads[ii].getValue();
+    if (getConstructorKind(vchildren[0]) == Attr::DATATYPE_CONSTRUCTOR)
+    {
+      Trace("overload") << "...maybe needs type argument?" << std::endl;
+      Expr cons(vchildren[0]);
+      Expr rt(retType);
+      tmp = mkExpr(Kind::APPLY_OPAQUE, {cons, rt});
+      vchildren[0] = tmp.getValue();
+    }
     Expr x = Expr(vchildren.size()>2 ? mkApplyInternal(vchildren) : mkExprInternal(Kind::APPLY, vchildren));
+    Trace("overload") << "...check type of " << x << std::endl;
     Expr t = d_tc.getType(x);
+    Trace("overload") << "...has type " << t << std::endl;
     // if term is well-formed, and matches the return type if it exists
     if (!t.isNull() && (retType==nullptr || retType==t.getValue()))
     {