diff options
Diffstat (limited to 'dhall/src/semantics')
| -rw-r--r-- | dhall/src/semantics/core/value_kind.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 6 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 76 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 45 | ||||
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 54 |
5 files changed, 95 insertions, 90 deletions
diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 47df39d..35b2b23 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -5,7 +5,7 @@ use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::{Normalized, NormalizedExpr}; use crate::semantics::to_expr; use crate::syntax::{ - Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; @@ -43,7 +43,7 @@ pub(crate) enum ValueKind { TextLit(Vec<InterpolatedTextContents<Value>>), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF<Value, Normalized>), + PartialExpr(ExprKind<Value, Normalized>), } impl ValueKind { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 77473f6..1548713 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use crate::syntax::{ExprF, InterpolatedTextContents, Label, V}; +use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; /// Stores a pair of variables: a normal one and one /// that corresponds to the alpha-normalized version of the first one. @@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> { } } -impl<T: Shift, E: Clone> Shift for ExprF<T, E> { +impl<T: Shift, E: Clone> Shift for ExprKind<T, E> { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(self.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { } } -impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> { +impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> { fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { self.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 157d1f3..3e612aa 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -7,8 +7,8 @@ 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 @@ -46,7 +46,7 @@ macro_rules! make_closure { ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; (1 + $($rest:tt)*) => { - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::NaturalPlus, make_closure!($($rest)*), Value::from_kind_and_type( @@ -61,7 +61,7 @@ macro_rules! make_closure { let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); let list_type = tail.get_type_not_sort(); - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::ListAppend, ValueKind::NEListLit(vec![head]) .into_value_with_type(list_type.clone()), @@ -404,7 +404,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { } _ => { drop(f_borrow); - ValueKind::PartialExpr(ExprF::App(f, a)) + ValueKind::PartialExpr(ExprKind::App(f, a)) } } } @@ -482,7 +482,7 @@ enum Ret<'a> { ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprF<Value, Normalized>), + Expr(ExprKind<Value, Normalized>), } fn apply_binop<'a>( @@ -590,7 +590,7 @@ fn apply_binop<'a>( }; let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), @@ -610,7 +610,7 @@ fn apply_binop<'a>( } pub(crate) fn normalize_one_layer( - expr: ExprF<Value, Normalized>, + expr: ExprKind<Value, Normalized>, ty: &Value, ) -> ValueKind { use ValueKind::{ @@ -620,31 +620,31 @@ pub(crate) fn normalize_one_layer( }; 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::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) => { + 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 { @@ -657,13 +657,13 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::NEListLit(elts) => { + ExprKind::NEListLit(elts) => { Ret::ValueKind(NEListLit(elts.into_iter().collect())) } - ExprF::RecordLit(kvs) => { + 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 @@ -673,7 +673,7 @@ pub(crate) fn normalize_one_layer( 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,15 +695,15 @@ 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() => { + 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::ValueKind(RecordLit( @@ -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) { @@ -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,7 +769,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::ToMap(_, _) => unimplemented!("toMap"), }; match ret { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 5041235..f83bb94 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -10,7 +10,8 @@ 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, RawExpr, + Span, }; fn tck_pi_type( @@ -149,24 +150,24 @@ pub fn rc<E>(x: RawExpr<E>) -> Expr<E> { // 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)*)) @@ -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() { @@ -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)); @@ -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()?, @@ -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(), @@ -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))) } diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 74bd2fe..6099976 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -3,7 +3,7 @@ use crate::semantics::core::value_kind::ValueKind; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::syntax; -use crate::syntax::{Builtin, ExprF}; +use crate::syntax::{Builtin, ExprKind}; #[derive(Copy, Clone)] /// Controls conversion from `Value` to `Expr` @@ -31,7 +31,7 @@ pub(crate) fn kind_to_expr( opts: ToExprOptions, ) -> NormalizedExpr { match kind { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( x.to_label_maybe_alpha(opts.alpha), t.to_expr(opts), e.to_expr(opts), @@ -39,59 +39,63 @@ pub(crate) fn kind_to_expr( ValueKind::AppliedBuiltin(b, args) => args .iter() .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + .fold(rc(ExprKind::Builtin(*b)), |acc, v| { + rc(ExprKind::App(acc, v)) + }), + ValueKind::Pi(x, t, e) => rc(ExprKind::Pi( x.to_label_maybe_alpha(opts.alpha), t.to_expr(opts), e.to_expr(opts), )), - ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprF::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), + ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), + ValueKind::Const(c) => rc(ExprKind::Const(*c)), + ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)), + ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)), + ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)), + ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)), + ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::OptionalNone)), n.to_expr(opts), )), - ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.to_expr(opts), - )))), - ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))), + ValueKind::EmptyListLit(n) => { + rc(ExprKind::EmptyListLit(rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + n.to_expr(opts), + )))) + } + ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit( elts.iter().map(|n| n.to_expr(opts)).collect(), )), - ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( + ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( + ValueKind::RecordType(kts) => rc(ExprKind::RecordType( kts.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::UnionType(kts) => rc(ExprF::UnionType( + ValueKind::UnionType(kts) => rc(ExprKind::UnionType( kts.iter() .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) .collect(), )), - ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( ValueKind::UnionType(kts.clone()).to_expr(opts), l.clone(), )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), v.to_expr(opts), )), - ValueKind::TextLit(elts) => rc(ExprF::TextLit( + ValueKind::TextLit(elts) => rc(ExprKind::TextLit( elts.iter() .map(|contents| contents.map_ref(|e| e.to_expr(opts))) .collect(), )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( syntax::BinOp::Equivalence, x.to_expr(opts), y.to_expr(opts), |