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 | |
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/env.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/tck/mod.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tir.rs | 13 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 55 |
4 files changed, 31 insertions, 51 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 6dd5076..1fa66f0 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -2,21 +2,21 @@ use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; /// Environment for indexing variables. -#[derive(Debug, Clone, Copy)] -pub(crate) struct VarEnv { +#[derive(Debug, Clone, Copy, Default)] +pub struct VarEnv { size: usize, } /// Environment for typing expressions. #[derive(Debug, Clone)] -pub(crate) struct TyEnv { +pub struct TyEnv { names: NameEnv, items: ValEnv<Type>, } impl VarEnv { pub fn new() -> Self { - VarEnv { size: 0 } + VarEnv::default() } pub fn from_size(size: usize) -> Self { VarEnv { size } diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index 93c8f48..6dddfc5 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,6 +1,6 @@ pub mod env; pub mod tir; pub mod typecheck; -pub(crate) use env::*; -pub(crate) use tir::*; -pub(crate) use typecheck::*; +pub use env::*; +pub use tir::*; +pub use typecheck::*; diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index aeb7bf9..89a8027 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,15 +1,14 @@ use crate::error::{ErrorBuilder, TypeError}; use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; -use crate::syntax::{Builtin, Const, Span}; -use crate::NormalizedExpr; +use crate::syntax::{Builtin, Const, Expr, Span}; /// The type of a type. 0 is `Type`, 1 is `Kind`, etc... #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] -pub(crate) struct Universe(u8); +pub struct Universe(u8); /// An expression representing a type #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) struct Type { +pub struct Type { val: Nir, univ: Universe, } @@ -17,7 +16,7 @@ pub(crate) struct Type { /// A hir expression plus its inferred type. /// Stands for "Typed intermediate representation" #[derive(Debug, Clone)] -pub(crate) struct Tir<'hir> { +pub struct Tir<'hir> { hir: &'hir Hir, ty: Type, } @@ -101,7 +100,7 @@ impl Type { pub fn to_hir(&self, venv: VarEnv) -> Hir { self.val.to_hir(venv) } - pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { + pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr { self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) } } @@ -124,7 +123,7 @@ impl<'hir> Tir<'hir> { pub fn as_hir(&self) -> &Hir { &self.hir } - pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr { self.as_hir().to_expr_tyenv(env) } 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)) } |