diff options
Diffstat (limited to 'dhall/src/semantics/phase/normalize.rs')
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 373 |
1 files changed, 6 insertions, 367 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ce37993..2d4b4b3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,373 +1,12 @@ use std::collections::HashMap; -use std::convert::TryInto; -use crate::semantics::phase::typecheck::{ - builtin_to_value_env, const_to_value, rc, -}; use crate::semantics::phase::Normalized; -use crate::semantics::tck::typecheck::type_with; use crate::semantics::NzEnv; -use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; -use crate::syntax; -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, +use crate::semantics::{ + apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (var($var:ident)) => {{ - rc(ExprKind::Var(syntax::V( - Label::from(stringify!($var)).into(), - 0 - ))) - }}; - (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var = Label::from(stringify!($var)); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - rc(ExprKind::Lam(var, ty, body)) - }}; - (Type) => { - rc(ExprKind::Const(Type)) - }; - (Natural) => { - rc(ExprKind::Builtin(Builtin::Natural)) - }; - (List $($ty:tt)*) => {{ - let ty = make_closure!($($ty)*); - rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - ty - )) - }}; - (Some($($v:tt)*)) => { - rc(ExprKind::SomeLit( - make_closure!($($v)*) - )) - }; - (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( - syntax::BinOp::NaturalPlus, - make_closure!($($v)*), - rc(ExprKind::NaturalLit(1)) - )) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( - syntax::BinOp::ListAppend, - rc(ExprKind::NEListLit(vec![head])), - tail, - )) - }}; -} - -#[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec<Value>, - ty: &Value, - types: Vec<Value>, - env: NzEnv, -) -> ValueKind<Value> { - use syntax::Builtin::*; - use ValueKind::*; - - // Small helper enum - enum Ret<'a> { - ValueKind(ValueKind<Value>), - 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 make_closure = |e| { - type_with(&env.to_alpha_tyenv(), &e) - .unwrap() - .normalize_whnf(&env) - }; - - let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), - _ => Ret::DoneAsIs, - }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), - _ => Ret::DoneAsIs, - }, - (NaturalShow, [n]) => { - match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) - } - (NaturalLit(0), _) => Ret::Value(b.clone()), - (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), - _ if a == b => Ret::ValueKind(NaturalLit(0)), - _ => Ret::DoneAsIs, - }, - (IntegerShow, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) - } - _ => Ret::DoneAsIs, - }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) - } - _ => Ret::DoneAsIs, - }, - (IntegerNegate, [n]) => match &*n.as_whnf() { - IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), - _ => Ret::DoneAsIs, - }, - (IntegerClamp, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) - } - _ => Ret::DoneAsIs, - }, - (DoubleShow, [n]) => { - match &*n.as_whnf() { - DoubleLit(n) => Ret::ValueKind(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::ValueKind(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::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, - } - } - _ => Ret::DoneAsIs, - }, - (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), - NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), - _ => Ret::DoneAsIs, - }, - (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(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_kind_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_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), - ); - kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::ValueKind(list) - } - _ => Ret::DoneAsIs, - } - } - (ListBuild, [t, f]) => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - λ(as : List var(T)) -> - [ var(a) ] # var(as) - )) - .app(t.clone()), - ) - .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]) => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - Some(var(a)) - )) - .app(t.clone()), - ) - .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]) => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure(make_closure!( - λ(x : Natural) -> - 1 + var(x) - ))) - .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::ValueKind(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, types, env), - } -} +use crate::syntax; +use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents}; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> { let f_borrow = f.as_whnf(); @@ -643,8 +282,8 @@ pub(crate) fn normalize_one_layer( unreachable!("This case should have been handled in typecheck") } ExprKind::Annot(x, _) => Ret::Value(x), - ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), + ExprKind::Const(c) => Ret::Value(Value::from_const(c)), + ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), |