diff options
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index e1518f9ca..f2044c7ef 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -573,6 +573,71 @@ public: std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false); + /** make flat function type + * + * Returns the "flat" function type corresponding to the function taking + * argument types "sorts" and range type "range". A flat function type is + * one whose range is not a function. Notice that if sorts is empty and range + * is not a function, then this function returns range itself. + * + * If range is a function type, we add its function argument sorts to sorts + * and consider its function range as the new range. For each sort S added + * to sorts in this process, we add a new bound variable of sort S to + * flattenVars. + * + * For example: + * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ): + * - returns the the function type (-> Int (-> Real Real) Int Bool) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * Notice that this method performs only one level of flattening, for example, + * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}): + * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool)) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * This method is required so that we do not return functions + * that have function return type (these give an unhandled exception + * in the ExprManager). For examples of the equivalence between function + * definitions in the proposed higher-order extension of the smt2 language, + * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf. + * + * The argument flattenVars is needed in the case of defined functions + * with function return type. These have implicit arguments, for instance: + * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x))) + * is equivalent to the command: + * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z)) + * where @ is (higher-order) application. In this example, z is added to + * flattenVars. + */ + Type mkFlatFunctionType(std::vector<Type>& sorts, + Type range, + std::vector<Expr>& flattenVars); + + /** make flat function type + * + * Same as above, but does not take argument flattenVars. + * This is used when the arguments of the function are not important (for + * instance, if we are only using this type in a declare-fun). + */ + Type mkFlatFunctionType(std::vector<Type>& sorts, Type range); + + /** make higher-order apply + * + * This returns the left-associative curried application of (function) expr to + * the arguments in args, starting at index startIndex. + * + * For example, mkHoApply( f, { a, b }, 0 ) returns + * (HO_APPLY (HO_APPLY f a) b) + * + * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where + * args[i-startIndex].getType() = Ti + * for each i where startIndex <= i < args.size(). If expr is not of this + * type, the expression returned by this method will not be well typed. + */ + Expr mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex = 0); + /** * Add an operator to the current legal set. * |