From ec28905d32c23109da17696faefab284fde3e103 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 18 Jan 2020 18:46:09 +0000 Subject: Introduce intermediate representation that stores typed expr --- dhall/src/semantics/tck/tyexpr.rs | 83 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 dhall/src/semantics/tck/tyexpr.rs (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs new file mode 100644 index 0000000..a8b8e58 --- /dev/null +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -0,0 +1,83 @@ +#![allow(dead_code)] +use crate::semantics::core::var::AlphaVar; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::Normalized; +use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; +use crate::semantics::Value; +use crate::syntax::{ExprKind, Label, Span, V}; + +pub(crate) type Type = Value; + +// An expression with inferred types at every node and resolved variables. +pub(crate) struct TyExpr { + kind: Box, + ty: Option, + span: Span, +} + +pub(crate) enum TyExprKind { + Var(AlphaVar), + // Forbidden ExprKind variants: Var + Expr(ExprKind), +} + +impl TyExpr { + pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { + TyExpr { + kind: Box::new(kind), + ty, + span, + } + } + + pub fn kind(&self) -> &TyExprKind { + &*self.kind + } + + /// Converts a value back to the corresponding AST expression. + pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr { + tyexpr_to_expr(self, opts, &Vec::new()) + } +} + +// TODO: mutate context once map_ref gets simplified +fn tyexpr_to_expr<'a>( + tyexpr: &'a TyExpr, + opts: ToExprOptions, + ctx: &Vec<&'a Label>, +) -> NormalizedExpr { + rc(match tyexpr.kind() { + TyExprKind::Var(v) if opts.alpha => { + ExprKind::Var(V("_".into(), v.idx())) + } + TyExprKind::Var(v) => { + let name = ctx[ctx.len() - 1 - v.idx()]; + let mut idx = 0; + for l in ctx.iter().rev().take(v.idx()) { + if *l == name { + idx += 1; + } + } + ExprKind::Var(V(name.clone(), idx)) + } + TyExprKind::Expr(e) => { + let e = e.map_ref_with_special_handling_of_binders( + |tye| tyexpr_to_expr(tye, opts, ctx), + |l, tye| { + let ctx = ctx.iter().copied().chain(Some(l)).collect(); + tyexpr_to_expr(tye, opts, &ctx) + }, + ); + + 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, + } + } + }) +} -- cgit v1.2.3 From d6e5c56a5ef1d5f2b7cafd4a8fb44ce038932547 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 18 Jan 2020 19:08:34 +0000 Subject: Add Expr visitor and improve tyexpr_to_expr --- dhall/src/semantics/tck/tyexpr.rs | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a8b8e58..f0fcdd1 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -36,15 +36,14 @@ impl TyExpr { /// Converts a value back to the corresponding AST expression. pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr { - tyexpr_to_expr(self, opts, &Vec::new()) + tyexpr_to_expr(self, opts, &mut Vec::new()) } } -// TODO: mutate context once map_ref gets simplified fn tyexpr_to_expr<'a>( tyexpr: &'a TyExpr, opts: ToExprOptions, - ctx: &Vec<&'a Label>, + ctx: &mut Vec<&'a Label>, ) -> NormalizedExpr { rc(match tyexpr.kind() { TyExprKind::Var(v) if opts.alpha => { @@ -61,13 +60,16 @@ fn tyexpr_to_expr<'a>( ExprKind::Var(V(name.clone(), idx)) } TyExprKind::Expr(e) => { - let e = e.map_ref_with_special_handling_of_binders( - |tye| tyexpr_to_expr(tye, opts, ctx), - |l, tye| { - let ctx = ctx.iter().copied().chain(Some(l)).collect(); - tyexpr_to_expr(tye, opts, &ctx) - }, - ); + let e = e.map_ref_maybe_binder(|l, tye| { + if let Some(l) = l { + ctx.push(l); + } + let e = tyexpr_to_expr(tye, opts, ctx); + if let Some(_) = l { + ctx.pop(); + } + e + }); match e { ExprKind::Lam(_, t, e) if opts.alpha => { -- cgit v1.2.3 From aec80599f161096b68cac88ffb8852a61b62fcfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 19 Jan 2020 18:30:13 +0000 Subject: Restore more types in value_to_tyexpr --- dhall/src/semantics/tck/tyexpr.rs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index f0fcdd1..36cae04 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,4 +1,6 @@ #![allow(dead_code)] +use crate::error::{TypeError, TypeMessage}; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -33,11 +35,21 @@ impl TyExpr { pub fn kind(&self) -> &TyExprKind { &*self.kind } + pub fn get_type(&self) -> Result { + match &self.ty { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + } + } /// Converts a value back to the corresponding AST expression. - pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr { + pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { tyexpr_to_expr(self, opts, &mut Vec::new()) } + // TODO: temporary hack + pub fn to_value(&self) -> Value { + todo!() + } } fn tyexpr_to_expr<'a>( -- cgit v1.2.3 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/tck/tyexpr.rs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 36cae04..72f5b1d 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -11,15 +11,17 @@ use crate::syntax::{ExprKind, Label, Span, V}; pub(crate) type Type = Value; // An expression with inferred types at every node and resolved variables. +#[derive(Debug, Clone)] pub(crate) struct TyExpr { kind: Box, ty: Option, span: Span, } +#[derive(Debug, Clone)] pub(crate) enum TyExprKind { Var(AlphaVar), - // Forbidden ExprKind variants: Var + // Forbidden ExprKind variants: Var, Import, Embed Expr(ExprKind), } @@ -63,12 +65,12 @@ fn tyexpr_to_expr<'a>( } TyExprKind::Var(v) => { let name = ctx[ctx.len() - 1 - v.idx()]; - let mut idx = 0; - for l in ctx.iter().rev().take(v.idx()) { - if *l == name { - idx += 1; - } - } + let idx = ctx + .iter() + .rev() + .take(v.idx()) + .filter(|l| **l == name) + .count(); ExprKind::Var(V(name.clone(), idx)) } TyExprKind::Expr(e) => { -- cgit v1.2.3 From 015b24b04128cbf5a60fbc8ac3f526306ca27378 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 17:43:44 +0000 Subject: Simplify type error type --- dhall/src/semantics/tck/tyexpr.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 72f5b1d..983f3f8 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,5 @@ #![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -40,7 +39,7 @@ impl TyExpr { pub fn get_type(&self) -> Result { match &self.ty { Some(t) => Ok(t.clone()), - None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + None => Err(TypeError::new(TypeMessage::Sort)), } } -- 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/tck/tyexpr.rs | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 983f3f8..c8be3a3 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,7 @@ #![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; +use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; @@ -51,6 +52,13 @@ impl TyExpr { pub fn to_value(&self) -> Value { todo!() } + + pub fn normalize_whnf(&self, env: &NzEnv) -> Value { + normalize_tyexpr_whnf(self, env) + } + pub fn normalize_whnf_noenv(&self) -> Value { + normalize_tyexpr_whnf(self, &NzEnv::new()) + } } fn tyexpr_to_expr<'a>( -- 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/tck/tyexpr.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index c8be3a3..a42265d 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::Value; use crate::syntax::{ExprKind, Label, Span, V}; @@ -48,6 +49,15 @@ impl TyExpr { pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { tyexpr_to_expr(self, opts, &mut Vec::new()) } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + let opts = ToExprOptions { + normalize: true, + alpha: false, + }; + let env = env.as_nameenv().names(); + let mut env = env.iter().collect(); + tyexpr_to_expr(self, opts, &mut env) + } // TODO: temporary hack pub fn to_value(&self) -> Value { todo!() -- 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/tck/tyexpr.rs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a42265d..9e8dc47 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -12,7 +12,7 @@ use crate::syntax::{ExprKind, Label, Span, V}; pub(crate) type Type = Value; // An expression with inferred types at every node and resolved variables. -#[derive(Debug, Clone)] +#[derive(Clone)] pub(crate) struct TyExpr { kind: Box, ty: Option, @@ -114,3 +114,16 @@ fn tyexpr_to_expr<'a>( } }) } + +impl std::fmt::Debug for TyExpr { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut x = fmt.debug_struct("TyExpr"); + x.field("kind", self.kind()); + if let Some(ty) = self.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } +} -- cgit v1.2.3 From e410dbb428e621fe600be43ddecca1c7bff7cb2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 19:11:52 +0000 Subject: Fix insufficient normalization --- dhall/src/semantics/tck/tyexpr.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 9e8dc47..e4108ad 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -67,7 +67,15 @@ impl TyExpr { normalize_tyexpr_whnf(self, env) } pub fn normalize_whnf_noenv(&self) -> Value { - normalize_tyexpr_whnf(self, &NzEnv::new()) + self.normalize_whnf(&NzEnv::new()) + } + pub fn normalize_nf(&self, env: &NzEnv) -> Value { + let mut val = self.normalize_whnf(env); + val.normalize_mut(); + val + } + pub fn normalize_nf_noenv(&self) -> Value { + self.normalize_nf(&NzEnv::new()) } } -- 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/tck/tyexpr.rs | 5 ----- 1 file changed, 5 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index e4108ad..abb6fa8 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,4 +1,3 @@ -#![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; @@ -58,10 +57,6 @@ impl TyExpr { let mut env = env.iter().collect(); tyexpr_to_expr(self, opts, &mut env) } - // TODO: temporary hack - pub fn to_value(&self) -> Value { - todo!() - } pub fn normalize_whnf(&self, env: &NzEnv) -> Value { normalize_tyexpr_whnf(self, env) -- 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/tck/tyexpr.rs | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index abb6fa8..b64c519 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,12 +1,13 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; +use crate::semantics::nze::nzexpr::NameEnv; use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::Value; -use crate::syntax::{ExprKind, Label, Span, V}; +use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; @@ -46,15 +47,14 @@ impl TyExpr { /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - tyexpr_to_expr(self, opts, &mut Vec::new()) + tyexpr_to_expr(self, opts, &mut NameEnv::new()) } pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { let opts = ToExprOptions { normalize: true, alpha: false, }; - let env = env.as_nameenv().names(); - let mut env = env.iter().collect(); + let mut env = env.as_nameenv().clone(); tyexpr_to_expr(self, opts, &mut env) } @@ -77,30 +77,21 @@ impl TyExpr { fn tyexpr_to_expr<'a>( tyexpr: &'a TyExpr, opts: ToExprOptions, - ctx: &mut Vec<&'a Label>, + env: &mut NameEnv, ) -> NormalizedExpr { rc(match tyexpr.kind() { TyExprKind::Var(v) if opts.alpha => { ExprKind::Var(V("_".into(), v.idx())) } - TyExprKind::Var(v) => { - let name = ctx[ctx.len() - 1 - v.idx()]; - let idx = ctx - .iter() - .rev() - .take(v.idx()) - .filter(|l| **l == name) - .count(); - ExprKind::Var(V(name.clone(), idx)) - } + TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)), TyExprKind::Expr(e) => { let e = e.map_ref_maybe_binder(|l, tye| { if let Some(l) = l { - ctx.push(l); + env.insert_mut(l); } - let e = tyexpr_to_expr(tye, opts, ctx); + let e = tyexpr_to_expr(tye, opts, env); if let Some(_) = l { - ctx.pop(); + env.remove_mut(); } e }); -- 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/tck/tyexpr.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index b64c519..262cda6 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,12 +1,10 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; -use crate::semantics::nze::nzexpr::NameEnv; -use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; +use crate::semantics::phase::normalize::normalize_tyexpr_whnf; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; -use crate::semantics::tck::typecheck::TyEnv; -use crate::semantics::Value; +use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; -- 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/tck/tyexpr.rs | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 262cda6..114bb14 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,5 +1,4 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::normalize::normalize_tyexpr_whnf; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -9,6 +8,19 @@ use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; +/// Stores an alpha-normalized variable. +#[derive(Debug, Clone, Copy)] +pub struct AlphaVar { + idx: usize, +} + +#[derive(Debug, Clone)] +pub(crate) enum TyExprKind { + Var(AlphaVar), + // Forbidden ExprKind variants: Var, Import, Embed + Expr(ExprKind), +} + // An expression with inferred types at every node and resolved variables. #[derive(Clone)] pub(crate) struct TyExpr { @@ -17,11 +29,13 @@ pub(crate) struct TyExpr { span: Span, } -#[derive(Debug, Clone)] -pub(crate) enum TyExprKind { - Var(AlphaVar), - // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), +impl AlphaVar { + pub(crate) fn new(idx: usize) -> Self { + AlphaVar { idx } + } + pub(crate) fn idx(&self) -> usize { + self.idx + } } impl TyExpr { -- cgit v1.2.3 From 655f67fb29ca847f86c3e19338757e7b031d4f50 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:09:39 +0000 Subject: Move builtins-related code to its own module --- dhall/src/semantics/tck/tyexpr.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 114bb14..bf7c130 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,9 +1,8 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::normalize_tyexpr_whnf; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; -use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; +use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; -- cgit v1.2.3 From 25bd09136742403d7f3d6c6143f72e6687f39457 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 14:48:38 +0000 Subject: Make unnormalized Values unobservable --- dhall/src/semantics/tck/tyexpr.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index bf7c130..5492b8b 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -76,9 +76,7 @@ impl TyExpr { self.normalize_whnf(&NzEnv::new()) } pub fn normalize_nf(&self, env: &NzEnv) -> Value { - let mut val = self.normalize_whnf(env); - val.normalize_mut(); - val + self.normalize_whnf(env) } pub fn normalize_nf_noenv(&self) -> Value { self.normalize_nf(&NzEnv::new()) -- cgit v1.2.3 From 67bbbafbc9730d74e20e5ac082ae9a87bdf2234e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 16:39:25 +0000 Subject: Introduce Thunks and normalize lazily --- dhall/src/semantics/tck/tyexpr.rs | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 5492b8b..0a27f32 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -49,6 +49,9 @@ impl TyExpr { pub fn kind(&self) -> &TyExprKind { &*self.kind } + pub fn span(&self) -> &Span { + &self.span + } pub fn get_type(&self) -> Result { match &self.ty { Some(t) => Ok(t.clone()), @@ -69,17 +72,18 @@ impl TyExpr { tyexpr_to_expr(self, opts, &mut env) } - pub fn normalize_whnf(&self, env: &NzEnv) -> Value { - normalize_tyexpr_whnf(self, env) - } - pub fn normalize_whnf_noenv(&self) -> Value { - self.normalize_whnf(&NzEnv::new()) + /// Eval the TyExpr. It will actually get evaluated only as needed on demand. + pub fn eval(&self, env: &NzEnv) -> Value { + Value::new_thunk(env, self.clone()) } - pub fn normalize_nf(&self, env: &NzEnv) -> Value { - self.normalize_whnf(env) + /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as + /// needed on demand. + pub fn eval_closed_expr(&self) -> Value { + self.eval(&NzEnv::new()) } - pub fn normalize_nf_noenv(&self) -> Value { - self.normalize_nf(&NzEnv::new()) + /// Eval a closed TyExpr fully and recursively; + pub fn rec_eval_closed_expr(&self) -> Value { + normalize_tyexpr_whnf(self, &NzEnv::new()) } } -- 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/tck/tyexpr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 0a27f32..98dc3f9 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,5 +1,5 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::phase::normalize::normalize_tyexpr_whnf; +use crate::semantics::normalize_tyexpr_whnf; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; -- 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/tck/tyexpr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 98dc3f9..4b88048 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,9 +1,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::normalize_tyexpr_whnf; -use crate::semantics::phase::Normalized; -use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; +use crate::Normalized; +use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; -- 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/tck/tyexpr.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 4b88048..1a048f9 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,5 +1,4 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::normalize_tyexpr_whnf; use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; use crate::Normalized; @@ -83,7 +82,9 @@ impl TyExpr { } /// Eval a closed TyExpr fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { - normalize_tyexpr_whnf(self, &NzEnv::new()) + let mut val = self.eval_closed_expr(); + val.normalize_mut(); + val } } -- cgit v1.2.3