From c448698f797f2304dca0e0b8b833959de00ca079 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 20 Jan 2020 15:27:19 +0000 Subject: Reimplement basic tck/nze with proper environments Inspired from dhall_haskell --- dhall/src/semantics/nze/mod.rs | 2 + dhall/src/semantics/nze/nzexpr.rs | 399 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 401 insertions(+) create mode 100644 dhall/src/semantics/nze/mod.rs create mode 100644 dhall/src/semantics/nze/nzexpr.rs (limited to 'dhall/src/semantics/nze') 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, + ty: Option, +} + +#[derive(Debug, Clone)] +pub(crate) enum TyExprKind { + Var(AlphaVar), + Expr(ExprKind), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzExpr { + kind: Box, + ty: Option>, +} + +#[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), + // 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) -> Option { + 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) -> Self { + TyExpr { + kind: Box::new(kind), + ty, + } + } + + pub fn kind(&self) -> &TyExprKind { + self.kind.as_ref() + } + pub fn get_type(&self) -> Result { + 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) -> 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 { + 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) -> Result { + 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) -> Result { + type_with(&TyEnv::new(), e) +} -- cgit v1.3.1 From 476ef4594c9e8c7121bd8fc303e74ef8207a88f4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 20 Jan 2020 16:17:48 +0000 Subject: Split TyEnv into two envs --- dhall/src/semantics/nze/nzexpr.rs | 254 +++++++++++++++++++++++--------------- 1 file changed, 152 insertions(+), 102 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 2f27dcb..3a5a1f9 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -36,24 +36,24 @@ pub(crate) enum NzExprKind { Lam { binder: Binder, annot: NzExpr, - env: TyEnv, + env: NzEnv, body: TyExpr, }, Pi { binder: Binder, annot: NzExpr, - env: TyEnv, + env: NzEnv, body: TyExpr, }, Expr(ExprKind), // Unevaled { - // env: TyEnv, + // env: NzEnv, // expr: TyExprKind, // }, } #[derive(Debug, Clone)] -enum TyEnvItem { +enum NzEnvItem { // Variable is bound with given type Kept(Type), // Variable has been replaced by corresponding value @@ -62,7 +62,18 @@ enum TyEnvItem { #[derive(Debug, Clone)] pub(crate) struct TyEnv { - env: Vec<(Binder, TyEnvItem)>, + names: NameEnv, + items: NzEnv, +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec, +} + +#[derive(Debug, Clone)] +pub(crate) struct NameEnv { + names: Vec, } #[derive(Debug, Clone, Copy)] @@ -78,58 +89,120 @@ pub(crate) struct NzVar { impl TyEnv { pub fn new() -> Self { - TyEnv { env: Vec::new() } - } - pub fn to_quoteenv(&self) -> QuoteEnv { - QuoteEnv { - size: self.env.len(), + TyEnv { + names: NameEnv::new(), + items: NzEnv::new(), } } - fn with_vec(&self, vec: Vec<(Binder, TyEnvItem)>) -> Self { - TyEnv { env: vec } + 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 { - let mut vec = self.env.clone(); - vec.push((x.clone(), TyEnvItem::Kept(t))); - self.with_vec(vec) + TyEnv { + names: self.names.insert(x), + items: self.items.insert_type(t), + } } 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) + TyEnv { + names: self.names.insert(x), + items: self.items.insert_value(e), + } } pub fn lookup_var(&self, var: &V) -> Option { + 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 { + NameEnv { names: Vec::new() } + } + pub fn as_quoteenv(&self) -> QuoteEnv { + QuoteEnv { + size: self.names.len(), + } + } + + pub fn insert(&self, x: &Binder) -> Self { + let mut env = self.clone(); + env.insert_mut(x); + env + } + pub fn insert_mut(&mut self, x: &Binder) { + self.names.push(x.clone()) + } + pub fn remove_mut(&mut self) { + self.names.pop(); + } + + pub fn unlabel_var(&self, var: &V) -> Option { let V(name, idx) = var; - let (idx, (_, item)) = self - .env + let (idx, _) = self + .names .iter() .rev() .enumerate() - .filter(|(_, (x, _))| x == name) + .filter(|(_, n)| *n == 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), - )) + Some(AlphaVar::new(V((), idx))) + } + pub fn label_var(&self, var: &AlphaVar) -> V { + 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 { - let idx = self.env.len() - 1 - var.idx(); - match &self.env[idx].1 { - TyEnvItem::Kept(ty) => NzExpr::new( + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => NzExpr::new( NzExprKind::Var { var: NzVar { idx } }, Some(ty.clone()), ), - TyEnvItem::Replaced(x) => x.clone(), + NzEnvItem::Replaced(x) => x.clone(), } } - pub fn size(&self) -> usize { - self.env.len() - } } impl QuoteEnv { @@ -166,54 +239,39 @@ impl TyExpr { /// 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)) + 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); } - 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, - } + let e = tye.to_expr_noalpha(env); + if let Some(_) = l { + env.remove_mut(); } - }) - } - - tyexpr_to_expr(self, opts, &mut Vec::new()) + 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: &TyEnv) -> NzExpr { + 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)) => { @@ -236,11 +294,8 @@ impl TyExpr { 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::Lam { env, body, .. } => { + return body.normalize_nf(&env.insert_value(arg)) } _ => NzExprKind::Expr(ExprKind::App(f, arg)), }, @@ -253,7 +308,7 @@ impl TyExpr { } pub fn normalize(&self) -> NzExpr { - self.normalize_nf(&TyEnv::new()) + self.normalize_nf(&NzEnv::new()) } } @@ -287,7 +342,7 @@ impl NzExpr { } => TyExprKind::Expr(ExprKind::Lam( binder.clone(), annot.quote(qenv), - body.normalize_nf(&env.insert_type(binder, annot.clone())) + body.normalize_nf(&env.insert_type(annot.clone())) .quote(qenv.insert()), )), NzExprKind::Pi { @@ -298,7 +353,7 @@ impl NzExpr { } => TyExprKind::Expr(ExprKind::Pi( binder.clone(), annot.quote(qenv), - body.normalize_nf(&env.insert_type(binder, annot.clone())) + body.normalize_nf(&env.insert_type(annot.clone())) .quote(qenv.insert()), )), NzExprKind::Expr(e) => { @@ -329,7 +384,7 @@ fn type_with(env: &TyEnv, e: Expr) -> Result { }, ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot.clone())?; - let annot_nf = annot.normalize_nf(env); + let annot_nf = annot.normalize_nf(env.as_nzenv()); let body = type_with( &env.insert_type(&binder, annot_nf.clone()), body.clone(), @@ -338,8 +393,8 @@ fn type_with(env: &TyEnv, e: Expr) -> Result { NzExprKind::Pi { binder: binder.clone(), annot: annot_nf, - env: env.clone(), - body: body.get_type()?.quote(env.to_quoteenv()), + env: env.as_nzenv().clone(), + body: body.get_type()?.quote(env.as_quoteenv()), }, None, // TODO: function_check ); @@ -350,7 +405,7 @@ fn type_with(env: &TyEnv, e: Expr) -> Result { } ExprKind::Pi(binder, annot, body) => { let annot = type_with(env, annot.clone())?; - let annot_nf = annot.normalize_nf(env); + let annot_nf = annot.normalize_nf(env.as_nzenv()); let body = type_with( &env.insert_type(&binder, annot_nf.clone()), body.clone(), @@ -364,23 +419,18 @@ fn type_with(env: &TyEnv, e: Expr) -> Result { 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() - { + let (_expected_arg_ty, body_env, body_ty) = match tf.kind() { NzExprKind::Pi { - binder, - annot, - env, - body, - } => (binder, annot, env, body), + 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); - let ty = - body_ty.normalize_nf(&body_env.insert_value(&binder, arg_nf)); + 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)), -- cgit v1.3.1 From 3182c121815857c0b2b3c057f1d2944c51332cdc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 18:51:00 +0000 Subject: Prepare Value for reverse variables I thought it would work ><. It's a bit too early --- dhall/src/semantics/core/context.rs | 10 ++++++++-- dhall/src/semantics/core/value.rs | 40 ++++++++++++++++++++++++------------- dhall/src/semantics/core/visitor.rs | 2 +- dhall/src/semantics/nze/mod.rs | 2 +- dhall/src/semantics/nze/nzexpr.rs | 14 ++++++++++++- 5 files changed, 49 insertions(+), 19 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 8c64c26..7972a20 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,6 +2,7 @@ use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Binder}; +use crate::semantics::nze::NzVar; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -42,7 +43,6 @@ impl TyCtx { let mut var = var.clone(); let mut shift_delta: isize = 0; let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i)); - let found_item = loop { if let Some((label, item)) = rev_ctx.next() { var = match var.over_binder(&label) { @@ -57,10 +57,16 @@ impl TyCtx { return None; } }; + let var_idx = rev_ctx + .filter(|(_, i)| match i { + CtxItem::Kept(_) => true, + CtxItem::Replaced(_) => false, + }) + .count(); let v = match found_item { CtxItem::Kept(t) => Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default()), + ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)), t.clone(), ), CtxItem::Replaced(v) => v.clone(), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index dc6a116..a7c207d 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,6 +4,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; +use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ @@ -60,7 +61,7 @@ pub(crate) enum ValueKind { // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), - Var(AlphaVar), + Var(AlphaVar, NzVar), Const(Const), BoolLit(bool), NaturalLit(Natural), @@ -167,7 +168,7 @@ impl Value { self.normalize_nf(); } - self.to_tyexpr().to_expr(opts) + self.to_tyexpr(QuoteEnv::new()).to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() @@ -257,7 +258,7 @@ impl Value { match &*self.as_kind() { // If the var matches, we can just reuse the provided value instead of copying it. // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { + ValueKind::Var(v, _) if v == var => { if let Ok(self_ty) = self.get_type() { val.check_type(&self_ty.subst_shift(var, val)); } @@ -288,18 +289,27 @@ impl Value { // } // } - pub fn to_tyexpr(&self) -> TyExpr { + pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { let self_kind = self.as_kind(); let self_ty = self.as_internal().ty.clone(); let self_span = self.as_internal().span.clone(); - if let ValueKind::Var(v) = &*self_kind { - return TyExpr::new(TyExprKind::Var(*v), self_ty, self_span); + if let ValueKind::Var(v, _w) = &*self_kind { + return TyExpr::new( + // TODO: Only works when we don't normalize under lambdas + // TyExprKind::Var(qenv.lookup(w)), + TyExprKind::Var(*v), + self_ty, + self_span, + ); } // TODO: properly recover intermediate types; `None` is a time-bomb here. - let self_kind = self_kind.map_ref(|v| v.to_tyexpr()); + let self_kind = self_kind.map_ref_with_special_handling_of_binders( + |v| v.to_tyexpr(qenv), + |_, _, v| v.to_tyexpr(qenv.insert()), + ); let expr = match self_kind { - ValueKind::Var(_) => unreachable!(), + ValueKind::Var(..) => unreachable!(), ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e), ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), ValueKind::AppliedBuiltin(b, args) => { @@ -320,13 +330,13 @@ impl Value { ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), ValueKind::EmptyOptionalLit(n) => ExprKind::App( - builtin_to_value(Builtin::OptionalNone).to_tyexpr(), + builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), n, ), ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( TyExprKind::Expr(ExprKind::App( - builtin_to_value(Builtin::List).to_tyexpr(), + builtin_to_value(Builtin::List).to_tyexpr(qenv), n, )), Some(const_to_value(Const::Type)), @@ -470,7 +480,7 @@ impl ValueKind { pub(crate) fn normalize_mut(&mut self) { match self { - ValueKind::Var(_) + ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::BoolLit(_) | ValueKind::NaturalLit(_) @@ -545,7 +555,7 @@ impl ValueKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), _ => self.traverse_ref_with_special_handling_of_binders( |x| Ok(x.shift(delta, var)?), |_, _, x| Ok(x.shift(delta, &var.under_binder())?), @@ -554,8 +564,10 @@ impl ValueKind { } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Var(v, _) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v, w) => { + ValueKind::Var(v.shift(-1, var).unwrap(), *w) + } _ => self.map_ref_with_special_handling_of_binders( |x| x.subst_shift(var, val), |_, _, x| { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index a449f6c..5a04747 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -81,7 +81,7 @@ where Pi(l.clone(), t, e) } AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), - Var(v) => Var(v.clone()), + Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), NaturalLit(n) => NaturalLit(*n), diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index ef8918f..213404c 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,2 +1,2 @@ pub mod nzexpr; -// pub(crate) use nzexpr::*; +pub(crate) use nzexpr::*; diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 3a5a1f9..1256ea0 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -82,10 +82,16 @@ pub(crate) struct QuoteEnv { } // Reverse-debruijn index: counts number of binders from the bottom of the stack. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, Eq)] pub(crate) struct NzVar { idx: usize, } +// TODO: temporary hopefully +impl std::cmp::PartialEq for NzVar { + fn eq(&self, _other: &Self) -> bool { + true + } +} impl TyEnv { pub fn new() -> Self { @@ -219,6 +225,12 @@ impl QuoteEnv { } } +impl NzVar { + pub fn new(idx: usize) -> Self { + NzVar { idx } + } +} + impl TyExpr { pub fn new(kind: TyExprKind, ty: Option) -> Self { TyExpr { -- cgit v1.3.1 From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 Jan 2020 22:22:01 +0000 Subject: Implement basic env-based normalization for Value-based TyExpr --- dhall/src/semantics/core/value.rs | 267 ++++++++++++++++++++------------- dhall/src/semantics/core/visitor.rs | 18 +++ dhall/src/semantics/nze/nzexpr.rs | 2 + dhall/src/semantics/phase/normalize.rs | 85 ++++++++++- dhall/src/semantics/tck/tyexpr.rs | 8 + dhall/src/tests.rs | 14 +- 6 files changed, 283 insertions(+), 111 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index a7c207d..8beed24 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::nze::{NzVar, QuoteEnv}; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; +use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, @@ -53,11 +53,27 @@ pub(crate) enum Form { NF, } +#[derive(Debug, Clone)] +pub(crate) struct Closure { + env: NzEnv, + body: TyExpr, +} + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures Lam(Binder, Value, Value), Pi(Binder, Value, Value), + LamClosure { + binder: Binder, + annot: Value, + closure: Closure, + }, + PiClosure { + binder: Binder, + annot: Value, + closure: Closure, + }, // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), @@ -267,128 +283,136 @@ impl Value { _ => self.as_internal().subst_shift(var, val).into_value(), } } - // pub(crate) fn subst_ctx(&self, ctx: &TyCtx) -> Self { - // match &*self.as_kind() { - // ValueKind::Var(var) => match ctx.lookup_alpha(var) { - // Some(val) => val, - // None => unreachable!("Internal type error"), - // }, - // kind => { - // let kind = kind.map_ref_with_special_handling_of_binders( - // |x| x.subst_ctx(ctx), - // |b, t, x| x.subst_ctx(&ctx.insert_type(b, t.clone())), - // ); - // ValueInternal { - // form: Unevaled, - // kind, - // ty: self.as_internal().ty.clone(), - // span: self.as_internal().span.clone(), - // } - // .into_value() - // } - // } - // } pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { - let self_kind = self.as_kind(); - let self_ty = self.as_internal().ty.clone(); - let self_span = self.as_internal().span.clone(); - if let ValueKind::Var(v, _w) = &*self_kind { - return TyExpr::new( + let tye = match &*self.as_kind() { + ValueKind::Var(v, _w) => { + TyExprKind::Var(*v) // TODO: Only works when we don't normalize under lambdas - // TyExprKind::Var(qenv.lookup(w)), - TyExprKind::Var(*v), - self_ty, - self_span, - ); - } - - // TODO: properly recover intermediate types; `None` is a time-bomb here. - let self_kind = self_kind.map_ref_with_special_handling_of_binders( - |v| v.to_tyexpr(qenv), - |_, _, v| v.to_tyexpr(qenv.insert()), - ); - let expr = match self_kind { - ValueKind::Var(..) => unreachable!(), - ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e), - ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), - ValueKind::AppliedBuiltin(b, args) => { - args.into_iter().fold(ExprKind::Builtin(b), |acc, v| { - ExprKind::App( - TyExpr::new( - TyExprKind::Expr(acc), - None, // TODO - Span::Artificial, - ), - v, - ) - }) + // TyExprKind::Var(qenv.lookup(w)) } - ValueKind::Const(c) => ExprKind::Const(c), - ValueKind::BoolLit(b) => ExprKind::BoolLit(b), - ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n), - ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), - ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), - ValueKind::EmptyOptionalLit(n) => ExprKind::App( - builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), - n, - ), - ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( - TyExprKind::Expr(ExprKind::App( - builtin_to_value(Builtin::List).to_tyexpr(qenv), - n, - )), - Some(const_to_value(Const::Type)), - Span::Artificial, + ValueKind::LamClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Lam( + binder.to_label(), + annot.to_tyexpr(qenv), + closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()), )), - ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), - ValueKind::RecordLit(kvs) => { - ExprKind::RecordLit(kvs.into_iter().collect()) - } - ValueKind::RecordType(kts) => { - ExprKind::RecordType(kts.into_iter().collect()) - } - ValueKind::UnionType(kts) => { - ExprKind::UnionType(kts.into_iter().collect()) - } - ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( - TyExpr::new( - TyExprKind::Expr(ExprKind::UnionType( - kts.into_iter().collect(), - )), - Some(t), - Span::Artificial, - ), - l, - ), - ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( - TyExpr::new( - TyExprKind::Expr(ExprKind::Field( + ValueKind::PiClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Pi( + binder.to_label(), + annot.to_tyexpr(qenv), + closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()), + )), + self_kind => { + // TODO: properly recover intermediate types; `None` is a time-bomb here. + let self_kind = self_kind + .map_ref_with_special_handling_of_binders( + |v| v.to_tyexpr(qenv), + |_, _, v| v.to_tyexpr(qenv.insert()), + ); + let expr = match self_kind { + ValueKind::Var(..) + | ValueKind::LamClosure { .. } + | ValueKind::PiClosure { .. } => unreachable!(), + ValueKind::Lam(x, t, e) => { + ExprKind::Lam(x.to_label(), t, e) + } + ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), + ValueKind::AppliedBuiltin(b, args) => { + args.into_iter().fold(ExprKind::Builtin(b), |acc, v| { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(acc), + None, // TODO + Span::Artificial, + ), + v, + ) + }) + } + ValueKind::Const(c) => ExprKind::Const(c), + ValueKind::BoolLit(b) => ExprKind::BoolLit(b), + ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n), + ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), + ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), + ValueKind::EmptyOptionalLit(n) => ExprKind::App( + builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), + n, + ), + ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), + ValueKind::EmptyListLit(n) => { + ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + builtin_to_value(Builtin::List).to_tyexpr(qenv), + n, + )), + Some(const_to_value(Const::Type)), + Span::Artificial, + )) + } + ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), + ValueKind::RecordLit(kvs) => { + ExprKind::RecordLit(kvs.into_iter().collect()) + } + ValueKind::RecordType(kts) => { + ExprKind::RecordType(kts.into_iter().collect()) + } + ValueKind::UnionType(kts) => { + ExprKind::UnionType(kts.into_iter().collect()) + } + ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( TyExpr::new( TyExprKind::Expr(ExprKind::UnionType( kts.into_iter().collect(), )), - Some(uniont), + Some(t), Span::Artificial, ), l, - )), - Some(ctort), - Span::Artificial, - ), - v, - ), - ValueKind::TextLit(elts) => { - ExprKind::TextLit(elts.into_iter().collect()) - } - ValueKind::Equivalence(x, y) => { - ExprKind::BinOp(BinOp::Equivalence, x, y) + ), + ValueKind::UnionLit(l, v, kts, uniont, ctort) => { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter().collect(), + )), + Some(uniont), + Span::Artificial, + ), + l, + )), + Some(ctort), + Span::Artificial, + ), + v, + ) + } + ValueKind::TextLit(elts) => { + ExprKind::TextLit(elts.into_iter().collect()) + } + ValueKind::Equivalence(x, y) => { + ExprKind::BinOp(BinOp::Equivalence, x, y) + } + ValueKind::PartialExpr(e) => e, + }; + TyExprKind::Expr(expr) } - ValueKind::PartialExpr(e) => e, }; - TyExpr::new(TyExprKind::Expr(expr), self_ty, self_span) + let self_ty = self.as_internal().ty.clone(); + let self_span = self.as_internal().span.clone(); + TyExpr::new(tye, self_ty, self_span) + } + pub fn to_tyexpr_noenv(&self) -> TyExpr { + self.to_tyexpr(QuoteEnv::new()) } } @@ -502,6 +526,10 @@ impl ValueKind { t.normalize_mut(); e.normalize_mut(); } + ValueKind::LamClosure { annot, .. } + | ValueKind::PiClosure { annot, .. } => { + annot.normalize_mut(); + } ValueKind::AppliedBuiltin(_, args) => { for x in args.iter_mut() { x.normalize_mut(); @@ -620,6 +648,21 @@ impl ValueKind { } } +impl Closure { + pub fn new(env: &NzEnv, body: TyExpr) -> Self { + Closure { + env: env.clone(), + body: body, + } + } + pub fn apply(&self, val: Value) -> Value { + self.body.normalize_whnf(&self.env.insert_value(val)) + } + pub fn apply_ty(&self, ty: Value) -> Value { + self.body.normalize_whnf(&self.env.insert_type(ty)) + } +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -628,6 +671,14 @@ impl std::cmp::PartialEq for Value { } impl std::cmp::Eq for Value {} +// TODO: panics +impl std::cmp::PartialEq for Closure { + fn eq(&self, _other: &Self) -> bool { + panic!("comparing closures for equality seems like a bad idea") + } +} +impl std::cmp::Eq for Closure {} + impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index 5a04747..ee44ed7 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -80,6 +80,24 @@ where let (t, e) = v.visit_binder(l, t, e)?; Pi(l.clone(), t, e) } + LamClosure { + binder, + annot, + closure, + } => LamClosure { + binder: binder.clone(), + annot: v.visit_val(annot)?, + closure: closure.clone(), + }, + PiClosure { + binder, + annot, + closure, + } => PiClosure { + binder: binder.clone(), + annot: v.visit_val(annot)?, + closure: closure.clone(), + }, AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 1256ea0..723c895 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -200,6 +200,7 @@ impl NzEnv { 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( @@ -211,6 +212,7 @@ impl NzEnv { } } +// TODO: rename to VarEnv impl QuoteEnv { pub fn new() -> Self { QuoteEnv { size: 0 } diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f0a6a8c..7fd76df 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,9 +1,12 @@ use std::collections::HashMap; use std::convert::TryInto; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{ + AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -786,3 +789,83 @@ pub(crate) fn normalize_whnf( v => v, } } + +#[derive(Debug, Clone)] +enum NzEnvItem { + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec, +} + +impl NzEnv { + pub fn new() -> Self { + NzEnv { items: Vec::new() } + } + + pub fn insert_type(&self, t: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Kept(t)); + env + } + pub fn insert_value(&self, e: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Replaced(e)); + env + } + pub fn lookup_val(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( + ValueKind::Var(var.clone(), NzVar::new(idx)), + ty.clone(), + ), + NzEnvItem::Replaced(x) => x.clone(), + } + } +} + +/// Normalize a TyExpr into WHNF +pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { + let kind = match e.kind() { + TyExprKind::Var(var) => return env.lookup_val(var), + TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + ValueKind::LamClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + ValueKind::PiClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(e) => { + let e = e.map_ref(|tye| tye.normalize_whnf(env)); + match e { + ExprKind::App(f, arg) => { + let f_borrow = f.as_whnf(); + match &*f_borrow { + ValueKind::LamClosure { closure, .. } => { + return closure.apply(arg) + } + _ => { + drop(f_borrow); + ValueKind::PartialExpr(ExprKind::App(f, arg)) + } + } + } + _ => ValueKind::PartialExpr(e), + } + } + }; + Value::from_kind_and_type_whnf(kind, e.get_type().unwrap()) +} diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 983f3f8..c8be3a3 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,7 @@ #![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; +use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; @@ -51,6 +52,13 @@ impl TyExpr { pub fn to_value(&self) -> Value { todo!() } + + pub fn normalize_whnf(&self, env: &NzEnv) -> Value { + normalize_tyexpr_whnf(self, env) + } + pub fn normalize_whnf_noenv(&self) -> Value { + normalize_tyexpr_whnf(self, &NzEnv::new()) + } } fn tyexpr_to_expr<'a>( diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 7795d17..4928c51 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -206,11 +206,21 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .normalize() + // .to_expr(); let expr = parse_file_str(&expr_file_path)? .resolve()? .typecheck()? - .normalize() - .to_expr(); + .to_value() + .to_tyexpr_noenv() + .normalize_whnf_noenv() + .to_expr(crate::semantics::phase::ToExprOptions { + alpha: false, + normalize: true, + }); // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? // .normalize() -- cgit v1.3.1 From a24f2d1367b2848779014c7bb3ecfe6bfbcff7d7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 18:38:30 +0000 Subject: Fix some variable shifting failures --- dhall/src/semantics/core/context.rs | 17 +++++++++++++++-- dhall/src/semantics/core/value.rs | 18 +++++++++++------- dhall/src/semantics/nze/nzexpr.rs | 8 ++++++++ dhall/src/semantics/phase/normalize.rs | 24 +++++++++++++++++++----- 4 files changed, 53 insertions(+), 14 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 7972a20..0e62fef 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,7 +2,8 @@ use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Binder}; -use crate::semantics::nze::NzVar; +use crate::semantics::nze::{NzVar, QuoteEnv}; +use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -69,7 +70,19 @@ impl TyCtx { ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)), t.clone(), ), - CtxItem::Replaced(v) => v.clone(), + CtxItem::Replaced(v) => v.clone() + // .to_tyexpr(QuoteEnv::construct(var_idx)) + // .normalize_whnf(&NzEnv::construct( + // self.ctx + // .iter() + // .filter_map(|(_, i)| match i { + // CtxItem::Kept(t) => { + // Some(NzEnvItem::Kept(t.clone())) + // } + // CtxItem::Replaced(_) => None, + // }) + // .collect(), + // )), }; // Can't fail because delta is positive let v = v.shift(shift_delta, &AlphaVar::default()).unwrap(); diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 96bb99a..11d8bd8 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -185,7 +185,7 @@ impl Value { self.normalize_nf(); } - self.to_tyexpr(QuoteEnv::new()).to_expr(opts) + self.to_tyexpr_noenv().to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() @@ -292,11 +292,9 @@ impl Value { pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { let tye = match &*self.as_kind() { - ValueKind::Var(v, _w) => { - TyExprKind::Var(*v) - // TODO: Only works when we don't normalize under lambdas - // TyExprKind::Var(qenv.lookup(w)) - } + // ValueKind::Var(v, _w) => TyExprKind::Var(*v), + // TODO: Only works when we don't normalize under lambdas + ValueKind::Var(_v, w) => TyExprKind::Var(qenv.lookup(w)), ValueKind::LamClosure { binder, annot, @@ -611,7 +609,13 @@ impl ValueKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), + ValueKind::Var(v, w) if var.idx() <= v.idx() => { + ValueKind::Var(v.shift(delta, var)?, *w) + } + ValueKind::Var(v, w) => { + ValueKind::Var(v.shift(delta, var)?, w.shift(delta)) + } + // ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), _ => self.traverse_ref_with_special_handling_of_binders( |x| Ok(x.shift(delta, var)?), |_, _, x| Ok(x.shift(delta, &var.under_binder())?), diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 723c895..49aa704 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -217,6 +217,9 @@ impl QuoteEnv { pub fn new() -> Self { QuoteEnv { size: 0 } } + pub fn construct(size: usize) -> Self { + QuoteEnv { size } + } pub fn insert(&self) -> Self { QuoteEnv { size: self.size + 1, @@ -231,6 +234,11 @@ impl NzVar { pub fn new(idx: usize) -> Self { NzVar { idx } } + pub fn shift(&self, delta: isize) -> Self { + NzVar { + idx: (self.idx as isize + delta) as usize, + } + } } impl TyExpr { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ac60ce0..3ddfb84 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -12,8 +12,8 @@ use crate::semantics::{ use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, - Label, NaiveDouble, + BinOp, Builtin, Const, ExprKind, InterpolatedText, + InterpolatedTextContents, Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -822,7 +822,7 @@ pub(crate) fn normalize_whnf( } #[derive(Debug, Clone)] -enum NzEnvItem { +pub(crate) enum NzEnvItem { // Variable is bound with given type Kept(Value), // Variable has been replaced by corresponding value @@ -838,6 +838,9 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } + pub fn construct(items: Vec) -> Self { + NzEnv { items } + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -851,9 +854,16 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); + let var_idx = self.items[..idx] + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(var.clone(), NzVar::new(var_idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), @@ -863,7 +873,11 @@ impl NzEnv { /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = tye.get_type().unwrap(); + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return Value::from_const(Const::Sort), + }; + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { -- cgit v1.3.1 From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 Jan 2020 18:45:09 +0000 Subject: Fix a bunch of bugs and more tck --- dhall/src/semantics/core/var.rs | 8 ++++- dhall/src/semantics/nze/nzexpr.rs | 24 +++++++++---- dhall/src/semantics/phase/mod.rs | 5 +++ dhall/src/semantics/phase/normalize.rs | 5 ++- dhall/src/semantics/phase/resolve.rs | 8 +++-- dhall/src/semantics/phase/typecheck.rs | 26 ++++++++------ dhall/src/semantics/tck/tyexpr.rs | 10 ++++++ dhall/src/semantics/tck/typecheck.rs | 64 +++++++++++++++++++--------------- dhall/src/tests.rs | 11 +++--- 9 files changed, 104 insertions(+), 57 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 0d2c1d4..cf45d5e 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,10 +1,16 @@ use crate::syntax::{Label, V}; /// Stores an alpha-normalized variable. -#[derive(Clone, Copy, PartialEq, Eq)] +#[derive(Clone, Copy, Eq)] pub struct AlphaVar { alpha: V<()>, } +// TODO: temporary hopefully +impl std::cmp::PartialEq for AlphaVar { + fn eq(&self, _other: &Self) -> bool { + true + } +} // Exactly like a Label, but equality returns always true. // This is so that ValueKind equality is exactly alpha-equivalence. diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 49aa704..33fdde3 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -82,16 +82,16 @@ pub(crate) struct QuoteEnv { } // Reverse-debruijn index: counts number of binders from the bottom of the stack. -#[derive(Debug, Clone, Copy, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) struct NzVar { idx: usize, } // TODO: temporary hopefully -impl std::cmp::PartialEq for NzVar { - fn eq(&self, _other: &Self) -> bool { - true - } -} +// impl std::cmp::PartialEq for NzVar { +// fn eq(&self, _other: &Self) -> bool { +// true +// } +// } impl TyEnv { pub fn new() -> Self { @@ -144,6 +144,9 @@ impl NameEnv { size: self.names.len(), } } + pub fn names(&self) -> &[Binder] { + &self.names + } pub fn insert(&self, x: &Binder) -> Self { let mut env = self.clone(); @@ -220,13 +223,20 @@ impl QuoteEnv { pub fn construct(size: usize) -> Self { QuoteEnv { size } } + pub fn size(&self) -> usize { + self.size + } 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)) + self.lookup_fallible(var).unwrap() + } + pub fn lookup_fallible(&self, var: &NzVar) -> Option { + let idx = self.size.checked_sub(var.idx + 1)?; + Some(AlphaVar::new(V((), idx))) } } diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 4dc91e7..67cdc91 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -89,6 +89,11 @@ impl Resolved { pub fn to_expr(&self) -> ResolvedExpr { self.0.clone() } + pub fn tck_and_normalize_new_flow(&self) -> Result { + let val = crate::semantics::tck::typecheck::typecheck(&self.0)? + .normalize_whnf_noenv(); + Ok(Normalized(Typed(val))) + } } impl Typed { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 33e1f2b..5fc72fc 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::NzVar; +use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ builtin_to_value, const_to_value, rc, typecheck, }; @@ -859,6 +859,9 @@ impl NzEnv { pub fn construct(items: Vec) -> Self { NzEnv { items } } + pub fn as_quoteenv(&self) -> QuoteEnv { + QuoteEnv::construct(self.items.len()) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index cc4a024..64106aa 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -52,10 +52,14 @@ fn load_import( import_cache: &mut ImportCache, import_stack: &ImportStack, ) -> Result { + // Ok( + // do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? + // .typecheck()? + // .normalize(), + // ) Ok( do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - .typecheck()? - .normalize(), + .tck_and_normalize_new_flow()?, ) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 1aab736..18e70e4 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { pub(crate) fn builtin_to_value(b: Builtin) -> Value { Value::from_kind_and_type( ValueKind::from_builtin(b), - typecheck(type_of_builtin(b)).unwrap(), + crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) + .unwrap() + .normalize_whnf_noenv(), ) } @@ -380,17 +382,21 @@ fn type_last_layer( ExprKind::App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (tx, tb) = match &*tf_borrow { - ValueKind::Pi(_, tx, tb) => (tx, tb), + match &*tf_borrow { + ValueKind::Pi(_, tx, tb) => { + if &a.get_type()? != tx { + return mkerr("TypeMismatch"); + } + + let ret = tb.subst_shift(&AlphaVar::default(), a); + ret.normalize_nf(); + RetTypeOnly(ret) + } + ValueKind::PiClosure { closure, .. } => { + RetTypeOnly(closure.apply(a.clone())) + } _ => return mkerr("NotAFunction"), - }; - if &a.get_type()? != tx { - return mkerr("TypeMismatch"); } - - let ret = tb.subst_shift(&AlphaVar::default(), a); - ret.normalize_nf(); - RetTypeOnly(ret) } ExprKind::Annot(x, t) => { if &x.get_type()? != t { diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index c8be3a3..a42265d 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::Value; use crate::syntax::{ExprKind, Label, Span, V}; @@ -48,6 +49,15 @@ impl TyExpr { pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { tyexpr_to_expr(self, opts, &mut Vec::new()) } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + let opts = ToExprOptions { + normalize: true, + alpha: false, + }; + let env = env.as_nameenv().names(); + let mut env = env.iter().collect(); + tyexpr_to_expr(self, opts, &mut env) + } // TODO: temporary hack pub fn to_value(&self) -> Value { todo!() diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 1b64d28..4ca5d4d 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -275,10 +275,22 @@ fn type_one_layer( } ExprKind::Annot(x, t) => { let t = t.normalize_whnf(env.as_nzenv()); - if x.get_type()? != t { - return mkerr("annot mismatch"); + let x_ty = x.get_type()?; + if x_ty != t { + return mkerr(format!( + "annot mismatch: ({} : {}) : {}", + x.to_expr_tyenv(env), + x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env), + t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env) + )); + // return mkerr(format!( + // "annot mismatch: {} != {}", + // x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env), + // t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env) + // )); + // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,)); } - t + x_ty } ExprKind::App(f, arg) => { let tf = f.get_type()?; @@ -389,35 +401,29 @@ fn type_one_layer( let yk = y.get_type()?.as_const().unwrap(); Value::from_const(max(xk, yk)) } - // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => { - // match &*l.get_type()?.as_whnf() { - // ValueKind::AppliedBuiltin(List, _, _) => {} - // _ => return mkerr("BinOpTypeMismatch"), - // } - - // if l.get_type()? != r.get_type()? { - // return mkerr("BinOpTypeMismatch"); - // } + ExprKind::BinOp(BinOp::ListAppend, l, r) => { + let l_ty = l.get_type()?; + match &*l_ty.as_whnf() { + ValueKind::AppliedBuiltin(Builtin::List, _, _) => {} + _ => return mkerr("BinOpTypeMismatch"), + } - // l.get_type()? - // } - // ExprKind::BinOp(BinOp::Equivalence, l, r) => { - // if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { - // return mkerr("EquivalenceArgumentMustBeTerm"); - // } - // if r.get_type()?.get_type()?.as_const() != Some(Const::Type) { - // return mkerr("EquivalenceArgumentMustBeTerm"); - // } + if l_ty != r.get_type()? { + return mkerr("BinOpTypeMismatch"); + } - // if l.get_type()? != r.get_type()? { - // return mkerr("EquivalenceTypeMismatch"); - // } + l_ty + } + ExprKind::BinOp(BinOp::Equivalence, l, r) => { + if l.get_type()? != r.get_type()? { + return mkerr("EquivalenceTypeMismatch"); + } + if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { + return mkerr("EquivalenceArgumentsMustBeTerms"); + } - // RetWhole(Value::from_kind_and_type( - // ValueKind::Equivalence(l.clone(), r.clone()), - // Value::from_const(Type), - // )) - // } + Value::from_const(Const::Type) + } ExprKind::BinOp(o, l, r) => { let t = builtin_to_value(match o { BinOp::BoolAnd diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f51f6a8..88c09cc 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -232,13 +232,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // alpha: false, // normalize: true, // }); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::tck::typecheck::typecheck(&expr)? - .normalize_whnf_noenv() - .to_expr(crate::semantics::phase::ToExprOptions { - alpha: false, - normalize: true, - }); + let expr = parse_file_str(&expr_file_path)? + .resolve()? + .tck_and_normalize_new_flow()? + .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.3.1 From 8ced62a2cdde95c4d67298289756c12f53656df0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 18:41:20 +0000 Subject: Fix all sorts of variable shenanigans --- dhall/src/semantics/core/value.rs | 118 ++++---------------------------------- dhall/src/semantics/nze/nzexpr.rs | 34 ++++++++--- dhall/src/semantics/tck/tyexpr.rs | 15 ++++- dhall/src/tests.rs | 18 ++++++ tests_buffer | 1 + 5 files changed, 69 insertions(+), 117 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 35913cf..42da653 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -303,7 +303,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Lam( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::PiClosure { binder, @@ -312,7 +314,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Pi( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::AppliedBuiltin(b, args, types) => { TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( @@ -692,119 +696,16 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { self.body.normalize_whnf(&self.env.insert_value(val)) } - pub fn apply_fresh(&self, env: QuoteEnv) -> Value { + pub fn apply_var(&self, var: NzVar) -> Value { let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), NzVar::new(env.size())), + ValueKind::Var(AlphaVar::default(), var), self.arg_ty.clone(), ); self.apply(val) } - pub fn normalize(&self) -> Value { - self.body - .normalize_whnf(&self.env.insert_type(self.arg_ty.clone())) - } } /// Compare two values for equality modulo alpha/beta-equivalence. -// TODO: use Rc comparison to shortcut on identical pointers -fn equiv(val1: &Value, val2: &Value) -> bool { - struct ValueWithEnv<'v> { - val: &'v Value, - env: QuoteEnv, - } - impl<'v> PartialEq for ValueWithEnv<'v> { - fn eq(&self, other: &ValueWithEnv<'v>) -> bool { - equiv_with_env(self.env, self.val, other.env, other.val) - } - } - // Push the given context into every subnode of the ValueKind. That way, normal equality of the - // resulting value will take into account the context. - fn push_context<'v>( - env: QuoteEnv, - kind: &'v ValueKind, - ) -> ValueKind> { - kind.map_ref_with_special_handling_of_binders( - |val| ValueWithEnv { val, env }, - |_, _, val| ValueWithEnv { - val, - env: env.insert(), - }, - ) - } - - fn equiv_with_env<'v>( - env1: QuoteEnv, - val1: &'v Value, - env2: QuoteEnv, - val2: &'v Value, - ) -> bool { - use ValueKind::Var; - let kind1 = val1.as_whnf(); - let kind2 = val2.as_whnf(); - match (&*kind1, &*kind2) { - (Var(_, v1), Var(_, v2)) => { - v1 == v2 - // match (env1.lookup(v1), env2.lookup(v2)) { - // // Both vars were found in the environment, check they point to the same - // // binder. - // // Does that even make any sense with an incomplete environment ? - // // I have no clue what I'm doing anymore. - // (Some(i), Some(j)) => i == j, - // // Both vars point to outside the environment ???? - // // (None, None) => v1 == v2, - // _ => false, - // } - } - // (Var(_, v1), Var(_, v2)) => env1.lookup(v1) == env2.lookup(v2), - ( - ValueKind::LamClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::LamClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - ( - ValueKind::PiClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::PiClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - (k1, k2) => push_context(env1, k1) == push_context(env2, k2), - } - } - - // TODO: need to use ambiant env instead of creating new one - // Might be possible to generate free variables differently to avoid this - equiv_with_env(QuoteEnv::new(), val1, QuoteEnv::new(), val2) -} - // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -815,7 +716,8 @@ impl std::cmp::Eq for Value {} impl std::cmp::PartialEq for Closure { fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() + let v = NzVar::fresh(); + self.apply_var(v) == other.apply_var(v) } } impl std::cmp::Eq for Closure {} diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 33fdde3..6559082 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -81,10 +81,12 @@ pub(crate) struct QuoteEnv { size: usize, } -// Reverse-debruijn index: counts number of binders from the bottom of the stack. #[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub(crate) struct NzVar { - idx: usize, +pub(crate) enum NzVar { + /// Reverse-debruijn index: counts number of binders from the bottom of the stack. + Bound(usize), + /// Fake fresh variable generated for expression equality checking. + Fresh(usize), } // TODO: temporary hopefully // impl std::cmp::PartialEq for NzVar { @@ -207,7 +209,9 @@ impl NzEnv { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(ty) => NzExpr::new( - NzExprKind::Var { var: NzVar { idx } }, + NzExprKind::Var { + var: NzVar::new(idx), + }, Some(ty.clone()), ), NzEnvItem::Replaced(x) => x.clone(), @@ -235,18 +239,32 @@ impl QuoteEnv { self.lookup_fallible(var).unwrap() } pub fn lookup_fallible(&self, var: &NzVar) -> Option { - let idx = self.size.checked_sub(var.idx + 1)?; + let idx = self.size.checked_sub(var.idx() + 1)?; Some(AlphaVar::new(V((), idx))) } } impl NzVar { pub fn new(idx: usize) -> Self { - NzVar { idx } + NzVar::Bound(idx) + } + pub fn fresh() -> Self { + use std::sync::atomic::{AtomicUsize, Ordering}; + // Global counter to ensure uniqueness of the generated id. + static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0); + let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); + NzVar::Fresh(id) } pub fn shift(&self, delta: isize) -> Self { - NzVar { - idx: (self.idx as isize + delta) as usize, + NzVar::new((self.idx() as isize + delta) as usize) + } + // Panics on a fresh variable. + pub fn idx(&self) -> usize { + match self { + NzVar::Bound(i) => *i, + NzVar::Fresh(_) => panic!( + "Trying to use a fresh variable outside of equality checking" + ), } } } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a42265d..9e8dc47 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -12,7 +12,7 @@ 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)] +#[derive(Clone)] pub(crate) struct TyExpr { kind: Box, ty: Option, @@ -114,3 +114,16 @@ fn tyexpr_to_expr<'a>( } }) } + +impl std::fmt::Debug for TyExpr { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut x = fmt.debug_struct("TyExpr"); + x.field("kind", self.kind()); + if let Some(ty) = self.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } +} diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 88c09cc..971c48d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -164,6 +164,7 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // 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 expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); let ty = crate::semantics::tck::typecheck::typecheck(&expr)? .get_type()? @@ -173,6 +174,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { }); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); + // + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? + // .get_type()?; + // let expected = parse_file_str(&expected_file_path)?.to_expr(); + // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? + // .normalize_whnf_noenv(); + // // if ty != expected { + // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // })) + // // } + // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { let mut res = diff --git a/tests_buffer b/tests_buffer index 225fc98..a872503 100644 --- a/tests_buffer +++ b/tests_buffer @@ -47,6 +47,7 @@ success/ somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases somehow test types added to the Foo/build closures + λ(x : ∀(a : Type) → a) → x failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > -- cgit v1.3.1 From 084e81956e99bc759012be7c171f4095c2e59d22 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 19:34:11 +0000 Subject: Thread env through nztion to fix Foo/build closures --- dhall/build.rs | 7 ---- dhall/src/semantics/core/value.rs | 21 +++++++--- dhall/src/semantics/core/visitor.rs | 9 +++-- dhall/src/semantics/nze/nzexpr.rs | 5 +++ dhall/src/semantics/phase/normalize.rs | 70 ++++++++++++++++++++++------------ dhall/src/semantics/phase/typecheck.rs | 20 ++++++---- dhall/src/semantics/tck/typecheck.rs | 14 +++++-- 7 files changed, 95 insertions(+), 51 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/build.rs b/dhall/build.rs index ed8d98b..c95a26d 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -276,13 +276,6 @@ fn generate_tests() -> std::io::Result<()> { // TODO: record completion || path == "simple/completion" || path == "unit/Completion" - // TODO: fix variables in Foo/build - || path == "unit/ListBuildFoldFusion" - || path == "unit/ListBuildImplementation" - || path == "unit/NaturalBuildFoldFusion" - || path == "unit/NaturalBuildImplementation" - || path == "unit/OptionalBuildFoldFusion" - || path == "unit/OptionalBuildImplementation" }), input_type: FileType::Text, output_type: Some(FileType::Text), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 42da653..71c5c65 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -6,7 +6,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; -use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, builtin_to_value_env, const_to_value, +}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, }; @@ -77,7 +79,8 @@ pub(crate) enum ValueKind { }, // Invariant: in whnf, the evaluation must not be able to progress further. // Keep types around to be able to recover the types of partial applications. - AppliedBuiltin(Builtin, Vec, Vec), + // Keep env around to construct Foo/build closures; hopefully temporary. + AppliedBuiltin(Builtin, Vec, Vec, NzEnv), Var(AlphaVar, NzVar), Const(Const), @@ -144,7 +147,10 @@ impl Value { const_to_value(c) } pub(crate) fn from_builtin(b: Builtin) -> Self { - builtin_to_value(b) + Self::from_builtin_env(b, &NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { + builtin_to_value_env(b, env) } pub(crate) fn with_span(self, span: Span) -> Self { self.as_internal_mut().span = span; @@ -318,7 +324,7 @@ impl Value { .apply_var(NzVar::new(qenv.size())) .to_tyexpr(qenv.insert()), )), - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, _) => { TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( ExprKind::Builtin(*b), |acc, (v, ty)| { @@ -561,7 +567,7 @@ impl ValueKind { | ValueKind::PiClosure { annot, .. } => { annot.normalize_mut(); } - ValueKind::AppliedBuiltin(_, args, _) => { + ValueKind::AppliedBuiltin(_, args, _, _) => { for x in args.iter_mut() { x.normalize_mut(); } @@ -609,7 +615,10 @@ impl ValueKind { } pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![], vec![]) + ValueKind::from_builtin_env(b, NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![], vec![], env) } fn shift(&self, delta: isize, var: &AlphaVar) -> Option { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index 64250b0..61a7d0b 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -98,9 +98,12 @@ where annot: v.visit_val(annot)?, closure: closure.clone(), }, - AppliedBuiltin(b, xs, types) => { - AppliedBuiltin(*b, v.visit_vec(xs)?, v.visit_vec(types)?) - } + AppliedBuiltin(b, xs, types, env) => AppliedBuiltin( + *b, + v.visit_vec(xs)?, + v.visit_vec(types)?, + env.clone(), + ), Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 6559082..92ba8fd 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -141,6 +141,11 @@ impl NameEnv { pub fn new() -> Self { NameEnv { names: Vec::new() } } + pub fn from_binders(names: impl Iterator) -> Self { + NameEnv { + names: names.collect(), + } + } pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv { size: self.names.len(), diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 5fc72fc..a11cb75 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -4,9 +4,11 @@ use std::convert::TryInto; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ - builtin_to_value, const_to_value, rc, typecheck, + builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; +use crate::semantics::tck::typecheck::type_with; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; @@ -73,6 +75,7 @@ pub(crate) fn apply_builtin( args: Vec, ty: &Value, types: Vec, + env: NzEnv, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -86,6 +89,11 @@ pub(crate) fn apply_builtin( ValueWithRemainingArgs(&'a [Value], Value), DoneAsIs, } + let make_closure = |e| { + type_with(&env.to_alpha_tyenv(), &e) + .unwrap() + .normalize_whnf(&env) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), @@ -272,13 +280,12 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(list_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> λ(as : List var(T)) -> [ var(a) ] # var(as) )) - .unwrap() .app(t.clone()), ) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), @@ -300,12 +307,11 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(optional_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> Some(var(a)) )) - .unwrap() .app(t.clone()), ) .app( @@ -326,13 +332,10 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app( - typecheck(make_closure!( - λ(x : Natural) -> - 1 + var(x) - )) - .unwrap(), - ) + .app(make_closure(make_closure!( + λ(x : Natural) -> + 1 + var(x) + ))) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), @@ -366,7 +369,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args, types), + Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), } } @@ -379,7 +382,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, env) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); let types = types @@ -387,7 +390,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { .cloned() .chain(once(f.get_type().unwrap())) .collect(); - apply_builtin(*b, args, ty, types) + apply_builtin(*b, args, ty, types, env.clone()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -625,6 +628,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, + env: &NzEnv, ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, @@ -649,7 +653,7 @@ pub(crate) fn normalize_one_layer( } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -659,11 +663,12 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -827,10 +832,10 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types) => { - apply_builtin(b, args, ty, types) + ValueKind::AppliedBuiltin(b, args, types, env) => { + apply_builtin(b, args, ty, types, env) } - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -862,6 +867,9 @@ impl NzEnv { pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv::construct(self.items.len()) } + pub fn to_alpha_tyenv(&self) -> TyEnv { + TyEnv::from_nzenv_alpha(self) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -890,6 +898,10 @@ impl NzEnv { NzEnvItem::Replaced(x) => x.clone(), } } + + pub fn size(&self) -> usize { + self.items.len() + } } /// Normalize a TyExpr into WHNF @@ -924,10 +936,18 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - normalize_one_layer(e, &ty) + normalize_one_layer(e, &ty, env) } }; // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } + +/// Ignore NzEnv when comparing +impl std::cmp::PartialEq for NzEnv { + fn eq(&self, _other: &Self) -> bool { + true + } +} +impl std::cmp::Eq for NzEnv {} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 18e70e4..f559323 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -5,6 +5,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; +use crate::semantics::phase::normalize::NzEnv; use crate::semantics::phase::Normalized; use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; @@ -278,8 +279,11 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { + builtin_to_value_env(b, &NzEnv::new()) +} +pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { Value::from_kind_and_type( - ValueKind::from_builtin(b), + ValueKind::from_builtin_env(b, env.clone()), crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) .unwrap() .normalize_whnf_noenv(), @@ -433,11 +437,12 @@ fn type_last_layer( } ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( @@ -596,7 +601,7 @@ fn type_last_layer( } ExprKind::BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _, _) => {} + ValueKind::AppliedBuiltin(List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -666,6 +671,7 @@ fn type_last_layer( syntax::Builtin::Optional, args, _, + _, ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 4ca5d4d..e2619b5 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -35,6 +35,14 @@ impl TyEnv { items: NzEnv::new(), } } + pub fn from_nzenv_alpha(items: &NzEnv) -> Self { + TyEnv { + names: NameEnv::from_binders( + std::iter::repeat("_".into()).take(items.size()), + ), + items: items.clone(), + } + } pub fn as_quoteenv(&self) -> QuoteEnv { self.names.as_quoteenv() } @@ -147,7 +155,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.normalize_whnf(env.as_nzenv()); match &*t.as_whnf() { - ValueKind::AppliedBuiltin(Builtin::List, args, _) + ValueKind::AppliedBuiltin(Builtin::List, args, _, _) if args.len() == 1 => {} _ => return mkerr("InvalidListType"), }; @@ -404,7 +412,7 @@ fn type_one_layer( ExprKind::BinOp(BinOp::ListAppend, l, r) => { let l_ty = l.get_type()?; match &*l_ty.as_whnf() { - ValueKind::AppliedBuiltin(Builtin::List, _, _) => {} + ValueKind::AppliedBuiltin(Builtin::List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -572,7 +580,7 @@ fn type_one_layer( /// 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( +pub(crate) fn type_with( env: &TyEnv, expr: &Expr, ) -> Result { -- cgit v1.3.1 From db6c09f33c3c794e4b6ec8a7aa80978d945a9d7a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:26:42 +0000 Subject: Remove dead code --- dhall/src/error/mod.rs | 17 +- dhall/src/semantics/core/context.rs | 95 ----- dhall/src/semantics/core/value.rs | 32 -- dhall/src/semantics/core/visitor.rs | 8 - dhall/src/semantics/nze/nzexpr.rs | 411 +--------------------- dhall/src/semantics/phase/normalize.rs | 7 - dhall/src/semantics/phase/typecheck.rs | 624 +-------------------------------- dhall/src/semantics/tck/tyexpr.rs | 5 - dhall/src/semantics/tck/typecheck.rs | 30 +- dhall/src/syntax/ast/expr.rs | 4 - 10 files changed, 31 insertions(+), 1202 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5330c59..215a7bf 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,7 +3,7 @@ use std::io::Error as IOError; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; -use crate::syntax::{Import, Label, ParseError, Span}; +use crate::syntax::{Import, ParseError}; pub type Result = std::result::Result; @@ -45,7 +45,7 @@ pub struct TypeError { /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage { - UnboundVariable(Span), + // UnboundVariable(Span), InvalidInputType(Value), InvalidOutputType(Value), // NotAFunction(Value), @@ -57,7 +57,7 @@ pub(crate) enum TypeMessage { // InvalidPredicate(Value), // IfBranchMismatch(Value, Value), // IfBranchMustBeTerm(bool, Value), - InvalidFieldType(Label, Value), + // InvalidFieldType(Label, Value), // NotARecord(Label, Value), // MustCombineRecord(Value), // MissingRecordField(Label, Value), @@ -76,9 +76,9 @@ pub(crate) enum TypeMessage { // ProjectionMissingEntry, // ProjectionDuplicateField, Sort, - RecordTypeDuplicateField, + // RecordTypeDuplicateField, // RecordTypeMergeRequiresRecordType(Value), - UnionTypeDuplicateField, + // UnionTypeDuplicateField, // EquivalenceArgumentMustBeTerm(bool, Value), // EquivalenceTypeMismatch(Value, Value), // AssertMismatch(Value, Value), @@ -96,7 +96,7 @@ impl std::fmt::Display for TypeError { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; let msg = match &self.message { - UnboundVariable(var) => var.error("Type error: Unbound variable"), + // UnboundVariable(var) => var.error("Type error: Unbound variable"), InvalidInputType(v) => { v.span().error("Type error: Invalid function input") } @@ -171,8 +171,3 @@ impl From for Error { Error::Typecheck(err) } } -impl From 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/context.rs b/dhall/src/semantics/core/context.rs index 9749c50..8b13789 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,96 +1 @@ -use crate::error::TypeError; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Binder}; -use crate::semantics::nze::NzVar; -// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; -use crate::syntax::{Label, V}; -#[derive(Debug, Clone)] -enum CtxItem { - // Variable is bound with given type - Kept(Value), - // Variable has been replaced by corresponding value - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct TyCtx { - ctx: Vec<(Binder, CtxItem)>, -} - -impl TyCtx { - pub fn new() -> Self { - TyCtx { ctx: Vec::new() } - } - fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self { - TyCtx { ctx: vec } - } - pub fn insert_type(&self, x: &Binder, t: Value) -> Self { - let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Kept(t.under_binder()))); - self.with_vec(vec) - } - pub fn insert_value( - &self, - x: &Binder, - e: Value, - ) -> Result { - let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Replaced(e))); - Ok(self.with_vec(vec)) - } - pub fn lookup(&self, var: &V