From 0d49e89286892ae7c46365e0b2bcf66e6cd3603a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Feb 2025 09:03:08 -0600 Subject: [PATCH] Support ambiguous parameteric datatype constructors (#106) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR ensures ethos can properly parse and type check ambiguous datatype constructors in the SMT-LIB 2.X standard. Say a datatype constructor is "ambiguous" if it of type: ``` (-> T1 ... Tn T) ``` where some free parameter of T is not contained in the free parameters of T1...Tn. (Note n may be 0). To support ambiguous datatype constructors in Eunoia/Ethos, we require several things. **(1) Their declared type is made unambiguous.** In particular, all ambiguous datatype constructors are instead defined to be of type: ``` (-> (Quote T) T1 ... Tn T) ``` This is done automatically, so that for: ``` (declare-datatypes ((List 1)) ((par (X)((nil) (cons (head X) (tail (List X))))))) ``` If the user asked for the types of the constructors, they would get: ``` (eo::typeof nil) == (-> (Quote (List X)) (List X)) (eo::typeof cons) == (-> X (List X) (List X)) ``` **(2) Type annotations on datatype constructors are treated as opaque applications.** We expect `(as nil (List Int))` to be a constant of type `(List Int)`. This is implemented by parsing `(as nil (List Int))` as `(_ nil (List Int))`, where this is an "opaque" application. Effectively, this means that `(_ nil (List Int))` is a constant symbol that is indexed by its type. Note in this understanding, Ethos is overloading the meaning of the `as` operator in SMT-LIB for two purposes. First, for overloaded symbols which is a way of determining which symbol is being referred to, and for parameteric datatypes where it is interpreted as being an (opaque) argument. Only the latter is implemented currently. **(3) Extend the semantics of eo::dt_selectors.** Currently, `(eo::dt_selectors c)` evaluates the list of selectors only if c is a constructor constant. To handle ambiguous datatype constructors, we also say that `(eo::dt_selectors (_ c T))` evaluates to the list of selectors of `c`. Example: ``` (eo::dt_selectors (as nil (List Int))) == eo::List::nil ``` **(4) Extend the semantics of eo::dt_constructors.** Currently, `(eo::dt_constructors T)` evaluates the list of constructors only if `T` is an (uninstantiated) datatype type. We extend this for instantiated datatypes to automatically apply the appropriate annotations. For example, ``` (eo::dt_constructors List) == (eo::List::cons nil (eo::List::cons cons eo::List::nil)) (eo::dt_constructors (List T)) == (eo::List::cons (as nil (List T)) (eo::List::cons cons eo::List::nil)) ``` **(5) The SMT-LIB syntax `as` is now parsed in Ethos (in all contexts).** Note this only is processed when applied to ambiguous datatype constructors. Processing `as` for symbol disambiguation is still TODO. --------- Co-authored-by: Hans-Jörg --- NEWS.md | 7 +++ src/attr.cpp | 1 + src/attr.h | 7 +-- src/cmd_parser.cpp | 9 +++- src/expr_parser.cpp | 56 +++++++++++++++++---- src/expr_parser.h | 30 ++++++++++-- src/kind.cpp | 2 + src/kind.h | 3 +- src/state.cpp | 20 +++++++- src/state.h | 4 ++ src/type_checker.cpp | 60 ++++++++++++++++++++--- tests/CMakeLists.txt | 4 ++ tests/datatypes-split-rule-param-uinst.eo | 60 +++++++++++++++++++++++ tests/datatypes-split-rule-param.eo | 46 +++++++++++++++++ tests/param-dt-parse-amb-fun.eo | 14 ++++++ tests/param-dt-parse.eo | 14 ++++++ user_manual.md | 45 ++++++++++++++++- 17 files changed, 353 insertions(+), 29 deletions(-) create mode 100644 tests/datatypes-split-rule-param-uinst.eo create mode 100644 tests/datatypes-split-rule-param.eo create mode 100644 tests/param-dt-parse-amb-fun.eo create mode 100644 tests/param-dt-parse.eo diff --git a/NEWS.md b/NEWS.md index 75a3ebc7..76cc126c 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,5 +1,12 @@ This file contains a summary of important user-visible changes. +ethos 0.1.2 prerelease +====================== + +- Adds support for the SMT-LIB `as` annotations for ambiguous datatype constructors, i.e. those whose return type cannot be inferred from its argument types. Following SMT-LIB convention, ambiguous datatype constructors are expected to be annotated with their *return* type using `as`, which internally is treated as a type argument to the constructor. +- The semantics for `eo::dt_constructors` is extended for instantiated parametric datatypes. For example calling `eo::dt_constructors` on `(List Int)` returns the list containing `cons` and `(as nil (List Int))`. +- The semantics for `eo::dt_selectors` is extended for annotated constructors. For example calling `eo::dt_selectors` on `(as nil (List Int))` returns the empty list. + ethos 0.1.1 =========== diff --git a/src/attr.cpp b/src/attr.cpp index be5b59ed..4677029b 100644 --- a/src/attr.cpp +++ b/src/attr.cpp @@ -38,6 +38,7 @@ std::ostream& operator<<(std::ostream& o, Attr a) case Attr::DATATYPE: o << "DATATYPE"; break; case Attr::CODATATYPE: o << "CODATATYPE"; break; case Attr::DATATYPE_CONSTRUCTOR: o << "DATATYPE_CONSTRUCTOR"; break; + case Attr::AMB_DATATYPE_CONSTRUCTOR: o << "AMB_DATATYPE_CONSTRUCTOR"; break; default: o << "UnknownAttr(" << unsigned(a) << ")"; break; } return o; diff --git a/src/attr.h b/src/attr.h index 39f94a66..cf7e64ba 100644 --- a/src/attr.h +++ b/src/attr.h @@ -19,7 +19,7 @@ namespace ethos { enum class Attr { NONE = 0, - + VAR, IMPLICIT, REQUIRES, @@ -34,11 +34,11 @@ enum class Attr BINDER, LET_BINDER, OPAQUE, - + // smt3 things that are not strictly supported SYNTAX, RESTRICT, - + // indicate how to construct proof rule steps PREMISE_LIST, @@ -53,6 +53,7 @@ enum class Attr // datatypes DATATYPE, DATATYPE_CONSTRUCTOR, + AMB_DATATYPE_CONSTRUCTOR, // constructors requiring an opaque type argument CODATATYPE }; diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index 8925dc3a..e7b379c0 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -243,6 +243,7 @@ bool CmdParser::parseNextCommand() std::vector arities; std::map> dts; std::map> dtcons; + std::unordered_set ambCons; if (isMulti) { d_lex.eatToken(Token::LPAREN); @@ -268,7 +269,7 @@ bool CmdParser::parseNextCommand() std::string name = d_eparser.parseSymbol(); dnames.push_back(name); } - if (!d_eparser.parseDatatypesDef(dnames, arities, dts, dtcons)) + if (!d_eparser.parseDatatypesDef(dnames, arities, dts, dtcons, ambCons)) { d_lex.parseError("Failed to bind symbols for datatype definition"); } @@ -282,9 +283,13 @@ bool CmdParser::parseNextCommand() } for (std::pair>& c : dtcons) { + // may be ambiguous + Attr ac = ambCons.find(c.first) != ambCons.end() + ? Attr::AMB_DATATYPE_CONSTRUCTOR + : 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 index eb7bf547..b18f6fc2 100644 --- a/src/expr_parser.cpp +++ b/src/expr_parser.cpp @@ -867,7 +867,8 @@ bool ExprParser::parseDatatypesDef( const std::vector& dnames, const std::vector& arities, std::map>& dts, - std::map>& dtcons) + std::map>& dtcons, + std::unordered_set& ambCons) { Assert(dnames.size() == arities.size() || (dnames.size() == 1 && arities.empty())); @@ -962,7 +963,8 @@ bool ExprParser::parseDatatypesDef( dti = d_state.mkExpr(Kind::APPLY, dapp); } std::vector> toBind; - parseConstructorDefinitionList(dti, dts[dt.getValue()], dtcons, toBind); + std::vector& clist = dts[dt.getValue()]; + parseConstructorDefinitionList(dti, clist, dtcons, toBind, ambCons, params); if (pushedScope) { d_lex.eatToken(Token::RPAREN); @@ -990,7 +992,9 @@ void ExprParser::parseConstructorDefinitionList( Expr& dt, std::vector& conslist, std::map>& dtcons, - std::vector>& toBind) + std::vector>& toBind, + std::unordered_set& ambCons, + const std::vector& params) { d_lex.eatToken(Token::LPAREN); Expr boolType = d_state.mkBoolType(); @@ -1017,6 +1021,24 @@ void ExprParser::parseConstructorDefinitionList( toBind.emplace_back(ss.str(), updater); d_lex.eatToken(Token::RPAREN); } + bool isAmb = false; + if (!params.empty()) + { + // if this is an ambiguous datatype constructor, we add (Quote T) + // as the first argument type. + Expr tup = d_state.mkExpr(Kind::TUPLE, typelist); + std::vector pargs = Expr::getVariables(tup); + Expr fv = findFreeVar(dt, pargs); + Trace("param-dt") << "Parameteric datatype constructor: " << name; + Trace("param-dt") << (fv.isNull() ? " un" : " ") << "ambiguous" + << std::endl; + if (!fv.isNull()) + { + Expr odt = d_state.mkQuoteType(dt); + typelist.insert(typelist.begin(), odt); + isAmb = true; + } + } Expr ctype = d_state.mkFunctionType(typelist, dt); Expr cons = d_state.mkSymbol(Kind::CONST, name, ctype); toBind.emplace_back(name, cons); @@ -1028,6 +1050,10 @@ void ExprParser::parseConstructorDefinitionList( Expr tester = d_state.mkSymbol(Kind::CONST, ss.str(), dtype); toBind.emplace_back(ss.str(), tester); dtcons[cons.getValue()] = sels; + if (isAmb) + { + ambCons.insert(cons.getValue()); + } } } @@ -1402,7 +1428,7 @@ Expr ExprParser::typeCheck(Expr& e, const Expr& expected) return et; } -void ExprParser::ensureBound(const Expr& e, const std::vector& bvs) +Expr ExprParser::findFreeVar(const Expr& e, const std::vector& bvs) { std::vector efv = Expr::getVariables(e); for (const Expr& v : efv) @@ -1414,14 +1440,24 @@ void ExprParser::ensureBound(const Expr& e, const std::vector& bvs) { continue; } - std::stringstream msg; - msg << "Unexpected free parameter in expression:" << std::endl; - msg << " Expression: " << e << std::endl; - msg << " Free parameter: " << v << std::endl; - msg << "Bound parameters: " << bvs << std::endl; - d_lex.parseError(msg.str()); + return v; } } + return d_null; +} + +void ExprParser::ensureBound(const Expr& e, const std::vector& bvs) +{ + Expr v = findFreeVar(e, bvs); + if (!v.isNull()) + { + std::stringstream msg; + msg << "Unexpected free parameter in expression:" << std::endl; + msg << " Expression: " << e << std::endl; + msg << " Free parameter: " << v << std::endl; + msg << "Bound parameters: " << bvs << std::endl; + d_lex.parseError(msg.str()); + } } void ExprParser::processAttributeMap(const AttrMap& attrs, diff --git a/src/expr_parser.h b/src/expr_parser.h index dafc2b6d..23efac43 100644 --- a/src/expr_parser.h +++ b/src/expr_parser.h @@ -85,11 +85,20 @@ class ExprParser * datatype_dec := * (+) | (par (+) (+)) * constructor_dec := ( ( )∗) + * + * @param dnames The names of the datatypes. + * @param arities The arities of the datatypes given by the names dnames. + * @param dts Mapping from datatypes to their constructor symbols. + * @param dtcons Mapping from constructors to their selector symbols. + * @param ambCons The subset of constructors in the domain of dtcons that are + * ambiguous constructors, i.e. require their return type as the first + * argument. */ bool parseDatatypesDef(const std::vector& dnames, const std::vector& arities, std::map>& dts, - std::map>& dtcons); + std::map>& dtcons, + std::unordered_set& ambCons); /** * Parses ':X', returns 'X' */ @@ -139,7 +148,14 @@ class ExprParser Expr getProofRule(const std::string& name); /** Bind, or throw error otherwise */ void bind(const std::string& name, Expr& e); - /** Ensure bound */ + /** + * @return a variable from the free variables of e that is not in bvs if + * one exists, or the null expression otherwise. + */ + Expr findFreeVar(const Expr& e, const std::vector& bvs); + /** + * Throw an exception if the free variables of e are not in bvs. + */ void ensureBound(const Expr& e, const std::vector& bvs); //-------------------------- end checking /** @@ -159,12 +175,20 @@ class ExprParser /** * Parse constructor definition list, add to declaration type. The expected * syntax is '(+)'. + * @param dt The datatype this constructor list is for. + * @param conslist Populated with the constructors of dt. + * @param dtcons Mapping from constructors to their selector symbols. + * @param toBind The symbols to bind. + * @param ambCons The subset of conslist that are ambiguous constructors. + * @param param The parameters of dt. */ void parseConstructorDefinitionList( Expr& dt, std::vector& conslist, std::map>& dtcons, - std::vector>& toBind); + std::vector>& toBind, + std::unordered_set& ambCons, + const std::vector& params); /** Return the unsigned for the current token string. */ uint32_t tokenStrToUnsigned(); /** diff --git a/src/kind.cpp b/src/kind.cpp index 10b3bac4..5b75480a 100644 --- a/src/kind.cpp +++ b/src/kind.cpp @@ -36,6 +36,7 @@ std::ostream& operator<<(std::ostream& o, Kind k) case Kind::TUPLE: o << "TUPLE"; break; case Kind::PROGRAM: o << "PROGRAM"; break; case Kind::AS: o << "AS"; break; + case Kind::AS_RETURN: o << "AS_RETURN"; break; case Kind::PARAMETERIZED: o << "PARAMETERIZED"; break; case Kind::APPLY_OPAQUE: o << "APPLY_OPAQUE"; break; // literals @@ -118,6 +119,7 @@ std::string kindToTerm(Kind k) case Kind::LAMBDA: ss << "lambda"; break; case Kind::PROGRAM: ss << "program"; break; case Kind::AS: ss << "eo::as"; break; + case Kind::AS_RETURN: ss << "as"; break; case Kind::PARAMETERIZED: ss << "eo::_"; break; // operations on literals default: diff --git a/src/kind.h b/src/kind.h index b8d7cad3..944c2189 100644 --- a/src/kind.h +++ b/src/kind.h @@ -34,7 +34,8 @@ enum class Kind LAMBDA, TUPLE, PROGRAM, - AS, + AS, // (eo::as t T), where T is the type of t + AS_RETURN, // SMT-LIB (as t T), where T is the return type of t PARAMETERIZED, APPLY_OPAQUE, diff --git a/src/state.cpp b/src/state.cpp index eb1787da..e3847176 100644 --- a/src/state.cpp +++ b/src/state.cpp @@ -150,6 +150,7 @@ State::State(Options& opts, Stats& stats) bindBuiltinEval("dt_selectors", Kind::EVAL_DT_SELECTORS); // as + bindBuiltin("as", Kind::AS_RETURN); bindBuiltinEval("as", Kind::AS); // note we don't allow parsing (Proof ...), (Quote ...), or (quote ...). @@ -564,6 +565,9 @@ Expr State::mkBoolType() Expr State::mkListType() { return d_listType; } +Expr State::mkListCons() { return d_listCons; } +Expr State::mkListNil() { return d_listNil; } + Expr State::mkProofType(const Expr& proven) { return Expr(mkExprInternal(Kind::PROOF_TYPE, {proven.getValue()})); @@ -912,10 +916,22 @@ Expr State::mkExpr(Kind k, const std::vector& children) << ", " << children.size() << " arguments" << std::endl; } } + else if (k == Kind::AS_RETURN) + { + // (as nil (List Int)) --> (_ nil (List Int)) + if (getConstructorKind(vchildren[0]) == Attr::AMB_DATATYPE_CONSTRUCTOR + && children.size() == 2) + { + Trace("overload") << "...type arg for ambiguous constructor" << std::endl; + return mkExpr(Kind::APPLY_OPAQUE, {children[0], children[1]}); + } + // note we don't support other uses of `as` for symbol disambiguation yet, + // we fallthrough and construct the bogus term of kind AS_RETURN. + } else if (k==Kind::AS) { - // if it has 2 children, process it, otherwise we make the bogus term - // below + // if it has 2 children, process it, otherwise we make the bogus term of + // kind AS below if (vchildren.size()==2) { Trace("overload") << "process eo::as " << children[0] << " " << children[1] << std::endl; diff --git a/src/state.h b/src/state.h index a0721ce7..22ff8d51 100644 --- a/src/state.h +++ b/src/state.h @@ -105,6 +105,10 @@ class State Expr mkBoolType(); /** eo::List */ Expr mkListType(); + /** eo::List::cons */ + Expr mkListCons(); + /** eo::List::nil */ + Expr mkListNil(); /** (Proof ) */ Expr mkProofType(const Expr& proven); /** (Quote ) */ diff --git a/src/type_checker.cpp b/src/type_checker.cpp index cac84653..7989a42b 100644 --- a/src/type_checker.cpp +++ b/src/type_checker.cpp @@ -298,11 +298,12 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out) } break; case Kind::AS: + case Kind::AS_RETURN: { // constructing an application of AS means the type was incorrect. if (out) { - (*out) << "Encountered bad type for eo::as"; + (*out) << "Encountered bad type for " << kindToTerm(k); } return d_null; } @@ -1214,23 +1215,70 @@ Expr TypeChecker::evaluateLiteralOpInternal( } } break; - case Kind::EVAL_DT_CONSTRUCTORS: case Kind::EVAL_DT_SELECTORS: { - AppInfo* ac = d_state.getAppInfo(args[0]); + // it may be an ambiguous constructor with an annotation, in which + // case we extract the underlying symbol + Expr sym(args[0]); + sym = sym.getKind() == Kind::APPLY_OPAQUE ? sym[0] : sym; + AppInfo* ac = d_state.getAppInfo(sym.getValue()); 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)) + if (a == Attr::DATATYPE_CONSTRUCTOR + || a == Attr::AMB_DATATYPE_CONSTRUCTOR) { return ac->d_attrConsTerm; } } } break; + case Kind::EVAL_DT_CONSTRUCTORS: + { + Expr sym(args[0]); + // It might be a parametric datatype? We check if it is an apply and + // that it is fully applied (i.e. its type is Type). + bool isParam = false; + if (sym.getKind() == Kind::APPLY && getType(sym) == d_state.mkType()) + { + isParam = true; + do + { + sym = sym[0]; + } while (sym.getKind() == Kind::APPLY); + } + AppInfo* ac = d_state.getAppInfo(sym.getValue()); + if (ac != nullptr && ac->d_attrCons == Attr::DATATYPE) + { + // if parametric, add opaque argument annotations to constructors + // that are marked as AMB_DATATYPE_CONSTRUCTOR. + if (isParam) + { + std::vector cargs; + Expr cop = d_state.mkListCons(); + getNAryChildren(ac->d_attrConsTerm.getValue(), + cop.getValue(), + nullptr, + cargs, + false); + std::vector cargsp; + for (ExprValue* c : cargs) + { + Expr ce(c); + if (d_state.getConstructorKind(c) == Attr::AMB_DATATYPE_CONSTRUCTOR) + { + Expr dt(args[0]); + ce = d_state.mkExpr(Kind::APPLY_OPAQUE, {ce, dt}); + } + cargsp.push_back(ce); + } + return d_state.mkList(cargsp); + } + return ac->d_attrConsTerm; + } + } + break; default: break; } diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index f4cd5c92..bf26f056 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -133,6 +133,10 @@ set(ethos_test_file_list simul-overload.eo bang-lex.eo segfault-98.eo + param-dt-parse.eo + param-dt-parse-amb-fun.eo + datatypes-split-rule-param.eo + datatypes-split-rule-param-uinst.eo ) if(ENABLE_ORACLES) diff --git a/tests/datatypes-split-rule-param-uinst.eo b/tests/datatypes-split-rule-param-uinst.eo new file mode 100644 index 00000000..127f50c9 --- /dev/null +++ b/tests/datatypes-split-rule-param-uinst.eo @@ -0,0 +1,60 @@ +; This version of the signature assumes testers are written e.g. (_ is nil), for the uninstantiated version of the constructor + +; helper method to get the *uninstantiated* form of the list of constructors of a datatype +(program $dt_get_constructors ((D Type) (T Type) (DC (-> Type Type))) + (Type) eo::List + ( + (($dt_get_constructors (DC T)) ($dt_get_constructors DC)) ; user-defined parameteric datatypes, traverse + (($dt_get_constructors D) (eo::dt_constructors D)) ; ordinary user-defined datatypes + ) +) + +(declare-type Int ()) +(declare-datatypes ((Lst 1)) ((par (X)((cons (head X) (tail (Lst X))) (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 ($dt_get_constructors (eo::typeof x)) x) +) + +(declare-const x (Lst Int)) + +(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 + (eo::define ((U (eo::typeof x))) + ($mk_dt_inst (eo::dt_selectors c) x + ; start with the *instantiated* version of the constructor, which is at the same index + (eo::list_nth + eo::List::cons + (eo::dt_constructors U) + (eo::list_find eo::List::cons ($dt_get_constructors U) c)))))) +) + +(step @p1 (= (is cons x) (= x (cons (head x) (tail x)))) :rule dt-inst :args (cons x)) +(step @p1 (= (is nil x) (= x (as nil (Lst Int)))) :rule dt-inst :args (nil x)) diff --git a/tests/datatypes-split-rule-param.eo b/tests/datatypes-split-rule-param.eo new file mode 100644 index 00000000..489cab80 --- /dev/null +++ b/tests/datatypes-split-rule-param.eo @@ -0,0 +1,46 @@ +; This version of the signature assumes testers are written e.g. (_ is (as nil (Lst Int))), for the instantiated version of the constructor + +; use SMT-LIB syntax for as +;(define as ((T Type :implicit) (x T) (S Type)) (as x S)) + +(declare-type Int ()) +(declare-datatypes ((Lst 1)) ((par (X)((cons (head X) (tail (Lst X))) (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 Int)) + +(step @p0 (or (is cons x) (is (as nil (Lst Int)) 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 (as nil (Lst Int)) x) (= x (as nil (Lst Int)))) :rule dt-inst :args ((as nil (Lst Int)) x)) diff --git a/tests/param-dt-parse-amb-fun.eo b/tests/param-dt-parse-amb-fun.eo new file mode 100644 index 00000000..8d5c0411 --- /dev/null +++ b/tests/param-dt-parse-amb-fun.eo @@ -0,0 +1,14 @@ + +(declare-type Int ()) +(declare-consts Int) + +(declare-const @test (-> (! Type :opaque :var T) Int T)) + +(define t () (@test Bool 0) :type Bool) + +(declare-datatypes ( (List 1) ) ( +(par ( X ) ( (nil (data Int)) (cons (head X) (tail (List X))))) +)) + +(define d1 () (_ (as nil (List Int)) 0) :type (List Int)) +(define d2 () (cons 0 d1) :type (List Int)) diff --git a/tests/param-dt-parse.eo b/tests/param-dt-parse.eo new file mode 100644 index 00000000..090d3f3e --- /dev/null +++ b/tests/param-dt-parse.eo @@ -0,0 +1,14 @@ + +(declare-type Int ()) +(declare-consts Int) + +(declare-const @test (-> (! Type :opaque :var T) Int T)) + +(define t () (@test Bool 0) :type Bool) + +(declare-datatypes ( (List 1) ) ( +(par ( X ) ( (nil) (cons (head X) (tail (List X))))) +)) + +(define d1 () (as nil (List Int)) :type (List Int)) +(define d2 () (cons 0 d1) :type (List Int)) diff --git a/user_manual.md b/user_manual.md index 5ef6e083..21e186b3 100644 --- a/user_manual.md +++ b/user_manual.md @@ -1173,8 +1173,8 @@ Examples of these operators are given below. ```smt (declare-datatypes ((Tree 0)) (((node (left Tree) (right Tree)) (leaf)))) -(eo::dt_constructors Tree) == (eo::List::cons node (eo::List::cons leaf eo::List::nil)) -(eo::dt_selectors node) == (eo::List::cons left (eo::List::cons right eo::List::nil)) +(eo::dt_constructors Tree) == (eo::List::cons node (eo::List::cons leaf eo::List::nil)) +(eo::dt_selectors node) == (eo::List::cons left (eo::List::cons right eo::List::nil)) (eo::dt_selectors leaf) == eo::List::nil (declare-datatypes ((Color 0)) (((red) (green) (blue)))) @@ -1230,6 +1230,47 @@ Applying the proof rule `dt-split` to a variable `x` of type `Tree` allows us to Note that the definitino of `dt-split` is applicable to *any* datatype definition. In particular, as a second example, we see the rule applied to a term `y` of type `Color` gives us a conclusion with three disjuncts. +### Parametric datatypes + +Ethos supports reasoning about parametric datatypes with ambiguous datatype construtors using the same syntax as SMT-LIB 2.6. + +In detail, we say a datatype constructor is "ambiguous" if it of type: +``` +(-> T1 ... Tn T) +``` +where some free parameter of T is not contained in the free parameters of `T1, ..., Tn`. (Note `n` may be 0). + +All ambiguous datatype constructors are required to be annotated using the SMT-LIB 2.6 syntax `(as )`. +For example: +``` +(declare-datatypes ((Tree 1)) ((par (X) (((node (left Tree) (data X) (right Tree)) (leaf)))))) +``` +In the this example, `leaf` is an ambiguous datatype constructor, while `node` is not. +Instances of ambiguous datatype constructors are expected to be annotated with their return type using the syntax e.g. `(as leaf (Tree Int))`. +This denotes a constant (e.g. a term with zero arguments), whose type is `(Tree Int)`. + +> __Note:__ Internally, all ambiguous datatype constructors are instead defined to be of type `(-> (Quote T) T1 ... Tn T)` +This is done automatically, so that for the aforementioned datatype, the type of `leaf` is `(-> (Quote (Tree X)) (Tree X))`. +Ethos interprets `(as leaf (Tree Int))` as `(_ leaf (Tree Int))`, where this is an "opaque" application (see [opaque](#opaque)). +Conceptually, this means that `(_ leaf (Tree Int))` is a constant symbol (with no children) that is indexed by its type. + +The semantics of `eo::dt_constructors` and `eo::dt_selectors` is overloaded to handle (annotated) constructors and (instantiated) parameteric datatypes. +For example, given the previous definition, note the following: +``` +(eo::dt_constructors Tree) == (eo::List::cons node (eo::List::cons leaf eo::List::nil)) +(eo::dt_constructors (Tree Int)) == (eo::List::cons node (eo::List::cons (as leaf (Tree Int)) eo::List::nil)) +(eo::dt_constructors (Tree U)) == (eo::List::cons node (eo::List::cons (as leaf (Tree U)) eo::List::nil)) + +(eo::dt_selectors node) == (eo::List::cons left (eo::List::cons data (eo::List::cons right eo::List::nil))) +(eo::dt_selectors leaf) == eo::List::nil +(eo::dt_selectors (as leaf (Tree Int))) == eo::List::nil +``` + +In particular, the constructors of a *fully* instantiated parameteric datatype are such that its ambiguous constructors are annotated in the return value, and its unambiguous constructors are included as-is. +The selectors of a constructor (which are never ambiguous) are returned independently of whether the constructor is annotated. + +> __Note:__ Note that `eo::dt_constructors` does not evaluate on parametric types that are partially applied, e.g. `(eo::dt_constructors (Pair Int))` does not evaluate, where `Pair` expects two type parameters. + ## Declaring Proof Rules The generic syntax for a `declare-rule` command accepted by `ethos` is: