.

docs/main.typ

@@ -33,7 +33,7 @@ isn't checked.
   [(infallible) *pattern*], [binder #mbnf("| (") #rsyn(`[`) #mbnf("(") pattern #mbnf(")") #rsyn(`,`) #mbnf("*") #rsyn(`]`) #mbnf(")")], [a pattern is used to (optionally) destructure data],
   [*expr*(essions)], [
     #mbnf("(") #rsyn(`λ`) pattern #mbnf("(") #rsyn(`:`) expr #mbnf(")?") #rsyn(`→`) expr #mbnf(")") \
-  #mbnf("| (") #rsyn(`π`) pattern #rsyn(`:`) expr #rsyn(`→`) expr #mbnf(")") \
+  #mbnf("| (") #rsyn(`Λ`) pattern #rsyn(`:`) expr #rsyn(`→`) expr #mbnf(")") \
   #mbnf("| (") #rsyn(`&`) ident #mbnf(") | (") #rsyn(`^&`)  ident #mbnf(")") \
   #mbnf("| (") #rsyn(`@{`) expr #rsyn(`}&`) expr #mbnf(")")
   ], [],
@@ -68,3 +68,9 @@ There exist a few escape hooks for this. References and types can be freely dupl
 And these rules don't apply in the result side of dependently typed functions (but they apply in
 functions invoked by them because the system doesn't have global knowledge if a function only ever
 gets invoked by result sides of dependently typed functions).
+
+== Closures
+
+Closures are a bit complicated, because they can bind stuff linearly
+(which in turn means they themselves can only be used linearly), and because they can bind references from
+their environment, which means that it must be possible to track these bound references.

rust/crates/yanais-syntax/src/error.rs

@@ -0,0 +1,148 @@
+/*
+ * SPDX-FileCopyrightText: 2023 Alain Zscheile <fogti+devel@ytrizja.de>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+use core::{fmt, result::Result as CoreResult};
+use miette::Diagnostic;
+use std::sync::Arc;
+
+use crate::EvEqSourceSpan;
+
+#[derive(Clone, Debug)]
+pub struct Error {
+    pub span: EvEqSourceSpan,
+    pub kind: ErrorKind,
+}
+
+impl fmt::Display for Error {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        if f.alternate() {
+            write!(f, "{}: ", self.span)?;
+        }
+        fmt::Display::fmt(&self.kind, f)
+    }
+}
+
+impl std::error::Error for Error {
+    #[inline(always)]
+    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
+        self.kind.source()
+    }
+}
+
+pub type Result<T> = CoreResult<T, Error>;
+
+#[derive(Debug)]
+pub struct FullError {
+    pub span: EvEqSourceSpan,
+    pub kind: ErrorKind,
+    pub code: miette::NamedSource,
+}
+
+impl Error {
+    #[inline]
+    pub fn with_code(self, code: miette::NamedSource) -> FullError {
+        FullError {
+            span: self.span,
+            kind: self.kind,
+            code,
+        }
+    }
+}
+
+impl fmt::Display for FullError {
+    #[inline(always)]
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        fmt::Display::fmt(&self.kind, f)
+    }
+}
+
+impl std::error::Error for FullError {
+    #[inline(always)]
+    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
+        self.kind.source()
+    }
+}
+
+impl miette::Diagnostic for FullError {
+    #[inline(always)]
+    fn code<'a>(&'a self) -> Option<Box<dyn fmt::Display + 'a>> {
+        self.kind.code()
+    }
+
+    #[inline(always)]
+    fn severity(&self) -> Option<miette::Severity> {
+        None
+    }
+
+    #[inline(always)]
+    fn source_code(&self) -> Option<&dyn miette::SourceCode> {
+        Some(&self.code)
+    }
+
+    #[inline(always)]
+    fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
+        use miette::LabeledSpan as Lsp;
+        Some(Box::new(
+            Some(Lsp::new(None, self.span.0.offset(), self.span.0.len())).into_iter(),
+        ))
+    }
+}
+
+#[derive(Clone, Debug, Diagnostic, thiserror::Error)]
+pub enum ErrorKind {
+    #[error("expected {0}")]
+    #[diagnostic(code(yanais::parser::expected))]
+    Expected(ErrorCtx),
+
+    #[error("end of file encountered inside {0}")]
+    #[diagnostic(code(yanais::parser::unexpected_eof))]
+    UnexpectedEof(ErrorCtx),
+
+    #[error("unhandled character '{0}'")]
+    #[diagnostic(code(yanais::lexer::unhandled_char))]
+    UnhandledChar(char),
+
+    #[error(transparent)]
+    #[diagnostic(code(yanais::parser::invalid_int))]
+    InvalidInt(#[from] core::num::ParseIntError),
+
+    #[error("comment nesting overflowed")]
+    #[diagnostic(code(yanais::lexer::comment_nest_overflow))]
+    CommentNestOverflow,
+
+    #[error("duplicated record field identifier {0:?}")]
+    #[diagnostic(code(yanais::parser::record_dup_ident))]
+    RecordDupIdent(Arc<str>),
+
+    #[error("unknown identifer {0:?}")]
+    #[diagnostic(code(yanais::parser::unknown_ident))]
+    UnknownIdent(Arc<str>),
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum ErrorCtx {
+    Comment,
+    Literal,
+    Pattern,
+    Record,
+    Select,
+    String,
+    Ident,
+}
+
+impl fmt::Display for ErrorCtx {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(match self {
+            ErrorCtx::Comment => "comment",
+            ErrorCtx::Literal => "literal",
+            ErrorCtx::Pattern => "pattern",
+            ErrorCtx::Record => "record",
+            ErrorCtx::Select => "selection",
+            ErrorCtx::String => "string",
+            ErrorCtx::Ident => "identifier",
+        })
+    }
+}

rust/crates/yanais-syntax/src/expr.rs

@@ -0,0 +1,22 @@
+use crate::{pat::Pattern, record::Record, EvEqSourceSpan};
+use yanais_literal::Literal;
+
+#[derive(Clone, Debug)]
+pub struct Lambda {
+    pub pat: Pattern,
+    pub ty: Option<Box<Expr>>,
+    pub res: Box<Expr>,
+}
+
+#[derive(Clone, Debug)]
+pub enum Expr {
+    Literal(Literal),
+
+    Lambda(Lambda),
+    TyLambda(Lambda),
+    LinTyLambda(Lambda),
+    Apply(Box<Expr>, Vec<(EvEqSourceSpan, Expr)>),
+
+    Record(Record<Expr>),
+    TyRecord(Record<Expr>),
+}

rust/crates/yanais-syntax/src/kw.rs

@@ -8,12 +8,20 @@ use crate::{lex, Env as ParseEnv, Error, ErrorCtx, EvEqSourceSpan, MaybeParse, P
 
 pub use yanais_literal::{IntSize, Literal, TyLit};
 
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub enum Kw {
+    Literal(Literal),
+    Lambda,
+    TyLambda,
+    TyLambdaLin,
+}
+
 impl ParseDefaultCtx for (EvEqSourceSpan, Literal) {
     const DFL_CTX: ErrorCtx = ErrorCtx::Literal;
 }
 
-impl MaybeParse<Literal> for (EvEqSourceSpan, Literal) {
-    fn maybe_parse(env: &mut ParseEnv<'_, Literal>) -> Result<Option<Self>, Error> {
+impl MaybeParse<Kw> for (EvEqSourceSpan, Literal) {
+    fn maybe_parse(env: &mut ParseEnv<'_, Kw>) -> Result<Option<Self>, Error> {
         let mut nxtlxr = env.lxr.clone();
         let lex::Token {
             kind,
@@ -25,7 +33,7 @@ impl MaybeParse<Literal> for (EvEqSourceSpan, Literal) {
 
         use lex::TokenKind as Tk;
         Ok(match kind {
-            Tk::Kw(lit) => {
+            Tk::Kw(Kw::Literal(lit)) => {
                 env.lxr = nxtlxr;
                 Some((tok_span, lit))
             }
@@ -33,3 +41,19 @@ impl MaybeParse<Literal> for (EvEqSourceSpan, Literal) {
         })
     }
 }
+
+impl core::str::FromStr for Kw {
+    type Err = ();
+
+    fn from_str(s: &str) -> Result<Kw, ()> {
+        if let Ok(lit) = s.parse::<Literal>() {
+            return Ok(Kw::Literal(lit));
+        }
+        Ok(match s {
+            "λ" => Kw::Lambda,
+            "Λ" => Kw::TyLambda,
+            "Λlin" => Kw::TyLambdaLin,
+            _ => return Err(()),
+        })
+    }
+}

rust/crates/yanais-syntax/src/lib.rs

@@ -4,12 +4,17 @@
  * SPDX-License-Identifier: Apache-2.0
  */
 
-use core::{cmp, fmt, result::Result as CoreResult};
-use miette::{Diagnostic, SourceSpan};
+use core::{cmp, fmt};
+use miette::SourceSpan;
 use std::sync::Arc;
 
+mod error;
+pub use error::{Error, ErrorCtx, ErrorKind, FullError, Result};
+
+pub mod expr;
+mod kw;
+pub use kw::Kw;
 pub mod lex;
-pub mod literal;
 pub mod pat;
 pub mod record;
 
@@ -91,143 +96,6 @@ impl<'a> From<&'a EvEqSourceSpan> for SourceSpan {
     }
 }
 
-#[derive(Clone, Debug)]
-pub struct Error {
-    pub span: EvEqSourceSpan,
-    pub kind: ErrorKind,
-}
-
-impl fmt::Display for Error {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        if f.alternate() {
-            write!(f, "{}: ", self.span)?;
-        }
-        fmt::Display::fmt(&self.kind, f)
-    }
-}
-
-impl std::error::Error for Error {
-    #[inline(always)]
-    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
-        self.kind.source()
-    }
-}
-
-pub type Result<T> = CoreResult<T, Error>;
-
-#[derive(Debug)]
-pub struct FullError {
-    pub span: EvEqSourceSpan,
-    pub kind: ErrorKind,
-    pub code: miette::NamedSource,
-}
-
-impl Error {
-    #[inline]
-    pub fn with_code(self, code: miette::NamedSource) -> FullError {
-        FullError {
-            span: self.span,
-            kind: self.kind,
-            code,
-        }
-    }
-}
-
-impl fmt::Display for FullError {
-    #[inline(always)]
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        fmt::Display::fmt(&self.kind, f)
-    }
-}
-
-impl std::error::Error for FullError {
-    #[inline(always)]
-    fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
-        self.kind.source()
-    }
-}
-
-impl miette::Diagnostic for FullError {
-    #[inline(always)]
-    fn code<'a>(&'a self) -> Option<Box<dyn fmt::Display + 'a>> {
-        self.kind.code()
-    }
-
-    #[inline(always)]
-    fn severity(&self) -> Option<miette::Severity> {
-        None
-    }
-
-    #[inline(always)]
-    fn source_code(&self) -> Option<&dyn miette::SourceCode> {
-        Some(&self.code)
-    }
-
-    #[inline(always)]
-    fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
-        use miette::LabeledSpan as Lsp;
-        Some(Box::new(
-            Some(Lsp::new(None, self.span.0.offset(), self.span.0.len())).into_iter(),
-        ))
-    }
-}
-
-#[derive(Clone, Debug, Diagnostic, thiserror::Error)]
-pub enum ErrorKind {
-    #[error("expected {0}")]
-    #[diagnostic(code(yanais::parser::expected))]
-    Expected(ErrorCtx),
-
-    #[error("end of file encountered inside {0}")]
-    #[diagnostic(code(yanais::parser::unexpected_eof))]
-    UnexpectedEof(ErrorCtx),
-
-    #[error("unhandled character '{0}'")]
-    #[diagnostic(code(yanais::lexer::unhandled_char))]
-    UnhandledChar(char),
-
-    #[error(transparent)]
-    #[diagnostic(code(yanais::parser::invalid_int))]
-    InvalidInt(#[from] core::num::ParseIntError),
-
-    #[error("comment nesting overflowed")]
-    #[diagnostic(code(yanais::lexer::comment_nest_overflow))]
-    CommentNestOverflow,
-
-    #[error("duplicated record field identifier {0:?}")]
-    #[diagnostic(code(yanais::parser::record_dup_ident))]
-    RecordDupIdent(Arc<str>),
-
-    #[error("unknown identifer {0:?}")]
-    #[diagnostic(code(yanais::parser::unknown_ident))]
-    UnknownIdent(Arc<str>),
-}
-
-#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
-pub enum ErrorCtx {
-    Comment,
-    Literal,
-    Pattern,
-    Record,
-    Select,
-    String,
-    Ident,
-}
-
-impl fmt::Display for ErrorCtx {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.write_str(match self {
-            ErrorCtx::Comment => "comment",
-            ErrorCtx::Literal => "literal",
-            ErrorCtx::Pattern => "pattern",
-            ErrorCtx::Record => "record",
-            ErrorCtx::Select => "selection",
-            ErrorCtx::String => "string",
-            ErrorCtx::Ident => "identifier",
-        })
-    }
-}
-
 #[derive(Clone)]
 pub struct Env<'a, Kw> {
     pub lxr: lex::Lexer<'a, Kw>,
@@ -255,8 +123,8 @@ impl<'a, Kw> Env<'a, Kw> {
     }
 }
 
-pub trait Keywords: Sized + core::cmp::PartialEq + core::str::FromStr {}
-impl<T: Sized + core::cmp::PartialEq + core::str::FromStr> Keywords for T {}
+pub trait Keywords: Sized + cmp::PartialEq + core::str::FromStr {}
+impl<T: Sized + cmp::PartialEq + core::str::FromStr> Keywords for T {}
 
 pub trait Parse<Kw: Keywords>: Sized {
     fn parse(env: &mut Env<'_, Kw>) -> Result<Self>;
@@ -284,3 +152,58 @@ impl<Kw: Keywords, T: MaybeParse<Kw>> Parse<Kw> for T {
         })
     }
 }
+
+#[derive(Clone, Debug, PartialEq)]
+pub struct TaggedIdent {
+    pub span: EvEqSourceSpan,
+    pub name: Arc<str>,
+}
+
+#[derive(Clone, Debug)]
+pub struct SelIdent {
+    pub span: EvEqSourceSpan,
+    // de-Bruijn index
+    pub dbidx: usize,
+}
+
+impl ParseDefaultCtx for TaggedIdent {
+    const DFL_CTX: ErrorCtx = ErrorCtx::Ident;
+}
+
+impl<Kw: Keywords> MaybeParse<Kw> for TaggedIdent {
+    fn maybe_parse(env: &mut Env<'_, Kw>) -> Result<Option<Self>> {
+        let lxrbak = env.lxr.clone();
+        let lex::Token { span, kind } = none_up!(env.lxr.next())?;
+
+        Ok(if let lex::TokenKind::Ident(name) = kind {
+            Some(TaggedIdent { span, name })
+        } else {
+            env.lxr = lxrbak;
+            None
+        })
+    }
+}
+
+impl ParseDefaultCtx for SelIdent {
+    const DFL_CTX: ErrorCtx = ErrorCtx::Ident;
+}
+
+impl<Kw: Keywords> MaybeParse<Kw> for SelIdent {
+    fn maybe_parse(env: &mut Env<'_, Kw>) -> Result<Option<Self>> {
+        let lxrbak = env.lxr.clone();
+        let lex::Token { span, kind } = none_up!(env.lxr.next())?;
+
+        if let lex::TokenKind::Ident(name) = kind {
+            match env.lookup(&name) {
+                Some(dbidx) => Ok(Some(SelIdent { span, dbidx })),
+                None => Err(Error {
+                    span,
+                    kind: ErrorKind::UnknownIdent(name),
+                }),
+            }
+        } else {
+            env.lxr = lxrbak;
+            Ok(None)
+        }
+    }
+}