From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:17:41 +0000 Subject: Simplify conversions to/from TyExpr --- dhall/src/semantics/hir.rs | 8 +- dhall/src/semantics/nze/value.rs | 20 +-- dhall/src/semantics/tck/tyexpr.rs | 11 +- dhall/src/semantics/tck/typecheck.rs | 157 +++++++++------------ .../unit/RecursiveRecordMergeLhsNotRecord.txt | 5 + .../unit/RecursiveRecordMergeOverlapping.txt | 5 + .../unit/RecursiveRecordMergeRhsNotRecord.txt | 5 + .../unit/RecursiveRecordTypeMergeOverlapping.txt | 5 + 8 files changed, 108 insertions(+), 108 deletions(-) diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index 288031c..f91aa73 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -1,5 +1,6 @@ #![allow(dead_code)] -use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; +use crate::error::TypeError; +use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -69,6 +70,11 @@ impl Hir { hir_to_expr(self, opts, &mut env) } + /// Typecheck the Hir. + pub fn typecheck(&self, env: &TyEnv) -> Result { + type_with(env, self) + } + /// Eval the Hir. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: &NzEnv) -> Value { Value::new_thunk(env.clone(), self.clone()) diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 2ae6852..0603fb5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,12 +1,10 @@ use std::collections::HashMap; use std::rc::Rc; -use crate::error::TypeError; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, - type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, - TyExpr, VarEnv, + apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, + BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, @@ -146,8 +144,7 @@ impl Value { if opts.normalize { self.normalize(); } - - self.to_tyexpr_noenv().to_expr(opts) + self.to_hir_noenv().to_expr(opts) } pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) @@ -161,10 +158,6 @@ impl Value { Value::from_kind(apply_any(self.clone(), v)) } - pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result { - self.to_tyexpr_tyenv(tyenv).get_type() - } - pub fn to_hir(&self, venv: VarEnv) -> Hir { let map_uniontype = |kts: &HashMap>| { ExprKind::UnionType( @@ -270,13 +263,6 @@ impl Value { pub fn to_hir_noenv(&self) -> Hir { self.to_hir(VarEnv::new()) } - pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { - let hir = self.to_hir(tyenv.as_varenv()); - type_with(tyenv, &hir).unwrap() - } - pub fn to_tyexpr_noenv(&self) -> TyExpr { - self.to_tyexpr_tyenv(&TyEnv::new()) - } } impl ValueInternal { diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index b49ea3e..dc14cd2 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,6 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv}; -use crate::syntax::Span; +use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value}; +use crate::syntax::{Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; @@ -33,7 +33,12 @@ impl TyExpr { } } pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { - Ok(self.get_type()?.to_tyexpr_tyenv(env)) + Ok(self.get_type()?.to_hir(env.as_varenv()).typecheck(env)?) + } + /// Get the kind (the type of the type) of this value + // TODO: avoid recomputing so much + pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { + Ok(self.get_type_tyexpr(env)?.get_type()?.as_const()) } pub fn to_hir(&self) -> Hir { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c854552..794edcf 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -12,28 +12,6 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, }; -fn type_of_recordtype<'a>( - span: Span, - tys: impl Iterator>, -) -> Result { - let span_err = |msg: &str| { - mkerr( - ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) - .format(), - ) - }; - // An empty record type has type Type - let mut k = Const::Type; - for t in tys { - match t.get_type()?.as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } - } - Ok(Value::from_const(k)) -} - fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { Const::Type @@ -42,8 +20,19 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub fn mkerr(x: S) -> Result { - Err(TypeError::new(TypeMessage::Custom(x.to_string()))) +pub fn mkerr(msg: S) -> Result { + Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) +} + +pub fn mk_span_err( + span: &Span, + msg: S, +) -> Result { + mkerr( + ErrorBuilder::new(msg.to_string()) + .span_err(span.clone(), msg.to_string()) + .format(), + ) } /// When all sub-expressions have been typed, check the remaining toplevel @@ -53,13 +42,7 @@ fn type_one_layer( ekind: ExprKind, span: Span, ) -> Result { - let span_err = |msg: &str| { - mkerr( - ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) - .format(), - ) - }; + let span_err = |msg: &str| mk_span_err(&span, msg); let ty = match &ekind { ExprKind::Import(..) => unreachable!( @@ -68,10 +51,9 @@ fn type_one_layer( ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { - let body_ty = body.get_type()?; - let body_ty = body_ty.to_tyexpr_tyenv( + let body_ty = body.get_type_tyexpr( &env.insert_type(&binder.clone(), annot.eval(env)), - ); + )?; let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env) } @@ -157,19 +139,19 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - let t = x.get_type()?; - if t.get_type(env)?.as_const() != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidListType"); } + let t = x.get_type()?; Value::from_builtin(Builtin::List).app(t) } ExprKind::SomeLit(x) => { - let t = x.get_type()?; - if t.get_type(env)?.as_const() != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } + let t = x.get_type()?; Value::from_builtin(Builtin::Optional).app(t) } ExprKind::RecordLit(kvs) => { @@ -183,18 +165,23 @@ fn type_one_layer( } Entry::Vacant(e) => e.insert(v.get_type()?), }; + + // Check that the fields have a valid kind + match v.get_kind(env)? { + Some(_) => {} + None => return span_err("InvalidFieldType"), + } } - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), - )?; Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; let mut seen_fields = HashMap::new(); - for (x, _) in kts { + // An empty record type has type Type + let mut k = Const::Type; + + for (x, t) in kts { // Check for duplicated entries match seen_fields.entry(x.clone()) { Entry::Occupied(_) => { @@ -202,12 +189,15 @@ fn type_one_layer( } Entry::Vacant(e) => e.insert(()), }; + + // Check the type is a Const and compute final type + match t.get_type()?.as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } } - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Borrowed(t)), - )? + Value::from_const(k) } ExprKind::UnionType(kts) => { use std::collections::hash_map::Entry; @@ -337,9 +327,7 @@ fn type_one_layer( if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - let y_ty = y.get_type()?; - let y_ty = y_ty.to_tyexpr_tyenv(env); - if y_ty.get_type()?.as_const() != Some(Const::Type) { + if y.get_kind(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { @@ -369,45 +357,44 @@ fn type_one_layer( Ok(r_t.clone()) })?; - // Construct the final record type - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), - )?; Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type()?.to_tyexpr_tyenv(env), - y.get_type()?.to_tyexpr_tyenv(env), + x.get_type_tyexpr(env)?, + y.get_type_tyexpr(env)?, ); - type_one_layer(env, ekind, Span::Artificial)?.eval(env) + type_one_layer(env, ekind, span.clone())?.eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - let x_val = x.eval(env); - let y_val = y.eval(env); - let kts_x = match x_val.kind() { - ValueKind::RecordType(kts) => kts, - _ => return span_err("RecordTypeMergeRequiresRecordType"), - }; - let kts_y = match y_val.kind() { - ValueKind::RecordType(kts) => kts, - _ => return span_err("RecordTypeMergeRequiresRecordType"), - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - type_one_layer( - env, - ExprKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - tx.to_tyexpr_tyenv(env), - ty.to_tyexpr_tyenv(env), - ), - Span::Artificial, - )?; + fn check_rectymerge( + span: &Span, + env: &TyEnv, + x: Type, + y: Type, + ) -> Result<(), TypeError> { + let kts_x = match x.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + }; + let kts_y = match y.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + }; + for (k, tx) in kts_x { + if let Some(ty) = kts_y.get(k) { + check_rectymerge( + span, + env, + tx.clone(), + ty.clone(), + )?; + } } + Ok(()) } + check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const let xk = x.get_type()?.as_const().unwrap(); @@ -434,9 +421,7 @@ fn type_one_layer( if l.get_type()? != r.get_type()? { return span_err("EquivalenceTypeMismatch"); } - if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const() - != Some(Const::Type) - { + if l.get_kind(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -605,6 +590,9 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { + if record.get_kind(env)? != Some(Const::Type) { + return span_err("`toMap` only accepts records of type `Type`"); + } let record_t = record.get_type()?; let kts = match record_t.kind() { ValueKind::RecordType(kts) => kts, @@ -652,11 +640,6 @@ fn type_one_layer( annot_val } else { let entry_type = kts.iter().next().unwrap().1.clone(); - if entry_type.get_type(env)?.as_const() != Some(Const::Type) { - return span_err( - "`toMap` only accepts records of type `Type`", - ); - } for (_, t) in kts.iter() { if *t != entry_type { return span_err( diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt index f74e839..02cf64f 100644 --- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt +++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt @@ -1 +1,6 @@ Type error: error: RecordTypeMergeRequiresRecordType + --> :1:0 + | +1 | True ∧ {=} + | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType + | diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt index f74e839..202a3e5 100644 --- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt +++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt @@ -1 +1,6 @@ Type error: error: RecordTypeMergeRequiresRecordType + --> :1:0 + | +1 | { x = True } ∧ { x = False } + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType + | diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt index f74e839..a0b4676 100644 --- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt +++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt @@ -1 +1,6 @@ Type error: error: RecordTypeMergeRequiresRecordType + --> :1:0 + | +1 | {=} ∧ True + | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType + | diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt index f74e839..769712b 100644 --- a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt +++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt @@ -1 +1,6 @@ Type error: error: RecordTypeMergeRequiresRecordType + --> :1:0 + | +1 | { x : Bool } ⩓ { x : Natural } + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType + | -- cgit v1.2.3