diff options
Diffstat (limited to 'dhall/src/semantics/phase/typecheck.rs')
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 121 |
1 files changed, 61 insertions, 60 deletions
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))) } |