flgrubm/linlog - Change ULA55AHINIZ4OTSTAGONIR7OFUBC3EJANWX3XSXPPCU5CNSECQCQC

Add sequent parser

Created by flgrubm on January 3, 2026

ULA55AHINIZ4OTSTAGONIR7OFUBC3EJANWX3XSXPPCU5CNSECQCQC

Dependencies

In channels

main

Change contents

File deletion: terms.rs

BF:BFD[3.8576] → [2.0:32]

BF:BFD[2.32] → [2.33:33]

B:BD[2.33] → [2.34:1699]

// linlog © Fabian Lukas Grubmüller 2026
// Licensed under the EUPL
use std::collections::HashMap;
/// Symbols for the `Term`s in polish notation
#[derive(Debug)]
pub enum Symbol {
    Var(usize),
    Zero,
    One,
    Bot,
    Top,
    Dual,
    Tensor,
    Plus,
    With,
    Par,
    Bang,
    Quest,
    Lollipop,
}
pub struct Term<'a> {
    term: Box<[Symbol]>,
    labels: Box<[&'a str]>,
}
impl<'a> Term<'a> {
    pub fn parse(t: &'a str) -> Result<Self, ()> {
        let mut label_map: HashMap<&'a str, usize> = HashMap::with_capacity(t.len());
        let mut term: Vec<Symbol> = Vec::with_capacity(t.len());
        let mut labels: Vec<&'a str> = Vec::with_capacity(t.len());
        todo!();
        Ok(Self {
            term: term.into_boxed_slice(),
            labels: labels.into_boxed_slice(),
        })
    }
    pub fn try_new(term: Box<[Symbol]>, labels: Box<[&'a str]>) -> Result<Self, ()> {
        if Self::verify(&term) {
            Ok(Self { term, labels })
        } else {
            Err(())
        }
    }
    pub fn verify(t: &[Symbol]) -> bool {
        use Symbol::*;
        let mut leaves_left = 1usize;
        for sym in t.iter() {
            match sym {
                Var(_) | Zero | One | Bot | Top => {
                    if leaves_left == 0 {
                        return false;
                    } else {
                        leaves_left -= 1;
                    }
                }
                Tensor | Plus | With | Par | Lollipop => {
                    leaves_left += 1;
                }
                Dual | Bang | Quest => {}
            }
        }
        leaves_left == 0
    }
}

File addition: sequents (d--x------)
[3.8576]

File addition: raw.rs (----------)

[0.20]

// linlog © Fabian Lukas Grubmüller 2026
// Licensed under the EUPL

File addition: parsing.rs (----------)

[0.20]

// linlog © Fabian Lukas Grubmüller 2026
// Licensed under the EUPL
use chumsky::pratt::*;
use chumsky::prelude::*;
enum Term<'a> {
    Var(&'a str),
    Zero,
    One,
    Bot,
    Top,
    Neg(Box<Term<'a>>),
    Bang(Box<Term<'a>>),
    Quest(Box<Term<'a>>),
    Tensor(Box<Term<'a>>, Box<Term<'a>>),
    Par(Box<Term<'a>>, Box<Term<'a>>),
    With(Box<Term<'a>>, Box<Term<'a>>),
    Plus(Box<Term<'a>>, Box<Term<'a>>),
    Lollipop(Box<Term<'a>>, Box<Term<'a>>),
}
struct Sequent<'a> {
    left: Vec<Term<'a>>,
    right: Vec<Term<'a>>,
}
fn constant_parser<'a>() -> impl Parser<'a, &'a str, Term<'a>, extra::Err<Simple<'a, char>>> + Clone
{
    choice((
        text::keyword("0").map(|_| Term::Zero),
        text::keyword("1").map(|_| Term::One),
        text::keyword("bot").map(|_| Term::Bot),
        text::keyword("⊥").map(|_| Term::Bot),
        text::keyword("top").map(|_| Term::Top),
        text::keyword("⊤").map(|_| Term::Top),
    ))
}
fn variable_parser<'a>() -> impl Parser<'a, &'a str, Term<'a>, extra::Err<Simple<'a, char>>> + Clone
{
    text::ident().map(Term::Var)
}
fn term_parser<'a>() -> impl Parser<'a, &'a str, Term<'a>, extra::Err<Simple<'a, char>>> + Clone {
    recursive(|term| {
        let atom = choice((
            constant_parser(),
            variable_parser(),
            term.delimited_by(just('('), just(')')),
        ))
        .padded();
        // binding strength:
        // postfix '^' > prefix '~', '!', '?' > Tensor > Par > With > Sum > Lollipop
        atom.pratt((
            // Unaties
            postfix(7, just('^'), |lhs, _, _| Term::Neg(Box::new(lhs))),
            prefix(6, just('~'), |_, rhs, _| Term::Neg(Box::new(rhs))),
            prefix(6, just('!'), |_, rhs, _| Term::Bang(Box::new(rhs))),
            prefix(6, just('?'), |_, rhs, _| Term::Quest(Box::new(rhs))),
            // Tensor
            infix(left(5), just('*'), |l, _, r, _| {
                Term::Tensor(Box::new(l), Box::new(r))
            }),
            infix(left(5), just('⊗'), |l, _, r, _| {
                Term::Tensor(Box::new(l), Box::new(r))
            }),
            // Par
            infix(left(4), text::keyword("par"), |l, _, r, _| {
                Term::Par(Box::new(l), Box::new(r))
            }),
            infix(left(4), just('|'), |l, _, r, _| {
                Term::Par(Box::new(l), Box::new(r))
            }),
            infix(left(4), just('⅋'), |l, _, r, _| {
                Term::Par(Box::new(l), Box::new(r))
            }),
            // With
            infix(left(3), just('&'), |l, _, r, _| {
                Term::With(Box::new(l), Box::new(r))
            }),
            // Plus
            infix(left(2), just('+'), |l, _, r, _| {
                Term::Plus(Box::new(l), Box::new(r))
            }),
            infix(left(2), just('⊕'), |l, _, r, _| {
                Term::Plus(Box::new(l), Box::new(r))
            }),
            // Lollipop
            infix(right(1), just("-o"), |l, _, r, _| {
                Term::Lollipop(Box::new(l), Box::new(r))
            }),
            infix(right(0), just('⊸'), |l, _, r, _| {
                Term::Lollipop(Box::new(l), Box::new(r))
            }),
        ))
    })
}
fn sequent_parser<'a>() -> impl Parser<'a, &'a str, Sequent<'a>, extra::Err<Simple<'a, char>>> {
    let terms_list = term_parser()
        .clone()
        .separated_by(just(',').padded())
        .collect::<Vec<Term<'a>>>();
    let tack = choice((just("|-"), just("⊢"))).padded();
    terms_list
        .clone() // Parse LHS
        .then(tack) // Ignore the tack (but consume it)
        .then(terms_list) // Parse RHS
        .map(|((left, _), right)| Sequent { left, right })
        .then_ignore(end()) // Ensure the parser consumes the entire input string
}

File addition: mod.rs (----------)

[0.20]

// linlog © Fabian Lukas Grubmüller 2026
// Licensed under the EUPL
mod parsing;
mod raw;

Replacement in core/src/lib.rs at line 4 [3.8609]
B:BD[2.1701] → [2.1701:1716]
```
pub mod terms;
```
[2.1701]
[3.8680]
```
pub mod sequents;
```

Insertion in core/Cargo.toml at line 7 [3.8927]

[3.9005]

[2.1717]

chumsky = { version = "0.12.0", features = ["memoization", "pratt"] }

Insertion in Cargo.lock at line 6 [3.23598]

[3.23715]

[2.1759]

name = "aho-corasick"
version = "1.1.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301"
dependencies = [
 "memchr",
]
[[package]]
name = "allocator-api2"
version = "0.2.21"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923"
[[package]]

Insertion in Cargo.lock at line 25 [3.23598]

[2.1938]


[[package]]
name = "ar_archive_writer"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f0c269894b6fe5e9d7ada0cf69b5bf847ff35bc25fc271f08e1d080fce80339a"
dependencies = [
 "object",
]
[[package]]
name = "cc"
version = "1.2.51"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7a0aeaff4ff1a90589618835a598e545176939b97874f7abc7851caa0618f203"
dependencies = [
 "find-msvc-tools",
 "shlex",
]
[[package]]
name = "cfg-if"
version = "1.0.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
[[package]]
name = "chumsky"
version = "0.12.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4ba4a05c9ce83b07de31b31c874e87c069881ac4355db9e752e3a55c11ec75a6"
dependencies = [
 "hashbrown",
 "regex-automata",
 "serde",
 "stacker",
 "unicode-ident",
 "unicode-segmentation",
]
[[package]]
name = "equivalent"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
[[package]]
name = "find-msvc-tools"
version = "0.1.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "645cbb3a84e60b7531617d5ae4e57f7e27308f6445f5abf653209ea76dec8dff"

Insertion in Cargo.lock at line 78 [3.23598]

[2.1951]

[3.23715]

name = "foldhash"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
[[package]]
name = "hashbrown"
version = "0.15.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
dependencies = [
 "allocator-api2",
 "equivalent",
 "foldhash",
]
[[package]]
name = "libc"
version = "0.2.178"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "37c93d8daa9d8a012fd8ab92f088405fb202ea0b6ab73ee2482ae66af4f42091"
[[package]]

Insertion in Cargo.lock at line 104 [3.23598]
[2.1969]
[2.1969]
```
 "chumsky",
```

Insertion in Cargo.lock at line 115 [3.23598]

[3.23830]

[2.1998]


[[package]]
name = "memchr"
version = "2.7.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f52b00d39961fc5b2736ea853c9cc86238e165017a493d1d5c8eac6bdc4cc273"

Insertion in Cargo.lock at line 123 [3.23598]

[2.2011]

name = "object"
version = "0.32.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a6a622008b6e321afc04970976f62ee297fdbaa6f95318ca343e3eebb9648441"
dependencies = [
 "memchr",
]
[[package]]

Insertion in Cargo.lock at line 138 [3.23598]

[2.2230]

]
[[package]]
name = "psm"
version = "0.1.28"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d11f2fedc3b7dafdc2851bc52f277377c5473d378859be234bc7ebb593144d01"
dependencies = [
 "ar_archive_writer",
 "cc",

Insertion in Cargo.lock at line 155 [3.23598]

[2.2422]

dependencies = [
 "proc-macro2",
]
[[package]]
name = "regex-automata"
version = "0.3.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "59b23e92ee4318893fa3fe3e6fb365258efbfe6ac6ab30f090cdcbb7aa37efa9"
dependencies = [
 "aho-corasick",
 "memchr",
 "regex-syntax",
]
[[package]]
name = "regex-syntax"
version = "0.7.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da"
[[package]]
name = "serde"
version = "1.0.228"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"

Insertion in Cargo.lock at line 182 [3.23598]

[2.2439]

 "serde_core",
 "serde_derive",
]
[[package]]
name = "serde_core"
version = "1.0.228"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
dependencies = [
 "serde_derive",
]
[[package]]
name = "serde_derive"
version = "1.0.228"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
dependencies = [

Insertion in Cargo.lock at line 202 [3.23598]
[2.2455]
[2.2455]
```
 "quote",
 "syn",
```

Insertion in Cargo.lock at line 207 [3.23598]

[2.2470]

name = "shlex"
version = "1.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
[[package]]
name = "stacker"
version = "0.1.22"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e1f8b29fb42aafcea4edeeb6b2f2d7ecd0d969c48b4cf0d2e64aafc471dd6e59"
dependencies = [
 "cc",
 "cfg-if",
 "libc",
 "psm",
 "windows-sys",
]
[[package]]

Insertion in Cargo.lock at line 261 [3.23598]

[2.3391]


[[package]]
name = "unicode-segmentation"
version = "1.12.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f6ccf251212114b54433ec949fd6a7841275f9ada20dddd2f29e9ceea4501493"
[[package]]
name = "windows-sys"
version = "0.59.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
dependencies = [
 "windows-targets",
]
[[package]]
name = "windows-targets"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
dependencies = [
 "windows_aarch64_gnullvm",
 "windows_aarch64_msvc",
 "windows_i686_gnu",
 "windows_i686_gnullvm",
 "windows_i686_msvc",
 "windows_x86_64_gnu",
 "windows_x86_64_gnullvm",
 "windows_x86_64_msvc",
]
[[package]]
name = "windows_aarch64_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
[[package]]
name = "windows_aarch64_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
[[package]]
name = "windows_i686_gnu"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
[[package]]
name = "windows_i686_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
[[package]]
name = "windows_i686_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
[[package]]
name = "windows_x86_64_gnu"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
[[package]]
name = "windows_x86_64_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
[[package]]
name = "windows_x86_64_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"

Add sequent parser

Dependencies

In channels

Change contents

File deletion: terms.rs

File addition: sequents (d--x------)

File addition: raw.rs (----------)

File addition: parsing.rs (----------)

File addition: mod.rs (----------)

Replacement in core/src/lib.rs at line 4 [3.8609]

Insertion in core/Cargo.toml at line 7 [3.8927]

Insertion in Cargo.lock at line 6 [3.23598]

Insertion in Cargo.lock at line 25 [3.23598]

Insertion in Cargo.lock at line 78 [3.23598]

Insertion in Cargo.lock at line 104 [3.23598]

Insertion in Cargo.lock at line 115 [3.23598]

Insertion in Cargo.lock at line 123 [3.23598]

Insertion in Cargo.lock at line 138 [3.23598]

Insertion in Cargo.lock at line 155 [3.23598]

Insertion in Cargo.lock at line 182 [3.23598]

Insertion in Cargo.lock at line 202 [3.23598]

Insertion in Cargo.lock at line 207 [3.23598]

Insertion in Cargo.lock at line 261 [3.23598]