We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
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:
codef
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.
The text was updated successfully, but these errors were encountered:
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)), }
Sorry, something went wrong.
No branches or pull requests
Currently we have toplevel codefinitions:
and local comatches
Morally, the
codef
construct is just syntactic sugar for:But in the implementation we don't make that explicit:
So I propose to make it explicit by changing the definition to something like:
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.
The text was updated successfully, but these errors were encountered: