From 0fddeedc0c47b1b1fb4ebedbb609479da1a94c6c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Nov 2024 16:52:15 -0600 Subject: [PATCH] Add two datatypes rules to CPC Eunoia signature (#11358) Also refactors tuples and nullables to use a more uniform syntax. Further rules to follow. --- proofs/eo/cpc/Cpc.eo | 2 +- proofs/eo/cpc/rules/Datatypes.eo | 146 +++++++++++++++++++++++++++ proofs/eo/cpc/theories/Datatypes.eo | 23 +++-- src/proof/alf/alf_node_converter.cpp | 30 +++--- src/proof/alf/alf_printer.cpp | 2 + 5 files changed, 179 insertions(+), 24 deletions(-) create mode 100644 proofs/eo/cpc/rules/Datatypes.eo diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo index b00f385e37b..4567a1ac56b 100644 --- a/proofs/eo/cpc/Cpc.eo +++ b/proofs/eo/cpc/Cpc.eo @@ -70,7 +70,7 @@ (include "./theories/Bags.eo") (include "./theories/FiniteFields.eo") (include "./rules/Quantifiers.eo") -(include "./theories/Datatypes.eo") +(include "./rules/Datatypes.eo") (include "./theories/SepLogic.eo") (include "./rules/Rewrites.eo") diff --git a/proofs/eo/cpc/rules/Datatypes.eo b/proofs/eo/cpc/rules/Datatypes.eo new file mode 100644 index 00000000000..7adaf46f2b0 --- /dev/null +++ b/proofs/eo/cpc/rules/Datatypes.eo @@ -0,0 +1,146 @@ +(include "../theories/Datatypes.eo") + + +; program: $dt_get_constructors +; args: +; - T Type: The datatype to get the constructors for. +; return: The list of constructors of T, as a eo::List. +; note: > +; (Unit) tuples are treated as a special case of datatypes with a single +; constructor. Parametric datatypes must reference the type constructor to +; extract their constructors. +(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type))) + (Type) eo::List + ( + (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil)) + (($dt_get_constructors UnitTuple) (eo::cons eo::List::cons tuple.unit eo::List::nil)) + (($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 + ) +) + +; program: $tuple_get_selectors_rec +; args: +; - T Type: The tuple type to get the selectors for. +; - n Int: The number of component types we have processed so far. +; return: The list of selectors of T, as a eo::List. +; note: > +; Tuples use a special selector tuple.select indexed by an integer, which is +; why they require a special method here. +(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int)) + (Type Int) Bool + ( + (($tuple_get_selectors_rec UnitTuple n) eo::List::nil) + (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1)))) + ) +) + +; program: $dt_get_selectors +; args: +; - D Type: The type to get the selectors for. +; - c T: The constructor of D. +; return: The list of selectors of c, as a eo::List. +; note: > +; (Unit) tuples are treated as a special case of datatypes whose selectors are +; tuple.select indexed by an integer, which requires the above method. +(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list)) + (Type T) eo::List + ( + (($dt_get_selectors (Tuple T1 T2) tuple) ($tuple_get_selectors_rec (Tuple T1 T2) 0)) + (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil) + (($dt_get_selectors D c) (eo::dt_selectors c)) ; user-defined datatypes + ) +) + +;;;;; ProofRule::DT_SPLIT + +; program: $mk_dt_split +; args: +; - L eo::List: The list of a constructors yet to process. +; - x D: The datatype term we are splitting on. +; return: A disjunction of testers for the constructors in L, applied to x. +(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))) + ) +) + +; rule: dt_split +; implements: ProofRule::DT_SPLIT. +; args: +; - x D: The datatype term to split on. +; conclusion: > +; A disjunction of testers, indicating the possible top symbols of x. This is +; computed by getting the constructors for the type of x and calling the above +; $mk_dt_split method. +(declare-rule dt_split ((D Type) (x D)) + :args (x) + :conclusion ($singleton_elim ($mk_dt_split ($dt_get_constructors (eo::typeof x)) x)) +) + +;;;;; ProofRewriteRule::DT_INST + +; program: $mk_dt_inst_rec +; args: +; - L eo::List: The list of a selectors yet to process. +; - x D: The datatype term we applying dt-inst to. +; - t T: The accumulated return value, which is a constructor applied to a list of testers applied to x. +; return: The result of dt-inst for x, given t and the remaining selectors in x. +(program $mk_dt_inst_rec ((D Type) (x D) (T Type) (t T) (S Type) (s S) (xs eo::List :list)) + (eo::List D T) Bool + ( + (($mk_dt_inst_rec eo::List::nil x t) t) + (($mk_dt_inst_rec (eo::List::cons s xs) x t) ($mk_dt_inst_rec xs x (t (s x)))) + ) +) + +; program: $mk_dt_inst_tuple_rec +; args: +; - T Type: The type of x we have yet to process. +; - x D: The tuple term we applying dt-inst to. +; - n Int: The number of component types of the type of x we have processed. +; return: The result of dt-inst for x, given t and the remaining selectors in x. +; note: > +; This method is different from $mk_dt_inst_rec since the constructor tuple +; is n-ary. For example, for (Tuple Int Int), this method will return +; (tuple (tuple.select 0 x) (tuple (tuple.select 1 x) tuple.unit)), whereas +; for an ordinary constructor C : (-> Int Int D) with selectors s1, s2, +; $mk_dt_inst_rec above returns (C (s1 x) (s2 x)). +(program $mk_dt_inst_tuple_rec ((D Type) (x D) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int)) + (Type D Int) Bool + ( + (($mk_dt_inst_tuple_rec UnitTuple x n) tuple.unit) + (($mk_dt_inst_tuple_rec (Tuple T1 T2) x n) (eo::cons tuple (tuple.select n x) ($mk_dt_inst_tuple_rec T2 x (eo::add n 1)))) + ) +) + +; program: $mk_dt_inst +; args: +; - D Type: The datatype we are considering. +; - c C: The constructor of datatype D. +; - x D: The datatype term of type D we are applying dt-inst to. +; return: An equality that is equivalent to (is c x). +(program $mk_dt_inst ((C Type) (D Type) (x D) (c C) (T1 Type) (T2 Type :list) (DC (-> Type Type))) + (Type C D) Bool + ( + (($mk_dt_inst (Tuple T1 T2) tuple x) ($mk_dt_inst_tuple_rec (Tuple T1 T2) x 0)) + (($mk_dt_inst UnitTuple tuple.unit x) tuple.unit) + (($mk_dt_inst D c x) ($mk_dt_inst_rec ($dt_get_selectors D c) x c)) ; user-defined datatypes + ) +) + +; rule: dt-inst +; implements: ProofRewriteRule::DT_INST. +; args: +; - eq Bool: The equality to prove. +; requires: > +; We require that $mk_dt_inst applied to the left hand side returns +; the right hand side. +; conclusion: The given equality. +(declare-rule dt-inst ((D Type) (T Type) (c T) (x D) (t T)) + :args ((= (is c x) (= x t))) + :requires ((($mk_dt_inst (eo::typeof x) c x) t)) + :conclusion (= (is c x) (= x t)) +) diff --git a/proofs/eo/cpc/theories/Datatypes.eo b/proofs/eo/cpc/theories/Datatypes.eo index d565d1ff571..47545f10e53 100644 --- a/proofs/eo/cpc/theories/Datatypes.eo +++ b/proofs/eo/cpc/theories/Datatypes.eo @@ -1,5 +1,22 @@ (include "../programs/Nary.eo") +; note: > +; This is the generic tester predicate whose first argument is expected to be +; a constructor symbol for datatype D. We do not currently check this is the +; case. +(declare-const is (-> (! Type :var C :implicit) + (! Type :var D :implicit) + C D Bool)) + +; note: > +; This is the generic updater whose first argument is expected to be +; a selector symbol for datatype D. We do not currently check this is the +; case. +(declare-const update (-> (! Type :var D :implicit) + (! Type :var T :implicit) + (! Type :var S :implicit) + S D T D)) + ; disclaimer: > ; This sort is not in the SMT-LIB standard. All further function ; symbols over this sort are also not part of the SMT-LIB standard. @@ -15,10 +32,6 @@ (declare-const tuple.select (-> (! Type :var T :implicit) (! Int :var i) T (eo::list_nth Tuple T i))) -(declare-const tuple.update - (-> (! Type :var T :implicit) (! Type :var S :implicit) - Int T S T)) -(declare-const is-tuple (-> (! Type :var T :implicit) T Bool)) ; disclaimer: > ; This sort is not in the SMT-LIB standard. All further function @@ -26,8 +39,6 @@ (declare-const Nullable (-> Type Type)) (declare-const nullable.null (-> (! Type :var T) (Nullable T))) (declare-const nullable.some (-> (! Type :var T :implicit) T (Nullable T))) -(declare-const nullable.is_some (-> (! Type :var T :implicit) (Nullable T) Bool)) -(declare-const nullable.is_null (-> (! Type :var T :implicit) (Nullable T) Bool)) (declare-const nullable.val (-> (! Type :var T :implicit) (Nullable T) T)) ; program: $get_type_nullable_lift diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index 650641e6f34..ba3aea500cd 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -457,28 +457,20 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast) { if (k == Kind::APPLY_TESTER) { + indices.clear(); size_t cindex = DType::indexOf(op); const DType& dt = DType::datatypeOf(op); + opName << "is"; if (dt.isTuple()) { - opName << "is-tuple"; - } - else if (dt.isNullable()) - { - if (cindex == 0) - { - opName << "nullable.is_null"; - } - else - { - opName << "nullable.is_some"; - } + std::string tname = dt[0].getNumArgs() == 0 ? "tuple.unit" : "tuple"; + Node tsym = mkInternalSymbol(tname, dt[0].getConstructor().getType()); + indices.push_back(tsym); } else { - opName << "is-" << dt[cindex].getConstructor(); + indices.push_back(dt[cindex].getConstructor()); } - indices.clear(); } else if (k == Kind::APPLY_UPDATER) { @@ -486,14 +478,18 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast) size_t index = DType::indexOf(op); const DType& dt = DType::datatypeOf(op); size_t cindex = DType::cindexOf(op); + opName << "update"; if (dt.isTuple()) { - opName << "tuple.update"; - indices.push_back(d_nm->mkConstInt(cindex)); + std::vector args; + args.push_back(d_nm->mkConstInt(cindex)); + Node ssym = mkInternalApp( + "tuple.select", args, dt[cindex][index].getSelector().getType()); + indices.push_back(ssym); } else { - opName << "update-" << dt[cindex][index].getSelector(); + indices.push_back(dt[cindex][index].getSelector()); } } else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV) diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 4e33c9d5aa6..7a38281a370 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -172,6 +172,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) case ProofRule::STRING_SEQ_UNIT_INJ: case ProofRule::STRING_DECOMPOSE: case ProofRule::STRING_EXT: + case ProofRule::DT_SPLIT: case ProofRule::ITE_EQ: case ProofRule::INSTANTIATE: case ProofRule::SKOLEMIZE: @@ -274,6 +275,7 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n) case ProofRewriteRule::EXISTS_ELIM: case ProofRewriteRule::QUANT_UNUSED_VARS: case ProofRewriteRule::ARRAYS_SELECT_CONST: + case ProofRewriteRule::DT_INST: case ProofRewriteRule::QUANT_MERGE_PRENEX: case ProofRewriteRule::QUANT_MINISCOPE: case ProofRewriteRule::QUANT_MINISCOPE_FV: