Skip to main content
Deno 2 is finally here 🎉️
Learn more
Module

x/lambdapi/src/deps.ts

Deno TypeScript implementation of LambdaPi interpreter from "A Tutorial Implementation of a Dependently Typed Lambda Calculus" https://www.andres-loeh.de/LambdaPi/
Latest
import * as lambdapi from "https://deno.land/x/lambdapi@v1.0.1/src/deps.ts";

Applicative Parser

Variables

float parses a floating point number.

integer parses an integer number.

sexpr parses an s-expression which can consist of an atom, integer, float, or string, and lists of these types enclosed in parentheses. See SExp and Atom for result structure.

Functions

apply applies a higher-order parser to another parser.

between applies parser ps then parser p then parser pe, but only returns the result of parser p.

Cartesian runs the first parser, and then if it succeeds, runs the second parser. The first and second parsers can be different types.

choice tries each parser in turn, returning the first success, or failing if none succeed.

Either runs the first parser, and then if it fails, runs the second parser. The first and second parsers must be the same type.

Empty parser matches end-of-file or fails.

Fail parser consumes no input and always fails, with error message fail.

first applies both parsers, but only returns the result of the first.

Fix finds the fixed-point of the f parser argument. Used to implement dynamic recursion.

Forget runs the forget parser and returns its result without consuming any input. This is used to implement lookahead.

LMap applies map to the attributes passed from the parent node in the parser tree structure.

many applies parser p zero or more times, returning an immutable list, this cannot fail.

many1 applies parser p one or more times, returning an immutable list, this will fail if it does not succeed at least once.

OneOf parser consumes one character if it is in the oneOf string argument or fails.

opt applies parser p and succeeds with default value x if it fails

optSpaces accepts zero or more spaces, always succeeds.

Read strings line-by-line from a Reader.

Return is constant parser that evalueates to result and cannot fail.

RMap applies the map function to the result of running the parser argument.

second applies both parsers, but only returns the result of the second.

seq applies each parser in sequence and returns a tuple of their results if they all succeed, or fails if any fail.

seqMap accepts a map function as the first argument, and then the remaining arguments are parsers. If all the parsers succeed, the map function is called with the result of each parser as an argument to the map function in the same order as the parsers.

show pretty prints the parser argument.

spaces succeeds if there are one or more spaces, otherwise fails

string matches string s or fails.

symbols extracts all the valid symbold from the parser argument.

string matches string token and consumes any trailing spaces, or fails.

Try backtracks the parser if it fails, so another option can be tried.

Type Aliases

Type of Atom for example s-expression parser.

Parse is the type returned by the parse function, which takes an input string cs, a position pos, and the inherited attributes attr passed to the root of the parser, and returns the input string, the updated position, and the result of the parser.

Parser<A> is the type of a parser combinator that returns a value with generic type A.

Type of SExp for example s-expression parser.