From 9741e3280ed03920732430e7994e1f8482c9ddd6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 17:48:13 +0200 Subject: s/DhallError/ImportError/ --- dhall/src/imports.rs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index 96268ca..95cf6fa 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -22,7 +22,7 @@ pub enum ImportRoot { fn resolve_import( import: &Import, root: &ImportRoot, -) -> Result, DhallError> { +) -> Result, ImportError> { use self::ImportRoot::*; use dhall_core::FilePrefix::*; use dhall_core::ImportLocation::*; @@ -43,23 +43,23 @@ fn resolve_import( } #[derive(Debug)] -pub enum DhallError { +pub enum ImportError { ParseError(ParseError), IOError(std::io::Error), } -impl From for DhallError { +impl From for ImportError { fn from(e: ParseError) -> Self { - DhallError::ParseError(e) + ImportError::ParseError(e) } } -impl From for DhallError { +impl From for ImportError { fn from(e: std::io::Error) -> Self { - DhallError::IOError(e) + ImportError::IOError(e) } } -impl fmt::Display for DhallError { +impl fmt::Display for ImportError { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use self::DhallError::*; + use self::ImportError::*; match self { ParseError(e) => e.fmt(f), IOError(e) => e.fmt(f), @@ -70,7 +70,7 @@ impl fmt::Display for DhallError { pub fn load_dhall_file( f: &Path, resolve_imports: bool, -) -> Result, DhallError> { +) -> Result, ImportError> { let mut buffer = String::new(); File::open(f)?.read_to_string(&mut buffer)?; let expr = parse_expr(&*buffer)?; @@ -88,7 +88,7 @@ pub fn load_dhall_file( pub fn load_dhall_file_no_resolve_imports( f: &Path, -) -> Result { +) -> Result { let mut buffer = String::new(); File::open(f)?.read_to_string(&mut buffer)?; let expr = parse_expr(&*buffer)?; -- cgit v1.2.3 From d9b4bd8d4019ca9ab999c0c4657663604158101c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 17:50:47 +0200 Subject: s/Type/StaticType/ --- dhall/src/dhall_type.rs | 22 +++++++++++----------- dhall/src/lib.rs | 3 +-- 2 files changed, 12 insertions(+), 13 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/dhall_type.rs b/dhall/src/dhall_type.rs index 6b0e06e..64e07d9 100644 --- a/dhall/src/dhall_type.rs +++ b/dhall/src/dhall_type.rs @@ -4,37 +4,37 @@ use dhall_generator::*; #[derive(Debug, Clone)] pub enum ConversionError {} -pub trait Type { +pub trait StaticType { fn get_type() -> DhallExpr; // fn as_dhall(&self) -> DhallExpr; // fn from_dhall(e: DhallExpr) -> Result; } -impl Type for bool { +impl StaticType for bool { fn get_type() -> DhallExpr { dhall_expr!(Bool) } } -impl Type for Natural { +impl StaticType for Natural { fn get_type() -> DhallExpr { dhall_expr!(Natural) } } -impl Type for Integer { +impl StaticType for Integer { fn get_type() -> DhallExpr { dhall_expr!(Integer) } } -impl Type for String { +impl StaticType for String { fn get_type() -> DhallExpr { dhall_expr!(Text) } } -impl Type for (A, B) { +impl StaticType for (A, B) { fn get_type() -> DhallExpr { let ta = A::get_type(); let tb = B::get_type(); @@ -42,33 +42,33 @@ impl Type for (A, B) { } } -impl Type for Option { +impl StaticType for Option { fn get_type() -> DhallExpr { let t = T::get_type(); dhall_expr!(Optional t) } } -impl Type for Vec { +impl StaticType for Vec { fn get_type() -> DhallExpr { let t = T::get_type(); dhall_expr!(List t) } } -impl<'a, T: Type> Type for &'a T { +impl<'a, T: StaticType> StaticType for &'a T { fn get_type() -> DhallExpr { T::get_type() } } -impl Type for std::marker::PhantomData { +impl StaticType for std::marker::PhantomData { fn get_type() -> DhallExpr { dhall_expr!({}) } } -impl Type for Result { +impl StaticType for Result { fn get_type() -> DhallExpr { let tt = T::get_type(); let te = E::get_type(); diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 103fd29..5a155c8 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -16,8 +16,7 @@ pub mod typecheck; pub use crate::dhall_type::*; pub use dhall_generator::expr; pub use dhall_generator::subexpr; -pub use dhall_generator::Type; - +pub use dhall_generator::StaticType; pub use crate::imports::*; // pub struct DhallExpr(dhall_core::DhallExpr); -- cgit v1.2.3 From 42d0f8100462f8a17a3ba1b86664310cdb71dfdc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 17:55:43 +0200 Subject: Rename some modules --- dhall/src/dhall_type.rs | 77 ------------------------------------------------- dhall/src/lib.rs | 6 ++-- dhall/src/traits.rs | 77 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 80 insertions(+), 80 deletions(-) delete mode 100644 dhall/src/dhall_type.rs create mode 100644 dhall/src/traits.rs (limited to 'dhall/src') diff --git a/dhall/src/dhall_type.rs b/dhall/src/dhall_type.rs deleted file mode 100644 index 64e07d9..0000000 --- a/dhall/src/dhall_type.rs +++ /dev/null @@ -1,77 +0,0 @@ -use dhall_core::*; -use dhall_generator::*; - -#[derive(Debug, Clone)] -pub enum ConversionError {} - -pub trait StaticType { - fn get_type() -> DhallExpr; - // fn as_dhall(&self) -> DhallExpr; - // fn from_dhall(e: DhallExpr) -> Result; -} - -impl StaticType for bool { - fn get_type() -> DhallExpr { - dhall_expr!(Bool) - } -} - -impl StaticType for Natural { - fn get_type() -> DhallExpr { - dhall_expr!(Natural) - } -} - -impl StaticType for Integer { - fn get_type() -> DhallExpr { - dhall_expr!(Integer) - } -} - -impl StaticType for String { - fn get_type() -> DhallExpr { - dhall_expr!(Text) - } -} - -impl StaticType for (A, B) { - fn get_type() -> DhallExpr { - let ta = A::get_type(); - let tb = B::get_type(); - dhall_expr!({ _1: ta, _2: tb }) - } -} - -impl StaticType for Option { - fn get_type() -> DhallExpr { - let t = T::get_type(); - dhall_expr!(Optional t) - } -} - -impl StaticType for Vec { - fn get_type() -> DhallExpr { - let t = T::get_type(); - dhall_expr!(List t) - } -} - -impl<'a, T: StaticType> StaticType for &'a T { - fn get_type() -> DhallExpr { - T::get_type() - } -} - -impl StaticType for std::marker::PhantomData { - fn get_type() -> DhallExpr { - dhall_expr!({}) - } -} - -impl StaticType for Result { - fn get_type() -> DhallExpr { - let tt = T::get_type(); - let te = E::get_type(); - dhall_expr!(< Ok: tt | Err: te>) - } -} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 5a155c8..7439312 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -10,14 +10,14 @@ mod normalize; pub use crate::normalize::*; pub mod binary; -mod dhall_type; pub mod imports; +mod traits; pub mod typecheck; -pub use crate::dhall_type::*; +pub use crate::imports::*; +pub use crate::traits::*; pub use dhall_generator::expr; pub use dhall_generator::subexpr; pub use dhall_generator::StaticType; -pub use crate::imports::*; // pub struct DhallExpr(dhall_core::DhallExpr); diff --git a/dhall/src/traits.rs b/dhall/src/traits.rs new file mode 100644 index 0000000..64e07d9 --- /dev/null +++ b/dhall/src/traits.rs @@ -0,0 +1,77 @@ +use dhall_core::*; +use dhall_generator::*; + +#[derive(Debug, Clone)] +pub enum ConversionError {} + +pub trait StaticType { + fn get_type() -> DhallExpr; + // fn as_dhall(&self) -> DhallExpr; + // fn from_dhall(e: DhallExpr) -> Result; +} + +impl StaticType for bool { + fn get_type() -> DhallExpr { + dhall_expr!(Bool) + } +} + +impl StaticType for Natural { + fn get_type() -> DhallExpr { + dhall_expr!(Natural) + } +} + +impl StaticType for Integer { + fn get_type() -> DhallExpr { + dhall_expr!(Integer) + } +} + +impl StaticType for String { + fn get_type() -> DhallExpr { + dhall_expr!(Text) + } +} + +impl StaticType for (A, B) { + fn get_type() -> DhallExpr { + let ta = A::get_type(); + let tb = B::get_type(); + dhall_expr!({ _1: ta, _2: tb }) + } +} + +impl StaticType for Option { + fn get_type() -> DhallExpr { + let t = T::get_type(); + dhall_expr!(Optional t) + } +} + +impl StaticType for Vec { + fn get_type() -> DhallExpr { + let t = T::get_type(); + dhall_expr!(List t) + } +} + +impl<'a, T: StaticType> StaticType for &'a T { + fn get_type() -> DhallExpr { + T::get_type() + } +} + +impl StaticType for std::marker::PhantomData { + fn get_type() -> DhallExpr { + dhall_expr!({}) + } +} + +impl StaticType for Result { + fn get_type() -> DhallExpr { + let tt = T::get_type(); + let te = E::get_type(); + dhall_expr!(< Ok: tt | Err: te>) + } +} -- cgit v1.2.3 From 366bc783e62682c9597e8caba1dac56638d34fa9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 18:24:49 +0200 Subject: Define some newtypes for Expr Closes #50 --- dhall/src/expr.rs | 35 +++++++++++++++++++++++++++++++++++ dhall/src/lib.rs | 10 ++-------- 2 files changed, 37 insertions(+), 8 deletions(-) create mode 100644 dhall/src/expr.rs (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs new file mode 100644 index 0000000..0d093cb --- /dev/null +++ b/dhall/src/expr.rs @@ -0,0 +1,35 @@ +use crate::typecheck::TypeError; +use dhall_core::*; + +pub struct Parsed(SubExpr); +pub struct Resolved(SubExpr); +pub struct Typed(SubExpr, Type); +pub struct Type(Box); +pub struct Normalized(SubExpr); + +// impl Parsed { +// pub fn resolve(self) -> Result { +// Ok(Resolved(crate::imports::resolve(self.0)?)) +// } +// } +impl Resolved { + pub fn typecheck(self) -> Result> { + let typ = Type(Box::new(Normalized(crate::typecheck::type_of( + self.0.clone(), + )?))); + Ok(Typed(self.0, typ)) + } +} +impl Typed { + pub fn normalize(self) -> Normalized { + Normalized(crate::normalize::normalize(self.0)) + } + pub fn get_type(&self) -> &Type { + &self.1 + } +} +impl Type { + pub fn as_expr(&self) -> &Normalized { + &*self.0 + } +} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 7439312..fee5ba8 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -18,11 +18,5 @@ pub use crate::traits::*; pub use dhall_generator::expr; pub use dhall_generator::subexpr; pub use dhall_generator::StaticType; - -// pub struct DhallExpr(dhall_core::DhallExpr); - -// impl DhallExpr { -// pub fn normalize(self) -> Self { -// DhallExpr(crate::normalize::normalize(self.0)) -// } -// } +pub mod expr; +pub use crate::expr::*; -- cgit v1.2.3 From 396ec334bac1e8d10a2d2b2d683c93e3b2ff4d8d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 20:04:04 +0200 Subject: Massage import loading into new API Closes #9 --- dhall/src/expr.rs | 30 +++++++++++------ dhall/src/imports.rs | 95 +++++++++++++++++++++++++++++++--------------------- 2 files changed, 76 insertions(+), 49 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 0d093cb..72633ea 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -1,17 +1,27 @@ +use crate::imports::ImportError; +use crate::imports::ImportRoot; use crate::typecheck::TypeError; use dhall_core::*; -pub struct Parsed(SubExpr); -pub struct Resolved(SubExpr); -pub struct Typed(SubExpr, Type); -pub struct Type(Box); -pub struct Normalized(SubExpr); +#[derive(Debug, Clone)] +pub struct Parsed(pub(crate) SubExpr, pub(crate) ImportRoot); +#[derive(Debug, Clone)] +pub struct Resolved(pub(crate) SubExpr); +#[derive(Debug, Clone)] +pub struct Typed(pub(crate) SubExpr, Type); +#[derive(Debug, Clone)] +pub struct Type(pub(crate) Box); +#[derive(Debug, Clone)] +pub struct Normalized(pub(crate) SubExpr); -// impl Parsed { -// pub fn resolve(self) -> Result { -// Ok(Resolved(crate::imports::resolve(self.0)?)) -// } -// } +impl Parsed { + pub fn resolve(self) -> Result { + crate::imports::resolve_expr(self, true) + } + pub fn resolve_no_imports(self) -> Result { + crate::imports::resolve_expr(self, false) + } +} impl Resolved { pub fn typecheck(self) -> Result> { let typ = Type(Box::new(Normalized(crate::typecheck::type_of( diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index 95cf6fa..bc38bb6 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -1,6 +1,7 @@ // use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X}; use dhall_core::{Expr, Import, X}; // use std::path::Path; +use crate::expr::*; use dhall_core::*; use std::fmt; use std::fs::File; @@ -8,6 +9,34 @@ use std::io::Read; use std::path::Path; use std::path::PathBuf; +#[derive(Debug)] +pub enum ImportError { + ParseError(ParseError), + IOError(std::io::Error), + UnexpectedImportError(Import), +} +impl From for ImportError { + fn from(e: ParseError) -> Self { + ImportError::ParseError(e) + } +} +impl From for ImportError { + fn from(e: std::io::Error) -> Self { + ImportError::IOError(e) + } +} +impl fmt::Display for ImportError { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use self::ImportError::*; + match self { + ParseError(e) => e.fmt(f), + IOError(e) => e.fmt(f), + UnexpectedImportError(e) => e.fmt(f), + } + } +} + +// Deprecated pub fn panic_imports(expr: &Expr) -> Expr { let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) }; expr.map_embed(&no_import) @@ -42,55 +71,43 @@ fn resolve_import( } } -#[derive(Debug)] -pub enum ImportError { - ParseError(ParseError), - IOError(std::io::Error), -} -impl From for ImportError { - fn from(e: ParseError) -> Self { - ImportError::ParseError(e) - } -} -impl From for ImportError { - fn from(e: std::io::Error) -> Self { - ImportError::IOError(e) - } -} -impl fmt::Display for ImportError { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use self::ImportError::*; - match self { - ParseError(e) => e.fmt(f), - IOError(e) => e.fmt(f), +pub(crate) fn resolve_expr( + Parsed(expr, root): Parsed, + allow_imports: bool, +) -> Result { + let resolve = |import: &Import| -> Result, ImportError> { + if allow_imports { + let expr = resolve_import(import, &root)?; + Ok(expr.roll()) + } else { + Err(ImportError::UnexpectedImportError(import.clone())) } - } + }; + let expr = expr.as_ref().traverse_embed(&resolve)?; + Ok(Resolved(expr.squash_embed())) +} + +pub fn load_from_file(f: &Path) -> Result { + let mut buffer = String::new(); + File::open(f)?.read_to_string(&mut buffer)?; + let expr = parse_expr(&*buffer)?; + let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); + Ok(Parsed(expr, root)) } +// Deprecated pub fn load_dhall_file( f: &Path, resolve_imports: bool, ) -> Result, ImportError> { - let mut buffer = String::new(); - File::open(f)?.read_to_string(&mut buffer)?; - let expr = parse_expr(&*buffer)?; - let expr = if resolve_imports { - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - let resolve = |import: &Import| -> Expr { - resolve_import(import, &root).unwrap() - }; - expr.as_ref().map_embed(&resolve).squash_embed() - } else { - panic_imports(expr.as_ref()) - }; - Ok(expr) + let expr = load_from_file(f)?; + let expr = resolve_expr(expr, resolve_imports)?; + Ok(expr.0.unroll()) } +// Deprecated pub fn load_dhall_file_no_resolve_imports( f: &Path, ) -> Result { - let mut buffer = String::new(); - File::open(f)?.read_to_string(&mut buffer)?; - let expr = parse_expr(&*buffer)?; - Ok(expr) + Ok(load_from_file(f)?.0) } -- cgit v1.2.3 From 412d0fac51b7b51aabcb049e3d6ba52f3dda1529 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 20:32:25 +0200 Subject: Move binary decoding to new API --- dhall/src/expr.rs | 22 ++++++++++++++-------- dhall/src/imports.rs | 49 ++++++++++++++++++++++++++++++++++++++++--------- dhall/src/lib.rs | 2 +- 3 files changed, 55 insertions(+), 18 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 72633ea..ae52e4d 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -1,27 +1,33 @@ -use crate::imports::ImportError; use crate::imports::ImportRoot; use crate::typecheck::TypeError; use dhall_core::*; -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Eq)] pub struct Parsed(pub(crate) SubExpr, pub(crate) ImportRoot); -#[derive(Debug, Clone)] + +#[derive(Debug, Clone, PartialEq, Eq)] pub struct Resolved(pub(crate) SubExpr); + #[derive(Debug, Clone)] pub struct Typed(pub(crate) SubExpr, Type); + #[derive(Debug, Clone)] pub struct Type(pub(crate) Box); + #[derive(Debug, Clone)] pub struct Normalized(pub(crate) SubExpr); -impl Parsed { - pub fn resolve(self) -> Result { - crate::imports::resolve_expr(self, true) +impl PartialEq for Parsed { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 } - pub fn resolve_no_imports(self) -> Result { - crate::imports::resolve_expr(self, false) +} +impl std::fmt::Display for Parsed { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.0.fmt(f) } } + impl Resolved { pub fn typecheck(self) -> Result> { let typ = Type(Box::new(Normalized(crate::typecheck::type_of( diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index bc38bb6..5d94b6a 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -1,6 +1,7 @@ // use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X}; use dhall_core::{Expr, Import, X}; // use std::path::Path; +use crate::binary::DecodeError; use crate::expr::*; use dhall_core::*; use std::fmt; @@ -12,6 +13,7 @@ use std::path::PathBuf; #[derive(Debug)] pub enum ImportError { ParseError(ParseError), + BinaryDecodeError(DecodeError), IOError(std::io::Error), UnexpectedImportError(Import), } @@ -20,6 +22,11 @@ impl From for ImportError { ImportError::ParseError(e) } } +impl From for ImportError { + fn from(e: DecodeError) -> Self { + ImportError::BinaryDecodeError(e) + } +} impl From for ImportError { fn from(e: std::io::Error) -> Self { ImportError::IOError(e) @@ -30,6 +37,7 @@ impl fmt::Display for ImportError { use self::ImportError::*; match self { ParseError(e) => e.fmt(f), + BinaryDecodeError(_) => unimplemented!(), IOError(e) => e.fmt(f), UnexpectedImportError(e) => e.fmt(f), } @@ -71,7 +79,7 @@ fn resolve_import( } } -pub(crate) fn resolve_expr( +fn resolve_expr( Parsed(expr, root): Parsed, allow_imports: bool, ) -> Result { @@ -87,12 +95,35 @@ pub(crate) fn resolve_expr( Ok(Resolved(expr.squash_embed())) } -pub fn load_from_file(f: &Path) -> Result { - let mut buffer = String::new(); - File::open(f)?.read_to_string(&mut buffer)?; - let expr = parse_expr(&*buffer)?; - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - Ok(Parsed(expr, root)) +impl Parsed { + pub fn load_from_file(f: &Path) -> Result { + let mut buffer = String::new(); + File::open(f)?.read_to_string(&mut buffer)?; + let expr = parse_expr(&*buffer)?; + let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); + Ok(Parsed(expr, root)) + } + + pub fn load_from_str(s: &str) -> Result { + let expr = parse_expr(s)?; + let root = ImportRoot::LocalDir(std::env::current_dir()?); + Ok(Parsed(expr, root)) + } + + pub fn load_from_binary_file(f: &Path) -> Result { + let mut buffer = Vec::new(); + File::open(f)?.read_to_end(&mut buffer)?; + let expr = crate::binary::decode(&buffer)?; + let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); + Ok(Parsed(expr, root)) + } + + pub fn resolve(self) -> Result { + crate::imports::resolve_expr(self, true) + } + pub fn resolve_no_imports(self) -> Result { + crate::imports::resolve_expr(self, false) + } } // Deprecated @@ -100,7 +131,7 @@ pub fn load_dhall_file( f: &Path, resolve_imports: bool, ) -> Result, ImportError> { - let expr = load_from_file(f)?; + let expr = Parsed::load_from_file(f)?; let expr = resolve_expr(expr, resolve_imports)?; Ok(expr.0.unroll()) } @@ -109,5 +140,5 @@ pub fn load_dhall_file( pub fn load_dhall_file_no_resolve_imports( f: &Path, ) -> Result { - Ok(load_from_file(f)?.0) + Ok(Parsed::load_from_file(f)?.0) } diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index fee5ba8..28b43ba 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -9,7 +9,7 @@ mod normalize; pub use crate::normalize::*; -pub mod binary; +mod binary; pub mod imports; mod traits; pub mod typecheck; -- cgit v1.2.3 From 7983c43210f5fcaa439fa1c6742e72252652e4f4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 20:50:57 +0200 Subject: Thread Typed through type_with --- dhall/src/expr.rs | 34 +++++-------------- dhall/src/normalize.rs | 10 ++++++ dhall/src/typecheck.rs | 89 +++++++++++++++++++++++++++----------------------- 3 files changed, 67 insertions(+), 66 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index ae52e4d..cc7f064 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -1,5 +1,4 @@ use crate::imports::ImportRoot; -use crate::typecheck::TypeError; use dhall_core::*; #[derive(Debug, Clone, Eq)] @@ -9,10 +8,11 @@ pub struct Parsed(pub(crate) SubExpr, pub(crate) ImportRoot); pub struct Resolved(pub(crate) SubExpr); #[derive(Debug, Clone)] -pub struct Typed(pub(crate) SubExpr, Type); +pub struct Typed(pub(crate) SubExpr, pub(crate) Type); -#[derive(Debug, Clone)] -pub struct Type(pub(crate) Box); +// #[derive(Debug, Clone)] +// pub struct Type(pub(crate) Box); +pub type Type = SubExpr; #[derive(Debug, Clone)] pub struct Normalized(pub(crate) SubExpr); @@ -28,24 +28,8 @@ impl std::fmt::Display for Parsed { } } -impl Resolved { - pub fn typecheck(self) -> Result> { - let typ = Type(Box::new(Normalized(crate::typecheck::type_of( - self.0.clone(), - )?))); - Ok(Typed(self.0, typ)) - } -} -impl Typed { - pub fn normalize(self) -> Normalized { - Normalized(crate::normalize::normalize(self.0)) - } - pub fn get_type(&self) -> &Type { - &self.1 - } -} -impl Type { - pub fn as_expr(&self) -> &Normalized { - &*self.0 - } -} +// impl Type { +// pub fn as_expr(&self) -> &Normalized { +// &*self.0 +// } +// } diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 24a8601..8ed2136 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -1,8 +1,18 @@ #![allow(non_snake_case)] +use crate::expr::*; use dhall_core::*; use dhall_generator::dhall_expr; use std::fmt; +impl Typed { + pub fn normalize(self) -> Normalized { + Normalized(normalize(self.0)) + } + pub fn get_type(&self) -> &Type { + &self.1 + } +} + fn apply_builtin(b: Builtin, args: &Vec>) -> WhatNext where S: fmt::Debug + Clone, diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e63b032..f5dbbbf 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -2,6 +2,7 @@ use std::collections::HashSet; use std::fmt; +use crate::expr::*; use crate::normalize::normalize; use dhall_core; use dhall_core::context::Context; @@ -10,6 +11,17 @@ use dhall_generator as dhall; use self::TypeMessage::*; +impl Resolved { + pub fn typecheck(self) -> Result> { + // let typ = Type(Box::new(Normalized(crate::typecheck::type_of( + // self.0.clone(), + // )?))); + // Ok(Typed(self.0, typ)) + let typ = crate::typecheck::type_of(self.0.clone())?; + Ok(Typed(self.0, typ)) + } +} + fn axiom(c: Const) -> Result> { use dhall_core::Const::*; use dhall_core::ExprF::*; @@ -199,13 +211,10 @@ where /// /// `type_with` normalizes the type since while type-checking. It expects the /// context to contain only normalized expressions. -pub fn type_with( - ctx: &Context>, - e: SubExpr, -) -> Result, TypeError> -where - S: ::std::fmt::Debug + Clone, -{ +pub fn type_with( + ctx: &Context>, + e: SubExpr, +) -> Result> { use dhall_core::BinOp::*; use dhall_core::Builtin::*; use dhall_core::Const::*; @@ -228,19 +237,19 @@ where let ctx2 = ctx .insert(x.clone(), t2.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, b.clone())?; - let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?; + let tB = type_with(&ctx2, b.clone())?.1; + let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1; Ok(Pi(x.clone(), t2, tB)) } Pi(x, tA, tB) => { - let ttA = type_with(ctx, tA.clone())?; + let ttA = type_with(ctx, tA.clone())?.1; let tA = normalize(SubExpr::clone(tA)); let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?; let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, tB.clone())?; + let tB = type_with(&ctx2, tB.clone())?.1; let kB = match tB.as_ref() { Const(k) => *k, _ => { @@ -264,15 +273,15 @@ where SubExpr::clone(r) }; - let tR = type_with(ctx, r)?; - let ttR = type_with(ctx, tR.clone())?; + let tR = type_with(ctx, r)?.1; + let ttR = type_with(ctx, tR.clone())?.1; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?; let ctx2 = ctx.insert(f.clone(), tR.clone()); - let tB = type_with(&ctx2, b.clone())?; - let ttB = type_with(ctx, tB.clone())?; + let tB = type_with(&ctx2, b.clone())?.1; + let ttB = type_with(ctx, tB.clone())?.1; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?; @@ -285,7 +294,7 @@ where } _ => match e .as_ref() - .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))? + .traverse_ref_simple(|e| type_with(ctx, e.clone()))? { Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), @@ -295,10 +304,10 @@ where Some(e) => Ok(e.unroll()), None => Err(mkerr(UnboundVariable)), }, - App((f, mut tf), args) => { + App(Typed(f, mut tf), args) => { let mut iter = args.into_iter(); let mut seen_args: Vec> = vec![]; - while let Some((a, ta)) = iter.next() { + while let Some(Typed(a, ta)) = iter.next() { seen_args.push(a.clone()); let (x, tx, tb) = match tf.as_ref() { Pi(x, tx, tb) => (x, tx, tb), @@ -321,18 +330,18 @@ where } Ok(tf.unroll()) } - Annot((x, tx), (t, _)) => { + Annot(Typed(x, tx), Typed(t, _)) => { let t = normalize(t.clone()); ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || { AnnotMismatch(x.clone(), t.clone(), tx.clone()) })?; Ok(t.unroll()) } - BoolIf((x, tx), (y, ty), (z, tz)) => { + BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => { ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || { InvalidPredicate(x.clone(), tx.clone()) })?; - let tty = type_with(ctx, ty.clone())?; + let tty = type_with(ctx, ty.clone())?.1; ensure_is_type( tty.clone(), IfBranchMustBeTerm( @@ -343,7 +352,7 @@ where ), )?; - let ttz = type_with(ctx, tz.clone())?; + let ttz = type_with(ctx, tz.clone())?.1; ensure_is_type( ttz.clone(), IfBranchMustBeTerm( @@ -364,35 +373,35 @@ where })?; Ok(ty.unroll()) } - EmptyListLit((t, tt)) => { - ensure_is_type(tt, InvalidListType(t.clone()))?; - let t = normalize(SubExpr::clone(t)); + EmptyListLit(Typed(t, tt)) => { + ensure_is_type(tt.clone(), InvalidListType(t.clone()))?; + let t = Typed(t, tt).normalize().0; Ok(dhall::expr!(List t)) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); - let (_, (_, t)) = iter.next().unwrap(); - let s = type_with(ctx, t.clone())?; + let (_, Typed(_, t)) = iter.next().unwrap(); + let s = type_with(ctx, t.clone())?.1; ensure_is_type(s, InvalidListType(t.clone()))?; - for (i, (y, ty)) in iter { + for (i, Typed(y, ty)) in iter { ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || { InvalidListElement(i, t.clone(), y.clone(), ty.clone()) })?; } Ok(dhall::expr!(List t)) } - EmptyOptionalLit((t, tt)) => { + EmptyOptionalLit(Typed(t, tt)) => { ensure_is_type(tt, InvalidOptionalType(t.clone()))?; let t = normalize(t.clone()); Ok(dhall::expr!(Optional t)) } - NEOptionalLit((_, t)) => { - let s = type_with(ctx, t.clone())?; + NEOptionalLit(Typed(_, t)) => { + let s = type_with(ctx, t.clone())?.1; ensure_is_type(s, InvalidOptionalType(t.clone()))?; Ok(dhall::expr!(Optional t)) } RecordType(kts) => { - for (k, (t, tt)) in kts { + for (k, Typed(t, tt)) in kts { ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?; } Ok(Const(Type)) @@ -400,15 +409,15 @@ where RecordLit(kvs) => { let kts = kvs .into_iter() - .map(|(k, (v, t))| { - let s = type_with(ctx, t.clone())?; + .map(|(k, Typed(v, t))| { + let s = type_with(ctx, t.clone())?.1; ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; Ok((k.clone(), t)) }) .collect::>()?; Ok(RecordType(kts)) } - Field((r, tr), x) => match tr.as_ref() { + Field(Typed(r, tr), x) => match tr.as_ref() { RecordType(kts) => match kts.get(&x) { Some(e) => Ok(e.unroll()), None => Err(mkerr(MissingField(x.clone(), tr.clone()))), @@ -422,7 +431,7 @@ where DoubleLit(_) => Ok(Builtin(Double)), // TODO: check type of interpolations TextLit(_) => Ok(Builtin(Text)), - BinOp(o, (l, tl), (r, tr)) => { + BinOp(o, Typed(l, tl), Typed(r, tr)) => { let t = Builtin(match o { BoolAnd => Bool, BoolOr => Bool, @@ -448,17 +457,15 @@ where _ => panic!("Unimplemented typecheck case: {:?}", e), }, }?; - Ok(rc(ret)) + Ok(Typed(e, rc(ret))) } /// `typeOf` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -pub fn type_of( - e: SubExpr, -) -> Result, TypeError> { +pub fn type_of(e: SubExpr) -> Result, TypeError> { let ctx = Context::new(); - type_with(&ctx, e) //.map(|e| e.into_owned()) + type_with(&ctx, e).map(|e| e.1) } /// The specific type error -- cgit v1.2.3 From c4438eb3d52b1a69c9022b12e8de135b8c9991c9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 21:54:55 +0200 Subject: Start taking Typed seriously --- dhall/src/expr.rs | 2 +- dhall/src/normalize.rs | 5 +- dhall/src/typecheck.rs | 239 +++++++++++++++++++++++++++---------------------- 3 files changed, 135 insertions(+), 111 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index cc7f064..831fbc5 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -15,7 +15,7 @@ pub struct Typed(pub(crate) SubExpr, pub(crate) Type); pub type Type = SubExpr; #[derive(Debug, Clone)] -pub struct Normalized(pub(crate) SubExpr); +pub struct Normalized(pub(crate) SubExpr, pub(crate) Type); impl PartialEq for Parsed { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 8ed2136..f9633fb 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -6,10 +6,7 @@ use std::fmt; impl Typed { pub fn normalize(self) -> Normalized { - Normalized(normalize(self.0)) - } - pub fn get_type(&self) -> &Type { - &self.1 + Normalized(normalize(self.0), self.1) } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index f5dbbbf..d62fe5a 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -3,7 +3,6 @@ use std::collections::HashSet; use std::fmt; use crate::expr::*; -use crate::normalize::normalize; use dhall_core; use dhall_core::context::Context; use dhall_core::*; @@ -21,6 +20,16 @@ impl Resolved { Ok(Typed(self.0, typ)) } } +impl Typed { + pub fn get_type(&self) -> &Type { + &self.1 + } +} +impl Normalized { + pub fn get_type(&self) -> &Type { + &self.1 + } +} fn axiom(c: Const) -> Result> { use dhall_core::Const::*; @@ -231,23 +240,29 @@ pub fn type_with( _ => Err(mkerr(msg)), }; + enum Ret { + ErrRet(TypeError), + OkNormalized(Normalized), + OkRet(Expr), + } + use Ret::*; let ret = match e.as_ref() { Lam(x, t, b) => { - let t2 = normalize(SubExpr::clone(t)); + let t2 = type_with(ctx, t.clone())?.normalize(); let ctx2 = ctx - .insert(x.clone(), t2.clone()) + .insert(x.clone(), t2.0.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let tB = type_with(&ctx2, b.clone())?.1; let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1; - Ok(Pi(x.clone(), t2, tB)) + OkRet(Pi(x.clone(), t2.0, tB)) } Pi(x, tA, tB) => { - let ttA = type_with(ctx, tA.clone())?.1; - let tA = normalize(SubExpr::clone(tA)); - let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?; + let tA = type_with(ctx, tA.clone())?.normalize(); + let kA = + ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?; let ctx2 = ctx - .insert(x.clone(), tA.clone()) + .insert(x.clone(), tA.0.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let tB = type_with(&ctx2, tB.clone())?.1; let kB = match tB.as_ref() { @@ -262,8 +277,8 @@ pub fn type_with( }; match rule(kA, kB) { - Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))), - Ok(_) => Ok(Const(kB)), + Err(()) => ErrRet(mkerr(NoDependentTypes(tA.0.clone(), tB))), + Ok(_) => OkRet(Const(kB)), } } Let(f, mt, r, b) => { @@ -273,24 +288,33 @@ pub fn type_with( SubExpr::clone(r) }; - let tR = type_with(ctx, r)?.1; - let ttR = type_with(ctx, tR.clone())?.1; + let r = type_with(ctx, r)?; + let tr = type_with(ctx, r.get_type().clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway - let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?; + let kR = ensure_const( + tr.get_type(), + InvalidInputType(r.get_type().clone()), + )?; - let ctx2 = ctx.insert(f.clone(), tR.clone()); - let tB = type_with(&ctx2, b.clone())?.1; - let ttB = type_with(ctx, tB.clone())?.1; + let ctx2 = ctx.insert(f.clone(), r.get_type().clone()); + let b = type_with(&ctx2, b.clone())?; + let tb = type_with(ctx, b.get_type().clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway - let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?; + let kB = ensure_const( + tb.get_type(), + InvalidOutputType(b.get_type().clone()), + )?; if let Err(()) = rule(kR, kB) { - return Err(mkerr(NoDependentLet(tR, tB))); + return Err(mkerr(NoDependentLet( + r.get_type().clone(), + b.get_type().clone(), + ))); } - Ok(tB.unroll()) + OkRet(b.get_type().unroll()) } _ => match e .as_ref() @@ -299,84 +323,85 @@ pub fn type_with( Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), - Const(c) => axiom(c).map(Const), + Const(c) => OkRet(Const(axiom(c)?)), Var(V(x, n)) => match ctx.lookup(&x, n) { - Some(e) => Ok(e.unroll()), - None => Err(mkerr(UnboundVariable)), + Some(e) => OkRet(e.unroll()), + None => ErrRet(mkerr(UnboundVariable)), }, - App(Typed(f, mut tf), args) => { + App(f, args) => { let mut iter = args.into_iter(); let mut seen_args: Vec> = vec![]; + let mut tf = type_with(ctx, f.get_type().clone())?.normalize(); while let Some(Typed(a, ta)) = iter.next() { seen_args.push(a.clone()); - let (x, tx, tb) = match tf.as_ref() { + let (x, tx, tb) = match tf.0.as_ref() { Pi(x, tx, tb) => (x, tx, tb), _ => { return Err(mkerr(NotAFunction( - rc(App(f.clone(), seen_args)), + rc(App(f.0.clone(), seen_args)), tf, ))); } }; ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || { TypeMismatch( - rc(App(f.clone(), seen_args.clone())), + rc(App(f.0.clone(), seen_args.clone())), tx.clone(), a.clone(), ta.clone(), ) })?; - tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb)); + tf = + type_with(ctx, subst_shift(&V(x.clone(), 0), &a, &tb))? + .normalize(); } - Ok(tf.unroll()) + OkNormalized(tf) } - Annot(Typed(x, tx), Typed(t, _)) => { - let t = normalize(t.clone()); - ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || { - AnnotMismatch(x.clone(), t.clone(), tx.clone()) - })?; - Ok(t.unroll()) + Annot(x, t) => { + let t = t.normalize(); + ensure_equal( + t.0.as_ref(), + x.get_type().as_ref(), + mkerr, + || AnnotMismatch(x.clone(), t.clone()), + )?; + OkNormalized(t) } - BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => { - ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || { - InvalidPredicate(x.clone(), tx.clone()) - })?; - let tty = type_with(ctx, ty.clone())?.1; + BoolIf(x, y, z) => { + ensure_equal( + x.get_type().as_ref(), + &Builtin(Bool), + mkerr, + || InvalidPredicate(x.clone()), + )?; + let ty = type_with(ctx, y.get_type().clone())?.normalize(); ensure_is_type( - tty.clone(), - IfBranchMustBeTerm( - true, - y.clone(), - ty.clone(), - tty.clone(), - ), + ty.get_type().clone(), + IfBranchMustBeTerm(true, y.clone()), )?; - let ttz = type_with(ctx, tz.clone())?.1; + let tz = type_with(ctx, z.get_type().clone())?.normalize(); ensure_is_type( - ttz.clone(), - IfBranchMustBeTerm( - false, - z.clone(), - tz.clone(), - ttz.clone(), - ), + tz.get_type().clone(), + IfBranchMustBeTerm(false, z.clone()), )?; - ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || { - IfBranchMismatch( - y.clone(), - z.clone(), - ty.clone(), - tz.clone(), - ) - })?; - Ok(ty.unroll()) + ensure_equal( + y.get_type().as_ref(), + z.get_type().as_ref(), + mkerr, + || IfBranchMismatch(y.clone(), z.clone()), + )?; + + OkNormalized(ty) } - EmptyListLit(Typed(t, tt)) => { - ensure_is_type(tt.clone(), InvalidListType(t.clone()))?; - let t = Typed(t, tt).normalize().0; - Ok(dhall::expr!(List t)) + EmptyListLit(t) => { + ensure_is_type( + t.get_type().clone(), + InvalidListType(t.0.clone()), + )?; + let t = t.normalize().0; + OkRet(dhall::expr!(List t)) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); @@ -388,23 +413,26 @@ pub fn type_with( InvalidListElement(i, t.clone(), y.clone(), ty.clone()) })?; } - Ok(dhall::expr!(List t)) + OkRet(dhall::expr!(List t)) } - EmptyOptionalLit(Typed(t, tt)) => { - ensure_is_type(tt, InvalidOptionalType(t.clone()))?; - let t = normalize(t.clone()); - Ok(dhall::expr!(Optional t)) + EmptyOptionalLit(t) => { + ensure_is_type( + t.get_type().clone(), + InvalidOptionalType(t.0.clone()), + )?; + let t = t.normalize().0; + OkRet(dhall::expr!(Optional t)) } NEOptionalLit(Typed(_, t)) => { let s = type_with(ctx, t.clone())?.1; ensure_is_type(s, InvalidOptionalType(t.clone()))?; - Ok(dhall::expr!(Optional t)) + OkRet(dhall::expr!(Optional t)) } RecordType(kts) => { for (k, Typed(t, tt)) in kts { ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?; } - Ok(Const(Type)) + OkRet(Const(Type)) } RecordLit(kvs) => { let kts = kvs @@ -415,23 +443,23 @@ pub fn type_with( Ok((k.clone(), t)) }) .collect::>()?; - Ok(RecordType(kts)) + OkRet(RecordType(kts)) } - Field(Typed(r, tr), x) => match tr.as_ref() { + Field(r, x) => match r.get_type().as_ref() { RecordType(kts) => match kts.get(&x) { - Some(e) => Ok(e.unroll()), - None => Err(mkerr(MissingField(x.clone(), tr.clone()))), + Some(e) => OkRet(e.unroll()), + None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))), }, - _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))), + _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))), }, - Builtin(b) => Ok(type_of_builtin(b)), - BoolLit(_) => Ok(Builtin(Bool)), - NaturalLit(_) => Ok(Builtin(Natural)), - IntegerLit(_) => Ok(Builtin(Integer)), - DoubleLit(_) => Ok(Builtin(Double)), + Builtin(b) => OkRet(type_of_builtin(b)), + BoolLit(_) => OkRet(Builtin(Bool)), + NaturalLit(_) => OkRet(Builtin(Natural)), + IntegerLit(_) => OkRet(Builtin(Integer)), + DoubleLit(_) => OkRet(Builtin(Double)), // TODO: check type of interpolations - TextLit(_) => Ok(Builtin(Text)), - BinOp(o, Typed(l, tl), Typed(r, tr)) => { + TextLit(_) => OkRet(Builtin(Text)), + BinOp(o, l, r) => { let t = Builtin(match o { BoolAnd => Bool, BoolOr => Bool, @@ -443,21 +471,25 @@ pub fn type_with( _ => panic!("Unimplemented typecheck case: {:?}", e), }); - ensure_equal(tl.as_ref(), &t, mkerr, || { - BinOpTypeMismatch(o, l.clone(), tl.clone()) + ensure_equal(l.get_type().as_ref(), &t, mkerr, || { + BinOpTypeMismatch(o, l.clone()) })?; - ensure_equal(tr.as_ref(), &t, mkerr, || { - BinOpTypeMismatch(o, r.clone(), tr.clone()) + ensure_equal(r.get_type().as_ref(), &t, mkerr, || { + BinOpTypeMismatch(o, r.clone()) })?; - Ok(t) + OkRet(t) } Embed(p) => match p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), }, - }?; - Ok(Typed(e, rc(ret))) + }; + match ret { + OkRet(ret) => Ok(Typed(e, rc(ret))), + OkNormalized(ret) => Ok(Typed(e, ret.0)), + ErrRet(e) => Err(e), + } } /// `typeOf` is the same as `type_with` with an empty context, meaning that the @@ -474,23 +506,18 @@ pub enum TypeMessage { UnboundVariable, InvalidInputType(SubExpr), InvalidOutputType(SubExpr), - NotAFunction(SubExpr, SubExpr), + NotAFunction(SubExpr, Normalized), TypeMismatch(SubExpr, SubExpr, SubExpr, SubExpr), - AnnotMismatch(SubExpr, SubExpr, SubExpr), + AnnotMismatch(Typed, Normalized), Untyped, InvalidListElement(usize, SubExpr, SubExpr, SubExpr), InvalidListType(SubExpr), InvalidOptionalElement(SubExpr, SubExpr, SubExpr), InvalidOptionalLiteral(usize), InvalidOptionalType(SubExpr), - InvalidPredicate(SubExpr, SubExpr), - IfBranchMismatch( - SubExpr, - SubExpr, - SubExpr, - SubExpr, - ), - IfBranchMustBeTerm(bool, SubExpr, SubExpr, SubExpr), + InvalidPredicate(Typed), + IfBranchMismatch(Typed, Typed), + IfBranchMustBeTerm(bool, Typed), InvalidField(Label, SubExpr), InvalidFieldType(Label, SubExpr), InvalidAlternative(Label, SubExpr), @@ -505,9 +532,9 @@ pub enum TypeMessage { HandlerInputTypeMismatch(Label, SubExpr, SubExpr), HandlerOutputTypeMismatch(Label, SubExpr, SubExpr), HandlerNotAFunction(Label, SubExpr), - NotARecord(Label, SubExpr, SubExpr), - MissingField(Label, SubExpr), - BinOpTypeMismatch(BinOp, SubExpr, SubExpr), + NotARecord(Label, Typed), + MissingField(Label, Typed), + BinOpTypeMismatch(BinOp, Typed), NoDependentLet(SubExpr, SubExpr), NoDependentTypes(SubExpr, SubExpr), } -- cgit v1.2.3 From f93aee4dcf71c85b826244b3b57949ffbdb820c4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 22:37:39 +0200 Subject: Add Sort type universe --- dhall/src/typecheck.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index d62fe5a..5457701 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -36,16 +36,19 @@ fn axiom(c: Const) -> Result> { use dhall_core::ExprF::*; match c { Type => Ok(Kind), - Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)), + Kind => Ok(Sort), + Sort => Err(TypeError::new(&Context::new(), rc(Const(Sort)), Untyped)), } } fn rule(a: Const, b: Const) -> Result { use dhall_core::Const::*; match (a, b) { - (Type, Kind) => Err(()), + (_, Type) => Ok(Type), (Kind, Kind) => Ok(Kind), - (Type, Type) | (Kind, Type) => Ok(Type), + (Sort, Sort) => Ok(Sort), + (Sort, Kind) => Ok(Sort), + _ => Err(()), } } -- cgit v1.2.3 From b0eb080caab28196a09c5b60c5b6556846732563 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 23:07:30 +0200 Subject: Store the whole type hierarchy in a Type --- dhall/src/expr.rs | 17 ++-- dhall/src/typecheck.rs | 260 ++++++++++++++++++++++++++++++------------------- 2 files changed, 167 insertions(+), 110 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 831fbc5..ad35645 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -10,9 +10,14 @@ pub struct Resolved(pub(crate) SubExpr); #[derive(Debug, Clone)] pub struct Typed(pub(crate) SubExpr, pub(crate) Type); -// #[derive(Debug, Clone)] -// pub struct Type(pub(crate) Box); -pub type Type = SubExpr; +#[derive(Debug, Clone)] +pub struct Type(pub(crate) TypeInternal); + +#[derive(Debug, Clone)] +pub(crate) enum TypeInternal { + Expr(Box), + Universe(usize), +} #[derive(Debug, Clone)] pub struct Normalized(pub(crate) SubExpr, pub(crate) Type); @@ -27,9 +32,3 @@ impl std::fmt::Display for Parsed { self.0.fmt(f) } } - -// impl Type { -// pub fn as_expr(&self) -> &Normalized { -// &*self.0 -// } -// } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 5457701..d0e1d44 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -16,8 +16,8 @@ impl Resolved { // self.0.clone(), // )?))); // Ok(Typed(self.0, typ)) - let typ = crate::typecheck::type_of(self.0.clone())?; - Ok(Typed(self.0, typ)) + let typ = crate::typecheck::type_of_(self.0.clone())?; + Ok(typ) } } impl Typed { @@ -30,14 +30,22 @@ impl Normalized { &self.1 } } - -fn axiom(c: Const) -> Result> { - use dhall_core::Const::*; - use dhall_core::ExprF::*; - match c { - Type => Ok(Kind), - Kind => Ok(Sort), - Sort => Err(TypeError::new(&Context::new(), rc(Const(Sort)), Untyped)), +impl Type { + // pub fn as_expr(&self) -> &Normalized { + // &*self.0 + // } + pub fn as_expr(&self) -> &SubExpr { + &self.as_normalized().0 + } + pub fn as_normalized(&self) -> &Normalized { + use TypeInternal::*; + match &self.0 { + Expr(e) => &e, + Universe(_) => unimplemented!(), + } + } + pub fn get_type(&self) -> &Type { + self.as_normalized().get_type() } } @@ -232,13 +240,15 @@ pub fn type_with( use dhall_core::Const::*; use dhall_core::ExprF::*; let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg); - let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() - { - Const(k) => Ok(*k), - _ => Err(mkerr(msg)), - }; + let ensure_const = + |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref() + { + Const(k) => Ok(*k), + _ => Err(mkerr(msg)), + }; let ensure_is_type = - |x: SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() { + |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref() + { Const(Type) => Ok(()), _ => Err(mkerr(msg)), }; @@ -246,6 +256,7 @@ pub fn type_with( enum Ret { ErrRet(TypeError), OkNormalized(Normalized), + OkType(crate::expr::Type), OkRet(Expr), } use Ret::*; @@ -255,9 +266,12 @@ pub fn type_with( let ctx2 = ctx .insert(x.clone(), t2.0.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, b.clone())?.1; - let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1; - OkRet(Pi(x.clone(), t2.0, tB)) + let b = type_with(&ctx2, b.clone())?; + let _ = type_with( + ctx, + rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())), + )?; + OkRet(Pi(x.clone(), t2.0, b.get_type().as_expr().clone())) } Pi(x, tA, tB) => { let tA = type_with(ctx, tA.clone())?.normalize(); @@ -267,20 +281,23 @@ pub fn type_with( let ctx2 = ctx .insert(x.clone(), tA.0.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, tB.clone())?.1; - let kB = match tB.as_ref() { + let tB = type_with(&ctx2, tB.clone())?; + let kB = match tB.get_type().as_expr().as_ref() { Const(k) => *k, _ => { return Err(TypeError::new( &ctx2, e.clone(), - InvalidOutputType(tB), + InvalidOutputType(tB.get_type().clone()), )); } }; match rule(kA, kB) { - Err(()) => ErrRet(mkerr(NoDependentTypes(tA.0.clone(), tB))), + Err(()) => ErrRet(mkerr(NoDependentTypes( + tA.0.clone(), + tB.get_type().clone(), + ))), Ok(_) => OkRet(Const(kB)), } } @@ -292,32 +309,30 @@ pub fn type_with( }; let r = type_with(ctx, r)?; - let tr = type_with(ctx, r.get_type().clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kR = ensure_const( - tr.get_type(), - InvalidInputType(r.get_type().clone()), + r.get_type().get_type(), + InvalidInputType(r.get_type().as_expr().clone()), )?; - let ctx2 = ctx.insert(f.clone(), r.get_type().clone()); + let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone()); let b = type_with(&ctx2, b.clone())?; - let tb = type_with(ctx, b.get_type().clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kB = ensure_const( - tb.get_type(), + b.get_type().get_type(), InvalidOutputType(b.get_type().clone()), )?; if let Err(()) = rule(kR, kB) { return Err(mkerr(NoDependentLet( - r.get_type().clone(), - b.get_type().clone(), + r.get_type().as_expr().clone(), + b.get_type().as_expr().clone(), ))); } - OkRet(b.get_type().unroll()) + OkType(b.get_type().clone()) } _ => match e .as_ref() @@ -326,7 +341,9 @@ pub fn type_with( Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), - Const(c) => OkRet(Const(axiom(c)?)), + Const(Type) => OkRet(Const(Kind)), + Const(Kind) => OkRet(Const(Sort)), + Const(Sort) => ErrRet(mkerr(Untyped)), Var(V(x, n)) => match ctx.lookup(&x, n) { Some(e) => OkRet(e.unroll()), None => ErrRet(mkerr(UnboundVariable)), @@ -334,9 +351,9 @@ pub fn type_with( App(f, args) => { let mut iter = args.into_iter(); let mut seen_args: Vec> = vec![]; - let mut tf = type_with(ctx, f.get_type().clone())?.normalize(); - while let Some(Typed(a, ta)) = iter.next() { - seen_args.push(a.clone()); + let mut tf = f.get_type().as_normalized().clone(); + while let Some(a) = iter.next() { + seen_args.push(a.0.clone()); let (x, tx, tb) = match tf.0.as_ref() { Pi(x, tx, tb) => (x, tx, tb), _ => { @@ -346,17 +363,23 @@ pub fn type_with( ))); } }; - ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || { - TypeMismatch( - rc(App(f.0.clone(), seen_args.clone())), - tx.clone(), - a.clone(), - ta.clone(), - ) - })?; - tf = - type_with(ctx, subst_shift(&V(x.clone(), 0), &a, &tb))? - .normalize(); + ensure_equal( + tx.as_ref(), + a.get_type().as_expr().as_ref(), + mkerr, + || { + TypeMismatch( + rc(App(f.0.clone(), seen_args.clone())), + tx.clone(), + a.clone(), + ) + }, + )?; + tf = type_with( + ctx, + subst_shift(&V(x.clone(), 0), &a.0, &tb), + )? + .normalize(); } OkNormalized(tf) } @@ -364,91 +387,103 @@ pub fn type_with( let t = t.normalize(); ensure_equal( t.0.as_ref(), - x.get_type().as_ref(), + x.get_type().as_expr().as_ref(), mkerr, || AnnotMismatch(x.clone(), t.clone()), )?; - OkNormalized(t) + OkType(x.get_type().clone()) } BoolIf(x, y, z) => { ensure_equal( - x.get_type().as_ref(), + x.get_type().as_expr().as_ref(), &Builtin(Bool), mkerr, || InvalidPredicate(x.clone()), )?; - let ty = type_with(ctx, y.get_type().clone())?.normalize(); ensure_is_type( - ty.get_type().clone(), + y.get_type().get_type(), IfBranchMustBeTerm(true, y.clone()), )?; - let tz = type_with(ctx, z.get_type().clone())?.normalize(); ensure_is_type( - tz.get_type().clone(), + z.get_type().get_type(), IfBranchMustBeTerm(false, z.clone()), )?; ensure_equal( - y.get_type().as_ref(), - z.get_type().as_ref(), + y.get_type().as_expr().as_ref(), + z.get_type().as_expr().as_ref(), mkerr, || IfBranchMismatch(y.clone(), z.clone()), )?; - OkNormalized(ty) + OkType(y.get_type().clone()) } EmptyListLit(t) => { - ensure_is_type( - t.get_type().clone(), - InvalidListType(t.0.clone()), - )?; + ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?; let t = t.normalize().0; OkRet(dhall::expr!(List t)) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); - let (_, Typed(_, t)) = iter.next().unwrap(); - let s = type_with(ctx, t.clone())?.1; - ensure_is_type(s, InvalidListType(t.clone()))?; - for (i, Typed(y, ty)) in iter { - ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || { - InvalidListElement(i, t.clone(), y.clone(), ty.clone()) - })?; + let (_, x) = iter.next().unwrap(); + ensure_is_type( + x.get_type().get_type(), + InvalidListType(x.get_type().as_expr().clone()), + )?; + for (i, y) in iter { + ensure_equal( + x.get_type().as_expr().as_ref(), + y.get_type().as_expr().as_ref(), + mkerr, + || { + InvalidListElement( + i, + x.get_type().as_expr().clone(), + y.clone(), + ) + }, + )?; } + let t = x.get_type().as_expr().clone(); OkRet(dhall::expr!(List t)) } EmptyOptionalLit(t) => { - ensure_is_type( - t.get_type().clone(), - InvalidOptionalType(t.0.clone()), - )?; + ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?; let t = t.normalize().0; OkRet(dhall::expr!(Optional t)) } - NEOptionalLit(Typed(_, t)) => { - let s = type_with(ctx, t.clone())?.1; - ensure_is_type(s, InvalidOptionalType(t.clone()))?; + NEOptionalLit(x) => { + ensure_is_type( + x.get_type().get_type(), + InvalidOptionalType(x.get_type().as_expr().clone()), + )?; + let t = x.get_type().as_expr().clone(); OkRet(dhall::expr!(Optional t)) } RecordType(kts) => { - for (k, Typed(t, tt)) in kts { - ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?; + for (k, t) in kts { + ensure_is_type( + t.get_type(), + InvalidFieldType(k.clone(), t.clone()), + )?; } OkRet(Const(Type)) } RecordLit(kvs) => { let kts = kvs .into_iter() - .map(|(k, Typed(v, t))| { - let s = type_with(ctx, t.clone())?.1; - ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; - Ok((k.clone(), t)) + .map(|(k, v)| { + ensure_is_type( + v.get_type().get_type(), + InvalidField(k.clone(), v.clone()), + )?; + Ok((k.clone(), v.get_type().as_expr().clone())) }) .collect::>()?; OkRet(RecordType(kts)) } - Field(r, x) => match r.get_type().as_ref() { + Field(r, x) => match r.get_type().as_expr().as_ref() { RecordType(kts) => match kts.get(&x) { Some(e) => OkRet(e.unroll()), None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))), @@ -474,13 +509,19 @@ pub fn type_with( _ => panic!("Unimplemented typecheck case: {:?}", e), }); - ensure_equal(l.get_type().as_ref(), &t, mkerr, || { - BinOpTypeMismatch(o, l.clone()) - })?; + ensure_equal( + l.get_type().as_expr().as_ref(), + &t, + mkerr, + || BinOpTypeMismatch(o, l.clone()), + )?; - ensure_equal(r.get_type().as_ref(), &t, mkerr, || { - BinOpTypeMismatch(o, r.clone()) - })?; + ensure_equal( + r.get_type().as_expr().as_ref(), + &t, + mkerr, + || BinOpTypeMismatch(o, r.clone()), + )?; OkRet(t) } @@ -489,8 +530,20 @@ pub fn type_with( }, }; match ret { - OkRet(ret) => Ok(Typed(e, rc(ret))), - OkNormalized(ret) => Ok(Typed(e, ret.0)), + OkRet(Const(Sort)) => { + Ok(Typed(e, crate::expr::Type(TypeInternal::Universe(3)))) + } + OkRet(ret) => Ok(Typed( + e, + crate::expr::Type(TypeInternal::Expr(Box::new( + type_with(ctx, rc(ret))?.normalize(), + ))), + )), + OkNormalized(ret) => Ok(Typed( + e, + crate::expr::Type(TypeInternal::Expr(Box::new(ret))), + )), + OkType(ret) => Ok(Typed(e, ret)), ErrRet(e) => Err(e), } } @@ -500,7 +553,12 @@ pub fn type_with( /// will fail. pub fn type_of(e: SubExpr) -> Result, TypeError> { let ctx = Context::new(); - type_with(&ctx, e).map(|e| e.1) + type_with(&ctx, e).map(|e| e.get_type().as_expr().clone()) +} + +pub fn type_of_(e: SubExpr) -> Result> { + let ctx = Context::new(); + type_with(&ctx, e) } /// The specific type error @@ -508,12 +566,12 @@ pub fn type_of(e: SubExpr) -> Result, TypeError> { pub enum TypeMessage { UnboundVariable, InvalidInputType(SubExpr), - InvalidOutputType(SubExpr), + InvalidOutputType(crate::expr::Type), NotAFunction(SubExpr, Normalized), - TypeMismatch(SubExpr, SubExpr, SubExpr, SubExpr), + TypeMismatch(SubExpr, SubExpr, Typed), AnnotMismatch(Typed, Normalized), Untyped, - InvalidListElement(usize, SubExpr, SubExpr, SubExpr), + InvalidListElement(usize, SubExpr, Typed), InvalidListType(SubExpr), InvalidOptionalElement(SubExpr, SubExpr, SubExpr), InvalidOptionalLiteral(usize), @@ -521,8 +579,8 @@ pub enum TypeMessage { InvalidPredicate(Typed), IfBranchMismatch(Typed, Typed), IfBranchMustBeTerm(bool, Typed), - InvalidField(Label, SubExpr), - InvalidFieldType(Label, SubExpr), + InvalidField(Label, Typed), + InvalidFieldType(Label, Typed), InvalidAlternative(Label, SubExpr), InvalidAlternativeType(Label, SubExpr), DuplicateAlternative(Label), @@ -539,7 +597,7 @@ pub enum TypeMessage { MissingField(Label, Typed), BinOpTypeMismatch(BinOp, Typed), NoDependentLet(SubExpr, SubExpr), - NoDependentTypes(SubExpr, SubExpr), + NoDependentTypes(SubExpr, crate::expr::Type), } /// A structured type error that includes context @@ -571,7 +629,7 @@ impl ::std::error::Error for TypeMessage { InvalidInputType(_) => "Invalid function input", InvalidOutputType(_) => "Invalid function output", NotAFunction(_, _) => "Not a function", - TypeMismatch(_, _, _, _) => "Wrong type of function argument", + TypeMismatch(_, _, _) => "Wrong type of function argument", _ => "Unhandled error", } } @@ -583,13 +641,13 @@ impl fmt::Display for TypeMessage { UnboundVariable => { f.write_str(include_str!("errors/UnboundVariable.txt")) } - TypeMismatch(e0, e1, e2, e3) => { + TypeMismatch(e0, e1, e2) => { let template = include_str!("errors/TypeMismatch.txt"); let s = template .replace("$txt0", &format!("{}", e0)) .replace("$txt1", &format!("{}", e1)) - .replace("$txt2", &format!("{}", e2)) - .replace("$txt3", &format!("{}", e3)); + .replace("$txt2", &format!("{}", e2.0)) + .replace("$txt3", &format!("{}", e2.get_type().as_expr())); f.write_str(&s) } _ => f.write_str("Unhandled error message"), -- cgit v1.2.3 From 2e29ffcff718db2f95372c6f5258338df92ea213 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 23:41:32 +0200 Subject: More improvements to typecheck --- dhall/src/typecheck.rs | 247 +++++++++++++++++++++++-------------------------- 1 file changed, 114 insertions(+), 133 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index d0e1d44..0ebc67e 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -21,6 +21,9 @@ impl Resolved { } } impl Typed { + fn as_expr(&self) -> &SubExpr { + &self.0 + } pub fn get_type(&self) -> &Type { &self.1 } @@ -29,15 +32,18 @@ impl Normalized { pub fn get_type(&self) -> &Type { &self.1 } + fn into_type(self) -> Type { + crate::expr::Type(TypeInternal::Expr(Box::new(self))) + } } impl Type { // pub fn as_expr(&self) -> &Normalized { // &*self.0 // } - pub fn as_expr(&self) -> &SubExpr { + fn as_expr(&self) -> &SubExpr { &self.as_normalized().0 } - pub fn as_normalized(&self) -> &Normalized { + fn as_normalized(&self) -> &Normalized { use TypeInternal::*; match &self.0 { Expr(e) => &e, @@ -49,6 +55,9 @@ impl Type { } } +const TYPE_OF_SORT: crate::expr::Type = + crate::expr::Type(TypeInternal::Universe(4)); + fn rule(a: Const, b: Const) -> Result { use dhall_core::Const::*; match (a, b) { @@ -209,8 +218,8 @@ fn type_of_builtin(b: Builtin) -> Expr { } fn ensure_equal<'a, S, F1, F2>( - x: &'a Expr, - y: &'a Expr, + x: &'a Type, + y: &'a Type, mkerr: F1, mkmsg: F2, ) -> Result<(), TypeError> @@ -219,7 +228,7 @@ where F1: FnOnce(TypeMessage) -> TypeError, F2: FnOnce() -> TypeMessage, { - if prop_equal(x, y) { + if prop_equal(x.as_expr().as_ref(), y.as_expr().as_ref()) { Ok(()) } else { Err(mkerr(mkmsg())) @@ -253,33 +262,40 @@ pub fn type_with( _ => Err(mkerr(msg)), }; + let mktype = + |ctx, x: SubExpr| Ok(type_with(ctx, x)?.normalize().into_type()); + enum Ret { - ErrRet(TypeError), - OkNormalized(Normalized), - OkType(crate::expr::Type), - OkRet(Expr), + RetType(crate::expr::Type), + RetExpr(Expr), } use Ret::*; let ret = match e.as_ref() { Lam(x, t, b) => { - let t2 = type_with(ctx, t.clone())?.normalize(); + let t2 = mktype(ctx, t.clone())?; let ctx2 = ctx - .insert(x.clone(), t2.0.clone()) + .insert(x.clone(), t2.as_expr().clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let b = type_with(&ctx2, b.clone())?; let _ = type_with( ctx, rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())), )?; - OkRet(Pi(x.clone(), t2.0, b.get_type().as_expr().clone())) + Ok(RetExpr(Pi( + x.clone(), + t2.as_expr().clone(), + b.get_type().as_expr().clone(), + ))) } Pi(x, tA, tB) => { - let tA = type_with(ctx, tA.clone())?.normalize(); - let kA = - ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?; + let tA = mktype(ctx, tA.clone())?; + let kA = ensure_const( + tA.get_type(), + InvalidInputType(tA.as_expr().clone()), + )?; let ctx2 = ctx - .insert(x.clone(), tA.0.clone()) + .insert(x.clone(), tA.as_expr().clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let tB = type_with(&ctx2, tB.clone())?; let kB = match tB.get_type().as_expr().as_ref() { @@ -294,11 +310,11 @@ pub fn type_with( }; match rule(kA, kB) { - Err(()) => ErrRet(mkerr(NoDependentTypes( - tA.0.clone(), + Err(()) => Err(mkerr(NoDependentTypes( + tA.as_expr().clone(), tB.get_type().clone(), ))), - Ok(_) => OkRet(Const(kB)), + Ok(k) => Ok(RetExpr(Const(k))), } } Let(f, mt, r, b) => { @@ -332,7 +348,7 @@ pub fn type_with( ))); } - OkType(b.get_type().clone()) + Ok(RetType(b.get_type().clone())) } _ => match e .as_ref() @@ -341,20 +357,20 @@ pub fn type_with( Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), - Const(Type) => OkRet(Const(Kind)), - Const(Kind) => OkRet(Const(Sort)), - Const(Sort) => ErrRet(mkerr(Untyped)), + Const(Type) => Ok(RetExpr(Const(Kind))), + Const(Kind) => Ok(RetExpr(Const(Sort))), + Const(Sort) => Ok(RetType(TYPE_OF_SORT)), Var(V(x, n)) => match ctx.lookup(&x, n) { - Some(e) => OkRet(e.unroll()), - None => ErrRet(mkerr(UnboundVariable)), + Some(e) => Ok(RetExpr(e.unroll())), + None => Err(mkerr(UnboundVariable)), }, App(f, args) => { let mut iter = args.into_iter(); let mut seen_args: Vec> = vec![]; - let mut tf = f.get_type().as_normalized().clone(); + let mut tf = f.get_type().clone(); while let Some(a) = iter.next() { seen_args.push(a.0.clone()); - let (x, tx, tb) = match tf.0.as_ref() { + let (x, tx, tb) = match tf.as_expr().as_ref() { Pi(x, tx, tb) => (x, tx, tb), _ => { return Err(mkerr(NotAFunction( @@ -363,40 +379,29 @@ pub fn type_with( ))); } }; - ensure_equal( - tx.as_ref(), - a.get_type().as_expr().as_ref(), - mkerr, - || { - TypeMismatch( - rc(App(f.0.clone(), seen_args.clone())), - tx.clone(), - a.clone(), - ) - }, - )?; - tf = type_with( - ctx, - subst_shift(&V(x.clone(), 0), &a.0, &tb), - )? - .normalize(); + let tx = mktype(ctx, tx.clone())?; + ensure_equal(&tx, a.get_type(), mkerr, || { + TypeMismatch( + rc(App(f.0.clone(), seen_args.clone())), + tx.clone(), + a.clone(), + ) + })?; + tf = mktype(ctx, subst_shift(&V(x.clone(), 0), &a.0, &tb))?; } - OkNormalized(tf) + Ok(RetType(tf)) } Annot(x, t) => { - let t = t.normalize(); - ensure_equal( - t.0.as_ref(), - x.get_type().as_expr().as_ref(), - mkerr, - || AnnotMismatch(x.clone(), t.clone()), - )?; - OkType(x.get_type().clone()) + let t = t.normalize().into_type(); + ensure_equal(&t, x.get_type(), mkerr, || { + AnnotMismatch(x.clone(), t.clone()) + })?; + Ok(RetType(x.get_type().clone())) } BoolIf(x, y, z) => { ensure_equal( - x.get_type().as_expr().as_ref(), - &Builtin(Bool), + x.get_type(), + &mktype(ctx, rc(Builtin(Bool)))?, mkerr, || InvalidPredicate(x.clone()), )?; @@ -410,19 +415,16 @@ pub fn type_with( IfBranchMustBeTerm(false, z.clone()), )?; - ensure_equal( - y.get_type().as_expr().as_ref(), - z.get_type().as_expr().as_ref(), - mkerr, - || IfBranchMismatch(y.clone(), z.clone()), - )?; + ensure_equal(y.get_type(), z.get_type(), mkerr, || { + IfBranchMismatch(y.clone(), z.clone()) + })?; - OkType(y.get_type().clone()) + Ok(RetType(y.get_type().clone())) } EmptyListLit(t) => { ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?; let t = t.normalize().0; - OkRet(dhall::expr!(List t)) + Ok(RetExpr(dhall::expr!(List t))) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); @@ -432,26 +434,21 @@ pub fn type_with( InvalidListType(x.get_type().as_expr().clone()), )?; for (i, y) in iter { - ensure_equal( - x.get_type().as_expr().as_ref(), - y.get_type().as_expr().as_ref(), - mkerr, - || { - InvalidListElement( - i, - x.get_type().as_expr().clone(), - y.clone(), - ) - }, - )?; + ensure_equal(x.get_type(), y.get_type(), mkerr, || { + InvalidListElement( + i, + x.get_type().as_expr().clone(), + y.clone(), + ) + })?; } let t = x.get_type().as_expr().clone(); - OkRet(dhall::expr!(List t)) + Ok(RetExpr(dhall::expr!(List t))) } EmptyOptionalLit(t) => { ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?; let t = t.normalize().0; - OkRet(dhall::expr!(Optional t)) + Ok(RetExpr(dhall::expr!(Optional t))) } NEOptionalLit(x) => { ensure_is_type( @@ -459,7 +456,7 @@ pub fn type_with( InvalidOptionalType(x.get_type().as_expr().clone()), )?; let t = x.get_type().as_expr().clone(); - OkRet(dhall::expr!(Optional t)) + Ok(RetExpr(dhall::expr!(Optional t))) } RecordType(kts) => { for (k, t) in kts { @@ -468,7 +465,7 @@ pub fn type_with( InvalidFieldType(k.clone(), t.clone()), )?; } - OkRet(Const(Type)) + Ok(RetExpr(Const(Type))) } RecordLit(kvs) => { let kts = kvs @@ -481,70 +478,54 @@ pub fn type_with( Ok((k.clone(), v.get_type().as_expr().clone())) }) .collect::>()?; - OkRet(RecordType(kts)) + Ok(RetExpr(RecordType(kts))) } Field(r, x) => match r.get_type().as_expr().as_ref() { RecordType(kts) => match kts.get(&x) { - Some(e) => OkRet(e.unroll()), - None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))), + Some(e) => Ok(RetExpr(e.unroll())), + None => Err(mkerr(MissingField(x.clone(), r.clone()))), }, - _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))), + _ => Err(mkerr(NotARecord(x.clone(), r.clone()))), }, - Builtin(b) => OkRet(type_of_builtin(b)), - BoolLit(_) => OkRet(Builtin(Bool)), - NaturalLit(_) => OkRet(Builtin(Natural)), - IntegerLit(_) => OkRet(Builtin(Integer)), - DoubleLit(_) => OkRet(Builtin(Double)), + Builtin(b) => Ok(RetExpr(type_of_builtin(b))), + BoolLit(_) => Ok(RetExpr(Builtin(Bool))), + NaturalLit(_) => Ok(RetExpr(Builtin(Natural))), + IntegerLit(_) => Ok(RetExpr(Builtin(Integer))), + DoubleLit(_) => Ok(RetExpr(Builtin(Double))), // TODO: check type of interpolations - TextLit(_) => OkRet(Builtin(Text)), + TextLit(_) => Ok(RetExpr(Builtin(Text))), BinOp(o, l, r) => { - let t = Builtin(match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, - _ => panic!("Unimplemented typecheck case: {:?}", e), - }); - - ensure_equal( - l.get_type().as_expr().as_ref(), - &t, - mkerr, - || BinOpTypeMismatch(o, l.clone()), + let t = mktype( + ctx, + rc(Builtin(match o { + BoolAnd => Bool, + BoolOr => Bool, + BoolEQ => Bool, + BoolNE => Bool, + NaturalPlus => Natural, + NaturalTimes => Natural, + TextAppend => Text, + _ => panic!("Unimplemented typecheck case: {:?}", e), + })), )?; - ensure_equal( - r.get_type().as_expr().as_ref(), - &t, - mkerr, - || BinOpTypeMismatch(o, r.clone()), - )?; + ensure_equal(l.get_type(), &t, mkerr, || { + BinOpTypeMismatch(o, l.clone()) + })?; - OkRet(t) + ensure_equal(r.get_type(), &t, mkerr, || { + BinOpTypeMismatch(o, r.clone()) + })?; + + Ok(RetType(t)) } Embed(p) => match p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), }, - }; + }?; match ret { - OkRet(Const(Sort)) => { - Ok(Typed(e, crate::expr::Type(TypeInternal::Universe(3)))) - } - OkRet(ret) => Ok(Typed( - e, - crate::expr::Type(TypeInternal::Expr(Box::new( - type_with(ctx, rc(ret))?.normalize(), - ))), - )), - OkNormalized(ret) => Ok(Typed( - e, - crate::expr::Type(TypeInternal::Expr(Box::new(ret))), - )), - OkType(ret) => Ok(Typed(e, ret)), - ErrRet(e) => Err(e), + RetExpr(ret) => Ok(Typed(e, mktype(ctx, rc(ret))?)), + RetType(typ) => Ok(Typed(e, typ)), } } @@ -567,9 +548,9 @@ pub enum TypeMessage { UnboundVariable, InvalidInputType(SubExpr), InvalidOutputType(crate::expr::Type), - NotAFunction(SubExpr, Normalized), - TypeMismatch(SubExpr, SubExpr, Typed), - AnnotMismatch(Typed, Normalized), + NotAFunction(SubExpr, crate::expr::Type), + TypeMismatch(SubExpr, crate::expr::Type, Typed), + AnnotMismatch(Typed, crate::expr::Type), Untyped, InvalidListElement(usize, SubExpr, Typed), InvalidListType(SubExpr), @@ -645,8 +626,8 @@ impl fmt::Display for TypeMessage { let template = include_str!("errors/TypeMismatch.txt"); let s = template .replace("$txt0", &format!("{}", e0)) - .replace("$txt1", &format!("{}", e1)) - .replace("$txt2", &format!("{}", e2.0)) + .replace("$txt1", &format!("{}", e1.as_expr())) + .replace("$txt2", &format!("{}", e2.as_expr())) .replace("$txt3", &format!("{}", e2.get_type().as_expr())); f.write_str(&s) } -- cgit v1.2.3 From 0ce048e4d95b08e50dec0f2e0f6736f3c5b646f2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 7 Apr 2019 00:24:34 +0200 Subject: More typecheck --- dhall/src/typecheck.rs | 164 ++++++++++++++++++++++++++----------------------- 1 file changed, 86 insertions(+), 78 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 0ebc67e..29ad6d4 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,5 +1,4 @@ #![allow(non_snake_case)] -use std::collections::HashSet; use std::fmt; use crate::expr::*; @@ -12,10 +11,6 @@ use self::TypeMessage::*; impl Resolved { pub fn typecheck(self) -> Result> { - // let typ = Type(Box::new(Normalized(crate::typecheck::type_of( - // self.0.clone(), - // )?))); - // Ok(Typed(self.0, typ)) let typ = crate::typecheck::type_of_(self.0.clone())?; Ok(typ) } @@ -24,11 +19,23 @@ impl Typed { fn as_expr(&self) -> &SubExpr { &self.0 } + fn into_expr(self) -> SubExpr { + self.0 + } + pub fn into_type(self) -> Type { + self.1 + } pub fn get_type(&self) -> &Type { &self.1 } } impl Normalized { + fn as_expr(&self) -> &SubExpr { + &self.0 + } + fn into_expr(self) -> SubExpr { + self.0 + } pub fn get_type(&self) -> &Type { &self.1 } @@ -37,11 +44,8 @@ impl Normalized { } } impl Type { - // pub fn as_expr(&self) -> &Normalized { - // &*self.0 - // } fn as_expr(&self) -> &SubExpr { - &self.as_normalized().0 + &self.as_normalized().as_expr() } fn as_normalized(&self) -> &Normalized { use TypeInternal::*; @@ -50,13 +54,24 @@ impl Type { Universe(_) => unimplemented!(), } } + fn into_expr(self) -> SubExpr { + use TypeInternal::*; + match self.0 { + Expr(e) => e.into_expr(), + Universe(_) => unimplemented!(), + } + } pub fn get_type(&self) -> &Type { - self.as_normalized().get_type() + use TypeInternal::*; + match &self.0 { + Expr(e) => e.get_type(), + Universe(_) => unimplemented!(), + // Universe(n) => &Type(Universe(n+1)), + } } } -const TYPE_OF_SORT: crate::expr::Type = - crate::expr::Type(TypeInternal::Universe(4)); +const TYPE_OF_SORT: Type = Type(TypeInternal::Universe(4)); fn rule(a: Const, b: Const) -> Result { use dhall_core::Const::*; @@ -89,11 +104,7 @@ fn match_vars(vl: &V