From 30bbf22fbfaead80322888eba7b7acdf908c3f3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 15:00:44 +0000 Subject: Rename ValueF to ValueKind --- dhall/src/semantics/phase/mod.rs | 14 +-- dhall/src/semantics/phase/normalize.rs | 216 ++++++++++++++++----------------- dhall/src/semantics/phase/typecheck.rs | 72 +++++------ 3 files changed, 151 insertions(+), 151 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 752c257..f27088c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -2,7 +2,7 @@ use std::fmt::Display; use std::path::Path; use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::syntax::binary; @@ -91,8 +91,8 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(Value::from_const(c)) } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(Value::from_valuef_and_type(v, t.into_value())) + pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { + Typed(Value::from_kind_and_type(v, t.into_value())) } pub(crate) fn from_value(th: Value) -> Self { Typed(th) @@ -148,8 +148,8 @@ impl Typed { pub fn make_record_type( kts: impl Iterator, ) -> Self { - Typed::from_valuef_and_type( - ValueF::RecordType( + Typed::from_kind_and_type( + ValueKind::RecordType( kts.map(|(k, t)| (k.into(), t.into_value())).collect(), ), Typed::const_type(), @@ -158,8 +158,8 @@ impl Typed { pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Typed::from_valuef_and_type( - ValueF::UnionType( + Typed::from_kind_and_type( + ValueKind::UnionType( kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) .collect(), ), diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 81c3ce1..157d1f3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; @@ -19,7 +19,7 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - ValueF::Var(var) + ValueKind::Var(var) .into_value_with_type(make_closure!($($ty)*)) }}; // Warning: assumes that $ty, as a dhall value, has type `Type` @@ -28,9 +28,9 @@ macro_rules! make_closure { 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) + let lam_ty = ValueKind::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) + ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty) }}; (Natural) => { Value::from_builtin(Builtin::Natural) @@ -43,14 +43,14 @@ macro_rules! make_closure { 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) + ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; (1 + $($rest:tt)*) => { - ValueF::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprF::BinOp( syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Value::from_valuef_and_type( - ValueF::NaturalLit(1), + Value::from_kind_and_type( + ValueKind::NaturalLit(1), make_closure!(Natural) ), )).into_value_with_type( @@ -61,9 +61,9 @@ macro_rules! make_closure { let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); let list_type = tail.get_type_not_sort(); - ValueF::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprF::BinOp( syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![head]) + ValueKind::NEListLit(vec![head]) .into_value_with_type(list_type.clone()), tail, )).into_value_with_type(list_type) @@ -75,13 +75,13 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, -) -> ValueF { +) -> ValueKind { use syntax::Builtin::*; - use ValueF::*; + use ValueKind::*; // Small helper enum enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), // For applications that can return a function, it's important to keep the remaining // arguments to apply them to the resulting function. @@ -90,38 +90,38 @@ pub(crate) fn apply_builtin( } let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())), + (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), _ => Ret::DoneAsIs, }, (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), _ => Ret::DoneAsIs, }, (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), _ => Ret::DoneAsIs, }, (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)), + NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), _ => Ret::DoneAsIs, }, - (NaturalShow, [n]) => match &*n.as_whnf() { - NaturalLit(n) => { - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - n.to_string(), - )])) + (NaturalShow, [n]) => { + match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueKind(TextLit(vec![ + InterpolatedTextContents::Text(n.to_string()), + ])), + _ => Ret::DoneAsIs, } - _ => 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 })) + Ret::ValueKind(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)), + (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), + _ if a == b => Ret::ValueKind(NaturalLit(0)), _ => Ret::DoneAsIs, }, (IntegerShow, [n]) => match &*n.as_whnf() { @@ -131,24 +131,24 @@ pub(crate) fn apply_builtin( } else { format!("+{}", n) }; - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)])) + Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) } _ => Ret::DoneAsIs, }, (IntegerToDouble, [n]) => match &*n.as_whnf() { IntegerLit(n) => { - Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))) + Ret::ValueKind(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(), - )])) + (DoubleShow, [n]) => { + match &*n.as_whnf() { + DoubleLit(n) => Ret::ValueKind(TextLit(vec![ + InterpolatedTextContents::Text(n.to_string()), + ])), + _ => Ret::DoneAsIs, } - _ => Ret::DoneAsIs, - }, + } (TextShow, [v]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { @@ -158,7 +158,7 @@ pub(crate) fn apply_builtin( let txt: InterpolatedText = std::iter::empty().collect(); let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ + Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(s), ])) } @@ -172,7 +172,7 @@ pub(crate) fn apply_builtin( )) .collect(); let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ + Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(s), ])) } @@ -182,28 +182,28 @@ pub(crate) fn apply_builtin( _ => Ret::DoneAsIs, }, (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueF(NaturalLit(0)), - NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())), + EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), + NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), _ => Ret::DoneAsIs, }, (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), + EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { - Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())) + Ret::ValueKind(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( + 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::ValueF(EmptyListLit(n.clone())), + EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), NEListLit(xs) => { - Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())) + Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) } _ => Ret::DoneAsIs, }, @@ -222,7 +222,7 @@ pub(crate) fn apply_builtin( 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( + let t = Value::from_kind_and_type( RecordType(kts), Value::from_const(Type), ); @@ -237,7 +237,7 @@ pub(crate) fn apply_builtin( let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_valuef_and_type( + Value::from_kind_and_type( NaturalLit(i), Value::from_builtin( Builtin::Natural, @@ -245,7 +245,7 @@ pub(crate) fn apply_builtin( ), ); kvs.insert("value".into(), e.clone()); - Value::from_valuef_and_type( + Value::from_kind_and_type( RecordLit(kvs), t.clone(), ) @@ -254,14 +254,14 @@ pub(crate) fn apply_builtin( ), _ => unreachable!(), }; - Ret::ValueF(list) + Ret::ValueKind(list) } _ => Ret::DoneAsIs, } } (ListBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(ListFold, args) => { + ValueKind::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { Ret::Value(args[1].clone()) } else { @@ -303,7 +303,7 @@ pub(crate) fn apply_builtin( }, (OptionalBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(OptionalFold, args) => { + ValueKind::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { Ret::Value(args[1].clone()) } else { @@ -338,7 +338,7 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(NaturalFold, args) => { + ValueKind::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { Ret::Value(args[0].clone()) } else { @@ -375,7 +375,7 @@ pub(crate) fn apply_builtin( _ => Ret::DoneAsIs, }; match ret { - Ret::ValueF(v) => v, + 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(); @@ -388,23 +388,23 @@ pub(crate) fn apply_builtin( } } -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF { +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => { + ValueKind::Lam(x, _, e) => { e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) } - ValueF::AppliedBuiltin(b, args) => { + ValueKind::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()) + ValueKind::UnionConstructor(l, kts) => { + ValueKind::UnionLit(l.clone(), a, kts.clone()) } _ => { drop(f_borrow); - ValueF::PartialExpr(ExprF::App(f, a)) + ValueKind::PartialExpr(ExprF::App(f, a)) } } } @@ -426,7 +426,7 @@ pub(crate) fn squash_textlit( Expr(e) => { let e_borrow = e.as_whnf(); match &*e_borrow { - ValueF::TextLit(elts2) => { + ValueKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -479,7 +479,7 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), Expr(ExprF), @@ -496,7 +496,7 @@ fn apply_binop<'a>( NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use ValueF::{ + use ValueKind::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; @@ -505,58 +505,58 @@ fn apply_binop<'a>( 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, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(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(true), _) => Ret::ValueKind(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueKind(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)), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueKind(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)), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)), (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x + y)) + Ret::ValueKind(NaturalLit(x + y)) } - (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x * y)) + Ret::ValueKind(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(), - )), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind( + 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( + (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(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( + Ret::ValueKind(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( + Ret::ValueKind(TextLit(squash_textlit( once(x).chain(y.iter().cloned()), ))) } @@ -573,7 +573,7 @@ fn apply_binop<'a>( // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::ValueF(RecordLit(kvs)) + Ret::ValueKind(RecordLit(kvs)) } (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { @@ -589,8 +589,8 @@ fn apply_binop<'a>( _ => unreachable!("Internal type error"), }; let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_valuef_and_type( - ValueF::PartialExpr(ExprF::BinOp( + Ok(Value::from_kind_and_type( + ValueKind::PartialExpr(ExprF::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), @@ -598,7 +598,7 @@ fn apply_binop<'a>( kts.get(k).expect("Internal type error").clone(), )) })?; - Ret::ValueF(RecordLit(kvs)) + Ret::ValueKind(RecordLit(kvs)) } (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { @@ -612,8 +612,8 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprF, ty: &Value, -) -> ValueF { - use ValueF::{ +) -> ValueKind { + use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, UnionLit, UnionType, @@ -639,17 +639,17 @@ pub(crate) fn normalize_one_layer( } 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::BoolLit(b) => Ret::ValueKind(BoolLit(b)), + ExprF::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), + ExprF::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), + ExprF::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprF::SomeLit(e) => Ret::ValueKind(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())) + Ret::ValueKind(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -658,10 +658,10 @@ pub(crate) fn normalize_one_layer( } } ExprF::NEListLit(elts) => { - Ret::ValueF(NEListLit(elts.into_iter().collect())) + Ret::ValueKind(NEListLit(elts.into_iter().collect())) } ExprF::RecordLit(kvs) => { - Ret::ValueF(RecordLit(kvs.into_iter().collect())) + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) } ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; @@ -670,7 +670,7 @@ pub(crate) fn normalize_one_layer( if let [Expr(th)] = elts.as_slice() { Ret::Value(th.clone()) } else { - Ret::ValueF(TextLit(elts)) + Ret::ValueKind(TextLit(elts)) } } ExprF::BoolIf(ref b, ref e1, ref e2) => { @@ -701,12 +701,12 @@ pub(crate) fn normalize_one_layer( }, ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueF(RecordLit(HashMap::new())) + Ret::ValueKind(RecordLit(HashMap::new())) } ExprF::Projection(ref v, ref ls) => { let v_borrow = v.as_whnf(); match &*v_borrow { - RecordLit(kvs) => Ret::ValueF(RecordLit( + RecordLit(kvs) => Ret::ValueKind(RecordLit( ls.iter() .filter_map(|l| { kvs.get(l).map(|x| (l.clone(), x.clone())) @@ -730,7 +730,7 @@ pub(crate) fn normalize_one_layer( } }, UnionType(kts) => { - Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) + Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) } _ => { drop(v_borrow); @@ -773,20 +773,20 @@ pub(crate) fn normalize_one_layer( }; match ret { - Ret::ValueF(v) => v, + Ret::ValueKind(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), + Ret::Expr(expr) => ValueKind::PartialExpr(expr), } } -/// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF { +/// Normalize a ValueKind into WHNF +pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { 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())) + ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(squash_textlit(elts.into_iter())) } // All other cases are already in WHNF v => v, diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 59380a3..96a0b4b 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; @@ -39,8 +39,8 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Value::from_valuef_and_type( - ValueF::Pi(x.into(), tx, te), + Ok(Value::from_kind_and_type( + ValueKind::Pi(x.into(), tx, te), Value::from_const(k), )) } @@ -71,8 +71,8 @@ fn tck_record_type( }; } - Ok(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), Value::from_const(k), )) } @@ -116,8 +116,8 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(Value::from_valuef_and_type( - ValueF::UnionType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::UnionType(new_kts), Value::from_const(k), )) } @@ -131,13 +131,13 @@ fn function_check(a: Const, b: Const) -> Const { } pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueF::Const(c); + let v = ValueKind::Const(c); match c { Const::Type => { - Value::from_valuef_and_type(v, const_to_value(Const::Kind)) + Value::from_kind_and_type(v, const_to_value(Const::Kind)) } Const::Kind => { - Value::from_valuef_and_type(v, const_to_value(Const::Sort)) + Value::from_kind_and_type(v, const_to_value(Const::Sort)) } Const::Sort => Value::const_sort(), } @@ -290,8 +290,8 @@ fn type_of_builtin(b: Builtin) -> Expr { pub(crate) fn builtin_to_value(b: Builtin) -> Value { let ctx = TypecheckContext::new(); - Value::from_valuef_and_type( - ValueF::from_builtin(b), + Value::from_kind_and_type( + ValueKind::from_builtin(b), type_with(&ctx, type_of_builtin(b)).unwrap(), ) } @@ -313,8 +313,8 @@ fn type_with( let ctx2 = ctx.insert_type(var, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; - Value::from_valuef_and_type( - ValueF::Lam(var.clone().into(), annot.clone(), body), + Value::from_kind_and_type( + ValueKind::Lam(var.clone().into(), annot.clone(), body), tck_pi_type(ctx, var.clone(), annot, body_type)?, ) } @@ -389,7 +389,7 @@ fn type_last_layer( let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); let (x, tx, tb) = match &*tf_borrow { - ValueF::Pi(x, tx, tb) => (x, tx, tb), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { @@ -406,8 +406,8 @@ fn type_last_layer( } Assert(t) => { match &*t.as_whnf() { - ValueF::Equivalence(x, y) if x == y => {} - ValueF::Equivalence(x, y) => { + ValueKind::Equivalence(x, y) if x == y => {} + ValueKind::Equivalence(x, y) => { return mkerr(AssertMismatch(x.clone(), y.clone())) } _ => return mkerr(AssertMustTakeEquivalence), @@ -415,7 +415,7 @@ fn type_last_layer( RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) { + if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { return mkerr(InvalidPredicate(x.clone())); } @@ -435,7 +435,7 @@ fn type_last_layer( } EmptyListLit(t) => { match &*t.as_whnf() { - ValueF::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args) if args.len() == 1 => {} _ => return mkerr(InvalidListType(t.clone())), } @@ -482,7 +482,7 @@ fn type_last_layer( )?), Field(r, x) => { match &*r.get_type()?.as_whnf() { - ValueF::RecordType(kts) => match kts.get(&x) { + ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => { RetTypeOnly(tth.clone()) }, @@ -492,7 +492,7 @@ fn type_last_layer( // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { - ValueF::UnionType(kts) => match kts.get(&x) { + ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { RetTypeOnly( @@ -553,14 +553,14 @@ fn type_last_layer( // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(r.clone())), }; @@ -589,7 +589,7 @@ fn type_last_layer( // Extract the LHS record type let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } @@ -598,7 +598,7 @@ fn type_last_layer( // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } @@ -626,7 +626,7 @@ fn type_last_layer( } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueF::AppliedBuiltin(List, _) => {} + ValueKind::AppliedBuiltin(List, _) => {} _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } @@ -648,8 +648,8 @@ fn type_last_layer( return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - RetWhole(Value::from_valuef_and_type( - ValueF::Equivalence(l.clone(), r.clone()), + RetWhole(Value::from_kind_and_type( + ValueKind::Equivalence(l.clone(), r.clone()), Value::from_const(Type), )) } @@ -684,14 +684,14 @@ fn type_last_layer( let record_type = record.get_type()?; let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), }; let union_type = union.get_type()?; let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { - ValueF::UnionType(kts) => kts, + ValueKind::UnionType(kts) => kts, _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), }; @@ -703,7 +703,7 @@ fn type_last_layer( 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), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -765,7 +765,7 @@ fn type_last_layer( let record_type = record.get_type()?; let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(ProjectionMustBeRecord), }; @@ -777,8 +777,8 @@ fn type_last_layer( }; } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + RetTypeOnly(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), record_type.get_type()?, )) } @@ -786,8 +786,8 @@ fn type_last_layer( }; Ok(match ret { - RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( - ValueF::PartialExpr(e), + RetTypeOnly(typ) => Value::from_kind_and_type_and_span( + ValueKind::PartialExpr(e), typ, span, ), -- cgit v1.2.3