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.2.3 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.2.3 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/nze/mod.rs | 2 +- dhall/src/semantics/nze/nzexpr.rs | 14 +++++++++++++- 2 files changed, 14 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze') 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.2.3 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/nze/nzexpr.rs | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dhall/src/semantics/nze') 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 } -- cgit v1.2.3 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/nze/nzexpr.rs | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dhall/src/semantics/nze') 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 { -- cgit v1.2.3 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/nze/nzexpr.rs | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'dhall/src/semantics/nze') 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))) } } -- cgit v1.2.3 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/nze/nzexpr.rs | 34 ++++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/nze') 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" + ), } } } -- cgit v1.2.3 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/src/semantics/nze/nzexpr.rs | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'dhall/src/semantics/nze') 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(), -- cgit v1.2.3 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/semantics/nze/nzexpr.rs | 411 ++------------------------------------ 1 file changed, 15 insertions(+), 396 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 92ba8fd..043840e 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -1,76 +1,8 @@ -#![allow(dead_code)] use crate::semantics::core::var::AlphaVar; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; -use crate::syntax::{Expr, ExprKind, Label, V}; +use crate::syntax::{Label, V}; -pub(crate) type Type = NzExpr; -#[derive(Debug, Clone)] -pub(crate) struct TypeError; pub(crate) type Binder = Label; -// An expression with inferred types at every node and resolved variables. -#[derive(Debug, Clone)] -pub(crate) struct TyExpr { - kind: Box, - 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: NzEnv, - body: TyExpr, - }, - Pi { - binder: Binder, - annot: NzExpr, - env: NzEnv, - body: TyExpr, - }, - Expr(ExprKind), - // Unevaled { - // env: NzEnv, - // expr: TyExprKind, - // }, -} - -#[derive(Debug, Clone)] -enum NzEnvItem { - // Variable is bound with given type - Kept(Type), - // Variable has been replaced by corresponding value - Replaced(NzExpr), -} - -#[derive(Debug, Clone)] -pub(crate) struct TyEnv { - names: NameEnv, - items: NzEnv, -} - -#[derive(Debug, Clone)] -pub(crate) struct NzEnv { - items: Vec, -} - #[derive(Debug, Clone)] pub(crate) struct NameEnv { names: Vec, @@ -88,54 +20,6 @@ pub(crate) enum NzVar { /// Fake fresh variable generated for expression equality checking. Fresh(usize), } -// TODO: temporary hopefully -// impl std::cmp::PartialEq for NzVar { -// fn eq(&self, _other: &Self) -> bool { -// true -// } -// } - -impl TyEnv { - pub fn new() -> Self { - TyEnv { - names: NameEnv::new(), - items: NzEnv::new(), - } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.names.as_quoteenv() - } - pub fn as_nzenv(&self) -> &NzEnv { - &self.items - } - pub fn as_nameenv(&self) -> &NameEnv { - &self.names - } - - pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_type(t), - } - } - pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_value(e), - } - } - pub fn lookup_var(&self, var: &V) -> 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 { @@ -163,9 +47,9 @@ impl NameEnv { pub fn insert_mut(&mut self, x: &Binder) { self.names.push(x.clone()) } - pub fn remove_mut(&mut self) { - self.names.pop(); - } + // pub fn remove_mut(&mut self) { + // self.names.pop(); + // } pub fn unlabel_var(&self, var: &V) -> Option { let V(name, idx) = var; @@ -178,50 +62,17 @@ impl NameEnv { .nth(*idx)?; Some(AlphaVar::new(V((), idx))) } - pub fn label_var(&self, var: &AlphaVar) -> V { - let name = &self.names[self.names.len() - 1 - var.idx()]; - let idx = self - .names - .iter() - .rev() - .take(var.idx()) - .filter(|n| *n == name) - .count(); - V(name.clone(), idx) - } - pub fn size(&self) -> usize { - self.names.len() - } -} - -impl NzEnv { - pub fn new() -> Self { - NzEnv { items: Vec::new() } - } - - pub fn insert_type(&self, t: NzExpr) -> Self { - let mut env = self.clone(); - env.items.push(NzEnvItem::Kept(t)); - env - } - pub fn insert_value(&self, e: NzExpr) -> Self { - let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e)); - env - } - pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr { - // TODO: use VarEnv - let idx = self.items.len() - 1 - var.idx(); - match &self.items[idx] { - NzEnvItem::Kept(ty) => NzExpr::new( - NzExprKind::Var { - var: NzVar::new(idx), - }, - Some(ty.clone()), - ), - NzEnvItem::Replaced(x) => x.clone(), - } - } + // pub fn label_var(&self, var: &AlphaVar) -> V { + // let name = &self.names[self.names.len() - 1 - var.idx()]; + // let idx = self + // .names + // .iter() + // .rev() + // .take(var.idx()) + // .filter(|n| *n == name) + // .count(); + // V(name.clone(), idx) + // } } // TODO: rename to VarEnv @@ -229,9 +80,6 @@ impl QuoteEnv { pub fn new() -> Self { QuoteEnv { size: 0 } } - pub fn construct(size: usize) -> Self { - QuoteEnv { size } - } pub fn size(&self) -> usize { self.size } @@ -273,232 +121,3 @@ impl NzVar { } } } - -impl TyExpr { - pub fn new(kind: TyExprKind, ty: Option) -> 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 { - if opts.alpha { - self.to_expr_alpha() - } else { - self.to_expr_noalpha(&mut NameEnv::new()) - } - } - fn to_expr_noalpha(&self, env: &mut NameEnv) -> NormalizedExpr { - rc(match self.kind() { - TyExprKind::Var(var) => ExprKind::Var(env.label_var(var)), - TyExprKind::Expr(e) => e.map_ref_maybe_binder(|l, tye| { - if let Some(l) = l { - env.insert_mut(l); - } - let e = tye.to_expr_noalpha(env); - if let Some(_) = l { - env.remove_mut(); - } - e - }), - }) - } - fn to_expr_alpha(&self) -> NormalizedExpr { - rc(match self.kind() { - TyExprKind::Var(var) => ExprKind::Var(V("_".into(), var.idx())), - TyExprKind::Expr(e) => match e.map_ref(TyExpr::to_expr_alpha) { - ExprKind::Lam(_, t, e) => ExprKind::Lam("_".into(), t, e), - ExprKind::Pi(_, t, e) => ExprKind::Pi("_".into(), t, e), - e => e, - }, - }) - } - - pub fn normalize_nf(&self, env: &NzEnv) -> NzExpr { - let kind = match self.kind() { - TyExprKind::Var(var) => return env.lookup_val(var), - TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - NzExprKind::Lam { - binder: binder.clone(), - annot: annot.normalize_nf(env), - env: env.clone(), - body: body.clone(), - } - } - TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - NzExprKind::Pi { - binder: binder.clone(), - annot: annot.normalize_nf(env), - env: env.clone(), - body: body.clone(), - } - } - TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.normalize_nf(env)); - match e { - ExprKind::App(f, arg) => match f.kind() { - NzExprKind::Lam { env, body, .. } => { - return body.normalize_nf(&env.insert_value(arg)) - } - _ => NzExprKind::Expr(ExprKind::App(f, arg)), - }, - _ => NzExprKind::Expr(e), - } - } - }; - let ty = self.ty.clone(); - NzExpr::new(kind, ty) - } - - pub fn normalize(&self) -> NzExpr { - self.normalize_nf(&NzEnv::new()) - } -} - -impl NzExpr { - pub fn new(kind: NzExprKind, ty: Option) -> 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(annot.clone())) - .quote(qenv.insert()), - )), - NzExprKind::Pi { - binder, - annot, - env, - body, - } => TyExprKind::Expr(ExprKind::Pi( - binder.clone(), - annot.quote(qenv), - body.normalize_nf(&env.insert_type(annot.clone())) - .quote(qenv.insert()), - )), - NzExprKind::Expr(e) => { - TyExprKind::Expr(e.map_ref(|nze| nze.quote(qenv))) - } // NzExprKind::Unevaled { env, expr } => { - // return TyExpr::new(expr.clone(), ty.clone()) - // .normalize_nf(env) - // .quote(qenv) - // } - }; - TyExpr::new(kind, ty) - } - pub fn to_expr(&self) -> NormalizedExpr { - self.quote(QuoteEnv::new()).to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } -} - -/// Type-check an expression and return the expression alongside its type if type-checking -/// succeeded, or an error if type-checking failed. -fn type_with(env: &TyEnv, e: Expr) -> 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.as_nzenv()); - let body = type_with( - &env.insert_type(&binder, annot_nf.clone()), - body.clone(), - )?; - let ty = NzExpr::new( - NzExprKind::Pi { - binder: binder.clone(), - annot: annot_nf, - env: env.as_nzenv().clone(), - body: body.get_type()?.quote(env.as_quoteenv()), - }, - None, // TODO: function_check - ); - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), - Some(ty), - )) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot.clone())?; - let annot_nf = annot.normalize_nf(env.as_nzenv()); - let body = type_with( - &env.insert_type(&binder, annot_nf.clone()), - body.clone(), - )?; - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), - None, // TODO: function_check - )) - } - ExprKind::App(f, arg) => { - let f = type_with(env, f.clone())?; - let arg = type_with(env, arg.clone())?; - let tf = f.get_type()?; - let (_expected_arg_ty, body_env, body_ty) = match tf.kind() { - NzExprKind::Pi { - annot, env, body, .. - } => (annot, env, body), - _ => return Err(TypeError), - }; - // if arg.get_type()? != *expected_arg_ty { - // return Err(TypeError); - // } - - let arg_nf = arg.normalize_nf(env.as_nzenv()); - let ty = body_ty.normalize_nf(&body_env.insert_value(arg_nf)); - - Ok(TyExpr::new( - TyExprKind::Expr(ExprKind::App(f, arg)), - Some(ty), - )) - } - e => Ok(TyExpr::new( - TyExprKind::Expr(e.traverse_ref(|e| type_with(env, e.clone()))?), - None, - )), - } -} - -pub(crate) fn typecheck(e: Expr) -> Result { - type_with(&TyEnv::new(), e) -} -- cgit v1.2.3 From 26d4975a4c94c2b9fd0c075ad94c2588e3cf24e8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:29:53 +0000 Subject: Use NameEnv in tyexpr_to_expr --- dhall/src/semantics/nze/nzexpr.rs | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 043840e..7263cac 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -35,9 +35,6 @@ 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(); @@ -47,9 +44,9 @@ impl NameEnv { pub fn insert_mut(&mut self, x: &Binder) { self.names.push(x.clone()) } - // pub fn remove_mut(&mut self) { - // self.names.pop(); - // } + pub fn remove_mut(&mut self) { + self.names.pop(); + } pub fn unlabel_var(&self, var: &V) -> Option { let V(name, idx) = var; @@ -62,17 +59,17 @@ impl NameEnv { .nth(*idx)?; 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 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) + } } // TODO: rename to VarEnv -- cgit v1.2.3 From 22bec94618454f57773716870f5624579ab712ce Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:31:53 +0000 Subject: s/QuoteEnv/VarEnv/ --- dhall/src/semantics/nze/nzexpr.rs | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 7263cac..87d0269 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -9,7 +9,7 @@ pub(crate) struct NameEnv { } #[derive(Debug, Clone, Copy)] -pub(crate) struct QuoteEnv { +pub(crate) struct VarEnv { size: usize, } @@ -30,8 +30,8 @@ impl NameEnv { names: names.collect(), } } - pub fn as_quoteenv(&self) -> QuoteEnv { - QuoteEnv { + pub fn as_varenv(&self) -> VarEnv { + VarEnv { size: self.names.len(), } } @@ -72,16 +72,15 @@ impl NameEnv { } } -// TODO: rename to VarEnv -impl QuoteEnv { +impl VarEnv { pub fn new() -> Self { - QuoteEnv { size: 0 } + VarEnv { size: 0 } } pub fn size(&self) -> usize { self.size } pub fn insert(&self) -> Self { - QuoteEnv { + VarEnv { size: self.size + 1, } } -- cgit v1.2.3 From 280b3174476ef8fe5a98f3614f4fe253fa243d8c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:35:28 +0000 Subject: Finally get rid of all of the shift/subst_shift ! --- dhall/src/semantics/nze/nzexpr.rs | 3 --- 1 file changed, 3 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 87d0269..c065a5b 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -104,9 +104,6 @@ impl NzVar { let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); NzVar::Fresh(id) } - pub fn shift(&self, delta: isize) -> Self { - NzVar::new((self.idx() as isize + delta) as usize) - } // Panics on a fresh variable. pub fn idx(&self) -> usize { match self { -- cgit v1.2.3 From 489174a426e6057a68b6edd2e9b4387d09912a25 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:56:52 +0000 Subject: Move envs to their own files --- dhall/src/semantics/nze/env.rs | 87 ++++++++++++++++++++++++++++ dhall/src/semantics/nze/mod.rs | 4 +- dhall/src/semantics/nze/nzexpr.rs | 116 -------------------------------------- 3 files changed, 89 insertions(+), 118 deletions(-) create mode 100644 dhall/src/semantics/nze/env.rs delete mode 100644 dhall/src/semantics/nze/nzexpr.rs (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs new file mode 100644 index 0000000..203d99a --- /dev/null +++ b/dhall/src/semantics/nze/env.rs @@ -0,0 +1,87 @@ +use crate::semantics::{AlphaVar, TyEnv, Value, ValueKind}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +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), +} + +#[derive(Debug, Clone)] +pub(crate) 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 NzVar { + pub fn new(idx: usize) -> Self { + 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) + } + /// Get index of bound variable. + /// 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" + ), + } + } +} + +impl NzEnv { + pub fn new() -> Self { + NzEnv { items: Vec::new() } + } + 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(); + 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(), + } + } + + pub fn size(&self) -> usize { + self.items.len() + } +} + +/// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`. +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/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index 213404c..1cd2363 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 mod env; +pub(crate) use env::*; diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs deleted file mode 100644 index c065a5b..0000000 --- a/dhall/src/semantics/nze/nzexpr.rs +++ /dev/null @@ -1,116 +0,0 @@ -use crate::semantics::core::var::AlphaVar; -use crate::syntax::{Label, V}; - -pub(crate) type Binder = Label; - -#[derive(Debug, Clone)] -pub(crate) struct NameEnv { - names: Vec, -} - -#[derive(Debug, Clone, Copy)] -pub(crate) struct VarEnv { - size: usize, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -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), -} - -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_varenv(&self) -> VarEnv { - VarEnv { - 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, _) = self - .names - .iter() - .rev() - .enumerate() - .filter(|(_, n)| *n == name) - .nth(*idx)?; - 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) - } -} - -impl VarEnv { - pub fn new() -> Self { - VarEnv { size: 0 } - } - pub fn size(&self) -> usize { - self.size - } - pub fn insert(&self) -> Self { - VarEnv { - size: self.size + 1, - } - } - pub fn lookup(&self, var: &NzVar) -> AlphaVar { - 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))) - } -} - -impl NzVar { - pub fn new(idx: usize) -> Self { - 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) - } - // 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" - ), - } - } -} -- cgit v1.2.3 From a928c3c4f51d87fd942e8a81727962c00abf6808 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 22:06:01 +0000 Subject: Cleanup variable handling --- dhall/src/semantics/nze/env.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 203d99a..3c42ee7 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -66,7 +66,7 @@ impl NzEnv { 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)), + ValueKind::Var(NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), -- cgit v1.2.3 From 7dd2d64073b662acccb39601591c754279385308 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:24:48 +0000 Subject: No need for the current env to tck Foo/build closures --- dhall/src/semantics/nze/env.rs | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 3c42ee7..dee597a 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, TyEnv, Value, ValueKind}; +use crate::semantics::{AlphaVar, Value, ValueKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum NzVar { @@ -9,7 +9,7 @@ pub(crate) enum NzVar { } #[derive(Debug, Clone)] -pub(crate) enum NzEnvItem { +enum NzEnvItem { // Variable is bound with given type Kept(Value), // Variable has been replaced by corresponding value @@ -48,9 +48,6 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } - 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(); @@ -72,10 +69,6 @@ impl NzEnv { NzEnvItem::Replaced(x) => x.clone(), } } - - pub fn size(&self) -> usize { - self.items.len() - } } /// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`. -- cgit v1.2.3 From 17732b041dbd44f39ce3d04a289146db9882e865 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:53:37 +0000 Subject: Encapsulate partially applied builtin in a separate struct --- dhall/src/semantics/nze/env.rs | 8 -------- 1 file changed, 8 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index dee597a..a083076 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -70,11 +70,3 @@ impl NzEnv { } } } - -/// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`. -impl std::cmp::PartialEq for NzEnv { - fn eq(&self, _other: &Self) -> bool { - true - } -} -impl std::cmp::Eq for NzEnv {} -- cgit v1.2.3 From 0c95dd4f940e796865976dad594068ae0fff8f7c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:01:36 +0000 Subject: Move Value-related stuff under semantics::nze --- dhall/src/semantics/nze/mod.rs | 5 + dhall/src/semantics/nze/value.rs | 698 +++++++++++++++++++++++++++++++++++++ dhall/src/semantics/nze/var.rs | 36 ++ dhall/src/semantics/nze/visitor.rs | 167 +++++++++ 4 files changed, 906 insertions(+) create mode 100644 dhall/src/semantics/nze/value.rs create mode 100644 dhall/src/semantics/nze/var.rs create mode 100644 dhall/src/semantics/nze/visitor.rs (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index 1cd2363..f367f8f 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,2 +1,7 @@ pub mod env; +pub mod value; +pub mod var; +pub mod visitor; pub(crate) use env::*; +pub(crate) use value::*; +pub(crate) use var::*; diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs new file mode 100644 index 0000000..4960076 --- /dev/null +++ b/dhall/src/semantics/nze/value.rs @@ -0,0 +1,698 @@ +use std::cell::{Ref, RefCell, RefMut}; +use std::collections::HashMap; +use std::rc::Rc; + +use crate::error::{TypeError, TypeMessage}; +use crate::semantics::nze::visitor; +use crate::semantics::phase::normalize::{ + apply_any, normalize_tyexpr_whnf, normalize_whnf, +}; +use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::semantics::Binder; +use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; +use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; +use crate::syntax::{ + BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, Span, +}; + +use self::Form::{Unevaled, WHNF}; + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation +/// automatically. Uses a RefCell to share computation. +/// Can optionally store a type from typechecking to preserve type information. +/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence +/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively +/// normalize as needed. +#[derive(Clone)] +pub(crate) struct Value(Rc>); + +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +#[derive(Debug)] +struct ValueInternal { + form: Form, + kind: ValueKind, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option, + span: Span, +} + +#[derive(Debug, Clone, Copy)] +pub(crate) enum Form { + /// No constraints; expression may not be normalized at all. + Unevaled, + /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may + /// not be normalized. This means that the first constructor of the contained ValueKind is the first + /// constructor of the final Normal Form (NF). + /// When all the Values in a ValueKind are in WHNF, and recursively so, then the + /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so + /// if we have the first constructor of the NF at all levels, we actually have the NF. + WHNF, +} + +/// An unevaluated subexpression +#[derive(Debug, Clone)] +pub(crate) struct Thunk { + env: NzEnv, + body: TyExpr, +} + +/// An unevaluated subexpression that takes an argument. +#[derive(Debug, Clone)] +pub(crate) enum Closure { + /// Normal closure + Closure { + arg_ty: Value, + env: NzEnv, + body: TyExpr, + }, + /// Closure that ignores the argument passed + ConstantClosure { env: NzEnv, body: TyExpr }, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueKind { + /// Closures + 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(BuiltinClosure), + + Var(NzVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + // Also keep the type of the uniontype around + UnionConstructor(Label, HashMap>, Value), + // Also keep the type of the uniontype and the constructor around + UnionLit(Label, Value, HashMap>, Value, Value), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind), + // Invariant: absent in whnf + Thunk(Thunk), +} + +impl Value { + fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { + ValueInternal { + form, + kind, + ty: Some(ty), + span, + } + .into_value() + } + pub(crate) fn const_sort() -> Value { + ValueInternal { + form: WHNF, + kind: ValueKind::Const(Const::Sort), + ty: None, + span: Span::Artificial, + } + .into_value() + } + pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { + ValueInternal { + form: Unevaled, + kind: ValueKind::Thunk(Thunk::new(env, tye.clone())), + ty: tye.get_type().ok(), + span: tye.span().clone(), + } + .into_value() + } + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { + Value::new(v, Unevaled, t, Span::Artificial) + } + pub(crate) fn from_kind_and_type_whnf( + v: ValueKind, + t: Value, + ) -> Value { + Value::new(v, WHNF, t, Span::Artificial) + } + pub(crate) fn from_const(c: Const) -> Self { + let v = ValueKind::Const(c); + match c { + Const::Type => { + Value::from_kind_and_type(v, Value::from_const(Const::Kind)) + } + Const::Kind => { + Value::from_kind_and_type(v, Value::from_const(Const::Sort)) + } + Const::Sort => Value::const_sort(), + } + } + pub(crate) fn from_builtin(b: Builtin) -> Self { + Self::from_builtin_env(b, &NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { + Value::from_kind_and_type( + ValueKind::from_builtin_env(b, env.clone()), + typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(), + ) + } + + pub(crate) fn as_const(&self) -> Option { + match &*self.kind() { + ValueKind::Const(c) => Some(*c), + _ => None, + } + } + pub(crate) fn span(&self) -> Span { + self.as_internal().span.clone() + } + + fn as_internal(&self) -> Ref { + self.0.borrow() + } + fn as_internal_mut(&self) -> RefMut { + self.0.borrow_mut() + } + /// This is what you want if you want to pattern-match on the value. + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn kind(&self) -> Ref> { + self.normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_kind) + } + + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + if opts.normalize { + self.normalize_nf(); + } + + self.to_tyexpr_noenv().to_expr(opts) + } + pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { + self.kind().clone() + } + /// Before discarding type information, check that it matches the expected return type. + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { + self.check_type(ty); + self.to_whnf_ignore_type() + } + + /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { + match Rc::get_mut(&mut self.0) { + // Mutate directly if sole owner + Some(refcell) => f(RefCell::get_mut(refcell)), + // Otherwise mutate through the refcell + None => f(&mut self.as_internal_mut()), + } + } + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this. + pub(crate) fn normalize_mut(&mut self) { + self.mutate_internal(|vint| vint.normalize_nf()) + } + + pub(crate) fn normalize_whnf(&self) { + let borrow = self.as_internal(); + match borrow.form { + Unevaled => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); + } + // Already in WHNF + WHNF => {} + } + } + pub(crate) fn normalize_nf(&self) { + self.as_internal_mut().normalize_nf(); + } + + pub(crate) fn app(&self, v: Value) -> Value { + let body_t = match &*self.get_type_not_sort().kind() { + ValueKind::PiClosure { annot, closure, .. } => { + v.check_type(annot); + closure.apply(v.clone()) + } + _ => unreachable!("Internal type error"), + }; + Value::from_kind_and_type_whnf( + apply_any(self.clone(), v, &body_t), + body_t, + ) + } + + /// In debug mode, panic if the provided type doesn't match the value's type. + /// Otherwise does nothing. + pub(crate) fn check_type(&self, _ty: &Value) { + // TODO: reenable + // debug_assert_eq!( + // Some(ty), + // self.get_type().ok().as_ref(), + // "Internal type error" + // ); + } + pub(crate) fn get_type(&self) -> Result { + Ok(self.as_internal().get_type()?.clone()) + } + /// When we know the value isn't `Sort`, this gets the type directly + pub(crate) fn get_type_not_sort(&self) -> Value { + self.get_type() + .expect("Internal type error: value is `Sort` but shouldn't be") + } + + pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + let tye = match &*self.kind() { + ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), + ValueKind::LamClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Lam( + binder.to_label(), + annot.to_tyexpr(venv), + closure.to_tyexpr(venv), + )), + ValueKind::PiClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Pi( + binder.to_label(), + annot.to_tyexpr(venv), + closure.to_tyexpr(venv), + )), + ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), + ValueKind::UnionConstructor(l, kts, t) => { + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| v.to_tyexpr(venv)), + ) + }) + .collect(), + )), + Some(t.clone()), + Span::Artificial, + ), + l.clone(), + )) + } + ValueKind::UnionLit(l, v, kts, uniont, ctort) => { + TyExprKind::Expr(ExprKind::App( + TyExpr::new( + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref() + .map(|v| v.to_tyexpr(venv)), + ) + }) + .collect(), + )), + Some(uniont.clone()), + Span::Artificial, + ), + l.clone(), + )), + Some(ctort.clone()), + Span::Artificial, + ), + v.to_tyexpr(venv), + )) + } + ValueKind::Thunk(th) => return th.to_tyexpr(venv), + self_kind => { + let self_kind = self_kind.map_ref(|v| v.to_tyexpr(venv)); + let expr = match self_kind { + ValueKind::Var(..) + | ValueKind::LamClosure { .. } + | ValueKind::PiClosure { .. } + | ValueKind::AppliedBuiltin(..) + | ValueKind::UnionConstructor(..) + | ValueKind::UnionLit(..) + | ValueKind::Thunk(..) => unreachable!(), + 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( + Value::from_builtin(Builtin::OptionalNone) + .to_tyexpr(venv), + n, + ), + ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), + ValueKind::EmptyListLit(n) => { + ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + Value::from_builtin(Builtin::List) + .to_tyexpr(venv), + n, + )), + Some(Value::from_const(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::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) + } + }; + + 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(VarEnv::new()) + } +} + +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_kind(&self) -> &ValueKind { + &self.kind + } + + fn normalize_whnf(&mut self) { + let dummy = ValueInternal { + form: Unevaled, + kind: ValueKind::Const(Const::Type), + ty: None, + span: Span::Artificial, + }; + let vint = std::mem::replace(self, dummy); + *self = match (&vint.form, &vint.ty) { + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + kind: normalize_whnf(vint.kind, &ty), + ty: vint.ty, + span: vint.span, + }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: WHNF, + kind: ValueKind::Const(Const::Sort), + ty: None, + span: vint.span, + }, + // Already in WHNF + (WHNF, _) => vint, + } + } + fn normalize_nf(&mut self) { + if let Unevaled = self.form { + self.normalize_whnf(); + } + self.kind.normalize_mut(); + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => Err(TypeError::new(TypeMessage::Sort)), + } + } +} + +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueKind::Var(..) + | ValueKind::Const(_) + | ValueKind::BoolLit(_) + | ValueKind::NaturalLit(_) + | ValueKind::IntegerLit(_) + | ValueKind::DoubleLit(_) => {} + + ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueKind::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueKind::LamClosure { annot, .. } + | ValueKind::PiClosure { annot, .. } => { + annot.normalize_mut(); + } + ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(), + ValueKind::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::UnionType(kts) + | ValueKind::UnionConstructor(_, kts, _) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::UnionLit(_, v, kts, _, _) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueKind::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueKind::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + ValueKind::Thunk(..) => { + unreachable!("Should only normalize_mut values in WHNF") + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + ValueKind::from_builtin_env(b, NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { + ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env)) + } +} + +impl ValueKind { + fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( + &'a self, + visit_val: impl FnMut(&'a V) -> Result, + visit_under_binder: impl for<'b> FnMut( + &'a Binder, + &'b V, + &'a V, + ) -> Result, + ) -> Result, E> { + use visitor::ValueKindVisitor; + visitor::TraverseRefWithBindersVisitor { + visit_val, + visit_under_binder, + } + .visit(self) + } + + fn map_ref_with_special_handling_of_binders<'a, V2>( + &'a self, + mut map_val: impl FnMut(&'a V) -> V2, + mut map_under_binder: impl for<'b> FnMut(&'a Binder, &'b V, &'a V) -> V2, + ) -> ValueKind { + use crate::syntax::trivial_result; + trivial_result(self.traverse_ref_with_special_handling_of_binders( + |x| Ok(map_val(x)), + |l, t, x| Ok(map_under_binder(l, t, x)), + )) + } + + fn map_ref<'a, V2>( + &'a self, + map_val: impl Fn(&'a V) -> V2, + ) -> ValueKind { + self.map_ref_with_special_handling_of_binders(&map_val, |_, _, x| { + map_val(x) + }) + } +} + +impl Thunk { + pub fn new(env: &NzEnv, body: TyExpr) -> Self { + Thunk { + env: env.clone(), + body, + } + } + + pub fn eval(&self) -> Value { + normalize_tyexpr_whnf(&self.body, &self.env) + } + pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + self.eval().to_tyexpr(venv) + } +} + +impl Closure { + pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self { + Closure::Closure { + arg_ty, + env: env.clone(), + body, + } + } + /// New closure that ignores its argument + pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { + Closure::ConstantClosure { + env: env.clone(), + body, + } + } + + pub fn apply(&self, val: Value) -> Value { + match self { + Closure::Closure { env, body, .. } => { + body.eval(&env.insert_value(val)) + } + Closure::ConstantClosure { env, body, .. } => body.eval(env), + } + } + fn apply_var(&self, var: NzVar) -> Value { + match self { + Closure::Closure { arg_ty, .. } => { + let val = Value::from_kind_and_type( + ValueKind::Var(var), + arg_ty.clone(), + ); + self.apply(val) + } + Closure::ConstantClosure { env, body, .. } => body.eval(env), + } + } + + /// Convert this closure to a TyExpr + pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + self.apply_var(NzVar::new(venv.size())) + .to_tyexpr(venv.insert()) + } + /// If the closure variable is free in the closure, return Err. Otherwise, return the value + /// with that free variable remove. + pub fn remove_binder(&self) -> Result { + let v = NzVar::fresh(); + match self { + Closure::Closure { .. } => { + // TODO: handle case where variable is used in closure + // TODO: return information about where the variable is used + Ok(self.apply_var(v)) + } + Closure::ConstantClosure { .. } => { + // Ok: the variable is indeed ignored + Ok(self.apply_var(v)) + } + } + } +} + +/// Compare two values for equality modulo alpha/beta-equivalence. +// TODO: use Rc comparison to shortcut on identical pointers +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.kind() == *other.kind() + } +} +impl std::cmp::Eq for Value {} + +impl std::cmp::PartialEq for Thunk { + fn eq(&self, _other: &Self) -> bool { + unreachable!( + "Trying to compare thunks but we should only compare WHNFs" + ) + } +} +impl std::cmp::Eq for Thunk {} + +impl std::cmp::PartialEq for Closure { + fn eq(&self, other: &Self) -> bool { + let v = NzVar::fresh(); + self.apply_var(v) == other.apply_var(v) + } +} +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(); + if let ValueKind::Const(c) = &vint.kind { + write!(fmt, "{:?}", c) + } else { + let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); + x.field("value", &vint.kind); + if let Some(ty) = vint.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } + } +} diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs new file mode 100644 index 0000000..264b81d --- /dev/null +++ b/dhall/src/semantics/nze/var.rs @@ -0,0 +1,36 @@ +use crate::syntax::Label; + +// Exactly like a Label, but equality returns always true. +// This is so that ValueKind equality is exactly alpha-equivalence. +#[derive(Clone, Eq)] +pub struct Binder { + name: Label, +} + +impl Binder { + pub(crate) fn new(name: Label) -> Self { + Binder { name } + } + pub(crate) fn to_label(&self) -> Label { + self.clone().into() + } +} + +/// Equality up to alpha-equivalence +impl std::cmp::PartialEq for Binder { + fn eq(&self, _other: &Self) -> bool { + true + } +} + +impl std::fmt::Debug for Binder { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "Binder({})", &self.name) + } +} + +impl From for Label { + fn from(x: Binder) -> Label { + x.name + } +} diff --git a/dhall/src/semantics/nze/visitor.rs b/dhall/src/semantics/nze/visitor.rs new file mode 100644 index 0000000..d1a85d8 --- /dev/null +++ b/dhall/src/semantics/nze/visitor.rs @@ -0,0 +1,167 @@ +use std::iter::FromIterator; + +use crate::semantics::{Binder, BuiltinClosure, ValueKind}; +use crate::syntax::Label; + +/// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets +/// us have as much mutability as we can. See the equivalent file in `crate::syntax` for more +/// details. +pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized { + type Error; + + fn visit_val(&mut self, val: &'a V1) -> Result; + fn visit_binder( + mut self, + _label: &'a Binder, + ty: &'a V1, + val: &'a V1, + ) -> Result<(V2, V2), Self::Error> { + Ok((self.visit_val(ty)?, self.visit_val(val)?)) + } + fn visit_vec(&mut self, x: &'a [V1]) -> Result, Self::Error> { + x.iter().map(|e| self.visit_val(e)).collect() + } + fn visit_opt( + &mut self, + x: &'a Option, + ) -> Result, Self::Error> { + Ok(match x { + Some(x) => Some(self.visit_val(x)?), + None => None, + }) + } + fn visit_map( + &mut self, + x: impl IntoIterator, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, V2)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) + .collect() + } + fn visit_optmap( + &mut self, + x: impl IntoIterator)>, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, Option)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) + .collect() + } + + fn visit( + self, + input: &'a ValueKind, + ) -> Result, Self::Error> { + visit_ref(self, input) + } +} + +fn visit_ref<'a, Visitor, V1, V2>( + mut v: Visitor, + input: &'a ValueKind, +) -> Result, Visitor::Error> +where + Visitor: ValueKindVisitor<'a, V1, V2>, +{ + use ValueKind::*; + Ok(match input { + 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(BuiltinClosure { + b, + args, + types, + env, + }) => AppliedBuiltin(BuiltinClosure { + b: *b, + args: v.visit_vec(args)?, + types: v.visit_vec(types)?, + env: env.clone(), + }), + Var(v) => Var(*v), + Const(k) => Const(*k), + BoolLit(b) => BoolLit(*b), + NaturalLit(n) => NaturalLit(*n), + IntegerLit(n) => IntegerLit(*n), + DoubleLit(n) => DoubleLit(*n), + EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_val(t)?), + NEOptionalLit(x) => NEOptionalLit(v.visit_val(x)?), + EmptyListLit(t) => EmptyListLit(v.visit_val(t)?), + NEListLit(xs) => NEListLit(v.visit_vec(xs)?), + RecordType(kts) => RecordType(v.visit_map(kts)?), + RecordLit(kvs) => RecordLit(v.visit_map(kvs)?), + UnionType(kts) => UnionType(v.visit_optmap(kts)?), + UnionConstructor(l, kts, uniont) => UnionConstructor( + l.clone(), + v.visit_optmap(kts)?, + v.visit_val(uniont)?, + ), + UnionLit(l, x, kts, uniont, ctort) => UnionLit( + l.clone(), + v.visit_val(x)?, + v.visit_optmap(kts)?, + v.visit_val(uniont)?, + v.visit_val(ctort)?, + ), + TextLit(ts) => TextLit( + ts.iter() + .map(|t| t.traverse_ref(|e| v.visit_val(e))) + .collect::>()?, + ), + Equivalence(x, y) => Equivalence(v.visit_val(x)?, v.visit_val(y)?), + PartialExpr(e) => PartialExpr(e.traverse_ref(|e| v.visit_val(e))?), + Thunk(th) => Thunk(th.clone()), + }) +} + +pub struct TraverseRefWithBindersVisitor { + pub visit_val: F1, + pub visit_under_binder: F2, +} + +impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> + for TraverseRefWithBindersVisitor +where + V1: 'a, + F1: FnMut(&'a V1) -> Result, + F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result, +{ + type Error = Err; + + fn visit_val(&mut self, val: &'a V1) -> Result { + (self.visit_val)(val) + } + fn visit_binder<'b>( + mut self, + label: &'a Binder, + ty: &'a V1, + val: &'a V1, + ) -> Result<(V2, V2), Self::Error> { + let val = (self.visit_under_binder)(label, ty, val)?; + let ty = (self.visit_val)(ty)?; + Ok((ty, val)) + } +} -- cgit v1.2.3 From 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:04:28 +0000 Subject: Move normalize under nze --- dhall/src/semantics/nze/mod.rs | 2 + dhall/src/semantics/nze/normalize.rs | 507 +++++++++++++++++++++++++++++++++++ dhall/src/semantics/nze/value.rs | 4 +- 3 files changed, 510 insertions(+), 3 deletions(-) create mode 100644 dhall/src/semantics/nze/normalize.rs (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index f367f8f..e3b37cd 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,7 +1,9 @@ pub mod env; +pub mod normalize; pub mod value; pub mod var; pub mod visitor; pub(crate) use env::*; +pub(crate) use normalize::*; pub(crate) use value::*; pub(crate) use var::*; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs new file mode 100644 index 0000000..ea1a25b --- /dev/null +++ b/dhall/src/semantics/nze/normalize.rs @@ -0,0 +1,507 @@ +use std::collections::HashMap; + +use crate::semantics::phase::Normalized; +use crate::semantics::NzEnv; +use crate::semantics::{ + Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; +use crate::syntax::{ + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, +}; + +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { + let f_borrow = f.kind(); + match &*f_borrow { + ValueKind::LamClosure { closure, .. } => { + closure.apply(a).to_whnf_check_type(ty) + } + ValueKind::AppliedBuiltin(closure) => { + closure.apply(a, f.get_type().unwrap(), ty) + } + ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( + l.clone(), + a, + kts.clone(), + uniont.clone(), + f.get_type().unwrap(), + ), + _ => { + drop(f_borrow); + ValueKind::PartialExpr(ExprKind::App(f, a)) + } + } +} + +pub(crate) fn squash_textlit( + elts: impl Iterator>, +) -> Vec> { + use std::mem::replace; + use InterpolatedTextContents::{Expr, Text}; + + fn inner( + elts: impl Iterator>, + crnt_str: &mut String, + ret: &mut Vec>, + ) { + for contents in elts { + match contents { + Text(s) => crnt_str.push_str(&s), + Expr(e) => { + let e_borrow = e.kind(); + match &*e_borrow { + ValueKind::TextLit(elts2) => { + inner(elts2.iter().cloned(), crnt_str, ret) + } + _ => { + drop(e_borrow); + if !crnt_str.is_empty() { + ret.push(Text(replace(crnt_str, String::new()))) + } + ret.push(Expr(e.clone())) + } + } + } + } + } + } + + let mut crnt_str = String::new(); + let mut ret = Vec::new(); + inner(elts, &mut crnt_str, &mut ret); + if !crnt_str.is_empty() { + ret.push(Text(replace(&mut crnt_str, String::new()))) + } + ret +} + +pub(crate) fn merge_maps( + map1: &HashMap, + map2: &HashMap, + mut f: F, +) -> Result, Err> +where + F: FnMut(&K, &V, &V) -> Result, + K: std::hash::Hash + Eq + Clone, + V: Clone, +{ + let mut kvs = HashMap::new(); + for (x, v2) in map2 { + let newv = if let Some(v1) = map1.get(x) { + f(x, v1, v2)? + } else { + v2.clone() + }; + kvs.insert(x.clone(), newv); + } + for (x, v1) in map1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v1.clone()); + } + Ok(kvs) +} + +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueKind(ValueKind), + Value(Value), + ValueRef(&'a Value), + Expr(ExprKind), +} + +fn apply_binop<'a>( + o: BinOp, + x: &'a Value, + y: &'a Value, + ty: &Value, +) -> Option> { + use BinOp::{ + BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, + NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, + RightBiasedRecordMerge, TextAppend, + }; + use ValueKind::{ + BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, + TextLit, + }; + let x_borrow = x.kind(); + let y_borrow = y.kind(); + Some(match (o, &*x_borrow, &*y_borrow) { + (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), + (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)), + (BoolAnd, _, _) if x == y => Ret::ValueRef(x), + (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)), + (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), + (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolOr, _, _) if x == y => Ret::ValueRef(x), + (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), + (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)), + (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), + (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)), + + (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), + (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), + (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { + Ret::ValueKind(NaturalLit(x + y)) + } + (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), + (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), + (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), + (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { + Ret::ValueKind(NaturalLit(x * y)) + } + + (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), + (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind( + NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), + ), + + (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), + (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), + (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( + squash_textlit(x.iter().chain(y.iter()).cloned()), + )), + (TextAppend, TextLit(x), _) => { + use std::iter::once; + let y = InterpolatedTextContents::Expr(y.clone()); + Ret::ValueKind(TextLit(squash_textlit( + x.iter().cloned().chain(once(y)), + ))) + } + (TextAppend, _, TextLit(y)) => { + use std::iter::once; + let x = InterpolatedTextContents::Expr(x.clone()); + Ret::ValueKind(TextLit(squash_textlit( + once(x).chain(y.iter().cloned()), + ))) + } + + (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + Ret::ValueRef(x) + } + (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + Ret::ValueRef(y) + } + (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let mut kvs = kvs2.clone(); + for (x, v) in kvs1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v.clone()); + } + Ret::ValueKind(RecordLit(kvs)) + } + + (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + Ret::ValueRef(x) + } + (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + Ret::ValueRef(y) + } + (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let ty_borrow = ty.kind(); + let kts = match &*ty_borrow { + RecordType(kts) => kts, + _ => unreachable!("Internal type error"), + }; + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { + Ok(Value::from_kind_and_type( + ValueKind::PartialExpr(ExprKind::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + )), + kts.get(k).expect("Internal type error").clone(), + )) + })?; + Ret::ValueKind(RecordLit(kvs)) + } + + (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { + let kts = merge_maps::<_, _, _, !>( + kts_x, + kts_y, + // If the Label exists for both records, then we hit the recursive case. + |_, l: &Value, r: &Value| { + Ok(Value::from_kind_and_type( + ValueKind::PartialExpr(ExprKind::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + )), + ty.clone(), + )) + }, + )?; + Ret::ValueKind(RecordType(kts)) + } + + (Equivalence, _, _) => { + Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) + } + + _ => return None, + }) +} + +pub(crate) fn normalize_one_layer( + expr: ExprKind, + ty: &Value, + env: &NzEnv, +) -> ValueKind { + use ValueKind::{ + BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, + NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, + UnionConstructor, UnionLit, UnionType, + }; + + let ret = match expr { + ExprKind::Import(_) => unreachable!( + "There should remain no imports in a resolved expression" + ), + // Those cases have already been completely handled in the typechecking phase (using + // `RetWhole`), so they won't appear here. + ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) + | ExprKind::Embed(_) + | ExprKind::Var(_) => { + unreachable!("This case should have been handled in typecheck") + } + ExprKind::Annot(x, _) => Ret::Value(x), + ExprKind::Const(c) => Ret::Value(Value::from_const(c)), + ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), + ExprKind::Assert(_) => Ret::Expr(expr), + ExprKind::App(v, a) => Ret::Value(v.app(a)), + ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), + ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), + ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), + ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), + ExprKind::EmptyListLit(t) => { + let arg = match &*t.kind() { + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, + args, + .. + }) if args.len() == 1 => args[0].clone(), + _ => panic!("internal type error"), + }; + Ret::ValueKind(ValueKind::EmptyListLit(arg)) + } + ExprKind::NEListLit(elts) => { + Ret::ValueKind(NEListLit(elts.into_iter().collect())) + } + ExprKind::RecordLit(kvs) => { + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) + } + ExprKind::RecordType(kvs) => { + Ret::ValueKind(RecordType(kvs.into_iter().collect())) + } + ExprKind::UnionType(kvs) => { + Ret::ValueKind(UnionType(kvs.into_iter().collect())) + } + ExprKind::TextLit(elts) => { + use InterpolatedTextContents::Expr; + let elts: Vec<_> = squash_textlit(elts.into_iter()); + // Simplify bare interpolation + if let [Expr(th)] = elts.as_slice() { + Ret::Value(th.clone()) + } else { + Ret::ValueKind(TextLit(elts)) + } + } + ExprKind::BoolIf(ref b, ref e1, ref e2) => { + let b_borrow = b.kind(); + match &*b_borrow { + BoolLit(true) => Ret::ValueRef(e1), + BoolLit(false) => Ret::ValueRef(e2), + _ => { + let e1_borrow = e1.kind(); + let e2_borrow = e2.kind(); + match (&*e1_borrow, &*e2_borrow) { + // Simplify `if b then True else False` + (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), + _ if e1 == e2 => Ret::ValueRef(e1), + _ => { + drop(b_borrow); + drop(e1_borrow); + drop(e2_borrow); + Ret::Expr(expr) + } + } + } + } + } + ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + Some(ret) => ret, + None => Ret::Expr(expr), + }, + + ExprKind::Projection(_, ref ls) if ls.is_empty() => { + Ret::ValueKind(RecordLit(HashMap::new())) + } + ExprKind::Projection(ref v, ref ls) => { + let v_borrow = v.kind(); + match &*v_borrow { + RecordLit(kvs) => Ret::ValueKind(RecordLit( + ls.iter() + .filter_map(|l| { + kvs.get(l).map(|x| (l.clone(), x.clone())) + }) + .collect(), + )), + _ => { + drop(v_borrow); + Ret::Expr(expr) + } + } + } + ExprKind::Field(ref v, ref l) => { + let v_borrow = v.kind(); + match &*v_borrow { + RecordLit(kvs) => match kvs.get(l) { + Some(r) => Ret::Value(r.clone()), + None => { + drop(v_borrow); + Ret::Expr(expr) + } + }, + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), + _ => { + drop(v_borrow); + Ret::Expr(expr) + } + } + } + ExprKind::ProjectionByExpr(_, _) => { + unimplemented!("selection by expression") + } + ExprKind::Completion(_, _) => unimplemented!("record completion"), + + ExprKind::Merge(ref handlers, ref variant, _) => { + let handlers_borrow = handlers.kind(); + let variant_borrow = variant.kind(); + match (&*handlers_borrow, &*variant_borrow) { + (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) + { + Some(h) => Ret::Value(h.clone()), + None => { + drop(handlers_borrow); + drop(variant_borrow); + Ret::Expr(expr) + } + }, + (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { + Some(h) => Ret::Value(h.app(v.clone())), + None => { + drop(handlers_borrow); + drop(variant_borrow); + Ret::Expr(expr) + } + }, + (RecordLit(kvs), EmptyOptionalLit(_)) => { + match kvs.get(&"None".into()) { + Some(h) => Ret::Value(h.clone()), + None => { + drop(handlers_borrow); + drop(variant_borrow); + Ret::Expr(expr) + } + } + } + (RecordLit(kvs), NEOptionalLit(v)) => { + match kvs.get(&"Some".into()) { + Some(h) => Ret::Value(h.app(v.clone())), + None => { + drop(handlers_borrow); + drop(variant_borrow); + Ret::Expr(expr) + } + } + } + _ => { + drop(handlers_borrow); + drop(variant_borrow); + Ret::Expr(expr) + } + } + } + ExprKind::ToMap(_, _) => unimplemented!("toMap"), + }; + + match ret { + Ret::ValueKind(v) => v, + Ret::Value(v) => v.to_whnf_check_type(ty), + Ret::ValueRef(v) => v.to_whnf_check_type(ty), + Ret::Expr(expr) => ValueKind::PartialExpr(expr), + } +} + +/// Normalize a ValueKind into WHNF +pub(crate) fn normalize_whnf( + v: ValueKind, + ty: &Value, +) -> ValueKind { + match v { + ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), + ValueKind::Thunk(th) => th.eval().kind().clone(), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(squash_textlit(elts.into_iter())) + } + // All other cases are already in WHNF + v => v, + } +} + +/// Normalize a TyExpr into WHNF +pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { + 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)) => { + let annot = annot.eval(env); + ValueKind::LamClosure { + binder: Binder::new(binder.clone()), + annot: annot.clone(), + closure: Closure::new(annot, env, body.clone()), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = annot.eval(env); + let closure = Closure::new(annot.clone(), env, body.clone()); + ValueKind::PiClosure { + binder: Binder::new(binder.clone()), + annot, + closure, + } + } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.eval(env); + return body.eval(&env.insert_value(val)); + } + TyExprKind::Expr(e) => { + let e = e.map_ref(|tye| tye.eval(env)); + normalize_one_layer(e, &ty, env) + } + }; + + // dbg!(tye.kind(), env, &kind); + Value::from_kind_and_type_whnf(kind, ty) +} diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 4960076..215c342 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,11 +4,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::visitor; -use crate::semantics::phase::normalize::{ - apply_any, normalize_tyexpr_whnf, normalize_whnf, -}; use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::Binder; +use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ -- cgit v1.2.3 From 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:09:16 +0000 Subject: Move main API to lib.rs --- dhall/src/semantics/nze/normalize.rs | 2 +- dhall/src/semantics/nze/value.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index ea1a25b..6564018 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use crate::semantics::phase::Normalized; use crate::semantics::NzEnv; use crate::semantics::{ Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, @@ -8,6 +7,7 @@ use crate::semantics::{ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, }; +use crate::Normalized; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.kind(); diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 215c342..0a9de6a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,6 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::visitor; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::Binder; use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; @@ -13,6 +12,7 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; +use crate::{Normalized, NormalizedExpr, ToExprOptions}; use self::Form::{Unevaled, WHNF}; -- cgit v1.2.3 From 7062de011eab7954f4bcf78fa1cf970ba91d6a5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:04:16 +0000 Subject: Remove Value visitor It's mostly useful when we can change types, but it's also too constraining if we can, because then we can't enforce complex invariants like the one for TextLit. --- dhall/src/semantics/nze/mod.rs | 1 - dhall/src/semantics/nze/value.rs | 228 ++++++++++++++----------------------- dhall/src/semantics/nze/visitor.rs | 167 --------------------------- 3 files changed, 87 insertions(+), 309 deletions(-) delete mode 100644 dhall/src/semantics/nze/visitor.rs (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index e3b37cd..3d9c5eb 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -2,7 +2,6 @@ pub mod env; pub mod normalize; pub mod value; pub mod var; -pub mod visitor; pub(crate) use env::*; pub(crate) use normalize::*; pub(crate) use value::*; diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 0a9de6a..6ab6fe3 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -3,7 +3,6 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::nze::visitor; use crate::semantics::Binder; use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; @@ -276,62 +275,96 @@ impl Value { } pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + let map_uniontype = |kts: &HashMap>| { + ExprKind::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv))) + }) + .collect(), + ) + }; + let tye = match &*self.kind() { ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), - ValueKind::LamClosure { - binder, - annot, - closure, - } => TyExprKind::Expr(ExprKind::Lam( - binder.to_label(), - annot.to_tyexpr(venv), - closure.to_tyexpr(venv), - )), - ValueKind::PiClosure { - binder, - annot, - closure, - } => TyExprKind::Expr(ExprKind::Pi( - binder.to_label(), - annot.to_tyexpr(venv), - closure.to_tyexpr(venv), - )), ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), - ValueKind::UnionConstructor(l, kts, t) => { - TyExprKind::Expr(ExprKind::Field( - TyExpr::new( - TyExprKind::Expr(ExprKind::UnionType( - kts.into_iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| v.to_tyexpr(venv)), - ) - }) - .collect(), + ValueKind::Thunk(th) => return th.to_tyexpr(venv), + self_kind => TyExprKind::Expr(match self_kind { + ValueKind::Var(..) + | ValueKind::AppliedBuiltin(..) + | ValueKind::Thunk(..) => unreachable!(), + ValueKind::LamClosure { + binder, + annot, + closure, + } => ExprKind::Lam( + binder.to_label(), + annot.to_tyexpr(venv), + closure.to_tyexpr(venv), + ), + ValueKind::PiClosure { + binder, + annot, + closure, + } => ExprKind::Pi( + binder.to_label(), + annot.to_tyexpr(venv), + closure.to_tyexpr(venv), + ), + 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( + Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv), + n.to_tyexpr(venv), + ), + ValueKind::NEOptionalLit(n) => { + ExprKind::SomeLit(n.to_tyexpr(venv)) + } + ValueKind::EmptyListLit(n) => { + ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + Value::from_builtin(Builtin::List).to_tyexpr(venv), + n.to_tyexpr(venv), )), + Some(Value::from_const(Const::Type)), + Span::Artificial, + )) + } + ValueKind::NEListLit(elts) => ExprKind::NEListLit( + elts.iter().map(|v| v.to_tyexpr(venv)).collect(), + ), + ValueKind::TextLit(elts) => ExprKind::TextLit( + elts.iter() + .map(|t| t.map_ref(|v| v.to_tyexpr(venv))) + .collect(), + ), + ValueKind::RecordLit(kvs) => ExprKind::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_tyexpr(venv))) + .collect(), + ), + ValueKind::RecordType(kts) => ExprKind::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_tyexpr(venv))) + .collect(), + ), + ValueKind::UnionType(kts) => map_uniontype(kts), + ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(map_uniontype(kts)), Some(t.clone()), Span::Artificial, ), l.clone(), - )) - } - ValueKind::UnionLit(l, v, kts, uniont, ctort) => { - TyExprKind::Expr(ExprKind::App( + ), + ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( TyExpr::new( TyExprKind::Expr(ExprKind::Field( TyExpr::new( - TyExprKind::Expr(ExprKind::UnionType( - kts.into_iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref() - .map(|v| v.to_tyexpr(venv)), - ) - }) - .collect(), - )), + TyExprKind::Expr(map_uniontype(kts)), Some(uniont.clone()), Span::Artificial, ), @@ -341,61 +374,14 @@ impl Value { Span::Artificial, ), v.to_tyexpr(venv), - )) - } - ValueKind::Thunk(th) => return th.to_tyexpr(venv), - self_kind => { - let self_kind = self_kind.map_ref(|v| v.to_tyexpr(venv)); - let expr = match self_kind { - ValueKind::Var(..) - | ValueKind::LamClosure { .. } - | ValueKind::PiClosure { .. } - | ValueKind::AppliedBuiltin(..) - | ValueKind::UnionConstructor(..) - | ValueKind::UnionLit(..) - | ValueKind::Thunk(..) => unreachable!(), - 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( - Value::from_builtin(Builtin::OptionalNone) - .to_tyexpr(venv), - n, - ), - ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), - ValueKind::EmptyListLit(n) => { - ExprKind::EmptyListLit(TyExpr::new( - TyExprKind::Expr(ExprKind::App( - Value::from_builtin(Builtin::List) - .to_tyexpr(venv), - n, - )), - Some(Value::from_const(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::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::Equivalence(x, y) => ExprKind::BinOp( + BinOp::Equivalence, + x.to_tyexpr(venv), + y.to_tyexpr(venv), + ), + ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)), + }), }; let self_ty = self.as_internal().ty.clone(); @@ -535,46 +521,6 @@ impl ValueKind { } } -impl ValueKind { - fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( - &'a self, - visit_val: impl FnMut(&'a V) -> Result, - visit_under_binder: impl for<'b> FnMut( - &'a Binder, - &'b V, - &'a V, - ) -> Result, - ) -> Result, E> { - use visitor::ValueKindVisitor; - visitor::TraverseRefWithBindersVisitor { - visit_val, - visit_under_binder, - } - .visit(self) - } - - fn map_ref_with_special_handling_of_binders<'a, V2>( - &'a self, - mut map_val: impl FnMut(&'a V) -> V2, - mut map_under_binder: impl for<'b> FnMut(&'a Binder, &'b V, &'a V) -> V2, - ) -> ValueKind { - use crate::syntax::trivial_result; - trivial_result(self.traverse_ref_with_special_handling_of_binders( - |x| Ok(map_val(x)), - |l, t, x| Ok(map_under_binder(l, t, x)), - )) - } - - fn map_ref<'a, V2>( - &'a self, - map_val: impl Fn(&'a V) -> V2, - ) -> ValueKind { - self.map_ref_with_special_handling_of_binders(&map_val, |_, _, x| { - map_val(x) - }) - } -} - impl Thunk { pub fn new(env: &NzEnv, body: TyExpr) -> Self { Thunk { diff --git a/dhall/src/semantics/nze/visitor.rs b/dhall/src/semantics/nze/visitor.rs deleted file mode 100644 index d1a85d8..0000000 --- a/dhall/src/semantics/nze/visitor.rs +++ /dev/null @@ -1,167 +0,0 @@ -use std::iter::FromIterator; - -use crate::semantics::{Binder, BuiltinClosure, ValueKind}; -use crate::syntax::Label; - -/// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets -/// us have as much mutability as we can. See the equivalent file in `crate::syntax` for more -/// details. -pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized { - type Error; - - fn visit_val(&mut self, val: &'a V1) -> Result; - fn visit_binder( - mut self, - _label: &'a Binder, - ty: &'a V1, - val: &'a V1, - ) -> Result<(V2, V2), Self::Error> { - Ok((self.visit_val(ty)?, self.visit_val(val)?)) - } - fn visit_vec(&mut self, x: &'a [V1]) -> Result, Self::Error> { - x.iter().map(|e| self.visit_val(e)).collect() - } - fn visit_opt( - &mut self, - x: &'a Option, - ) -> Result, Self::Error> { - Ok(match x { - Some(x) => Some(self.visit_val(x)?), - None => None, - }) - } - fn visit_map( - &mut self, - x: impl IntoIterator, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, V2)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) - .collect() - } - fn visit_optmap( - &mut self, - x: impl IntoIterator)>, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, Option)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) - .collect() - } - - fn visit( - self, - input: &'a ValueKind, - ) -> Result, Self::Error> { - visit_ref(self, input) - } -} - -fn visit_ref<'a, Visitor, V1, V2>( - mut v: Visitor, - input: &'a ValueKind, -) -> Result, Visitor::Error> -where - Visitor: ValueKindVisitor<'a, V1, V2>, -{ - use ValueKind::*; - Ok(match input { - 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(BuiltinClosure { - b, - args, - types, - env, - }) => AppliedBuiltin(BuiltinClosure { - b: *b, - args: v.visit_vec(args)?, - types: v.visit_vec(types)?, - env: env.clone(), - }), - Var(v) => Var(*v), - Const(k) => Const(*k), - BoolLit(b) => BoolLit(*b), - NaturalLit(n) => NaturalLit(*n), - IntegerLit(n) => IntegerLit(*n), - DoubleLit(n) => DoubleLit(*n), - EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_val(t)?), - NEOptionalLit(x) => NEOptionalLit(v.visit_val(x)?), - EmptyListLit(t) => EmptyListLit(v.visit_val(t)?), - NEListLit(xs) => NEListLit(v.visit_vec(xs)?), - RecordType(kts) => RecordType(v.visit_map(kts)?), - RecordLit(kvs) => RecordLit(v.visit_map(kvs)?), - UnionType(kts) => UnionType(v.visit_optmap(kts)?), - UnionConstructor(l, kts, uniont) => UnionConstructor( - l.clone(), - v.visit_optmap(kts)?, - v.visit_val(uniont)?, - ), - UnionLit(l, x, kts, uniont, ctort) => UnionLit( - l.clone(), - v.visit_val(x)?, - v.visit_optmap(kts)?, - v.visit_val(uniont)?, - v.visit_val(ctort)?, - ), - TextLit(ts) => TextLit( - ts.iter() - .map(|t| t.traverse_ref(|e| v.visit_val(e))) - .collect::>()?, - ), - Equivalence(x, y) => Equivalence(v.visit_val(x)?, v.visit_val(y)?), - PartialExpr(e) => PartialExpr(e.traverse_ref(|e| v.visit_val(e))?), - Thunk(th) => Thunk(th.clone()), - }) -} - -pub struct TraverseRefWithBindersVisitor { - pub visit_val: F1, - pub visit_under_binder: F2, -} - -impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> - for TraverseRefWithBindersVisitor -where - V1: 'a, - F1: FnMut(&'a V1) -> Result, - F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result, -{ - type Error = Err; - - fn visit_val(&mut self, val: &'a V1) -> Result { - (self.visit_val)(val) - } - fn visit_binder<'b>( - mut self, - label: &'a Binder, - ty: &'a V1, - val: &'a V1, - ) -> Result<(V2, V2), Self::Error> { - let val = (self.visit_under_binder)(label, ty, val)?; - let ty = (self.visit_val)(ty)?; - Ok((ty, val)) - } -} -- cgit v1.2.3 From 0749482ad2ab9340fb45a2fe2997d2ea04516d75 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:06:53 +0000 Subject: Remove type parameter from ValueKind --- dhall/src/semantics/nze/normalize.rs | 11 ++++------- dhall/src/semantics/nze/value.rs | 27 ++++++++++++--------------- 2 files changed, 16 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 6564018..90036e3 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -9,7 +9,7 @@ use crate::syntax::{ }; use crate::Normalized; -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.kind(); match &*f_borrow { ValueKind::LamClosure { closure, .. } => { @@ -102,7 +102,7 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), Expr(ExprKind), @@ -255,7 +255,7 @@ pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, env: &NzEnv, -) -> ValueKind { +) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, @@ -450,10 +450,7 @@ pub(crate) fn normalize_one_layer( } /// Normalize a ValueKind into WHNF -pub(crate) fn normalize_whnf( - v: ValueKind, - ty: &Value, -) -> ValueKind { +pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { match v { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 6ab6fe3..8fad911 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -28,7 +28,7 @@ pub(crate) struct Value(Rc>); #[derive(Debug)] struct ValueInternal { form: Form, - kind: ValueKind, + kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -68,7 +68,7 @@ pub(crate) enum Closure { } #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { +pub(crate) enum ValueKind { /// Closures LamClosure { binder: Binder, @@ -112,7 +112,7 @@ pub(crate) enum ValueKind { } impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { + fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, kind, @@ -139,13 +139,10 @@ impl Value { } .into_value() } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { Value::new(v, Unevaled, t, Span::Artificial) } - pub(crate) fn from_kind_and_type_whnf( - v: ValueKind, - t: Value, - ) -> Value { + pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { Value::new(v, WHNF, t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { @@ -189,7 +186,7 @@ impl Value { /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. - pub(crate) fn kind(&self) -> Ref> { + pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_kind) } @@ -202,11 +199,11 @@ impl Value { self.to_tyexpr_noenv().to_expr(opts) } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { + pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.kind().clone() } /// Before discarding type information, check that it matches the expected return type. - pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { self.check_type(ty); self.to_whnf_ignore_type() } @@ -397,7 +394,7 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } - fn as_kind(&self) -> &ValueKind { + fn as_kind(&self) -> &ValueKind { &self.kind } @@ -442,7 +439,7 @@ impl ValueInternal { } } -impl ValueKind { +impl ValueKind { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_kind_and_type(self, t) } @@ -513,10 +510,10 @@ impl ValueKind { } } - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { ValueKind::from_builtin_env(b, NzEnv::new()) } - pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env)) } } -- cgit v1.2.3 From dc01ef2030e1177e4f247f4ddc0a3f69241d5cfc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:32:22 +0000 Subject: Factor out text literals in Value This allows encapsulating invariants properly and reducing clutter --- dhall/src/semantics/nze/normalize.rs | 52 +++++++++++-------------- dhall/src/semantics/nze/value.rs | 74 +++++++++++++++++++++++++++++++----- 2 files changed, 87 insertions(+), 39 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 90036e3..89424e9 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -2,7 +2,8 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, + Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, + ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, @@ -121,7 +122,6 @@ fn apply_binop<'a>( }; use ValueKind::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, }; let x_borrow = x.kind(); let y_borrow = y.kind(); @@ -164,25 +164,21 @@ fn apply_binop<'a>( NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), ), - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueKind(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueKind(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) + (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => { + Ret::ValueRef(y) + } + (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => { + Ret::ValueRef(x) + } + (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => { + Ret::ValueKind(ValueKind::TextLit(x.concat(y))) } + (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind( + ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))), + ), + (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind( + ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)), + ), (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { Ret::ValueRef(x) @@ -258,8 +254,8 @@ pub(crate) fn normalize_one_layer( ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, - UnionConstructor, UnionLit, UnionType, + NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor, + UnionLit, UnionType, }; let ret = match expr { @@ -309,13 +305,12 @@ pub(crate) fn normalize_one_layer( Ret::ValueKind(UnionType(kvs.into_iter().collect())) } ExprKind::TextLit(elts) => { - use InterpolatedTextContents::Expr; - let elts: Vec<_> = squash_textlit(elts.into_iter()); + let tlit = TextLit::new(elts.into_iter()); // Simplify bare interpolation - if let [Expr(th)] = elts.as_slice() { - Ret::Value(th.clone()) + if let Some(v) = tlit.as_single_expr() { + Ret::Value(v.clone()) } else { - Ret::ValueKind(TextLit(elts)) + Ret::ValueKind(ValueKind::TextLit(tlit)) } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { @@ -455,9 +450,6 @@ pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::Thunk(th) => th.eval().kind().clone(), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(squash_textlit(elts.into_iter())) - } // All other cases are already in WHNF v => v, } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 8fad911..06d8df8 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::Binder; -use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; +use crate::semantics::{ + apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit, +}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ @@ -67,6 +69,12 @@ pub(crate) enum Closure { ConstantClosure { env: NzEnv, body: TyExpr }, } +/// A text literal with interpolations. +// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous +// text values must be merged. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct TextLit(Vec>); + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures @@ -101,9 +109,7 @@ pub(crate) enum ValueKind { UnionConstructor(Label, HashMap>, Value), // Also keep the type of the uniontype and the constructor around UnionLit(Label, Value, HashMap>, Value, Value), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), + TextLit(TextLit), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind), @@ -492,11 +498,7 @@ impl ValueKind { x.normalize_mut(); } } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } + ValueKind::TextLit(tlit) => tlit.normalize_mut(), ValueKind::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); @@ -594,6 +596,60 @@ impl Closure { } } +impl TextLit { + pub fn new( + elts: impl Iterator>, + ) -> Self { + TextLit(squash_textlit(elts)) + } + pub fn interpolate(v: Value) -> TextLit { + TextLit(vec![InterpolatedTextContents::Expr(v)]) + } + pub fn from_text(s: String) -> TextLit { + TextLit(vec![InterpolatedTextContents::Text(s)]) + } + + pub fn concat(&self, other: &TextLit) -> TextLit { + TextLit::new(self.iter().chain(other.iter()).cloned()) + } + pub fn is_empty(&self) -> bool { + self.0.is_empty() + } + /// If the literal consists of only one interpolation and not text, return the interpolated + /// value. + pub fn as_single_expr(&self) -> Option<&Value> { + use InterpolatedTextContents::Expr; + if let [Expr(v)] = self.0.as_slice() { + Some(v) + } else { + None + } + } + /// If there are no interpolations, return the corresponding text value. + pub fn as_text(&self) -> Option { + use InterpolatedTextContents::Text; + if self.is_empty() { + Some(String::new()) + } else if let [Text(s)] = self.0.as_slice() { + Some(s.clone()) + } else { + None + } + } + pub fn iter( + &self, + ) -> impl Iterator> { + self.0.iter() + } + /// Normalize the contained values. This does not break the invariant because we have already + /// ensured that no contained values normalize to a TextLit. + pub fn normalize_mut(&mut self) { + for x in self.0.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } +} + /// Compare two values for equality modulo alpha/beta-equivalence. // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { -- cgit v1.2.3 From 3c4895a06a4910184203d8531e7ab318db71fb15 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:13:37 +0000 Subject: Prepare ValueInternal with new `Form`s --- dhall/src/semantics/nze/value.rs | 103 +++++++++++++++++++-------------------- 1 file changed, 50 insertions(+), 53 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 06d8df8..31acb11 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -30,23 +30,22 @@ pub(crate) struct Value(Rc>); #[derive(Debug)] struct ValueInternal { form: Form, - kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, span: Span, } -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone)] pub(crate) enum Form { /// No constraints; expression may not be normalized at all. - Unevaled, + Unevaled(ValueKind), /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may /// not be normalized. This means that the first constructor of the contained ValueKind is the first /// constructor of the final Normal Form (NF). /// When all the Values in a ValueKind are in WHNF, and recursively so, then the /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so /// if we have the first constructor of the NF at all levels, we actually have the NF. - WHNF, + WHNF(ValueKind), } /// An unevaluated subexpression @@ -118,10 +117,9 @@ pub(crate) enum ValueKind { } impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { + fn new(form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, - kind, ty: Some(ty), span, } @@ -129,8 +127,7 @@ impl Value { } pub(crate) fn const_sort() -> Value { ValueInternal { - form: WHNF, - kind: ValueKind::Const(Const::Sort), + form: WHNF(ValueKind::Const(Const::Sort)), ty: None, span: Span::Artificial, } @@ -138,18 +135,17 @@ impl Value { } pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { - form: Unevaled, - kind: ValueKind::Thunk(Thunk::new(env, tye.clone())), + form: Unevaled(ValueKind::Thunk(Thunk::new(env, tye.clone()))), ty: tye.get_type().ok(), span: tye.span().clone(), } .into_value() } pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(v, Unevaled, t, Span::Artificial) + Value::new(Unevaled(v), t, Span::Artificial) } pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(v, WHNF, t, Span::Artificial) + Value::new(WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -194,7 +190,10 @@ impl Value { /// panics. pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); - Ref::map(self.as_internal(), ValueInternal::as_kind) + Ref::map(self.as_internal(), |vint| match &vint.form { + Unevaled(..) => unreachable!(), + WHNF(k) => k, + }) } /// Converts a value back to the corresponding AST expression. @@ -232,12 +231,12 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Unevaled => { + Unevaled(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already in WHNF - WHNF => {} + WHNF(_) => {} } } pub(crate) fn normalize_nf(&self) { @@ -400,41 +399,29 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } - fn as_kind(&self) -> &ValueKind { - &self.kind - } fn normalize_whnf(&mut self) { - let dummy = ValueInternal { - form: Unevaled, - kind: ValueKind::Const(Const::Type), - ty: None, - span: Span::Artificial, - }; - let vint = std::mem::replace(self, dummy); - *self = match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - kind: normalize_whnf(vint.kind, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: WHNF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: vint.span, - }, + use std::mem::replace; + let dummy = Unevaled(ValueKind::Const(Const::Type)); + self.form = match replace(&mut self.form, dummy) { + Unevaled(kind) => { + WHNF(match &self.ty { + Some(ty) => normalize_whnf(kind, &ty), + // `value` is `Sort` + None => ValueKind::Const(Const::Sort), + }) + } // Already in WHNF - (WHNF, _) => vint, - } + form @ WHNF(_) => form, + }; } fn normalize_nf(&mut self) { - if let Unevaled = self.form { + if let Unevaled(_) = self.form { self.normalize_whnf(); } - self.kind.normalize_mut(); + match &mut self.form { + Unevaled(k) | WHNF(k) => k.normalize_mut(), + } } fn get_type(&self) -> Result<&Value, TypeError> { @@ -679,17 +666,27 @@ 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(); - if let ValueKind::Const(c) = &vint.kind { - write!(fmt, "{:?}", c) - } else { - let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); - x.field("value", &vint.kind); - if let Some(ty) = vint.ty.as_ref() { - x.field("type", &ty); - } else { - x.field("type", &None::<()>); + let mut x = match &vint.form { + WHNF(kind) => { + if let ValueKind::Const(c) = kind { + return write!(fmt, "{:?}", c); + } else { + let mut x = fmt.debug_struct(&format!("Value@WHNF")); + x.field("kind", kind); + x + } } - x.finish() + Unevaled(kind) => { + let mut x = fmt.debug_struct(&format!("Value@Unevaled")); + x.field("kind", kind); + x + } + }; + if let Some(ty) = vint.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); } + x.finish() } } -- cgit v1.2.3 From 40336a928dfc3d1f96273d39ba564334b1719344 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:27:33 +0000 Subject: Move Thunk value into ValueInternal --- dhall/src/semantics/nze/normalize.rs | 1 - dhall/src/semantics/nze/value.rs | 66 +++++++++++++++++------------------- 2 files changed, 32 insertions(+), 35 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 89424e9..16c886e 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -449,7 +449,6 @@ pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { match v { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), - ValueKind::Thunk(th) => th.eval().kind().clone(), // All other cases are already in WHNF v => v, } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 31acb11..8ae0939 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -15,8 +15,6 @@ use crate::syntax::{ }; use crate::{Normalized, NormalizedExpr, ToExprOptions}; -use self::Form::{Unevaled, WHNF}; - /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a RefCell to share computation. /// Can optionally store a type from typechecking to preserve type information. @@ -37,6 +35,7 @@ struct ValueInternal { #[derive(Debug, Clone)] pub(crate) enum Form { + Thunk(Thunk), /// No constraints; expression may not be normalized at all. Unevaled(ValueKind), /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -112,8 +111,6 @@ pub(crate) enum ValueKind { Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind), - // Invariant: absent in whnf - Thunk(Thunk), } impl Value { @@ -127,7 +124,7 @@ impl Value { } pub(crate) fn const_sort() -> Value { ValueInternal { - form: WHNF(ValueKind::Const(Const::Sort)), + form: Form::WHNF(ValueKind::Const(Const::Sort)), ty: None, span: Span::Artificial, } @@ -135,17 +132,17 @@ impl Value { } pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { - form: Unevaled(ValueKind::Thunk(Thunk::new(env, tye.clone()))), + form: Form::Thunk(Thunk::new(env, tye.clone())), ty: tye.get_type().ok(), span: tye.span().clone(), } .into_value() } pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(Unevaled(v), t, Span::Artificial) + Value::new(Form::Unevaled(v), t, Span::Artificial) } pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(WHNF(v), t, Span::Artificial) + Value::new(Form::WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -191,8 +188,8 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), |vint| match &vint.form { - Unevaled(..) => unreachable!(), - WHNF(k) => k, + Form::Thunk(..) | Form::Unevaled(..) => unreachable!(), + Form::WHNF(k) => k, }) } @@ -231,12 +228,12 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Unevaled(_) => { + Form::Thunk(..) | Form::Unevaled(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already in WHNF - WHNF(_) => {} + Form::WHNF(_) => {} } } pub(crate) fn normalize_nf(&self) { @@ -290,11 +287,10 @@ impl Value { let tye = match &*self.kind() { ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), - ValueKind::Thunk(th) => return th.to_tyexpr(venv), self_kind => TyExprKind::Expr(match self_kind { - ValueKind::Var(..) - | ValueKind::AppliedBuiltin(..) - | ValueKind::Thunk(..) => unreachable!(), + ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { + unreachable!() + } ValueKind::LamClosure { binder, annot, @@ -402,25 +398,27 @@ impl ValueInternal { fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Unevaled(ValueKind::Const(Const::Type)); + let dummy = Form::Unevaled(ValueKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { - Unevaled(kind) => { - WHNF(match &self.ty { + Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), + Form::Unevaled(kind) => { + Form::WHNF(match &self.ty { Some(ty) => normalize_whnf(kind, &ty), // `value` is `Sort` None => ValueKind::Const(Const::Sort), }) } // Already in WHNF - form @ WHNF(_) => form, + form @ Form::WHNF(_) => form, }; } fn normalize_nf(&mut self) { - if let Unevaled(_) = self.form { + if let Form::Thunk(..) | Form::Unevaled(_) = self.form { self.normalize_whnf(); } match &mut self.form { - Unevaled(k) | WHNF(k) => k.normalize_mut(), + Form::Thunk(..) | Form::Unevaled(_) => unreachable!(), + Form::WHNF(k) => k.normalize_mut(), } } @@ -493,9 +491,6 @@ impl ValueKind { ValueKind::PartialExpr(e) => { e.map_mut(Value::normalize_mut); } - ValueKind::Thunk(..) => { - unreachable!("Should only normalize_mut values in WHNF") - } } } @@ -515,12 +510,10 @@ impl Thunk { } } + // TODO: maybe return a ValueKind ? pub fn eval(&self) -> Value { normalize_tyexpr_whnf(&self.body, &self.env) } - pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { - self.eval().to_tyexpr(venv) - } } impl Closure { @@ -667,7 +660,17 @@ impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); let mut x = match &vint.form { - WHNF(kind) => { + Form::Thunk(th) => { + let mut x = fmt.debug_struct(&format!("Value@Thunk")); + x.field("thunk", th); + x + } + Form::Unevaled(kind) => { + let mut x = fmt.debug_struct(&format!("Value@Unevaled")); + x.field("kind", kind); + x + } + Form::WHNF(kind) => { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); } else { @@ -676,11 +679,6 @@ impl std::fmt::Debug for Value { x } } - Unevaled(kind) => { - let mut x = fmt.debug_struct(&format!("Value@Unevaled")); - x.field("kind", kind); - x - } }; if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); -- cgit v1.2.3 From 673a580e11d31356bec25d73213b283685fd6ea3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:49:03 +0000 Subject: Clarify normalization to ensure we only nze once --- dhall/src/semantics/nze/env.rs | 2 +- dhall/src/semantics/nze/normalize.rs | 25 ++++-------- dhall/src/semantics/nze/value.rs | 79 ++++++++++++++++++++---------------- 3 files changed, 52 insertions(+), 54 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index a083076..073886e 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -62,7 +62,7 @@ impl NzEnv { 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( + NzEnvItem::Kept(ty) => Value::from_kind_and_type( ValueKind::Var(NzVar::new(idx)), ty.clone(), ), diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 16c886e..7632d12 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -208,12 +208,12 @@ fn apply_binop<'a>( _ => unreachable!("Internal type error"), }; let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprKind::BinOp( + Ok(Value::from_partial_expr( + ExprKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )), + ), kts.get(k).expect("Internal type error").clone(), )) })?; @@ -226,12 +226,12 @@ fn apply_binop<'a>( kts_y, // If the Label exists for both records, then we hit the recursive case. |_, l: &Value, r: &Value| { - Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprKind::BinOp( + Ok(Value::from_partial_expr( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), - )), + ), ty.clone(), )) }, @@ -444,16 +444,6 @@ pub(crate) fn normalize_one_layer( } } -/// Normalize a ValueKind into WHNF -pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { - match v { - ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), - // All other cases are already in WHNF - v => v, - } -} - /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let ty = match tye.get_type() { @@ -490,6 +480,5 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } }; - // dbg!(tye.kind(), env, &kind); - Value::from_kind_and_type_whnf(kind, ty) + Value::from_kind_and_type(kind, ty) } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 8ae0939..108dc9c 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::Binder; use crate::semantics::{ - apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit, + apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, }; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; @@ -16,34 +16,30 @@ use crate::syntax::{ use crate::{Normalized, NormalizedExpr, ToExprOptions}; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation -/// automatically. Uses a RefCell to share computation. -/// Can optionally store a type from typechecking to preserve type information. -/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence +/// automatically. Uses a Rc to share computation. +/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence /// (renaming of bound variables) and beta-equivalence (normalization). It will recursively /// normalize as needed. #[derive(Clone)] pub(crate) struct Value(Rc>); -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form #[derive(Debug)] struct ValueInternal { form: Form, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) + /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, } +/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as +/// explained in the doc for `ValueKind`. #[derive(Debug, Clone)] pub(crate) enum Form { + /// A totally unnormalized value. Thunk(Thunk), - /// No constraints; expression may not be normalized at all. - Unevaled(ValueKind), - /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may - /// not be normalized. This means that the first constructor of the contained ValueKind is the first - /// constructor of the final Normal Form (NF). - /// When all the Values in a ValueKind are in WHNF, and recursively so, then the - /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so - /// if we have the first constructor of the NF at all levels, we actually have the NF. + /// A partially normalized value that may need to go through `normalize_one_layer`. + PartialExpr(ExprKind), + /// A value in WHNF. WHNF(ValueKind), } @@ -73,6 +69,13 @@ pub(crate) enum Closure { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct TextLit(Vec>); +/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is +/// normalized up to the first constructor, but subexpressions may not be fully normalized. +/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in +/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so +/// if we have the first constructor of the NF at all levels, we actually have the NF. +/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and +/// we only need to recursively normalize its sub-`Value`s to get to the NF. #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures @@ -86,7 +89,6 @@ pub(crate) enum ValueKind { annot: Value, closure: Closure, }, - // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(BuiltinClosure), Var(NzVar), @@ -109,7 +111,7 @@ pub(crate) enum ValueKind { UnionLit(Label, Value, HashMap>, Value, Value), TextLit(TextLit), Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. + /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? PartialExpr(ExprKind), } @@ -130,6 +132,7 @@ impl Value { } .into_value() } + /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal { form: Form::Thunk(Thunk::new(env, tye.clone())), @@ -138,10 +141,15 @@ impl Value { } .into_value() } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(Form::Unevaled(v), t, Span::Artificial) + /// Construct a Value from a partially normalized expression that's not in WHNF. + pub(crate) fn from_partial_expr( + e: ExprKind, + t: Value, + ) -> Value { + Value::new(Form::PartialExpr(e), t, Span::Artificial) } - pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { + /// Make a Value from a ValueKind + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { Value::new(Form::WHNF(v), t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { @@ -188,7 +196,7 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_internal(), |vint| match &vint.form { - Form::Thunk(..) | Form::Unevaled(..) => unreachable!(), + Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), Form::WHNF(k) => k, }) } @@ -228,7 +236,7 @@ impl Value { pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { - Form::Thunk(..) | Form::Unevaled(_) => { + Form::Thunk(..) | Form::PartialExpr(_) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } @@ -248,10 +256,7 @@ impl Value { } _ => unreachable!("Internal type error"), }; - Value::from_kind_and_type_whnf( - apply_any(self.clone(), v, &body_t), - body_t, - ) + Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t) } /// In debug mode, panic if the provided type doesn't match the value's type. @@ -398,12 +403,13 @@ impl ValueInternal { fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Form::Unevaled(ValueKind::Const(Const::Type)); + let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), - Form::Unevaled(kind) => { + Form::PartialExpr(e) => { Form::WHNF(match &self.ty { - Some(ty) => normalize_whnf(kind, &ty), + // TODO: env + Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), // `value` is `Sort` None => ValueKind::Const(Const::Sort), }) @@ -413,11 +419,11 @@ impl ValueInternal { }; } fn normalize_nf(&mut self) { - if let Form::Thunk(..) | Form::Unevaled(_) = self.form { + if let Form::Thunk(..) | Form::PartialExpr(_) = self.form { self.normalize_whnf(); } match &mut self.form { - Form::Thunk(..) | Form::Unevaled(_) => unreachable!(), + Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } @@ -451,9 +457,10 @@ impl ValueKind { ValueKind::NEOptionalLit(th) => { th.normalize_mut(); } - ValueKind::LamClosure { annot, .. } - | ValueKind::PiClosure { annot, .. } => { + ValueKind::LamClosure { annot, closure, .. } + | ValueKind::PiClosure { annot, closure, .. } => { annot.normalize_mut(); + closure.normalize_mut(); } ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(), ValueKind::NEListLit(elts) => { @@ -553,6 +560,8 @@ impl Closure { } } + // TODO: somehow normalize the body. Might require to pass an env. + pub fn normalize_mut(&mut self) {} /// Convert this closure to a TyExpr pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { self.apply_var(NzVar::new(venv.size())) @@ -665,9 +674,9 @@ impl std::fmt::Debug for Value { x.field("thunk", th); x } - Form::Unevaled(kind) => { - let mut x = fmt.debug_struct(&format!("Value@Unevaled")); - x.field("kind", kind); + Form::PartialExpr(e) => { + let mut x = fmt.debug_struct(&format!("Value@PartialExpr")); + x.field("expr", e); x } Form::WHNF(kind) => { -- cgit v1.2.3 From d8de45763037937b5c2dedbe5f7bb95a4e7bc7cd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:56:31 +0000 Subject: Avoid unnecessary allocations of `Value`s --- dhall/src/semantics/nze/env.rs | 16 ++++++++++------ dhall/src/semantics/nze/normalize.rs | 21 +++++++++------------ dhall/src/semantics/nze/value.rs | 6 ++---- 3 files changed, 21 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 073886e..0b22a8b 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -59,14 +59,18 @@ impl NzEnv { env.items.push(NzEnvItem::Replaced(e)); env } - pub fn lookup_val(&self, var: &AlphaVar) -> Value { + pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => Value::from_kind_and_type( - ValueKind::Var(NzVar::new(idx)), - ty.clone(), - ), - NzEnvItem::Replaced(x) => x.clone(), + NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), + NzEnvItem::Replaced(x) => x.kind().clone(), + } + } + pub fn lookup_ty(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => ty.clone(), + NzEnvItem::Replaced(x) => x.get_type().unwrap(), } } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 7632d12..e677f78 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -445,14 +445,9 @@ pub(crate) fn normalize_one_layer( } /// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - 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), +pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { + match tye.kind() { + TyExprKind::Var(var) => env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); ValueKind::LamClosure { @@ -472,13 +467,15 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - return body.eval(&env.insert_value(val)); + body.eval(&env.insert_value(val)).kind().clone() } TyExprKind::Expr(e) => { + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return ValueKind::Const(Const::Sort), + }; let e = e.map_ref(|tye| tye.eval(env)); normalize_one_layer(e, &ty, env) } - }; - - Value::from_kind_and_type(kind, ty) + } } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 108dc9c..ff0ca42 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -405,7 +405,7 @@ impl ValueInternal { use std::mem::replace; let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); self.form = match replace(&mut self.form, dummy) { - Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()), + Form::Thunk(th) => Form::WHNF(th.eval()), Form::PartialExpr(e) => { Form::WHNF(match &self.ty { // TODO: env @@ -516,9 +516,7 @@ impl Thunk { body, } } - - // TODO: maybe return a ValueKind ? - pub fn eval(&self) -> Value { + pub fn eval(&self) -> ValueKind { normalize_tyexpr_whnf(&self.body, &self.env) } } -- cgit v1.2.3 From b79a9b81a803794a7a86d953ced24f0d3e2fd212 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 20:23:06 +0000 Subject: Only the Form must be in a RefCell --- dhall/src/semantics/nze/value.rs | 128 ++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 61 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index ff0ca42..d737a0f 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,4 +1,4 @@ -use std::cell::{Ref, RefCell, RefMut}; +use std::cell::{Ref, RefCell}; use std::collections::HashMap; use std::rc::Rc; @@ -21,11 +21,11 @@ use crate::{Normalized, NormalizedExpr, ToExprOptions}; /// (renaming of bound variables) and beta-equivalence (normalization). It will recursively /// normalize as needed. #[derive(Clone)] -pub(crate) struct Value(Rc>); +pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - form: Form, + form: RefCell
, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -117,28 +117,23 @@ pub(crate) enum ValueKind { impl Value { fn new(form: Form, ty: Value, span: Span) -> Value { - ValueInternal { - form, - ty: Some(ty), - span, - } - .into_value() + ValueInternal::new(form, Some(ty), span).into_value() } pub(crate) fn const_sort() -> Value { - ValueInternal { - form: Form::WHNF(ValueKind::Const(Const::Sort)), - ty: None, - span: Span::Artificial, - } + ValueInternal::new( + Form::WHNF(ValueKind::Const(Const::Sort)), + None, + Span::Artificial, + ) .into_value() } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { - ValueInternal { - form: Form::Thunk(Thunk::new(env, tye.clone())), - ty: tye.get_type().ok(), - span: tye.span().clone(), - } + ValueInternal::new( + Form::Thunk(Thunk::new(env, tye.clone())), + tye.get_type().ok(), + tye.span().clone(), + ) .into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. @@ -181,21 +176,18 @@ impl Value { } } pub(crate) fn span(&self) -> Span { - self.as_internal().span.clone() + self.0.span.clone() } - fn as_internal(&self) -> Ref { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut { - self.0.borrow_mut() + fn as_form(&self) -> Ref { + self.0.form.borrow() } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); - Ref::map(self.as_internal(), |vint| match &vint.form { + Ref::map(self.as_form(), |form| match form { Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), Form::WHNF(k) => k, }) @@ -219,33 +211,25 @@ impl Value { } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { + fn mutate_form(&mut self, f: impl FnOnce(&mut Form, &Option)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(refcell) => f(RefCell::get_mut(refcell)), + Some(vint) => f(RefCell::get_mut(&mut vint.form), &vint.ty), // Otherwise mutate through the refcell - None => f(&mut self.as_internal_mut()), + None => f(&mut self.0.form.borrow_mut(), &self.0.ty), } } /// Normalizes contents to normal form; faster than `normalize_nf` if /// no one else shares this. pub(crate) fn normalize_mut(&mut self) { - self.mutate_internal(|vint| vint.normalize_nf()) + self.mutate_form(|form, ty| form.normalize_nf(ty)) } pub(crate) fn normalize_whnf(&self) { - let borrow = self.as_internal(); - match borrow.form { - Form::Thunk(..) | Form::PartialExpr(_) => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already in WHNF - Form::WHNF(_) => {} - } + self.0.normalize_whnf() } pub(crate) fn normalize_nf(&self) { - self.as_internal_mut().normalize_nf(); + self.0.normalize_nf() } pub(crate) fn app(&self, v: Value) -> Value { @@ -270,7 +254,7 @@ impl Value { // ); } pub(crate) fn get_type(&self) -> Result { - Ok(self.as_internal().get_type()?.clone()) + Ok(self.0.get_type()?.clone()) } /// When we know the value isn't `Sort`, this gets the type directly pub(crate) fn get_type_not_sort(&self) -> Value { @@ -387,9 +371,7 @@ impl Value { }), }; - let self_ty = self.as_internal().ty.clone(); - let self_span = self.as_internal().span.clone(); - TyExpr::new(tye, self_ty, self_span) + TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone()) } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr(VarEnv::new()) @@ -397,17 +379,48 @@ impl Value { } impl ValueInternal { + fn new(form: Form, ty: Option, span: Span) -> Self { + ValueInternal { + form: RefCell::new(form), + ty, + span, + } + } fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) + Value(Rc::new(self)) } - fn normalize_whnf(&mut self) { + fn normalize_whnf(&self) { + if !self.form.borrow().is_whnf() { + self.form.borrow_mut().normalize_whnf(&self.ty) + } + } + fn normalize_nf(&self) { + self.form.borrow_mut().normalize_nf(&self.ty) + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => Err(TypeError::new(TypeMessage::Sort)), + } + } +} + +impl Form { + fn is_whnf(&self) -> bool { + match self { + Form::Thunk(..) | Form::PartialExpr(..) => false, + Form::WHNF(..) => true, + } + } + fn normalize_whnf(&mut self, ty: &Option) { use std::mem::replace; let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); - self.form = match replace(&mut self.form, dummy) { + *self = match replace(self, dummy) { Form::Thunk(th) => Form::WHNF(th.eval()), Form::PartialExpr(e) => { - Form::WHNF(match &self.ty { + Form::WHNF(match ty { // TODO: env Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), // `value` is `Sort` @@ -418,22 +431,15 @@ impl ValueInternal { form @ Form::WHNF(_) => form, }; } - fn normalize_nf(&mut self) { - if let Form::Thunk(..) | Form::PartialExpr(_) = self.form { - self.normalize_whnf(); + fn normalize_nf(&mut self, ty: &Option) { + if !self.is_whnf() { + self.normalize_whnf(ty); } - match &mut self.form { + match self { Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => Err(TypeError::new(TypeMessage::Sort)), - } - } } impl ValueKind { @@ -665,8 +671,8 @@ 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(); - let mut x = match &vint.form { + let vint: &ValueInternal = &self.0; + let mut x = match &*vint.form.borrow() { Form::Thunk(th) => { let mut x = fmt.debug_struct(&format!("Value@Thunk")); x.field("thunk", th); -- cgit v1.2.3 From a87b22da10aa20cef939d3c3c7b56710a1f78c2c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 20:36:10 +0000 Subject: Move Form::PartialExpr into Thunk --- dhall/src/semantics/nze/value.rs | 82 ++++++++++++++++++++++------------------ 1 file changed, 46 insertions(+), 36 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d737a0f..87ebfcd 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -35,19 +35,23 @@ struct ValueInternal { /// explained in the doc for `ValueKind`. #[derive(Debug, Clone)] pub(crate) enum Form { - /// A totally unnormalized value. + /// An unevaluated value. Thunk(Thunk), - /// A partially normalized value that may need to go through `normalize_one_layer`. - PartialExpr(ExprKind), /// A value in WHNF. WHNF(ValueKind), } /// An unevaluated subexpression #[derive(Debug, Clone)] -pub(crate) struct Thunk { - env: NzEnv, - body: TyExpr, +pub(crate) enum Thunk { + /// A completely unnormalized expression. + Thunk { env: NzEnv, body: TyExpr }, + /// A partially normalized expression that may need to go through `normalize_one_layer`. + PartialExpr { + env: NzEnv, + expr: ExprKind, + ty: Value, + }, } /// An unevaluated subexpression that takes an argument. @@ -139,9 +143,15 @@ impl Value { /// Construct a Value from a partially normalized expression that's not in WHNF. pub(crate) fn from_partial_expr( e: ExprKind, - t: Value, + ty: Value, ) -> Value { - Value::new(Form::PartialExpr(e), t, Span::Artificial) + // TODO: env + let env = NzEnv::new(); + Value::new( + Form::Thunk(Thunk::from_partial_expr(env, e, ty.clone())), + ty, + Span::Artificial, + ) } /// Make a Value from a ValueKind pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { @@ -188,7 +198,7 @@ impl Value { pub(crate) fn kind(&self) -> Ref { self.normalize_whnf(); Ref::map(self.as_form(), |form| match form { - Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(), + Form::Thunk(..) => unreachable!(), Form::WHNF(k) => k, }) } @@ -211,18 +221,18 @@ impl Value { } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_form(&mut self, f: impl FnOnce(&mut Form, &Option)) { + fn mutate_form(&mut self, f: impl FnOnce(&mut Form)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(vint) => f(RefCell::get_mut(&mut vint.form), &vint.ty), + Some(vint) => f(RefCell::get_mut(&mut vint.form)), // Otherwise mutate through the refcell - None => f(&mut self.0.form.borrow_mut(), &self.0.ty), + None => f(&mut self.0.form.borrow_mut()), } } /// Normalizes contents to normal form; faster than `normalize_nf` if /// no one else shares this. pub(crate) fn normalize_mut(&mut self) { - self.mutate_form(|form, ty| form.normalize_nf(ty)) + self.mutate_form(|form| form.normalize_nf()) } pub(crate) fn normalize_whnf(&self) { @@ -392,11 +402,11 @@ impl ValueInternal { fn normalize_whnf(&self) { if !self.form.borrow().is_whnf() { - self.form.borrow_mut().normalize_whnf(&self.ty) + self.form.borrow_mut().normalize_whnf() } } fn normalize_nf(&self) { - self.form.borrow_mut().normalize_nf(&self.ty) + self.form.borrow_mut().normalize_nf() } fn get_type(&self) -> Result<&Value, TypeError> { @@ -410,33 +420,25 @@ impl ValueInternal { impl Form { fn is_whnf(&self) -> bool { match self { - Form::Thunk(..) | Form::PartialExpr(..) => false, + Form::Thunk(..) => false, Form::WHNF(..) => true, } } - fn normalize_whnf(&mut self, ty: &Option) { + fn normalize_whnf(&mut self) { use std::mem::replace; - let dummy = Form::PartialExpr(ExprKind::Const(Const::Type)); + let dummy = Form::WHNF(ValueKind::Const(Const::Type)); *self = match replace(self, dummy) { Form::Thunk(th) => Form::WHNF(th.eval()), - Form::PartialExpr(e) => { - Form::WHNF(match ty { - // TODO: env - Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()), - // `value` is `Sort` - None => ValueKind::Const(Const::Sort), - }) - } // Already in WHNF form @ Form::WHNF(_) => form, }; } - fn normalize_nf(&mut self, ty: &Option) { + fn normalize_nf(&mut self) { if !self.is_whnf() { - self.normalize_whnf(ty); + self.normalize_whnf(); } match self { - Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(), + Form::Thunk(..) => unreachable!(), Form::WHNF(k) => k.normalize_mut(), } } @@ -517,13 +519,26 @@ impl ValueKind { impl Thunk { pub fn new(env: &NzEnv, body: TyExpr) -> Self { - Thunk { + Thunk::Thunk { env: env.clone(), body, } } + pub fn from_partial_expr( + env: NzEnv, + expr: ExprKind, + ty: Value, + ) -> Self { + Thunk::PartialExpr { env, expr, ty } + } + // TODO: take by value pub fn eval(&self) -> ValueKind { - normalize_tyexpr_whnf(&self.body, &self.env) + match self { + Thunk::Thunk { env, body } => normalize_tyexpr_whnf(body, env), + Thunk::PartialExpr { env, expr, ty } => { + normalize_one_layer(expr.clone(), ty, env) + } + } } } @@ -678,11 +693,6 @@ impl std::fmt::Debug for Value { x.field("thunk", th); x } - Form::PartialExpr(e) => { - let mut x = fmt.debug_struct(&format!("Value@PartialExpr")); - x.field("expr", e); - x - } Form::WHNF(kind) => { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); -- cgit v1.2.3 From 884774dbf13fd0a0fb6936c4259527a30a285ff0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 21:06:12 +0000 Subject: Replace Form with a pair of RefCells, in preparation for OnceCell --- dhall/src/semantics/nze/value.rs | 159 +++++++++++++++++---------------------- 1 file changed, 71 insertions(+), 88 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 87ebfcd..d25e8b5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -25,22 +25,15 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - form: RefCell, + /// Exactly one of `thunk` of `kind` must be set at a given time. + /// Once `thunk` is unset and `kind` is set, we never go back. + thunk: RefCell>, + kind: RefCell>, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, } -/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as -/// explained in the doc for `ValueKind`. -#[derive(Debug, Clone)] -pub(crate) enum Form { - /// An unevaluated value. - Thunk(Thunk), - /// A value in WHNF. - WHNF(ValueKind), -} - /// An unevaluated subexpression #[derive(Debug, Clone)] pub(crate) enum Thunk { @@ -120,12 +113,9 @@ pub(crate) enum ValueKind { } impl Value { - fn new(form: Form, ty: Value, span: Span) -> Value { - ValueInternal::new(form, Some(ty), span).into_value() - } pub(crate) fn const_sort() -> Value { - ValueInternal::new( - Form::WHNF(ValueKind::Const(Const::Sort)), + ValueInternal::from_whnf( + ValueKind::Const(Const::Sort), None, Span::Artificial, ) @@ -133,8 +123,8 @@ impl Value { } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { - ValueInternal::new( - Form::Thunk(Thunk::new(env, tye.clone())), + ValueInternal::from_thunk( + Thunk::new(env, tye.clone()), tye.get_type().ok(), tye.span().clone(), ) @@ -147,15 +137,16 @@ impl Value { ) -> Value { // TODO: env let env = NzEnv::new(); - Value::new( - Form::Thunk(Thunk::from_partial_expr(env, e, ty.clone())), - ty, + ValueInternal::from_thunk( + Thunk::from_partial_expr(env, e, ty.clone()), + Some(ty), Span::Artificial, ) + .into_value() } /// Make a Value from a ValueKind pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(Form::WHNF(v), t, Span::Artificial) + ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); @@ -189,18 +180,11 @@ impl Value { self.0.span.clone() } - fn as_form(&self) -> Ref { - self.0.form.borrow() - } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. pub(crate) fn kind(&self) -> Ref { - self.normalize_whnf(); - Ref::map(self.as_form(), |form| match form { - Form::Thunk(..) => unreachable!(), - Form::WHNF(k) => k, - }) + self.0.kind() } /// Converts a value back to the corresponding AST expression. @@ -220,24 +204,16 @@ impl Value { self.to_whnf_ignore_type() } - /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_form(&mut self, f: impl FnOnce(&mut Form)) { + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this. + pub(crate) fn normalize_mut(&mut self) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(vint) => f(RefCell::get_mut(&mut vint.form)), + Some(vint) => vint.normalize_nf_mut(), // Otherwise mutate through the refcell - None => f(&mut self.0.form.borrow_mut()), + None => self.0.normalize_nf(), } } - /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - self.mutate_form(|form| form.normalize_nf()) - } - - pub(crate) fn normalize_whnf(&self) { - self.0.normalize_whnf() - } pub(crate) fn normalize_nf(&self) { self.0.normalize_nf() } @@ -389,9 +365,18 @@ impl Value { } impl ValueInternal { - fn new(form: Form, ty: Option, span: Span) -> Self { + fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { ValueInternal { - form: RefCell::new(form), + thunk: RefCell::new(None), + kind: RefCell::new(Some(k)), + ty, + span, + } + } + fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { + ValueInternal { + kind: RefCell::new(None), + thunk: RefCell::new(Some(th)), ty, span, } @@ -400,13 +385,38 @@ impl ValueInternal { Value(Rc::new(self)) } + fn kind(&self) -> Ref { + self.normalize_whnf(); + Ref::map(self.kind.borrow(), |kind| kind.as_ref().unwrap()) + } fn normalize_whnf(&self) { - if !self.form.borrow().is_whnf() { - self.form.borrow_mut().normalize_whnf() + if self.kind.borrow().is_none() { + let mut thunk_borrow = self.thunk.borrow_mut(); + let kind = thunk_borrow.as_ref().unwrap().eval(); + *thunk_borrow = None; + *self.kind.borrow_mut() = Some(kind); } } fn normalize_nf(&self) { - self.form.borrow_mut().normalize_nf() + self.normalize_whnf(); + self.kind.borrow_mut().as_mut().unwrap().normalize_mut() + } + // Avoids a RefCell lock + fn normalize_whnf_mut(&mut self) { + let self_thunk = RefCell::get_mut(&mut self.thunk); + if let Some(thunk) = &mut *self_thunk { + let self_kind = RefCell::get_mut(&mut self.kind); + let mut kind = thunk.eval(); + kind.normalize_mut(); + *self_kind = Some(kind); + *self_thunk = None; + } + } + // Avoids a RefCell lock + fn normalize_nf_mut(&mut self) { + self.normalize_whnf_mut(); + let self_kind = RefCell::get_mut(&mut self.kind); + self_kind.as_mut().unwrap().normalize_mut(); } fn get_type(&self) -> Result<&Value, TypeError> { @@ -417,33 +427,6 @@ impl ValueInternal { } } -impl Form { - fn is_whnf(&self) -> bool { - match self { - Form::Thunk(..) => false, - Form::WHNF(..) => true, - } - } - fn normalize_whnf(&mut self) { - use std::mem::replace; - let dummy = Form::WHNF(ValueKind::Const(Const::Type)); - *self = match replace(self, dummy) { - Form::Thunk(th) => Form::WHNF(th.eval()), - // Already in WHNF - form @ Form::WHNF(_) => form, - }; - } - fn normalize_nf(&mut self) { - if !self.is_whnf() { - self.normalize_whnf(); - } - match self { - Form::Thunk(..) => unreachable!(), - Form::WHNF(k) => k.normalize_mut(), - } - } -} - impl ValueKind { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_kind_and_type(self, t) @@ -687,21 +670,21 @@ 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.0; - let mut x = match &*vint.form.borrow() { - Form::Thunk(th) => { - let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", th); + let kind_borrow = vint.kind.borrow(); + let mut x = if let Some(kind) = kind_borrow.as_ref() { + if let ValueKind::Const(c) = kind { + return write!(fmt, "{:?}", c); + } else { + let mut x = fmt.debug_struct(&format!("Value@WHNF")); + x.field("kind", kind); x } - Form::WHNF(kind) => { - if let ValueKind::Const(c) = kind { - return write!(fmt, "{:?}", c); - } else { - let mut x = fmt.debug_struct(&format!("Value@WHNF")); - x.field("kind", kind); - x - } - } + } else { + let thunk_borrow = vint.thunk.borrow(); + let th = thunk_borrow.as_ref().unwrap(); + let mut x = fmt.debug_struct(&format!("Value@Thunk")); + x.field("thunk", th); + x }; if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); -- cgit v1.2.3 From 2700af36adfac4390b9395ac2ed0e534b7eac887 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 21:43:50 +0000 Subject: Use OnceCell to enable returning &ValKind --- dhall/src/semantics/nze/value.rs | 121 +++++++++++++++++---------------------- 1 file changed, 53 insertions(+), 68 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d25e8b5..945ee6e 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,4 +1,5 @@ -use std::cell::{Ref, RefCell}; +use once_cell::unsync::OnceCell; +use std::cell::RefCell; use std::collections::HashMap; use std::rc::Rc; @@ -28,7 +29,7 @@ struct ValueInternal { /// Exactly one of `thunk` of `kind` must be set at a given time. /// Once `thunk` is unset and `kind` is set, we never go back. thunk: RefCell>, - kind: RefCell>, + kind: OnceCell, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -183,14 +184,14 @@ impl Value { /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. - pub(crate) fn kind(&self) -> Ref { + pub(crate) fn kind(&self) -> &ValueKind { self.0.kind() } /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { if opts.normalize { - self.normalize_nf(); + self.normalize(); } self.to_tyexpr_noenv().to_expr(opts) @@ -204,18 +205,18 @@ impl Value { self.to_whnf_ignore_type() } - /// Normalizes contents to normal form; faster than `normalize_nf` if + /// Normalizes contents to normal form; faster than `normalize` if /// no one else shares this. pub(crate) fn normalize_mut(&mut self) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(vint) => vint.normalize_nf_mut(), + Some(vint) => vint.normalize_mut(), // Otherwise mutate through the refcell - None => self.0.normalize_nf(), + None => self.normalize(), } } - pub(crate) fn normalize_nf(&self) { - self.0.normalize_nf() + pub(crate) fn normalize(&self) { + self.0.normalize() } pub(crate) fn app(&self, v: Value) -> Value { @@ -366,17 +367,19 @@ impl Value { impl ValueInternal { fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { + let kind = OnceCell::new(); + kind.set(k).unwrap(); ValueInternal { thunk: RefCell::new(None), - kind: RefCell::new(Some(k)), + kind, ty, span, } } fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { ValueInternal { - kind: RefCell::new(None), thunk: RefCell::new(Some(th)), + kind: OnceCell::new(), ty, span, } @@ -385,38 +388,23 @@ impl ValueInternal { Value(Rc::new(self)) } - fn kind(&self) -> Ref { - self.normalize_whnf(); - Ref::map(self.kind.borrow(), |kind| kind.as_ref().unwrap()) - } - fn normalize_whnf(&self) { - if self.kind.borrow().is_none() { - let mut thunk_borrow = self.thunk.borrow_mut(); - let kind = thunk_borrow.as_ref().unwrap().eval(); - *thunk_borrow = None; - *self.kind.borrow_mut() = Some(kind); + fn kind(&self) -> &ValueKind { + if self.kind.get().is_none() { + let thunk = self.thunk.borrow_mut().take().unwrap(); + self.kind.set(thunk.eval()).unwrap(); } + self.kind.get().unwrap() } - fn normalize_nf(&self) { - self.normalize_whnf(); - self.kind.borrow_mut().as_mut().unwrap().normalize_mut() + fn normalize(&self) { + self.kind().normalize(); } // Avoids a RefCell lock - fn normalize_whnf_mut(&mut self) { - let self_thunk = RefCell::get_mut(&mut self.thunk); - if let Some(thunk) = &mut *self_thunk { - let self_kind = RefCell::get_mut(&mut self.kind); - let mut kind = thunk.eval(); - kind.normalize_mut(); - *self_kind = Some(kind); - *self_thunk = None; + fn normalize_mut(&mut self) { + if self.kind.get().is_none() { + let thunk = RefCell::get_mut(&mut self.thunk).take().unwrap(); + self.kind.set(thunk.eval()).unwrap(); } - } - // Avoids a RefCell lock - fn normalize_nf_mut(&mut self) { - self.normalize_whnf_mut(); - let self_kind = RefCell::get_mut(&mut self.kind); - self_kind.as_mut().unwrap().normalize_mut(); + self.normalize(); } fn get_type(&self) -> Result<&Value, TypeError> { @@ -432,7 +420,7 @@ impl ValueKind { Value::from_kind_and_type(self, t) } - pub(crate) fn normalize_mut(&mut self) { + pub(crate) fn normalize(&self) { match self { ValueKind::Var(..) | ValueKind::Const(_) @@ -442,52 +430,52 @@ impl ValueKind { | ValueKind::DoubleLit(_) => {} ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); + tth.normalize(); } ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); + th.normalize(); } ValueKind::LamClosure { annot, closure, .. } | ValueKind::PiClosure { annot, closure, .. } => { - annot.normalize_mut(); - closure.normalize_mut(); + annot.normalize(); + closure.normalize(); } - ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(), + ValueKind::AppliedBuiltin(closure) => closure.normalize(), ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); + for x in elts.iter() { + x.normalize(); } } ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); + for x in kvs.values() { + x.normalize(); } } ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); + for x in kvs.values() { + x.normalize(); } } ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts, _) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); + for x in kts.values().flat_map(|opt| opt) { + x.normalize(); } } ValueKind::UnionLit(_, v, kts, _, _) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); + v.normalize(); + for x in kts.values().flat_map(|opt| opt) { + x.normalize(); } } - ValueKind::TextLit(tlit) => tlit.normalize_mut(), + ValueKind::TextLit(tlit) => tlit.normalize(), ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); + x.normalize(); + y.normalize(); } ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); + e.map_ref(Value::normalize); } } } @@ -563,7 +551,7 @@ impl Closure { } // TODO: somehow normalize the body. Might require to pass an env. - pub fn normalize_mut(&mut self) {} + pub fn normalize(&self) {} /// Convert this closure to a TyExpr pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { self.apply_var(NzVar::new(venv.size())) @@ -634,9 +622,9 @@ impl TextLit { } /// Normalize the contained values. This does not break the invariant because we have already /// ensured that no contained values normalize to a TextLit. - pub fn normalize_mut(&mut self) { - for x in self.0.iter_mut() { - x.map_mut(Value::normalize_mut); + pub fn normalize(&self) { + for x in self.0.iter() { + x.map_ref(Value::normalize); } } } @@ -670,8 +658,7 @@ 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.0; - let kind_borrow = vint.kind.borrow(); - let mut x = if let Some(kind) = kind_borrow.as_ref() { + let mut x = if let Some(kind) = vint.kind.get() { if let ValueKind::Const(c) = kind { return write!(fmt, "{:?}", c); } else { @@ -680,10 +667,8 @@ impl std::fmt::Debug for Value { x } } else { - let thunk_borrow = vint.thunk.borrow(); - let th = thunk_borrow.as_ref().unwrap(); let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", th); + x.field("thunk", vint.thunk.borrow().as_ref().unwrap()); x }; if let Some(ty) = vint.ty.as_ref() { -- cgit v1.2.3 From ace2a1f2783f770dc801f74e9118d39c73eb158a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:00:32 +0000 Subject: Get rid of all the manual Ref borrows --- dhall/src/semantics/nze/normalize.rs | 170 ++++++++++++----------------------- 1 file changed, 55 insertions(+), 115 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index e677f78..e9d140b 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -11,8 +11,7 @@ use crate::syntax::{ use crate::Normalized; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.kind(); - match &*f_borrow { + match f.kind() { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } @@ -26,10 +25,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { uniont.clone(), f.get_type().unwrap(), ), - _ => { - drop(f_borrow); - ValueKind::PartialExpr(ExprKind::App(f, a)) - } + _ => ValueKind::PartialExpr(ExprKind::App(f, a)), } } @@ -47,21 +43,17 @@ pub(crate) fn squash_textlit( for contents in elts { match contents { Text(s) => crnt_str.push_str(&s), - Expr(e) => { - let e_borrow = e.kind(); - match &*e_borrow { - ValueKind::TextLit(elts2) => { - inner(elts2.iter().cloned(), crnt_str, ret) - } - _ => { - drop(e_borrow); - if !crnt_str.is_empty() { - ret.push(Text(replace(crnt_str, String::new()))) - } - ret.push(Expr(e.clone())) + Expr(e) => match e.kind() { + ValueKind::TextLit(elts2) => { + inner(elts2.iter().cloned(), crnt_str, ret) + } + _ => { + if !crnt_str.is_empty() { + ret.push(Text(replace(crnt_str, String::new()))) } + ret.push(Expr(e.clone())) } - } + }, } } } @@ -123,9 +115,7 @@ fn apply_binop<'a>( use ValueKind::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, }; - let x_borrow = x.kind(); - let y_borrow = y.kind(); - Some(match (o, &*x_borrow, &*y_borrow) { + Some(match (o, x.kind(), y.kind()) { (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), @@ -202,8 +192,7 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.kind(); - let kts = match &*ty_borrow { + let kts = match ty.kind() { RecordType(kts) => kts, _ => unreachable!("Internal type error"), }; @@ -314,23 +303,15 @@ pub(crate) fn normalize_one_layer( } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.kind(); - match &*b_borrow { + match b.kind() { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.kind(); - let e2_borrow = e2.kind(); - match (&*e1_borrow, &*e2_borrow) { + match (e1.kind(), e2.kind()) { // Simplify `if b then True else False` (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), _ if e1 == e2 => Ret::ValueRef(e1), - _ => { - drop(b_borrow); - drop(e1_borrow); - drop(e2_borrow); - Ret::Expr(expr) - } + _ => Ret::Expr(expr), } } } @@ -343,94 +324,53 @@ pub(crate) fn normalize_one_layer( ExprKind::Projection(_, ref ls) if ls.is_empty() => { Ret::ValueKind(RecordLit(HashMap::new())) } - ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.kind(); - match &*v_borrow { - RecordLit(kvs) => Ret::ValueKind(RecordLit( - ls.iter() - .filter_map(|l| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::Field(ref v, ref l) => { - let v_borrow = v.kind(); - match &*v_borrow { - RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), - None => { - drop(v_borrow); - Ret::Expr(expr) - } - }, - UnionType(kts) => Ret::ValueKind(UnionConstructor( - l.clone(), - kts.clone(), - v.get_type().unwrap(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } + ExprKind::Projection(ref v, ref ls) => match v.kind() { + RecordLit(kvs) => Ret::ValueKind(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), + _ => Ret::Expr(expr), + }, + ExprKind::Field(ref v, ref l) => match v.kind() { + RecordLit(kvs) => match kvs.get(l) { + Some(r) => Ret::Value(r.clone()), + None => Ret::Expr(expr), + }, + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), + _ => Ret::Expr(expr), + }, ExprKind::ProjectionByExpr(_, _) => { unimplemented!("selection by expression") } ExprKind::Completion(_, _) => unimplemented!("record completion"), ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.kind(); - let variant_borrow = variant.kind(); - match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) - { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), EmptyOptionalLit(_)) => { - match kvs.get(&"None".into()) { + match handlers.kind() { + RecordLit(kvs) => match variant.kind() { + UnionConstructor(l, _, _) => match kvs.get(l) { Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - (RecordLit(kvs), NEOptionalLit(v)) => { - match kvs.get(&"Some".into()) { + None => Ret::Expr(expr), + }, + UnionLit(l, v, _, _, _) => match kvs.get(l) { Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - _ => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } + None => Ret::Expr(expr), + }, + EmptyOptionalLit(_) => match kvs.get(&"None".into()) { + Some(h) => Ret::Value(h.clone()), + None => Ret::Expr(expr), + }, + NEOptionalLit(v) => match kvs.get(&"Some".into()) { + Some(h) => Ret::Value(h.app(v.clone())), + None => Ret::Expr(expr), + }, + _ => Ret::Expr(expr), + }, + _ => Ret::Expr(expr), } } ExprKind::ToMap(_, _) => unimplemented!("toMap"), -- cgit v1.2.3 From 4e2bb03bcf6355d49216c6886bf03e5aeaad16cc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:01:54 +0000 Subject: Eval Thunk by move --- dhall/src/semantics/nze/value.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 945ee6e..724e3e8 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -502,12 +502,11 @@ impl Thunk { ) -> Self { Thunk::PartialExpr { env, expr, ty } } - // TODO: take by value - pub fn eval(&self) -> ValueKind { + pub fn eval(self) -> ValueKind { match self { - Thunk::Thunk { env, body } => normalize_tyexpr_whnf(body, env), + Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), Thunk::PartialExpr { env, expr, ty } => { - normalize_one_layer(expr.clone(), ty, env) + normalize_one_layer(expr, &ty, &env) } } } -- cgit v1.2.3 From 70af1a47bce9e6c8282d6e53cf82aeda9aab10de Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:08:57 +0000 Subject: Tweak ConstantClosure --- dhall/src/semantics/nze/value.rs | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 724e3e8..67ab90a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -58,7 +58,7 @@ pub(crate) enum Closure { body: TyExpr, }, /// Closure that ignores the argument passed - ConstantClosure { env: NzEnv, body: TyExpr }, + ConstantClosure { body: Value }, } /// A text literal with interpolations. @@ -521,11 +521,8 @@ impl Closure { } } /// New closure that ignores its argument - pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { - Closure::ConstantClosure { - env: env.clone(), - body, - } + pub fn new_constant(body: Value) -> Self { + Closure::ConstantClosure { body } } pub fn apply(&self, val: Value) -> Value { @@ -533,7 +530,7 @@ impl Closure { Closure::Closure { env, body, .. } => { body.eval(&env.insert_value(val)) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } fn apply_var(&self, var: NzVar) -> Value { @@ -545,7 +542,7 @@ impl Closure { ); self.apply(val) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } @@ -559,17 +556,14 @@ impl Closure { /// If the closure variable is free in the closure, return Err. Otherwise, return the value /// with that free variable remove. pub fn remove_binder(&self) -> Result { - let v = NzVar::fresh(); match self { Closure::Closure { .. } => { + let v = NzVar::fresh(); // TODO: handle case where variable is used in closure // TODO: return information about where the variable is used Ok(self.apply_var(v)) } - Closure::ConstantClosure { .. } => { - // Ok: the variable is indeed ignored - Ok(self.apply_var(v)) - } + Closure::ConstantClosure { body, .. } => Ok(body.clone()), } } } -- cgit v1.2.3 From 4312ad935d881f269fa7e9cc3d880fa763db957d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 22:10:40 +0000 Subject: Use Rc equality to shortcut Value equality --- dhall/src/semantics/nze/value.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 67ab90a..de40d53 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -623,10 +623,9 @@ impl TextLit { } /// Compare two values for equality modulo alpha/beta-equivalence. -// TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - *self.kind() == *other.kind() + Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind() } } impl std::cmp::Eq for Value {} -- cgit v1.2.3 From aa93f18c8ef9ad13c6bb4ddef90b419b3ed546f4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 31 Jan 2020 19:46:16 +0000 Subject: Factor out custom Lazy struct --- dhall/src/semantics/nze/lazy.rs | 64 ++++++++++++++++++++++++++++++++++++++++ dhall/src/semantics/nze/mod.rs | 1 + dhall/src/semantics/nze/value.rs | 53 +++++++++++---------------------- 3 files changed, 83 insertions(+), 35 deletions(-) create mode 100644 dhall/src/semantics/nze/lazy.rs (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/lazy.rs b/dhall/src/semantics/nze/lazy.rs new file mode 100644 index 0000000..d361313 --- /dev/null +++ b/dhall/src/semantics/nze/lazy.rs @@ -0,0 +1,64 @@ +use once_cell::unsync::OnceCell; +use std::cell::Cell; +use std::fmt::Debug; +use std::ops::Deref; + +pub trait Eval { + fn eval(self) -> Tgt; +} + +/// A value which is initialized from a `Src` on the first access. +pub struct Lazy { + /// Exactly one of `src` of `tgt` must be set at a given time. + /// Once `src` is unset and `tgt` is set, we never go back. + src: Cell>, + tgt: OnceCell, +} + +impl Lazy +where + Src: Eval, +{ + /// Creates a new lazy value with the given initializing value. + pub fn new(src: Src) -> Self { + Lazy { + src: Cell::new(Some(src)), + tgt: OnceCell::new(), + } + } + /// Creates a new lazy value with the given already-initialized value. + pub fn new_completed(tgt: Tgt) -> Self { + let lazy = Lazy { + src: Cell::new(None), + tgt: OnceCell::new(), + }; + let _ = lazy.tgt.set(tgt); + lazy + } +} + +impl Deref for Lazy +where + Src: Eval, +{ + type Target = Tgt; + fn deref(&self) -> &Self::Target { + self.tgt.get_or_init(|| { + let src = self.src.take().unwrap(); + src.eval() + }) + } +} + +impl Debug for Lazy +where + Tgt: Debug, +{ + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if let Some(tgt) = self.tgt.get() { + fmt.debug_tuple("Lazy@Init").field(tgt).finish() + } else { + fmt.debug_tuple("Lazy@Uninit").finish() + } + } +} diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index 3d9c5eb..2c8d907 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,4 +1,5 @@ pub mod env; +pub mod lazy; pub mod normalize; pub mod value; pub mod var; diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index de40d53..ae06942 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,9 +1,8 @@ -use once_cell::unsync::OnceCell; -use std::cell::RefCell; use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; +use crate::semantics::nze::lazy; use crate::semantics::Binder; use crate::semantics::{ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, @@ -26,10 +25,7 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { - /// Exactly one of `thunk` of `kind` must be set at a given time. - /// Once `thunk` is unset and `kind` is set, we never go back. - thunk: RefCell>, - kind: OnceCell, + kind: lazy::Lazy, /// This is None if and only if `form` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -367,19 +363,15 @@ impl Value { impl ValueInternal { fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { - let kind = OnceCell::new(); - kind.set(k).unwrap(); ValueInternal { - thunk: RefCell::new(None), - kind, + kind: lazy::Lazy::new_completed(k), ty, span, } } fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { ValueInternal { - thunk: RefCell::new(Some(th)), - kind: OnceCell::new(), + kind: lazy::Lazy::new(th), ty, span, } @@ -389,21 +381,13 @@ impl ValueInternal { } fn kind(&self) -> &ValueKind { - if self.kind.get().is_none() { - let thunk = self.thunk.borrow_mut().take().unwrap(); - self.kind.set(thunk.eval()).unwrap(); - } - self.kind.get().unwrap() + &self.kind } fn normalize(&self) { self.kind().normalize(); } - // Avoids a RefCell lock + // TODO: deprecated fn normalize_mut(&mut self) { - if self.kind.get().is_none() { - let thunk = RefCell::get_mut(&mut self.thunk).take().unwrap(); - self.kind.set(thunk.eval()).unwrap(); - } self.normalize(); } @@ -622,6 +606,12 @@ impl TextLit { } } +impl lazy::Eval for Thunk { + fn eval(self) -> ValueKind { + self.eval() + } +} + /// Compare two values for equality modulo alpha/beta-equivalence. impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -650,19 +640,12 @@ 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.0; - let mut x = if let Some(kind) = vint.kind.get() { - if let ValueKind::Const(c) = kind { - return write!(fmt, "{:?}", c); - } else { - let mut x = fmt.debug_struct(&format!("Value@WHNF")); - x.field("kind", kind); - x - } - } else { - let mut x = fmt.debug_struct(&format!("Value@Thunk")); - x.field("thunk", vint.thunk.borrow().as_ref().unwrap()); - x - }; + let kind = vint.kind(); + if let ValueKind::Const(c) = kind { + return write!(fmt, "{:?}", c); + } + let mut x = fmt.debug_struct(&format!("Value@WHNF")); + x.field("kind", kind); if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); } else { -- cgit v1.2.3