This page requires javascript to work

[][src]Module minitt::ast

Syntax: term, expression, context.

Methods are defined in reduce/read_back modules but their documents are here.

No dependency.

Structs

AnonymousValue

Just a wrapper for a value but does not do Eq comparison. This is an implementation detail and should not be noticed much when reading the source code.

Declaration

Decl in Mini-TT. $D ::= p:A=M\ |\ \textsf{rec}\ p:A=M$

GenericCase

Generic definition for three kinds of case trees

Typed

$p:A$, Pattern with type explicitly specified. This is just a helper struct.

Enums

Closure

Clos in Mini-TT.

Expression

Exp in Mini-TT. Expression language for Mini-TT.

GenericNeutral

Generic definition for two kinds of neutral terms.

GenericTelescope

Generic definition for two kinds of telescopes.
Value can be specialized with Value or NormalExpression.

Pattern

Patt in Mini-TT.

Value

Val in Mini-TT, value term.
Terms are either of canonical form or neutral form.

Functions

branch_to_righted

This function name is mysterious, but I failed to find a better name. It's for converting a Branch into a CaseTree by inserting the context to every Cases.

nil_rc

Because we can't impl a Default for Rc. $()$

up_dec_rc

Just for simplifying constructing an Rc. $\rho, p=D$

up_var_rc

Just for simplifying constructing an Rc. $\rho, p=v$

Type Definitions

Branch

$S ::= ()\ |\ (\textsf{c}\ M, S)$, Pattern matching branch.

Case

One single case in case trees.

CaseTree

$\lang S,\rho \rang$, SClos in Mini-TT.
Case tree.

GenericBranch

$S(M) ::= ()\ |\ (\textsf{c}\ M, S)$

Level
Neutral

$k ::= k(v)$. Neut in Mini-TT, neutral value.

Telescope

$\rho ::= \rho(v)$ Rho in Mini-TT, dependent context.

TelescopeRc