luau/EqSat/include/Luau/Language.h

386 lines
7.7 KiB
C
Raw Normal View History

Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details
#pragma once
#include "Luau/Id.h"
#include "Luau/LanguageHash.h"
#include "Luau/Slice.h"
#include "Luau/Variant.h"
#include <algorithm>
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
#include <array>
#include <type_traits>
#include <unordered_set>
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
#include <utility>
#include <vector>
#define LUAU_EQSAT_UNIT(name) \
struct name : ::Luau::EqSat::Unit<name> \
{ \
static constexpr const char* tag = #name; \
using Unit::Unit; \
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
#define LUAU_EQSAT_ATOM(name, t) \
struct name : public ::Luau::EqSat::Atom<name, t> \
{ \
static constexpr const char* tag = #name; \
using Atom::Atom; \
}
#define LUAU_EQSAT_NODE_ARRAY(name, ops) \
struct name : public ::Luau::EqSat::NodeVector<name, std::array<::Luau::EqSat::Id, ops>> \
{ \
static constexpr const char* tag = #name; \
using NodeVector::NodeVector; \
}
#define LUAU_EQSAT_NODE_VECTOR(name) \
struct name : public ::Luau::EqSat::NodeVector<name, std::vector<::Luau::EqSat::Id>> \
{ \
static constexpr const char* tag = #name; \
using NodeVector::NodeVector; \
}
#define LUAU_EQSAT_NODE_SET(name) \
struct name : public ::Luau::EqSat::NodeSet<name, std::vector<::Luau::EqSat::Id>> \
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{ \
static constexpr const char* tag = #name; \
using NodeSet::NodeSet; \
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
#define LUAU_EQSAT_NODE_ATOM_WITH_VECTOR(name, t) \
struct name : public ::Luau::EqSat::NodeAtomAndVector<name, t, std::vector<::Luau::EqSat::Id>> \
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{ \
static constexpr const char* tag = #name; \
using NodeAtomAndVector::NodeAtomAndVector; \
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
namespace Luau::EqSat
{
template<typename Phantom>
struct Unit
{
Slice<Id> mutableOperands()
{
return {};
}
Slice<const Id> operands() const
{
return {};
}
bool operator==(const Unit& rhs) const
{
return true;
}
bool operator!=(const Unit& rhs) const
{
return false;
}
struct Hash
{
size_t operator()(const Unit& value) const
{
// chosen by fair dice roll.
// guaranteed to be random.
return 4;
}
};
};
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
template<typename Phantom, typename T>
struct Atom
{
Atom(const T& value)
: _value(value)
{
}
const T& value() const
{
return _value;
}
public:
Slice<Id> mutableOperands()
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return {};
}
Slice<const Id> operands() const
{
return {};
}
bool operator==(const Atom& rhs) const
{
return _value == rhs._value;
}
bool operator!=(const Atom& rhs) const
{
return !(*this == rhs);
}
struct Hash
{
size_t operator()(const Atom& value) const
{
return languageHash(value._value);
}
};
private:
T _value;
};
template<typename Phantom, typename X, typename T>
struct NodeAtomAndVector
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
template<typename... Args>
NodeAtomAndVector(const X& value, Args&&... args)
: _value(value)
, vector{std::forward<Args>(args)...}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
}
Id operator[](size_t i) const
{
return vector[i];
}
public:
const X& value() const
{
return _value;
}
Slice<Id> mutableOperands()
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return Slice{vector.data(), vector.size()};
}
Slice<const Id> operands() const
{
return Slice{vector.data(), vector.size()};
}
bool operator==(const NodeAtomAndVector& rhs) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return _value == rhs._value && vector == rhs.vector;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
bool operator!=(const NodeAtomAndVector& rhs) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return !(*this == rhs);
}
struct Hash
{
size_t operator()(const NodeAtomAndVector& value) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
size_t result = languageHash(value._value);
hashCombine(result, languageHash(value.vector));
return result;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
};
private:
X _value;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
T vector;
};
template<typename Phantom, typename T>
struct NodeVector
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
template<typename... Args>
NodeVector(Args&&... args)
: vector{std::forward<Args>(args)...}
{
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
Id operator[](size_t i) const
{
return vector[i];
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
public:
Slice<Id> mutableOperands()
{
return Slice{vector.data(), vector.size()};
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
Slice<const Id> operands() const
{
return Slice{vector.data(), vector.size()};
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
bool operator==(const NodeVector& rhs) const
{
return vector == rhs.vector;
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
bool operator!=(const NodeVector& rhs) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return !(*this == rhs);
}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
struct Hash
{
size_t operator()(const NodeVector& value) const
{
return languageHash(value.vector);
}
};
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
private:
T vector;
};
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
template<typename Phantom, typename T>
struct NodeSet
{
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
template<typename... Args>
NodeSet(Args&&... args)
: vector{std::forward<Args>(args)...}
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
std::sort(begin(vector), end(vector));
auto it = std::unique(begin(vector), end(vector));
vector.erase(it, end(vector));
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
Id operator[](size_t i) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return vector[i];
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
public:
Slice<Id> mutableOperands()
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return Slice{vector.data(), vector.size()};
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
Slice<const Id> operands() const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return Slice{vector.data(), vector.size()};
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
bool operator==(const NodeSet& rhs) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return vector == rhs.vector;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
bool operator!=(const NodeSet& rhs) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return !(*this == rhs);
}
struct Hash
{
size_t operator()(const NodeSet& value) const
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return languageHash(value.vector);
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
};
protected:
T vector;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
};
template<typename... Ts>
struct Language final
{
using VariantTy = Luau::Variant<Ts...>;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
template<typename T>
using WithinDomain = std::disjunction<std::is_same<std::decay_t<T>, Ts>...>;
template<typename T>
Language(T&& t, std::enable_if_t<WithinDomain<T>::value>* = 0) noexcept
: v(std::forward<T>(t))
{
}
int index() const noexcept
{
return v.index();
}
/// This should only be used in canonicalization!
/// Always prefer operands()
Slice<Id> mutableOperands() noexcept
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
{
return visit(
[](auto&& v) -> Slice<Id>
{
return v.mutableOperands();
},
v
);
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
Slice<const Id> operands() const noexcept
{
return visit(
[](auto&& v) -> Slice<const Id>
{
return v.operands();
},
v
);
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
}
template<typename T>
T* get() noexcept
{
static_assert(WithinDomain<T>::value);
return v.template get_if<T>();
}
template<typename T>
const T* get() const noexcept
{
static_assert(WithinDomain<T>::value);
return v.template get_if<T>();
}
bool operator==(const Language& rhs) const noexcept
{
return v == rhs.v;
}
bool operator!=(const Language& rhs) const noexcept
{
return !(*this == rhs);
}
public:
struct Hash
{
size_t operator()(const Language& language) const
{
size_t seed = std::hash<int>{}(language.index());
hashCombine(
seed,
visit(
[](auto&& v)
{
return typename std::decay_t<decltype(v)>::Hash{}(v);
},
language.v
)
);
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
return seed;
}
};
private:
VariantTy v;
Equality graphs (#1285) Working towards a full e-graph implementation as described by the [egg paper](https://arxiv.org/pdf/2004.03082). The type system has a couple of places where e-graphs would've been useful and solved some classes of problems trivially. For example: 1. Normalization and simplification cannot handle cyclic types due to the nature of their implementation. 2. Normalization can't tell when two tables or functions are equivalent, but simplification theoretically can albeit not implemented. 3. Normalization requires deep normalization for inhabitance check, whereas simplification would've returned the `never` type itself indicating uninhabited. 4. Simplification requires constraint ordering to have perfect timing to simplify. 5. Adding a rewrite rule requires implementing it twice, once in simplification and once again in normalization with completely different code design making it hard to verify that their behavior is materially equivalent. 6. In cases where we must cache for performance, two different types that are isomorphic have different cache entries resulting in cache misses. 7. Type family reduction can handle cyclic type families, but only if the cycle is not obscured by a different type family instance. (`t1 where t1 = union<number, add<t1, number>>` is irreducible) I think we're getting the point! --- Currently the implementation is missing a few features that makes e-graphs actually useful. Those will be coming in a future PR. 1. Pattern matching, 6. Applying rewrites, 7. Rewrite until saturation, and 8. Extracting the best e-node according to some cost function.
2024-07-16 18:35:20 +01:00
};
} // namespace Luau::EqSat