Skip to content
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

Feature/infer3 #103

Closed
wants to merge 17 commits into from
Closed

Feature/infer3 #103

wants to merge 17 commits into from

Conversation

leissa
Copy link
Member

@leissa leissa commented Oct 11, 2022

Type inference. While there is still work to do, all impala test cases work already.

@leissa leissa marked this pull request as draft October 15, 2022 14:08
@leissa
Copy link
Member Author

leissa commented Oct 15, 2022

Alright, so I did have a version where everything worked but porting the mem stuff is a bit more intrusive as loads/stores are built a lot in other phases/passes and there things are going south again. Anyway, in this current state I wouldn't merge anyway, I just wanted to have a discussion here, what exactly we want to do. So here is the problem:

  • Whenever, we need to infer sth, we create a nominal Infer node whose operand is nullptr.
  • The main magic happens when checking for alpha-equiv. If we have the situation that Infer ? should be equivalent to x, then we have Infer x.
  • Now we have those Infer x kind of nodes all over the place which is really annoying because everyone is just looking for x and fails with an error, if it sees Infer x instead.
  • For this reason, I added the Refer class that does this forwarding automatically. This works but is should really be geared even more tightly within Thorin.

So here is my proposal:

  • class Def becomes class Def_ (or does anyone has a better name)?.
  • You are not supposed to work directly with const Def_* anymore. For this reason, we have a class Def (like Refer) but even more tightly geared into Thorin. E.g., even the the operands, types etc should be of type Def or ArrayRef<Def> instead of const Def_* or ArrayRef<const Def_*>:
    const Def_* refer(const Def_* def) {
        if (!def) return nullptr;
    
        // find inferred Def_ through chain of Infers
        while (auto infer = def->isa<Infer>()) {
            if (auto op = infer->op())
                def = op;
            else
                break;
        }
    
        // TODO union-find-like path compression
        return def;
    }
    
    template<class D = Def_>
    class Def {
    public:
        Def() = default;
        Def(const D* ptr)
            : ptr_(ptr) {}
    
        const D* operator*() const { return refer(ptr_); }
        const D* operator->() const { return refer(ptr_); }
        operator const D*() const { return refer(ptr_); } // maybe we don't even need this one
        explicit operator bool() const { return ptr_; }
    
    private:
        const D* ptr_ = nullptr;
    };
    
    using Defs = Array<Def>;
  • For subclassing we could do Def<App>. E.g.:
    if (Def<App> app = def->isa<App>()) { // usually you are using "auto app = ..." anyway
    }
  • Only for nominals we would directly work with the pointers Def_*. Alternatively, we could add another wrapper class Nom and Nom<Lam> etc.
  • Has the additional advantage that we can hook in potentially other machinery into Def if we need this later on - e.g. using operator== for alpha-equiv.
  • One question is whether we want to keep all methods within Def_ or whether we should move it to Def. The latter option is weird because at least for virtual methods we need to work with const Def_* anyway and it's probably awkward to do def.foo() but def->rebuild(/*...*/).

Any opinions on that or other ideas?

@leissa leissa closed this Dec 9, 2022
@leissa leissa deleted the feature/infer3 branch April 17, 2023 13:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant