summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril Feneanar2019-08-26 19:52:11 +0200
committerGitHub2019-08-26 19:52:11 +0200
commit2f6ae31f4682266e647d25f7554a66d543bec7ac (patch)
tree700aa667954dff91599420f75aa55d606c7b04dd
parent38a82c53ef45e802cf5816a8afcbf36a69c91174 (diff)
parent829fff5bd3e2115c0a16d40a4dc266747d622b08 (diff)
Merge pull request #105 from Nadrieril/keep-type-info
Store type information everywhere in `Value`
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs148
-rw-r--r--dhall/src/core/valuef.rs42
-rw-r--r--dhall/src/error/mod.rs1
-rw-r--r--dhall/src/phase/mod.rs46
-rw-r--r--dhall/src/phase/normalize.rs592
-rw-r--r--dhall/src/phase/typecheck.rs131
-rw-r--r--dhall/src/tests.rs2
-rw-r--r--serde_dhall/src/lib.rs30
-rw-r--r--tests_buffer10
9 files changed, 521 insertions, 481 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5367c86..21ac288 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,19 +1,18 @@
-use std::borrow::Cow;
use std::cell::{Ref, RefCell, RefMut};
use std::rc::Rc;
-use dhall_syntax::Const;
+use dhall_syntax::{Builtin, Const};
use crate::core::context::TypecheckContext;
use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
-use crate::phase::typecheck::const_to_value;
+use crate::phase::normalize::{apply_any, normalize_whnf};
+use crate::phase::typecheck::{builtin_to_value, const_to_value};
use crate::phase::{NormalizedSubExpr, Typed};
#[derive(Debug, Clone, Copy)]
-enum Form {
+pub(crate) enum Form {
/// No constraints; expression may not be normalized at all.
Unevaled,
/// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
@@ -28,13 +27,14 @@ enum Form {
}
use Form::{Unevaled, NF, WHNF};
-#[derive(Debug)]
/// Partially normalized value.
/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
/// Invariant: if `form` is `NF`, `value` must be fully normalized
+#[derive(Debug)]
struct ValueInternal {
form: Form,
value: ValueF,
+ /// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
}
@@ -42,7 +42,7 @@ struct ValueInternal {
/// sharing computation automatically. Uses a RefCell to share computation.
/// Can optionally store a type from typechecking to preserve type information.
#[derive(Clone)]
-pub struct Value(Rc<RefCell<ValueInternal>>);
+pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
impl ValueInternal {
fn into_value(self) -> Value {
@@ -53,15 +53,30 @@ impl ValueInternal {
}
fn normalize_whnf(&mut self) {
- take_mut::take(self, |vint| match &vint.form {
- Unevaled => ValueInternal {
- form: WHNF,
- value: normalize_whnf(vint.value),
- ty: vint.ty,
+ take_mut::take_or_recover(
+ self,
+ // Dummy value in case the other closure panics
+ || ValueInternal {
+ form: Unevaled,
+ value: ValueF::Const(Const::Type),
+ ty: None,
},
- // Already in WHNF
- WHNF | NF => vint,
- })
+ |vint| match (&vint.form, &vint.ty) {
+ (Unevaled, Some(ty)) => ValueInternal {
+ form: WHNF,
+ value: normalize_whnf(vint.value, &ty),
+ ty: vint.ty,
+ },
+ // `value` is `Sort`
+ (Unevaled, None) => ValueInternal {
+ form: NF,
+ value: ValueF::Const(Const::Sort),
+ ty: None,
+ },
+ // Already in WHNF
+ (WHNF, _) | (NF, _) => vint,
+ },
+ )
}
fn normalize_nf(&mut self) {
match self.form {
@@ -81,39 +96,41 @@ impl ValueInternal {
fn get_type(&self) -> Result<&Value, TypeError> {
match &self.ty {
Some(t) => Ok(t),
- None => Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- )),
+ None => {
+ Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+ }
}
}
}
impl Value {
- pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
+ fn new(value: ValueF, form: Form, ty: Value) -> Value {
ValueInternal {
- form: Unevaled,
- value: v,
- ty: None,
+ form,
+ value,
+ ty: Some(ty),
}
.into_value()
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+ pub(crate) fn const_sort() -> Value {
ValueInternal {
- form: Unevaled,
- value: v,
- ty: Some(t),
+ form: NF,
+ value: ValueF::Const(Const::Sort),
+ ty: None,
}
.into_value()
}
- pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
- Value::from_valuef_and_type(v, Value::from_const(Const::Type))
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+ Value::new(v, Unevaled, t)
+ }
+ pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+ Value::new(v, WHNF, t)
}
pub(crate) fn from_const(c: Const) -> Self {
const_to_value(c)
}
- pub fn const_type() -> Self {
- Value::from_const(Const::Type)
+ pub(crate) fn from_builtin(b: Builtin) -> Self {
+ builtin_to_value(b)
}
pub(crate) fn as_const(&self) -> Option<Const> {
@@ -156,10 +173,14 @@ impl Value {
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.as_whnf().normalize_to_expr_maybe_alpha(true)
}
- /// TODO: cloning a valuef can often be avoided
- pub(crate) fn to_whnf(&self) -> ValueF {
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
self.as_whnf().clone()
}
+ /// Before discarding type information, check that it matches the expected return type.
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+ self.check_type(ty);
+ self.to_whnf_ignore_type()
+ }
pub(crate) fn into_typed(self) -> Typed {
Typed::from_value(self)
}
@@ -205,16 +226,40 @@ impl Value {
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
- ) -> OutputSubExpr {
+ ) -> NormalizedSubExpr {
self.as_nf().normalize_to_expr_maybe_alpha(alpha)
}
- pub(crate) fn app_value(&self, th: Value) -> ValueF {
- apply_any(self.clone(), th)
+ pub(crate) fn app(&self, v: Value) -> Value {
+ let body_t = match &*self.get_type_not_sort().as_whnf() {
+ ValueF::Pi(x, t, e) => {
+ v.check_type(t);
+ e.subst_shift(&x.into(), &v)
+ }
+ _ => unreachable!("Internal type error"),
+ };
+ Value::from_valuef_and_type_whnf(
+ apply_any(self.clone(), v, &body_t),
+ body_t,
+ )
}
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
- Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
+ /// In debug mode, panic if the provided type doesn't match the value's type.
+ /// Otherwise does nothing.
+ pub(crate) fn check_type(&self, ty: &Value) {
+ debug_assert_eq!(
+ Some(ty),
+ self.get_type().ok().as_ref(),
+ "Internal type error"
+ );
+ }
+ pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+ Ok(self.as_internal().get_type()?.clone())
+ }
+ /// When we know the value isn't `Sort`, this gets the type directly
+ pub(crate) fn get_type_not_sort(&self) -> Value {
+ self.get_type()
+ .expect("Internal type error: value is `Sort` but shouldn't be")
}
}
@@ -236,7 +281,17 @@ impl Shift for ValueInternal {
impl Subst<Value> for Value {
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
- Value(self.0.subst_shift(var, val))
+ match &*self.as_valuef() {
+ // If the var matches, we can just reuse the provided value instead of copying it.
+ // We also check that the types match, if in debug mode.
+ ValueF::Var(v) if v == var => {
+ if let Ok(self_ty) = self.get_type() {
+ val.check_type(&self_ty.subst_shift(var, val));
+ }
+ val.clone()
+ }
+ _ => Value(self.0.subst_shift(var, val)),
+ }
}
}
@@ -262,8 +317,17 @@ impl std::cmp::Eq for Value {}
impl std::fmt::Debug for Value {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let vint: &ValueInternal = &self.as_internal();
- fmt.debug_tuple(&format!("Value@{:?}", &vint.form))
- .field(&vint.value)
- .finish()
+ if let ValueF::Const(c) = &vint.value {
+ write!(fmt, "{:?}", c)
+ } else {
+ let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
+ x.field("value", &vint.value);
+ if let Some(ty) = vint.ty.as_ref() {
+ x.field("type", &ty);
+ } else {
+ x.field("type", &None::<()>);
+ }
+ x.finish()
+ }
}
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 0c3058d..9ea2467 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,8 +7,7 @@ use dhall_syntax::{
use crate::core::value::Value;
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::OutputSubExpr;
-use crate::phase::Normalized;
+use crate::phase::{Normalized, NormalizedSubExpr};
/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
/// normalized on-demand.
@@ -16,11 +15,11 @@ use crate::phase::Normalized;
/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
/// recursively normalize as needed.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ValueF {
+pub(crate) enum ValueF {
/// Closures
Lam(AlphaLabel, Value, Value),
Pi(AlphaLabel, Value, Value),
- // Invariant: the evaluation must not be able to progress further.
+ // Invariant: in whnf, the evaluation must not be able to progress further.
AppliedBuiltin(Builtin, Vec<Value>),
Var(AlphaVar),
@@ -34,32 +33,26 @@ pub enum ValueF {
// EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(Value),
NEListLit(Vec<Value>),
- RecordLit(HashMap<Label, Value>),
RecordType(HashMap<Label, Value>),
+ RecordLit(HashMap<Label, Value>),
UnionType(HashMap<Label, Option<Value>>),
UnionConstructor(Label, HashMap<Label, Option<Value>>),
UnionLit(Label, Value, HashMap<Label, Option<Value>>),
- // Invariant: this must not contain interpolations that are themselves TextLits, and
+ // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Value>>),
Equivalence(Value, Value),
- // Invariant: this must not contain a value captured by one of the variants above.
+ // Invariant: in whnf, this must not contain a value captured by one of the variants above.
PartialExpr(ExprF<Value, Normalized>),
}
impl ValueF {
- pub(crate) fn into_value_untyped(self) -> Value {
- Value::from_valuef_untyped(self)
- }
pub(crate) fn into_value_with_type(self, t: Value) -> Value {
Value::from_valuef_and_type(self, t)
}
- pub(crate) fn into_value_simple_type(self) -> Value {
- Value::from_valuef_simple_type(self)
- }
/// Convert the value to a fully normalized syntactic expression
- pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+ pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
self.normalize_to_expr_maybe_alpha(false)
}
/// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -67,7 +60,7 @@ impl ValueF {
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
- ) -> OutputSubExpr {
+ ) -> NormalizedSubExpr {
match self {
ValueF::Lam(x, t, e) => rc(ExprF::Lam(
x.to_label_maybe_alpha(alpha),
@@ -257,22 +250,7 @@ impl ValueF {
}
}
- /// Apply to a valuef
- pub(crate) fn app(self, val: ValueF) -> ValueF {
- self.app_valuef(val)
- }
-
- /// Apply to a valuef
- pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
- self.app_value(val.into_value_untyped())
- }
-
- /// Apply to a value
- pub fn app_value(self, th: Value) -> ValueF {
- Value::from_valuef_untyped(self).app_value(th)
- }
-
- pub fn from_builtin(b: Builtin) -> ValueF {
+ pub(crate) fn from_builtin(b: Builtin) -> ValueF {
ValueF::AppliedBuiltin(b, vec![])
}
}
@@ -355,7 +333,7 @@ impl Subst<Value> for ValueF {
t.subst_shift(var, val),
e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
),
- ValueF::Var(v) if v == var => val.to_whnf(),
+ ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
ValueF::Const(c) => ValueF::Const(*c),
ValueF::BoolLit(b) => ValueF::BoolLit(*b),
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13a9d7e..2ddaf3d 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -54,7 +54,6 @@ pub(crate) enum TypeMessage {
NotAFunction(Value),
TypeMismatch(Value, Value, Value),
AnnotMismatch(Value, Value),
- Untyped,
InvalidListElement(usize, Value, Value),
InvalidListType(Value),
InvalidOptionalType(Value),
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 1f7e5f0..ecf04e9 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,8 +1,7 @@
-use std::borrow::Cow;
use std::fmt::Display;
use std::path::Path;
-use dhall_syntax::{Const, SubExpr};
+use dhall_syntax::{Builtin, Const, SubExpr};
use crate::core::value::Value;
use crate::core::valuef::ValueF;
@@ -93,13 +92,13 @@ impl Typed {
pub(crate) fn from_const(c: Const) -> Self {
Typed(Value::from_const(c))
}
- pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
Typed(Value::from_valuef_and_type(v, t.into_value()))
}
pub(crate) fn from_value(th: Value) -> Self {
Typed(th)
}
- pub fn const_type() -> Self {
+ pub(crate) fn const_type() -> Self {
Typed::from_const(Const::Type)
}
@@ -109,7 +108,7 @@ impl Typed {
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.0.to_expr_alpha()
}
- pub fn to_value(&self) -> Value {
+ pub(crate) fn to_value(&self) -> Value {
self.0.clone()
}
pub(crate) fn into_value(self) -> Value {
@@ -121,8 +120,41 @@ impl Typed {
}
#[allow(dead_code)]
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> {
- Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed()))
+ pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
+ Ok(self.0.get_type()?.into_typed())
+ }
+
+ pub fn make_builtin_type(b: Builtin) -> Self {
+ Typed::from_value(Value::from_builtin(b))
+ }
+ pub fn make_optional_type(t: Typed) -> Self {
+ Typed::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_record_type(
+ kts: impl Iterator<Item = (String, Typed)>,
+ ) -> Self {
+ Typed::from_valuef_and_type(
+ ValueF::RecordType(
+ kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+ ),
+ Typed::const_type(),
+ )
+ }
+ pub fn make_union_type(
+ kts: impl Iterator<Item = (String, Option<Typed>)>,
+ ) -> Self {
+ Typed::from_valuef_and_type(
+ ValueF::UnionType(
+ kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+ .collect(),
+ ),
+ Typed::const_type(),
+ )
}
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a379a4b..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,5 +1,6 @@
use std::collections::HashMap;
+use dhall_syntax::Const::Type;
use dhall_syntax::{
BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
NaiveDouble,
@@ -7,42 +8,43 @@ use dhall_syntax::{
use crate::core::value::Value;
use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
-
-pub(crate) type OutputSubExpr = NormalizedSubExpr;
+use crate::core::var::{AlphaLabel, Shift, Subst};
+use crate::phase::Normalized;
// Ad-hoc macro to help construct closures
macro_rules! make_closure {
(#$var:ident) => { $var.clone() };
- (var($var:ident, $n:expr)) => {{
+ (var($var:ident, $n:expr, $($ty:tt)*)) => {{
let var = crate::core::var::AlphaVar::from_var_and_alpha(
Label::from(stringify!($var)).into(),
$n
);
- ValueF::Var(var).into_value_untyped()
+ ValueF::Var(var)
+ .into_value_with_type(make_closure!($($ty)*))
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
- (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
- ValueF::Lam(
- Label::from(stringify!($var)).into(),
- make_closure!($($ty)*),
- make_closure!($($rest)*),
- ).into_value_untyped()
- };
+ (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+ let var: AlphaLabel = Label::from(stringify!($var)).into();
+ let ty = make_closure!($($ty)*);
+ let body = make_closure!($($body)*);
+ let body_ty = body.get_type_not_sort();
+ let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+ .into_value_with_type(Value::from_const(Type));
+ ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+ }};
(Natural) => {
- ValueF::from_builtin(Builtin::Natural)
- .into_value_simple_type()
+ Value::from_builtin(Builtin::Natural)
};
(List $($rest:tt)*) => {
- ValueF::from_builtin(Builtin::List)
- .app_value(make_closure!($($rest)*))
- .into_value_simple_type()
- };
- (Some($($rest:tt)*)) => {
- ValueF::NEOptionalLit(make_closure!($($rest)*))
- .into_value_untyped()
+ Value::from_builtin(Builtin::List)
+ .app(make_closure!($($rest)*))
};
+ (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);
+ ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+ }};
(1 + $($rest:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::NaturalPlus,
@@ -55,81 +57,99 @@ macro_rules! make_closure {
make_closure!(Natural)
)
};
- ([ $($head:tt)* ] # $($tail:tt)*) => {
+ ([ $($head:tt)* ] # $($tail:tt)*) => {{
+ let head = make_closure!($($head)*);
+ let tail = make_closure!($($tail)*);
+ let list_type = tail.get_type_not_sort();
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::ListAppend,
- ValueF::NEListLit(vec![make_closure!($($head)*)])
- .into_value_untyped(),
- make_closure!($($tail)*),
- )).into_value_untyped()
- };
+ ValueF::NEListLit(vec![head])
+ .into_value_with_type(list_type.clone()),
+ tail,
+ )).into_value_with_type(list_type)
+ }};
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
+pub(crate) fn apply_builtin(
+ b: Builtin,
+ args: Vec<Value>,
+ ty: &Value,
+) -> ValueF {
use dhall_syntax::Builtin::*;
use ValueF::*;
- // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
+ // Small helper enum
+ enum Ret<'a> {
+ ValueF(ValueF),
+ 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 ret = match (b, args.as_slice()) {
- (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
- (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
- _ => Err(()),
+ (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (NaturalIsZero, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalEven, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
- _ => Err(()),
+ (NaturalEven, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
- _ => Err(()),
+ (NaturalOdd, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
- _ => Err(()),
+ (NaturalToInteger, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ _ => Ret::DoneAsIs,
},
- (NaturalShow, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
- )),
- _ => Err(()),
+ (NaturalShow, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
},
- (NaturalSubtract, [a, b, r..]) => {
- match (&*a.as_whnf(), &*b.as_whnf()) {
- (NaturalLit(a), NaturalLit(b)) => {
- Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
- }
- (NaturalLit(0), b) => Ok((r, b.clone())),
- (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
- _ if a == b => Ok((r, NaturalLit(0))),
- _ => Err(()),
+ (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+ (NaturalLit(a), NaturalLit(b)) => {
+ Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
}
- }
- (IntegerShow, [n, r..]) => match &*n.as_whnf() {
+ (NaturalLit(0), _) => Ret::Value(b.clone()),
+ (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ _ if a == b => Ret::ValueF(NaturalLit(0)),
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerShow, [n]) => match &*n.as_whnf() {
IntegerLit(n) => {
let s = if *n < 0 {
n.to_string()
} else {
format!("+{}", n)
};
- Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)])))
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
- IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
- _ => Err(()),
+ (IntegerToDouble, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+ }
+ _ => Ret::DoneAsIs,
},
- (DoubleShow, [n, r..]) => match &*n.as_whnf() {
- DoubleLit(n) => Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
- )),
- _ => Err(()),
+ (DoubleShow, [n]) => match &*n.as_whnf() {
+ DoubleLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
},
- (TextShow, [v, r..]) => match &*v.as_whnf() {
+ (TextShow, [v]) => match &*v.as_whnf() {
TextLit(elts) => {
match elts.as_slice() {
// Empty string literal.
@@ -138,10 +158,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
let txt: InterpolatedText<Normalized> =
std::iter::empty().collect();
let s = txt.to_string();
- Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
- ))
+ Ret::ValueF(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.
@@ -153,221 +172,238 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
))
.collect();
let s = txt.to_string();
- Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
- ))
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
}
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListLength, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, NaturalLit(0))),
- NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
- _ => Err(()),
+ (ListLength, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ _ => Ret::DoneAsIs,
},
- (ListHead, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
+ (ListHead, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
+ Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListLast, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
- }
- _ => Err(()),
+ (ListLast, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+ xs.iter().rev().next().unwrap().clone(),
+ )),
+ _ => Ret::DoneAsIs,
},
- (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
+ (ListReverse, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
+ Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(t) => {
- let mut kts = HashMap::new();
- kts.insert(
- "index".into(),
- Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
- );
- kts.insert("value".into(), t.clone());
- Ok((
- r,
- EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
- ))
- }
- NEListLit(xs) => {
- let xs = xs
- .iter()
- .enumerate()
- .map(|(i, e)| {
- let i = NaturalLit(i);
- let mut kvs = HashMap::new();
- kvs.insert(
- "index".into(),
- Value::from_valuef_untyped(i),
- );
- kvs.insert("value".into(), e.clone());
- Value::from_valuef_untyped(RecordLit(kvs))
- })
- .collect();
- Ok((r, NEListLit(xs)))
+ (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_valuef_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_valuef_and_type(
+ NaturalLit(i),
+ Value::from_builtin(
+ Builtin::Natural,
+ ),
+ ),
+ );
+ kvs.insert("value".into(), e.clone());
+ Value::from_valuef_and_type(
+ RecordLit(kvs),
+ t.clone(),
+ )
+ })
+ .collect(),
+ ),
+ _ => unreachable!(),
+ };
+ Ret::ValueF(list)
+ }
+ _ => Ret::DoneAsIs,
}
- _ => Err(()),
- },
- (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
+ }
+ (ListBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ret::Value(args[1].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
_ => {
- let list_t = ValueF::from_builtin(List)
- .app_value(t.clone())
- .into_value_simple_type();
- Ok((
- r,
- f.app_value(list_t.clone())
- .app_value({
- // Move `t` under new `x` variable
+ 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("x"));
+ let t2 = t1.under_binder(Label::from("xs"));
make_closure!(
λ(x : #t) ->
λ(xs : List #t1) ->
- [ var(x, 1) ] # var(xs, 0)
+ [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
)
})
- .app_value(
+ .app(
EmptyListLit(t.clone())
.into_value_with_type(list_t),
),
- ))
+ )
}
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, nil.to_whnf())),
+ EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
NEListLit(xs) => {
let mut v = nil.clone();
- for x in xs.iter().rev() {
- v = cons
- .clone()
- .app_value(x.clone())
- .app_value(v)
- .into_value_untyped();
+ for x in xs.iter().cloned().rev() {
+ v = cons.app(x).app(v);
}
- Ok((r, v.to_whnf()))
+ Ret::ValueWithRemainingArgs(r, v)
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
+ (OptionalBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ret::Value(args[1].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
_ => {
- let optional_t = ValueF::from_builtin(Optional)
- .app_value(t.clone())
- .into_value_simple_type();
- Ok((
- r,
- f.app_value(optional_t.clone())
- .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
- .app_value(
+ 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("x"));
+ make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+ })
+ .app(
EmptyOptionalLit(t.clone())
.into_value_with_type(optional_t),
),
- ))
+ )
}
},
(OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
- EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
- NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
- _ => Err(()),
+ EmptyOptionalLit(_) => {
+ Ret::ValueWithRemainingArgs(r, nothing.clone())
+ }
+ NEOptionalLit(x) => {
+ Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+ }
+ _ => Ret::DoneAsIs,
},
- (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
+ (NaturalBuild, [f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
- Ok((r, args[0].to_whnf()))
+ Ret::Value(args[0].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
- _ => {
- let nat_type =
- ValueF::from_builtin(Natural).into_value_simple_type();
- Ok((
- r,
- f.app_value(nat_type.clone())
- .app_value(
- make_closure!(λ(x : Natural) -> 1 + var(x, 0)),
- )
- .app_value(
- NaturalLit(0).into_value_with_type(nat_type),
- ),
- ))
- }
+ _ => Ret::Value(
+ f.app(Value::from_builtin(Natural))
+ .app(make_closure!(
+ λ(x : Natural) -> 1 + var(x, 0, Natural)
+ ))
+ .app(
+ NaturalLit(0)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ ),
+ ),
},
(NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
- NaturalLit(0) => Ok((r, zero.to_whnf())),
+ NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
NaturalLit(n) => {
- let fold = ValueF::from_builtin(NaturalFold)
- .app(NaturalLit(n - 1))
- .app_value(t.clone())
- .app_value(succ.clone())
- .app_value(zero.clone())
- .into_value_with_type(t.clone());
- Ok((r, succ.app_value(fold)))
+ 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))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- _ => Err(()),
+ _ => Ret::DoneAsIs,
};
match ret {
- Ok((unconsumed_args, mut v)) => {
+ Ret::ValueF(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_value(x);
+ v = v.app(x);
}
- v
+ v.to_whnf_check_type(ty)
}
- Err(()) => AppliedBuiltin(b, args),
+ Ret::DoneAsIs => AppliedBuiltin(b, args),
}
}
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
- let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+ ValueF::Lam(x, _, e) => {
+ e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+ }
ValueF::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
- apply_builtin(*b, args)
+ apply_builtin(*b, args, ty)
}
ValueF::UnionConstructor(l, kts) => {
ValueF::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
- fallback(f, a)
+ ValueF::PartialExpr(ExprF::App(f, a))
}
}
}
@@ -414,53 +450,20 @@ pub(crate) fn squash_textlit(
ret
}
-/// Performs an intersection of two HashMaps.
-///
-/// # Arguments
-///
-/// * `f` - Will compute the final value from the intersecting
-/// key and the values from both maps.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `f` function.
-///
-/// The final map will contain the shared keys from the
-/// two input maps with the final computed value from `f`.
-pub(crate) fn intersection_with_key<K, T, U, V>(
- mut f: impl FnMut(&K, &T, &U) -> V,
- map1: &HashMap<K, T>,
- map2: &HashMap<K, U>,
-) -> HashMap<K, V>
-where
- K: std::hash::Hash + Eq + Clone,
-{
- let mut kvs = HashMap::new();
-
- for (k, t) in map1 {
- // Only insert in the final map if the key exists in both
- if let Some(u) = map2.get(k) {
- kvs.insert(k.clone(), f(k, t, u));
- }
- }
-
- kvs
-}
-
-pub(crate) fn merge_maps<K, V>(
+pub(crate) fn merge_maps<K, V, F, Err>(
map1: &HashMap<K, V>,
map2: &HashMap<K, V>,
- mut f: impl FnMut(&V, &V) -> V,
-) -> HashMap<K, V>
+ mut f: F,
+) -> Result<HashMap<K, V>, Err>
where
+ F: FnMut(&K, &V, &V) -> Result<V, Err>,
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(v1, v2)
+ f(x, v1, v2)?
} else {
v2.clone()
};
@@ -470,7 +473,7 @@ where
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v1.clone());
}
- kvs
+ Ok(kvs)
}
// Small helper enum to avoid repetition
@@ -481,7 +484,12 @@ enum Ret<'a> {
Expr(ExprF<Value, Normalized>),
}
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(
+ o: BinOp,
+ x: &'a Value,
+ y: &'a Value,
+ ty: &Value,
+) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -574,62 +582,62 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- )))
- });
+ let ty_borrow = ty.as_whnf();
+ let kts = match &*ty_borrow {
+ RecordType(kts) => kts,
+ _ => unreachable!("Internal type error"),
+ };
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+ Ok(Value::from_valuef_and_type(
+ ValueF::PartialExpr(ExprF::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ )),
+ kts.get(k).expect("Internal type error").clone(),
+ ))
+ })?;
Ret::ValueF(RecordLit(kvs))
}
- (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
- }
- (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
- }
- (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
- RecursiveRecordTypeMerge,
- v1.clone(),
- v2.clone(),
- )))
- });
- Ret::ValueF(RecordType(kvs))
- }
-
- (Equivalence, _, _) => {
- Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+ (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
+ unreachable!("This case should have been handled in typecheck")
}
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(
+ expr: ExprF<Value, Normalized>,
+ ty: &Value,
+) -> ValueF {
use ValueF::{
- AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
- NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
- TextLit, UnionConstructor, UnionLit, UnionType,
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+ NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+ UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
ExprF::Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
- ExprF::Embed(_) => unreachable!(),
- ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => Ret::Value(x),
+ // Those cases have already been completely handled in the typechecking phase (using
+ // `RetWhole`), so they won't appear here.
+ ExprF::Lam(_, _, _)
+ | ExprF::Pi(_, _, _)
+ | ExprF::Let(_, _, _, _)
+ | ExprF::Embed(_)
+ | ExprF::Const(_)
+ | ExprF::Builtin(_)
+ | ExprF::Var(_)
+ | ExprF::Annot(_, _)
+ | ExprF::RecordType(_)
+ | ExprF::UnionType(_) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
ExprF::Assert(_) => Ret::Expr(expr),
- ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
- ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
- ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
- ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
- ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
- ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
+ ExprF::App(v, a) => Ret::Value(v.app(a)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -654,12 +662,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
ExprF::RecordLit(kvs) => {
Ret::ValueF(RecordLit(kvs.into_iter().collect()))
}
- ExprF::RecordType(kts) => {
- Ret::ValueF(RecordType(kts.into_iter().collect()))
- }
- ExprF::UnionType(kts) => {
- Ret::ValueF(UnionType(kts.into_iter().collect()))
- }
ExprF::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
@@ -692,7 +694,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
}
}
}
- ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
+ ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
@@ -749,7 +751,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::ValueF(h.app_value(v.clone())),
+ Some(h) => Ret::Value(h.app(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -767,17 +769,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
match ret {
Ret::ValueF(v) => v,
- Ret::Value(th) => th.as_whnf().clone(),
- Ret::ValueRef(th) => th.as_whnf().clone(),
+ Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::ValueRef(v) => v.to_whnf_check_type(ty),
Ret::Expr(expr) => ValueF::PartialExpr(expr),
}
}
/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
match v {
- ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
- ValueF::PartialExpr(e) => normalize_one_layer(e),
+ ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+ ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
ValueF::TextLit(elts) => {
ValueF::TextLit(squash_textlit(elts.into_iter()))
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 1ea87d1..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -31,7 +31,7 @@ fn tck_pi_type(
_ => {
return Err(TypeError::new(
&ctx2,
- InvalidOutputType(te.get_type()?.into_owned()),
+ InvalidOutputType(te.get_type()?),
))
}
};
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
- match c {
- Const::Type => Ok(const_to_value(Const::Kind)),
- Const::Kind => Ok(const_to_value(Const::Sort)),
- Const::Sort => {
- Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
- }
- }
-}
-
pub(crate) fn const_to_value(c: Const) -> Value {
let v = ValueF::Const(c);
- match type_of_const(c) {
- Ok(t) => Value::from_valuef_and_type(v, t),
- Err(_) => Value::from_valuef_untyped(v),
+ match c {
+ Const::Type => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ }
+ Const::Kind => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ }
+ Const::Sort => Value::const_sort(),
}
}
@@ -291,7 +286,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
Value::from_valuef_and_type(
- ValueF::PartialExpr(ExprF::Builtin(b)),
+ ValueF::from_builtin(b),
type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
)
}
@@ -307,14 +302,15 @@ fn type_with(
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
Ok(match e.as_ref() {
- Lam(x, t, b) => {
- let tx = type_with(ctx, t.clone())?;
- let ctx2 = ctx.insert_type(x, tx.clone());
- let b = type_with(&ctx2, b.clone())?;
- let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone());
- let tb = b.get_type()?.into_owned();
- let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
- Value::from_valuef_and_type(v, t)
+ Lam(var, annot, body) => {
+ let annot = type_with(ctx, annot.clone())?;
+ let ctx2 = ctx.insert_type(var, annot.clone());
+ let body = type_with(&ctx2, body.clone())?;
+ let body_type = body.get_type()?;
+ Value::from_valuef_and_type(
+ ValueF::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())?;
@@ -389,17 +385,17 @@ fn type_last_layer(
ValueF::Pi(x, tx, tb) => (x, tx, tb),
_ => return mkerr(NotAFunction(f.clone())),
};
- if a.get_type()?.as_ref() != tx {
+ if &a.get_type()? != tx {
return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
}
RetTypeOnly(tb.subst_shift(&x.into(), a))
}
Annot(x, t) => {
- if t != x.get_type()?.as_ref() {
+ if &x.get_type()? != t {
return mkerr(AnnotMismatch(x.clone(), t.clone()));
}
- RetTypeOnly(x.get_type()?.into_owned())
+ RetWhole(x.clone())
}
Assert(t) => {
match &*t.as_whnf() {
@@ -412,7 +408,7 @@ fn type_last_layer(
RetTypeOnly(t.clone())
}
BoolIf(x, y, z) => {
- if x.get_type()?.as_ref() != &builtin_to_value(Bool) {
+ if &*x.get_type()?.as_whnf() != &ValueF::from_builtin(Bool) {
return mkerr(InvalidPredicate(x.clone()));
}
@@ -428,7 +424,7 @@ fn type_last_layer(
return mkerr(IfBranchMismatch(y.clone(), z.clone()));
}
- RetTypeOnly(y.get_type()?.into_owned())
+ RetTypeOnly(y.get_type()?)
}
EmptyListLit(t) => {
match &*t.as_whnf() {
@@ -445,33 +441,27 @@ fn type_last_layer(
if x.get_type()? != y.get_type()? {
return mkerr(InvalidListElement(
i,
- x.get_type()?.into_owned(),
+ x.get_type()?,
y.clone(),
));
}
}
let t = x.get_type()?;
if t.get_type()?.as_const() != Some(Type) {
- return mkerr(InvalidListType(t.into_owned()));
+ return mkerr(InvalidListType(t));
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::from_builtin(dhall_syntax::Builtin::List)
- .app_value(t.into_owned()),
- Value::from_const(Type),
- ))
+ RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
}
SomeLit(x) => {
- let t = x.get_type()?.into_owned();
+ let t = x.get_type()?;
if t.get_type()?.as_const() != Some(Type) {
return mkerr(InvalidOptionalType(t));
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::from_builtin(dhall_syntax::Builtin::Optional)
- .app_value(t),
- Value::from_const(Type),
- ))
+ RetTypeOnly(
+ Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
+ )
}
RecordType(kts) => RetWhole(tck_record_type(
ctx,
@@ -483,8 +473,7 @@ fn type_last_layer(
)?),
RecordLit(kvs) => RetTypeOnly(tck_record_type(
ctx,
- kvs.iter()
- .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
+ kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
)?),
Field(r, x) => {
match &*r.get_type()?.as_whnf() {
@@ -545,7 +534,7 @@ fn type_last_layer(
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
- if x.get_type()?.as_ref() != &text_type {
+ if x.get_type()? != text_type {
return mkerr(InvalidTextInterpolation(x.clone()));
}
}
@@ -574,7 +563,9 @@ fn type_last_layer(
// Union the two records, prefering
// the values found in the RHS.
- let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
+ 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(
@@ -586,30 +577,12 @@ fn type_last_layer(
ctx,
ExprF::BinOp(
RecursiveRecordTypeMerge,
- l.get_type()?.into_owned(),
- r.get_type()?.into_owned(),
+ l.get_type()?,
+ r.get_type()?,
),
)?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
- use crate::phase::normalize::intersection_with_key;
-
- // Extract the Const of the LHS
- let k_l = match l.get_type()?.as_const() {
- Some(k) => k,
- _ => {
- return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
- }
- };
-
- // Extract the Const of the RHS
- let k_r = match r.get_type()?.as_const() {
- Some(k) => k,
- _ => {
- return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
- }
- };
-
- let k = max(k_l, k_r);
+ use crate::phase::normalize::merge_maps;
// Extract the LHS record type
let borrow_l = l.as_whnf();
@@ -630,9 +603,11 @@ fn type_last_layer(
};
// Ensure that the records combine without a type error
- let kts = intersection_with_key(
+ let kts = merge_maps(
+ kts_x,
+ kts_y,
// If the Label exists for both records, then we hit the recursive case.
- |_: &Label, l: &Value, r: &Value| {
+ |_, l: &Value, r: &Value| {
type_last_layer(
ctx,
ExprF::BinOp(
@@ -642,12 +617,9 @@ fn type_last_layer(
),
)
},
- kts_x,
- kts_y,
- );
- tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+ )?;
- RetTypeOnly(Value::from_const(k))
+ RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
}
BinOp(o @ ListAppend, l, r) => {
match &*l.get_type()?.as_whnf() {
@@ -659,7 +631,7 @@ fn type_last_layer(
return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
- RetTypeOnly(l.get_type()?.into_owned())
+ RetTypeOnly(l.get_type()?)
}
BinOp(Equivalence, l, r) => {
if l.get_type()?.get_type()?.as_const() != Some(Type) {
@@ -673,7 +645,10 @@ fn type_last_layer(
return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- RetTypeOnly(Value::from_const(Type))
+ RetWhole(Value::from_valuef_and_type(
+ ValueF::Equivalence(l.clone(), r.clone()),
+ Value::from_const(Type),
+ ))
}
BinOp(o, l, r) => {
let t = builtin_to_value(match o {
@@ -692,11 +667,11 @@ fn type_last_layer(
Equivalence => unreachable!(),
});
- if l.get_type()?.as_ref() != &t {
+ if l.get_type()? != t {
return mkerr(BinOpTypeMismatch(*o, l.clone()));
}
- if r.get_type()?.as_ref() != &t {
+ if r.get_type()? != t {
return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
@@ -800,7 +775,7 @@ fn type_last_layer(
RetTypeOnly(Value::from_valuef_and_type(
ValueF::RecordType(new_kts),
- record_type.get_type()?.into_owned(),
+ record_type.get_type()?,
))
}
};
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index be4805d..8f16a12 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -185,7 +185,7 @@ pub fn run_test(
}
TypeInference => {
let expr = expr.typecheck()?;
- let ty = expr.get_type()?.into_owned().normalize();
+ let ty = expr.get_type()?.normalize();
assert_eq_display!(ty, expected);
}
Normalization => {
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index cef11dd..ce3468f 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -124,8 +124,6 @@ pub use value::Value;
// A Dhall value.
pub mod value {
- use dhall::core::value::Value as DhallValue;
- use dhall::core::valuef::ValueF as DhallValueF;
use dhall::phase::{NormalizedSubExpr, Parsed, Typed};
use dhall_syntax::Builtin;
@@ -153,48 +151,32 @@ pub mod value {
pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
self.0.to_expr()
}
- pub(crate) fn to_value(&self) -> DhallValue {
- self.0.to_value()
- }
pub(crate) fn as_typed(&self) -> &Typed {
&self.0
}
- /// Assumes that the given value has type `Type`.
- pub(crate) fn make_simple_type(v: DhallValueF) -> Self {
- Value(Typed::from_valuef_and_type(v, Typed::const_type()))
- }
pub(crate) fn make_builtin_type(b: Builtin) -> Self {
- Self::make_simple_type(DhallValueF::from_builtin(b))
+ Value(Typed::make_builtin_type(b))
}
pub(crate) fn make_optional_type(t: Value) -> Self {
- Self::make_simple_type(
- DhallValueF::from_builtin(Builtin::Optional)
- .app_value(t.to_value()),
- )
+ Value(Typed::make_optional_type(t.0))
}
pub(crate) fn make_list_type(t: Value) -> Self {
- Self::make_simple_type(
- DhallValueF::from_builtin(Builtin::List)
- .app_value(t.to_value()),
- )
+ Value(Typed::make_list_type(t.0))
}
// Made public for the StaticType derive macro
#[doc(hidden)]
pub fn make_record_type(
kts: impl Iterator<Item = (String, Value)>,
) -> Self {
- Self::make_simple_type(DhallValueF::RecordType(
- kts.map(|(k, t)| (k.into(), t.to_value())).collect(),
- ))
+ Value(Typed::make_record_type(kts.map(|(k, t)| (k, t.0))))
}
#[doc(hidden)]
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Value>)>,
) -> Self {
- Self::make_simple_type(DhallValueF::UnionType(
- kts.map(|(k, t)| (k.into(), t.map(|t| t.to_value())))
- .collect(),
+ Value(Typed::make_union_type(
+ kts.map(|(k, t)| (k, t.map(|t| t.0))),
))
}
}
diff --git a/tests_buffer b/tests_buffer
index c6366ba..1ad880e 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -28,11 +28,18 @@ variables across import boundaries
TextLitNested1 "${""}${x}"
TextLitNested2 "${"${x}"}"
TextLitNested3 "${"${""}"}${x}"
+ regression/
+ NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True
typecheck:
something that involves destructuring a recordtype after merge
add some of the more complicated Prelude tests back, like List/enumerate
-failure on old-style optional literal
+success/
+ regression/
+ RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } }
+ somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type
+ somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases
+ somehow test types added to the Foo/build closures
failure/
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
@@ -41,5 +48,6 @@ failure/
merge {x=...,y=...} <x:T>.x
MergeBoolIsNotUnion merge x True
MergeOptionalIsNotUnion merge x (Some 1)
+ SortInLet let x = Sort in 1
equivalence: