Towards properties, avoid allocation of std::stringstream

src/attr.cpp

@@ -11,6 +11,9 @@ std::ostream& operator<<(std::ostream& o, Attr a)
  case Attr::IMPLICIT: o << "IMPLICIT"; break;
  case Attr::LIST: o << "LIST"; break;
  case Attr::SYNTAX: o << "SYNTAX"; break;
+ case Attr::RIGHT_ASSOC: o << "RIGHT_ASSOC"; break;
+ case Attr::LEFT_ASSOC: o << "LEFT_ASSOC"; break;
+ case Attr::CHAINABLE: o << "CHAINABLE"; break;
  default: o << "UnknownAttr(" << unsigned(a) << ")"; break;
  }
  return o;

src/attr.h

@@ -16,7 +16,11 @@ enum class Attr
  VAR,
  IMPLICIT,
  LIST,
- SYNTAX
+ SYNTAX,
+
+ RIGHT_ASSOC,
+ LEFT_ASSOC,
+ CHAINABLE
 };
 
 /** Print a kind to the stream, for debugging */

src/expr_info.cpp

@@ -2,7 +2,9 @@
 
 namespace alfc {
 
-ExprInfo::ExprInfo() : d_kind(Kind::NONE), d_isClosure(false) {}
+ExprInfo::ExprInfo() {}
+
+AppInfo::AppInfo() : d_attrCons( ), d_kind(Kind::NONE), d_isClosure(false) {}
 
 
 } // namespace alfc

src/expr_info.h

@@ -1,11 +1,17 @@
 #ifndef EXPR_INFO_H
 #define EXPR_INFO_H
 
+#include <unordered_set>
 #include <string>
+#include <memory>
+
 #include "kind.h"
+#include "attr.h"
 
 namespace alfc {
 
+class ExprValue;
+
 class ExprInfo
 {
 public:
@@ -14,6 +20,21 @@ class ExprInfo
  * String data
  */
  std::string d_str;
+};
+
+/**
+ * Information about how to construct applications of a function.
+ */
+class AppInfo
+{
+public:
+ AppInfo();
+ /** Attribute */
+ Attr d_attrCons;
+ /** Attribute */
+ std::shared_ptr<ExprValue> d_attrConsTerm;
+ /** Other marked attributes */
+ std::unordered_set<Attr> d_attrs;
  /**
  * Associated kind
  */

src/expr_parser.cpp

@@ -62,6 +62,10 @@ ExprParser::ExprParser(Lexer& lex, State& state)
  d_strToAttr[":var"] = Attr::VAR;
  d_strToAttr[":implicit"] = Attr::IMPLICIT;
  d_strToAttr[":list"] = Attr::LIST;
+ d_strToAttr[":syntax"] = Attr::SYNTAX;
+ d_strToAttr[":right-assoc"] = Attr::RIGHT_ASSOC;
+ d_strToAttr[":left-assoc"] = Attr::LEFT_ASSOC;
+ d_strToAttr[":chainable"] = Attr::CHAINABLE;
 
  d_strToLiteralKind["<numeral>"] = Kind::INTEGER;
  d_strToLiteralKind["<decimal>"] = Kind::DECIMAL;
@@ -560,6 +564,18 @@ void ExprParser::parseAttributeList(const Expr& e, std::map<Attr, Expr>& attrs)
  case Attr::IMPLICIT:
  // requires no value
  break;
+ case Attr::RIGHT_ASSOC:
+ case Attr::LEFT_ASSOC:
+ case Attr::CHAINABLE:
+ {
+ // optional value
+ Token tok = d_lex.peekToken();
+ if (tok!=Token::RPAREN && tok!=Token::KEYWORD)
+ {
+ val = parseExpr();
+ }
+ } 
+ break;
  default:
  d_lex.parseError("Unhandled attribute");
  break;
@@ -634,10 +650,14 @@ void ExprParser::bind(const std::string& name, const Expr& e)
 Expr ExprParser::typeCheck(Expr& e)
 {
  // type check immediately
- std::stringstream ss;
- Expr v = d_state.getTypeChecker().getType(e, ss);
+ Expr v = d_state.getTypeChecker().getType(e);
  if (v==nullptr)
  {
+ // we allocate stringstream for error messages only when an error occurs
+ // thus, we require recomputing the error message here.
+ std::stringstream ss;
+ v = d_state.getTypeChecker().getType(e, &ss);
+ //Assert (v==nullptr);
  std::stringstream msg;
  msg << "Type checking failed:" << std::endl;
  msg << "Expression: " << e << std::endl;

src/state.cpp

@@ -157,11 +157,30 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
  {
  // Assert (!children.empty());
  // see if there is a special kind for the head
- ExprInfo * ei = getInfo(children[0].get());
- if (ei!=nullptr && ei->d_kind!=Kind::NONE)
+ AppInfo * ai = getAppInfo(children[0].get());
+ if (ai!=nullptr)
  {
- std::vector<Expr> achildren(children.begin()+1, children.end());
- return mkExprInternal(ei->d_kind, achildren);
+ // if it corresponds to a builtin operator
+ if (ai->d_kind!=Kind::NONE)
+ {
+ std::vector<Expr> achildren(children.begin()+1, children.end());
+ return mkExprInternal(ai->d_kind, achildren);
+ }
+ // if it has a constructor attribute
+ switch (ai->d_attrCons)
+ {
+ case Attr::LEFT_ASSOC:
+ break;
+ case Attr::RIGHT_ASSOC:
+ break;
+ case Attr::CHAINABLE:
+ {
+ std::vector<Expr> children;
+ } 
+ break;
+ default:
+ break;
+ }
  }
  }
  return mkExprInternal(k, children);
@@ -219,8 +238,8 @@ bool State::bind(const std::string& name, const Expr& e)
 
 bool State::isClosure(const Expr& e) const 
 {
- std::map<const ExprValue *, ExprInfo>::const_iterator it = d_exprData.find(e.get());
- if (it!=d_exprData.end())
+ std::map<const ExprValue *, AppInfo>::const_iterator it = d_appData.find(e.get());
+ if (it!=d_appData.end())
  {
  return it->second.d_isClosure;
  }
@@ -252,6 +271,16 @@ ExprInfo* State::getOrMkInfo(const ExprValue* e)
  return &d_exprData[e];
 }
 
+AppInfo* State::getAppInfo(const ExprValue* e)
+{
+ std::map<const ExprValue *, AppInfo>::iterator it = d_appData.find(e);
+ if (it!=d_appData.end())
+ {
+ return &it->second;
+ }
+ return nullptr;
+}
+
 TypeChecker& State::getTypeChecker()
 {
  return d_tc;
@@ -270,9 +299,9 @@ void State::bindBuiltin(const std::string& name, Kind k, bool isClosure, const E
  if (isClosure || k!=Kind::NONE)
  {
  // associate the information
- ExprInfo * ei = getOrMkInfo(c.get());
- ei->d_kind = k;
- ei->d_isClosure = isClosure;
+ AppInfo& ai = d_appData[c.get()];
+ ai.d_kind = k;
+ ai.d_isClosure = isClosure;
  }
 }
 
@@ -311,4 +340,35 @@ Expr State::evaluate(const std::vector<Expr>& children, Ctx& newCtx)
  return app;
 }
 
+bool State::markAttributes(const Expr& v, const std::map<Attr, Expr>& attrs)
+{
+ AppInfo& ai = d_appData[v.get()];
+ for (const std::pair<const Attr, Expr>& a : attrs)
+ {
+ switch(a.first)
+ {
+ case Attr::LEFT_ASSOC:
+ case Attr::RIGHT_ASSOC:
+ case Attr::CHAINABLE:
+ // it specifies how to construct this
+ ai.d_attrCons = a.first;
+ ai.d_attrConsTerm = a.second;
+ // TODO: ensure its type has the right shape here?
+ //
+ if (a.first==Attr::CHAINABLE && a.second==nullptr)
+ {
+ return false;
+ }
+ break;
+ case Attr::LIST:
+ // remember it has been marked
+ ai.d_attrs.insert(a.first);
+ break;
+ default:
+ break;
+ }
+ }
+ return true;
+}
+
 } // namespace alfc

src/state.h

@@ -6,6 +6,7 @@
 #include <string>
 #include <filesystem>
 
+#include "attr.h"
 #include "expr.h"
 #include "expr_info.h"
 #include "expr_trie.h"
@@ -73,6 +74,8 @@ class State
  /** Get the type checker */
  TypeChecker& getTypeChecker();
 
+ /** Mark information */
+ bool markAttributes(const Expr& v, const std::map<Attr, Expr>& attrs);
  /** Define program */
  void defineProgram(const Expr& v, const Expr& prog);
  /** Has program? */
@@ -82,7 +85,10 @@ class State
 private:
  /** */
  Expr mkSymbolInternal(Kind k, const std::string& name, const Expr& type);
+ /** */
  Expr mkExprInternal(Kind k, const std::vector<Expr>& children, bool doHash=true);
+ /** */
+ AppInfo* getAppInfo(const ExprValue* e);
  /** 
  * Bind builtin
  */
@@ -101,10 +107,12 @@ class State
  std::vector<size_t> d_declsSizeCtx;
  /** literals */
  std::map<const ExprValue*, ExprInfo> d_exprData;
+ /** literals */
+ std::map<const ExprValue*, AppInfo> d_appData;
  /** hash */
  std::map<Kind, ExprTrie> d_trie;
  /** hash for literals */
- std::map< std::pair<Kind, std::string>, Expr> d_literalTrie;
+ std::map<std::pair<Kind, std::string>, Expr> d_literalTrie;
  /** input file */
  std::filesystem::path d_inputFile;
  /** files included */

src/type_checker.cpp

@@ -60,7 +60,7 @@ void TypeChecker::setTypeRule(Kind k, const Expr& t)
  it->second = t;
 }
 
-Expr TypeChecker::getType(Expr& e, std::ostream& out)
+Expr TypeChecker::getType(Expr& e, std::ostream* out)
 {
  std::unordered_set<Expr> visited;
  std::vector<Expr> toVisit;
@@ -94,7 +94,7 @@ Expr TypeChecker::getType(Expr& e, std::ostream& out)
  return e->d_type;
 }
 
-Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
+Expr TypeChecker::getTypeInternal(Expr& e, std::ostream* out)
 {
  // TODO: check arities
  // TODO: don't need to check child nullptr?
@@ -111,14 +111,20 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  if (hdType->getKind()!=Kind::FUNCTION_TYPE)
  {
  // non-function at head
- out << "Non-function as head of APPLY";
+ if (out)
+ {
+ (*out) << "Non-function as head of APPLY";
+ }
  return nullptr;
  }
  std::vector<Expr>& hdtypes = hdType->d_children;
  if (hdtypes.size()!=e->d_children.size())
  {
  // incorrect arity
- out << "Incorrect arity";
+ if (out)
+ {
+ (*out) << "Incorrect arity";
+ }
  return nullptr;
  }
  Expr retType = hdtypes.back();
@@ -134,9 +140,12 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  // unification, update retType
  if (!match(hdtypes[i-1], ctype, ctx, visited))
  {
- out << "Unexpected argument type " << i << std::endl;
- out << " LHS " << hdtypes[i-1] << std::endl;
- out << " RHS " << ctype << std::endl;
+ if (out)
+ {
+ (*out) << "Unexpected argument type " << i << std::endl;
+ (*out) << " LHS " << hdtypes[i-1] << std::endl;
+ (*out) << " RHS " << ctype << std::endl;
+ }
  return nullptr;
  }
  }
@@ -178,7 +187,10 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  }
  if (ctype->getKind()!=Kind::BOOL_TYPE)
  {
- out << "Non-Bool for argument of Proof";
+ if (out)
+ {
+ (*out) << "Non-Bool for argument of Proof";
+ }
  return nullptr;
  }
  }
@@ -194,7 +206,10 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  }
  if (ctype->getKind()!=Kind::TYPE)
  {
- out << "Non-type for function";
+ if (out)
+ {
+ (*out) << "Non-type for function";
+ }
  return nullptr;
  }
  }
@@ -204,7 +219,10 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  {
  if (e->d_children[i]->getKind()!=Kind::PAIR)
  {
- out << "Non-pair for requires";
+ if (out)
+ {
+ (*out) << "Non-pair for requires";
+ }
  return nullptr;
  }
  }
@@ -234,7 +252,10 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream& out)
  default:
  break;
  }
- out << "Unknown kind " << e->getKind();
+ if (out)
+ {
+ (*out) << "Unknown kind " << e->getKind();
+ }
  return nullptr;
 }
 

src/type_checker.h

@@ -20,7 +20,7 @@ class TypeChecker
  TypeChecker(State& s);
  ~TypeChecker();
  /** Return its type */
- Expr getType(Expr& e, std::ostream& out);
+ Expr getType(Expr& e, std::ostream* out = nullptr);
  /** Set type rule for literal */
  void setTypeRule(Kind k, const Expr& t);
  /** */
@@ -37,7 +37,7 @@ class TypeChecker
  Expr evaluate(Expr& e);
  private:
  /** Return its type */
- Expr getTypeInternal(Expr& e, std::ostream& out);
+ Expr getTypeInternal(Expr& e, std::ostream* out);
  /** The state */
  State& d_state;
  /** The builtin literal kinds */