From 5542797c77a9dfcdffec539f1a82341a450291a2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 15:31:06 +0000 Subject: s/TypecheckContext/TyCtx/ --- dhall/src/error/mod.rs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'dhall/src/error') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 6e7be64..56bc8ab 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,6 @@ use std::io::Error as IOError; -use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; @@ -41,7 +41,7 @@ pub enum EncodeError { #[derive(Debug)] pub struct TypeError { message: TypeMessage, - context: TypecheckContext, + context: TyCtx, } /// The specific type error @@ -88,10 +88,7 @@ pub(crate) enum TypeMessage { } impl TypeError { - pub(crate) fn new( - context: &TypecheckContext, - message: TypeMessage, - ) -> Self { + pub(crate) fn new(context: &TyCtx, message: TypeMessage) -> Self { TypeError { context: context.clone(), message, -- cgit v1.3.1 From c448698f797f2304dca0e0b8b833959de00ca079 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 20 Jan 2020 15:27:19 +0000 Subject: Reimplement basic tck/nze with proper environments Inspired from dhall_haskell --- dhall/src/error/mod.rs | 5 + dhall/src/semantics/core/var.rs | 3 + dhall/src/semantics/mod.rs | 1 + dhall/src/semantics/nze/mod.rs | 2 + dhall/src/semantics/nze/nzexpr.rs | 399 ++++++++++++++++++++++++++++++++++++++ dhall/src/semantics/tck/tyexpr.rs | 16 +- dhall/src/tests.rs | 19 +- 7 files changed, 432 insertions(+), 13 deletions(-) create mode 100644 dhall/src/semantics/nze/mod.rs create mode 100644 dhall/src/semantics/nze/nzexpr.rs (limited to 'dhall/src/error') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 56bc8ab..844a3e4 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -174,3 +174,8 @@ impl From for Error { Error::Typecheck(err) } } +impl From for Error { + fn from(_: crate::semantics::nze::nzexpr::TypeError) -> Error { + Error::Decode(DecodeError::WrongFormatError("type error".to_string())) + } +} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 0aa86d5..0d2c1d4 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -14,6 +14,9 @@ pub struct Binder { } impl AlphaVar { + pub(crate) fn new(alpha: V<()>) -> Self { + AlphaVar { alpha } + } pub(crate) fn default() -> Self { AlphaVar { alpha: V((), 0) } } diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 63f74ee..1304502 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,4 +1,5 @@ pub mod core; +pub mod nze; pub mod phase; pub mod tck; pub(crate) use self::core::*; diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs new file mode 100644 index 0000000..ef8918f --- /dev/null +++ b/dhall/src/semantics/nze/mod.rs @@ -0,0 +1,2 @@ +pub mod nzexpr; +// pub(crate) use nzexpr::*; diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs new file mode 100644 index 0000000..2f27dcb --- /dev/null +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -0,0 +1,399 @@ +#![allow(dead_code)] +use crate::semantics::core::var::AlphaVar; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::syntax::{Expr, ExprKind, Label, V}; + +pub(crate) type Type = NzExpr; +#[derive(Debug, Clone)] +pub(crate) struct TypeError; +pub(crate) type Binder = Label; + +// An expression with inferred types at every node and resolved variables. +#[derive(Debug, Clone)] +pub(crate) struct TyExpr { + kind: Box, + ty: Option, +} + +#[derive(Debug, Clone)] +pub(crate) enum TyExprKind { + Var(AlphaVar), + Expr(ExprKind), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzExpr { + kind: Box, + ty: Option>, +} + +#[derive(Debug, Clone)] +pub(crate) enum NzExprKind { + Var { + var: NzVar, + }, + Lam { + binder: Binder, + annot: NzExpr, + env: TyEnv, + body: TyExpr, + }, + Pi { + binder: Binder, + annot: NzExpr, + env: TyEnv, + body: TyExpr, + }, + Expr(ExprKind), + // Unevaled { + // env: TyEnv, + // expr: TyExprKind, + // }, +} + +#[derive(Debug, Clone)] +enum TyEnvItem { + // Variable is bound with given type + Kept(Type), + // Variable has been replaced by corresponding value + Replaced(NzExpr), +} + +#[derive(Debug, Clone)] +pub(crate) struct TyEnv { + env: Vec<(Binder, TyEnvItem)>, +} + +#[derive(Debug, Clone, Copy)] +pub(crate) struct QuoteEnv { + size: usize, +} + +// Reverse-debruijn index: counts number of binders from the bottom of the stack. +#[derive(Debug, Clone, Copy)] +pub(crate) struct NzVar { + idx: usize, +} + +impl TyEnv { + pub fn new() -> Self { + TyEnv { env: Vec::new() } + } + pub fn to_quoteenv(&self) -> QuoteEnv { + QuoteEnv { + size: self.env.len(), + } + } + fn with_vec(&self, vec: Vec<(Binder, TyEnvItem)>) -> Self { + TyEnv { env: vec } + } + + pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self { + let mut vec = self.env.clone(); + vec.push((x.clone(), TyEnvItem::Kept(t))); + self.with_vec(vec) + } + pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self { + let mut vec = self.env.clone(); + vec.push((x.clone(), TyEnvItem::Replaced(e))); + self.with_vec(vec) + } + pub fn lookup_var(&self, var: &V) -> Option { + let V(name, idx) = var; + let (idx, (_, item)) = self + .env + .iter() + .rev() + .enumerate() + .filter(|(_, (x, _))| x == name) + .nth(*idx)?; + let ty = match item { + TyEnvItem::Kept(ty) => ty.clone(), + TyEnvItem::Replaced(e) => e.get_type().unwrap(), + }; + Some(TyExpr::new( + TyExprKind::Var(AlphaVar::new(V((), idx))), + Some(ty), + )) + } + pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr { + let idx = self.env.len() - 1 - var.idx(); + match &self.env[idx].1 { + TyEnvItem::Kept(ty) => NzExpr::new( + NzExprKind::Var { var: NzVar { idx } }, + Some(ty.clone()), + ), + TyEnvItem::Replaced(x) => x.clone(), + } + } + pub fn size(&self) -> usize { + self.env.len() + } +} + +impl QuoteEnv { + pub fn new() -> Self { + QuoteEnv { size: 0 } + } + pub fn insert(&self) -> Self { + QuoteEnv { + size: self.size + 1, + } + } + pub fn lookup(&self, var: &NzVar) -> AlphaVar { + AlphaVar::new(V((), self.size - var.idx - 1)) + } +} + +impl TyExpr { + pub fn new(kind: TyExprKind, ty: Option) -> Self { + TyExpr { + kind: Box::new(kind), + ty, + } + } + + pub fn kind(&self) -> &TyExprKind { + self.kind.as_ref() + } + pub fn get_type(&self) -> Result { + match &self.ty { + Some(t) => Ok(t.clone()), + None => Err(TypeError), + } + } + + /// Converts a value back to the corresponding AST expression. + pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + fn tyexpr_to_expr<'a>( + tyexpr: &'a TyExpr, + opts: ToExprOptions, + env: &mut Vec<&'a Binder>, + ) -> NormalizedExpr { + rc(match tyexpr.kind() { + TyExprKind::Var(var) if opts.alpha => { + ExprKind::Var(V("_".into(), var.idx())) + } + TyExprKind::Var(var) => { + let name = env[env.len() - 1 - var.idx()]; + let idx = env + .iter() + .rev() + .take(var.idx()) + .filter(|l| **l == name) + .count(); + ExprKind::Var(V(name.clone(), idx)) + } + TyExprKind::Expr(e) => { + let e = e.map_ref_maybe_binder(|l, tye| { + if let Some(l) = l { + env.push(l); + } + let e = tyexpr_to_expr(tye, opts, env); + if let Some(_) = l { + env.pop(); + } + e + }); + + match e { + ExprKind::Lam(_, t, e) if opts.alpha => { + ExprKind::Lam("_".into(), t, e) + } + ExprKind::Pi(_, t, e) if opts.alpha => { + ExprKind::Pi("_".into(), t, e) + } + e => e, + } + } + }) + } + + tyexpr_to_expr(self, opts, &mut Vec::new()) + } + + pub fn normalize_nf(&self, env: &TyEnv) -> NzExpr { + let kind = match self.kind() { + TyExprKind::Var(var) => return env.lookup_val(var), + TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + NzExprKind::Lam { + binder: binder.clone(), + annot: annot.normalize_nf(env), + env: env.clone(), + body: body.clone(), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + NzExprKind::Pi { + binder: binder.clone(), + annot: annot.normalize_nf(env), + env: env.clone(), + body: body.clone(), + } + } + TyExprKind::Expr(e) => { + let e = e.map_ref(|tye| tye.normalize_nf(env)); + match e { + ExprKind::App(f, arg) => match f.kind() { + NzExprKind::Lam { + binder, env, body, .. + } => { + return body + .normalize_nf(&env.insert_value(binder, arg)) + } + _ => NzExprKind::Expr(ExprKind::App(f, arg)), + }, + _ => NzExprKind::Expr(e), + } + } + }; + let ty = self.ty.clone(); + NzExpr::new(kind, ty) + } + + pub fn normalize(&self) -> NzExpr { + self.normalize_nf(&TyEnv::new()) + } +} + +impl NzExpr { + pub fn new(kind: NzExprKind, ty: Option) -> Self { + NzExpr { + kind: Box::new(kind), + ty: ty.map(Box::new), + } + } + + pub fn kind(&self) -> &NzExprKind { + self.kind.as_ref() + } + pub fn get_type(&self) -> Result { + match &self.ty { + Some(t) => Ok(t.as_ref().clone()), + None => Err(TypeError), + } + } + + pub fn quote(&self, qenv: QuoteEnv) -> TyExpr { + let ty = self.ty.as_ref().map(|t| (**t).clone()); + let kind = match self.kind.as_ref() { + NzExprKind::Var { var } => TyExprKind::Var(qenv.lookup(var)), + NzExprKind::Lam { + binder, + annot, + env, + body, + } => TyExprKind::Expr(ExprKind::Lam( + binder.clone(), + annot.quote(qenv), + body.normalize_nf(&env.insert_type(binder, annot.clone())) + .quote(qenv.insert()), + )), + NzExprKind::Pi { + binder, + annot, + env, + body, + } => TyExprKind::Expr(ExprKind::Pi( + binder.clone(), + annot.quote(qenv), + body.normalize_nf(&env.insert_type(binder, annot.clone())) + .quote(qenv.insert()), + )), + NzExprKind::Expr(e) => { + TyExprKind::Expr(e.map_ref(|nze| nze.quote(qenv))) + } // NzExprKind::Unevaled { env, expr } => { + // return TyExpr::new(expr.clone(), ty.clone()) + // .normalize_nf(env) + // .quote(qenv) + // } + }; + TyExpr::new(kind, ty) + } + pub fn to_expr(&self) -> NormalizedExpr { + self.quote(QuoteEnv::new()).to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) + } +} + +/// Type-check an expression and return the expression alongside its type if type-checking +/// succeeded, or an error if type-checking failed. +fn type_with(env: &TyEnv, e: Expr) -> Result { + match e.as_ref() { + ExprKind::Var(var) => match env.lookup_var(&var) { + Some(x) => Ok(x), + None => Err(TypeError), + }, + ExprKind::Lam(binder, annot, body) => { + let annot = type_with(env, annot.clone())?; + let annot_nf = annot.normalize_nf(env); + let body = type_with( + &env.insert_type(&binder, annot_nf.clone()), + body.clone(), + )?; + let ty = NzExpr::new( + NzExprKind::Pi { + binder: binder.clone(), + annot: annot_nf, + env: env.clone(), + body: body.get_type()?.quote(env.to_quoteenv()), + }, + None, // TODO: function_check + ); + Ok(TyExpr::new( + TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), + Some(ty), + )) + } + ExprKind::Pi(binder, annot, body) => { + let annot = type_with(env, annot.clone())?; + let annot_nf = annot.normalize_nf(env); + let body = type_with( + &env.insert_type(&binder, annot_nf.clone()), + body.clone(), + )?; + Ok(TyExpr::new( + TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), + None, // TODO: function_check + )) + } + ExprKind::App(f, arg) => { + let f = type_with(env, f.clone())?; + let arg = type_with(env, arg.clone())?; + let tf = f.get_type()?; + let (binder, _expected_arg_ty, body_env, body_ty) = match tf.kind() + { + NzExprKind::Pi { + binder, + annot, + env, + body, + } => (binder, annot, env, body), + _ => return Err(TypeError), + }; + // if arg.get_type()? != *expected_arg_ty { + // return Err(TypeError); + // } + + let arg_nf = arg.normalize_nf(env); + let ty = + body_ty.normalize_nf(&body_env.insert_value(&binder, arg_nf)); + + Ok(TyExpr::new( + TyExprKind::Expr(ExprKind::App(f, arg)), + Some(ty), + )) + } + e => Ok(TyExpr::new( + TyExprKind::Expr(e.traverse_ref(|e| type_with(env, e.clone()))?), + None, + )), + } +} + +pub(crate) fn typecheck(e: Expr) -> Result { + type_with(&TyEnv::new(), e) +} diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 36cae04..72f5b1d 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -11,15 +11,17 @@ use crate::syntax::{ExprKind, Label, Span, V}; pub(crate) type Type = Value; // An expression with inferred types at every node and resolved variables. +#[derive(Debug, Clone)] pub(crate) struct TyExpr { kind: Box, ty: Option, span: Span, } +#[derive(Debug, Clone)] pub(crate) enum TyExprKind { Var(AlphaVar), - // Forbidden ExprKind variants: Var + // Forbidden ExprKind variants: Var, Import, Embed Expr(ExprKind), } @@ -63,12 +65,12 @@ fn tyexpr_to_expr<'a>( } TyExprKind::Var(v) => { let name = ctx[ctx.len() - 1 - v.idx()]; - let mut idx = 0; - for l in ctx.iter().rev().take(v.idx()) { - if *l == name { - idx += 1; - } - } + let idx = ctx + .iter() + .rev() + .take(v.idx()) + .filter(|l| **l == name) + .count(); ExprKind::Var(V(name.clone(), idx)) } TyExprKind::Expr(e) => { diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f1648cf..d86574a 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,9 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - let expr = - parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - let ty = expr.get_type()?.to_expr(); + // let expr = + // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + // let ty = expr.get_type()?.to_expr(); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; + let ty = tyexpr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -203,9 +206,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - let expr = parse_file_str(&expr_file_path)? - .resolve()? - .typecheck()? + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .normalize() + // .to_expr(); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let expr = crate::semantics::nze::nzexpr::typecheck(expr)? .normalize() .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); -- cgit v1.3.1 From 015b24b04128cbf5a60fbc8ac3f526306ca27378 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 17:43:44 +0000 Subject: Simplify type error type --- dhall/src/error/mod.rs | 13 ++++------- dhall/src/semantics/core/value.rs | 3 +-- dhall/src/semantics/phase/typecheck.rs | 42 ++++++++++------------------------ dhall/src/semantics/tck/tyexpr.rs | 3 +-- dhall/src/tests.rs | 26 ++++++++++----------- 5 files changed, 31 insertions(+), 56 deletions(-) (limited to 'dhall/src/error') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 844a3e4..5595c53 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,5 @@ use std::io::Error as IOError; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; @@ -37,11 +36,10 @@ pub enum EncodeError { CBORError(serde_cbor::error::Error), } -/// A structured type error that includes context +/// A structured type error #[derive(Debug)] pub struct TypeError { message: TypeMessage, - context: TyCtx, } /// The specific type error @@ -88,11 +86,8 @@ pub(crate) enum TypeMessage { } impl TypeError { - pub(crate) fn new(context: &TyCtx, message: TypeMessage) -> Self { - TypeError { - context: context.clone(), - message, - } + pub(crate) fn new(message: TypeMessage) -> Self { + TypeError { message } } } @@ -100,7 +95,7 @@ impl std::fmt::Display for TypeError { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; let msg = match &self.message { - UnboundVariable(span) => span.error("Type error: Unbound variable"), + UnboundVariable(var) => var.error("Type error: Unbound variable"), InvalidInputType(v) => { v.span().error("Type error: Invalid function input") } diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index f470019..dc6a116 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -3,7 +3,6 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; @@ -438,7 +437,7 @@ impl ValueInternal { fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), - None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + None => Err(TypeError::new(TypeMessage::Sort)), } } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 15025c1..9e41f1e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -14,27 +14,20 @@ use crate::syntax::{ }; fn tck_pi_type( - ctx: &TyCtx, binder: Binder, tx: Value, te: Value, ) -> Result { use TypeMessage::*; - let ctx2 = ctx.insert_type(&binder, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), + _ => return Err(TypeError::new(InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - &ctx2, - InvalidOutputType(te.get_type()?), - )) - } + _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))), }; let k = function_check(ka, kb); @@ -46,7 +39,6 @@ fn tck_pi_type( } fn tck_record_type( - ctx: &TyCtx, kts: impl IntoIterator>, ) -> Result { use std::collections::hash_map::Entry; @@ -59,13 +51,13 @@ fn tck_record_type( // Construct the union of the contained `Const`s match t.get_type()?.as_const() { Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), + None => return Err(TypeError::new(InvalidFieldType(x, t))), } // Check for duplicated entries let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, RecordTypeDuplicateField)) + return Err(TypeError::new(RecordTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -77,7 +69,7 @@ fn tck_record_type( )) } -fn tck_union_type(ctx: &TyCtx, kts: Iter) -> Result +fn tck_union_type(kts: Iter) -> Result where Iter: IntoIterator), TypeError>>, { @@ -93,17 +85,14 @@ where (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x, t.clone()), - )) + return Err(TypeError::new(InvalidFieldType(x, t.clone()))) } } } let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, UnionTypeDuplicateField)) + return Err(TypeError::new(UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -313,7 +302,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let body_type = body.get_type()?; Ok(Value::from_kind_and_type( ValueKind::Lam(binder.clone(), annot.clone(), body), - tck_pi_type(ctx, binder, annot, body_type)?, + tck_pi_type(binder, annot, body_type)?, )) } Pi(x, ta, tb) => { @@ -321,7 +310,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(&binder, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(ctx, binder, ta, tb) + tck_pi_type(binder, ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -337,9 +326,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), - None => { - Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span))) - } + None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), }, e => { // Typecheck recursively all subexpressions @@ -364,7 +351,7 @@ fn type_last_layer( use syntax::Const::Type; use syntax::ExprKind::*; use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); + let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); /// Intermediary return type enum Ret { @@ -474,15 +461,12 @@ fn type_last_layer( RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) } RecordType(kts) => RetWhole(tck_record_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), UnionType(kts) => RetWhole(tck_union_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), RecordLit(kvs) => RetTypeOnly(tck_record_type( - ctx, kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), )?), Field(r, x) => { @@ -502,7 +486,6 @@ fn type_last_layer( Some(Some(t)) => { RetTypeOnly( tck_pi_type( - ctx, ctx.new_binder(x), t.clone(), r.under_binder(), @@ -577,7 +560,6 @@ fn type_last_layer( // Construct the final record type from the union RetTypeOnly(tck_record_type( - ctx, kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), )?) } @@ -627,7 +609,7 @@ fn type_last_layer( }, )?; - RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) + RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 72f5b1d..983f3f8 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,5 @@ #![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -40,7 +39,7 @@ impl TyExpr { pub fn get_type(&self) -> Result { match &self.ty { Some(t) => Ok(t.clone()), - None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + None => Err(TypeError::new(TypeMessage::Sort)), } } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index d86574a..7795d17 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,12 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - // let expr = - // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - // let ty = expr.get_type()?.to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; - let ty = tyexpr.get_type()?.to_expr(); + let expr = + parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + let ty = expr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; + // let ty = tyexpr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -206,15 +206,15 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .normalize() - // .to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + let expr = parse_file_str(&expr_file_path)? + .resolve()? + .typecheck()? .normalize() .to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + // .normalize() + // .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.3.1 From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:15:17 +0000 Subject: Typecheck more cases --- dhall/src/error/mod.rs | 1 + dhall/src/semantics/phase/normalize.rs | 13 ++- dhall/src/semantics/phase/typecheck.rs | 11 +- dhall/src/semantics/tck/typecheck.rs | 187 +++++++++++++++++++++++---------- dhall/src/tests.rs | 15 ++- 5 files changed, 165 insertions(+), 62 deletions(-) (limited to 'dhall/src/error') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5595c53..850a792 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -83,6 +83,7 @@ pub(crate) enum TypeMessage { EquivalenceTypeMismatch(Value, Value), AssertMismatch(Value, Value), AssertMustTakeEquivalence, + Custom(String), } impl TypeError { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index e848601..066a004 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -625,12 +625,14 @@ pub(crate) fn normalize_one_layer( // `RetWhole`), so they won't appear here. ExprKind::Lam(_, _, _) | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) => { + | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Let(_, _, val, body) => { + Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) + } + ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), @@ -895,11 +897,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { closure: Closure::new(env, body.clone()), } } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.normalize_whnf(env); + return body.normalize_whnf(&env.insert_value(val)); + } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); normalize_one_layer(e, &ty) } }; + // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f2d1bf2..0f3754e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -189,7 +189,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr { +pub(crate) fn type_of_builtin(b: Builtin) -> Expr { use syntax::Builtin::*; rc(match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -321,7 +321,14 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let v = type_with(ctx, v)?; let binder = ctx.new_binder(x); - type_with(&ctx.insert_value(&binder, v.clone())?, e.clone()) + let e = + type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?; + // let e_ty = e.get_type()?; + // Ok(Value::from_kind_and_type( + // ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)), + // e_ty, + // )) + Ok(e) } Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index aab5f83..046c999 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -10,6 +10,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::nze::{NameEnv, QuoteEnv}; use crate::semantics::phase::normalize::{merge_maps, NzEnv}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, const_to_value, type_of_builtin, +}; use crate::semantics::phase::Normalized; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind, @@ -55,93 +58,171 @@ impl TyEnv { items: self.items.insert_value(e), } } - pub fn lookup_var(&self, var: &V