summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase/normalize.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/phase/normalize.rs')
-rw-r--r--dhall/src/semantics/phase/normalize.rs794
1 files changed, 794 insertions, 0 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
new file mode 100644
index 0000000..3ed53f4
--- /dev/null
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -0,0 +1,794 @@
+use std::collections::HashMap;
+
+use crate::syntax::Const::Type;
+use crate::syntax::{
+ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
+ NaiveDouble,
+};
+
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
+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, $($ty:tt)*)) => {{
+ let var = crate::core::var::AlphaVar::from_var_and_alpha(
+ Label::from(stringify!($var)).into(),
+ $n
+ );
+ 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)*) -> $($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) => {
+ Value::from_builtin(Builtin::Natural)
+ };
+ (List $($rest:tt)*) => {
+ 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(
+ crate::syntax::BinOp::NaturalPlus,
+ make_closure!($($rest)*),
+ Value::from_valuef_and_type(
+ ValueF::NaturalLit(1),
+ make_closure!(Natural)
+ ),
+ )).into_value_with_type(
+ make_closure!(Natural)
+ )
+ };
+ ([ $($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(
+ crate::syntax::BinOp::ListAppend,
+ 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>,
+ ty: &Value,
+) -> ValueF {
+ use crate::syntax::Builtin::*;
+ use ValueF::*;
+
+ // 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]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (NaturalIsZero, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalEven, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalOdd, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalToInteger, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalShow, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+ (NaturalLit(a), NaturalLit(b)) => {
+ Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
+ }
+ (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)
+ };
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerToDouble, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (DoubleShow, [n]) => match &*n.as_whnf() {
+ DoubleLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (TextShow, [v]) => match &*v.as_whnf() {
+ TextLit(elts) => {
+ match elts.as_slice() {
+ // Empty string literal.
+ [] => {
+ // Printing InterpolatedText takes care of all the escaping
+ let txt: InterpolatedText<Normalized> =
+ std::iter::empty().collect();
+ let s = txt.to_string();
+ 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.
+ [InterpolatedTextContents::Text(s)] => {
+ // Printing InterpolatedText takes care of all the escaping
+ let txt: InterpolatedText<Normalized> =
+ std::iter::once(InterpolatedTextContents::Text(
+ s.clone(),
+ ))
+ .collect();
+ let s = txt.to_string();
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
+ }
+ _ => Ret::DoneAsIs,
+ }
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (ListLength, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ _ => Ret::DoneAsIs,
+ },
+ (ListHead, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => {
+ Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (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]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
+ NEListLit(xs) => {
+ Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (ListIndexed, [_, l]) => {
+ let l_whnf = l.as_whnf();
+ match &*l_whnf {
+ EmptyListLit(_) | NEListLit(_) => {
+ // Extract the type of the list elements
+ let t = match &*l_whnf {
+ EmptyListLit(t) => t.clone(),
+ NEListLit(xs) => xs[0].get_type_not_sort(),
+ _ => unreachable!(),
+ };
+
+ // Construct the returned record type: { index: Natural, value: t }
+ let mut kts = HashMap::new();
+ kts.insert("index".into(), Value::from_builtin(Natural));
+ kts.insert("value".into(), t.clone());
+ let t = Value::from_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,
+ }
+ }
+ (ListBuild, [t, f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(ListFold, args) => {
+ if args.len() >= 2 {
+ Ret::Value(args[1].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => {
+ 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, #t2) ] # var(xs, 0, List #t2)
+ )
+ })
+ .app(
+ EmptyListLit(t.clone())
+ .into_value_with_type(list_t),
+ ),
+ )
+ }
+ },
+ (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
+ NEListLit(xs) => {
+ let mut v = nil.clone();
+ for x in xs.iter().cloned().rev() {
+ v = cons.app(x).app(v);
+ }
+ Ret::ValueWithRemainingArgs(r, v)
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (OptionalBuild, [t, f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(OptionalFold, args) => {
+ if args.len() >= 2 {
+ Ret::Value(args[1].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => {
+ 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(_) => {
+ Ret::ValueWithRemainingArgs(r, nothing.clone())
+ }
+ NEOptionalLit(x) => {
+ Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalBuild, [f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(NaturalFold, args) => {
+ if !args.is_empty() {
+ Ret::Value(args[0].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => 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) => Ret::ValueWithRemainingArgs(r, zero.clone()),
+ NaturalLit(n) => {
+ let fold = Value::from_builtin(NaturalFold)
+ .app(
+ NaturalLit(n - 1)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ )
+ .app(t.clone())
+ .app(succ.clone())
+ .app(zero.clone());
+ Ret::ValueWithRemainingArgs(r, succ.app(fold))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ _ => Ret::DoneAsIs,
+ };
+ match ret {
+ Ret::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(x);
+ }
+ v.to_whnf_check_type(ty)
+ }
+ Ret::DoneAsIs => AppliedBuiltin(b, args),
+ }
+}
+
+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_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, ty)
+ }
+ ValueF::UnionConstructor(l, kts) => {
+ ValueF::UnionLit(l.clone(), a, kts.clone())
+ }
+ _ => {
+ drop(f_borrow);
+ ValueF::PartialExpr(ExprF::App(f, a))
+ }
+ }
+}
+
+pub(crate) fn squash_textlit(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
+ use std::mem::replace;
+ use InterpolatedTextContents::{Expr, Text};
+
+ fn inner(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ crnt_str: &mut String,
+ 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_whnf();
+ match &*e_borrow {
+ ValueF::TextLit(elts2) => {
+ inner(elts2.iter().cloned(), crnt_str, ret)
+ }
+ _ => {
+ drop(e_borrow);
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(crnt_str, String::new())))
+ }
+ ret.push(Expr(e.clone()))
+ }
+ }
+ }
+ }
+ }
+ }
+
+ let mut crnt_str = String::new();
+ let mut ret = Vec::new();
+ inner(elts, &mut crnt_str, &mut ret);
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(&mut crnt_str, String::new())))
+ }
+ ret
+}
+
+pub(crate) fn merge_maps<K, V, F, Err>(
+ map1: &HashMap<K, V>,
+ map2: &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(x, v1, v2)?
+ } else {
+ v2.clone()
+ };
+ kvs.insert(x.clone(), newv);
+ }
+ for (x, v1) in map1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v1.clone());
+ }
+ Ok(kvs)
+}
+
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprF<Value, Normalized>),
+}
+
+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,
+ RightBiasedRecordMerge, TextAppend,
+ };
+ use ValueF::{
+ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
+ TextLit,
+ };
+ let x_borrow = x.as_whnf();
+ let y_borrow = y.as_whnf();
+ Some(match (o, &*x_borrow, &*y_borrow) {
+ (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::ValueF(NaturalLit(x + y))
+ }
+ (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::ValueF(NaturalLit(x * y))
+ }
+
+ (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::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::ValueF(TextLit(squash_textlit(
+ x.iter().cloned().chain(once(y)),
+ )))
+ }
+ (TextAppend, _, TextLit(y)) => {
+ use std::iter::once;
+ let x = InterpolatedTextContents::Expr(x.clone());
+ Ret::ValueF(TextLit(squash_textlit(
+ once(x).chain(y.iter().cloned()),
+ )))
+ }
+
+ (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let mut kvs = kvs2.clone();
+ for (x, v) in kvs1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v.clone());
+ }
+ Ret::ValueF(RecordLit(kvs))
+ }
+
+ (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let ty_borrow = ty.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, _, _) | (Equivalence, _, _) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
+
+ _ => return None,
+ })
+}
+
+pub(crate) fn normalize_one_layer(
+ expr: ExprF<Value, Normalized>,
+ ty: &Value,
+) -> ValueF {
+ use ValueF::{
+ 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"
+ ),
+ // 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::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)),
+ 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_whnf();
+ match &*t_borrow {
+ AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
+ Ret::ValueF(EmptyListLit(args[0].clone()))
+ }
+ _ => {
+ drop(t_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::NEListLit(elts) => {
+ Ret::ValueF(NEListLit(elts.into_iter().collect()))
+ }
+ ExprF::RecordLit(kvs) => {
+ Ret::ValueF(RecordLit(kvs.into_iter().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::Value(th.clone())
+ } else {
+ Ret::ValueF(TextLit(elts))
+ }
+ }
+ ExprF::BoolIf(ref b, ref e1, ref e2) => {
+ let b_borrow = b.as_whnf();
+ match &*b_borrow {
+ BoolLit(true) => Ret::ValueRef(e1),
+ BoolLit(false) => Ret::ValueRef(e2),
+ _ => {
+ let e1_borrow = e1.as_whnf();
+ let e2_borrow = e2.as_whnf();
+ match (&*e1_borrow, &*e2_borrow) {
+ // Simplify `if b then True else False`
+ (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ _ if e1 == e2 => Ret::ValueRef(e1),
+ _ => {
+ drop(b_borrow);
+ drop(e1_borrow);
+ drop(e2_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ }
+ }
+ ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ Some(ret) => ret,
+ None => Ret::Expr(expr),
+ },
+
+ ExprF::Projection(_, ref ls) if ls.is_empty() => {
+ Ret::ValueF(RecordLit(HashMap::new()))
+ }
+ ExprF::Projection(ref v, ref ls) => {
+ let v_borrow = v.as_whnf();
+ match &*v_borrow {
+ RecordLit(kvs) => Ret::ValueF(RecordLit(
+ ls.iter()
+ .filter_map(|l| {
+ kvs.get(l).map(|x| (l.clone(), x.clone()))
+ })
+ .collect(),
+ )),
+ _ => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::Field(ref v, ref l) => {
+ let v_borrow = v.as_whnf();
+ match &*v_borrow {
+ RecordLit(kvs) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ UnionType(kts) => {
+ Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
+ }
+ _ => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::ProjectionByExpr(_, _) => {
+ unimplemented!("selection by expression")
+ }
+
+ ExprF::Merge(ref handlers, ref variant, _) => {
+ 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::Value(h.clone()),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ _ => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::ToMap(_, _) => unimplemented!("toMap"),
+ };
+
+ match ret {
+ Ret::ValueF(v) => v,
+ 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, ty: &Value) -> ValueF {
+ match v {
+ 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()))
+ }
+ // All other cases are already in WHNF
+ v => v,
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 10:14:22 +0000