[−][src]Enum minitt::ast::Expression
Exp
in Mini-TT.
Expression language for Mini-TT.
$M,\ N,\ A,\ B ::=$
Variants
Unit
$0$
One
$\textbf{1}$
Type(Level)
$\textsf{U}$,
Type
. Extended with levels.
Void
Empty file
Var(String)
$x$,
bla
Sum(Branch)
$\textsf{Sum} \ S$,
Sum { Bla x }
Split(Branch)
$\textsf{fun} \ S$,
split { Bla x => y }
Merge(Box<Self>, Box<Self>)
This is an extension to Mini-TT, A ++ B
.
Pi(Typed, Box<Self>)
$\Pi p : A. B$ or $A \rightarrow B$,
\Pi a: b. c
or A -> B
Sigma(Typed, Box<Self>)
$\Sigma p : A. B$ or $A \times B$,
\Sigma a: b. c
or A * B
Lambda(Pattern, Option<AnonymousValue>, Box<Self>)
$\lambda p. M$,
\lambda a. c
, the optional value is the type of the argument.
This cannot be specified during parsing because it's used for generated intermediate values
during type-checking.
First(Box<Self>)
$M.1$,
bla.1
Second(Box<Self>)
$M.2$,
bla.2
Application(Box<Self>, Box<Self>)
$M \ N$,
f a
Pair(Box<Self>, Box<Self>)
$M, N$,
a, b
Constructor(String, Box<Self>)
$\textsf{c}\ M$, Cons a
Constant(Pattern, Box<Self>, Box<Self>)
const a = b
, this is an extension: a declaration whose type-signature is inferred.
This is very similar to a Declaration
.
Declaration(Box<Declaration>, Box<Self>)
$D; M$,
let bla
or rec bla
Methods
impl Expression
[src]
pub fn eval_to_sum(self, context: Telescope) -> Option<Vec<String>>
[src]
This is not present in Mini-TT.
Return true
if self
is a Sum
or Merge
.
This is quite expensive! Can we optimize it a little bit?
pub fn eval(self, context: Telescope) -> Value
[src]
$$
\begin{alignedat}{2}
& ⟦ \lambda p.M ⟧ \rho &&= \lang \lambda p.M,\rho \rang \\
& ⟦ x ⟧ \rho &&= \rho(x) \\
& ⟦ M \ N ⟧ \rho &&= \textsf{app} (⟦ M ⟧ \rho, ⟦ N ⟧ \rho) \\
& ⟦ \Pi \ p:A.B ⟧ \rho &&= \Pi (⟦ A ⟧ \rho) \lang \lambda p.B,\rho \rang \\
& ⟦ \textsf{U} ⟧ \rho &&= \textsf{U} \\
& ⟦ D; M ⟧ \rho &&= ⟦ M ⟧ (\rho(x); D) \\
& && \\
& ⟦ M,N ⟧ \rho &&= (⟦ M ⟧ \rho, ⟦ N ⟧ \rho) \\
& ⟦ 0 ⟧ \rho &&= 0 \\
& ⟦ M.1 ⟧ \rho &&= (⟦ M\rho ⟧).1 \\
& ⟦ M.2 ⟧ \rho &&= (⟦ M\rho ⟧).2 \\
& ⟦ \Sigma \ p:A.B ⟧ \rho &&= \Sigma (⟦ A ⟧ \rho) \lang \lambda p.B,\rho \rang \\
& ⟦ \textbf{1} ⟧ \rho &&= \textbf{1} \\
& && \\
& ⟦ c \ M ⟧ \rho &&= c(⟦ M ⟧ \rho) \\
& ⟦ \textsf{fun} \ S ⟧ \rho &&= \textsf{fun} \lang S,\rho \rang \\
& ⟦ \textsf{Sum} \ S ⟧ \rho &&= \textsf{Sum} \lang S,\rho \rang
\end{alignedat}
$$
eval
in Mini-TT.
Evaluate an Expression
to a Value
under a Telescope
,
panic if not well-typed.
Trait Implementations
impl Eq for Expression
[src]
fn assert_receiver_is_total_eq(&self)
[src]
impl Clone for Expression
[src]
fn clone(&self) -> Expression
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
impl PartialEq<Expression> for Expression
[src]
fn eq(&self, other: &Expression) -> bool
[src]
fn ne(&self, other: &Expression) -> bool
[src]
impl Debug for Expression
[src]
impl Display for Expression
[src]
Auto Trait Implementations
impl Unpin for Expression
impl !Sync for Expression
impl !Send for Expression
impl !UnwindSafe for Expression
impl !RefUnwindSafe for Expression
Blanket Implementations
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,