From 60425d58151fef142b066d523dc4d5e832070b9c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 14:30:15 +0000 Subject: Add new Value type in API --- dhall/src/semantics/tck/typecheck.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 173b76d..9fa33f2 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -808,8 +808,8 @@ pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result, TypeError> { /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with<'hir>( hir: &'hir Hir, - ty: Hir, + ty: &Hir, ) -> Result, 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)) } -- cgit v1.2.3 From 2f5c45fd2f712f7befe6f7c92b62dc76d5f77538 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 16:50:49 +0000 Subject: Rename LitKind to NumKind --- dhall/src/semantics/tck/typecheck.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 9fa33f2..6951d62 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -9,7 +9,7 @@ use crate::semantics::{ NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, }; fn check_rectymerge( @@ -96,14 +96,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) => { -- cgit v1.2.3 From 35db1b4b54dba8b0cafe661329e0099dfabd8073 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 17:04:47 +0000 Subject: Remove top-level Expr aliases --- dhall/src/semantics/tck/tir.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index aeb7bf9..1865b8e 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,7 +1,6 @@ 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)] @@ -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) } -- cgit v1.2.3 From ef3734a3e9381b2e91552089774126f58f560bc3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 21:21:32 +0000 Subject: Improve handling of builtin types in Nir --- dhall/src/semantics/tck/typecheck.rs | 28 ++++++---------------------- 1 file changed, 6 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 6951d62..880ab22 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ 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, NumKind, Span, @@ -121,11 +121,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 +372,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 +428,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 +583,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() { -- cgit v1.2.3 From 7848c8e8d3147ebe428290558aa6c0efcbf59ee5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 18 Mar 2020 18:58:51 +0000 Subject: Brutally make all of dhall pub --- dhall/src/semantics/tck/env.rs | 4 ++-- dhall/src/semantics/tck/mod.rs | 6 +++--- dhall/src/semantics/tck/tir.rs | 6 +++--- dhall/src/semantics/tck/typecheck.rs | 10 +++++----- 4 files changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 6dd5076..f2ef00a 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -3,13 +3,13 @@ use crate::syntax::Label; /// Environment for indexing variables. #[derive(Debug, Clone, Copy)] -pub(crate) struct VarEnv { +pub struct VarEnv { size: usize, } /// Environment for typing expressions. #[derive(Debug, Clone)] -pub(crate) struct TyEnv { +pub struct TyEnv { names: NameEnv, items: ValEnv, } 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 1865b8e..89a8027 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -4,11 +4,11 @@ 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, } @@ -16,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, } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 880ab22..205185f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -53,11 +53,11 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn mkerr(msg: S) -> Result { +pub fn mkerr(msg: S) -> Result { Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) } -pub(crate) fn mk_span_err( +pub fn mk_span_err( span: Span, msg: S, ) -> Result { @@ -688,7 +688,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, @@ -785,12 +785,12 @@ 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, TypeError> { +pub fn typecheck<'hir>(hir: &'hir Hir) -> Result, 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, ) -> Result, TypeError> { -- cgit v1.2.3 From fa89e9cb319b353332c9e835944e7f86a6604c42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 18 Mar 2020 21:37:14 +0000 Subject: Move Value, SimpleValue and SimpleType to serde --- dhall/src/semantics/tck/typecheck.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 205185f..c3334b5 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -57,10 +57,7 @@ pub fn mkerr(msg: S) -> Result { Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) } -pub fn mk_span_err( - span: Span, - msg: S, -) -> Result { +pub fn mk_span_err(span: Span, msg: S) -> Result { mkerr( ErrorBuilder::new(msg.to_string()) .span_err(span, msg.to_string()) -- cgit v1.2.3 From 820214615547101f8f2b5de209b5189968bddfee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Apr 2020 17:37:15 +0100 Subject: Fix clippy warnings --- dhall/src/semantics/tck/env.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index f2ef00a..1fa66f0 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -2,7 +2,7 @@ use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; /// Environment for indexing variables. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, Default)] pub struct VarEnv { size: usize, } @@ -16,7 +16,7 @@ pub struct TyEnv { impl VarEnv { pub fn new() -> Self { - VarEnv { size: 0 } + VarEnv::default() } pub fn from_size(size: usize) -> Self { VarEnv { size } -- cgit v1.2.3