n.bend source

n.bend on the hub · documented module

import Base# N, by Pedro Antonio Villanueva Juarez · https://github.com/PedroAVJ/n## N: a static type checker for `.n` source. A `.n` file is source code in any code (English,# Spanish, a diagram); N elaborates it into Bend terms, typed against V's modules, and reports# type errors. Where a span has more than one reading, that is a type error the author resolves# by choosing the reading they meant; where context settles it, N may fix it itself.# U is N's feelings stage: it runs after N and owns only the rules about feelings.# ---- source ----# A span of a `.n` file, by character offsets: [start, end).type Span is Data:  Span{start: Nat, end: Nat}# One reading of a span: the Bend term it elaborates to, as text.type Reading is Data:  Reading{span: Span, term: String}# ---- stages ----# Each question has exactly one owner: N checks the language, then U checks feelings.type Stage is Data:  N{}  U{}# ---- type errors ----# Ambiguous: the span has several readings and nothing settles which one is meant.# Inconsistent: two readings cannot both hold.# Unconfirmed: the author has not confirmed that the reading is what they meant.type Diagnostic is Data:  Ambiguous{stage: Stage, span: Span, readings: List<&2, Reading>}  Inconsistent{stage: Stage, a: Reading, b: Reading, why: String}  Unconfirmed{stage: Stage, reading: Reading}