-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Redesign proposal #21
Comments
Checking in MT if this is OK with the e-graphs implementation. I like the proposal, and it sounds like a good abstraction that fixes the leak. |
I agree with the introduction of On naming: |
I've been using |
@willow-ahrens
That's true. I was thinking of S-expressions here, |
Okay! To confirm my understanding, this proposal renames |
We used to have
but now we have
where perhaps |
Yes, all that is correct! :) |
I can start integrating this on a Metatheory branch when there's a test branch here |
Did you mean something like
? Same for MT,
Did you mean
? |
Interfaces for traversing terms is easy, but
similarterm
is the main magic of this package. The awkwardness of the current implementation is the use ofexprhead
as a keyword argument insimilarterm
. SymbolicUtils only has (mostly) terms that represent function calls, but we couldn't just ignoreexprhead
because Julia tries to dispatch on it. Also,exprhead
is set to:call
by default -- a clear sign of abstraction leak. I think it's time to take concept of a "head" seriously...The proposal is to just make
head
the first argument tosimilarterm
instead of the reference object in whose image we are trying to build the new term. It then also makes sense to renamesimilarterm
tomaketerm
. This also allows one to compute the head in other ways than using a reference term.So the new interface could be:
I'm using the word
tail
becausearguments
is already in use to mean basicallytail[2:end]
in the case that the head is a function call. It would presumably have this check programmatically, going forward.In SymbolicUtils, we would define
So this would stay within the closure of types that represent function calls.
In Metatheory you'd just need to add a MTHead type.
I have thought about this a lot, and I think it's easiest to leave
type
andmetadata
as keyword arguments, and not try to cram them intohead
or something like that, but other arguments are welcome. These are like the stuff after:
in a typed language definition.This should address #10 and answer #15.
@0x0f0f0f @willow-ahrens @YingboMa
The text was updated successfully, but these errors were encountered: