diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/phase/mod.rs | 30 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 274 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/parse.rs | 2 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/resolve.rs | 2 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 121 |
5 files changed, 214 insertions, 215 deletions
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 752c257..b22120d 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,11 @@ use std::fmt::Display; use std::path::Path; -use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::valuef::ValueF; +use crate::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::core::value::Value; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -76,13 +77,6 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - /// - /// `normalize` does not type-check the expression. You may want to type-check - /// expressions before normalizing them since normalization can convert an - /// ill-typed expression into a well-typed expression. - /// - /// However, `normalize` will not fail if the expression is ill-typed and will - /// leave ill-typed sub-expressions unevaluated. pub fn normalize(mut self) -> Normalized { self.normalize_mut(); Normalized(self) @@ -91,8 +85,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) @@ -101,18 +95,22 @@ impl Typed { Typed::from_const(Const::Type) } + /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } + /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. pub fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, }) } + /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the + /// process. pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: true, @@ -148,8 +146,8 @@ impl Typed { pub fn make_record_type( kts: impl Iterator<Item = (String, Typed)>, ) -> 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 +156,8 @@ impl Typed { pub fn make_union_type( kts: impl Iterator<Item = (String, Option<Typed>)>, ) -> 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..d81a910 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,14 +1,14 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, - NaiveDouble, + BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, + Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -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(ExprKind::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(ExprKind::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<Value>, 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<Normalized> = 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(ExprKind::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,10 +479,10 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprF<Value, Normalized>), + Expr(ExprKind<Value, Normalized>), } fn apply_binop<'a>( @@ -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(ExprKind::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, _, _) => { @@ -610,46 +610,46 @@ fn apply_binop<'a>( } pub(crate) fn normalize_one_layer( - expr: ExprF<Value, Normalized>, + expr: ExprKind<Value, Normalized>, ty: &Value, -) -> ValueF { - use ValueF::{ +) -> ValueKind { + use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, UnionLit, UnionType, }; let ret = match expr { - ExprF::Import(_) => unreachable!( + ExprKind::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(_) => { + ExprKind::Lam(_, _, _) + | ExprKind::Pi(_, _, _) + | ExprKind::Let(_, _, _, _) + | ExprKind::Embed(_) + | ExprKind::Const(_) + | ExprKind::Builtin(_) + | ExprKind::Var(_) + | ExprKind::Annot(_, _) + | ExprKind::RecordType(_) + | ExprKind::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) => { + ExprKind::Assert(_) => Ret::Expr(expr), + ExprKind::App(v, a) => Ret::Value(v.app(a)), + ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), + ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), + ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), + ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), + ExprKind::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); @@ -657,23 +657,23 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::NEListLit(elts) => { - Ret::ValueF(NEListLit(elts.into_iter().collect())) + ExprKind::NEListLit(elts) => { + Ret::ValueKind(NEListLit(elts.into_iter().collect())) } - ExprF::RecordLit(kvs) => { - Ret::ValueF(RecordLit(kvs.into_iter().collect())) + ExprKind::RecordLit(kvs) => { + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) } - ExprF::TextLit(elts) => { + ExprKind::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)) + Ret::ValueKind(TextLit(elts)) } } - ExprF::BoolIf(ref b, ref e1, ref e2) => { + ExprKind::BoolIf(ref b, ref e1, ref e2) => { let b_borrow = b.as_whnf(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), @@ -695,18 +695,18 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + ExprKind::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())) + ExprKind::Projection(_, ref ls) if ls.is_empty() => { + Ret::ValueKind(RecordLit(HashMap::new())) } - ExprF::Projection(ref v, ref ls) => { + ExprKind::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())) @@ -719,7 +719,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::Field(ref v, ref l) => { + ExprKind::Field(ref v, ref l) => { let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { @@ -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); @@ -738,11 +738,11 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ProjectionByExpr(_, _) => { + ExprKind::ProjectionByExpr(_, _) => { unimplemented!("selection by expression") } - ExprF::Merge(ref handlers, ref variant, _) => { + ExprKind::Merge(ref handlers, ref variant, _) => { let handlers_borrow = handlers.as_whnf(); let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { @@ -769,24 +769,24 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::ToMap(_, _) => unimplemented!("toMap"), }; 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/parse.rs b/dhall/src/semantics/phase/parse.rs index 4c8ad7b..00db422 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -2,7 +2,7 @@ use std::fs::File; use std::io::Read; use std::path::Path; -use crate::semantics::error::Error; +use crate::error::Error; use crate::semantics::phase::resolve::ImportRoot; use crate::semantics::phase::Parsed; use crate::syntax::binary; diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index 86dc7ae..cc4a024 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; -use crate::semantics::error::{Error, ImportError}; +use crate::error::{Error, ImportError}; use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 59380a3..c439f74 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,16 +1,17 @@ use std::cmp::max; use std::collections::HashMap; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, }; fn tck_pi_type( @@ -39,8 +40,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 +72,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 +117,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,42 +132,42 @@ 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(), } } -pub fn rc<E>(x: RawExpr<E>) -> Expr<E> { +pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> { Expr::new(x, Span::Artificial) } // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { - (Type) => { ExprF::Const(Const::Type) }; - (Bool) => { ExprF::Builtin(Builtin::Bool) }; - (Natural) => { ExprF::Builtin(Builtin::Natural) }; - (Integer) => { ExprF::Builtin(Builtin::Integer) }; - (Double) => { ExprF::Builtin(Builtin::Double) }; - (Text) => { ExprF::Builtin(Builtin::Text) }; + (Type) => { ExprKind::Const(Const::Type) }; + (Bool) => { ExprKind::Builtin(Builtin::Bool) }; + (Natural) => { ExprKind::Builtin(Builtin::Natural) }; + (Integer) => { ExprKind::Builtin(Builtin::Integer) }; + (Double) => { ExprKind::Builtin(Builtin::Double) }; + (Text) => { ExprKind::Builtin(Builtin::Text) }; ($var:ident) => { - ExprF::Var(syntax::V(stringify!($var).into(), 0)) + ExprKind::Var(syntax::V(stringify!($var).into(), 0)) }; (Optional $ty:ident) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::Optional)), rc(make_type!($ty)) ) }; (List $($rest:tt)*) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::List)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), rc(make_type!($($rest)*)) ) }; @@ -178,24 +179,24 @@ macro_rules! make_type { rc(make_type!($ty)), ); )* - ExprF::RecordType(kts) + ExprKind::RecordType(kts) }}; ($ty:ident -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($ty)), rc(make_type!($($rest)*)) ) }; (($($arg:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($($arg)*)), rc(make_type!($($rest)*)) ) }; (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( stringify!($var).into(), rc(make_type!($($ty)*)), rc(make_type!($($rest)*)) @@ -290,8 +291,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { 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(), ) } @@ -304,7 +305,7 @@ fn type_with( ctx: &TypecheckContext, e: Expr<Normalized>, ) -> Result<Value, TypeError> { - use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); Ok(match e.as_ref() { @@ -313,8 +314,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)?, ) } @@ -359,13 +360,13 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF<Value, Normalized>, + e: ExprKind<Value, Normalized>, span: Span, ) -> Result<Value, TypeError> { use syntax::BinOp::*; use syntax::Builtin::*; use syntax::Const::Type; - use syntax::ExprF::*; + use syntax::ExprKind::*; use TypeMessage::*; let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); @@ -389,7 +390,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 +407,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 +416,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 +436,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 +483,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 +493,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 +554,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())), }; @@ -578,7 +579,7 @@ fn type_last_layer( } BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.get_type()?, r.get_type()?, @@ -589,7 +590,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 +599,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())) } @@ -612,7 +613,7 @@ fn type_last_layer( |_, l: &Value, r: &Value| { type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), @@ -626,7 +627,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 +649,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 +685,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 +704,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 +766,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 +778,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 +787,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, ), @@ -806,5 +807,5 @@ pub(crate) fn typecheck_with( expr: Expr<Normalized>, ty: Expr<Normalized>, ) -> Result<Value, TypeError> { - typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) + typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty))) } |