From 5542797c77a9dfcdffec539f1a82341a450291a2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 15:31:06 +0000 Subject: s/TypecheckContext/TyCtx/ --- dhall/src/semantics/phase/typecheck.rs | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 3960146..16eabea 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -3,7 +3,7 @@ use std::cmp::max; use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{Shift, Subst}; @@ -16,7 +16,7 @@ use crate::syntax::{ }; fn tck_pi_type( - ctx: &TypecheckContext, + ctx: &TyCtx, x: Label, tx: Value, te: Value, @@ -48,7 +48,7 @@ fn tck_pi_type( } fn tck_record_type( - ctx: &TypecheckContext, + ctx: &TyCtx, kts: impl IntoIterator>, ) -> Result { use std::collections::hash_map::Entry; @@ -79,10 +79,7 @@ fn tck_record_type( )) } -fn tck_union_type( - ctx: &TypecheckContext, - kts: Iter, -) -> Result +fn tck_union_type(ctx: &TyCtx, kts: Iter) -> Result where Iter: IntoIterator), TypeError>>, { @@ -294,7 +291,7 @@ fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { - let ctx = TypecheckContext::new(); + let ctx = TyCtx::new(); Value::from_kind_and_type( ValueKind::from_builtin(b), type_with(&ctx, type_of_builtin(b)).unwrap(), @@ -305,10 +302,7 @@ pub(crate) fn builtin_to_value(b: Builtin) -> Value { /// succeeded, or an error if type-checking failed. /// Some normalization is done while typechecking, so the returned expression might be partially /// normalized as well. -fn type_with( - ctx: &TypecheckContext, - e: Expr, -) -> Result { +fn type_with(ctx: &TyCtx, e: Expr) -> Result { use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); @@ -364,7 +358,7 @@ fn type_with( /// When all sub-expressions have been typed, check the remaining toplevel /// layer. fn type_last_layer( - ctx: &TypecheckContext, + ctx: &TyCtx, e: ExprKind, span: Span, ) -> Result { @@ -827,7 +821,7 @@ fn type_last_layer( /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. pub(crate) fn typecheck(e: Expr) -> Result { - type_with(&TypecheckContext::new(), e) + type_with(&TyCtx::new(), e) } pub(crate) fn typecheck_with( -- cgit v1.2.3 From ce706817dcb5cb951c566410de92a4f85aae5361 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 15:36:10 +0000 Subject: Tiny clarification --- dhall/src/semantics/phase/typecheck.rs | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 16eabea..c8d934d 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -306,23 +306,23 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); - Ok(match e.as_ref() { + match e.as_ref() { Lam(var, annot, body) => { let annot = type_with(ctx, annot.clone())?; annot.normalize_nf(); let ctx2 = ctx.insert_type(var, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; - Value::from_kind_and_type( + Ok(Value::from_kind_and_type( ValueKind::Lam(var.clone().into(), annot.clone(), body), tck_pi_type(ctx, var.clone(), annot, body_type)?, - ) + )) } Pi(x, ta, tb) => { let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - return tck_pi_type(ctx, x.clone(), ta, tb); + tck_pi_type(ctx, x.clone(), ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -332,16 +332,13 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { }; let v = type_with(ctx, v)?; - return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); + type_with(&ctx.insert_value(x, v.clone())?, e.clone()) } - Embed(p) => p.clone().into_typed().into_value(), + Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { - Some(typed) => typed.clone(), + Some(typed) => Ok(typed.clone()), None => { - return Err(TypeError::new( - ctx, - TypeMessage::UnboundVariable(span), - )) + Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span))) } }, e => { @@ -350,9 +347,9 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { |e| type_with(ctx, e.clone()), |_, _| unreachable!(), )?; - type_last_layer(ctx, expr, span)? + type_last_layer(ctx, expr, span) } - }) + } } /// When all sub-expressions have been typed, check the remaining toplevel -- cgit v1.2.3 From 015b76ce47af5b1b31661a934aee13843215c6b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 16:48:33 +0000 Subject: Construct T/Build closures in Expr space --- dhall/src/semantics/phase/normalize.rs | 113 +++++++++++++++++---------------- dhall/src/semantics/phase/typecheck.rs | 3 +- 2 files changed, 58 insertions(+), 58 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index bf0c626..0c581fe 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,7 +3,8 @@ use std::convert::TryInto; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::core::var::Subst; +use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::Const::Type; @@ -14,60 +15,51 @@ use crate::syntax::{ // Ad-hoc macro to help construct closures macro_rules! make_closure { - (#$var:ident) => { $var.clone() }; - (var($var:ident, $n:expr, $($ty:tt)*)) => {{ - let var = AlphaVar::from_var_and_alpha( + (var($var:ident)) => {{ + rc(ExprKind::Var(syntax::V( Label::from(stringify!($var)).into(), - $n - ); - ValueKind::Var(var) - .into_value_with_type(make_closure!($($ty)*)) + 0 + ))) }}; - // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var: AlphaLabel = Label::from(stringify!($var)).into(); + let var = Label::from(stringify!($var)); let ty = make_closure!($($ty)*); let body = make_closure!($($body)*); - let body_ty = body.get_type_not_sort(); - let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty) - .into_value_with_type(Value::from_const(Type)); - ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty) + rc(ExprKind::Lam(var, ty, body)) }}; - (Natural) => { - Value::from_builtin(Builtin::Natural) + (Type) => { + rc(ExprKind::Const(Type)) }; - (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app(make_closure!($($rest)*)) + (Natural) => { + rc(ExprKind::Builtin(Builtin::Natural)) }; - (Some($($rest:tt)*)) => {{ - let v = make_closure!($($rest)*); - let v_type = v.get_type_not_sort(); - let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); - ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) + (List $($ty:tt)*) => {{ + let ty = make_closure!($($ty)*); + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + ty + )) }}; - (1 + $($rest:tt)*) => { - ValueKind::PartialExpr(ExprKind::BinOp( + (Some($($v:tt)*)) => { + rc(ExprKind::SomeLit( + make_closure!($($v)*) + )) + }; + (1 + $($v:tt)*) => { + rc(ExprKind::BinOp( syntax::BinOp::NaturalPlus, - make_closure!($($rest)*), - Value::from_kind_and_type( - ValueKind::NaturalLit(1), - make_closure!(Natural) - ), - )).into_value_with_type( - make_closure!(Natural) - ) + make_closure!($($v)*), + rc(ExprKind::NaturalLit(1)) + )) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - let list_type = tail.get_type_not_sort(); - ValueKind::PartialExpr(ExprKind::BinOp( + rc(ExprKind::BinOp( syntax::BinOp::ListAppend, - ValueKind::NEListLit(vec![head]) - .into_value_with_type(list_type.clone()), + rc(ExprKind::NEListLit(vec![head])), tail, - )).into_value_with_type(list_type) + )) }}; } @@ -274,16 +266,16 @@ pub(crate) fn apply_builtin( let list_t = Value::from_builtin(List).app(t.clone()); Ret::Value( f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("a")); - let t2 = t1.under_binder(Label::from("as")); - make_closure!( - λ(a : #t) -> - λ(as : List #t1) -> - [ var(a, 1, #t2) ] # var(as, 0, List #t2) - ) - }) + .app( + typecheck(make_closure!( + λ(T : Type) -> + λ(a : var(T)) -> + λ(as : List var(T)) -> + [ var(a) ] # var(as) + )) + .unwrap() + .app(t.clone()), + ) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), ) } @@ -302,10 +294,15 @@ pub(crate) fn apply_builtin( let optional_t = Value::from_builtin(Optional).app(t.clone()); Ret::Value( f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("a")); - make_closure!(λ(a: #t) -> Some(var(a, 0, #t1))) - }) + .app( + typecheck(make_closure!( + λ(T : Type) -> + λ(a : var(T)) -> + Some(var(a)) + )) + .unwrap() + .app(t.clone()), + ) .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), @@ -324,9 +321,13 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) + .app( + typecheck(make_closure!( + λ(x : Natural) -> + 1 + var(x) + )) + .unwrap(), + ) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index c8d934d..2e1cc02 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -291,10 +291,9 @@ fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { - let ctx = TyCtx::new(); Value::from_kind_and_type( ValueKind::from_builtin(b), - type_with(&ctx, type_of_builtin(b)).unwrap(), + typecheck(type_of_builtin(b)).unwrap(), ) } -- cgit v1.2.3 From 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 14:26:40 +0000 Subject: Parameterize ValueKind by its subnodes --- dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 15 +++++++++------ 2 files changed, 10 insertions(+), 7 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 5332eb3..104a1ba 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -94,7 +94,7 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(Value::from_const(c)) } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { Typed(Value::from_kind_and_type(v, t.into_value())) } pub(crate) fn from_value(th: Value) -> Self { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 0c581fe..7b4b37f 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -68,13 +68,13 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, -) -> ValueKind { +) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; // Small helper enum enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), Value(Value), // For applications that can return a function, it's important to keep the remaining // arguments to apply them to the resulting function. @@ -365,7 +365,7 @@ pub(crate) fn apply_builtin( } } -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.as_whnf(); match &*f_borrow { ValueKind::Lam(x, _, e) => { @@ -456,7 +456,7 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), Expr(ExprKind), @@ -589,7 +589,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, -) -> ValueKind { +) -> ValueKind { use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, @@ -779,7 +779,10 @@ 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(b, args) => apply_builtin(b, args, ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), -- cgit v1.2.3 From 654d752c65f0e221d225ed045a0aee62f223855e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 16:05:47 +0000 Subject: Introduce a notion of binder --- dhall/src/semantics/phase/typecheck.rs | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 2e1cc02..926598d 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -4,11 +4,9 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; +use crate::semantics::{Binder, Shift, Subst, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, @@ -17,12 +15,12 @@ use crate::syntax::{ fn tck_pi_type( ctx: &TyCtx, - x: Label, + binder: Binder, tx: Value, te: Value, ) -> Result { use TypeMessage::*; - let ctx2 = ctx.insert_type(&x, tx.clone()); + let ctx2 = ctx.insert_type(&binder, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, @@ -42,7 +40,7 @@ fn tck_pi_type( let k = function_check(ka, kb); Ok(Value::from_kind_and_type( - ValueKind::Pi(x.into(), tx, te), + ValueKind::Pi(binder, tx, te), Value::from_const(k), )) } @@ -307,21 +305,23 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { match e.as_ref() { Lam(var, annot, body) => { + let binder = ctx.new_binder(var); let annot = type_with(ctx, annot.clone())?; annot.normalize_nf(); - let ctx2 = ctx.insert_type(var, annot.clone()); + let ctx2 = ctx.insert_type(&binder, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; Ok(Value::from_kind_and_type( - ValueKind::Lam(var.clone().into(), annot.clone(), body), - tck_pi_type(ctx, var.clone(), annot, body_type)?, + ValueKind::Lam(binder.clone(), annot.clone(), body), + tck_pi_type(ctx, binder, annot, body_type)?, )) } Pi(x, ta, tb) => { + let binder = ctx.new_binder(x); let ta = type_with(ctx, ta.clone())?; - let ctx2 = ctx.insert_type(x, ta.clone()); + let ctx2 = ctx.insert_type(&binder, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(ctx, x.clone(), ta, tb) + tck_pi_type(ctx, binder, ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -331,7 +331,8 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { }; let v = type_with(ctx, v)?; - type_with(&ctx.insert_value(x, v.clone())?, e.clone()) + let binder = ctx.new_binder(x); + type_with(&ctx.insert_value(&binder, v.clone())?, e.clone()) } Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { @@ -496,7 +497,7 @@ fn type_last_layer( RetTypeOnly( tck_pi_type( ctx, - x.clone(), + ctx.new_binder(x), t.clone(), r.under_binder(x), )? -- cgit v1.2.3 From 8cbec8c75d9e52091bdfe28b60b6ee698d9c1392 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 17:23:21 +0000 Subject: Store corresponding binder id in AlphaVar --- dhall/src/semantics/phase/typecheck.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 926598d..7e408eb 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -494,10 +494,11 @@ fn type_last_layer( ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { + let x = ctx.new_binder(x); RetTypeOnly( tck_pi_type( ctx, - ctx.new_binder(x), + x.clone(), t.clone(), r.under_binder(x), )? -- cgit v1.2.3 From a030560e60c4ff1c724216f4a5640722eb89b227 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 21:38:34 +0000 Subject: Use binder ids to reconstruct variables in expr output --- dhall/src/semantics/phase/mod.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 104a1ba..5d17338 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -203,12 +203,6 @@ impl Shift for Normalized { } } -impl Subst for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Typed(self.0.subst_shift(var, val)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { -- cgit v1.2.3 From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 11:03:40 +0000 Subject: Remove Shift/Subst traits --- dhall/src/semantics/phase/mod.rs | 13 ------------- dhall/src/semantics/phase/normalize.rs | 1 - dhall/src/semantics/phase/typecheck.rs | 2 +- 3 files changed, 1 insertion(+), 15 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 5d17338..6afed88 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -191,18 +190,6 @@ impl Normalized { } } -impl Shift for Typed { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Typed(self.0.shift(delta, var)?)) - } -} - -impl Shift for Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Normalized(self.0.shift(delta, var)?)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7b4b37f..615b2ff 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,7 +3,6 @@ use std::convert::TryInto; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::Subst; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; use crate::syntax; diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 7e408eb..c77d9c4 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -use crate::semantics::{Binder, Shift, Subst, Value, ValueKind}; +use crate::semantics::{Binder, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, -- cgit v1.2.3 From 37acac4b972b38e8dbe2d174dae1031e5a8eda67 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 16:09:35 +0000 Subject: Tweak: handle empty lists in typeck --- dhall/src/semantics/phase/normalize.rs | 20 ++++---------------- dhall/src/semantics/phase/typecheck.rs | 14 ++++++++++---- 2 files changed, 14 insertions(+), 20 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 615b2ff..8f9a58a 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -590,9 +590,9 @@ pub(crate) fn normalize_one_layer( ty: &Value, ) -> ValueKind { use ValueKind::{ - AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, - IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, - UnionConstructor, UnionLit, UnionType, + BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, + NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, + UnionLit, UnionType, }; let ret = match expr { @@ -609,6 +609,7 @@ pub(crate) fn normalize_one_layer( | ExprKind::Builtin(_) | ExprKind::Var(_) | ExprKind::Annot(_, _) + | ExprKind::EmptyListLit(_) | ExprKind::RecordType(_) | ExprKind::UnionType(_) => { unreachable!("This case should have been handled in typecheck") @@ -620,19 +621,6 @@ pub(crate) fn normalize_one_layer( ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), - ExprKind::EmptyListLit(ref t) => { - // Check if the type is of the form `List x` - let t_borrow = t.as_whnf(); - match &*t_borrow { - AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueKind(EmptyListLit(args[0].clone())) - } - _ => { - drop(t_borrow); - Ret::Expr(expr) - } - } - } ExprKind::NEListLit(elts) => { Ret::ValueKind(NEListLit(elts.into_iter().collect())) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index c77d9c4..852f41b 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -433,12 +433,18 @@ fn type_last_layer( RetTypeOnly(y.get_type()?) } EmptyListLit(t) => { - match &*t.as_whnf() { + let arg = match &*t.as_whnf() { ValueKind::AppliedBuiltin(syntax::Builtin::List, args) - if args.len() == 1 => {} + if args.len() == 1 => + { + args[0].clone() + } _ => return mkerr(InvalidListType(t.clone())), - } - RetTypeOnly(t.clone()) + }; + RetWhole(Value::from_kind_and_type( + ValueKind::EmptyListLit(arg), + t.clone(), + )) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); -- cgit v1.2.3 From b7d847cc812e6a7ce52354b15a9ed6b41ffeb3b4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 18:57:52 +0000 Subject: Simplify --- dhall/src/semantics/phase/normalize.rs | 9 ++++----- dhall/src/semantics/phase/typecheck.rs | 22 +++++++++++----------- 2 files changed, 15 insertions(+), 16 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f9a58a..541a196 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; +use crate::semantics::{AlphaVar, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -367,9 +366,9 @@ pub(crate) fn apply_builtin( pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueKind::Lam(x, _, e) => { - e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) - } + ValueKind::Lam(_, _, e) => e + .subst_shift(&AlphaVar::default(), &a) + .to_whnf_check_type(ty), ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 852f41b..15025c1 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -use crate::semantics::{Binder, Value, ValueKind}; +use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, @@ -385,15 +385,15 @@ fn type_last_layer( App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (x, tx, tb) = match &*tf_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*tf_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - let ret = tb.subst_shift(&x.into(), a); + let ret = tb.subst_shift(&AlphaVar::default(), a); ret.normalize_nf(); RetTypeOnly(ret) } @@ -500,13 +500,12 @@ fn type_last_layer( ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - let x = ctx.new_binder(x); RetTypeOnly( tck_pi_type( ctx, - x.clone(), + ctx.new_binder(x), t.clone(), - r.under_binder(x), + r.under_binder(), )? ) }, @@ -719,8 +718,8 @@ fn type_last_layer( // Union alternative with type Some(Some(variant_type)) => { let handler_type_borrow = handler_type.as_whnf(); - let (x, tx, tb) = match &*handler_type_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*handler_type_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -736,8 +735,9 @@ fn type_last_layer( )); } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { + // Extract `tb` from under the binder. Fails if the variable was used + // in `tb`. + match tb.over_binder() { Some(x) => x, None => return mkerr( MergeHandlerReturnTypeMustNotBeDependent, -- cgit v1.2.3 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/phase/mod.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 6afed88..4dc91e7 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -38,6 +37,15 @@ pub struct Typed(Value); #[derive(Debug, Clone)] pub struct Normalized(Typed); +/// Controls conversion from `Value` to `Expr` +#[derive(Copy, Clone)] +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + impl Parsed { pub fn parse_file(f: &Path) -> Result { parse::parse_file(f) -- 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/phase/normalize.rs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 541a196..f0a6a8c 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -374,9 +374,13 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args, ty) } - ValueKind::UnionConstructor(l, kts) => { - ValueKind::UnionLit(l.clone(), a, kts.clone()) - } + 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)) @@ -692,9 +696,11 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - UnionType(kts) => { - Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) - } + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), _ => { drop(v_borrow); Ret::Expr(expr) @@ -710,7 +716,8 @@ pub(crate) fn normalize_one_layer( let handlers_borrow = handlers.as_whnf(); let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) + { Some(h) => Ret::Value(h.clone()), None => { drop(handlers_borrow); @@ -718,7 +725,7 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { Some(h) => Ret::Value(h.app(v.clone())), None => { drop(handlers_borrow); -- 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/phase/typecheck.rs | 42 ++++++++++------------------------ 1 file changed, 12 insertions(+), 30 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 15025c1..9e41f1e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -14,27 +14,20 @@ use crate::syntax::{ }; fn tck_pi_type( - ctx: &TyCtx, binder: Binder, tx: Value, te: Value, ) -> Result { use TypeMessage::*; - let ctx2 = ctx.insert_type(&binder, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), + _ => return Err(TypeError::new(InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - &ctx2, - InvalidOutputType(te.get_type()?), - )) - } + _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))), }; let k = function_check(ka, kb); @@ -46,7 +39,6 @@ fn tck_pi_type( } fn tck_record_type( - ctx: &TyCtx, kts: impl IntoIterator>, ) -> Result { use std::collections::hash_map::Entry; @@ -59,13 +51,13 @@ fn tck_record_type( // Construct the union of the contained `Const`s match t.get_type()?.as_const() { Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), + None => return Err(TypeError::new(InvalidFieldType(x, t))), } // Check for duplicated entries let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, RecordTypeDuplicateField)) + return Err(TypeError::new(RecordTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -77,7 +69,7 @@ fn tck_record_type( )) } -fn tck_union_type(ctx: &TyCtx, kts: Iter) -> Result +fn tck_union_type(kts: Iter) -> Result where Iter: IntoIterator), TypeError>>, { @@ -93,17 +85,14 @@ where (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x, t.clone()), - )) + return Err(TypeError::new(InvalidFieldType(x, t.clone()))) } } } let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, UnionTypeDuplicateField)) + return Err(TypeError::new(UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -313,7 +302,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let body_type = body.get_type()?; Ok(Value::from_kind_and_type( ValueKind::Lam(binder.clone(), annot.clone(), body), - tck_pi_type(ctx, binder, annot, body_type)?, + tck_pi_type(binder, annot, body_type)?, )) } Pi(x, ta, tb) => { @@ -321,7 +310,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(&binder, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(ctx, binder, ta, tb) + tck_pi_type(binder, ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -337,9 +326,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), - None => { - Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span))) - } + None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), }, e => { // Typecheck recursively all subexpressions @@ -364,7 +351,7 @@ fn type_last_layer( use syntax::Const::Type; use syntax::ExprKind::*; use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); + let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); /// Intermediary return type enum Ret { @@ -474,15 +461,12 @@ fn type_last_layer( RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) } RecordType(kts) => RetWhole(tck_record_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), UnionType(kts) => RetWhole(tck_union_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), RecordLit(kvs) => RetTypeOnly(tck_record_type( - ctx, kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), )?), Field(r, x) => { @@ -502,7 +486,6 @@ fn type_last_layer( Some(Some(t)) => { RetTypeOnly( tck_pi_type( - ctx, ctx.new_binder(x), t.clone(), r.under_binder(), @@ -577,7 +560,6 @@ fn type_last_layer( // Construct the final record type from the union RetTypeOnly(tck_record_type( - ctx, kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), )?) } @@ -627,7 +609,7 @@ fn type_last_layer( }, )?; - RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) + RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { -- 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/phase/normalize.rs | 85 +++++++++++++++++++++++++++++++++- 1 file changed, 84 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f0a6a8c..7fd76df 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,9 +1,12 @@ use std::collections::HashMap; use std::convert::TryInto; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{ + AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -786,3 +789,83 @@ pub(crate) fn normalize_whnf( v => v, } } + +#[derive(Debug, Clone)] +enum NzEnvItem { + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec, +} + +impl NzEnv { + pub fn new() -> Self { + NzEnv { items: Vec::new() } + } + + pub fn insert_type(&self, t: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Kept(t)); + env + } + pub fn insert_value(&self, e: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Replaced(e)); + env + } + pub fn lookup_val(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( + ValueKind::Var(var.clone(), NzVar::new(idx)), + ty.clone(), + ), + NzEnvItem::Replaced(x) => x.clone(), + } + } +} + +/// Normalize a TyExpr into WHNF +pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { + let kind = match e.kind() { + TyExprKind::Var(var) => return env.lookup_val(var), + TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + ValueKind::LamClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + ValueKind::PiClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(e) => { + let e = e.map_ref(|tye| tye.normalize_whnf(env)); + match e { + ExprKind::App(f, arg) => { + let f_borrow = f.as_whnf(); + match &*f_borrow { + ValueKind::LamClosure { closure, .. } => { + return closure.apply(arg) + } + _ => { + drop(f_borrow); + ValueKind::PartialExpr(ExprKind::App(f, arg)) + } + } + } + _ => ValueKind::PartialExpr(e), + } + } + }; + Value::from_kind_and_type_whnf(kind, e.get_type().unwrap()) +} -- cgit v1.2.3 From fccccac6463cb3ca91206d5c41bbf51fc2ec4e0f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 16:01:08 +0000 Subject: Reuse normalize_one_layer in new eval flow --- dhall/src/semantics/phase/normalize.rs | 68 ++++++++++++++++++++-------------- 1 file changed, 41 insertions(+), 27 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7fd76df..75d61d5 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,9 @@ use std::collections::HashMap; use std::convert::TryInto; use crate::semantics::nze::NzVar; -use crate::semantics::phase::typecheck::{rc, typecheck}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, const_to_value, rc, typecheck, +}; use crate::semantics::phase::Normalized; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, @@ -372,6 +374,9 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::Lam(_, _, e) => e .subst_shift(&AlphaVar::default(), &a) .to_whnf_check_type(ty), + ValueKind::LamClosure { closure, .. } => { + closure.apply(a).to_whnf_check_type(ty) + } ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); @@ -597,8 +602,8 @@ pub(crate) fn normalize_one_layer( ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, - UnionLit, UnionType, + NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, + UnionConstructor, UnionLit, UnionType, }; let ret = match expr { @@ -611,15 +616,12 @@ pub(crate) fn normalize_one_layer( | ExprKind::Pi(_, _, _) | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Const(_) - | ExprKind::Builtin(_) | ExprKind::Var(_) - | ExprKind::Annot(_, _) - | ExprKind::EmptyListLit(_) - | ExprKind::RecordType(_) - | ExprKind::UnionType(_) => { + | ExprKind::Annot(_, _) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Const(c) => Ret::Value(const_to_value(c)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -627,12 +629,29 @@ pub(crate) fn normalize_one_layer( 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.as_whnf() { + ValueKind::AppliedBuiltin(syntax::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()); @@ -665,6 +684,13 @@ pub(crate) fn normalize_one_layer( } } } + // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { } + // ExprKind::BinOp(Equivalence, l, r) => { + // RetWhole(Value::from_kind_and_type( + // ValueKind::Equivalence(l.clone(), r.clone()), + // Value::from_const(Type), + // )) + // } ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), @@ -831,8 +857,9 @@ impl NzEnv { } /// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { - let kind = match e.kind() { +pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { + let ty = tye.get_type().unwrap(); + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { ValueKind::LamClosure { @@ -850,22 +877,9 @@ pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - match e { - ExprKind::App(f, arg) => { - let f_borrow = f.as_whnf(); - match &*f_borrow { - ValueKind::LamClosure { closure, .. } => { - return closure.apply(arg) - } - _ => { - drop(f_borrow); - ValueKind::PartialExpr(ExprKind::App(f, arg)) - } - } - } - _ => ValueKind::PartialExpr(e), - } + normalize_one_layer(e, &ty) } }; - Value::from_kind_and_type_whnf(kind, e.get_type().unwrap()) + + Value::from_kind_and_type_whnf(kind, ty) } -- cgit v1.2.3 From bd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 16:29:25 +0000 Subject: Restore all types in Value::to_tyexpr --- dhall/src/semantics/phase/normalize.rs | 18 +++++++++++++----- dhall/src/semantics/phase/typecheck.rs | 12 +++++++----- 2 files changed, 20 insertions(+), 10 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 75d61d5..8f3953d 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -71,6 +71,7 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, + types: Vec, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -364,7 +365,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args), + Ret::DoneAsIs => AppliedBuiltin(b, args, types), } } @@ -377,10 +378,15 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(b, args, types) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args, ty) + let types = types + .iter() + .cloned() + .chain(once(f.get_type().unwrap())) + .collect(); + apply_builtin(*b, args, ty, types) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -631,7 +637,7 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => { args[0].clone() @@ -806,7 +812,9 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueKind::AppliedBuiltin(b, args, types) => { + apply_builtin(b, args, ty, types) + } ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 9e41f1e..f2d1bf2 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -421,7 +421,7 @@ fn type_last_layer( } EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => { args[0].clone() @@ -613,7 +613,7 @@ fn type_last_layer( } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _) => {} + ValueKind::AppliedBuiltin(List, _, _) => {} _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } @@ -679,9 +679,11 @@ fn type_last_layer( let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(syntax::Builtin::Optional, args) - if args.len() == 1 => - { + ValueKind::AppliedBuiltin( + syntax::Builtin::Optional, + args, + _, + ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); kts.insert("None".into(), None); -- cgit v1.2.3 From 700ff482fbff8960bc0e792fec6fd538c5428d70 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 17:07:56 +0000 Subject: Normalize more expressions --- dhall/src/semantics/phase/normalize.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f3953d..ac60ce0 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -594,10 +594,14 @@ fn apply_binop<'a>( Ret::ValueKind(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { + (RecursiveRecordTypeMerge, _, _) => { unreachable!("This case should have been handled in typecheck") } + (Equivalence, _, _) => { + Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) + } + _ => return None, }) } @@ -690,13 +694,6 @@ pub(crate) fn normalize_one_layer( } } } - // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { } - // ExprKind::BinOp(Equivalence, l, r) => { - // RetWhole(Value::from_kind_and_type( - // ValueKind::Equivalence(l.clone(), r.clone()), - // Value::from_const(Type), - // )) - // } ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), -- 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/phase/normalize.rs | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ac60ce0..3ddfb84 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -12,8 +12,8 @@ use crate::semantics::{ use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, - Label, NaiveDouble, + BinOp, Builtin, Const, ExprKind, InterpolatedText, + InterpolatedTextContents, Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -822,7 +822,7 @@ pub(crate) fn normalize_whnf( } #[derive(Debug, Clone)] -enum NzEnvItem { +pub(crate) enum NzEnvItem { // Variable is bound with given type Kept(Value), // Variable has been replaced by corresponding value @@ -838,6 +838,9 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } + pub fn construct(items: Vec) -> Self { + NzEnv { items } + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -851,9 +854,16 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); + let var_idx = self.items[..idx] + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(var.clone(), NzVar::new(var_idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), @@ -863,7 +873,11 @@ impl NzEnv { /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = tye.get_type().unwrap(); + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return Value::from_const(Const::Sort), + }; + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { -- cgit v1.2.3 From b72f0968ac19058b9cc513ab0ed1785133232a3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 21:33:21 +0000 Subject: Implement basic typecheck with new approach --- dhall/src/semantics/phase/normalize.rs | 1 + 1 file changed, 1 insertion(+) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 3ddfb84..e848601 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,3 +1,4 @@ +#![allow(dead_code)] use std::collections::HashMap; use std::convert::TryInto; -- cgit v1.2.3 From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:15:17 +0000 Subject: Typecheck more cases --- dhall/src/semantics/phase/normalize.rs | 13 ++++++++++--- dhall/src/semantics/phase/typecheck.rs | 11 +++++++++-- 2 files changed, 19 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index e848601..066a004 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -625,12 +625,14 @@ pub(crate) fn normalize_one_layer( // `RetWhole`), so they won't appear here. ExprKind::Lam(_, _, _) | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) => { + | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Let(_, _, val, body) => { + Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) + } + ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), @@ -895,11 +897,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { closure: Closure::new(env, body.clone()), } } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.normalize_whnf(env); + return body.normalize_whnf(&env.insert_value(val)); + } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); normalize_one_layer(e, &ty) } }; + // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f2d1bf2..0f3754e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -189,7 +189,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr { +pub(crate) fn type_of_builtin(b: Builtin) -> Expr { use syntax::Builtin::*; rc(match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -321,7 +321,14 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let v = type_with(ctx, v)?; let binder = ctx.new_binder(x); - type_with(&ctx.insert_value(&binder, v.clone())?, e.clone()) + let e = + type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?; + // let e_ty = e.get_type()?; + // Ok(Value::from_kind_and_type( + // ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)), + // e_ty, + // )) + Ok(e) } Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { -- cgit v1.2.3 From f2e8c414993d5c9fcc63f5c035f755712c01dad0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:20:53 +0000 Subject: Enable comparing Closures for equality --- dhall/src/semantics/phase/normalize.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 066a004..7f547d7 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -884,17 +884,20 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + let annot = annot.normalize_whnf(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), - annot: annot.normalize_whnf(env), - closure: Closure::new(env, body.clone()), + annot: annot.clone(), + closure: Closure::new(annot, env, body.clone()), } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = annot.normalize_whnf(env); + let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), - annot: annot.normalize_whnf(env), - closure: Closure::new(env, body.clone()), + annot, + closure, } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { -- cgit v1.2.3 From 8c64ae33149db4edaaa89d2d187baf10a2b9f8bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 13:29:27 +0000 Subject: Make most type errors stringy --- dhall/src/semantics/phase/typecheck.rs | 151 ++++++++++++--------------------- 1 file changed, 53 insertions(+), 98 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 0f3754e..44678cd 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -357,8 +357,8 @@ fn type_last_layer( use syntax::Builtin::*; use syntax::Const::Type; use syntax::ExprKind::*; - use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); + let mkerr = + |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string()))); /// Intermediary return type enum Ret { @@ -381,10 +381,10 @@ fn type_last_layer( let tf_borrow = tf.as_whnf(); let (tx, tb) = match &*tf_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => return mkerr(NotAFunction(f.clone())), + _ => return mkerr("NotAFunction"), }; if &a.get_type()? != tx { - return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); + return mkerr("TypeMismatch"); } let ret = tb.subst_shift(&AlphaVar::default(), a); @@ -393,35 +393,33 @@ fn type_last_layer( } Annot(x, t) => { if &x.get_type()? != t { - return mkerr(AnnotMismatch(x.clone(), t.clone())); + return mkerr("AnnotMismatch"); } RetWhole(x.clone()) } Assert(t) => { match &*t.as_whnf() { ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(x, y) => { - return mkerr(AssertMismatch(x.clone(), y.clone())) - } - _ => return mkerr(AssertMustTakeEquivalence), + ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), + _ => return mkerr("AssertMustTakeEquivalence"), } RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { - return mkerr(InvalidPredicate(x.clone())); + return mkerr("InvalidPredicate"); } if y.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(true, y.clone())); + return mkerr("IfBranchMustBeTerm"); } if z.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(false, z.clone())); + return mkerr("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { - return mkerr(IfBranchMismatch(y.clone(), z.clone())); + return mkerr("IfBranchMismatch"); } RetTypeOnly(y.get_type()?) @@ -433,7 +431,7 @@ fn type_last_layer( { args[0].clone() } - _ => return mkerr(InvalidListType(t.clone())), + _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( ValueKind::EmptyListLit(arg), @@ -443,18 +441,14 @@ fn type_last_layer( NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); - for (i, y) in iter { + for (_, y) in iter { if x.get_type()? != y.get_type()? { - return mkerr(InvalidListElement( - i, - x.get_type()?, - y.clone(), - )); + return mkerr("InvalidListElement"); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t)); + return mkerr("InvalidListType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) @@ -462,7 +456,7 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidOptionalType(t)); + return mkerr("InvalidOptionalType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) @@ -479,48 +473,25 @@ fn type_last_layer( Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => { - RetTypeOnly(tth.clone()) - }, - None => return mkerr(MissingRecordField(x.clone(), - r.clone())), + Some(tth) => RetTypeOnly(tth.clone()), + None => return mkerr("MissingRecordField"), }, // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > - Some(Some(t)) => { - RetTypeOnly( - tck_pi_type( - ctx.new_binder(x), - t.clone(), - r.under_binder(), - )? - ) - }, - Some(None) => { - RetTypeOnly(r.clone()) - }, - None => { - return mkerr(MissingUnionField( - x.clone(), - r.clone(), - )) - }, - }, - _ => { - return mkerr(NotARecord( - x.clone(), - r.clone() - )) + Some(Some(t)) => RetTypeOnly(tck_pi_type( + ctx.new_binder(x), + t.clone(), + r.under_binder(), + )?), + Some(None) => RetTypeOnly(r.clone()), + None => return mkerr("MissingUnionField"), }, + _ => return mkerr("NotARecord"), } - } - // _ => mkerr(NotARecord( - // x, - // r?, - // )), + } // _ => mkerr("NotARecord"), } } Const(c) => RetWhole(const_to_value(*c)), @@ -535,7 +506,7 @@ fn type_last_layer( use InterpolatedTextContents::Expr; if let Expr(x) = contents { if x.get_type()? != text_type { - return mkerr(InvalidTextInterpolation(x.clone())); + return mkerr("InvalidTextInterpolation"); } } } @@ -549,14 +520,14 @@ fn type_last_layer( let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(l.clone())), + _ => return mkerr("MustCombineRecord"), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(r.clone())), + _ => return mkerr("MustCombineRecord"), }; // Union the two records, prefering @@ -584,18 +555,14 @@ fn type_last_layer( let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Ensure that the records combine without a type error @@ -618,28 +585,28 @@ fn type_last_layer( RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } - BinOp(o @ ListAppend, l, r) => { + BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { ValueKind::AppliedBuiltin(List, _, _) => {} - _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), + _ => return mkerr("BinOpTypeMismatch"), } if l.get_type()? != r.get_type()? { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(l.get_type()?) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if r.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if l.get_type()? != r.get_type()? { - return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); + return mkerr("EquivalenceTypeMismatch"); } RetWhole(Value::from_kind_and_type( @@ -665,11 +632,11 @@ fn type_last_layer( }); if l.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, l.clone())); + return mkerr("BinOpTypeMismatch"); } if r.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(t) @@ -679,7 +646,7 @@ fn type_last_layer( let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), + _ => return mkerr("Merge1ArgMustBeRecord"), }; let union_type = union.get_type()?; @@ -697,9 +664,7 @@ fn type_last_layer( kts.insert("Some".into(), Some(ty.clone())); Cow::Owned(kts) } - _ => { - return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone())) - } + _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), }; let mut inferred_type = None; @@ -711,19 +676,11 @@ fn type_last_layer( let handler_type_borrow = handler_type.as_whnf(); let (tx, tb) = match &*handler_type_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => { - return mkerr(NotAFunction( - handler_type.clone(), - )) - } + _ => return mkerr("NotAFunction"), }; if variant_type != tx { - return mkerr(TypeMismatch( - handler_type.clone(), - tx.clone(), - variant_type.clone(), - )); + return mkerr("TypeMismatch"); } // Extract `tb` from under the binder. Fails if the variable was used @@ -731,41 +688,39 @@ fn type_last_layer( match tb.over_binder() { Some(x) => x, None => return mkerr( - MergeHandlerReturnTypeMustNotBeDependent, + "MergeHandlerReturnTypeMustNotBeDependent", ), } } // Union alternative without type Some(None) => handler_type.clone(), - None => { - return mkerr(MergeHandlerMissingVariant(x.clone())) - } + None => return mkerr("MergeHandlerMissingVariant"), }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - return mkerr(MergeHandlerTypeMismatch); + return mkerr("MergeHandlerTypeMismatch"); } } } } for x in variants.keys() { if !handlers.contains_key(x) { - return mkerr(MergeVariantMissingHandler(x.clone())); + return mkerr("MergeVariantMissingHandler"); } } match (inferred_type, type_annot.as_ref()) { (Some(t1), Some(t2)) => { if &t1 != t2 { - return mkerr(MergeAnnotMismatch); + return mkerr("MergeAnnotMismatch"); } RetTypeOnly(t1) } (Some(t), None) => RetTypeOnly(t), (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr(MergeEmptyNeedsAnnotation), + (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), } } ToMap(_, _) => unimplemented!("toMap"), @@ -774,18 +729,18 @@ fn type_last_layer( let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(ProjectionMustBeRecord), + _ => return mkerr("ProjectionMustBeRecord"), }; let mut new_kts = HashMap::new(); for l in labels { match kts.get(l) { - None => return mkerr(ProjectionMissingEntry), + None => return mkerr("ProjectionMissingEntry"), Some(t) => { use std::collections::hash_map::Entry; match new_kts.entry(l.clone()) { Entry::Occupied(_) => { - return mkerr(ProjectionDuplicateField) + return mkerr("ProjectionDuplicateField") } Entry::Vacant(e) => e.insert(t.clone()), } -- cgit v1.2.3 From 574fb56e87c1a71dc8d7efbff2789d3cfabdc529 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 13:51:24 +0000 Subject: More typecheck --- dhall/src/semantics/phase/normalize.rs | 19 ++++++- dhall/src/semantics/phase/typecheck.rs | 101 +++++++++++++++++---------------- 2 files changed, 70 insertions(+), 50 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7f547d7..33e1f2b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -595,8 +595,23 @@ fn apply_binop<'a>( Ret::ValueKind(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) => { - unreachable!("This case should have been handled in typecheck") + (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, _, _) => { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 44678cd..1aab736 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -356,7 +356,6 @@ fn type_last_layer( use syntax::BinOp::*; use syntax::Builtin::*; use syntax::Const::Type; - use syntax::ExprKind::*; let mkerr = |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string()))); @@ -370,13 +369,15 @@ fn type_last_layer( use Ret::*; let ret = match &e { - Import(_) => unreachable!( + ExprKind::Import(_) => unreachable!( "There should remain no imports in a resolved expression" ), - Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => { - unreachable!() - } - App(f, a) => { + ExprKind::Lam(_, _, _) + | ExprKind::Pi(_, _, _) + | ExprKind::Let(_, _, _, _) + | ExprKind::Embed(_) + | ExprKind::Var(_) => unreachable!(), + ExprKind::App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); let (tx, tb) = match &*tf_borrow { @@ -391,13 +392,13 @@ fn type_last_layer( ret.normalize_nf(); RetTypeOnly(ret) } - Annot(x, t) => { + ExprKind::Annot(x, t) => { if &x.get_type()? != t { return mkerr("AnnotMismatch"); } RetWhole(x.clone()) } - Assert(t) => { + ExprKind::Assert(t) => { match &*t.as_whnf() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), @@ -405,16 +406,16 @@ fn type_last_layer( } RetTypeOnly(t.clone()) } - BoolIf(x, y, z) => { + ExprKind::BoolIf(x, y, z) => { if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { return mkerr("InvalidPredicate"); } - if y.get_type()?.get_type()?.as_const() != Some(Type) { + if y.get_type()?.get_type()?.as_const() != Some(Const::Type) { return mkerr("IfBranchMustBeTerm"); } - if z.get_type()?.get_type()?.as_const() != Some(Type) { + if z.get_type()?.get_type()?.as_const() != Some(Const::Type) { return mkerr("IfBranchMustBeTerm"); } @@ -424,7 +425,7 @@ fn type_last_layer( RetTypeOnly(y.get_type()?) } - EmptyListLit(t) => { + ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => @@ -438,7 +439,7 @@ fn type_last_layer( t.clone(), )) } - NEListLit(xs) => { + ExprKind::NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); for (_, y) in iter { @@ -447,30 +448,30 @@ fn type_last_layer( } } let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { + if t.get_type()?.as_const() != Some(Const::Type) { return mkerr("InvalidListType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) } - SomeLit(x) => { + ExprKind::SomeLit(x) => { let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { + if t.get_type()?.as_const() != Some(Const::Type) { return mkerr("InvalidOptionalType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) } - RecordType(kts) => RetWhole(tck_record_type( + ExprKind::RecordType(kts) => RetWhole(tck_record_type( kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), - UnionType(kts) => RetWhole(tck_union_type( + ExprKind::UnionType(kts) => RetWhole(tck_union_type( kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), - RecordLit(kvs) => RetTypeOnly(tck_record_type( + ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type( kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), )?), - Field(r, x) => { + ExprKind::Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => RetTypeOnly(tth.clone()), @@ -494,13 +495,13 @@ fn type_last_layer( } // _ => mkerr("NotARecord"), } } - Const(c) => RetWhole(const_to_value(*c)), - Builtin(b) => RetWhole(builtin_to_value(*b)), - BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), - NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), - IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), - DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), - TextLit(interpolated) => { + ExprKind::Const(c) => RetWhole(const_to_value(*c)), + ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)), + ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), + ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), + ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), + ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), + ExprKind::TextLit(interpolated) => { let text_type = builtin_to_value(Text); for contents in interpolated.iter() { use InterpolatedTextContents::Expr; @@ -512,7 +513,7 @@ fn type_last_layer( } RetTypeOnly(text_type) } - BinOp(RightBiasedRecordMerge, l, r) => { + ExprKind::BinOp(RightBiasedRecordMerge, l, r) => { let l_type = l.get_type()?; let r_type = r.get_type()?; @@ -541,16 +542,18 @@ fn type_last_layer( kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), )?) } - BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( - ctx, - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.get_type()?, - r.get_type()?, - ), - Span::Artificial, - )?), - BinOp(RecursiveRecordTypeMerge, l, r) => { + ExprKind::BinOp(RecursiveRecordMerge, l, r) => { + RetTypeOnly(type_last_layer( + ctx, + ExprKind::BinOp( + RecursiveRecordTypeMerge, + l.get_type()?, + r.get_type()?, + ), + Span::Artificial, + )?) + } + ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { // Extract the LHS record type let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { @@ -585,7 +588,7 @@ fn type_last_layer( RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } - BinOp(ListAppend, l, r) => { + ExprKind::BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { ValueKind::AppliedBuiltin(List, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), @@ -597,11 +600,11 @@ fn type_last_layer( RetTypeOnly(l.get_type()?) } - BinOp(Equivalence, l, r) => { - if l.get_type()?.get_type()?.as_const() != Some(Type) { + ExprKind::BinOp(Equivalence, l, r) => { + if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { return mkerr("EquivalenceArgumentMustBeTerm"); } - if r.get_type()?.get_type()?.as_const() != Some(Type) { + if r.get_type()?.get_type()?.as_const() != Some(Const::Type) { return mkerr("EquivalenceArgumentMustBeTerm"); } @@ -614,7 +617,7 @@ fn type_last_layer( Value::from_const(Type), )) } - BinOp(o, l, r) => { + ExprKind::BinOp(o, l, r) => { let t = builtin_to_value(match o { BoolAnd => Bool, BoolOr => Bool, @@ -641,7 +644,7 @@ fn type_last_layer( RetTypeOnly(t) } - Merge(record, union, type_annot) => { + ExprKind::Merge(record, union, type_annot) => { let record_type = record.get_type()?; let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { @@ -723,8 +726,8 @@ fn type_last_layer( (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), } } - ToMap(_, _) => unimplemented!("toMap"), - Projection(record, labels) => { + ExprKind::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::Projection(record, labels) => { let record_type = record.get_type()?; let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { @@ -753,8 +756,10 @@ fn type_last_layer( record_type.get_type()?, )) } - ProjectionByExpr(_, _) => unimplemented!("selection by expression"), - Completion(_, _) => unimplemented!("record completion"), + ExprKind::ProjectionByExpr(_, _) => { + unimplemented!("selection by expression") + } + ExprKind::Completion(_, _) => unimplemented!("record completion"), }; Ok(match ret { -- 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/phase/mod.rs | 5 +++++ dhall/src/semantics/phase/normalize.rs | 5 ++++- dhall/src/semantics/phase/resolve.rs | 8 ++++++-- dhall/src/semantics/phase/typecheck.rs | 26 ++++++++++++++++---------- 4 files changed, 31 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 4dc91e7..67cdc91 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -89,6 +89,11 @@ impl Resolved { pub fn to_expr(&self) -> ResolvedExpr { self.0.clone() } + pub fn tck_and_normalize_new_flow(&self) -> Result { + let val = crate::semantics::tck::typecheck::typecheck(&self.0)? + .normalize_whnf_noenv(); + Ok(Normalized(Typed(val))) + } } impl Typed { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 33e1f2b..5fc72fc 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::NzVar; +use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ builtin_to_value, const_to_value, rc, typecheck, }; @@ -859,6 +859,9 @@ impl NzEnv { pub fn construct(items: Vec) -> Self { NzEnv { items } } + pub fn as_quoteenv(&self) -> QuoteEnv { + QuoteEnv::construct(self.items.len()) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index cc4a024..64106aa 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -52,10 +52,14 @@ fn load_import( import_cache: &mut ImportCache, import_stack: &ImportStack, ) -> Result { + // Ok( + // do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? + // .typecheck()? + // .normalize(), + // ) Ok( do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - .typecheck()? - .normalize(), + .tck_and_normalize_new_flow()?, ) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 1aab736..18e70e4 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { pub(crate) fn builtin_to_value(b: Builtin) -> Value { Value::from_kind_and_type( ValueKind::from_builtin(b), - typecheck(type_of_builtin(b)).unwrap(), + crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) + .unwrap() + .normalize_whnf_noenv(), ) } @@ -380,17 +382,21 @@ fn type_last_layer( ExprKind::App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (tx, tb) = match &*tf_borrow { - ValueKind::Pi(_, tx, tb) => (tx, tb), + match &*tf_borrow { + ValueKind::Pi(_, tx, tb) => { + if &a.get_type()? != tx { + return mkerr("TypeMismatch"); + } + + let ret = tb.subst_shift(&AlphaVar::default(), a); + ret.normalize_nf(); + RetTypeOnly(ret) + } + ValueKind::PiClosure { closure, .. } => { + RetTypeOnly(closure.apply(a.clone())) + } _ => return mkerr("NotAFunction"), - }; - if &a.get_type()? != tx { - return mkerr("TypeMismatch"); } - - let ret = tb.subst_shift(&AlphaVar::default(), a); - ret.normalize_nf(); - RetTypeOnly(ret) } ExprKind::Annot(x, t) => { if &x.get_type()? != t { -- 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/phase/normalize.rs | 70 ++++++++++++++++++++++------------ dhall/src/semantics/phase/typecheck.rs | 20 ++++++---- 2 files changed, 58 insertions(+), 32 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 5fc72fc..a11cb75 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -4,9 +4,11 @@ use std::convert::TryInto; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ - builtin_to_value, const_to_value, rc, typecheck, + builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; +use crate::semantics::tck::typecheck::type_with; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; @@ -73,6 +75,7 @@ pub(crate) fn apply_builtin( args: Vec, ty: &Value, types: Vec, + env: NzEnv, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -86,6 +89,11 @@ pub(crate) fn apply_builtin( ValueWithRemainingArgs(&'a [Value], Value), DoneAsIs, } + let make_closure = |e| { + type_with(&env.to_alpha_tyenv(), &e) + .unwrap() + .normalize_whnf(&env) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), @@ -272,13 +280,12 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(list_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> λ(as : List var(T)) -> [ var(a) ] # var(as) )) - .unwrap() .app(t.clone()), ) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), @@ -300,12 +307,11 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(optional_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> Some(var(a)) )) - .unwrap() .app(t.clone()), ) .app( @@ -326,13 +332,10 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app( - typecheck(make_closure!( - λ(x : Natural) -> - 1 + var(x) - )) - .unwrap(), - ) + .app(make_closure(make_closure!( + λ(x : Natural) -> + 1 + var(x) + ))) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), @@ -366,7 +369,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args, types), + Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), } } @@ -379,7 +382,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, env) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); let types = types @@ -387,7 +390,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { .cloned() .chain(once(f.get_type().unwrap())) .collect(); - apply_builtin(*b, args, ty, types) + apply_builtin(*b, args, ty, types, env.clone()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -625,6 +628,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, + env: &NzEnv, ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, @@ -649,7 +653,7 @@ pub(crate) fn normalize_one_layer( } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -659,11 +663,12 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -827,10 +832,10 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types) => { - apply_builtin(b, args, ty, types) + ValueKind::AppliedBuiltin(b, args, types, env) => { + apply_builtin(b, args, ty, types, env) } - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -862,6 +867,9 @@ impl NzEnv { pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv::construct(self.items.len()) } + pub fn to_alpha_tyenv(&self) -> TyEnv { + TyEnv::from_nzenv_alpha(self) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -890,6 +898,10 @@ impl NzEnv { NzEnvItem::Replaced(x) => x.clone(), } } + + pub fn size(&self) -> usize { + self.items.len() + } } /// Normalize a TyExpr into WHNF @@ -924,10 +936,18 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - normalize_one_layer(e, &ty) + normalize_one_layer(e, &ty, env) } }; // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } + +/// Ignore NzEnv when comparing +impl std::cmp::PartialEq for NzEnv { + fn eq(&self, _other: &Self) -> bool { + true + } +} +impl std::cmp::Eq for NzEnv {} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 18e70e4..f559323 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -5,6 +5,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; +use crate::semantics::phase::normalize::NzEnv; use crate::semantics::phase::Normalized; use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; @@ -278,8 +279,11 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { + builtin_to_value_env(b, &NzEnv::new()) +} +pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { Value::from_kind_and_type( - ValueKind::from_builtin(b), + ValueKind::from_builtin_env(b, env.clone()), crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) .unwrap() .normalize_whnf_noenv(), @@ -433,11 +437,12 @@ fn type_last_layer( } ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( @@ -596,7 +601,7 @@ fn type_last_layer( } ExprKind::BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _, _) => {} + ValueKind::AppliedBuiltin(List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -666,6 +671,7 @@ fn type_last_layer( syntax::Builtin::Optional, args, _, + _, ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); -- cgit v1.2.3 From 7683b0d762cf0df489ad4bc006e8db2358e81cf4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 21:50:04 +0000 Subject: Implement assert & merge and fix more bugs --- dhall/src/semantics/phase/normalize.rs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index a11cb75..532dae3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -855,17 +855,30 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, + vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { items: Vec::new() } + NzEnv { + items: Vec::new(), + vars: QuoteEnv::new(), + } } pub fn construct(items: Vec) -> Self { - NzEnv { items } + let vars = QuoteEnv::construct( + items + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(), + ); + NzEnv { items, vars } } pub fn as_quoteenv(&self) -> QuoteEnv { - QuoteEnv::construct(self.items.len()) + self.vars } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -874,6 +887,7 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); + env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { -- cgit v1.2.3 From f31ccaa40df77b1ca8b37db46a819460c831006e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:17:12 +0000 Subject: Fix more bugs --- dhall/src/semantics/phase/normalize.rs | 32 ++++---------------------------- 1 file changed, 4 insertions(+), 28 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 532dae3..f4e4099 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::{NzVar, QuoteEnv}; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; @@ -855,30 +855,14 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, - vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { - items: Vec::new(), - vars: QuoteEnv::new(), - } + NzEnv { items: Vec::new() } } pub fn construct(items: Vec) -> Self { - let vars = QuoteEnv::construct( - items - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(), - ); - NzEnv { items, vars } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.vars + NzEnv { items } } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -887,7 +871,6 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); - env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { @@ -897,16 +880,9 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); - let var_idx = self.items[..idx] - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(var_idx)), + ValueKind::Var(var.clone(), NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), -- cgit v1.2.3 From f88880004c7dcf5e67c4d5e2330e6e879523f27b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:30:12 +0000 Subject: Use Normalized in serde_dhall --- dhall/src/semantics/phase/mod.rs | 126 +++++++++++++++++++++++---------------- 1 file changed, 74 insertions(+), 52 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 67cdc91..68c32b2 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -35,7 +35,7 @@ pub struct Typed(Value); /// /// Invariant: the contained Typed expression must be in normal form, #[derive(Debug, Clone)] -pub struct Normalized(Typed); +pub struct Normalized(Value); /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -81,9 +81,8 @@ impl Resolved { pub fn typecheck(self) -> Result { Ok(typecheck::typecheck(self.0)?.into_typed()) } - pub fn typecheck_with(self, ty: &Typed) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())? - .into_typed()) + pub fn typecheck_with(self, ty: &Normalized) -> Result { + Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -92,39 +91,30 @@ impl Resolved { pub fn tck_and_normalize_new_flow(&self) -> Result { let val = crate::semantics::tck::typecheck::typecheck(&self.0)? .normalize_whnf_noenv(); - Ok(Normalized(Typed(val))) + Ok(Normalized(val)) } } impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(mut self) -> Normalized { - self.normalize_mut(); - Normalized(self) + self.0.normalize_mut(); + Normalized(self.0) } - pub(crate) fn from_const(c: Const) -> Self { - Typed(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { - Typed(Value::from_kind_and_type(v, t.into_value())) - } pub(crate) fn from_value(th: Value) -> Self { Typed(th) } - pub(crate) fn const_type() -> Self { - Typed::from_const(Const::Type) - } /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { + pub(crate) fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub fn normalize_to_expr(&self) -> NormalizedExpr { + pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, @@ -138,6 +128,34 @@ impl Typed { normalize: true, }) } + pub(crate) fn into_value(self) -> Value { + self.0 + } + + pub(crate) fn get_type(&self) -> Result { + Ok(self.0.get_type()?.into_typed()) + } +} + +impl Normalized { + pub fn encode(&self) -> Result, EncodeError> { + binary::encode(&self.to_expr()) + } + + pub fn to_expr(&self) -> NormalizedExpr { + // TODO: do it directly + self.to_typed().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { + // TODO: do it directly + self.to_typed().normalize_to_expr_alpha() + } + pub(crate) fn to_typed(&self) -> Typed { + Typed(self.0.clone()) + } + pub(crate) fn into_typed(self) -> Typed { + Typed(self.0) + } pub(crate) fn to_value(&self) -> Value { self.0.clone() } @@ -145,64 +163,58 @@ impl Typed { self.0 } - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() + pub(crate) fn from_const(c: Const) -> Self { + Normalized(Value::from_const(c)) } - - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + pub(crate) fn from_kind_and_type( + v: ValueKind, + t: Normalized, + ) -> Self { + Normalized(Value::from_kind_and_type(v, t.into_value())) + } + pub(crate) fn from_value(th: Value) -> Self { + Normalized(th) + } + pub(crate) fn const_type() -> Self { + Normalized::from_const(Const::Type) } pub fn make_builtin_type(b: Builtin) -> Self { - Typed::from_value(Value::from_builtin(b)) + Normalized::from_value(Value::from_builtin(b)) } - pub fn make_optional_type(t: Typed) -> Self { - Typed::from_value( + pub fn make_optional_type(t: Normalized) -> Self { + Normalized::from_value( Value::from_builtin(Builtin::Optional).app(t.to_value()), ) } - pub fn make_list_type(t: Typed) -> Self { - Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value())) + pub fn make_list_type(t: Normalized) -> Self { + Normalized::from_value( + Value::from_builtin(Builtin::List).app(t.to_value()), + ) } pub fn make_record_type( - kts: impl Iterator, + kts: impl Iterator, ) -> Self { - Typed::from_kind_and_type( + Normalized::from_kind_and_type( ValueKind::RecordType( kts.map(|(k, t)| (k.into(), t.into_value())).collect(), ), - Typed::const_type(), + Normalized::const_type(), ) } pub fn make_union_type( - kts: impl Iterator)>, + kts: impl Iterator)>, ) -> Self { - Typed::from_kind_and_type( + Normalized::from_kind_and_type( ValueKind::UnionType( kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) .collect(), ), - Typed::const_type(), + Normalized::const_type(), ) } } -impl Normalized { - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.to_expr()) - } - - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.0.normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.normalize_to_expr_alpha() - } - pub(crate) fn into_typed(self) -> Typed { - self.0 - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { @@ -226,7 +238,6 @@ macro_rules! derive_traits_for_wrapper_struct { derive_traits_for_wrapper_struct!(Parsed); derive_traits_for_wrapper_struct!(Resolved); -derive_traits_for_wrapper_struct!(Normalized); impl std::hash::Hash for Normalized { fn hash(&self, state: &mut H) @@ -245,9 +256,20 @@ impl PartialEq for Typed { self.0 == other.0 } } - impl Display for Typed { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) } } + +impl Eq for Normalized {} +impl PartialEq for Normalized { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } +} +impl Display for Normalized { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} -- cgit v1.2.3 From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/src/semantics/phase/mod.rs | 69 +++++++++++++--------------------- dhall/src/semantics/phase/typecheck.rs | 2 +- 2 files changed, 27 insertions(+), 44 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 68c32b2..0f8194c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,6 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; +use crate::semantics::tck::tyexpr::TyExpr; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(Value); +pub struct Typed(TyExpr); /// A normalized expression. /// @@ -78,11 +79,14 @@ impl Parsed { } impl Resolved { - pub fn typecheck(self) -> Result { - Ok(typecheck::typecheck(self.0)?.into_typed()) + pub fn typecheck(&self) -> Result { + Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) + Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( + &self.0, + ty.to_expr(), + )?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -97,43 +101,22 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(mut self) -> Normalized { - self.0.normalize_mut(); - Normalized(self.0) - } - - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) + pub fn normalize(&self) -> Normalized { + let mut val = self.0.normalize_whnf_noenv(); + val.normalize_mut(); + Normalized(val) } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self) -> ResolvedExpr { + fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } - /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the - /// process. - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + pub(crate) fn get_type(&self) -> Result { + Ok(Normalized(self.0.get_type()?)) } } @@ -142,19 +125,19 @@ impl Normalized { binary::encode(&self.to_expr()) } + /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr() + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) } + /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr_alpha() - } - pub(crate) fn to_typed(&self) -> Typed { - Typed(self.0.clone()) - } - pub(crate) fn into_typed(self) -> Typed { - Typed(self.0) + self.0.to_expr(ToExprOptions { + alpha: true, + normalize: false, + }) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.0 == other.0 + self.normalize() == other.normalize() } } impl Display for Typed { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f559323..6de65e8 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -336,7 +336,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { // )) Ok(e) } - Embed(p) => Ok(p.clone().into_typed().into_value()), + Embed(p) => Ok(p.clone().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), -- 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/phase/mod.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 0f8194c..2727a61 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -102,9 +102,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - let mut val = self.0.normalize_whnf_noenv(); - val.normalize_mut(); - Normalized(val) + Normalized(self.0.normalize_nf_noenv()) } /// Converts a value back to the corresponding AST expression. -- 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/phase/normalize.rs | 7 - dhall/src/semantics/phase/typecheck.rs | 624 +-------------------------------- 2 files changed, 2 insertions(+), 629 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f4e4099..d40456b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,4 +1,3 @@ -#![allow(dead_code)] use std::collections::HashMap; use std::convert::TryInto; @@ -376,9 +375,6 @@ pub(crate) fn apply_builtin( pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueKind::Lam(_, _, e) => e - .subst_shift(&AlphaVar::default(), &a) - .to_whnf_check_type(ty), ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } @@ -861,9 +857,6 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } - pub fn construct(items: Vec) -> Self { - NzEnv { items } - } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 6de65e8..4392365 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,122 +1,10 @@ -use std::borrow::Cow; -use std::cmp::max; -use std::collections::HashMap; - -use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; -use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::normalize::NzEnv; -use crate::semantics::phase::Normalized; -use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; +use crate::semantics::{Value, ValueKind}; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, - UnspannedExpr, + Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr, }; -fn tck_pi_type( - binder: Binder, - tx: Value, - te: Value, -) -> Result { - use TypeMessage::*; - - let ka = match tx.get_type()?.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(InvalidInputType(tx))), - }; - - let kb = match te.get_type()?.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))), - }; - - let k = function_check(ka, kb); - - Ok(Value::from_kind_and_type( - ValueKind::Pi(binder, tx, te), - Value::from_const(k), - )) -} - -fn tck_record_type( - kts: impl IntoIterator>, -) -> Result { - use std::collections::hash_map::Entry; - use TypeMessage::*; - let mut new_kts = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; - for e in kts { - let (x, t) = e?; - // Construct the union of the contained `Const`s - match t.get_type()?.as_const() { - Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(InvalidFieldType(x, t))), - } - // Check for duplicated entries - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(RecordTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - Ok(Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - Value::from_const(k), - )) -} - -fn tck_union_type(kts: Iter) -> Result -where - Iter: IntoIterator), TypeError>>, -{ - use std::collections::hash_map::Entry; - use TypeMessage::*; - let mut new_kts = HashMap::new(); - // Check that all types are the same const - let mut k = None; - for e in kts { - let (x, t) = e?; - if let Some(t) = &t { - match (k, t.get_type()?.as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new(InvalidFieldType(x, t.clone()))) - } - } - } - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(UnionTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - // An empty union type has type Type; - // an union type with only unary variants also has type Type - let k = k.unwrap_or(Const::Type); - - Ok(Value::from_kind_and_type( - ValueKind::UnionType(new_kts), - Value::from_const(k), - )) -} - -fn function_check(a: Const, b: Const) -> Const { - if b == Const::Type { - Const::Type - } else { - max(a, b) - } -} - pub(crate) fn const_to_value(c: Const) -> Value { let v = ValueKind::Const(c); match c { @@ -289,511 +177,3 @@ pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { .normalize_whnf_noenv(), ) } - -/// Type-check an expression and return the expression alongside its type if type-checking -/// succeeded, or an error if type-checking failed. -/// Some normalization is done while typechecking, so the returned expression might be partially -/// normalized as well. -fn type_with(ctx: &TyCtx, e: Expr) -> Result { - use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; - let span = e.span(); - - match e.as_ref() { - Lam(var, annot, body) => { - let binder = ctx.new_binder(var); - let annot = type_with(ctx, annot.clone())?; - annot.normalize_nf(); - let ctx2 = ctx.insert_type(&binder, annot.clone()); - let body = type_with(&ctx2, body.clone())?; - let body_type = body.get_type()?; - Ok(Value::from_kind_and_type( - ValueKind::Lam(binder.clone(), annot.clone(), body), - tck_pi_type(binder, annot, body_type)?, - )) - } - Pi(x, ta, tb) => { - let binder = ctx.new_binder(x); - let ta = type_with(ctx, ta.clone())?; - let ctx2 = ctx.insert_type(&binder, ta.clone()); - let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(binder, ta, tb) - } - Let(x, t, v, e) => { - let v = if let Some(t) = t { - t.rewrap(Annot(v.clone(), t.clone())) - } else { - v.clone() - }; - - let v = type_with(ctx, v)?; - let binder = ctx.new_binder(x); - let e = - type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?; - // let e_ty = e.get_type()?; - // Ok(Value::from_kind_and_type( - // ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)), - // e_ty, - // )) - Ok(e) - } - Embed(p) => Ok(p.clone().into_value()), - Var(var) => match ctx.lookup(&var) { - Some(typed) => Ok(typed.clone()), - None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), - }, - e => { - // Typecheck recursively all subexpressions - let expr = e.traverse_ref_with_special_handling_of_binders( - |e| type_with(ctx, e.clone()), - |_, _| unreachable!(), - )?; - type_last_layer(ctx, expr, span) - } - } -} - -/// When all sub-expressions have been typed, check the remaining toplevel -/// layer. -fn type_last_layer( - ctx: &TyCtx, - e: ExprKind, - span: Span, -) -> Result { - use syntax::BinOp::*; - use syntax::Builtin::*; - use syntax::Const::Type; - let mkerr = - |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string()))); - - /// Intermediary return type - enum Ret { - /// Returns the contained value as is - RetWhole(Value), - /// Returns the input expression `e` with the contained value as its type - RetTypeOnly(Value), - } - use Ret::*; - - let ret = match &e { - ExprKind::Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - ExprKind::Lam(_, _, _) - | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) - | ExprKind::Embed(_) - | ExprKind::Var(_) => unreachable!(), - ExprKind::App(f, a) => { - let tf = f.get_type()?; - let tf_borrow = tf.as_whnf(); - match &*tf_borrow { - ValueKind::Pi(_, tx, tb) => { - if &a.get_type()? != tx { - return mkerr("TypeMismatch"); - } - - let ret = tb.subst_shift(&AlphaVar::default(), a); - ret.normalize_nf(); - RetTypeOnly(ret) - } - ValueKind::PiClosure { closure, .. } => { - RetTypeOnly(closure.apply(a.clone())) - } - _ => return mkerr("NotAFunction"), - } - } - ExprKind::Annot(x, t) => { - if &x.get_type()? != t { - return mkerr("AnnotMismatch"); - } - RetWhole(x.clone()) - } - ExprKind::Assert(t) => { - match &*t.as_whnf() { - ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), - _ => return mkerr("AssertMustTakeEquivalence"), - } - RetTypeOnly(t.clone()) - } - ExprKind::BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { - return mkerr("InvalidPredicate"); - } - - if y.get_type()?.get_type()?.as_const() != Some(Const::Type) { - return mkerr("IfBranchMustBeTerm"); - } - - if z.get_type()?.get_type()?.as_const() != Some(Const::Type) { - return mkerr("IfBranchMustBeTerm"); - } - - if y.get_type()? != z.get_type()? { - return mkerr("IfBranchMismatch"); - } - - RetTypeOnly(y.get_type()?) - } - ExprKind::EmptyListLit(t) => { - let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin( - syntax::Builtin::List, - args, - _, - _, - ) if args.len() == 1 => args[0].clone(), - _ => return mkerr("InvalidListType"), - }; - RetWhole(Value::from_kind_and_type( - ValueKind::EmptyListLit(arg), - t.clone(), - )) - } - ExprKind::NEListLit(xs) => { - let mut iter = xs.iter().enumerate(); - let (_, x) = iter.next().unwrap(); - for (_, y) in iter { - if x.get_type()? != y.get_type()? { - return mkerr("InvalidListElement"); - } - } - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Const::Type) { - return mkerr("InvalidListType"); - } - - RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) - } - ExprKind::SomeLit(x) => { - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Const::Type) { - return mkerr("InvalidOptionalType"); - } - - RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) - } - ExprKind::RecordType(kts) => RetWhole(tck_record_type( - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - ExprKind::UnionType(kts) => RetWhole(tck_union_type( - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type( - kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), - )?), - ExprKind::Field(r, x) => { - match &*r.get_type()?.as_whnf() { - ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => RetTypeOnly(tth.clone()), - None => return mkerr("MissingRecordField"), - }, - // TODO: branch here only when r.get_type() is a Const - _ => { - match &*r.as_whnf() { - ValueKind::UnionType(kts) => match kts.get(&x) { - // Constructor has type T -> < x: T, ... > - Some(Some(t)) => RetTypeOnly(tck_pi_type( - ctx.new_binder(x), - t.clone(), - r.under_binder(), - )?), - Some(None) => RetTypeOnly(r.clone()), - None => return mkerr("MissingUnionField"), - }, - _ => return mkerr("NotARecord"), - } - } // _ => mkerr("NotARecord"), - } - } - ExprKind::Const(c) => RetWhole(const_to_value(*c)), - ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)), - ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), - ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), - ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), - ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), - ExprKind::TextLit(interpolated) => { - let text_type = builtin_to_value(Text); - for contents in interpolated.iter() { - use InterpolatedTextContents::Expr; - if let Expr(x) = contents { - if x.get_type()? != text_type { - return mkerr("InvalidTextInterpolation"); - } - } - } - RetTypeOnly(text_type) - } - ExprKind::BinOp(RightBiasedRecordMerge, l, r) => { - let l_type = l.get_type()?; - let r_type = r.get_type()?; - - // Extract the LHS record type - let l_type_borrow = l_type.as_whnf(); - let kts_x = match &*l_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("MustCombineRecord"), - }; - - // Extract the RHS record type - let r_type_borrow = r_type.as_whnf(); - let kts_y = match &*r_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("MustCombineRecord"), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { - Ok(r_t.clone()) - })?; - - // Construct the final record type from the union - RetTypeOnly(tck_record_type( - kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), - )?) - } - ExprKind::BinOp(RecursiveRecordMerge, l, r) => { - RetTypeOnly(type_last_layer( - ctx, - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.get_type()?, - r.get_type()?, - ), - Span::Artificial, - )?) - } - ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { - // Extract the LHS record type - let borrow_l = l.as_whnf(); - let kts_x = match &*borrow_l { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("RecordTypeMergeRequiresRecordType"), - }; - - // Extract the RHS record type - let borrow_r = r.as_whnf(); - let kts_y = match &*borrow_r { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("RecordTypeMergeRequiresRecordType"), - }; - - // Ensure that the records combine without a type error - 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| { - type_last_layer( - ctx, - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - Span::Artificial, - ) - }, - )?; - - RetWhole(tck_record_type(kts.into_iter().map(Ok))?) - } - ExprKind::BinOp(ListAppend, l, r) => { - match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _, _, _) => {} - _ => return mkerr("BinOpTypeMismatch"), - } - - if l.get_type()? != r.get_type()? { - return mkerr("BinOpTypeMismatch"); - } - - RetTypeOnly(l.get_type()?) - } - ExprKind::BinOp(Equivalence, l, r) => { - if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { - return mkerr("EquivalenceArgumentMustBeTerm"); - } - if r.get_type()?.get_type()?.as_const() != Some(Const::Type) { - return mkerr("EquivalenceArgumentMustBeTerm"); - } - - if l.get_type()? != r.get_type()? { - return mkerr("EquivalenceTypeMismatch"); - } - - RetWhole(Value::from_kind_and_type( - ValueKind::Equivalence(l.clone(), r.clone()), - Value::from_const(Type), - )) - } - ExprKind::BinOp(o, l, r) => { - let t = builtin_to_value(match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, - ListAppend => unreachable!(), - RightBiasedRecordMerge => unreachable!(), - RecursiveRecordMerge => unreachable!(), - RecursiveRecordTypeMerge => unreachable!(), - ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"), - Equivalence => unreachable!(), - }); - - if l.get_type()? != t { - return mkerr("BinOpTypeMismatch"); - } - - if r.get_type()? != t { - return mkerr("BinOpTypeMismatch"); - } - - RetTypeOnly(t) - } - ExprKind::Merge(record, union, type_annot) => { - let record_type = record.get_type()?; - let record_borrow = record_type.as_whnf(); - let handlers = match &*record_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("Merge1ArgMustBeRecord"), - }; - - let union_type = union.get_type()?; - let union_borrow = union_type.as_whnf(); - let variants = match &*union_borrow { - ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin( - syntax::Builtin::Optional, - args, - _, - _, - ) if args.len() == 1 => { - let ty = &args[0]; - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type = - match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let handler_type_borrow = handler_type.as_whnf(); - let (tx, tb) = match &*handler_type_borrow { - ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => return mkerr("NotAFunction"), - }; - - if variant_type != tx { - return mkerr("TypeMismatch"); - } - - // Extract `tb` from under the binder. Fails if the variable was used - // in `tb`. - match tb.over_binder() { - Some(x) => x, - None => return mkerr( - "MergeHandlerReturnTypeMustNotBeDependent", - ), - } - } - // Union alternative without type - Some(None) => handler_type.clone(), - None => return mkerr("MergeHandlerMissingVariant"), - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return mkerr("MergeHandlerTypeMismatch"); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return mkerr("MergeVariantMissingHandler"); - } - } - - match (inferred_type, type_annot.as_ref()) { - (Some(t1), Some(t2)) => { - if &t1 != t2 { - return mkerr("MergeAnnotMismatch"); - } - RetTypeOnly(t1) - } - (Some(t), None) => RetTypeOnly(t), - (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), - } - } - ExprKind::ToMap(_, _) => unimplemented!("toMap"), - ExprKind::Projection(record, labels) => { - let record_type = record.get_type()?; - let record_type_borrow = record_type.as_whnf(); - let kts = match &*record_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr("ProjectionMustBeRecord"), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return mkerr("ProjectionMissingEntry"), - Some(t) => { - use std::collections::hash_map::Entry; - match new_kts.entry(l.clone()) { - Entry::Occupied(_) => { - return mkerr("ProjectionDuplicateField") - } - Entry::Vacant(e) => e.insert(t.clone()), - } - } - }; - } - - RetTypeOnly(Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - record_type.get_type()?, - )) - } - ExprKind::ProjectionByExpr(_, _) => { - unimplemented!("selection by expression") - } - ExprKind::Completion(_, _) => unimplemented!("record completion"), - }; - - Ok(match ret { - RetTypeOnly(typ) => Value::from_kind_and_type_and_span( - ValueKind::PartialExpr(e), - typ, - span, - ), - RetWhole(v) => v.with_span(span), - }) -} - -/// `type_of` is the same as `type_with` with an empty context, meaning that the -/// expression must be closed (i.e. no free variables), otherwise type-checking -/// will fail. -pub(crate) fn typecheck(e: Expr) -> Result { - type_with(&TyCtx::new(), e) -} - -pub(crate) fn typecheck_with( - expr: Expr, - ty: Expr, -) -> Result { - typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty))) -} -- 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/phase/normalize.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d40456b..fa80b6e 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -638,15 +638,13 @@ pub(crate) fn normalize_one_layer( ), // Those cases have already been completely handled in the typechecking phase (using // `RetWhole`), so they won't appear here. - ExprKind::Lam(_, _, _) - | ExprKind::Pi(_, _, _) + ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } - ExprKind::Let(_, _, val, body) => { - Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) - } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), -- 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/phase/normalize.rs | 62 ++-------------------------------- dhall/src/semantics/phase/typecheck.rs | 3 +- 2 files changed, 3 insertions(+), 62 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index fa80b6e..ce37993 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,16 +1,13 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; use crate::semantics::tck::typecheck::type_with; -use crate::semantics::tck::typecheck::TyEnv; -use crate::semantics::{ - AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, -}; +use crate::semantics::NzEnv; +use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -838,53 +835,6 @@ pub(crate) fn normalize_whnf( } } -#[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 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() - } -} - /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let ty = match tye.get_type() { @@ -924,11 +874,3 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } - -/// Ignore NzEnv when comparing -impl std::cmp::PartialEq for NzEnv { - fn eq(&self, _other: &Self) -> bool { - true - } -} -impl std::cmp::Eq for NzEnv {} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 4392365..2e22ad2 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,5 +1,4 @@ -use crate::semantics::phase::normalize::NzEnv; -use crate::semantics::{Value, ValueKind}; +use crate::semantics::{NzEnv, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr, -- 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/phase/normalize.rs | 373 +-------------------------------- dhall/src/semantics/phase/typecheck.rs | 177 ---------------- 2 files changed, 6 insertions(+), 544 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ce37993..2d4b4b3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,373 +1,12 @@ use std::collections::HashMap; -use std::convert::TryInto; -use crate::semantics::phase::typecheck::{ - builtin_to_value_env, const_to_value, rc, -}; use crate::semantics::phase::Normalized; -use crate::semantics::tck::typecheck::type_with; use crate::semantics::NzEnv; -use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; -use crate::syntax; -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, +use crate::semantics::{ + apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (var($var:ident)) => {{ - rc(ExprKind::Var(syntax::V( - Label::from(stringify!($var)).into(), - 0 - ))) - }}; - (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var = Label::from(stringify!($var)); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - rc(ExprKind::Lam(var, ty, body)) - }}; - (Type) => { - rc(ExprKind::Const(Type)) - }; - (Natural) => { - rc(ExprKind::Builtin(Builtin::Natural)) - }; - (List $($ty:tt)*) => {{ - let ty = make_closure!($($ty)*); - rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - ty - )) - }}; - (Some($($v:tt)*)) => { - rc(ExprKind::SomeLit( - make_closure!($($v)*) - )) - }; - (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( - syntax::BinOp::NaturalPlus, - make_closure!($($v)*), - rc(ExprKind::NaturalLit(1)) - )) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( - syntax::BinOp::ListAppend, - rc(ExprKind::NEListLit(vec![head])), - tail, - )) - }}; -} - -#[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec, - ty: &Value, - types: Vec, - env: NzEnv, -) -> ValueKind { - use syntax::Builtin::*; - use ValueKind::*; - - // Small helper enum - enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - // For applications that can return a function, it's important to keep the remaining - // arguments to apply them to the resulting function. - ValueWithRemainingArgs(&'a [Value], Value), - DoneAsIs, - } - let make_closure = |e| { - type_with(&env.to_alpha_tyenv(), &e) - .unwrap() - .normalize_whnf(&env) - }; - - let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), - _ => Ret::DoneAsIs, - }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), - _ => Ret::DoneAsIs, - }, - (NaturalShow, [n]) => { - match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) - } - (NaturalLit(0), _) => Ret::Value(b.clone()), - (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), - _ if a == b => Ret::ValueKind(NaturalLit(0)), - _ => Ret::DoneAsIs, - }, - (IntegerShow, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) - } - _ => Ret::DoneAsIs, - }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) - } - _ => Ret::DoneAsIs, - }, - (IntegerNegate, [n]) => match &*n.as_whnf() { - IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), - _ => Ret::DoneAsIs, - }, - (IntegerClamp, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) - } - _ => Ret::DoneAsIs, - }, - (DoubleShow, [n]) => { - match &*n.as_whnf() { - DoubleLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (TextShow, [v]) => match &*v.as_whnf() { - TextLit(elts) => { - match elts.as_slice() { - // Empty string literal. - [] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = - std::iter::empty().collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - // If there are no interpolations (invariants ensure that when there are no - // interpolations, there is a single Text item) in the literal. - [InterpolatedTextContents::Text(s)] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = - std::iter::once(InterpolatedTextContents::Text( - s.clone(), - )) - .collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, - } - } - _ => Ret::DoneAsIs, - }, - (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), - NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), - _ => Ret::DoneAsIs, - }, - (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) - } - _ => Ret::DoneAsIs, - }, - (ListIndexed, [_, l]) => { - let l_whnf = l.as_whnf(); - match &*l_whnf { - EmptyListLit(_) | NEListLit(_) => { - // Extract the type of the list elements - let t = match &*l_whnf { - EmptyListLit(t) => t.clone(), - NEListLit(xs) => xs[0].get_type_not_sort(), - _ => unreachable!(), - }; - - // Construct the returned record type: { index: Natural, value: t } - let mut kts = HashMap::new(); - kts.insert("index".into(), Value::from_builtin(Natural)); - kts.insert("value".into(), t.clone()); - let t = Value::from_kind_and_type( - RecordType(kts), - Value::from_const(Type), - ); - - // Construct the new list, with added indices - let list = match &*l_whnf { - EmptyListLit(_) => EmptyListLit(t), - NEListLit(xs) => NEListLit( - xs.iter() - .enumerate() - .map(|(i, e)| { - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Value::from_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), - ); - kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::ValueKind(list) - } - _ => Ret::DoneAsIs, - } - } - (ListBuild, [t, f]) => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - λ(as : List var(T)) -> - [ var(a) ] # var(as) - )) - .app(t.clone()), - ) - .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), - ) - } - (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), - NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v); - } - Ret::ValueWithRemainingArgs(r, v) - } - _ => Ret::DoneAsIs, - }, - (OptionalBuild, [t, f]) => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - Some(var(a)) - )) - .app(t.clone()), - ) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ) - } - (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf() - { - EmptyOptionalLit(_) => { - Ret::ValueWithRemainingArgs(r, nothing.clone()) - } - NEOptionalLit(x) => { - Ret::ValueWithRemainingArgs(r, just.app(x.clone())) - } - _ => Ret::DoneAsIs, - }, - (NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure(make_closure!( - λ(x : Natural) -> - 1 + var(x) - ))) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), - ), - - (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() { - NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), - NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) - .app(t.clone()) - .app(succ.clone()) - .app(zero.clone()); - Ret::ValueWithRemainingArgs(r, succ.app(fold)) - } - _ => Ret::DoneAsIs, - }, - _ => Ret::DoneAsIs, - }; - match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => { - let n_consumed_args = args.len() - unconsumed_args.len(); - for x in args.into_iter().skip(n_consumed_args) { - v = v.app(x); - } - v.to_whnf_check_type(ty) - } - Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), - } -} +use crate::syntax; +use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents}; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); @@ -643,8 +282,8 @@ pub(crate) fn normalize_one_layer( unreachable!("This case should have been handled in typecheck") } ExprKind::Annot(x, _) => Ret::Value(x), - ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), + 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)), diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 2e22ad2..8b13789 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,178 +1 @@ -use crate::semantics::{NzEnv, Value, ValueKind}; -use crate::syntax; -use crate::syntax::{ - Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr, -}; -pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueKind::Const(c); - match c { - Const::Type => { - Value::from_kind_and_type(v, const_to_value(Const::Kind)) - } - Const::Kind => { - Value::from_kind_and_type(v, const_to_value(Const::Sort)) - } - Const::Sort => Value::const_sort(), - } -} - -pub fn rc(x: UnspannedExpr) -> Expr { - Expr::new(x, Span::Artificial) -} - -// Ad-hoc macro to help construct the types of builtins -macro_rules! make_type { - (Type) => { ExprKind::Const(Const::Type) }; - (Bool) => { ExprKind::Builtin(Builtin::Bool) }; - (Natural) => { ExprKind::Builtin(Builtin::Natural) }; - (Integer) => { ExprKind::Builtin(Builtin::Integer) }; - (Double) => { ExprKind::Builtin(Builtin::Double) }; - (Text) => { ExprKind::Builtin(Builtin::Text) }; - ($var:ident) => { - ExprKind::Var(syntax::V(stringify!($var).into(), 0)) - }; - (Optional $ty:ident) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::Optional)), - rc(make_type!($ty)) - ) - }; - (List $($rest:tt)*) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - rc(make_type!($($rest)*)) - ) - }; - ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = syntax::map::DupTreeMap::new(); - $( - kts.insert( - Label::from(stringify!($label)), - rc(make_type!($ty)), - ); - )* - ExprKind::RecordType(kts) - }}; - ($ty:ident -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($ty)), - rc(make_type!($($rest)*)) - ) - }; - (($($arg:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($($arg)*)), - rc(make_type!($($rest)*)) - ) - }; - (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - stringify!($var).into(), - rc(make_type!($($ty)*)), - rc(make_type!($($rest)*)) - ) - }; -} - -pub(crate) fn type_of_builtin(b: Builtin) -> Expr { - use syntax::Builtin::*; - rc(match b { - Bool | Natural | Integer | Double | Text => make_type!(Type), - List | Optional => make_type!( - Type -> Type - ), - - NaturalFold => make_type!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => make_type!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => make_type!( - Natural -> Bool - ), - NaturalToInteger => make_type!(Natural -> Integer), - NaturalShow => make_type!(Natural -> Text), - NaturalSubtract => make_type!(Natural -> Natural -> Natural), - - IntegerToDouble => make_type!(Integer -> Double), - IntegerShow => make_type!(Integer -> Text), - IntegerNegate => make_type!(Integer -> Integer), - IntegerClamp => make_type!(Integer -> Natural), - - DoubleShow => make_type!(Double -> Text), - TextShow => make_type!(Text -> Text), - - ListBuild => make_type!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => make_type!( - forall (a: Type) -> - (List a) -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), - ListHead | ListLast => { - make_type!(forall (a: Type) -> (List a) -> Optional a) - } - ListIndexed => make_type!( - forall (a: Type) -> - (List a) -> - List { index: Natural, value: a } - ), - ListReverse => make_type!( - forall (a: Type) -> (List a) -> List a - ), - - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => make_type!( - forall (A: Type) -> Optional A - ), - }) -} - -pub(crate) fn builtin_to_value(b: Builtin) -> Value { - builtin_to_value_env(b, &NzEnv::new()) -} -pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { - Value::from_kind_and_type( - ValueKind::from_builtin_env(b, env.clone()), - crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) - .unwrap() - .normalize_whnf_noenv(), - ) -} -- cgit v1.2.3 From 7743647137d1914c280e03d6aaee81e507cff97d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:17:49 +0000 Subject: Remove old typecheck module --- dhall/src/semantics/phase/mod.rs | 17 +++-------------- dhall/src/semantics/phase/resolve.rs | 8 ++------ dhall/src/semantics/phase/typecheck.rs | 1 - 3 files changed, 5 insertions(+), 21 deletions(-) delete mode 100644 dhall/src/semantics/phase/typecheck.rs (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 2727a61..f24a668 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -2,9 +2,7 @@ use std::fmt::Display; use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::tck::tyexpr::TyExpr; +use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -12,7 +10,6 @@ use resolve::ImportRoot; pub(crate) mod normalize; pub(crate) mod parse; pub(crate) mod resolve; -pub(crate) mod typecheck; pub type ParsedExpr = Expr; pub type DecodedExpr = Expr; @@ -80,23 +77,15 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) + Ok(Typed(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( - &self.0, - ty.to_expr(), - )?)) + Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { self.0.clone() } - pub fn tck_and_normalize_new_flow(&self) -> Result { - let val = crate::semantics::tck::typecheck::typecheck(&self.0)? - .normalize_whnf_noenv(); - Ok(Normalized(val)) - } } impl Typed { diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index 64106aa..cc4a024 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -52,14 +52,10 @@ fn load_import( import_cache: &mut ImportCache, import_stack: &ImportStack, ) -> Result { - // Ok( - // do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - // .typecheck()? - // .normalize(), - // ) Ok( do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - .tck_and_normalize_new_flow()?, + .typecheck()? + .normalize(), ) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs deleted file mode 100644 index 8b13789..0000000 --- a/dhall/src/semantics/phase/typecheck.rs +++ /dev/null @@ -1 +0,0 @@ - -- 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/phase/normalize.rs | 31 +++++++++++-------------------- 1 file changed, 11 insertions(+), 20 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 2d4b4b3..d7720c7 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,10 +3,11 @@ use std::collections::HashMap; use crate::semantics::phase::Normalized; use crate::semantics::NzEnv; use crate::semantics::{ - apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, + Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; +use crate::syntax::{ + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, }; -use crate::syntax; -use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents}; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); @@ -14,15 +15,8 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args, types, env) => { - use std::iter::once; - let args = args.iter().cloned().chain(once(a.clone())).collect(); - let types = types - .iter() - .cloned() - .chain(once(f.get_type().unwrap())) - .collect(); - apply_builtin(*b, args, ty, types, env.clone()) + ValueKind::AppliedBuiltin(closure) => { + closure.apply(a, f.get_type().unwrap(), ty) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -293,12 +287,11 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin( - syntax::Builtin::List, + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, args, - _, - _, - ) if args.len() == 1 => args[0].clone(), + .. + }) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -462,9 +455,7 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types, env) => { - apply_builtin(b, args, ty, types, env) - } + ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) -- cgit v1.2.3 From cb86493012b268ec32ad85a42b54fb1a2adab7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 14:20:01 +0000 Subject: s/as_whnf/kind/ --- dhall/src/semantics/phase/normalize.rs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d7720c7..f36ec4a 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -10,7 +10,7 @@ use crate::syntax::{ }; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.as_whnf(); + let f_borrow = f.kind(); match &*f_borrow { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) @@ -47,7 +47,7 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_whnf(); + let e_borrow = e.kind(); match &*e_borrow { ValueKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) @@ -123,8 +123,8 @@ fn apply_binop<'a>( BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_whnf(); - let y_borrow = y.as_whnf(); + 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), @@ -206,7 +206,7 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.as_whnf(); + let ty_borrow = ty.kind(); let kts = match &*ty_borrow { RecordType(kts) => kts, _ => unreachable!("Internal type error"), @@ -286,7 +286,7 @@ pub(crate) fn normalize_one_layer( ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { - let arg = match &*t.as_whnf() { + let arg = match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -319,13 +319,13 @@ pub(crate) fn normalize_one_layer( } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_whnf(); + let b_borrow = b.kind(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_whnf(); - let e2_borrow = e2.as_whnf(); + 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), @@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer( Ret::ValueKind(RecordLit(HashMap::new())) } ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => Ret::ValueKind(RecordLit( ls.iter() @@ -365,7 +365,7 @@ pub(crate) fn normalize_one_layer( } } ExprKind::Field(ref v, ref l) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Value(r.clone()), @@ -391,8 +391,8 @@ pub(crate) fn normalize_one_layer( ExprKind::Completion(_, _) => unimplemented!("record completion"), ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_whnf(); - let variant_borrow = variant.as_whnf(); + let handlers_borrow = handlers.kind(); + let variant_borrow = variant.kind(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) { -- 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/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index f24a668..a25f096 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -91,7 +91,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - Normalized(self.0.normalize_nf_noenv()) + Normalized(self.0.rec_eval_closed_expr()) } /// Converts a value back to the corresponding AST expression. diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f36ec4a..ea1a25b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -457,6 +457,7 @@ pub(crate) fn normalize_whnf( 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())) } @@ -475,7 +476,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), annot: annot.clone(), @@ -483,7 +484,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), @@ -492,11 +493,11 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { - let val = val.normalize_whnf(env); - return body.normalize_whnf(&env.insert_value(val)); + let val = val.eval(env); + return body.eval(&env.insert_value(val)); } TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.normalize_whnf(env)); + let e = e.map_ref(|tye| tye.eval(env)); normalize_one_layer(e, &ty, env) } }; -- 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/phase/mod.rs | 1 - dhall/src/semantics/phase/normalize.rs | 507 --------------------------------- 2 files changed, 508 deletions(-) delete mode 100644 dhall/src/semantics/phase/normalize.rs (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index a25f096..ff4b859 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -7,7 +7,6 @@ use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; -pub(crate) mod normalize; pub(crate) mod parse; pub(crate) mod resolve; diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs deleted file mode 100644 index ea1a25b..0000000 --- a/dhall/src/semantics/phase/normalize.rs +++ /dev/null @@ -1,507 +0,0 @@ -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) -} -- 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/phase/mod.rs | 242 ----------------------------------- dhall/src/semantics/phase/parse.rs | 2 +- dhall/src/semantics/phase/resolve.rs | 2 +- 3 files changed, 2 insertions(+), 244 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index ff4b859..02e2b18 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,244 +1,2 @@ -use std::fmt::Display; -use std::path::Path; - -use crate::error::{EncodeError, Error, ImportError, TypeError}; -use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; -use crate::syntax::binary; -use crate::syntax::{Builtin, Const, Expr}; -use resolve::ImportRoot; - pub(crate) mod parse; pub(crate) mod resolve; - -pub type ParsedExpr = Expr; -pub type DecodedExpr = Expr; -pub type ResolvedExpr = Expr; -pub type NormalizedExpr = Expr; - -#[derive(Debug, Clone)] -pub struct Parsed(ParsedExpr, ImportRoot); - -/// An expression where all imports have been resolved -/// -/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. -#[derive(Debug, Clone)] -pub struct Resolved(ResolvedExpr); - -/// A typed expression -#[derive(Debug, Clone)] -pub struct Typed(TyExpr); - -/// A normalized expression. -/// -/// Invariant: the contained Typed expression must be in normal form, -#[derive(Debug, Clone)] -pub struct Normalized(Value); - -/// Controls conversion from `Value` to `Expr` -#[derive(Copy, Clone)] -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - -impl Parsed { - pub fn parse_file(f: &Path) -> Result { - parse::parse_file(f) - } - pub fn parse_str(s: &str) -> Result { - parse::parse_str(s) - } - pub fn parse_binary_file(f: &Path) -> Result { - parse::parse_binary_file(f) - } - pub fn parse_binary(data: &[u8]) -> Result { - parse::parse_binary(data) - } - - pub fn resolve(self) -> Result { - resolve::resolve(self) - } - pub fn skip_resolve(self) -> Result { - resolve::skip_resolve_expr(self) - } - - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.0) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ParsedExpr { - self.0.clone() - } -} - -impl Resolved { - pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.0)?)) - } - pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) - } - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { - self.0.clone() - } -} - -impl Typed { - /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(&self) -> Normalized { - Normalized(self.0.rec_eval_closed_expr()) - } - - /// Converts a value back to the corresponding AST expression. - fn to_expr(&self) -> ResolvedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - - pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.get_type()?)) - } -} - -impl Normalized { - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.to_expr()) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: false, - }) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - - pub(crate) fn from_const(c: Const) -> Self { - Normalized(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type( - v: ValueKind, - t: Normalized, - ) -> Self { - Normalized(Value::from_kind_and_type(v, t.into_value())) - } - pub(crate) fn from_value(th: Value) -> Self { - Normalized(th) - } - pub(crate) fn const_type() -> Self { - Normalized::from_const(Const::Type) - } - - pub fn make_builtin_type(b: Builtin) -> Self { - Normalized::from_value(Value::from_builtin(b)) - } - pub fn make_optional_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::Optional).app(t.to_value()), - ) - } - pub fn make_list_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::List).app(t.to_value()), - ) - } - pub fn make_record_type( - kts: impl Iterator, - ) -> Self { - Normalized::from_kind_and_type( - ValueKind::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), - ), - Normalized::const_type(), - ) - } - pub fn make_union_type( - kts: impl Iterator)>, - ) -> Self { - Normalized::from_kind_and_type( - ValueKind::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) - .collect(), - ), - Normalized::const_type(), - ) - } -} - -macro_rules! derive_traits_for_wrapper_struct { - ($ty:ident) => { - impl std::cmp::PartialEq for $ty { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } - } - - impl std::cmp::Eq for $ty {} - - impl std::fmt::Display for $ty { - fn fmt( - &self, - f: &mut std::fmt::Formatter, - ) -> Result<(), std::fmt::Error> { - self.0.fmt(f) - } - } - }; -} - -derive_traits_for_wrapper_struct!(Parsed); -derive_traits_for_wrapper_struct!(Resolved); - -impl std::hash::Hash for Normalized { - fn hash(&self, state: &mut H) - where - H: std::hash::Hasher, - { - if let Ok(vec) = self.encode() { - vec.hash(state) - } - } -} - -impl Eq for Typed {} -impl PartialEq for Typed { - fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() - } -} -impl Display for Typed { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} - -impl Eq for Normalized {} -impl PartialEq for Normalized { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } -} -impl Display for Normalized { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs index 00db422..b72fe7f 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -4,9 +4,9 @@ use std::path::Path; use crate::error::Error; use crate::semantics::phase::resolve::ImportRoot; -use crate::semantics::phase::Parsed; use crate::syntax::binary; use crate::syntax::parse_expr; +use crate::Parsed; pub(crate) fn parse_file(f: &Path) -> Result { let mut buffer = String::new(); diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index cc4a024..3acf114 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -2,9 +2,9 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; use crate::error::{Error, ImportError}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; +use crate::{Normalized, NormalizedExpr, Parsed, Resolved}; type Import = syntax::Import; -- cgit v1.2.3 From 8ff022fa2cec34bc1d46ac3655d0c3d228ef893c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:16:25 +0000 Subject: Move parse and resolve up a level --- dhall/src/semantics/phase/mod.rs | 2 - dhall/src/semantics/phase/parse.rs | 37 ------- dhall/src/semantics/phase/resolve.rs | 181 ----------------------------------- 3 files changed, 220 deletions(-) delete mode 100644 dhall/src/semantics/phase/mod.rs delete mode 100644 dhall/src/semantics/phase/parse.rs delete mode 100644 dhall/src/semantics/phase/resolve.rs (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs deleted file mode 100644 index 02e2b18..0000000 --- a/dhall/src/semantics/phase/mod.rs +++ /dev/null @@ -1,2 +0,0 @@ -pub(crate) mod parse; -pub(crate) mod resolve; diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs deleted file mode 100644 index b72fe7f..0000000 --- a/dhall/src/semantics/phase/parse.rs +++ /dev/null @@ -1,37 +0,0 @@ -use std::fs::File; -use std::io::Read; -use std::path::Path; - -use crate::error::Error; -use crate::semantics::phase::resolve::ImportRoot; -use crate::syntax::binary; -use crate::syntax::parse_expr; -use crate::Parsed; - -pub(crate) fn parse_file(f: &Path) -> Result { - let mut buffer = String::new(); - File::open(f)?.read_to_string(&mut buffer)?; - let expr = parse_expr(&*buffer)?; - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_str(s: &str) -> Result { - let expr = parse_expr(s)?; - let root = ImportRoot::LocalDir(std::env::current_dir()?); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_binary(data: &[u8]) -> Result { - let expr = binary::decode(data)?; - let root = ImportRoot::LocalDir(std::env::current_dir()?); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_binary_file(f: &Path) -> Result { - let mut buffer = Vec::new(); - File::open(f)?.read_to_end(&mut buffer)?; - let expr = binary::decode(&buffer)?; - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - Ok(Parsed(expr, root)) -} diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs deleted file mode 100644 index 3acf114..0000000 --- a/dhall/src/semantics/phase/resolve.rs +++ /dev/null @@ -1,181 +0,0 @@ -use std::collections::HashMap; -use std::path::{Path, PathBuf}; - -use crate::error::{Error, ImportError}; -use crate::syntax; -use crate::syntax::{FilePath, ImportLocation, URL}; -use crate::{Normalized, NormalizedExpr, Parsed, Resolved}; - -type Import = syntax::Import; - -/// A root from which to resolve relative imports. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ImportRoot { - LocalDir(PathBuf), -} - -type ImportCache = HashMap; - -pub(crate) type ImportStack = Vec; - -fn resolve_import( - import: &Import, - root: &ImportRoot, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result { - use self::ImportRoot::*; - use syntax::FilePrefix::*; - use syntax::ImportLocation::*; - let cwd = match root { - LocalDir(cwd) => cwd, - }; - match &import.location { - Local(prefix, path) => { - let path_buf: PathBuf = path.file_path.iter().collect(); - let path_buf = match prefix { - // TODO: fail gracefully - Parent => cwd.parent().unwrap().join(path_buf), - Here => cwd.join(path_buf), - _ => unimplemented!("{:?}", import), - }; - Ok(load_import(&path_buf, import_cache, import_stack).map_err( - |e| ImportError::Recursive(import.clone(), Box::new(e)), - )?) - } - _ => unimplemented!("{:?}", import), - } -} - -fn load_import( - f: &Path, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result { - Ok( - do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - .typecheck()? - .normalize(), - ) -} - -fn do_resolve_expr( - parsed: Parsed, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result { - let Parsed(mut expr, root) = parsed; - let mut resolve = |import: Import| -> Result { - if import_stack.contains(&import) { - return Err(ImportError::ImportCycle(import_stack.clone(), import)); - } - match import_cache.get(&import) { - Some(expr) => Ok(expr.clone()), - None => { - // Copy the import stack and push the current import - let mut import_stack = import_stack.clone(); - import_stack.push(import.clone()); - - // Resolve the import recursively - let expr = resolve_import( - &import, - &root, - import_cache, - &import_stack, - )?; - - // Add the import to the cache - import_cache.insert(import, expr.clone()); - Ok(expr) - } - } - }; - expr.traverse_resolve_mut(&mut resolve)?; - Ok(Resolved(expr)) -} - -pub(crate) fn resolve(e: Parsed) -> Result { - do_resolve_expr(e, &mut HashMap::new(), &Vec::new()) -} - -pub(crate) fn skip_resolve_expr( - parsed: Parsed, -) -> Result { - let mut expr = parsed.0; - let mut resolve = |import: Import| -> Result { - Err(ImportError::UnexpectedImport(import)) - }; - expr.traverse_resolve_mut(&mut resolve)?; - Ok(Resolved(expr)) -} - -pub trait Canonicalize { - fn canonicalize(&self) -> Self; -} - -impl Canonicalize for FilePath { - fn canonicalize(&self) -> FilePath { - let mut file_path = Vec::new(); - let mut file_path_components = self.file_path.clone().into_iter(); - - loop { - let component = file_path_components.next(); - match component.as_ref() { - // ─────────────────── - // canonicalize(ε) = ε - None => break, - - // canonicalize(directory₀) = directory₁ - // ─────────────────────────────────────── - // canonicalize(directory₀/.) = directory₁ - Some(c) if c == "." => continue, - - Some(c) if c == ".." => match file_path_components.next() { - // canonicalize(directory₀) = ε - // ──────────────────────────── - // canonicalize(directory₀/..) = /.. - None => file_path.push("..".to_string()), - - // canonicalize(directory₀) = directory₁/.. - // ────────────────────────────────────────────── - // canonicalize(directory₀/..) = directory₁/../.. - Some(ref c) if c == ".." => { - file_path.push("..".to_string()); - file_path.push("..".to_string()); - } - - // canonicalize(directory₀) = directory₁/component - // ─────────────────────────────────────────────── ; If "component" is not - // canonicalize(directory₀/..) = directory₁ ; ".." - Some(_) => continue, - }, - - // canonicalize(directory₀) = directory₁ - // ───────────────────────────────────────────────────────── ; If no other - // canonicalize(directory₀/component) = directory₁/component ; rule matches - Some(c) => file_path.push(c.clone()), - } - } - - FilePath { file_path } - } -} - -impl Canonicalize for ImportLocation { - fn canonicalize(&self) -> ImportLocation { - match self { - ImportLocation::Local(prefix, file) => { - ImportLocation::Local(*prefix, file.canonicalize()) - } - ImportLocation::Remote(url) => ImportLocation::Remote(URL { - scheme: url.scheme, - authority: url.authority.clone(), - path: url.path.canonicalize(), - query: url.query.clone(), - headers: url.headers.clone(), - }), - ImportLocation::Env(name) => ImportLocation::Env(name.to_string()), - ImportLocation::Missing => ImportLocation::Missing, - } - } -} -- cgit v1.2.3