diff options
Diffstat (limited to 'dhall/src/semantics/nze/nzexpr.rs')
| -rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 411 |
1 files changed, 15 insertions, 396 deletions
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 92ba8fd..043840e 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -1,76 +1,8 @@ -#![allow(dead_code)] use crate::semantics::core::var::AlphaVar; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; -use crate::syntax::{Expr, ExprKind, Label, V}; +use crate::syntax::{Label, V}; -pub(crate) type Type = NzExpr; -#[derive(Debug, Clone)] -pub(crate) struct TypeError; pub(crate) type Binder = Label; -// An expression with inferred types at every node and resolved variables. -#[derive(Debug, Clone)] -pub(crate) struct TyExpr { - kind: Box<TyExprKind>, - ty: Option<Type>, -} - -#[derive(Debug, Clone)] -pub(crate) enum TyExprKind { - Var(AlphaVar), - Expr(ExprKind<TyExpr, Normalized>), -} - -#[derive(Debug, Clone)] -pub(crate) struct NzExpr { - kind: Box<NzExprKind>, - ty: Option<Box<Type>>, -} - -#[derive(Debug, Clone)] -pub(crate) enum NzExprKind { - Var { - var: NzVar, - }, - Lam { - binder: Binder, - annot: NzExpr, - env: NzEnv, - body: TyExpr, - }, - Pi { - binder: Binder, - annot: NzExpr, - env: NzEnv, - body: TyExpr, - }, - Expr(ExprKind<NzExpr, Normalized>), - // Unevaled { - // env: NzEnv, - // expr: TyExprKind, - // }, -} - -#[derive(Debug, Clone)] -enum NzEnvItem { - // Variable is bound with given type - Kept(Type), - // Variable has been replaced by corresponding value - Replaced(NzExpr), -} - -#[derive(Debug, Clone)] -pub(crate) struct TyEnv { - names: NameEnv, - items: NzEnv, -} - -#[derive(Debug, Clone)] -pub(crate) struct NzEnv { - items: Vec<NzEnvItem>, -} - #[derive(Debug, Clone)] pub(crate) struct NameEnv { names: Vec<Binder>, @@ -88,54 +20,6 @@ pub(crate) enum NzVar { /// Fake fresh variable generated for expression equality checking. Fresh(usize), } -// TODO: temporary hopefully -// impl std::cmp::PartialEq for NzVar { -// fn eq(&self, _other: &Self) -> bool { -// true -// } -// } - -impl TyEnv { - pub fn new() -> Self { - TyEnv { - names: NameEnv::new(), - items: NzEnv::new(), - } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.names.as_quoteenv() - } - pub fn as_nzenv(&self) -> &NzEnv { - &self.items - } - pub fn as_nameenv(&self) -> &NameEnv { - &self.names - } - - pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_type(t), - } - } - pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_value(e), - } - } - pub fn lookup_var(&self, var: &V<Binder>) -> Option<TyExpr> { - let var = self.names.unlabel_var(var)?; - let ty = self.lookup_val(&var).get_type().unwrap(); - Some(TyExpr::new(TyExprKind::Var(var), Some(ty))) - } - pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr { - self.items.lookup_val(var) - } - pub fn size(&self) -> usize { - self.names.size() - } -} impl NameEnv { pub fn new() -> Self { @@ -163,9 +47,9 @@ impl NameEnv { pub fn insert_mut(&mut self, x: &Binder) { self.names.push(x.clone()) } - pub fn remove_mut(&mut self) { - self.names.pop(); - } + // pub fn remove_mut(&mut self) { + // self.names.pop(); + // } pub fn unlabel_var(&self, var: &V<Binder>) -> Option<AlphaVar> { let V(name, idx) = var; @@ -178,50 +62,17 @@ impl NameEnv { .nth(*idx)?; Some(AlphaVar::new(V((), idx))) } - pub fn label_var(&self, var: &AlphaVar) -> V<Binder> { - let name = &self.names[self.names.len() - 1 - var.idx()]; - let idx = self - .names - .iter() - .rev() - .take(var.idx()) - .filter(|n| *n == name) - .count(); - V(name.clone(), idx) - } - pub fn size(&self) -> usize { - self.names.len() - } -} - -impl NzEnv { - pub fn new() -> Self { - NzEnv { items: Vec::new() } - } - - pub fn insert_type(&self, t: NzExpr) -> Self { - let mut env = self.clone(); - env.items.push(NzEnvItem::Kept(t)); - env - } - pub fn insert_value(&self, e: NzExpr) -> Self { - let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e)); - env - } - pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr { - // TODO: use VarEnv - let idx = self.items.len() - 1 - var.idx(); - match &self.items[idx] { - NzEnvItem::Kept(ty) => NzExpr::new( - NzExprKind::Var { - var: NzVar::new(idx), - }, - Some(ty.clone()), - ), - NzEnvItem::Replaced(x) => x.clone(), - } - } + // pub fn label_var(&self, var: &AlphaVar) -> V<Binder> { + // let name = &self.names[self.names.len() - 1 - var.idx()]; + // let idx = self + // .names + // .iter() + // .rev() + // .take(var.idx()) + // .filter(|n| *n == name) + // .count(); + // V(name.clone(), idx) + // } } // TODO: rename to VarEnv @@ -229,9 +80,6 @@ impl QuoteEnv { pub fn new() -> Self { QuoteEnv { size: 0 } } - pub fn construct(size: usize) -> Self { - QuoteEnv { size } - } pub fn size(&self) -> usize { self.size } @@ -273,232 +121,3 @@ impl NzVar { } } } - -impl TyExpr { - pub fn new(kind: TyExprKind, ty: Option<Type>) -> Self { - TyExpr { - kind: Box::new(kind), - ty, - } - } - - pub fn kind(&self) -> &TyExprKind { - self.kind.as_ref() - } - pub fn get_type(&self) -> Result<Type, TypeError> { - match &self.ty { - Some(t) => Ok(t.clone()), - None => Err(TypeError), - } - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.alpha { - self.to_expr_alpha() - } else { - self.to_expr_noalpha(&mut NameEnv::new()) - } - } - fn to_expr_noalpha(&self, env: &mut NameEnv) -> NormalizedExpr { - rc(match self.kind() { - TyExprKind::Var(var) => ExprKind::Var(env.label_var(var)), - TyExprKind::Expr(e) => e.map_ref_maybe_binder(|l, tye| { - if let Some(l) = l { - env.insert_mut(l); - } - let e = tye.to_expr_noalpha(env); - if let Some(_) = l { - env.remove_mut(); - } - e - }), - }) - } - fn to_expr_alpha(&self) -> NormalizedExpr { - rc(match self.kind() { - TyExprKind::Var(var) => ExprKind::Var(V("_".into(), var.idx())), - TyExprKind::Expr(e) => match e.map_ref(TyExpr::to_expr_alpha) { - ExprKind::Lam(_, t, e) => ExprKind::Lam("_".into(), t, e), - ExprKind::Pi(_, t, e) => ExprKind::Pi("_".into(), t, e), - e => e, - }, - }) - } - - pub fn normalize_nf(&self, env: &NzEnv) -> NzExpr { - let kind = match self.kind() { - TyExprKind::Var(var) => return env.lookup_val(var), - TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - NzExprKind::Lam { - binder: binder.clone(), - annot: annot.normalize_nf(env), - env: env.clone(), - body: body.clone(), - } - } - TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - NzExprKind::Pi { - binder: binder.clone(), - annot: annot.normalize_nf(env), - env: env.clone(), - body: body.clone(), - } - } - TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.normalize_nf(env)); - match e { - ExprKind::App(f, arg) => match f.kind() { - NzExprKind::Lam { env, body, .. } => { - return body.normalize_nf(&env.insert_value(arg)) - } - _ => NzExprKind::Expr(ExprKind::App(f, arg)), - }, - _ => NzExprKind::Expr(e), - } - } - }; - let ty = self.ty.clone(); - NzExpr::new(kind, ty) - } - - pub fn normalize(&self) -> NzExpr { - self.normalize_nf(&NzEnv::new()) - } -} - -impl NzExpr { - pub fn new(kind: NzExprKind, ty: Option<Type>) -> Self { - NzExpr { - kind: Box::new(kind), - ty: ty.map(Box::new), - } - } - - pub fn kind(&self) -> &NzExprKind { - self.kind.as_ref() - } - pub fn get_type(&self) -> Result<Type, TypeError> { - match &self.ty { - Some(t) => Ok(t.as_ref().clone()), - None => Err(TypeError), - } - } - - pub fn quote(&self, qenv: QuoteEnv) -> TyExpr { - let ty = self.ty.as_ref().map(|t| (**t).clone()); - let kind = match self.kind.as_ref() { - NzExprKind::Var { var } => TyExprKind::Var(qenv.lookup(var)), - NzExprKind::Lam { - binder, - annot, - env, - body, - } => TyExprKind::Expr(ExprKind::Lam( - binder.clone(), - annot.quote(qenv), - body.normalize_nf(&env.insert_type(annot.clone())) - .quote(qenv.insert()), - )), - NzExprKind::Pi { - binder, - annot, - env, - body, - } => TyExprKind::Expr(ExprKind::Pi( - binder.clone(), - annot.quote(qenv), - body.normalize_nf(&env.insert_type(annot.clone())) - .quote(qenv.insert()), - )), - NzExprKind::Expr(e) => { - TyExprKind::Expr(e.map_ref(|nze| nze.quote(qenv))) - } // NzExprKind::Unevaled { env, expr } => { - // return TyExpr::new(expr.clone(), ty.clone()) - // .normalize_nf(env) - // .quote(qenv) - // } - }; - TyExpr::new(kind, ty) - } - pub fn to_expr(&self) -> NormalizedExpr { - self.quote(QuoteEnv::new()).to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } -} - -/// Type-check an expression and return the expression alongside its type if type-checking -/// succeeded, or an error if type-checking failed. -fn type_with(env: &TyEnv, e: Expr<Normalized>) -> Result<TyExpr, TypeError> { - match e.as_ref() { - ExprKind::Var(var) => match env.lookup_var(&var) { - Some(x) => Ok(x), - None => Err(TypeError), - }, - ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot.clone())?; - let annot_nf = annot.normalize_nf(env.as_nzenv()); - let body = type_with( - &env.insert_type(&binder, annot_nf.clone()), - body.clone(), - )?; - let ty = NzExpr::new( - NzExprKind::Pi { - binder: binder.clone(), - annot: annot_nf, - env: env.as_nzenv().clone(), - body: body.get_type()?.quote(env.as_quoteenv()), - }, - None, // TODO: function_check - ); - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), - Some(ty), - )) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot.clone())?; - let annot_nf = annot.normalize_nf(env.as_nzenv()); - let body = type_with( - &env.insert_type(&binder, annot_nf.clone()), - body.clone(), - )?; - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), - None, // TODO: function_check - )) - } - ExprKind::App(f, arg) => { - let f = type_with(env, f.clone())?; - let arg = type_with(env, arg.clone())?; - let tf = f.get_type()?; - let (_expected_arg_ty, body_env, body_ty) = match tf.kind() { - NzExprKind::Pi { - annot, env, body, .. - } => (annot, env, body), - _ => return Err(TypeError), - }; - // if arg.get_type()? != *expected_arg_ty { - // return Err(TypeError); - // } - - let arg_nf = arg.normalize_nf(env.as_nzenv()); - let ty = body_ty.normalize_nf(&body_env.insert_value(arg_nf)); - - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::App(f, arg)), - Some(ty), - )) - } - e => Ok(TyExpr::new( - TyExprKind::Expr(e.traverse_ref(|e| type_with(env, e.clone()))?), - None, - )), - } -} - -pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> { - type_with(&TyEnv::new(), e) -} |