use voile_util::level::{Level, LevelType};
use voile_util::loc::{Ident, Labelled, Loc};
use voile_util::tags::{Plicit, VarRec};
use voile_util::vec1::Vec1;
pub type LabExpr = Labelled<Expr>;
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Param {
pub plicit: Plicit,
pub names: Vec<Ident>,
pub ty: Expr,
}
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum Expr {
Var(Ident),
Cons(Ident),
Meta(Ident),
Lift(Loc, LevelType, Box<Self>),
Proj(Box<Self>, Vec1<Ident>),
Type(Loc, Level),
App(Box<Vec1<Self>>),
Pipe(Box<Vec1<Self>>),
Tup(Box<Vec1<Self>>),
RowPoly(Loc, VarRec, Vec<LabExpr>, Option<Box<Self>>),
Rec(Loc, Vec<LabExpr>, Option<Box<Self>>),
RowKind(Loc, VarRec, Vec<Ident>),
Pi(Vec<Param>, Box<Self>),
Sig(Vec<Param>, Box<Self>),
Cases(Ident, Ident, Box<Self>, Box<Self>),
Whatever(Loc),
Lam(Loc, Vec<Ident>, Box<Self>),
}
impl Expr {
pub fn pi(params: Vec<Param>, expr: Self) -> Self {
Expr::Pi(params, Box::new(expr))
}
pub fn lam(info: Loc, params: Vec<Ident>, expr: Self) -> Self {
Expr::Lam(info, params, Box::new(expr))
}
pub fn app(applied: Self, arguments: Vec<Self>) -> Self {
Expr::App(Box::new(Vec1::new(applied, arguments)))
}
pub fn lift(info: Loc, count: LevelType, target: Self) -> Self {
Expr::Lift(info, count, Box::new(target))
}
pub fn pipe(first: Self, functions: Vec<Self>) -> Self {
Expr::Pipe(Box::new(Vec1::new(first, functions)))
}
pub fn row_polymorphic_type(
info: Loc,
labels: Vec<LabExpr>,
kind: VarRec,
rest: Option<Self>,
) -> Self {
Expr::RowPoly(info, kind, labels, rest.map(Box::new))
}
pub fn record(info: Loc, fields: Vec<LabExpr>, rest: Option<Self>) -> Self {
Expr::Rec(info, fields, rest.map(Box::new))
}
pub fn sum(info: Loc, labels: Vec<LabExpr>, rest: Option<Self>) -> Self {
Self::row_polymorphic_type(info, labels, VarRec::Variant, rest)
}
pub fn rec(info: Loc, labels: Vec<LabExpr>, rest: Option<Self>) -> Self {
Self::row_polymorphic_type(info, labels, VarRec::Record, rest)
}
pub fn tup(first: Self, rest: Vec<Self>) -> Self {
Expr::Tup(Box::new(Vec1::new(first, rest)))
}
pub fn sig(params: Vec<Param>, expr: Self) -> Self {
Expr::Sig(params, Box::new(expr))
}
pub fn proj(expr: Self, projections: Vec1<Ident>) -> Self {
Expr::Proj(Box::new(expr), projections)
}
pub fn cases(label: Ident, binding: Ident, body: Self, or: Self) -> Self {
Expr::Cases(label, binding, Box::new(body), Box::new(or))
}
}
#[derive(Debug, PartialEq, Eq, Copy, Clone, Ord, PartialOrd, Hash)]
pub enum DeclKind {
Impl,
Sign,
}
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Decl {
pub name: Ident,
pub body: Expr,
pub kind: DeclKind,
}