summaryrefslogtreecommitdiff
path: root/dhall/src/phase/normalize.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase/normalize.rs')
-rw-r--r--dhall/src/phase/normalize.rs592
1 files changed, 297 insertions, 295 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a379a4b..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,5 +1,6 @@
use std::collections::HashMap;
+use dhall_syntax::Const::Type;
use dhall_syntax::{
BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
NaiveDouble,
@@ -7,42 +8,43 @@ use dhall_syntax::{
use crate::core::value::Value;
use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
-
-pub(crate) type OutputSubExpr = NormalizedSubExpr;
+use crate::core::var::{AlphaLabel, Shift, Subst};
+use crate::phase::Normalized;
// Ad-hoc macro to help construct closures
macro_rules! make_closure {
(#$var:ident) => { $var.clone() };
- (var($var:ident, $n:expr)) => {{
+ (var($var:ident, $n:expr, $($ty:tt)*)) => {{
let var = crate::core::var::AlphaVar::from_var_and_alpha(
Label::from(stringify!($var)).into(),
$n
);
- ValueF::Var(var).into_value_untyped()
+ ValueF::Var(var)
+ .into_value_with_type(make_closure!($($ty)*))
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
- (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
- ValueF::Lam(
- Label::from(stringify!($var)).into(),
- make_closure!($($ty)*),
- make_closure!($($rest)*),
- ).into_value_untyped()
- };
+ (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+ let var: AlphaLabel = Label::from(stringify!($var)).into();
+ let ty = make_closure!($($ty)*);
+ let body = make_closure!($($body)*);
+ let body_ty = body.get_type_not_sort();
+ let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+ .into_value_with_type(Value::from_const(Type));
+ ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+ }};
(Natural) => {
- ValueF::from_builtin(Builtin::Natural)
- .into_value_simple_type()
+ Value::from_builtin(Builtin::Natural)
};
(List $($rest:tt)*) => {
- ValueF::from_builtin(Builtin::List)
- .app_value(make_closure!($($rest)*))
- .into_value_simple_type()
- };
- (Some($($rest:tt)*)) => {
- ValueF::NEOptionalLit(make_closure!($($rest)*))
- .into_value_untyped()
+ Value::from_builtin(Builtin::List)
+ .app(make_closure!($($rest)*))
};
+ (Some($($rest:tt)*)) => {{
+ let v = make_closure!($($rest)*);
+ let v_type = v.get_type_not_sort();
+ let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
+ ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+ }};
(1 + $($rest:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::NaturalPlus,
@@ -55,81 +57,99 @@ macro_rules! make_closure {
make_closure!(Natural)
)
};
- ([ $($head:tt)* ] # $($tail:tt)*) => {
+ ([ $($head:tt)* ] # $($tail:tt)*) => {{
+ let head = make_closure!($($head)*);
+ let tail = make_closure!($($tail)*);
+ let list_type = tail.get_type_not_sort();
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::ListAppend,
- ValueF::NEListLit(vec![make_closure!($($head)*)])
- .into_value_untyped(),
- make_closure!($($tail)*),
- )).into_value_untyped()
- };
+ ValueF::NEListLit(vec![head])
+ .into_value_with_type(list_type.clone()),
+ tail,
+ )).into_value_with_type(list_type)
+ }};
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
+pub(crate) fn apply_builtin(
+ b: Builtin,
+ args: Vec<Value>,
+ ty: &Value,
+) -> ValueF {
use dhall_syntax::Builtin::*;
use ValueF::*;
- // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
+ // Small helper enum
+ enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ // For applications that can return a function, it's important to keep the remaining
+ // arguments to apply them to the resulting function.
+ ValueWithRemainingArgs(&'a [Value], Value),
+ DoneAsIs,
+ }
+
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
- (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
- _ => Err(()),
+ (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (NaturalIsZero, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalEven, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
- _ => Err(()),
+ (NaturalEven, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
- _ => Err(()),
+ (NaturalOdd, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ _ => Ret::DoneAsIs,
},
- (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
- _ => Err(()),
+ (NaturalToInteger, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ _ => Ret::DoneAsIs,
},
- (NaturalShow, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
- )),
- _ => Err(()),
+ (NaturalShow, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
},
- (NaturalSubtract, [a, b, r..]) => {
- match (&*a.as_whnf(), &*b.as_whnf()) {
- (NaturalLit(a), NaturalLit(b)) => {
- Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
- }
- (NaturalLit(0), b) => Ok((r, b.clone())),
- (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
- _ if a == b => Ok((r, NaturalLit(0))),
- _ => Err(()),
+ (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+ (NaturalLit(a), NaturalLit(b)) => {
+ Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
}
- }
- (IntegerShow, [n, r..]) => match &*n.as_whnf() {
+ (NaturalLit(0), _) => Ret::Value(b.clone()),
+ (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ _ if a == b => Ret::ValueF(NaturalLit(0)),
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerShow, [n]) => match &*n.as_whnf() {
IntegerLit(n) => {
let s = if *n < 0 {
n.to_string()
} else {
format!("+{}", n)
};
- Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)])))
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
- IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
- _ => Err(()),
+ (IntegerToDouble, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+ }
+ _ => Ret::DoneAsIs,
},
- (DoubleShow, [n, r..]) => match &*n.as_whnf() {
- DoubleLit(n) => Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
- )),
- _ => Err(()),
+ (DoubleShow, [n]) => match &*n.as_whnf() {
+ DoubleLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
},
- (TextShow, [v, r..]) => match &*v.as_whnf() {
+ (TextShow, [v]) => match &*v.as_whnf() {
TextLit(elts) => {
match elts.as_slice() {
// Empty string literal.
@@ -138,10 +158,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
let txt: InterpolatedText<Normalized> =
std::iter::empty().collect();
let s = txt.to_string();
- Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
- ))
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
}
// If there are no interpolations (invariants ensure that when there are no
// interpolations, there is a single Text item) in the literal.
@@ -153,221 +172,238 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
))
.collect();
let s = txt.to_string();
- Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
- ))
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
}
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListLength, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, NaturalLit(0))),
- NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
- _ => Err(()),
+ (ListLength, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ _ => Ret::DoneAsIs,
},
- (ListHead, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
+ (ListHead, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
+ Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListLast, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
- }
- _ => Err(()),
+ (ListLast, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+ xs.iter().rev().next().unwrap().clone(),
+ )),
+ _ => Ret::DoneAsIs,
},
- (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
+ (ListReverse, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
+ Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(t) => {
- let mut kts = HashMap::new();
- kts.insert(
- "index".into(),
- Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
- );
- kts.insert("value".into(), t.clone());
- Ok((
- r,
- EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
- ))
- }
- NEListLit(xs) => {
- let xs = xs
- .iter()
- .enumerate()
- .map(|(i, e)| {
- let i = NaturalLit(i);
- let mut kvs = HashMap::new();
- kvs.insert(
- "index".into(),
- Value::from_valuef_untyped(i),
- );
- kvs.insert("value".into(), e.clone());
- Value::from_valuef_untyped(RecordLit(kvs))
- })
- .collect();
- Ok((r, NEListLit(xs)))
+ (ListIndexed, [_, l]) => {
+ let l_whnf = l.as_whnf();
+ match &*l_whnf {
+ EmptyListLit(_) | NEListLit(_) => {
+ // Extract the type of the list elements
+ let t = match &*l_whnf {
+ EmptyListLit(t) => t.clone(),
+ NEListLit(xs) => xs[0].get_type_not_sort(),
+ _ => unreachable!(),
+ };
+
+ // Construct the returned record type: { index: Natural, value: t }
+ let mut kts = HashMap::new();
+ kts.insert("index".into(), Value::from_builtin(Natural));
+ kts.insert("value".into(), t.clone());
+ let t = Value::from_valuef_and_type(
+ RecordType(kts),
+ Value::from_const(Type),
+ );
+
+ // Construct the new list, with added indices
+ let list = match &*l_whnf {
+ EmptyListLit(_) => EmptyListLit(t),
+ NEListLit(xs) => NEListLit(
+ xs.iter()
+ .enumerate()
+ .map(|(i, e)| {
+ let mut kvs = HashMap::new();
+ kvs.insert(
+ "index".into(),
+ Value::from_valuef_and_type(
+ NaturalLit(i),
+ Value::from_builtin(
+ Builtin::Natural,
+ ),
+ ),
+ );
+ kvs.insert("value".into(), e.clone());
+ Value::from_valuef_and_type(
+ RecordLit(kvs),
+ t.clone(),
+ )
+ })
+ .collect(),
+ ),
+ _ => unreachable!(),
+ };
+ Ret::ValueF(list)
+ }
+ _ => Ret::DoneAsIs,
}
- _ => Err(()),
- },
- (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
+ }
+ (ListBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ret::Value(args[1].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
_ => {
- let list_t = ValueF::from_builtin(List)
- .app_value(t.clone())
- .into_value_simple_type();
- Ok((
- r,
- f.app_value(list_t.clone())
- .app_value({
- // Move `t` under new `x` variable
+ let list_t = Value::from_builtin(List).app(t.clone());
+ Ret::Value(
+ f.app(list_t.clone())
+ .app({
+ // Move `t` under new variables
let t1 = t.under_binder(Label::from("x"));
+ let t2 = t1.under_binder(Label::from("xs"));
make_closure!(
λ(x : #t) ->
λ(xs : List #t1) ->
- [ var(x, 1) ] # var(xs, 0)
+ [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
)
})
- .app_value(
+ .app(
EmptyListLit(t.clone())
.into_value_with_type(list_t),
),
- ))
+ )
}
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, nil.to_whnf())),
+ EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
NEListLit(xs) => {
let mut v = nil.clone();
- for x in xs.iter().rev() {
- v = cons
- .clone()
- .app_value(x.clone())
- .app_value(v)
- .into_value_untyped();
+ for x in xs.iter().cloned().rev() {
+ v = cons.app(x).app(v);
}
- Ok((r, v.to_whnf()))
+ Ret::ValueWithRemainingArgs(r, v)
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
+ (OptionalBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ret::Value(args[1].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
_ => {
- let optional_t = ValueF::from_builtin(Optional)
- .app_value(t.clone())
- .into_value_simple_type();
- Ok((
- r,
- f.app_value(optional_t.clone())
- .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
- .app_value(
+ let optional_t = Value::from_builtin(Optional).app(t.clone());
+ Ret::Value(
+ f.app(optional_t.clone())
+ .app({
+ let t1 = t.under_binder(Label::from("x"));
+ make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+ })
+ .app(
EmptyOptionalLit(t.clone())
.into_value_with_type(optional_t),
),
- ))
+ )
}
},
(OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
- EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
- NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
- _ => Err(()),
+ EmptyOptionalLit(_) => {
+ Ret::ValueWithRemainingArgs(r, nothing.clone())
+ }
+ NEOptionalLit(x) => {
+ Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+ }
+ _ => Ret::DoneAsIs,
},
- (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
+ (NaturalBuild, [f]) => match &*f.as_whnf() {
// fold/build fusion
ValueF::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
- Ok((r, args[0].to_whnf()))
+ Ret::Value(args[0].clone())
} else {
// Do we really need to handle this case ?
unimplemented!()
}
}
- _ => {
- let nat_type =
- ValueF::from_builtin(Natural).into_value_simple_type();
- Ok((
- r,
- f.app_value(nat_type.clone())
- .app_value(
- make_closure!(λ(x : Natural) -> 1 + var(x, 0)),
- )
- .app_value(
- NaturalLit(0).into_value_with_type(nat_type),
- ),
- ))
- }
+ _ => Ret::Value(
+ f.app(Value::from_builtin(Natural))
+ .app(make_closure!(
+ λ(x : Natural) -> 1 + var(x, 0, Natural)
+ ))
+ .app(
+ NaturalLit(0)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ ),
+ ),
},
(NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
- NaturalLit(0) => Ok((r, zero.to_whnf())),
+ NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
NaturalLit(n) => {
- let fold = ValueF::from_builtin(NaturalFold)
- .app(NaturalLit(n - 1))
- .app_value(t.clone())
- .app_value(succ.clone())
- .app_value(zero.clone())
- .into_value_with_type(t.clone());
- Ok((r, succ.app_value(fold)))
+ let fold = Value::from_builtin(NaturalFold)
+ .app(
+ NaturalLit(n - 1)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ )
+ .app(t.clone())
+ .app(succ.clone())
+ .app(zero.clone());
+ Ret::ValueWithRemainingArgs(r, succ.app(fold))
}
- _ => Err(()),
+ _ => Ret::DoneAsIs,
},
- _ => Err(()),
+ _ => Ret::DoneAsIs,
};
match ret {
- Ok((unconsumed_args, mut v)) => {
+ Ret::ValueF(v) => v,
+ Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
let n_consumed_args = args.len() - unconsumed_args.len();
for x in args.into_iter().skip(n_consumed_args) {
- v = v.app_value(x);
+ v = v.app(x);
}
- v
+ v.to_whnf_check_type(ty)
}
- Err(()) => AppliedBuiltin(b, args),
+ Ret::DoneAsIs => AppliedBuiltin(b, args),
}
}
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
- let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+ ValueF::Lam(x, _, e) => {
+ e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+ }
ValueF::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
- apply_builtin(*b, args)
+ apply_builtin(*b, args, ty)
}
ValueF::UnionConstructor(l, kts) => {
ValueF::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
- fallback(f, a)
+ ValueF::PartialExpr(ExprF::App(f, a))
}
}
}
@@ -414,53 +450,20 @@ pub(crate) fn squash_textlit(
ret
}
-/// Performs an intersection of two HashMaps.
-///
-/// # Arguments
-///
-/// * `f` - Will compute the final value from the intersecting
-/// key and the values from both maps.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `f` function.
-///
-/// The final map will contain the shared keys from the
-/// two input maps with the final computed value from `f`.
-pub(crate) fn intersection_with_key<K, T, U, V>(
- mut f: impl FnMut(&K, &T, &U) -> V,
- map1: &HashMap<K, T>,
- map2: &HashMap<K, U>,
-) -> HashMap<K, V>
-where
- K: std::hash::Hash + Eq + Clone,
-{
- let mut kvs = HashMap::new();
-
- for (k, t) in map1 {
- // Only insert in the final map if the key exists in both
- if let Some(u) = map2.get(k) {
- kvs.insert(k.clone(), f(k, t, u));
- }
- }
-
- kvs
-}
-
-pub(crate) fn merge_maps<K, V>(
+pub(crate) fn merge_maps<K, V, F, Err>(
map1: &HashMap<K, V>,
map2: &HashMap<K, V>,
- mut f: impl FnMut(&V, &V) -> V,
-) -> HashMap<K, V>
+ mut f: F,
+) -> Result<HashMap<K, V>, Err>
where
+ F: FnMut(&K, &V, &V) -> Result<V, Err>,
K: std::hash::Hash + Eq + Clone,
V: Clone,
{
let mut kvs = HashMap::new();
for (x, v2) in map2 {
let newv = if let Some(v1) = map1.get(x) {
- f(v1, v2)
+ f(x, v1, v2)?
} else {
v2.clone()
};
@@ -470,7 +473,7 @@ where
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v1.clone());
}
- kvs
+ Ok(kvs)
}
// Small helper enum to avoid repetition
@@ -481,7 +484,12 @@ enum Ret<'a> {
Expr(ExprF<Value, Normalized>),
}
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(
+ o: BinOp,
+ x: &'a Value,
+ y: &'a Value,
+ ty: &Value,
+) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -574,62 +582,62 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- )))
- });
+ let ty_borrow = ty.as_whnf();
+ let kts = match &*ty_borrow {
+ RecordType(kts) => kts,
+ _ => unreachable!("Internal type error"),
+ };
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+ Ok(Value::from_valuef_and_type(
+ ValueF::PartialExpr(ExprF::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ )),
+ kts.get(k).expect("Internal type error").clone(),
+ ))
+ })?;
Ret::ValueF(RecordLit(kvs))
}
- (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
- }
- (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
- }
- (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
- RecursiveRecordTypeMerge,
- v1.clone(),
- v2.clone(),
- )))
- });
- Ret::ValueF(RecordType(kvs))
- }
-
- (Equivalence, _, _) => {
- Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+ (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
+ unreachable!("This case should have been handled in typecheck")
}
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(
+ expr: ExprF<Value, Normalized>,
+ ty: &Value,
+) -> ValueF {
use ValueF::{
- AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
- NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
- TextLit, UnionConstructor, UnionLit, UnionType,
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+ NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+ UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
ExprF::Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
- ExprF::Embed(_) => unreachable!(),
- ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => Ret::Value(x),
+ // Those cases have already been completely handled in the typechecking phase (using
+ // `RetWhole`), so they won't appear here.
+ ExprF::Lam(_, _, _)
+ | ExprF::Pi(_, _, _)
+ | ExprF::Let(_, _, _, _)
+ | ExprF::Embed(_)
+ | ExprF::Const(_)
+ | ExprF::Builtin(_)
+ | ExprF::Var(_)
+ | ExprF::Annot(_, _)
+ | ExprF::RecordType(_)
+ | ExprF::UnionType(_) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
ExprF::Assert(_) => Ret::Expr(expr),
- ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
- ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
- ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
- ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
- ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
- ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
+ ExprF::App(v, a) => Ret::Value(v.app(a)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -654,12 +662,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
ExprF::RecordLit(kvs) => {
Ret::ValueF(RecordLit(kvs.into_iter().collect()))
}
- ExprF::RecordType(kts) => {
- Ret::ValueF(RecordType(kts.into_iter().collect()))
- }
- ExprF::UnionType(kts) => {
- Ret::ValueF(UnionType(kts.into_iter().collect()))
- }
ExprF::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
@@ -692,7 +694,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
}
}
}
- ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
+ ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
@@ -749,7 +751,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::ValueF(h.app_value(v.clone())),
+ Some(h) => Ret::Value(h.app(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -767,17 +769,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
match ret {
Ret::ValueF(v) => v,
- Ret::Value(th) => th.as_whnf().clone(),
- Ret::ValueRef(th) => th.as_whnf().clone(),
+ Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::ValueRef(v) => v.to_whnf_check_type(ty),
Ret::Expr(expr) => ValueF::PartialExpr(expr),
}
}
/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
match v {
- ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
- ValueF::PartialExpr(e) => normalize_one_layer(e),
+ ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+ ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
ValueF::TextLit(elts) => {
ValueF::TextLit(squash_textlit(elts.into_iter()))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:57:41 +0000