summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/Cargo.toml1
-rw-r--r--dhall/build.rs5
-rw-r--r--dhall/src/core/context.rs162
-rw-r--r--dhall/src/core/mod.rs2
-rw-r--r--dhall/src/core/thunk.rs414
-rw-r--r--dhall/src/core/value.rs686
-rw-r--r--dhall/src/core/valuef.rs400
-rw-r--r--dhall/src/core/var.rs206
-rw-r--r--dhall/src/error/mod.rs54
-rw-r--r--dhall/src/phase/mod.rs75
-rw-r--r--dhall/src/phase/normalize.rs588
-rw-r--r--dhall/src/phase/typecheck.rs796
-rw-r--r--dhall/src/tests.rs28
13 files changed, 1478 insertions, 1939 deletions
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 0a257e4..16c1c78 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -9,6 +9,7 @@ build = "build.rs"
[dependencies]
bytecount = "0.5.1"
itertools = "0.8.0"
+take_mut = "0.2.2"
term-painter = "0.2.3"
serde = { version = "1.0" }
serde_cbor = "0.9.0"
diff --git a/dhall/build.rs b/dhall/build.rs
index 2305208..166b036 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -213,7 +213,10 @@ fn main() -> std::io::Result<()> {
"alpha_normalize",
"alpha-normalization/",
"AlphaNormalization",
- |_| false,
+ |path| {
+ // This test doesn't typecheck
+ path == "success/unit/FunctionNestedBindingXXFree"
+ },
)?;
make_test_module(
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 9230a2e..2bf39c5 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,64 +3,56 @@ use std::rc::Rc;
use dhall_syntax::{Label, V};
-use crate::core::thunk::Thunk;
use crate::core::value::Value;
+use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
-use crate::phase::{Type, Typed};
#[derive(Debug, Clone)]
-enum CtxItem<T> {
- Kept(AlphaVar, T),
- Replaced(Thunk, T),
+enum CtxItem {
+ Kept(AlphaVar, Value),
+ Replaced(Value),
}
#[derive(Debug, Clone)]
-struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
+pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>);
-#[derive(Debug, Clone)]
-pub(crate) struct NormalizationContext(Context<()>);
-
-#[derive(Debug, Clone)]
-pub(crate) struct TypecheckContext(Context<Type>);
-
-impl<T> Context<T> {
+impl TypecheckContext {
pub fn new() -> Self {
- Context(Rc::new(Vec::new()))
+ TypecheckContext(Rc::new(Vec::new()))
}
- pub fn insert_kept(&self, x: &Label, t: T) -> Self
- where
- T: Shift + Clone,
- {
+ pub fn insert_type(&self, x: &Label, t: Value) -> Self {
let mut vec = self.0.as_ref().clone();
vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
- Context(Rc::new(vec))
+ TypecheckContext(Rc::new(vec))
}
- pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self
- where
- T: Clone,
- {
+ pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> {
let mut vec = self.0.as_ref().clone();
- vec.push((x.clone(), CtxItem::Replaced(th, t)));
- Context(Rc::new(vec))
+ vec.push((x.clone(), CtxItem::Replaced(e)));
+ Ok(TypecheckContext(Rc::new(vec)))
}
- pub fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>>
- where
- T: Clone + Shift,
- {
+ pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
let mut var = var.clone();
let mut shift_map: HashMap<Label, _> = HashMap::new();
for (l, i) in self.0.iter().rev() {
match var.over_binder(l) {
- None => return Ok(i.under_multiple_binders(&shift_map)),
+ None => {
+ let i = i.under_multiple_binders(&shift_map);
+ return Some(match i {
+ CtxItem::Kept(newvar, t) => {
+ Value::from_valuef_and_type(ValueF::Var(newvar), t)
+ }
+ CtxItem::Replaced(v) => v,
+ });
+ }
Some(newvar) => var = newvar,
};
if let CtxItem::Kept(_, _) = i {
*shift_map.entry(l.clone()).or_insert(0) += 1;
}
}
- // Free variable
- Err(var)
+ // Unbound variable
+ None
}
/// Given a var that makes sense in the current context, map the given function in such a way
/// that the passed variable always makes sense in the context of the passed item.
@@ -69,11 +61,8 @@ impl<T> Context<T> {
fn do_with_var<E>(
&self,
var: &AlphaVar,
- mut f: impl FnMut(&AlphaVar, &CtxItem<T>) -> Result<CtxItem<T>, E>,
- ) -> Result<Self, E>
- where
- T: Clone,
- {
+ mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>,
+ ) -> Result<Self, E> {
let mut vec = Vec::new();
vec.reserve(self.0.len());
let mut var = var.clone();
@@ -91,16 +80,13 @@ impl<T> Context<T> {
vec.push((l.clone(), (*i).clone()));
}
vec.reverse();
- Ok(Context(Rc::new(vec)))
+ Ok(TypecheckContext(Rc::new(vec)))
}
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>
- where
- T: Clone + Shift,
- {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
if delta < 0 {
Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
} else {
- Some(Context(Rc::new(
+ Some(TypecheckContext(Rc::new(
self.0
.iter()
.map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?)))
@@ -108,117 +94,51 @@ impl<T> Context<T> {
)))
}
}
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self
- where
- T: Clone + Subst<Typed>,
- {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
.unwrap()
}
}
-impl NormalizationContext {
- pub fn new() -> Self {
- NormalizationContext(Context::new())
- }
- pub fn skip(&self, x: &Label) -> Self {
- NormalizationContext(self.0.insert_kept(x, ()))
- }
- pub fn lookup(&self, var: &V<Label>) -> Value {
- match self.0.lookup(var) {
- Ok(CtxItem::Replaced(t, ())) => t.to_value(),
- Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()),
- Err(var) => Value::Var(AlphaVar::from_var(var)),
- }
- }
-}
-
-impl TypecheckContext {
- pub fn new() -> Self {
- TypecheckContext(Context::new())
- }
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
- TypecheckContext(self.0.insert_kept(x, t))
- }
- pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> {
- Ok(TypecheckContext(self.0.insert_replaced(
- x,
- e.to_thunk(),
- e.get_type()?.into_owned(),
- )))
- }
- pub fn lookup(&self, var: &V<Label>) -> Option<Typed> {
- match self.0.lookup(var) {
- Ok(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type(
- Thunk::from_value(Value::Var(newvar.clone())),
- t.clone(),
- )),
- Ok(CtxItem::Replaced(th, t)) => {
- Some(Typed::from_thunk_and_type(th.clone(), t.clone()))
- }
- Err(_) => None,
- }
- }
-}
-
-impl<T: Shift> Shift for CtxItem<T> {
+impl Shift for CtxItem {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
CtxItem::Kept(v, t) => {
CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
}
- CtxItem::Replaced(e, t) => {
- CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?)
- }
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
})
}
}
-impl<T: Clone + Shift> Shift for Context<T> {
+impl Shift for TypecheckContext {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
self.shift(delta, var)
}
}
-impl Shift for NormalizationContext {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(NormalizationContext(self.0.shift(delta, var)?))
- }
-}
-
-impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for CtxItem {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match self {
- CtxItem::Replaced(e, t) => CtxItem::Replaced(
- e.subst_shift(var, val),
- t.subst_shift(var, val),
- ),
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
CtxItem::Kept(v, t) => match v.shift(-1, var) {
- None => {
- CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val))
- }
+ None => CtxItem::Replaced(val.clone()),
Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
},
}
}
}
-impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for TypecheckContext {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
self.subst_shift(var, val)
}
}
-impl Subst<Typed> for NormalizationContext {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- NormalizationContext(self.0.subst_shift(var, val))
- }
-}
-
+/// Don't count contexts when comparing stuff.
+/// This is dirty but needed.
impl PartialEq for TypecheckContext {
fn eq(&self, _: &Self) -> bool {
- // don't count contexts when comparing stuff
- // this is dirty but needed for now
true
}
}
diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs
index 0667df8..08213f7 100644
--- a/dhall/src/core/mod.rs
+++ b/dhall/src/core/mod.rs
@@ -1,4 +1,4 @@
pub mod context;
-pub mod thunk;
pub mod value;
+pub mod valuef;
pub mod var;
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
deleted file mode 100644
index 54a5442..0000000
--- a/dhall/src/core/thunk.rs
+++ /dev/null
@@ -1,414 +0,0 @@
-use std::borrow::Cow;
-use std::cell::{Ref, RefCell};
-use std::rc::Rc;
-
-use dhall_syntax::{Const, ExprF};
-
-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::typecheck::type_of_const;
-use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
-
-#[derive(Debug, Clone, Copy)]
-enum Marker {
- /// Weak Head Normal Form, i.e. subexpressions may not be normalized
- WHNF,
- /// Normal form, i.e. completely normalized
- NF,
-}
-use Marker::{NF, WHNF};
-
-#[derive(Debug)]
-enum ThunkInternal {
- /// Non-normalized value alongside a normalization context
- Unnormalized(NormalizationContext, InputSubExpr),
- /// 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<Thunk, Normalized>),
- /// Partially normalized value.
- /// Invariant: if the marker is `NF`, the value must be fully normalized
- Value(Marker, Value),
-}
-
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
-/// sharing computation automatically.
-/// Uses a RefCell to share computation.
-#[derive(Clone)]
-pub struct Thunk(Rc<RefCell<ThunkInternal>>);
-
-/// 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 TypedThunk {
- // Any value, along with (optionally) its type
- Untyped(Thunk),
- Typed(Thunk, Box<Type>),
- // 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 value
- // even though it doesn't itself have a type.
- Const(Const),
-}
-
-impl ThunkInternal {
- fn into_thunk(self) -> Thunk {
- Thunk(Rc::new(RefCell::new(self)))
- }
-
- fn normalize_whnf(&mut self) {
- match self {
- ThunkInternal::Unnormalized(ctx, e) => {
- *self = ThunkInternal::Value(
- WHNF,
- normalize_whnf(ctx.clone(), e.clone()),
- )
- }
- ThunkInternal::PartialExpr(e) => {
- *self =
- ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
- }
- // Already at least in WHNF
- ThunkInternal::Value(_, _) => {}
- }
- }
-
- fn normalize_nf(&mut self) {
- match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => {
- self.normalize_whnf();
- self.normalize_nf();
- }
- ThunkInternal::Value(m @ WHNF, v) => {
- v.normalize_mut();
- *m = NF;
- }
- // Already in NF
- ThunkInternal::Value(NF, _) => {}
- }
- }
-
- // Always use normalize_whnf before
- fn as_whnf(&self) -> &Value {
- match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => unreachable!(),
- ThunkInternal::Value(_, v) => v,
- }
- }
-
- // Always use normalize_nf before
- fn as_nf(&self) -> &Value {
- match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_)
- | ThunkInternal::Value(WHNF, _) => unreachable!(),
- ThunkInternal::Value(NF, v) => v,
- }
- }
-}
-
-impl Thunk {
- pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
- ThunkInternal::Unnormalized(ctx, e).into_thunk()
- }
-
- pub(crate) fn from_value(v: Value) -> Thunk {
- ThunkInternal::Value(WHNF, v).into_thunk()
- }
-
- pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
- ThunkInternal::PartialExpr(e).into_thunk()
- }
-
- // Normalizes contents to normal form; faster than `normalize_nf` if
- // no one else shares this thunk
- pub(crate) fn normalize_mut(&mut self) {
- match Rc::get_mut(&mut self.0) {
- // Mutate directly if sole owner
- Some(refcell) => RefCell::get_mut(refcell).normalize_nf(),
- // Otherwise mutate through the refcell
- None => self.0.borrow_mut().normalize_nf(),
- }
- }
-
- fn do_normalize_whnf(&self) {
- let borrow = self.0.borrow();
- match &*borrow {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => {
- drop(borrow);
- self.0.borrow_mut().normalize_whnf();
- }
- // Already at least in WHNF
- ThunkInternal::Value(_, _) => {}
- }
- }
-
- fn do_normalize_nf(&self) {
- let borrow = self.0.borrow();
- match &*borrow {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_)
- | ThunkInternal::Value(WHNF, _) => {
- drop(borrow);
- self.0.borrow_mut().normalize_nf();
- }
- // Already in NF
- ThunkInternal::Value(NF, _) => {}
- }
- }
-
- // WARNING: avoid normalizing any thunk while holding on to this ref
- // or you could run into BorrowMut panics
- pub(crate) fn normalize_nf(&self) -> Ref<Value> {
- self.do_normalize_nf();
- Ref::map(self.0.borrow(), ThunkInternal::as_nf)
- }
-
- // WARNING: avoid normalizing any thunk while holding on to this ref
- // or you could run into BorrowMut panics
- pub(crate) fn as_value(&self) -> Ref<Value> {
- self.do_normalize_whnf();
- Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
- }
-
- pub(crate) fn to_value(&self) -> Value {
- self.as_value().clone()
- }
-
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
- }
-
- pub(crate) fn app_val(&self, val: Value) -> Value {
- self.app_thunk(val.into_thunk())
- }
-
- pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
- apply_any(self.clone(), th)
- }
-}
-
-impl TypedThunk {
- pub(crate) fn from_value(v: Value) -> TypedThunk {
- TypedThunk::from_thunk(Thunk::from_value(v))
- }
-
- pub fn from_thunk(th: Thunk) -> TypedThunk {
- TypedThunk::from_thunk_untyped(th)
- }
-
- pub(crate) fn from_type(t: Type) -> TypedThunk {
- t.into_typethunk()
- }
-
- pub(crate) fn normalize_nf(&self) -> Value {
- match self {
- TypedThunk::Const(c) => Value::Const(*c),
- TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => {
- thunk.normalize_nf().clone()
- }
- }
- }
-
- pub(crate) fn to_typed(&self) -> Typed {
- self.clone().into_typed()
- }
-
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
- }
-
- pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- TypedThunk::Typed(th, Box::new(t))
- }
- pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- TypedThunk::Untyped(th)
- }
- pub(crate) fn from_const(c: Const) -> Self {
- TypedThunk::Const(c)
- }
- pub(crate) fn from_value_untyped(v: Value) -> Self {
- TypedThunk::from_thunk_untyped(Thunk::from_value(v))
- }
-
- // TODO: Avoid cloning if possible
- pub(crate) fn to_value(&self) -> Value {
- match self {
- TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(),
- TypedThunk::Const(c) => Value::Const(*c),
- }
- }
- pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
- self.to_value().normalize_to_expr()
- }
- pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
- self.to_value().normalize_to_expr_maybe_alpha(true)
- }
- pub(crate) fn to_thunk(&self) -> Thunk {
- match self {
- TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(),
- TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)),
- }
- }
- pub(crate) fn to_type(&self) -> Type {
- self.clone().into_typed().into_type()
- }
- pub(crate) fn into_typed(self) -> Typed {
- Typed::from_typethunk(self)
- }
- pub(crate) fn as_const(&self) -> Option<Const> {
- // TODO: avoid clone
- match &self.to_value() {
- Value::Const(c) => Some(*c),
- _ => None,
- }
- }
-
- pub(crate) fn normalize_mut(&mut self) {
- match self {
- TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => {
- th.normalize_mut()
- }
- TypedThunk::Const(_) => {}
- }
- }
-
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
- match self {
- TypedThunk::Untyped(_) => Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- )),
- TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)),
- TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)),
- }
- }
-}
-
-impl Shift for Thunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(self.0.borrow().shift(delta, var)?.into_thunk())
- }
-}
-
-impl Shift for ThunkInternal {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- ThunkInternal::Unnormalized(ctx, e) => {
- ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone())
- }
- ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
- e.traverse_ref_with_special_handling_of_binders(
- |v| Ok(v.shift(delta, var)?),
- |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- )?,
- ),
- ThunkInternal::Value(m, v) => {
- ThunkInternal::Value(*m, v.shift(delta, var)?)
- }
- })
- }
-}
-
-impl Shift for TypedThunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- 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)?),
- ),
- TypedThunk::Const(c) => TypedThunk::Const(*c),
- })
- }
-}
-
-impl Subst<Typed> for Thunk {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- self.0.borrow().subst_shift(var, val).into_thunk()
- }
-}
-
-impl Subst<Typed> for ThunkInternal {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
- ctx.subst_shift(var, val),
- e.clone(),
- ),
- ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
- e.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| {
- v.subst_shift(
- &var.under_binder(x),
- &val.under_binder(x),
- )
- },
- ),
- ),
- ThunkInternal::Value(_, v) => {
- // The resulting value may not stay in normal form after substitution
- ThunkInternal::Value(WHNF, v.subst_shift(var, val))
- }
- }
- }
-}
-
-impl Subst<Typed> for TypedThunk {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- TypedThunk::Untyped(th) => {
- TypedThunk::Untyped(th.subst_shift(var, val))
- }
- TypedThunk::Typed(th, t) => TypedThunk::Typed(
- th.subst_shift(var, val),
- Box::new(t.subst_shift(var, val)),
- ),
- TypedThunk::Const(c) => TypedThunk::Const(*c),
- }
- }
-}
-
-impl std::cmp::PartialEq for Thunk {
- fn eq(&self, other: &Self) -> bool {
- *self.as_value() == *other.as_value()
- }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for TypedThunk {
- fn eq(&self, other: &Self) -> bool {
- self.to_value() == other.to_value()
- }
-}
-impl std::cmp::Eq for TypedThunk {}
-
-impl std::fmt::Debug for Thunk {
- fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let b: &ThunkInternal = &self.0.borrow();
- match b {
- ThunkInternal::Value(m, v) => {
- f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish()
- }
- ThunkInternal::PartialExpr(e) => {
- f.debug_tuple("Thunk@PartialExpr").field(e).finish()
- }
- ThunkInternal::Unnormalized(ctx, e) => f
- .debug_tuple("Thunk@Unnormalized")
- .field(ctx)
- .field(e)
- .finish(),
- }
- }
-}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 61a8eea..0af7c8c 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,490 +1,272 @@
-use std::collections::HashMap;
+use std::borrow::Cow;
+use std::cell::{Ref, RefCell, RefMut};
+use std::rc::Rc;
-use dhall_syntax::{
- rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural,
-};
+use dhall_syntax::Const;
-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,
-};
-use crate::phase::{Normalized, Typed};
+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::type_of_const;
+use crate::phase::{NormalizedSubExpr, 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
-/// final Normal Form (NF).
-/// This WHNF must be preserved by operations on `Value`s. In particular, `subst_shift` could break
-/// the invariants so need to be careful to reevaluate as needed.
-/// Subexpressions are Thunks, which are partially evaluated expressions that are normalized
-/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the
-/// Value is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
-/// if we have the first constructor of the NF at all levels, we actually have the NF.
-/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence
-/// (normalization). Equality will normalize only as needed.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Value {
- /// Closures
- Lam(AlphaLabel, TypedThunk, Thunk),
- Pi(AlphaLabel, TypedThunk, TypedThunk),
- // Invariant: the evaluation must not be able to progress further.
- AppliedBuiltin(Builtin, Vec<Thunk>),
+#[derive(Debug, Clone, Copy)]
+enum Form {
+ /// No constraints; expression may not be normalized at all.
+ Unevaled,
+ /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
+ /// not be normalized. This means that the first constructor of the contained ValueF is the first
+ /// constructor of the final Normal Form (NF).
+ WHNF,
+ /// Normal Form, i.e. completely normalized.
+ /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the
+ /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
+ /// if we have the first constructor of the NF at all levels, we actually have the NF.
+ NF,
+}
+use Form::{Unevaled, NF, WHNF};
- Var(AlphaVar),
- Const(Const),
- BoolLit(bool),
- NaturalLit(Natural),
- IntegerLit(Integer),
- DoubleLit(NaiveDouble),
- EmptyOptionalLit(TypedThunk),
- NEOptionalLit(Thunk),
- // EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(TypedThunk),
- NEListLit(Vec<Thunk>),
- RecordLit(HashMap<Label, Thunk>),
- RecordType(HashMap<Label, TypedThunk>),
- UnionType(HashMap<Label, Option<TypedThunk>>),
- UnionConstructor(Label, HashMap<Label, Option<TypedThunk>>),
- UnionLit(Label, Thunk, HashMap<Label, Option<TypedThunk>>),
- // Invariant: this must not contain interpolations that are themselves TextLits, and
- // contiguous text values must be merged.
- TextLit(Vec<InterpolatedTextContents<Thunk>>),
- Equivalence(TypedThunk, TypedThunk),
- // Invariant: this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, Normalized>),
+#[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
+struct ValueInternal {
+ form: Form,
+ value: ValueF,
+ ty: Option<Value>,
}
-impl Value {
- pub(crate) fn into_thunk(self) -> Thunk {
- Thunk::from_value(self)
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
+/// sharing computation automatically. Uses a RefCell to share computation.
+/// Can optionally store a type from typechecking to preserve type information.
+#[derive(Clone)]
+pub struct Value(Rc<RefCell<ValueInternal>>);
+
+impl ValueInternal {
+ fn into_value(self) -> Value {
+ Value(Rc::new(RefCell::new(self)))
+ }
+ fn as_valuef(&self) -> &ValueF {
+ &self.value
}
- /// Convert the value to a fully normalized syntactic expression
- pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
- self.normalize_to_expr_maybe_alpha(false)
- }
- /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
- /// if alpha is `true`
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
- match self {
- Value::Lam(x, t, e) => rc(ExprF::Lam(
- x.to_label_maybe_alpha(alpha),
- t.normalize_to_expr_maybe_alpha(alpha),
- e.normalize_to_expr_maybe_alpha(alpha),
- )),
- Value::AppliedBuiltin(b, args) => {
- let mut e = rc(ExprF::Builtin(*b));
- for v in args {
- e = rc(ExprF::App(
- e,
- v.normalize_to_expr_maybe_alpha(alpha),
- ));
- }
- e
- }
- Value::Pi(x, t, e) => rc(ExprF::Pi(
- x.to_label_maybe_alpha(alpha),
- t.normalize_to_expr_maybe_alpha(alpha),
- e.normalize_to_expr_maybe_alpha(alpha),
- )),
- Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
- Value::Const(c) => rc(ExprF::Const(*c)),
- Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
- Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
- Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
- Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
- Value::EmptyOptionalLit(n) => rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::OptionalNone)),
- n.normalize_to_expr_maybe_alpha(alpha),
- )),
- Value::NEOptionalLit(n) => {
- rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
- }
- Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::List)),
- n.normalize_to_expr_maybe_alpha(alpha),
- )))),
- Value::NEListLit(elts) => rc(ExprF::NEListLit(
- elts.iter()
- .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
- .collect(),
- )),
- Value::RecordLit(kvs) => rc(ExprF::RecordLit(
- kvs.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
- })
- .collect(),
- )),
- Value::RecordType(kts) => rc(ExprF::RecordType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
- })
- .collect(),
- )),
- Value::UnionType(kts) => rc(ExprF::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (
- k.clone(),
- v.as_ref().map(|v| {
- v.normalize_to_expr_maybe_alpha(alpha)
- }),
- )
- })
- .collect(),
- )),
- Value::UnionConstructor(l, kts) => {
- let kts = kts
- .iter()
- .map(|(k, v)| {
- (
- k.clone(),
- v.as_ref().map(|v| {
- v.normalize_to_expr_maybe_alpha(alpha)
- }),
- )
- })
- .collect();
- rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
+ 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,
+ },
+ // Already in WHNF
+ WHNF | NF => vint,
+ })
+ }
+ fn normalize_nf(&mut self) {
+ match self.form {
+ Unevaled => {
+ self.normalize_whnf();
+ self.normalize_nf();
}
- Value::UnionLit(l, v, kts) => rc(ExprF::App(
- Value::UnionConstructor(l.clone(), kts.clone())
- .normalize_to_expr_maybe_alpha(alpha),
- v.normalize_to_expr_maybe_alpha(alpha),
- )),
- Value::TextLit(elts) => {
- use InterpolatedTextContents::{Expr, Text};
- rc(ExprF::TextLit(
- elts.iter()
- .map(|contents| match contents {
- Expr(e) => {
- Expr(e.normalize_to_expr_maybe_alpha(alpha))
- }
- Text(s) => Text(s.clone()),
- })
- .collect(),
- ))
+ WHNF => {
+ self.value.normalize_mut();
+ self.form = NF;
}
- Value::Equivalence(x, y) => rc(ExprF::BinOp(
- dhall_syntax::BinOp::Equivalence,
- x.normalize_to_expr_maybe_alpha(alpha),
- y.normalize_to_expr_maybe_alpha(alpha),
+ // Already in NF
+ NF => {}
+ }
+ }
+
+ fn get_type(&self) -> Result<&Value, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t),
+ None => Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Untyped,
)),
- Value::PartialExpr(e) => {
- rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
- }
}
}
+}
- pub(crate) fn normalize_mut(&mut self) {
- match self {
- Value::Var(_)
- | Value::Const(_)
- | Value::BoolLit(_)
- | Value::NaturalLit(_)
- | Value::IntegerLit(_)
- | Value::DoubleLit(_) => {}
+impl Value {
+ pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
+ ValueInternal {
+ form: Unevaled,
+ value: v,
+ ty: None,
+ }
+ .into_value()
+ }
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+ ValueInternal {
+ form: Unevaled,
+ value: v,
+ ty: Some(t),
+ }
+ .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_const(c: Const) -> Self {
+ match type_of_const(c) {
+ Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t),
+ Err(_) => Value::from_valuef_untyped(ValueF::Const(c)),
+ }
+ }
+ pub fn const_type() -> Self {
+ Value::from_const(Const::Type)
+ }
- Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => {
- tth.normalize_mut();
- }
+ pub(crate) fn as_const(&self) -> Option<Const> {
+ match &*self.as_whnf() {
+ ValueF::Const(c) => Some(*c),
+ _ => None,
+ }
+ }
- Value::NEOptionalLit(th) => {
- th.normalize_mut();
- }
- Value::Lam(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
- Value::Pi(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
- Value::AppliedBuiltin(_, args) => {
- for x in args.iter_mut() {
- x.normalize_mut();
- }
- }
- Value::NEListLit(elts) => {
- for x in elts.iter_mut() {
- x.normalize_mut();
- }
- }
- Value::RecordLit(kvs) => {
- for x in kvs.values_mut() {
- x.normalize_mut();
- }
- }
- Value::RecordType(kvs) => {
- for x in kvs.values_mut() {
- x.normalize_mut();
- }
- }
- Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
- for x in kts.values_mut().flat_map(|opt| opt) {
- x.normalize_mut();
- }
- }
- Value::UnionLit(_, v, kts) => {
- v.normalize_mut();
- for x in kts.values_mut().flat_map(|opt| opt) {
- x.normalize_mut();
- }
- }
- Value::TextLit(elts) => {
- for x in elts.iter_mut() {
- use InterpolatedTextContents::{Expr, Text};
- match x {
- Expr(n) => n.normalize_mut(),
- Text(_) => {}
- }
- }
- }
- Value::Equivalence(x, y) => {
- x.normalize_mut();
- y.normalize_mut();
+ fn as_internal(&self) -> Ref<ValueInternal> {
+ self.0.borrow()
+ }
+ fn as_internal_mut(&self) -> RefMut<ValueInternal> {
+ self.0.borrow_mut()
+ }
+ /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an
+ /// unevaled PartialExpr. You probably want to use `as_whnf`.
+ fn as_valuef(&self) -> Ref<ValueF> {
+ Ref::map(self.as_internal(), ValueInternal::as_valuef)
+ }
+ /// This is what you want if you want to pattern-match on the value.
+ /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
+ /// panics.
+ pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
+ self.normalize_whnf();
+ self.as_valuef()
+ }
+ /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
+ /// panics.
+ pub(crate) fn as_nf(&self) -> Ref<ValueF> {
+ self.normalize_nf();
+ self.as_valuef()
+ }
+
+ // TODO: rename `normalize_to_expr`
+ pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
+ self.as_whnf().normalize_to_expr()
+ }
+ // TODO: rename `normalize_to_expr_maybe_alpha`
+ 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 {
+ self.as_whnf().clone()
+ }
+ pub(crate) fn into_typed(self) -> Typed {
+ Typed::from_value(self)
+ }
+
+ /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
+ fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
+ match Rc::get_mut(&mut self.0) {
+ // Mutate directly if sole owner
+ Some(refcell) => f(RefCell::get_mut(refcell)),
+ // Otherwise mutate through the refcell
+ None => f(&mut self.as_internal_mut()),
+ }
+ }
+ /// Normalizes contents to normal form; faster than `normalize_nf` if
+ /// no one else shares this.
+ pub(crate) fn normalize_mut(&mut self) {
+ self.mutate_internal(|vint| vint.normalize_nf())
+ }
+
+ pub(crate) fn normalize_whnf(&self) {
+ let borrow = self.as_internal();
+ match borrow.form {
+ Unevaled => {
+ drop(borrow);
+ self.as_internal_mut().normalize_whnf();
}
- Value::PartialExpr(e) => {
- // TODO: need map_mut
- e.map_ref(|v| {
- v.normalize_nf();
- });
+ // Already at least in WHNF
+ WHNF | NF => {}
+ }
+ }
+ pub(crate) fn normalize_nf(&self) {
+ let borrow = self.as_internal();
+ match borrow.form {
+ Unevaled | WHNF => {
+ drop(borrow);
+ self.as_internal_mut().normalize_nf();
}
+ // Already in NF
+ NF => {}
}
}
- /// Apply to a value
- pub(crate) fn app(self, val: Value) -> Value {
- self.app_val(val)
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
+ self.as_nf().normalize_to_expr_maybe_alpha(alpha)
}
- /// Apply to a value
- pub(crate) fn app_val(self, val: Value) -> Value {
- self.app_thunk(val.into_thunk())
+ pub(crate) fn app_value(&self, th: Value) -> ValueF {
+ apply_any(self.clone(), th)
}
- /// Apply to a thunk
- pub fn app_thunk(self, th: Thunk) -> Value {
- Thunk::from_value(self).app_thunk(th)
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
+ Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
}
+}
- pub fn from_builtin(b: Builtin) -> Value {
- Value::AppliedBuiltin(b, vec![])
+impl Shift for Value {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Value(self.0.shift(delta, var)?))
}
}
-impl Shift for Value {
+impl Shift for ValueInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- Value::Lam(x, t, e) => Value::Lam(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
- Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
- *b,
- args.iter()
- .map(|v| Ok(v.shift(delta, var)?))
- .collect::<Result<_, _>>()?,
- ),
- Value::Pi(x, t, e) => Value::Pi(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
- Value::Var(v) => Value::Var(v.shift(delta, var)?),
- Value::Const(c) => Value::Const(*c),
- Value::BoolLit(b) => Value::BoolLit(*b),
- Value::NaturalLit(n) => Value::NaturalLit(*n),
- Value::IntegerLit(n) => Value::IntegerLit(*n),
- Value::DoubleLit(n) => Value::DoubleLit(*n),
- Value::EmptyOptionalLit(tth) => {
- Value::EmptyOptionalLit(tth.shift(delta, var)?)
- }
- Value::NEOptionalLit(th) => {
- Value::NEOptionalLit(th.shift(delta, var)?)
- }
- Value::EmptyListLit(tth) => {
- Value::EmptyListLit(tth.shift(delta, var)?)
- }
- Value::NEListLit(elts) => Value::NEListLit(
- elts.iter()
- .map(|v| Ok(v.shift(delta, var)?))
- .collect::<Result<_, _>>()?,
- ),
- Value::RecordLit(kvs) => Value::RecordLit(
- kvs.iter()
- .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
- .collect::<Result<_, _>>()?,
- ),
- Value::RecordType(kvs) => Value::RecordType(
- kvs.iter()
- .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
- .collect::<Result<_, _>>()?,
- ),
- Value::UnionType(kts) => Value::UnionType(
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
- Value::UnionConstructor(x, kts) => Value::UnionConstructor(
- x.clone(),
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
- Value::UnionLit(x, v, kts) => Value::UnionLit(
- x.clone(),
- v.shift(delta, var)?,
- kts.iter()
- .map(|(k, v)| {
- Ok((
- k.clone(),
- v.as_ref()
- .map(|v| Ok(v.shift(delta, var)?))
- .transpose()?,
- ))
- })
- .collect::<Result<_, _>>()?,
- ),
- Value::TextLit(elts) => Value::TextLit(
- elts.iter()
- .map(|contents| {
- use InterpolatedTextContents::{Expr, Text};
- Ok(match contents {
- Expr(th) => Expr(th.shift(delta, var)?),
- Text(s) => Text(s.clone()),
- })
- })
- .collect::<Result<_, _>>()?,
- ),
- Value::Equivalence(x, y) => {
- Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
- }
- Value::PartialExpr(e) => Value::PartialExpr(
- e.traverse_ref_with_special_handling_of_binders(
- |v| Ok(v.shift(delta, var)?),
- |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- )?,
- ),
+ Some(ValueInternal {
+ form: self.form,
+ value: self.value.shift(delta, var)?,
+ ty: self.ty.shift(delta, var)?,
})
}
}
-impl Subst<Typed> for Value {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- // Retry normalizing since substituting may allow progress
- Value::AppliedBuiltin(b, args) => apply_builtin(
- *b,
- args.iter().map(|v| v.subst_shift(var, val)).collect(),
- ),
- // Retry normalizing since substituting may allow progress
- Value::PartialExpr(e) => {
- normalize_one_layer(e.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| {
- v.subst_shift(
- &var.under_binder(x),
- &val.under_binder(x),
- )
- },
- ))
- }
- // Retry normalizing since substituting may allow progress
- Value::TextLit(elts) => {
- Value::TextLit(squash_textlit(elts.iter().map(|contents| {
- use InterpolatedTextContents::{Expr, Text};
- match contents {
- Expr(th) => Expr(th.subst_shift(var, val)),
- Text(s) => Text(s.clone()),
- }
- })))
- }
- Value::Lam(x, t, e) => Value::Lam(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
- Value::Pi(x, t, e) => Value::Pi(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
- Value::Var(v) if v == var => val.to_value(),
- Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()),
- Value::Const(c) => Value::Const(*c),
- Value::BoolLit(b) => Value::BoolLit(*b),
- Value::NaturalLit(n) => Value::NaturalLit(*n),
- Value::IntegerLit(n) => Value::IntegerLit(*n),
- Value::DoubleLit(n) => Value::DoubleLit(*n),
- Value::EmptyOptionalLit(tth) => {
- Value::EmptyOptionalLit(tth.subst_shift(var, val))
- }
- Value::NEOptionalLit(th) => {
- Value::NEOptionalLit(th.subst_shift(var, val))
- }
- Value::EmptyListLit(tth) => {
- Value::EmptyListLit(tth.subst_shift(var, val))
- }
- Value::NEListLit(elts) => Value::NEListLit(
- elts.iter().map(|v| v.subst_shift(var, val)).collect(),
- ),
- Value::RecordLit(kvs) => Value::RecordLit(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
- .collect(),
- ),
- Value::RecordType(kvs) => Value::RecordType(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
- .collect(),
- ),
- Value::UnionType(kts) => Value::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
- ),
- Value::UnionConstructor(x, kts) => Value::UnionConstructor(
- x.clone(),
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
- ),
- Value::UnionLit(x, v, kts) => Value::UnionLit(
- x.clone(),
- v.subst_shift(var, val),
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
- })
- .collect(),
- ),
- Value::Equivalence(x, y) => Value::Equivalence(
- x.subst_shift(var, val),
- y.subst_shift(var, val),
- ),
+impl Subst<Value> for Value {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ Value(self.0.subst_shift(var, val))
+ }
+}
+
+impl Subst<Value> for ValueInternal {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ ValueInternal {
+ // The resulting value may not stay in wnhf after substitution
+ form: Unevaled,
+ value: self.value.subst_shift(var, val),
+ ty: self.ty.subst_shift(var, val),
}
}
}
+
+// TODO: use Rc comparison to shortcut on identical pointers
+impl std::cmp::PartialEq for Value {
+ fn eq(&self, other: &Self) -> bool {
+ *self.as_whnf() == *other.as_whnf()
+ }
+}
+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()
+ }
+}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
new file mode 100644
index 0000000..0c3058d
--- /dev/null
+++ b/dhall/src/core/valuef.rs
@@ -0,0 +1,400 @@
+use std::collections::HashMap;
+
+use dhall_syntax::{
+ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+ NaiveDouble, Natural,
+};
+
+use crate::core::value::Value;
+use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::phase::normalize::OutputSubExpr;
+use crate::phase::Normalized;
+
+/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
+/// normalized on-demand.
+/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
+/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
+/// recursively normalize as needed.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum ValueF {
+ /// Closures
+ Lam(AlphaLabel, Value, Value),
+ Pi(AlphaLabel, Value, Value),
+ // Invariant: the evaluation must not be able to progress further.
+ AppliedBuiltin(Builtin, Vec<Value>),
+
+ Var(AlphaVar),
+ Const(Const),
+ BoolLit(bool),
+ NaturalLit(Natural),
+ IntegerLit(Integer),
+ DoubleLit(NaiveDouble),
+ EmptyOptionalLit(Value),
+ NEOptionalLit(Value),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ EmptyListLit(Value),
+ NEListLit(Vec<Value>),
+ RecordLit(HashMap<Label, Value>),
+ RecordType(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
+ // 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.
+ 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 {
+ self.normalize_to_expr_maybe_alpha(false)
+ }
+ /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
+ /// if alpha is `true`
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
+ match self {
+ ValueF::Lam(x, t, e) => rc(ExprF::Lam(
+ x.to_label_maybe_alpha(alpha),
+ t.normalize_to_expr_maybe_alpha(alpha),
+ e.normalize_to_expr_maybe_alpha(alpha),
+ )),
+ ValueF::AppliedBuiltin(b, args) => {
+ let mut e = rc(ExprF::Builtin(*b));
+ for v in args {
+ e = rc(ExprF::App(
+ e,
+ v.normalize_to_expr_maybe_alpha(alpha),
+ ));
+ }
+ e
+ }
+ ValueF::Pi(x, t, e) => rc(ExprF::Pi(
+ x.to_label_maybe_alpha(alpha),
+ t.normalize_to_expr_maybe_alpha(alpha),
+ e.normalize_to_expr_maybe_alpha(alpha),
+ )),
+ ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
+ ValueF::Const(c) => rc(ExprF::Const(*c)),
+ ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)),
+ ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
+ ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
+ ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
+ ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
+ rc(ExprF::Builtin(Builtin::OptionalNone)),
+ n.normalize_to_expr_maybe_alpha(alpha),
+ )),
+ ValueF::NEOptionalLit(n) => {
+ rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
+ }
+ ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+ rc(ExprF::Builtin(Builtin::List)),
+ n.normalize_to_expr_maybe_alpha(alpha),
+ )))),
+ ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
+ elts.iter()
+ .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
+ .collect(),
+ )),
+ ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+ })
+ .collect(),
+ )),
+ ValueF::RecordType(kts) => rc(ExprF::RecordType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+ })
+ .collect(),
+ )),
+ ValueF::UnionType(kts) => rc(ExprF::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (
+ k.clone(),
+ v.as_ref().map(|v| {
+ v.normalize_to_expr_maybe_alpha(alpha)
+ }),
+ )
+ })
+ .collect(),
+ )),
+ ValueF::UnionConstructor(l, kts) => {
+ let kts = kts
+ .iter()
+ .map(|(k, v)| {
+ (
+ k.clone(),
+ v.as_ref().map(|v| {
+ v.normalize_to_expr_maybe_alpha(alpha)
+ }),
+ )
+ })
+ .collect();
+ rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
+ }
+ ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
+ ValueF::UnionConstructor(l.clone(), kts.clone())
+ .normalize_to_expr_maybe_alpha(alpha),
+ v.normalize_to_expr_maybe_alpha(alpha),
+ )),
+ ValueF::TextLit(elts) => {
+ use InterpolatedTextContents::{Expr, Text};
+ rc(ExprF::TextLit(
+ elts.iter()
+ .map(|contents| match contents {
+ Expr(e) => {
+ Expr(e.normalize_to_expr_maybe_alpha(alpha))
+ }
+ Text(s) => Text(s.clone()),
+ })
+ .collect(),
+ ))
+ }
+ ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
+ dhall_syntax::BinOp::Equivalence,
+ x.normalize_to_expr_maybe_alpha(alpha),
+ y.normalize_to_expr_maybe_alpha(alpha),
+ )),
+ ValueF::PartialExpr(e) => {
+ rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
+ }
+ }
+ }
+
+ pub(crate) fn normalize_mut(&mut self) {
+ match self {
+ ValueF::Var(_)
+ | ValueF::Const(_)
+ | ValueF::BoolLit(_)
+ | ValueF::NaturalLit(_)
+ | ValueF::IntegerLit(_)
+ | ValueF::DoubleLit(_) => {}
+
+ ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
+ tth.normalize_mut();
+ }
+
+ ValueF::NEOptionalLit(th) => {
+ th.normalize_mut();
+ }
+ ValueF::Lam(_, t, e) => {
+ t.normalize_mut();
+ e.normalize_mut();
+ }
+ ValueF::Pi(_, t, e) => {
+ t.normalize_mut();
+ e.normalize_mut();
+ }
+ ValueF::AppliedBuiltin(_, args) => {
+ for x in args.iter_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueF::NEListLit(elts) => {
+ for x in elts.iter_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueF::RecordLit(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueF::RecordType(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueF::UnionLit(_, v, kts) => {
+ v.normalize_mut();
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueF::TextLit(elts) => {
+ for x in elts.iter_mut() {
+ use InterpolatedTextContents::{Expr, Text};
+ match x {
+ Expr(n) => n.normalize_mut(),
+ Text(_) => {}
+ }
+ }
+ }
+ ValueF::Equivalence(x, y) => {
+ x.normalize_mut();
+ y.normalize_mut();
+ }
+ ValueF::PartialExpr(e) => {
+ // TODO: need map_mut
+ e.map_ref(|v| {
+ v.normalize_nf();
+ });
+ }
+ }
+ }
+
+ /// 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 {
+ ValueF::AppliedBuiltin(b, vec![])
+ }
+}
+
+impl Shift for ValueF {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ ValueF::Lam(x, t, e) => ValueF::Lam(
+ x.clone(),
+ t.shift(delta, var)?,
+ e.shift(delta, &var.under_binder(x))?,
+ ),
+ ValueF::AppliedBuiltin(b, args) => {
+ ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
+ }
+ ValueF::Pi(x, t, e) => ValueF::Pi(
+ x.clone(),
+ t.shift(delta, var)?,
+ e.shift(delta, &var.under_binder(x))?,
+ ),
+ ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?),
+ ValueF::Const(c) => ValueF::Const(*c),
+ ValueF::BoolLit(b) => ValueF::BoolLit(*b),
+ ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
+ ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
+ ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
+ ValueF::EmptyOptionalLit(tth) => {
+ ValueF::EmptyOptionalLit(tth.shift(delta, var)?)
+ }
+ ValueF::NEOptionalLit(th) => {
+ ValueF::NEOptionalLit(th.shift(delta, var)?)
+ }
+ ValueF::EmptyListLit(tth) => {
+ ValueF::EmptyListLit(tth.shift(delta, var)?)
+ }
+ ValueF::NEListLit(elts) => {
+ ValueF::NEListLit(elts.shift(delta, var)?)
+ }
+ ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
+ ValueF::RecordType(kvs) => {
+ ValueF::RecordType(kvs.shift(delta, var)?)
+ }
+ ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
+ ValueF::UnionConstructor(x, kts) => {
+ ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+ }
+ ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
+ x.clone(),
+ v.shift(delta, var)?,
+ kts.shift(delta, var)?,
+ ),
+ ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
+ ValueF::Equivalence(x, y) => {
+ ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+ }
+ ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
+ })
+ }
+}
+
+impl Subst<Value> for ValueF {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ match self {
+ ValueF::AppliedBuiltin(b, args) => {
+ ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
+ }
+ ValueF::PartialExpr(e) => {
+ ValueF::PartialExpr(e.subst_shift(var, val))
+ }
+ ValueF::TextLit(elts) => {
+ ValueF::TextLit(elts.subst_shift(var, val))
+ }
+ ValueF::Lam(x, t, e) => ValueF::Lam(
+ x.clone(),
+ t.subst_shift(var, val),
+ e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ ),
+ ValueF::Pi(x, t, e) => ValueF::Pi(
+ x.clone(),
+ 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) => ValueF::Var(v.shift(-1, var).unwrap()),
+ ValueF::Const(c) => ValueF::Const(*c),
+ ValueF::BoolLit(b) => ValueF::BoolLit(*b),
+ ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
+ ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
+ ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
+ ValueF::EmptyOptionalLit(tth) => {
+ ValueF::EmptyOptionalLit(tth.subst_shift(var, val))
+ }
+ ValueF::NEOptionalLit(th) => {
+ ValueF::NEOptionalLit(th.subst_shift(var, val))
+ }
+ ValueF::EmptyListLit(tth) => {
+ ValueF::EmptyListLit(tth.subst_shift(var, val))
+ }
+ ValueF::NEListLit(elts) => {
+ ValueF::NEListLit(elts.subst_shift(var, val))
+ }
+ ValueF::RecordLit(kvs) => {
+ ValueF::RecordLit(kvs.subst_shift(var, val))
+ }
+ ValueF::RecordType(kvs) => {
+ ValueF::RecordType(kvs.subst_shift(var, val))
+ }
+ ValueF::UnionType(kts) => {
+ ValueF::UnionType(kts.subst_shift(var, val))
+ }
+ ValueF::UnionConstructor(x, kts) => {
+ ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
+ }
+ ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
+ x.clone(),
+ v.subst_shift(var, val),
+ kts.subst_shift(var, val),
+ ),
+ ValueF::Equivalence(x, y) => ValueF::Equivalence(
+ x.subst_shift(var, val),
+ y.subst_shift(var, val),
+ ),
+ }
+ }
+}
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 4ef1b93..ce4d137 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -2,17 +2,17 @@ use std::collections::HashMap;
use dhall_syntax::{Label, V};
-/// Stores a pair of variables: a normal one and if relevant one
+/// Stores a pair of variables: a normal one and one
/// that corresponds to the alpha-normalized version of the first one.
-/// Equality is up to alpha-equivalence.
+/// Equality is up to alpha-equivalence (compares on the second one only).
#[derive(Clone, Eq)]
pub struct AlphaVar {
normal: V<Label>,
- alpha: Option<V<()>>,
+ alpha: V<()>,
}
// Exactly like a Label, but equality returns always true.
-// This is so that Value equality is exactly alpha-equivalence.
+// This is so that ValueF equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct AlphaLabel(Label);
@@ -50,27 +50,22 @@ pub(crate) trait Shift: Sized {
}
}
-pub(crate) trait Subst<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self;
+pub(crate) trait Subst<S> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self;
}
impl AlphaVar {
pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
- match (alpha, &self.alpha) {
- (true, Some(x)) => V("_".into(), x.1),
- _ => self.normal.clone(),
- }
- }
- pub(crate) fn from_var(normal: V<Label>) -> Self {
- AlphaVar {
- normal,
- alpha: None,
+ if alpha {
+ V("_".into(), self.alpha.1)
+ } else {
+ self.normal.clone()
}
}
pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
AlphaVar {
normal,
- alpha: Some(V((), alpha)),
+ alpha: V((), alpha),
}
}
}
@@ -92,31 +87,15 @@ impl Shift for AlphaVar {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(AlphaVar {
normal: self.normal.shift(delta, &var.normal)?,
- alpha: match (&self.alpha, &var.alpha) {
- (Some(x), Some(v)) => Some(x.shift(delta, v)?),
- _ => None,
- },
+ alpha: self.alpha.shift(delta, &var.alpha)?,
})
}
}
-impl Shift for () {
- fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
- Some(())
- }
-}
-
-impl<T> Subst<T> for () {
- fn subst_shift(&self, _var: &AlphaVar, _val: &T) -> Self {}
-}
-
+/// Equality up to alpha-equivalence
impl std::cmp::PartialEq for AlphaVar {
fn eq(&self, other: &Self) -> bool {
- match (&self.alpha, &other.alpha) {
- (Some(x), Some(y)) => x == y,
- (None, None) => self.normal == other.normal,
- _ => false,
- }
+ self.alpha == other.alpha
}
}
impl std::cmp::PartialEq for AlphaLabel {
@@ -127,10 +106,7 @@ impl std::cmp::PartialEq for AlphaLabel {
impl std::fmt::Debug for AlphaVar {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- match &self.alpha {
- Some(a) => write!(f, "AlphaVar({}, {})", self.normal, a.1),
- None => write!(f, "AlphaVar({}, free)", self.normal),
- }
+ write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1)
}
}
@@ -144,7 +120,7 @@ impl From<Label> for AlphaVar {
fn from(x: Label) -> AlphaVar {
AlphaVar {
normal: V(x, 0),
- alpha: Some(V((), 0)),
+ alpha: V((), 0),
}
}
}
@@ -175,3 +151,153 @@ impl From<AlphaLabel> for Label {
x.0
}
}
+impl Shift for () {
+ fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
+ Some(())
+ }
+}
+
+impl<A: Shift, B: Shift> Shift for (A, B) {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for Option<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ None => None,
+ Some(x) => Some(x.shift(delta, var)?),
+ })
+ }
+}
+
+impl<T: Shift> Shift for Box<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Box::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::rc::Rc<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::cell::RefCell<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(self.traverse_ref_with_special_handling_of_binders(
+ |v| Ok(v.shift(delta, var)?),
+ |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
+ )?)
+ }
+}
+
+impl<T: Shift> Shift for Vec<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|v| Ok(v.shift(delta, var)?))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<K, T: Shift> Shift for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ use dhall_syntax::InterpolatedTextContents::{Expr, Text};
+ Some(match self {
+ Expr(x) => Expr(x.shift(delta, var)?),
+ Text(s) => Text(s.clone()),
+ })
+ }
+}
+
+impl<S> Subst<S> for () {
+ fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
+}
+
+impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ (self.0.subst_shift(var, val), self.1.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Option<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.as_ref().map(|x| x.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Box<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ Box::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::rc::Rc::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::cell::RefCell::new(self.borrow().subst_shift(var, val))
+ }
+}
+
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.map_ref_with_special_handling_of_binders(
+ |v| v.subst_shift(var, val),
+ |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ )
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Vec<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter().map(|v| v.subst_shift(var, val)).collect()
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ use dhall_syntax::InterpolatedTextContents::{Expr, Text};
+ match self {
+ Expr(x) => Expr(x.subst_shift(var, val)),
+ Text(s) => Text(s.clone()),
+ }
+ }
+}
+
+impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter()
+ .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+ .collect()
+ }
+}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 8f6ff51..13a9d7e 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -3,8 +3,9 @@ use std::io::Error as IOError;
use dhall_syntax::{BinOp, Import, Label, ParseError, V};
use crate::core::context::TypecheckContext;
+use crate::core::value::Value;
use crate::phase::resolve::ImportStack;
-use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
+use crate::phase::NormalizedSubExpr;
pub type Result<T> = std::result::Result<T, Error>;
@@ -48,28 +49,27 @@ pub struct TypeError {
#[derive(Debug)]
pub(crate) enum TypeMessage {
UnboundVariable(V<Label>),
- InvalidInputType(Normalized),
- InvalidOutputType(Normalized),
- NotAFunction(Typed),
- TypeMismatch(Typed, Normalized, Typed),
- AnnotMismatch(Typed, Normalized),
+ InvalidInputType(Value),
+ InvalidOutputType(Value),
+ NotAFunction(Value),
+ TypeMismatch(Value, Value, Value),
+ AnnotMismatch(Value, Value),
Untyped,
- FieldCollision(Label),
- InvalidListElement(usize, Normalized, Typed),
- InvalidListType(Normalized),
- InvalidOptionalType(Normalized),
- InvalidPredicate(Typed),
- IfBranchMismatch(Typed, Typed),
- IfBranchMustBeTerm(bool, Typed),
- InvalidFieldType(Label, Type),
- NotARecord(Label, Normalized),
- MustCombineRecord(Typed),
- MissingRecordField(Label, Typed),
- MissingUnionField(Label, Normalized),
- BinOpTypeMismatch(BinOp, Typed),
- InvalidTextInterpolation(Typed),
- Merge1ArgMustBeRecord(Typed),
- Merge2ArgMustBeUnion(Typed),
+ InvalidListElement(usize, Value, Value),
+ InvalidListType(Value),
+ InvalidOptionalType(Value),
+ InvalidPredicate(Value),
+ IfBranchMismatch(Value, Value),
+ IfBranchMustBeTerm(bool, Value),
+ InvalidFieldType(Label, Value),
+ NotARecord(Label, Value),
+ MustCombineRecord(Value),
+ MissingRecordField(Label, Value),
+ MissingUnionField(Label, Value),
+ BinOpTypeMismatch(BinOp, Value),
+ InvalidTextInterpolation(Value),
+ Merge1ArgMustBeRecord(Value),
+ Merge2ArgMustBeUnion(Value),
MergeEmptyNeedsAnnotation,
MergeHandlerMissingVariant(Label),
MergeVariantMissingHandler(Label),
@@ -79,14 +79,12 @@ pub(crate) enum TypeMessage {
ProjectionMustBeRecord,
ProjectionMissingEntry,
Sort,
- RecordMismatch(Typed, Typed),
RecordTypeDuplicateField,
- RecordTypeMergeRequiresRecordType(Type),
- RecordTypeMismatch(Type, Type, Type, Type),
+ RecordTypeMergeRequiresRecordType(Value),
UnionTypeDuplicateField,
- EquivalenceArgumentMustBeTerm(bool, Typed),
- EquivalenceTypeMismatch(Typed, Typed),
- AssertMismatch(Typed, Typed),
+ EquivalenceArgumentMustBeTerm(bool, Value),
+ EquivalenceTypeMismatch(Value, Value),
+ AssertMismatch(Value, Value),
AssertMustTakeEquivalence,
}
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 778f990..1f7e5f0 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,8 +4,8 @@ use std::path::Path;
use dhall_syntax::{Const, SubExpr};
-use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
+use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(TypedThunk);
+pub struct Typed(Value);
/// A normalized expression.
///
@@ -41,8 +41,6 @@ pub struct Typed(TypedThunk);
#[derive(Debug, Clone)]
pub struct Normalized(Typed);
-pub type Type = Typed;
-
impl Parsed {
pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
parse::parse_file(f)
@@ -71,15 +69,10 @@ impl Parsed {
impl Resolved {
pub fn typecheck(self) -> Result<Typed, TypeError> {
- typecheck::typecheck(self)
- }
- pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
- typecheck::typecheck_with(self, ty)
+ Ok(typecheck::typecheck(self.0)?.into_typed())
}
- /// Pretends this expression has been typechecked. Use with care.
- #[allow(dead_code)]
- pub(crate) fn skip_typecheck(self) -> Typed {
- typecheck::skip_typecheck(self)
+ pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
+ Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
}
}
@@ -97,58 +90,39 @@ impl Typed {
Normalized(self)
}
- pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Typed(TypedThunk::from_thunk_and_type(th, t))
- }
- pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- Typed(TypedThunk::from_thunk_untyped(th))
- }
pub(crate) fn from_const(c: Const) -> Self {
- Typed(TypedThunk::from_const(c))
+ Typed(Value::from_const(c))
}
- pub fn from_value_untyped(v: Value) -> Self {
- Typed(TypedThunk::from_value_untyped(v))
+ pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
+ Typed(Value::from_valuef_and_type(v, t.into_value()))
}
- pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
+ pub(crate) fn from_value(th: Value) -> Self {
Typed(th)
}
-
- pub(crate) fn to_value(&self) -> Value {
- self.0.to_value()
+ pub fn const_type() -> Self {
+ Typed::from_const(Const::Type)
}
+
pub fn to_expr(&self) -> NormalizedSubExpr {
self.0.to_expr()
}
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.0.to_expr_alpha()
}
- pub fn to_thunk(&self) -> Thunk {
- self.0.to_thunk()
- }
- // Deprecated
- pub fn to_type(&self) -> Type {
- self.clone()
+ pub fn to_value(&self) -> Value {
+ self.0.clone()
}
- // Deprecated
- pub(crate) fn into_type(self) -> Type {
- self
- }
- pub(crate) fn into_typethunk(self) -> TypedThunk {
+ pub(crate) fn into_value(self) -> Value {
self.0
}
- pub(crate) fn to_normalized(&self) -> Normalized {
- self.clone().normalize()
- }
- pub(crate) fn as_const(&self) -> Option<Const> {
- self.0.as_const()
- }
pub(crate) fn normalize_mut(&mut self) {
self.0.normalize_mut()
}
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
- self.0.get_type()
+ #[allow(dead_code)]
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> {
+ Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed()))
}
}
@@ -164,13 +138,6 @@ impl Normalized {
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.0.to_expr_alpha()
}
- #[allow(dead_code)]
- pub(crate) fn to_type(&self) -> Type {
- self.0.to_type()
- }
- pub(crate) fn to_value(&self) -> Value {
- self.0.to_value()
- }
pub(crate) fn into_typed(self) -> Typed {
self.0
}
@@ -188,8 +155,8 @@ impl Shift for Normalized {
}
}
-impl Subst<Typed> for Typed {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for Typed {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
Typed(self.0.subst_shift(var, val))
}
}
@@ -234,7 +201,7 @@ impl std::hash::Hash for Normalized {
impl Eq for Typed {}
impl PartialEq for Typed {
fn eq(&self, other: &Self) -> bool {
- self.to_value() == other.to_value()
+ self.0 == other.0
}
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fd0197d..a379a4b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,13 +5,11 @@ use dhall_syntax::{
NaiveDouble,
};
-use crate::core::context::NormalizationContext;
-use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
+use crate::core::valuef::ValueF;
use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr};
-pub(crate) type InputSubExpr = ResolvedSubExpr;
pub(crate) type OutputSubExpr = NormalizedSubExpr;
// Ad-hoc macro to help construct closures
@@ -22,67 +20,76 @@ macro_rules! make_closure {
Label::from(stringify!($var)).into(),
$n
);
- Value::Var(var).into_thunk()
+ ValueF::Var(var).into_value_untyped()
}};
+ // Warning: assumes that $ty, as a dhall value, has type `Type`
(λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
- Value::Lam(
+ ValueF::Lam(
Label::from(stringify!($var)).into(),
- TypedThunk::from_thunk_untyped(make_closure!($($ty)*)),
+ make_closure!($($ty)*),
make_closure!($($rest)*),
- ).into_thunk()
+ ).into_value_untyped()
+ };
+ (Natural) => {
+ ValueF::from_builtin(Builtin::Natural)
+ .into_value_simple_type()
};
- (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() };
(List $($rest:tt)*) => {
- Value::from_builtin(Builtin::List)
- .app_thunk(make_closure!($($rest)*))
- .into_thunk()
+ ValueF::from_builtin(Builtin::List)
+ .app_value(make_closure!($($rest)*))
+ .into_value_simple_type()
};
- (Some $($rest:tt)*) => {
- Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+ (Some($($rest:tt)*)) => {
+ ValueF::NEOptionalLit(make_closure!($($rest)*))
+ .into_value_untyped()
};
(1 + $($rest:tt)*) => {
- Value::PartialExpr(ExprF::BinOp(
+ ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::NaturalPlus,
make_closure!($($rest)*),
- Thunk::from_value(Value::NaturalLit(1)),
- )).into_thunk()
+ Value::from_valuef_and_type(
+ ValueF::NaturalLit(1),
+ make_closure!(Natural)
+ ),
+ )).into_value_with_type(
+ make_closure!(Natural)
+ )
};
([ $($head:tt)* ] # $($tail:tt)*) => {
- Value::PartialExpr(ExprF::BinOp(
+ ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::ListAppend,
- Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+ ValueF::NEListLit(vec![make_closure!($($head)*)])
+ .into_value_untyped(),
make_closure!($($tail)*),
- )).into_thunk()
+ )).into_value_untyped()
};
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
use dhall_syntax::Builtin::*;
- use Value::*;
+ use ValueF::*;
// Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t, r..]) => {
- Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone()))))
- }
- (NaturalIsZero, [n, r..]) => match &*n.as_value() {
+ (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
+ (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
_ => Err(()),
},
- (NaturalEven, [n, r..]) => match &*n.as_value() {
+ (NaturalEven, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
_ => Err(()),
},
- (NaturalOdd, [n, r..]) => match &*n.as_value() {
+ (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
_ => Err(()),
},
- (NaturalToInteger, [n, r..]) => match &*n.as_value() {
+ (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
_ => Err(()),
},
- (NaturalShow, [n, r..]) => match &*n.as_value() {
+ (NaturalShow, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((
r,
TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
@@ -90,7 +97,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Err(()),
},
(NaturalSubtract, [a, b, r..]) => {
- match (&*a.as_value(), &*b.as_value()) {
+ match (&*a.as_whnf(), &*b.as_whnf()) {
(NaturalLit(a), NaturalLit(b)) => {
Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
}
@@ -100,7 +107,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Err(()),
}
}
- (IntegerShow, [n, r..]) => match &*n.as_value() {
+ (IntegerShow, [n, r..]) => match &*n.as_whnf() {
IntegerLit(n) => {
let s = if *n < 0 {
n.to_string()
@@ -111,18 +118,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
}
_ => Err(()),
},
- (IntegerToDouble, [n, r..]) => match &*n.as_value() {
+ (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
_ => Err(()),
},
- (DoubleShow, [n, r..]) => match &*n.as_value() {
+ (DoubleShow, [n, r..]) => match &*n.as_whnf() {
DoubleLit(n) => Ok((
r,
TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
)),
_ => Err(()),
},
- (TextShow, [v, r..]) => match &*v.as_value() {
+ (TextShow, [v, r..]) => match &*v.as_whnf() {
TextLit(elts) => {
match elts.as_slice() {
// Empty string literal.
@@ -156,41 +163,44 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
}
_ => Err(()),
},
- (ListLength, [_, l, r..]) => match &*l.as_value() {
+ (ListLength, [_, l, r..]) => match &*l.as_whnf() {
EmptyListLit(_) => Ok((r, NaturalLit(0))),
NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
_ => Err(()),
},
- (ListHead, [_, l, r..]) => match &*l.as_value() {
+ (ListHead, [_, l, r..]) => match &*l.as_whnf() {
EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
NEListLit(xs) => {
Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
}
_ => Err(()),
},
- (ListLast, [_, l, r..]) => match &*l.as_value() {
+ (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(()),
},
- (ListReverse, [_, l, r..]) => match &*l.as_value() {
+ (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
NEListLit(xs) => {
Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
}
_ => Err(()),
},
- (ListIndexed, [_, l, r..]) => match &*l.as_value() {
+ (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
EmptyListLit(t) => {
let mut kts = HashMap::new();
kts.insert(
"index".into(),
- TypedThunk::from_value(Value::from_builtin(Natural)),
+ Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
);
kts.insert("value".into(), t.clone());
- Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts)))))
+ Ok((
+ r,
+ EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
+ ))
}
NEListLit(xs) => {
let xs = xs
@@ -199,105 +209,131 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
.map(|(i, e)| {
let i = NaturalLit(i);
let mut kvs = HashMap::new();
- kvs.insert("index".into(), Thunk::from_value(i));
+ kvs.insert(
+ "index".into(),
+ Value::from_valuef_untyped(i),
+ );
kvs.insert("value".into(), e.clone());
- Thunk::from_value(RecordLit(kvs))
+ Value::from_valuef_untyped(RecordLit(kvs))
})
.collect();
Ok((r, NEListLit(xs)))
}
_ => Err(()),
},
- (ListBuild, [t, f, r..]) => match &*f.as_value() {
+ (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
// fold/build fusion
- Value::AppliedBuiltin(ListFold, args) => {
+ ValueF::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_value()))
+ Ok((r, args[1].to_whnf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
- .app_thunk({
- // Move `t` under new `x` variable
- let t1 = t.under_binder(Label::from("x"));
- make_closure!(
- λ(x : #t) ->
- λ(xs : List #t1) ->
- [ var(x, 1) ] # var(xs, 0)
- )
- })
- .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
- )),
+ _ => {
+ 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 t1 = t.under_binder(Label::from("x"));
+ make_closure!(
+ λ(x : #t) ->
+ λ(xs : List #t1) ->
+ [ var(x, 1) ] # var(xs, 0)
+ )
+ })
+ .app_value(
+ EmptyListLit(t.clone())
+ .into_value_with_type(list_t),
+ ),
+ ))
+ }
},
- (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
- EmptyListLit(_) => Ok((r, nil.to_value())),
+ (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ok((r, nil.to_whnf())),
NEListLit(xs) => {
let mut v = nil.clone();
for x in xs.iter().rev() {
v = cons
.clone()
- .app_thunk(x.clone())
- .app_thunk(v)
- .into_thunk();
+ .app_value(x.clone())
+ .app_value(v)
+ .into_value_untyped();
}
- Ok((r, v.to_value()))
+ Ok((r, v.to_whnf()))
}
_ => Err(()),
},
- (OptionalBuild, [t, f, r..]) => match &*f.as_value() {
+ (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
// fold/build fusion
- Value::AppliedBuiltin(OptionalFold, args) => {
+ ValueF::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_value()))
+ Ok((r, args[1].to_whnf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
- .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
- .app_val(EmptyOptionalLit(TypedThunk::from_thunk(
- t.clone(),
- ))),
- )),
+ _ => {
+ 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(
+ EmptyOptionalLit(t.clone())
+ .into_value_with_type(optional_t),
+ ),
+ ))
+ }
},
- (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
- EmptyOptionalLit(_) => Ok((r, nothing.to_value())),
- NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+ (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(()),
},
- (NaturalBuild, [f, r..]) => match &*f.as_value() {
+ (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
// fold/build fusion
- Value::AppliedBuiltin(NaturalFold, args) => {
+ ValueF::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
- Ok((r, args[0].to_value()))
+ Ok((r, args[0].to_whnf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(Natural))
- .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
- .app_val(NaturalLit(0)),
- )),
+ _ => {
+ 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),
+ ),
+ ))
+ }
},
- (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() {
- NaturalLit(0) => Ok((r, zero.to_value())),
+ (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
+ NaturalLit(0) => Ok((r, zero.to_whnf())),
NaturalLit(n) => {
- let fold = Value::from_builtin(NaturalFold)
+ let fold = ValueF::from_builtin(NaturalFold)
.app(NaturalLit(n - 1))
- .app_thunk(t.clone())
- .app_thunk(succ.clone())
- .app_thunk(zero.clone());
- Ok((r, succ.app_val(fold)))
+ .app_value(t.clone())
+ .app_value(succ.clone())
+ .app_value(zero.clone())
+ .into_value_with_type(t.clone());
+ Ok((r, succ.app_value(fold)))
}
_ => Err(()),
},
@@ -307,7 +343,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
Ok((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_thunk(x);
+ v = v.app_value(x);
}
v
}
@@ -315,22 +351,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
}
}
-pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value {
- let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
+ let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
- let f_borrow = f.as_value();
+ let f_borrow = f.as_whnf();
match &*f_borrow {
- Value::Lam(x, _, e) => {
- let val = Typed::from_thunk_untyped(a);
- e.subst_shift(&x.into(), &val).to_value()
- }
- Value::AppliedBuiltin(b, args) => {
+ ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+ ValueF::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args)
}
- Value::UnionConstructor(l, kts) => {
- Value::UnionLit(l.clone(), a, kts.clone())
+ ValueF::UnionConstructor(l, kts) => {
+ ValueF::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
@@ -340,23 +373,23 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value {
}
pub(crate) fn squash_textlit(
- elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
-) -> Vec<InterpolatedTextContents<Thunk>> {
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
use std::mem::replace;
use InterpolatedTextContents::{Expr, Text};
fn inner(
- elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
crnt_str: &mut String,
- ret: &mut Vec<InterpolatedTextContents<Thunk>>,
+ ret: &mut Vec<InterpolatedTextContents<Value>>,
) {
for contents in elts {
match contents {
Text(s) => crnt_str.push_str(&s),
Expr(e) => {
- let e_borrow = e.as_value();
+ let e_borrow = e.as_whnf();
match &*e_borrow {
- Value::TextLit(elts2) => {
+ ValueF::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
}
_ => {
@@ -381,32 +414,6 @@ pub(crate) fn squash_textlit(
ret
}
-/// Reduces the imput expression to a Value. Evaluates as little as possible.
-pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
- match expr.as_ref() {
- ExprF::Embed(e) => return e.to_value(),
- ExprF::Var(v) => return ctx.lookup(v),
- _ => {}
- }
-
- // Thunk subexpressions
- let expr: ExprF<Thunk, Normalized> =
- expr.as_ref().map_ref_with_special_handling_of_binders(
- |e| Thunk::new(ctx.clone(), e.clone()),
- |x, e| Thunk::new(ctx.skip(x), e.clone()),
- );
-
- normalize_one_layer(expr)
-}
-
-// Small helper enum to avoid repetition
-enum Ret<'a> {
- Value(Value),
- Thunk(Thunk),
- ThunkRef(&'a Thunk),
- Expr(ExprF<Thunk, Normalized>),
-}
-
/// Performs an intersection of two HashMaps.
///
/// # Arguments
@@ -441,60 +448,6 @@ where
kvs
}
-/// Performs an outer join of two HashMaps.
-///
-/// # Arguments
-///
-/// * `ft` - Will convert the values of the first map
-/// into the target value.
-///
-/// * `fu` - Will convert the values of the second map
-/// into the target value.
-///
-/// * `fktu` - Will convert the key and values from both maps
-/// into the target type.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `fktu` function. Otherwise, the
-/// final value will be calculated by either the `ft` or `fu` value
-/// depending on which map the key is present in.
-///
-/// The final map will contain all keys from the two input maps with
-/// also values computed as per above.
-pub(crate) fn outer_join<K, T, U, V>(
- mut ft: impl FnMut(&T) -> V,
- mut fu: impl FnMut(&U) -> V,
- mut fktu: 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 (k1, t) in map1 {
- let v = if let Some(u) = map2.get(k1) {
- // The key exists in both maps
- // so use all values for computation
- fktu(k1, t, u)
- } else {
- // Key only exists in map1
- ft(t)
- };
- kvs.insert(k1.clone(), v);
- }
-
- for (k1, u) in map2 {
- // Insert if key was missing in map1
- kvs.entry(k1.clone()).or_insert(fu(u));
- }
-
- kvs
-}
-
pub(crate) fn merge_maps<K, V>(
map1: &HashMap<K, V>,
map2: &HashMap<K, V>,
@@ -520,82 +473,90 @@ where
kvs
}
-fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprF<Value, Normalized>),
+}
+
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use Value::{
+ use ValueF::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
TextLit,
};
- let x_borrow = x.as_value();
- let y_borrow = y.as_value();
+ let x_borrow = x.as_whnf();
+ let y_borrow = y.as_whnf();
Some(match (o, &*x_borrow, &*y_borrow) {
- (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
- (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
- (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)),
- (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
- (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)),
- (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
- (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
- (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
- (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
- (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
- (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)),
- (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
- (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
- (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)),
-
- (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
- (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
+ (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
+ (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
+ (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
+ (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
+ (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
+ (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => Ret::ValueF(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::ValueF(BoolLit(x == y)),
+ (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
+ (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
+ (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
+ (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
+ (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
+
+ (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Ret::Value(NaturalLit(x + y))
+ Ret::ValueF(NaturalLit(x + y))
}
- (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)),
- (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
- (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
+ (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Ret::Value(NaturalLit(x * y))
+ Ret::ValueF(NaturalLit(x * y))
}
- (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
- (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => {
- Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
- }
+ (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
+ xs.iter().chain(ys.iter()).cloned().collect(),
+ )),
- (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
- (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
- (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit(
+ (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::ValueF(TextLit(
squash_textlit(x.iter().chain(y.iter()).cloned()),
)),
(TextAppend, TextLit(x), _) => {
use std::iter::once;
let y = InterpolatedTextContents::Expr(y.clone());
- Ret::Value(TextLit(squash_textlit(
+ Ret::ValueF(TextLit(squash_textlit(
x.iter().cloned().chain(once(y)),
)))
}
(TextAppend, _, TextLit(y)) => {
use std::iter::once;
let x = InterpolatedTextContents::Expr(x.clone());
- Ret::Value(TextLit(squash_textlit(
+ Ret::ValueF(TextLit(squash_textlit(
once(x).chain(y.iter().cloned()),
)))
}
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -603,54 +564,53 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- Ret::Value(RecordLit(kvs))
+ Ret::ValueF(RecordLit(kvs))
}
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Thunk::from_partial_expr(ExprF::BinOp(
+ Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
- ))
+ )))
});
- Ret::Value(RecordLit(kvs))
+ Ret::ValueF(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
+ Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
RecursiveRecordTypeMerge,
- v1.to_thunk(),
- v2.to_thunk(),
+ v1.clone(),
+ v2.clone(),
)))
});
- Ret::Value(RecordType(kvs))
+ Ret::ValueF(RecordType(kvs))
}
- (Equivalence, _, _) => Ret::Value(Value::Equivalence(
- TypedThunk::from_thunk(x.clone()),
- TypedThunk::from_thunk(y.clone()),
- )),
+ (Equivalence, _, _) => {
+ Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+ }
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
- use Value::{
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+ use ValueF::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
TextLit, UnionConstructor, UnionLit, UnionType,
@@ -662,36 +622,25 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
),
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => Ret::Thunk(x),
+ ExprF::Annot(x, _) => Ret::Value(x),
ExprF::Assert(_) => Ret::Expr(expr),
- ExprF::Lam(x, t, e) => {
- Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e))
- }
- ExprF::Pi(x, t, e) => Ret::Value(Pi(
- x.into(),
- TypedThunk::from_thunk(t),
- TypedThunk::from_thunk(e),
- )),
- ExprF::Let(x, _, v, b) => {
- let v = Typed::from_thunk_untyped(v);
- Ret::Thunk(b.subst_shift(&x.into(), &v))
- }
- ExprF::App(v, a) => Ret::Value(v.app_thunk(a)),
- ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)),
- ExprF::Const(c) => Ret::Value(Value::Const(c)),
- ExprF::BoolLit(b) => Ret::Value(BoolLit(b)),
- ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
- ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
- ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
- ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
+ 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::BoolLit(b) => Ret::ValueF(BoolLit(b)),
+ ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
+ ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
+ ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
+ ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
ExprF::EmptyListLit(ref t) => {
// Check if the type is of the form `List x`
- let t_borrow = t.as_value();
+ let t_borrow = t.as_whnf();
match &*t_borrow {
AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
- Ret::Value(EmptyListLit(TypedThunk::from_thunk(
- args[0].clone(),
- )))
+ Ret::ValueF(EmptyListLit(args[0].clone()))
}
_ => {
drop(t_borrow);
@@ -700,43 +649,39 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
}
}
ExprF::NEListLit(elts) => {
- Ret::Value(NEListLit(elts.into_iter().collect()))
+ Ret::ValueF(NEListLit(elts.into_iter().collect()))
}
ExprF::RecordLit(kvs) => {
- Ret::Value(RecordLit(kvs.into_iter().collect()))
+ 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::RecordType(kts) => Ret::Value(RecordType(
- kts.into_iter()
- .map(|(k, t)| (k, TypedThunk::from_thunk(t)))
- .collect(),
- )),
- ExprF::UnionType(kts) => Ret::Value(UnionType(
- kts.into_iter()
- .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t))))
- .collect(),
- )),
ExprF::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
// Simplify bare interpolation
if let [Expr(th)] = elts.as_slice() {
- Ret::Thunk(th.clone())
+ Ret::Value(th.clone())
} else {
- Ret::Value(TextLit(elts))
+ Ret::ValueF(TextLit(elts))
}
}
ExprF::BoolIf(ref b, ref e1, ref e2) => {
- let b_borrow = b.as_value();
+ let b_borrow = b.as_whnf();
match &*b_borrow {
- BoolLit(true) => Ret::ThunkRef(e1),
- BoolLit(false) => Ret::ThunkRef(e2),
+ BoolLit(true) => Ret::ValueRef(e1),
+ BoolLit(false) => Ret::ValueRef(e2),
_ => {
- let e1_borrow = e1.as_value();
- let e2_borrow = e2.as_value();
+ let e1_borrow = e1.as_whnf();
+ let e2_borrow = e2.as_whnf();
match (&*e1_borrow, &*e2_borrow) {
// Simplify `if b then True else False`
- (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
- _ if e1 == e2 => Ret::ThunkRef(e1),
+ (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ _ if e1 == e2 => Ret::ValueRef(e1),
_ => {
drop(b_borrow);
drop(e1_borrow);
@@ -753,12 +698,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
},
ExprF::Projection(_, ref ls) if ls.is_empty() => {
- Ret::Value(RecordLit(HashMap::new()))
+ Ret::ValueF(RecordLit(HashMap::new()))
}
ExprF::Projection(ref v, ref ls) => {
- let v_borrow = v.as_value();
+ let v_borrow = v.as_whnf();
match &*v_borrow {
- RecordLit(kvs) => Ret::Value(RecordLit(
+ RecordLit(kvs) => Ret::ValueF(RecordLit(
ls.iter()
.filter_map(|l| {
kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -772,17 +717,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
}
}
ExprF::Field(ref v, ref l) => {
- let v_borrow = v.as_value();
+ let v_borrow = v.as_whnf();
match &*v_borrow {
RecordLit(kvs) => match kvs.get(l) {
- Some(r) => Ret::Thunk(r.clone()),
+ Some(r) => Ret::Value(r.clone()),
None => {
drop(v_borrow);
Ret::Expr(expr)
}
},
UnionType(kts) => {
- Ret::Value(UnionConstructor(l.clone(), kts.clone()))
+ Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
}
_ => {
drop(v_borrow);
@@ -792,11 +737,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
}
ExprF::Merge(ref handlers, ref variant, _) => {
- let handlers_borrow = handlers.as_value();
- let variant_borrow = variant.as_value();
+ 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) {
- Some(h) => Ret::Thunk(h.clone()),
+ Some(h) => Ret::Value(h.clone()),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -804,7 +749,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::Value(h.app_thunk(v.clone())),
+ Some(h) => Ret::ValueF(h.app_value(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -821,9 +766,22 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
};
match ret {
- Ret::Value(v) => v,
- Ret::Thunk(th) => th.to_value(),
- Ret::ThunkRef(th) => th.to_value(),
- Ret::Expr(expr) => Value::PartialExpr(expr),
+ Ret::ValueF(v) => v,
+ Ret::Value(th) => th.as_whnf().clone(),
+ Ret::ValueRef(th) => th.as_whnf().clone(),
+ Ret::Expr(expr) => ValueF::PartialExpr(expr),
+ }
+}
+
+/// Normalize a ValueF into WHNF
+pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+ match v {
+ ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
+ ValueF::PartialExpr(e) => normalize_one_layer(e),
+ ValueF::TextLit(elts) => {
+ ValueF::TextLit(squash_textlit(elts.into_iter()))
+ }
+ // All other cases are already in WHNF
+ v => v,
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 56fb5ed..c47eb78 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,33 +1,29 @@
+use std::cmp::max;
use std::collections::HashMap;
use dhall_syntax::{
rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
};
-use crate::core::context::{NormalizationContext, TypecheckContext};
-use crate::core::thunk::{Thunk, TypedThunk};
+use crate::core::context::TypecheckContext;
use crate::core::value::Value;
+use crate::core::valuef::ValueF;
use crate::core::var::{Shift, Subst};
use crate::error::{TypeError, TypeMessage};
-use crate::phase::{Normalized, Resolved, Type, Typed};
+use crate::phase::Normalized;
fn tck_pi_type(
ctx: &TypecheckContext,
x: Label,
- tx: Type,
- te: Type,
-) -> Result<Typed, TypeError> {
+ tx: Value,
+ te: Value,
+) -> Result<Value, TypeError> {
use crate::error::TypeMessage::*;
let ctx2 = ctx.insert_type(&x, tx.clone());
let ka = match tx.get_type()?.as_const() {
Some(k) => k,
- _ => {
- return Err(TypeError::new(
- ctx,
- InvalidInputType(tx.to_normalized()),
- ))
- }
+ _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
};
let kb = match te.get_type()?.as_const() {
@@ -35,68 +31,58 @@ fn tck_pi_type(
_ => {
return Err(TypeError::new(
&ctx2,
- InvalidOutputType(te.get_type()?.to_normalized()),
+ InvalidOutputType(te.get_type()?.into_owned()),
))
}
};
let k = function_check(ka, kb);
- Ok(Typed::from_thunk_and_type(
- Value::Pi(
- x.into(),
- TypedThunk::from_type(tx),
- TypedThunk::from_type(te),
- )
- .into_thunk(),
- Type::from_const(k),
+ Ok(Value::from_valuef_and_type(
+ ValueF::Pi(x.into(), tx, te),
+ Value::from_const(k),
))
}
fn tck_record_type(
ctx: &TypecheckContext,
- kts: impl IntoIterator<Item = Result<(Label, Type), TypeError>>,
-) -> Result<Typed, TypeError> {
+ kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
+) -> Result<Value, TypeError> {
use crate::error::TypeMessage::*;
use std::collections::hash_map::Entry;
let mut new_kts = HashMap::new();
- // Check that all types are the same const
- let mut k = None;
+ // An empty record type has type Type
+ let mut k = Const::Type;
for e in kts {
let (x, t) = e?;
- match (k, t.get_type()?.as_const()) {
- (None, Some(k2)) => k = Some(k2),
- (Some(k1), Some(k2)) if k1 == k2 => {}
- _ => {
- return Err(TypeError::new(
- ctx,
- InvalidFieldType(x.clone(), t.clone()),
- ))
- }
+ // 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))),
}
- let entry = new_kts.entry(x.clone());
+ // Check for duplicated entries
+ let entry = new_kts.entry(x);
match &entry {
Entry::Occupied(_) => {
return Err(TypeError::new(ctx, RecordTypeDuplicateField))
}
- Entry::Vacant(_) => {
- entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
- }
+ Entry::Vacant(_) => entry.or_insert_with(|| t),
};
}
- // An empty record type has type Type
- let k = k.unwrap_or(dhall_syntax::Const::Type);
- Ok(Typed::from_thunk_and_type(
- Value::RecordType(new_kts).into_thunk(),
- Type::from_const(k),
+ Ok(Value::from_valuef_and_type(
+ ValueF::RecordType(new_kts),
+ Value::from_const(k),
))
}
-fn tck_union_type(
+fn tck_union_type<Iter>(
ctx: &TypecheckContext,
- kts: impl IntoIterator<Item = Result<(Label, Option<Type>), TypeError>>,
-) -> Result<Typed, TypeError> {
+ kts: Iter,
+) -> Result<Value, TypeError>
+where
+ Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
+{
use crate::error::TypeMessage::*;
use std::collections::hash_map::Entry;
let mut new_kts = HashMap::new();
@@ -111,46 +97,42 @@ fn tck_union_type(
_ => {
return Err(TypeError::new(
ctx,
- InvalidFieldType(x.clone(), t.clone()),
+ InvalidFieldType(x, t.clone()),
))
}
}
}
- let entry = new_kts.entry(x.clone());
+ let entry = new_kts.entry(x);
match &entry {
Entry::Occupied(_) => {
return Err(TypeError::new(ctx, UnionTypeDuplicateField))
}
- Entry::Vacant(_) => entry.or_insert_with(|| {
- t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
- }),
+ 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(dhall_syntax::Const::Type);
+ let k = k.unwrap_or(Const::Type);
- Ok(Typed::from_thunk_and_type(
- Value::UnionType(new_kts).into_thunk(),
- Type::from_const(k),
+ Ok(Value::from_valuef_and_type(
+ ValueF::UnionType(new_kts),
+ Value::from_const(k),
))
}
fn function_check(a: Const, b: Const) -> Const {
- use dhall_syntax::Const::Type;
- use std::cmp::max;
- if b == Type {
- Type
+ if b == Const::Type {
+ Const::Type
} else {
max(a, b)
}
}
-pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> {
+pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> {
match c {
- Const::Type => Ok(Type::from_const(Const::Kind)),
- Const::Kind => Ok(Type::from_const(Const::Sort)),
+ Const::Type => Ok(Value::from_const(Const::Kind)),
+ Const::Kind => Ok(Value::from_const(Const::Sort)),
Const::Sort => {
Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
}
@@ -298,25 +280,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
}
}
-/// Takes an expression that is meant to contain a Type
-/// and turn it into a type, typechecking it along the way.
-pub(crate) fn mktype(
- ctx: &TypecheckContext,
- e: SubExpr<Normalized>,
-) -> Result<Type, TypeError> {
- Ok(type_with(ctx, e)?.to_type())
-}
-
-pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> {
- mktype(&TypecheckContext::new(), SubExpr::from_builtin(b))
-}
-
-/// Intermediary return type
-enum Ret {
- /// Returns the contained value as is
- RetWhole(Typed),
- /// Use the contained Type as the type of the input expression
- RetTypeOnly(Type),
+// TODO: this can't fail in practise
+pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> {
+ type_with(&TypecheckContext::new(), SubExpr::from_builtin(b))
}
/// Type-check an expression and return the expression alongside its type if type-checking
@@ -326,28 +292,23 @@ enum Ret {
fn type_with(
ctx: &TypecheckContext,
e: SubExpr<Normalized>,
-) -> Result<Typed, TypeError> {
+) -> Result<Value, TypeError> {
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
- use Ret::*;
Ok(match e.as_ref() {
Lam(x, t, b) => {
- let tx = mktype(ctx, t.clone())?;
+ let tx = type_with(ctx, t.clone())?;
let ctx2 = ctx.insert_type(x, tx.clone());
let b = type_with(&ctx2, b.clone())?;
- let v = Value::Lam(
- x.clone().into(),
- TypedThunk::from_type(tx.clone()),
- b.to_thunk(),
- );
+ 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)?.to_type();
- Typed::from_thunk_and_type(Thunk::from_value(v), t)
+ let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
+ Value::from_valuef_and_type(v, t)
}
Pi(x, ta, tb) => {
- let ta = mktype(ctx, ta.clone())?;
+ let ta = type_with(ctx, ta.clone())?;
let ctx2 = ctx.insert_type(x, ta.clone());
- let tb = mktype(&ctx2, tb.clone())?;
+ let tb = type_with(&ctx2, tb.clone())?;
return tck_pi_type(ctx, x.clone(), ta, tb);
}
Let(x, t, v, e) => {
@@ -360,9 +321,9 @@ fn type_with(
let v = type_with(ctx, v)?;
return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
}
- Embed(p) => p.clone().into_typed(),
+ Embed(p) => p.clone().into_typed().into_value(),
Var(var) => match ctx.lookup(&var) {
- Some(typed) => typed,
+ Some(typed) => typed.clone(),
None => {
return Err(TypeError::new(
ctx,
@@ -370,24 +331,13 @@ fn type_with(
))
}
},
- _ => {
+ e => {
// Typecheck recursively all subexpressions
- let expr =
- e.as_ref().traverse_ref_with_special_handling_of_binders(
- |e| type_with(ctx, e.clone()),
- |_, _| unreachable!(),
- )?;
- let ret = type_last_layer(ctx, &expr)?;
- match ret {
- RetTypeOnly(typ) => {
- let expr = expr.map_ref(|typed| typed.to_thunk());
- Typed::from_thunk_and_type(
- Thunk::from_partial_expr(expr),
- typ,
- )
- }
- RetWhole(tt) => tt,
- }
+ let expr = e.traverse_ref_with_special_handling_of_binders(
+ |e| type_with(ctx, e.clone()),
+ |_, _| unreachable!(),
+ )?;
+ type_last_layer(ctx, expr)?
}
})
}
@@ -396,17 +346,25 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: &ExprF<Typed, Normalized>,
-) -> Result<Ret, TypeError> {
+ e: ExprF<Value, Normalized>,
+) -> Result<Value, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;
use dhall_syntax::Builtin::*;
use dhall_syntax::Const::Type;
use dhall_syntax::ExprF::*;
+ let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
+
+ /// 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 mkerr = |msg: TypeMessage| TypeError::new(ctx, msg);
- match e {
+ let ret = match &e {
Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
@@ -415,456 +373,296 @@ fn type_last_layer(
}
App(f, a) => {
let tf = f.get_type()?;
- let (x, tx, tb) = match &tf.to_value() {
- Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()),
- _ => return Err(mkerr(NotAFunction(f.clone()))),
+ let tf_borrow = tf.as_whnf();
+ let (x, tx, tb) = match &*tf_borrow {
+ ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ _ => return mkerr(NotAFunction(f.clone())),
};
- if a.get_type()?.as_ref() != &tx {
- return Err(mkerr(TypeMismatch(
- f.clone(),
- tx.to_normalized(),
- a.clone(),
- )));
+ if a.get_type()?.as_ref() != tx {
+ return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
}
- Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a)))
+ RetTypeOnly(tb.subst_shift(&x.into(), a))
}
Annot(x, t) => {
- let t = t.to_type();
- if &t != x.get_type()?.as_ref() {
- return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized())));
+ if t != x.get_type()?.as_ref() {
+ return mkerr(AnnotMismatch(x.clone(), t.clone()));
}
- Ok(RetTypeOnly(x.get_type()?.into_owned()))
+ RetTypeOnly(x.get_type()?.into_owned())
}
Assert(t) => {
- match t.to_value() {
- Value::Equivalence(ref x, ref y) if x == y => {}
- Value::Equivalence(x, y) => {
- return Err(mkerr(AssertMismatch(
- x.to_typed(),
- y.to_typed(),
- )))
+ match &*t.as_whnf() {
+ ValueF::Equivalence(x, y) if x == y => {}
+ ValueF::Equivalence(x, y) => {
+ return mkerr(AssertMismatch(x.clone(), y.clone()))
}
- _ => return Err(mkerr(AssertMustTakeEquivalence)),
+ _ => return mkerr(AssertMustTakeEquivalence),
}
- Ok(RetTypeOnly(t.to_type()))
+ RetTypeOnly(t.clone())
}
BoolIf(x, y, z) => {
if x.get_type()?.as_ref() != &builtin_to_type(Bool)? {
- return Err(mkerr(InvalidPredicate(x.clone())));
+ return mkerr(InvalidPredicate(x.clone()));
}
if y.get_type()?.get_type()?.as_const() != Some(Type) {
- return Err(mkerr(IfBranchMustBeTerm(true, y.clone())));
+ return mkerr(IfBranchMustBeTerm(true, y.clone()));
}
if z.get_type()?.get_type()?.as_const() != Some(Type) {
- return Err(mkerr(IfBranchMustBeTerm(false, z.clone())));
+ return mkerr(IfBranchMustBeTerm(false, z.clone()));
}
if y.get_type()? != z.get_type()? {
- return Err(mkerr(IfBranchMismatch(y.clone(), z.clone())));
+ return mkerr(IfBranchMismatch(y.clone(), z.clone()));
}
- Ok(RetTypeOnly(y.get_type()?.into_owned()))
+ RetTypeOnly(y.get_type()?.into_owned())
}
EmptyListLit(t) => {
- let t = t.to_type();
- match &t.to_value() {
- Value::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+ match &*t.as_whnf() {
+ ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args)
if args.len() == 1 => {}
- _ => {
- return Err(TypeError::new(
- ctx,
- InvalidListType(t.to_normalized()),
- ))
- }
+ _ => return mkerr(InvalidListType(t.clone())),
}
- Ok(RetTypeOnly(t))
+ RetTypeOnly(t.clone())
}
NEListLit(xs) => {
let mut iter = xs.iter().enumerate();
let (_, x) = iter.next().unwrap();
for (i, y) in iter {
if x.get_type()? != y.get_type()? {
- return Err(mkerr(InvalidListElement(
+ return mkerr(InvalidListElement(
i,
- x.get_type()?.to_normalized(),
+ x.get_type()?.into_owned(),
y.clone(),
- )));
+ ));
}
}
let t = x.get_type()?;
if t.get_type()?.as_const() != Some(Type) {
- return Err(TypeError::new(
- ctx,
- InvalidListType(t.to_normalized()),
- ));
+ return mkerr(InvalidListType(t.into_owned()));
}
- Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
- Value::from_builtin(dhall_syntax::Builtin::List)
- .app(t.to_value())
- .into_thunk(),
- Typed::from_const(Type),
- )
- .to_type(),
+ RetTypeOnly(Value::from_valuef_and_type(
+ ValueF::from_builtin(dhall_syntax::Builtin::List)
+ .app_value(t.into_owned()),
+ Value::from_const(Type),
))
}
SomeLit(x) => {
let t = x.get_type()?.into_owned();
if t.get_type()?.as_const() != Some(Type) {
- return Err(TypeError::new(
- ctx,
- InvalidOptionalType(t.to_normalized()),
- ));
+ return mkerr(InvalidOptionalType(t));
}
- Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
- Value::from_builtin(dhall_syntax::Builtin::Optional)
- .app(t.to_value())
- .into_thunk(),
- Typed::from_const(Type).into_type(),
- )
- .to_type(),
+ RetTypeOnly(Value::from_valuef_and_type(
+ ValueF::from_builtin(dhall_syntax::Builtin::Optional)
+ .app_value(t),
+ Value::from_const(Type),
))
}
- RecordType(kts) => Ok(RetWhole(tck_record_type(
+ RecordType(kts) => RetWhole(tck_record_type(
ctx,
- kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))),
- )?)),
- UnionType(kts) => Ok(RetWhole(tck_union_type(
+ 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.as_ref().map(|t| t.to_type())))),
- )?)),
- RecordLit(kvs) => Ok(RetTypeOnly(
- tck_record_type(
- ctx,
- kvs.iter()
- .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
- )?
- .into_type(),
- )),
+ 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()?.into_owned()))),
+ )?),
Field(r, x) => {
- match &r.get_type()?.to_value() {
- Value::RecordType(kts) => match kts.get(&x) {
+ match &*r.get_type()?.as_whnf() {
+ ValueF::RecordType(kts) => match kts.get(&x) {
Some(tth) => {
- Ok(RetTypeOnly(tth.to_type()))
+ RetTypeOnly(tth.clone())
},
- None => Err(mkerr(MissingRecordField(x.clone(),
- r.clone()))),
+ None => return mkerr(MissingRecordField(x.clone(),
+ r.clone())),
},
// TODO: branch here only when r.get_type() is a Const
_ => {
- let r = r.to_type();
- match &r.to_value() {
- Value::UnionType(kts) => match kts.get(&x) {
+ match &*r.as_whnf() {
+ ValueF::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
- // TODO: avoid capture
- Ok(RetTypeOnly(
+ RetTypeOnly(
tck_pi_type(
ctx,
"_".into(),
- t.to_type(),
- r.clone(),
- )?.to_type()
- ))
+ t.clone(),
+ r.under_binder(Label::from("_")),
+ )?
+ )
},
Some(None) => {
- Ok(RetTypeOnly(r.clone()))
+ RetTypeOnly(r.clone())
},
None => {
- Err(mkerr(MissingUnionField(
+ return mkerr(MissingUnionField(
x.clone(),
- r.to_normalized(),
- )))
+ r.clone(),
+ ))
},
},
_ => {
- Err(mkerr(NotARecord(
+ return mkerr(NotARecord(
x.clone(),
- r.to_normalized()
- )))
+ r.clone()
+ ))
},
}
}
- // _ => Err(mkerr(NotARecord(
+ // _ => mkerr(NotARecord(
// x,
- // r.to_type()?.to_normalized(),
- // ))),
+ // r?,
+ // )),
}
}
- Const(c) => Ok(RetWhole(Typed::from_const(*c))),
- Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)),
- BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
- NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
- IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
- DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)),
+ Const(c) => RetWhole(Value::from_const(*c)),
+ Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?),
+ BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?),
+ NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?),
+ IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?),
+ DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?),
TextLit(interpolated) => {
let text_type = builtin_to_type(Text)?;
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
if x.get_type()?.as_ref() != &text_type {
- return Err(mkerr(InvalidTextInterpolation(x.clone())));
+ return mkerr(InvalidTextInterpolation(x.clone()));
}
}
}
- Ok(RetTypeOnly(text_type))
+ RetTypeOnly(text_type)
}
BinOp(RightBiasedRecordMerge, l, r) => {
use crate::phase::normalize::merge_maps;
let l_type = l.get_type()?;
- let l_kind = l_type.get_type()?;
let r_type = r.get_type()?;
- let r_kind = r_type.get_type()?;
-
- // Check the equality of kinds.
- // This is to disallow expression such as:
- // "{ x = Text } // { y = 1 }"
- if l_kind != r_kind {
- return Err(mkerr(RecordMismatch(l.clone(), r.clone())));
- }
// Extract the LHS record type
- let kts_x = match l_type.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(MustCombineRecord(l.clone()))),
+ let l_type_borrow = l_type.as_whnf();
+ let kts_x = match &*l_type_borrow {
+ ValueF::RecordType(kts) => kts,
+ _ => return mkerr(MustCombineRecord(l.clone())),
};
// Extract the RHS record type
- let kts_y = match r_type.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(MustCombineRecord(r.clone()))),
+ let r_type_borrow = r_type.as_whnf();
+ let kts_y = match &*r_type_borrow {
+ ValueF::RecordType(kts) => kts,
+ _ => return mkerr(MustCombineRecord(r.clone())),
};
// 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| r_t.clone());
// Construct the final record type from the union
- Ok(RetTypeOnly(
- tck_record_type(
- ctx,
- kts.iter().map(|(x, v)| Ok((x.clone(), v.to_type()))),
- )?
- .into_type(),
- ))
- }
- BinOp(RecursiveRecordMerge, l, r) => {
- // A recursive function to dig down into
- // records of records when merging.
- fn combine_record_types(
- ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypedThunk>,
- kts_r: HashMap<Label, TypedThunk>,
- ) -> Result<Typed, TypeError> {
- use crate::phase::normalize::outer_join;
-
- // If the Label exists for both records and Type for the values
- // are records themselves, then we hit the recursive case.
- // Otherwise we have a field collision.
- let combine = |k: &Label,
- inner_l: &TypedThunk,
- inner_r: &TypedThunk|
- -> Result<Typed, TypeError> {
- match (inner_l.to_value(), inner_r.to_value()) {
- (
- Value::RecordType(inner_l_kvs),
- Value::RecordType(inner_r_kvs),
- ) => {
- combine_record_types(ctx, inner_l_kvs, inner_r_kvs)
- }
- (_, _) => {
- Err(TypeError::new(ctx, FieldCollision(k.clone())))
- }
- }
- };
-
- let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
- |l| Ok(l.to_type()),
- |r| Ok(r.to_type()),
- |k: &Label, l: &TypedThunk, r: &TypedThunk| {
- combine(k, l, r)
- },
- &kts_l,
- &kts_r,
- );
-
- Ok(tck_record_type(
- ctx,
- kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))),
- )?
- .into_type())
- };
-
- let l_type = l.get_type()?;
- let l_kind = l_type.get_type()?;
- let r_type = r.get_type()?;
- let r_kind = r_type.get_type()?;
-
- // Check the equality of kinds.
- // This is to disallow expression such as:
- // "{ x = Text } // { y = 1 }"
- if l_kind != r_kind {
- return Err(mkerr(RecordMismatch(l.clone(), r.clone())));
- }
-
- // Extract the LHS record type
- let kts_x = match l_type.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(MustCombineRecord(l.clone()))),
- };
-
- // Extract the RHS record type
- let kts_y = match r_type.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(MustCombineRecord(r.clone()))),
- };
-
- combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r))
+ RetTypeOnly(tck_record_type(
+ ctx,
+ kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+ )?)
}
+ BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+ ctx,
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ l.get_type()?.into_owned(),
+ r.get_type()?.into_owned(),
+ ),
+ )?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
- // A recursive function to dig down into
- // records of records when merging.
- fn combine_record_types(
- ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypedThunk>,
- kts_r: HashMap<Label, TypedThunk>,
- ) -> Result<Typed, TypeError> {
- use crate::phase::normalize::intersection_with_key;
-
- // If the Label exists for both records and Type for the values
- // are records themselves, then we hit the recursive case.
- // Otherwise we have a field collision.
- let combine = |k: &Label,
- kts_l_inner: &TypedThunk,
- kts_r_inner: &TypedThunk|
- -> Result<Typed, TypeError> {
- match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
- (
- Value::RecordType(kvs_l_inner),
- Value::RecordType(kvs_r_inner),
- ) => {
- combine_record_types(ctx, kvs_l_inner, kvs_r_inner)
- }
- (_, _) => {
- Err(TypeError::new(ctx, FieldCollision(k.clone())))
- }
- }
- };
-
- let kts = intersection_with_key(
- |k: &Label, l: &TypedThunk, r: &TypedThunk| {
- combine(k, l, r)
- },
- &kts_l,
- &kts_r,
- );
-
- Ok(tck_record_type(
- ctx,
- kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))),
- )?
- .into_type())
- };
+ use crate::phase::normalize::intersection_with_key;
// Extract the Const of the LHS
- let k_l = match l.get_type()?.to_value() {
- Value::Const(k) => k,
+ let k_l = match l.get_type()?.as_const() {
+ Some(k) => k,
_ => {
- return Err(mkerr(RecordTypeMergeRequiresRecordType(
- l.clone(),
- )))
+ return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
}
};
// Extract the Const of the RHS
- let k_r = match r.get_type()?.to_value() {
- Value::Const(k) => k,
+ let k_r = match r.get_type()?.as_const() {
+ Some(k) => k,
_ => {
- return Err(mkerr(RecordTypeMergeRequiresRecordType(
- r.clone(),
- )))
+ return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
}
};
- // Const values must match for the Records
- let k = if k_l == k_r {
- k_l
- } else {
- return Err(mkerr(RecordTypeMismatch(
- Typed::from_const(k_l),
- Typed::from_const(k_r),
- l.clone(),
- r.clone(),
- )));
- };
+ let k = max(k_l, k_r);
// Extract the LHS record type
- let kts_x = match l.to_value() {
- Value::RecordType(kts) => kts,
+ let borrow_l = l.as_whnf();
+ let kts_x = match &*borrow_l {
+ ValueF::RecordType(kts) => kts,
_ => {
- return Err(mkerr(RecordTypeMergeRequiresRecordType(
- l.clone(),
- )))
+ return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
}
};
// Extract the RHS record type
- let kts_y = match r.to_value() {
- Value::RecordType(kts) => kts,
+ let borrow_r = r.as_whnf();
+ let kts_y = match &*borrow_r {
+ ValueF::RecordType(kts) => kts,
_ => {
- return Err(mkerr(RecordTypeMergeRequiresRecordType(
- r.clone(),
- )))
+ return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
}
};
// Ensure that the records combine without a type error
- // and if not output the final Const value.
- combine_record_types(ctx, kts_x, kts_y)
- .and(Ok(RetTypeOnly(Typed::from_const(k))))
+ let kts = intersection_with_key(
+ // If the Label exists for both records, then we hit the recursive case.
+ |_: &Label, l: &Value, r: &Value| {
+ type_last_layer(
+ ctx,
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ ),
+ )
+ },
+ kts_x,
+ kts_y,
+ );
+ tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+
+ RetTypeOnly(Value::from_const(k))
}
BinOp(o @ ListAppend, l, r) => {
- match l.get_type()?.to_value() {
- Value::AppliedBuiltin(List, _) => {}
- _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
+ match &*l.get_type()?.as_whnf() {
+ ValueF::AppliedBuiltin(List, _) => {}
+ _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
}
if l.get_type()? != r.get_type()? {
- return Err(mkerr(BinOpTypeMismatch(*o, r.clone())));
+ return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
- Ok(RetTypeOnly(l.get_type()?.into_owned()))
+ RetTypeOnly(l.get_type()?.into_owned())
}
BinOp(Equivalence, l, r) => {
if l.get_type()?.get_type()?.as_const() != Some(Type) {
- return Err(mkerr(EquivalenceArgumentMustBeTerm(
- true,
- l.clone(),
- )));
+ return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone()));
}
if r.get_type()?.get_type()?.as_const() != Some(Type) {
- return Err(mkerr(EquivalenceArgumentMustBeTerm(
- false,
- r.clone(),
- )));
+ return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone()));
}
if l.get_type()? != r.get_type()? {
- return Err(mkerr(EquivalenceTypeMismatch(
- r.clone(),
- l.clone(),
- )));
+ return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- Ok(RetTypeOnly(Typed::from_const(Type).into_type()))
+ RetTypeOnly(Value::from_const(Type))
}
BinOp(o, l, r) => {
let t = builtin_to_type(match o {
@@ -884,140 +682,136 @@ fn type_last_layer(
})?;
if l.get_type()?.as_ref() != &t {
- return Err(mkerr(BinOpTypeMismatch(*o, l.clone())));
+ return mkerr(BinOpTypeMismatch(*o, l.clone()));
}
if r.get_type()?.as_ref() != &t {
- return Err(mkerr(BinOpTypeMismatch(*o, r.clone())));
+ return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
- Ok(RetTypeOnly(t))
+ RetTypeOnly(t)
}
Merge(record, union, type_annot) => {
- let handlers = match record.get_type()?.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))),
+ let record_type = record.get_type()?;
+ let record_borrow = record_type.as_whnf();
+ let handlers = match &*record_borrow {
+ ValueF::RecordType(kts) => kts,
+ _ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
};
- let variants = match union.get_type()?.to_value() {
- Value::UnionType(kts) => kts,
- _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))),
+ let union_type = union.get_type()?;
+ let union_borrow = union_type.as_whnf();
+ let variants = match &*union_borrow {
+ ValueF::UnionType(kts) => kts,
+ _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
};
let mut inferred_type = None;
- for (x, handler) in handlers.iter() {
- let handler_return_type = match variants.get(x) {
- // Union alternative with type
- Some(Some(variant_type)) => {
- let variant_type = variant_type.to_type();
- let handler_type = handler.to_type();
- let (x, tx, tb) = match &handler_type.to_value() {
- Value::Pi(x, tx, tb) => {
- (x.clone(), tx.to_type(), tb.to_type())
+ 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 (x, tx, tb) = match &*handler_type_borrow {
+ ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ _ => {
+ return mkerr(NotAFunction(
+ handler_type.clone(),
+ ))
+ }
+ };
+
+ if variant_type != tx {
+ return mkerr(TypeMismatch(
+ handler_type.clone(),
+ tx.clone(),
+ variant_type.clone(),
+ ));
}
- _ => return Err(mkerr(NotAFunction(handler_type))),
- };
-
- if &variant_type != &tx {
- return Err(mkerr(TypeMismatch(
- handler_type,
- tx.to_normalized(),
- variant_type,
- )));
- }
- // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
- match tb.over_binder(x) {
- Some(x) => x,
- None => {
- return Err(mkerr(
+ // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+ match tb.over_binder(x) {
+ Some(x) => x,
+ None => return mkerr(
MergeHandlerReturnTypeMustNotBeDependent,
- ))
+ ),
}
}
- }
- // Union alternative without type
- Some(None) => handler.to_type(),
- None => {
- return Err(mkerr(MergeHandlerMissingVariant(
- x.clone(),
- )))
- }
- };
+ // Union alternative without type
+ Some(None) => handler_type.clone(),
+ None => {
+ return mkerr(MergeHandlerMissingVariant(x.clone()))
+ }
+ };
match &inferred_type {
None => inferred_type = Some(handler_return_type),
Some(t) => {
if t != &handler_return_type {
- return Err(mkerr(MergeHandlerTypeMismatch));
+ return mkerr(MergeHandlerTypeMismatch);
}
}
}
}
for x in variants.keys() {
if !handlers.contains_key(x) {
- return Err(mkerr(MergeVariantMissingHandler(x.clone())));
+ return mkerr(MergeVariantMissingHandler(x.clone()));
}
}
match (inferred_type, type_annot) {
(Some(ref t1), Some(t2)) => {
- let t2 = t2.to_type();
- if t1 != &t2 {
- return Err(mkerr(MergeAnnotMismatch));
+ if t1 != t2 {
+ return mkerr(MergeAnnotMismatch);
}
- Ok(RetTypeOnly(t2))
+ RetTypeOnly(t2.clone())
}
- (Some(t), None) => Ok(RetTypeOnly(t)),
- (None, Some(t)) => Ok(RetTypeOnly(t.to_type())),
- (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)),
+ (Some(t), None) => RetTypeOnly(t),
+ (None, Some(t)) => RetTypeOnly(t.clone()),
+ (None, None) => return mkerr(MergeEmptyNeedsAnnotation),
}
}
Projection(record, labels) => {
- let trecord = record.get_type()?;
- let kts = match trecord.to_value() {
- Value::RecordType(kts) => kts,
- _ => return Err(mkerr(ProjectionMustBeRecord)),
+ let record_type = record.get_type()?;
+ let record_borrow = record_type.as_whnf();
+ let kts = match &*record_borrow {
+ ValueF::RecordType(kts) => kts,
+ _ => return mkerr(ProjectionMustBeRecord),
};
let mut new_kts = HashMap::new();
for l in labels {
match kts.get(l) {
- None => return Err(mkerr(ProjectionMissingEntry)),
+ None => return mkerr(ProjectionMissingEntry),
Some(t) => new_kts.insert(l.clone(), t.clone()),
};
}
- Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
- Value::RecordType(new_kts).into_thunk(),
- trecord.get_type()?.into_owned(),
- )
- .to_type(),
+ RetTypeOnly(Value::from_valuef_and_type(
+ ValueF::RecordType(new_kts),
+ record_type.get_type()?.into_owned(),
))
}
- }
+ };
+
+ Ok(match ret {
+ RetTypeOnly(typ) => {
+ Value::from_valuef_and_type(ValueF::PartialExpr(e), typ)
+ }
+ RetWhole(v) => v,
+ })
}
-/// `typeOf` is the same as `type_with` with an empty context, meaning that the
+/// `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.
-fn type_of(e: SubExpr<Normalized>) -> Result<Typed, TypeError> {
- let ctx = TypecheckContext::new();
- let e = type_with(&ctx, e)?;
- // Ensure `e` has a type (i.e. `e` is not `Sort`)
- e.get_type()?;
- Ok(e)
+pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> {
+ type_with(&TypecheckContext::new(), e)
}
-pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
- type_of(e.0)
-}
-
-pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
- let expr: SubExpr<_> = e.0;
- let ty: SubExpr<_> = ty.to_expr();
- type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
-}
-pub(crate) fn skip_typecheck(e: Resolved) -> Typed {
- Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0))
+pub(crate) fn typecheck_with(
+ expr: SubExpr<Normalized>,
+ ty: SubExpr<Normalized>,
+) -> Result<Value, TypeError> {
+ typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index d269523..be4805d 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -169,7 +169,7 @@ pub fn run_test(
let expected_file_path = base_path + "B.dhall";
let expected = parse_file_str(&expected_file_path)?
.resolve()?
- .skip_typecheck()
+ .typecheck()?
.normalize();
match feature {
@@ -177,24 +177,23 @@ pub fn run_test(
unreachable!()
}
Import => {
- let expr = expr.skip_typecheck().normalize();
+ let expr = expr.typecheck()?.normalize();
assert_eq_display!(expr, expected);
}
Typecheck => {
- expr.typecheck_with(&expected.to_type())?;
+ expr.typecheck_with(&expected.into_typed())?.get_type()?;
}
TypeInference => {
let expr = expr.typecheck()?;
- let ty = expr.get_type()?.into_owned();
- assert_eq_display!(ty.to_normalized(), expected);
+ let ty = expr.get_type()?.into_owned().normalize();
+ assert_eq_display!(ty, expected);
}
Normalization => {
- let expr = expr.skip_typecheck().normalize();
+ let expr = expr.typecheck()?.normalize();
assert_eq_display!(expr, expected);
}
AlphaNormalization => {
- let expr =
- expr.skip_typecheck().normalize().to_expr_alpha();
+ let expr = expr.typecheck()?.normalize().to_expr_alpha();
assert_eq_display!(expr, expected.to_expr());
}
}
@@ -226,10 +225,15 @@ pub fn run_test(
}
Normalization | AlphaNormalization => unreachable!(),
Typecheck | TypeInference => {
- parse_file_str(&file_path)?
- .skip_resolve()?
- .typecheck()
- .unwrap_err();
+ let res =
+ parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+ match res {
+ Err(_) => {}
+ // If e did typecheck, check that it doesn't have a type
+ Ok(e) => {
+ e.get_type().unwrap_err();
+ }
+ }
}
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 16:14:08 +0000