summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/error/mod.rs5
-rw-r--r--dhall/src/semantics/core/var.rs3
-rw-r--r--dhall/src/semantics/mod.rs1
-rw-r--r--dhall/src/semantics/nze/mod.rs2
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs399
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs16
-rw-r--r--dhall/src/tests.rs19
7 files changed, 432 insertions, 13 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 56bc8ab..844a3e4 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -174,3 +174,8 @@ impl From<TypeError> for Error {
Error::Typecheck(err)
}
}
+impl From<crate::semantics::nze::nzexpr::TypeError> for Error {
+ fn from(_: crate::semantics::nze::nzexpr::TypeError) -> Error {
+ Error::Decode(DecodeError::WrongFormatError("type error".to_string()))
+ }
+}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 0aa86d5..0d2c1d4 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -14,6 +14,9 @@ pub struct Binder {
}
impl AlphaVar {
+ pub(crate) fn new(alpha: V<()>) -> Self {
+ AlphaVar { alpha }
+ }
pub(crate) fn default() -> Self {
AlphaVar { alpha: V((), 0) }
}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 63f74ee..1304502 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,4 +1,5 @@
pub mod core;
+pub mod nze;
pub mod phase;
pub mod tck;
pub(crate) use self::core::*;
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
new file mode 100644
index 0000000..ef8918f
--- /dev/null
+++ b/dhall/src/semantics/nze/mod.rs
@@ -0,0 +1,2 @@
+pub mod nzexpr;
+// pub(crate) use nzexpr::*;
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
new file mode 100644
index 0000000..2f27dcb
--- /dev/null
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -0,0 +1,399 @@
+#![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};
+
+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: TyEnv,
+ body: TyExpr,
+ },
+ Pi {
+ binder: Binder,
+ annot: NzExpr,
+ env: TyEnv,
+ body: TyExpr,
+ },
+ Expr(ExprKind<NzExpr, Normalized>),
+ // Unevaled {
+ // env: TyEnv,
+ // expr: TyExprKind,
+ // },
+}
+
+#[derive(Debug, Clone)]
+enum TyEnvItem {
+ // Variable is bound with given type
+ Kept(Type),
+ // Variable has been replaced by corresponding value
+ Replaced(NzExpr),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct TyEnv {
+ env: Vec<(Binder, TyEnvItem)>,
+}
+
+#[derive(Debug, Clone, Copy)]
+pub(crate) struct QuoteEnv {
+ size: usize,
+}
+
+// Reverse-debruijn index: counts number of binders from the bottom of the stack.
+#[derive(Debug, Clone, Copy)]
+pub(crate) struct NzVar {
+ idx: usize,
+}
+
+impl TyEnv {
+ pub fn new() -> Self {
+ TyEnv { env: Vec::new() }
+ }
+ pub fn to_quoteenv(&self) -> QuoteEnv {
+ QuoteEnv {
+ size: self.env.len(),
+ }
+ }
+ fn with_vec(&self, vec: Vec<(Binder, TyEnvItem)>) -> Self {
+ TyEnv { env: vec }
+ }
+
+ pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self {
+ let mut vec = self.env.clone();
+ vec.push((x.clone(), TyEnvItem::Kept(t)));
+ self.with_vec(vec)
+ }
+ pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self {
+ let mut vec = self.env.clone();
+ vec.push((x.clone(), TyEnvItem::Replaced(e)));
+ self.with_vec(vec)
+ }
+ pub fn lookup_var(&self, var: &V<Binder>) -> Option<TyExpr> {
+ let V(name, idx) = var;
+ let (idx, (_, item)) = self
+ .env
+ .iter()
+ .rev()
+ .enumerate()
+ .filter(|(_, (x, _))| x == name)
+ .nth(*idx)?;
+ let ty = match item {
+ TyEnvItem::Kept(ty) => ty.clone(),
+ TyEnvItem::Replaced(e) => e.get_type().unwrap(),
+ };
+ Some(TyExpr::new(
+ TyExprKind::Var(AlphaVar::new(V((), idx))),
+ Some(ty),
+ ))
+ }
+ pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr {
+ let idx = self.env.len() - 1 - var.idx();
+ match &self.env[idx].1 {
+ TyEnvItem::Kept(ty) => NzExpr::new(
+ NzExprKind::Var { var: NzVar { idx } },
+ Some(ty.clone()),
+ ),
+ TyEnvItem::Replaced(x) => x.clone(),
+ }
+ }
+ pub fn size(&self) -> usize {
+ self.env.len()
+ }
+}
+
+impl QuoteEnv {
+ pub fn new() -> Self {
+ QuoteEnv { size: 0 }
+ }
+ pub fn insert(&self) -> Self {
+ QuoteEnv {
+ size: self.size + 1,
+ }
+ }
+ pub fn lookup(&self, var: &NzVar) -> AlphaVar {
+ AlphaVar::new(V((), self.size - var.idx - 1))
+ }
+}
+
+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 {
+ fn tyexpr_to_expr<'a>(
+ tyexpr: &'a TyExpr,
+ opts: ToExprOptions,
+ env: &mut Vec<&'a Binder>,
+ ) -> NormalizedExpr {
+ rc(match tyexpr.kind() {
+ TyExprKind::Var(var) if opts.alpha => {
+ ExprKind::Var(V("_".into(), var.idx()))
+ }
+ TyExprKind::Var(var) => {
+ let name = env[env.len() - 1 - var.idx()];
+ let idx = env
+ .iter()
+ .rev()
+ .take(var.idx())
+ .filter(|l| **l == name)
+ .count();
+ ExprKind::Var(V(name.clone(), idx))
+ }
+ TyExprKind::Expr(e) => {
+ let e = e.map_ref_maybe_binder(|l, tye| {
+ if let Some(l) = l {
+ env.push(l);
+ }
+ let e = tyexpr_to_expr(tye, opts, env);
+ if let Some(_) = l {
+ env.pop();
+ }
+ e
+ });
+
+ match e {
+ ExprKind::Lam(_, t, e) if opts.alpha => {
+ ExprKind::Lam("_".into(), t, e)
+ }
+ ExprKind::Pi(_, t, e) if opts.alpha => {
+ ExprKind::Pi("_".into(), t, e)
+ }
+ e => e,
+ }
+ }
+ })
+ }
+
+ tyexpr_to_expr(self, opts, &mut Vec::new())
+ }
+
+ pub fn normalize_nf(&self, env: &TyEnv) -> 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 {
+ binder, env, body, ..
+ } => {
+ return body
+ .normalize_nf(&env.insert_value(binder, 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(&TyEnv::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(binder, 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(binder, 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);
+ 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.clone(),
+ body: body.get_type()?.quote(env.to_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);
+ 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 (binder, _expected_arg_ty, body_env, body_ty) = match tf.kind()
+ {
+ NzExprKind::Pi {
+ binder,
+ annot,
+ env,
+ body,
+ } => (binder, annot, env, body),
+ _ => return Err(TypeError),
+ };
+ // if arg.get_type()? != *expected_arg_ty {
+ // return Err(TypeError);
+ // }
+
+ let arg_nf = arg.normalize_nf(env);
+ let ty =
+ body_ty.normalize_nf(&body_env.insert_value(&binder, 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)
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 36cae04..72f5b1d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -11,15 +11,17 @@ use crate::syntax::{ExprKind, Label, Span, V};
pub(crate) type Type = Value;
// An expression with inferred types at every node and resolved variables.
+#[derive(Debug, Clone)]
pub(crate) struct TyExpr {
kind: Box<TyExprKind>,
ty: Option<Type>,
span: Span,
}
+#[derive(Debug, Clone)]
pub(crate) enum TyExprKind {
Var(AlphaVar),
- // Forbidden ExprKind variants: Var
+ // Forbidden ExprKind variants: Var, Import, Embed
Expr(ExprKind<TyExpr, Normalized>),
}
@@ -63,12 +65,12 @@ fn tyexpr_to_expr<'a>(
}
TyExprKind::Var(v) => {
let name = ctx[ctx.len() - 1 - v.idx()];
- let mut idx = 0;
- for l in ctx.iter().rev().take(v.idx()) {
- if *l == name {
- idx += 1;
- }
- }
+ let idx = ctx
+ .iter()
+ .rev()
+ .take(v.idx())
+ .filter(|l| **l == name)
+ .count();
ExprKind::Var(V(name.clone(), idx))
}
TyExprKind::Expr(e) => {
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index f1648cf..d86574a 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -158,9 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
parse_file_str(&file_path)?.resolve().unwrap_err();
}
TypeInferenceSuccess(expr_file_path, expected_file_path) => {
- let expr =
- parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
- let ty = expr.get_type()?.to_expr();
+ // let expr =
+ // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
+ // let ty = expr.get_type()?.to_expr();
+ let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
+ let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?;
+ let ty = tyexpr.get_type()?.to_expr();
let expected = parse_file_str(&expected_file_path)?.to_expr();
assert_eq_display!(ty, expected);
}
@@ -203,9 +206,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
}
}
Normalization(expr_file_path, expected_file_path) => {
- let expr = parse_file_str(&expr_file_path)?
- .resolve()?
- .typecheck()?
+ // let expr = parse_file_str(&expr_file_path)?
+ // .resolve()?
+ // .typecheck()?
+ // .normalize()
+ // .to_expr();
+ let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
+ let expr = crate::semantics::nze::nzexpr::typecheck(expr)?
.normalize()
.to_expr();
let expected = parse_file_str(&expected_file_path)?.to_expr();
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 13:08:23 +0000