Global

Members

(constant) DIALECTS

The four host-language dialect tag prefixes plus the shared dialect. Exported so that external tooling can refer to them symbolically.

Source:

(constant) SUPPORTED_LANGUAGES :ReadonlyArray.<('rust'|'js'|'javascript'|'lean'|'rocq')>

The four host languages plus their aliases.

Type:
  • ReadonlyArray.<('rust'|'js'|'javascript'|'lean'|'rocq')>
Source:

Methods

check()

Check that a kernel term has the expected type.

Source:

checkProgram()

Public entry point: parse both .lino sources, pair queries with derivations 1:1, and verify each pair structurally. Returns { ok: [{rule, expr}, ...], errors: [{path, message}, ...] }.

Source:

cloneCst(node) → {CstNode}

Compute and return a structural copy of a CST node. Used by translators that need to mutate without altering the input.

Parameters:
Name Type Description
node CstNode
Source:
Returns:
Type
CstNode

computeFormSpans()

Compute 1-based source spans for every top-level LiNo form in text.

Source:

cstToLino(node) → {string}

Serialise a CST node into a .lino S-expression suitable for embedding in .lino files or for round-trip testing. The serialisation is the literal shape documented in docs/case-studies/issue-138/cst-model.md:

(lino-cst.list <tag> <child> <child> ...) (lino-cst.token "<text>") (lino-cst.trivia "<text>")

String contents are escaped using JSON rules so that the result is a valid LiNo expression. parseCstLino is the exact inverse.

Parameters:
Name Type Description
node CstNode

tree to serialise.
Source:
Returns:
Type
string

evaluate(code, optionsopt) → {object}

Evaluate LiNo source and return query results plus structured diagnostics.

Parameters:
Name Type Attributes Description
code string

LiNo source text.
options object <optional>

Evaluation options.

Properties
Name Type Attributes Default Description
file string <optional>

Source file path used in diagnostics.
env Env | object <optional>

Existing environment or environment options.
trace boolean <optional>
 false

Include deterministic trace events.
withProofs boolean <optional>
 false

Include proof witnesses for queries.
Source:
Returns:

Results, diagnostics, and optional trace/proof arrays.

Type
object

evaluateFile()

Read and evaluate a LiNo file, resolving imports relative to that file.

Source:

exportIsabelle()

Export the supported typed LiNo fragment to Isabelle/HOL source text.

Source:

extractLiterateLino()

Extract LiNo code from fenced lino blocks in a literate .lino.md file.

Non-LiNo prose and other code fences become blank lines so diagnostics keep the original Markdown line numbers.

Source:

extractProgram()

Extract selected LiNo definitions into JavaScript or Rust source code.

Source:

isConvertible(left, right, ctxopt, optionsopt) → {boolean}

Check definitional equality by normalizing two terms in the supplied context.

Parameters:
Name Type Attributes Description
left *

Left AST term.
right *

Right AST term.
ctx object <optional>

Type-checking context.
options object <optional>

Conversion options.
Source:
Returns:

True when the terms are convertible.

Type
boolean

leaves(node) → {Iterable.<(CstTokenNode|CstTriviaNode)>}

Iterate every leaf (token or trivia) of a CST in document order.

Parameters:
Name Type Description
node CstNode

tree to walk.
Source:
Returns:
Type
Iterable.<(CstTokenNode|CstTriviaNode)>

linoToCst(src) → {CstNode}

Parse the .lino S-expression produced by cstToLino() back into a CstNode tree. Inverse of cstToLino.

Parameters:
Name Type Description
src string

.lino S-expression.
Source:
Returns:
Type
CstNode

list(tag, children, optsopt) → {CstListNode}

Construct a list CST node.

Parameters:
Name Type Attributes Description
tag string | null

dialect-specific symbol, e.g. lino-cst.rust.fn.
children Array.<CstNode>

child nodes in document order.
opts CstListOptions <optional>

optional open/close delimiter strings to emit around the children.
Source:
Returns:
Type
CstListNode

nf()

Reduce a term to normal form.

Source:

parseJs(src) → {CstNode}

Parse JavaScript source into a lino-cst.js.* CST.

Parameters:
Name Type Description
src string

JS source.
Source:
Returns:
Type
CstNode

parseLean(src) → {CstNode}

Parse Lean 4 source into a lino-cst.lean.* CST.

Parameters:
Name Type Description
src string

Lean source.
Source:
Returns:
Type
CstNode

parseLino()

Parse LiNo source text with the official links-notation parser.

Source:

parseRocq(src) → {CstNode}

Parse Rocq source into a lino-cst.rocq.* CST.

Parameters:
Name Type Description
src string
Source:
Returns:
Type
CstNode

parseRust(src) → {CstNode}

Parse Rust source into a lino-cst.rust.* CST.

The returned tree is a single source_file list. Every byte of src is preserved verbatim in the resulting tree; printRust(parseRust(src)) === src for any well-tokenised input.

Parameters:
Name Type Description
src string

Rust source.
Source:
Returns:

CST root.

Type
CstNode

parseToCst(src, lang) → {CstNode}

Parse host-language source into a .lino CST.

Parameters:
Name Type Description
src string

host-language source.
lang 'rust' | 'js' | 'javascript' | 'lean' | 'rocq'
Source:
Returns:
Type
CstNode

printCst(node) → {string}

Print a CST node back to its original byte-for-byte source representation.

The walk is the five-line algorithm from the model document:

  • for token and trivia nodes, emit node.text.
  • for list nodes, emit open, then children in order, then close.
Parameters:
Name Type Description
node CstNode

tree to print.
Source:
Returns:

reconstructed source.

Type
string

printFromCst(node, lang) → {string}

Print a CST node back to host-language source.

Parameters:
Name Type Description
node CstNode

CST tree.
lang 'rust' | 'js' | 'javascript' | 'lean' | 'rocq'
Source:
Returns:
Type
string

printJs(node) → {string}

Print a JS CST back to source.

Parameters:
Name Type Description
node CstNode
Source:
Returns:
Type
string

printLean(node) → {string}

Print a Lean CST back to source.

Parameters:
Name Type Description
node CstNode
Source:
Returns:
Type
string

printRocq(node) → {string}

Print a Rocq CST back to source.

Parameters:
Name Type Description
node CstNode
Source:
Returns:
Type
string

printRust(node) → {string}

Print a Rust CST back to source. Inverse of parseRust.

Parameters:
Name Type Description
node CstNode
Source:
Returns:
Type
string

roundTrip(src, lang) → {Object}

Verify that printFromCst(parseToCst(src, lang), lang) === src.

Parameters:
Name Type Description
src string

host-language source.
lang 'rust' | 'js' | 'javascript' | 'lean' | 'rocq'
Source:
Returns:
Type
Object

run()

Compatibility wrapper that evaluates LiNo text and returns only query values.

Source:

synth()

Synthesize the type of a kernel term.

Source:

token(text, tagopt) → {CstTokenNode}

Construct a token CST leaf.

Parameters:
Name Type Attributes Description
text string

original source bytes for the lexeme.
tag string | null <optional>

optional dialect-specific symbol.
Source:
Returns:
Type
CstTokenNode

trivia(text, tagopt) → {CstTriviaNode}

Construct a trivia CST leaf (whitespace or comment).

Parameters:
Name Type Attributes Description
text string

original source bytes.
tag string | null <optional>

optional categorisation, e.g. comment.line.
Source:
Returns:
Type
CstTriviaNode

whnf()

Reduce a term to weak-head normal form without descending into arguments.

Source:

Type Definitions

CstListNode

Type:
  • Object
Properties:
Name Type Description
kind 'list'
tag string | null
open string | null
close string | null
children Array.<CstNode>
Source:

CstListOptions

Type:
  • Object
Properties:
Name Type Attributes Description
open string | null <optional>
close string | null <optional>
Source:

CstNode

Type:
Source:

CstTokenNode

Type:
  • Object
Properties:
Name Type Description
kind 'token'
tag string | null
text string
Source:

CstTriviaNode

Type:
  • Object
Properties:
Name Type Description
kind 'trivia'
tag string | null
text string
Source: