From 52f9ecfc4dac65d305fd920e8c7f748889a0804f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 12 Aug 2019 23:24:48 +0200 Subject: Move api into its own crate --- dhall/src/core/mod.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs index a202e72..0667df8 100644 --- a/dhall/src/core/mod.rs +++ b/dhall/src/core/mod.rs @@ -1,4 +1,4 @@ -pub(crate) mod context; -pub(crate) mod thunk; -pub(crate) mod value; -pub(crate) mod var; +pub mod context; +pub mod thunk; +pub mod value; +pub mod var; -- cgit v1.2.3 From 1ed3123aeb3c9272b6810605a7ee781c42095f09 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:20:35 +0200 Subject: Swap Typed and TypeThunk --- dhall/src/core/thunk.rs | 125 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 104 insertions(+), 21 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index f41579c..740ecbc 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -1,15 +1,18 @@ +use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{ExprF, X}; +use dhall_syntax::{Const, ExprF, X}; -use crate::core::context::NormalizationContext; +use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; -use crate::phase::{Type, Typed}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -42,7 +45,16 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub struct TypeThunk(Typed); +pub enum TypeThunk { + // Any value, along with (optionally) its type + Untyped(Thunk), + Typed(Thunk, Box), + // One of the base higher-kinded typed. + // Used to avoid storing the same tower ot Type->Kind->Sort + // over and over again. Also enables having Sort as a type + // even though it doesn't itself have a type. + Const(Const), +} impl ThunkInternal { fn into_thunk(self) -> Thunk { @@ -190,39 +202,94 @@ impl TypeThunk { } pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk(Typed::from_thunk_untyped(th)) + TypeThunk::from_thunk_untyped(th) } pub fn from_type(t: Type) -> TypeThunk { - TypeThunk(t) + t.into_typethunk() } - pub fn normalize_mut(&mut self) { - self.0.normalize_mut() + pub fn normalize_nf(&self) -> Value { + match self { + TypeThunk::Const(c) => Value::Const(*c), + TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + thunk.normalize_nf().clone() + } + } } - pub fn normalize_nf(&self) -> Value { - self.0.to_value().normalize() + pub fn to_typed(&self) -> Typed { + self.clone().into_typed() } - pub fn to_value(&self) -> Value { - self.0.to_value() + pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub fn to_thunk(&self) -> Thunk { - self.0.to_thunk() + pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + TypeThunk::Typed(th, Box::new(t)) + } + pub fn from_thunk_untyped(th: Thunk) -> Self { + TypeThunk::Untyped(th) + } + pub fn from_const(c: Const) -> Self { + TypeThunk::Const(c) + } + pub fn from_value_untyped(v: Value) -> Self { + TypeThunk::from_thunk_untyped(Thunk::from_value(v)) } + // TODO: Avoid cloning if possible + pub fn to_value(&self) -> Value { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), + TypeThunk::Const(c) => Value::Const(*c), + } + } + pub fn to_expr(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr() + } + pub fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr_maybe_alpha(true) + } + pub fn to_thunk(&self) -> Thunk { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), + TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + } + } pub fn to_type(&self) -> Type { - self.0.to_type() + self.clone().into_typed().into_type() + } + pub fn into_typed(self) -> Typed { + Typed::from_typethunk(self) + } + pub fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_value() { + Value::Const(c) => Some(*c), + _ => None, + } } - pub fn to_typed(&self) -> Typed { - self.0.clone() + pub fn normalize_mut(&mut self) { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + th.normalize_mut() + } + TypeThunk::Const(_) => {} + } } - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + pub fn get_type(&self) -> Result, TypeError> { + match self { + TypeThunk::Untyped(_) => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, + )), + TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + } } } @@ -254,7 +321,14 @@ impl Shift for ThunkInternal { impl Shift for TypeThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypeThunk(self.0.shift(delta, var)?)) + Some(match self { + TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.shift(delta, var)?, + Box::new(t.shift(delta, var)?), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + }) } } @@ -293,7 +367,16 @@ impl Subst for ThunkInternal { impl Subst for TypeThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypeThunk(self.0.subst_shift(var, val)) + match self { + TypeThunk::Untyped(th) => { + TypeThunk::Untyped(th.subst_shift(var, val)) + } + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.subst_shift(var, val), + Box::new(t.subst_shift(var, val)), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + } } } -- cgit v1.2.3 From fb0120dffe8e9552c3da7b994ad850f66dc612a3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:21:54 +0200 Subject: s/TypeThunk/TypedThunk/g --- dhall/src/core/thunk.rs | 68 +++++++++++++++++++++++++------------------------ dhall/src/core/value.rs | 24 ++++++++--------- 2 files changed, 47 insertions(+), 45 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 740ecbc..38c54f7 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -45,7 +45,7 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub enum TypeThunk { +pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), @@ -196,23 +196,23 @@ impl Thunk { } } -impl TypeThunk { - pub fn from_value(v: Value) -> TypeThunk { - TypeThunk::from_thunk(Thunk::from_value(v)) +impl TypedThunk { + pub fn from_value(v: Value) -> TypedThunk { + TypedThunk::from_thunk(Thunk::from_value(v)) } - pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk::from_thunk_untyped(th) + pub fn from_thunk(th: Thunk) -> TypedThunk { + TypedThunk::from_thunk_untyped(th) } - pub fn from_type(t: Type) -> TypeThunk { + pub fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } pub fn normalize_nf(&self) -> Value { match self { - TypeThunk::Const(c) => Value::Const(*c), - TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } } @@ -227,23 +227,23 @@ impl TypeThunk { } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - TypeThunk::Typed(th, Box::new(t)) + TypedThunk::Typed(th, Box::new(t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - TypeThunk::Untyped(th) + TypedThunk::Untyped(th) } pub fn from_const(c: Const) -> Self { - TypeThunk::Const(c) + TypedThunk::Const(c) } pub fn from_value_untyped(v: Value) -> Self { - TypeThunk::from_thunk_untyped(Thunk::from_value(v)) + TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), - TypeThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), + TypedThunk::Const(c) => Value::Const(*c), } } pub fn to_expr(&self) -> NormalizedSubExpr { @@ -254,8 +254,8 @@ impl TypeThunk { } pub fn to_thunk(&self) -> Thunk { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), - TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), + TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), } } pub fn to_type(&self) -> Type { @@ -274,21 +274,21 @@ impl TypeThunk { pub fn normalize_mut(&mut self) { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.normalize_mut() } - TypeThunk::Const(_) => {} + TypedThunk::Const(_) => {} } } pub fn get_type(&self) -> Result, TypeError> { match self { - TypeThunk::Untyped(_) => Err(TypeError::new( + TypedThunk::Untyped(_) => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, )), - TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), - TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } } @@ -319,15 +319,17 @@ impl Shift for ThunkInternal { } } -impl Shift for TypeThunk { +impl Shift for TypedThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.shift(delta, var)?) + } + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.shift(delta, var)?, Box::new(t.shift(delta, var)?), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), }) } } @@ -365,17 +367,17 @@ impl Subst for ThunkInternal { } } -impl Subst for TypeThunk { +impl Subst for TypedThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - TypeThunk::Untyped(th) => { - TypeThunk::Untyped(th.subst_shift(var, val)) + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.subst_shift(var, val)) } - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.subst_shift(var, val), Box::new(t.subst_shift(var, val)), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), } } } @@ -387,9 +389,9 @@ impl std::cmp::PartialEq for Thunk { } impl std::cmp::Eq for Thunk {} -impl std::cmp::PartialEq for TypeThunk { +impl std::cmp::PartialEq for TypedThunk { fn eq(&self, other: &Self) -> bool { self.to_value() == other.to_value() } } -impl std::cmp::Eq for TypeThunk {} +impl std::cmp::Eq for TypedThunk {} diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0b68bf6..8486d6e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, X, }; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, @@ -26,15 +26,15 @@ use crate::phase::Typed; #[derive(Debug, Clone, PartialEq, Eq)] pub enum Value { /// Closures - Lam(AlphaLabel, TypeThunk, Thunk), - Pi(AlphaLabel, TypeThunk, TypeThunk), + Lam(AlphaLabel, TypedThunk, Thunk), + Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypeThunk), + OptionalSomeClosure(TypedThunk), /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypeThunk, Option), + ListConsClosure(TypedThunk, Option), /// `λ(x : Natural) -> x + 1` NaturalSuccClosure, @@ -44,20 +44,20 @@ pub enum Value { NaturalLit(Natural), IntegerLit(Integer), DoubleLit(NaiveDouble), - EmptyOptionalLit(TypeThunk), + EmptyOptionalLit(TypedThunk), NEOptionalLit(Thunk), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypeThunk), + EmptyListLit(TypedThunk), NEListLit(Vec), RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Thunk, HashMap>), // Invariant: this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), - Equivalence(TypeThunk, TypeThunk), + Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } -- cgit v1.2.3 From cbd62bb57bcc94e0133c57437488a5af22a0b1c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:34:38 +0200 Subject: Typos --- dhall/src/core/thunk.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 38c54f7..c18014e 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -49,9 +49,9 @@ pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), - // One of the base higher-kinded typed. + // One of the base higher-kinded types. // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a type + // over and over again. Also enables having Sort as a value // even though it doesn't itself have a type. Const(Const), } -- cgit v1.2.3 From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 20:54:15 +0200 Subject: Stop tracking the absence of Embed values at the type level --- dhall/src/core/thunk.rs | 12 ++++++------ dhall/src/core/value.rs | 10 +++++----- 2 files changed, 11 insertions(+), 11 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index c18014e..4d193f9 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF, X}; +use dhall_syntax::{Const, ExprF}; use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; @@ -12,7 +12,7 @@ use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; use crate::phase::typecheck::type_of_const; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -30,7 +30,7 @@ enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. - PartialExpr(ExprF), + PartialExpr(ExprF), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized Value(Marker, Value), @@ -123,7 +123,7 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF) -> Thunk { + pub fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } @@ -309,7 +309,7 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +356,7 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8486d6e..88d7a20 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, X, + NaiveDouble, Natural, }; use crate::core::thunk::{Thunk, TypedThunk}; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; -use crate::phase::Typed; +use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the @@ -59,7 +59,7 @@ pub enum Value { TextLit(Vec>), Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } impl Value { @@ -475,7 +475,7 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +500,7 @@ impl Subst for Value { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, )) } // Retry normalizing since substituting may allow progress -- cgit v1.2.3 From 51dbaa0b66089bca63aa9cf69a1e0ec59df053b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 21:10:59 +0200 Subject: Considerably simplify Embed handling --- dhall/src/core/thunk.rs | 2 -- dhall/src/core/value.rs | 8 +++----- 2 files changed, 3 insertions(+), 7 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 4d193f9..7c5c537 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -309,7 +309,6 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(Normalized::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +355,6 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - Normalized::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 88d7a20..20a6021 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -243,7 +243,7 @@ impl Value { y.normalize_to_expr_maybe_alpha(alpha), )), Value::PartialExpr(e) => { - rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha))) + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } } @@ -333,8 +333,8 @@ impl Value { y.normalize_mut(); } Value::PartialExpr(e) => { - // TODO: need map_mut_simple - e.map_ref_simple(|v| { + // TODO: need map_mut + e.map_ref(|v| { v.normalize_nf(); }); } @@ -475,7 +475,6 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +499,6 @@ impl Subst for Value { &val.under_binder(x), ) }, - Normalized::clone, )) } // Retry normalizing since substituting may allow progress -- cgit v1.2.3 From 67cdda53d95057174b86878f22dbc0efc0255fd9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 14 Aug 2019 22:55:00 +0200 Subject: Fix typo in normalization --- dhall/src/core/value.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 20a6021..845596b 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -107,7 +107,7 @@ impl Value { )) }; (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - rc(ExprF::Pi( + rc(ExprF::Lam( stringify!($var).into(), make_expr!($($ty)*), make_expr!($($rest)*) -- cgit v1.2.3 From ba19f41873fec98bb24ba709f4b76c3f58ca5aaa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 13:05:23 +0200 Subject: Fix bug in shifting contexts --- dhall/src/core/context.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 62affcf..8d14415 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -97,7 +97,16 @@ impl Context { where T: Clone + Shift, { - Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) + if delta < 0 { + Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) + } else { + Some(Context(Rc::new( + self.0 + .iter() + .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) + .collect::>()?, + ))) + } } fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self where -- cgit v1.2.3 From aabca76a62256aa7cad66c2016ed504e49651d5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 13:06:56 +0200 Subject: Remove special closures from Value Instead construct their values directly --- dhall/src/core/value.rs | 95 +------------------------------------------------ dhall/src/core/var.rs | 6 ++++ 2 files changed, 7 insertions(+), 94 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 845596b..036a20c 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -30,13 +30,6 @@ pub enum Value { Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), - /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypedThunk), - /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` - /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypedThunk, Option), - /// `λ(x : Natural) -> x + 1` - NaturalSuccClosure, Var(AlphaVar), Const(Const), @@ -74,47 +67,6 @@ impl Value { /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - // Ad-hoc macro to help construct the unapplied closures - macro_rules! make_expr { - (Natural) => { rc(ExprF::Builtin(Builtin::Natural)) }; - (var($var:ident)) => { - rc(ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))) - }; - ($var:ident) => { $var }; - (List $($rest:tt)*) => { - rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - make_expr!($($rest)*) - )) - }; - (Some $($rest:tt)*) => { - rc(ExprF::SomeLit( - make_expr!($($rest)*) - )) - }; - (1 + $($rest:tt)*) => { - rc(ExprF::BinOp( - dhall_syntax::BinOp::NaturalPlus, - rc(ExprF::NaturalLit(1)), - make_expr!($($rest)*) - )) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => { - rc(ExprF::BinOp( - dhall_syntax::BinOp::ListAppend, - rc(ExprF::NEListLit(vec![make_expr!($($head)*)])), - make_expr!($($tail)*) - )) - }; - (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - rc(ExprF::Lam( - stringify!($var).into(), - make_expr!($($ty)*), - make_expr!($($rest)*) - )) - }; - } - match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -131,27 +83,6 @@ impl Value { } e } - Value::OptionalSomeClosure(n) => { - let a = n.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(x: a) -> Some var(x)) - } - Value::ListConsClosure(a, None) => { - // Avoid accidental capture of the new `x` variable - let a1 = a.under_binder(Label::from("x")); - let a1 = a1.normalize_to_expr_maybe_alpha(alpha); - let a = a.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(x : a) -> λ(xs : List a1) -> [ var(x) ] # var(xs)) - } - Value::ListConsClosure(n, Some(v)) => { - // Avoid accidental capture of the new `xs` variable - let v = v.under_binder(Label::from("xs")); - let v = v.normalize_to_expr_maybe_alpha(alpha); - let a = n.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(xs : List a) -> [ v ] # var(xs)) - } - Value::NaturalSuccClosure => { - make_expr!(λ(x : Natural) -> 1 + var(x)) - } Value::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), t.normalize_to_expr_maybe_alpha(alpha), @@ -257,8 +188,7 @@ impl Value { pub fn normalize_mut(&mut self) { match self { - Value::NaturalSuccClosure - | Value::Var(_) + Value::Var(_) | Value::Const(_) | Value::BoolLit(_) | Value::NaturalLit(_) @@ -266,7 +196,6 @@ impl Value { | Value::DoubleLit(_) => {} Value::EmptyOptionalLit(tth) - | Value::OptionalSomeClosure(tth) | Value::EmptyListLit(tth) => { tth.normalize_mut(); } @@ -287,12 +216,6 @@ impl Value { x.normalize_mut(); } } - Value::ListConsClosure(t, v) => { - t.normalize_mut(); - for x in v.iter_mut() { - x.normalize_mut(); - } - } Value::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); @@ -375,14 +298,6 @@ impl Shift for Value { .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.shift(delta, var)?) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.shift(delta, var)?, - v.as_ref().map(|v| Ok(v.shift(delta, var)?)).transpose()?, - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.shift(delta, var)?, @@ -516,14 +431,6 @@ impl Subst for Value { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.subst_shift(var, val)) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.subst_shift(var, val), - v.as_ref().map(|v| v.subst_shift(var, val)), - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.subst_shift(var, val), diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index 35bff80..0faa091 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -67,6 +67,12 @@ impl AlphaVar { alpha: None, } } + pub fn from_var_and_alpha(normal: V