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

Unify toplevel codefinition and local comatch. #194

Open
BinderDavid opened this issue May 4, 2024 · 1 comment
Open

Unify toplevel codefinition and local comatch. #194

BinderDavid opened this issue May 4, 2024 · 1 comment

Comments

@BinderDavid
Copy link
Collaborator

BinderDavid commented May 4, 2024

Currently we have toplevel codefinitions:

codef CountUp(n: Nat): Stream(Nat) {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

and local comatches

comatch {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

Morally, the codef construct is just syntactic sugar for:

let CountUp(n : Nat): Stream(Nat) {
    comatch {
      head(_) => n,
      tail(_) => CountUp(S(n)),
    }
}

But in the implementation we don't make that explicit:

#[derive(Debug, Clone)]
pub struct Codef {
    pub span: Option<Span>,
    pub doc: Option<DocComment>,
    pub name: Ident,
    pub attr: Attribute,
    pub params: Telescope,
    pub typ: TypCtor,
    pub body: Match,
}

So I propose to make it explicit by changing the definition to something like:

#[derive(Debug, Clone)]
pub struct Codef {
    pub span: Option<Span>,
    pub doc: Option<DocComment>,
    pub name: Ident,
    pub attr: Attribute,
    pub params: Telescope,
    pub typ: TypCtor,
    pub body: LocalComatch,
}

We can do a similar thing for Def/LocalMatch, but there they don't behave similarly enough yet due to the different handling of self parameters.

@BinderDavid
Copy link
Collaborator Author

I think this means that we also have to add a returns clause for local comatches, which makes sense.
Currently we cannot infer the type of a comatch:

impl CheckInfer for LocalComatch {
    fn check(&self, prg: &Prg, ctx: &mut Ctx, t: Rc<Exp>) -> Result<Self, TypeError> {
      ...
    }

    fn infer(&self, _prg: &Prg, _ctx: &mut Ctx) -> Result<Self, TypeError> {
        Err(TypeError::CannotInferComatch { span: self.span().to_miette() })
    }
}

but we can add specialized syntax for the expected return type, i.e:

comatch : Stream(Nat) {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

Then we would desugar the codefinition from above to:

let CountUp(n : Nat): Stream(Nat) {
    comatch : Stream(Nat) {
      head(_) => n,
      tail(_) => CountUp(S(n)),
    }

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

No branches or pull requests

1 participant