diff options
author | Nadrieril | 2020-04-05 17:57:07 +0100 |
---|---|---|
committer | GitHub | 2020-04-05 17:57:07 +0100 |
commit | 7e977f282fb6a0eff0ef45738b9b5c98dc4c6fee (patch) | |
tree | ad4249609707fd8720a44469152105c2f6a67c79 /dhall/src/semantics/tck/typecheck.rs | |
parent | 5a5aa49e64197899006751db72e404f4b2292d4e (diff) | |
parent | 820214615547101f8f2b5de209b5189968bddfee (diff) |
Merge pull request #154 from Nadrieril/cleanup-api
Rewrite serde_dhall API
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 55 |
1 files changed, 18 insertions, 37 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 173b76d..c3334b5 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,11 +5,11 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, - NirKind, Tir, TyEnv, Type, + type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv, + Type, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, }; fn check_rectymerge( @@ -53,14 +53,11 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> { +pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) } -pub(crate) fn mk_span_err<T, S: ToString>( - span: Span, - msg: S, -) -> Result<T, TypeError> { +pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> { mkerr( ErrorBuilder::new(msg.to_string()) .span_err(span, msg.to_string()) @@ -96,14 +93,14 @@ fn type_one_layer( let t_hir = type_of_builtin(*b); typecheck(&t_hir)?.eval_to_type(env)? } - ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), - ExprKind::Lit(LitKind::Natural(_)) => { + ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool), + ExprKind::Num(NumKind::Natural(_)) => { Type::from_builtin(Builtin::Natural) } - ExprKind::Lit(LitKind::Integer(_)) => { + ExprKind::Num(NumKind::Integer(_)) => { Type::from_builtin(Builtin::Integer) } - ExprKind::Lit(LitKind::Double(_)) => { + ExprKind::Num(NumKind::Double(_)) => { Type::from_builtin(Builtin::Double) } ExprKind::TextLit(interpolated) => { @@ -121,11 +118,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.eval_to_type(env)?; match t.kind() { - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - }) if args.len() == 1 => {} + NirKind::ListType(..) => {} _ => return span_err("InvalidListType"), }; t @@ -376,10 +369,7 @@ fn type_one_layer( } ExprKind::BinOp(BinOp::ListAppend, l, r) => { match l.ty().kind() { - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - .. - }) => {} + NirKind::ListType(..) => {} _ => return span_err("BinOpTypeMismatch"), } @@ -435,12 +425,7 @@ fn type_one_layer( let union_type = union.ty(); let variants = match union_type.kind() { NirKind::UnionType(kts) => Cow::Borrowed(kts), - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::Optional, - args, - .. - }) if args.len() == 1 => { - let ty = &args[0]; + NirKind::OptionalType(ty) => { let mut kts = HashMap::new(); kts.insert("None".into(), None); kts.insert("Some".into(), Some(ty.clone())); @@ -595,11 +580,7 @@ fn type_one_layer( let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; let arg = match annot_val.kind() { - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - }) if args.len() == 1 => &args[0], + NirKind::ListType(t) => t, _ => return span_err(err_msg), }; let kts = match arg.kind() { @@ -704,7 +685,7 @@ fn type_one_layer( /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation /// to compare with. -pub(crate) fn type_with<'hir>( +pub fn type_with<'hir>( env: &TyEnv, hir: &'hir Hir, annot: Option<Type>, @@ -801,15 +782,15 @@ pub(crate) fn type_with<'hir>( /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> { +pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> { type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with<'hir>( +pub fn typecheck_with<'hir>( hir: &'hir Hir, - ty: Hir, + ty: &Hir, ) -> Result<Tir<'hir>, TypeError> { - let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; + let ty = typecheck(ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } |