summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs411
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)
-}