diff --git a/include/anthem/AST.h b/include/anthem/AST.h new file mode 100644 index 0000000..5463bb4 --- /dev/null +++ b/include/anthem/AST.h @@ -0,0 +1,151 @@ +#ifndef __ANTHEM__AST_H +#define __ANTHEM__AST_H + +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// AST +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Primitives +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct BinaryOperation +{ + enum class Operator + { + Add, + Subtract + }; + + Operator operator_; + Term left; + Term right; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Boolean +{ + bool value = false; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Equals +{ + Term left; + Term right; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Function +{ + const char *name = nullptr; + std::vector arguments; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Integer +{ + int value; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct IntegerRange +{ + Integer from; + Integer to; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Predicate +{ + const char *name = nullptr; + std::vector arguments; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Variable +{ + const char *name = nullptr; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Expressions +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct And +{ + std::vector arguments; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Biconditional +{ + Formula left; + Formula right; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Exists +{ + std::vector variables; + Formula formula; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct ForAll +{ + std::vector variables; + Formula formula; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Implies +{ + Formula antecedent; + Formula consequent; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Not +{ + Formula argument; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Or +{ + std::vector arguments; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h new file mode 100644 index 0000000..4c9f3c2 --- /dev/null +++ b/include/anthem/ASTForward.h @@ -0,0 +1,97 @@ +#ifndef __ANTHEM__AST_FORWARD_H +#define __ANTHEM__AST_FORWARD_H + +#include +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// AST Forward Declarations +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct And; +struct BinaryOperation; +struct Biconditional; +struct Boolean; +struct Constant; +struct Equals; +struct Exists; +struct ForAll; +struct Function; +struct Implies; +struct Integer; +struct IntegerRange; +struct Not; +struct Or; +struct Predicate; +struct Variable; + +using AndPointer = std::unique_ptr; +using BinaryOperationPointer = std::unique_ptr; +using BiconditionalPointer = std::unique_ptr; +using BooleanPointer = std::unique_ptr; +using ConstantPointer = std::unique_ptr; +using EqualsPointer = std::unique_ptr; +using ExistsPointer = std::unique_ptr; +using ForAllPointer = std::unique_ptr; +using FunctionPointer = std::unique_ptr; +using ImpliesPointer = std::unique_ptr; +using IntegerPointer = std::unique_ptr; +using IntegerRangePointer = std::unique_ptr; +using NotPointer = std::unique_ptr; +using OrPointer = std::unique_ptr; +using PredicatePointer = std::unique_ptr; +using VariablePointer = std::unique_ptr; + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Variants +//////////////////////////////////////////////////////////////////////////////////////////////////// + +using TermT = mapbox::util::variant< + BinaryOperationPointer, + ConstantPointer, + IntegerPointer, + FunctionPointer, + VariablePointer>; + +class Term : public TermT +{ + using TermT::TermT; +}; + +using FormulaT = mapbox::util::variant< + AndPointer, + BiconditionalPointer, + BooleanPointer, + EqualsPointer, + ExistsPointer, + ForAllPointer, + ImpliesPointer, + NotPointer, + OrPointer, + PredicatePointer>; + +class Formula : public FormulaT +{ + using FormulaT::FormulaT; +}; + +using Formulas = std::vector; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif