AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
23 stars 2 forks source link

ETrms that contain their full context #70

Closed olynch closed 1 year ago

olynch commented 1 year ago

This changes the implementation of EGraphs so that the "arguments" to an ETrm are e-class ids for all of the variables in the context of the term constructor, as opposed to just the direct arguments to the term constructor.

I'm not sure if this is the right way to go, because in a sense this is redundant information which will potentially cause the egraph to be less efficient when rebuilding, as there are more dependencies now. On the other hand, we compute the context when we call add!, in order to compute the type information, so it might make sense to just store it, because it will be used during program extraction.

olynch commented 1 year ago

This is old enough that there isn't much of a point in keeping it around, as it is not a priority now, and if we eventually need it we'll probably rewrite it anyways.