Skip to content

Commit

Permalink
Avoid recomputing universes in tck
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Feb 16, 2020
1 parent 80722b6 commit c451c18
Show file tree
Hide file tree
Showing 7 changed files with 97 additions and 59 deletions.
6 changes: 3 additions & 3 deletions dhall/src/semantics/nze/value.rs
View file
Expand Up @@ -4,7 +4,7 @@ use std::rc::Rc;
use crate::semantics::nze::lazy;
use crate::semantics::{
apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
Expand Down Expand Up @@ -139,8 +139,8 @@ impl Value {
self.0.kind()
}

pub(crate) fn to_type(&self) -> Type {
self.clone().into()
pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
Type::new(self.clone(), u.into())
}
/// Converts a value back to the corresponding AST expression.
pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
Expand Down
49 changes: 25 additions & 24 deletions dhall/src/semantics/tck/tyexpr.rs
View file
Expand Up @@ -11,6 +11,7 @@ pub(crate) struct Universe(u8);
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) struct Type {
val: Value,
univ: Universe,
}

/// A hir expression plus its inferred type.
Expand Down Expand Up @@ -39,18 +40,28 @@ impl Universe {
pub fn next(self) -> Self {
Universe(self.0 + 1)
}
pub fn previous(self) -> Option<Self> {
if self.0 == 0 {
None
} else {
Some(Universe(self.0 - 1))
}
}
}

impl Type {
pub fn new(val: Value, _u: Universe) -> Self {
Type { val }
pub fn new(val: Value, univ: Universe) -> Self {
Type { val, univ }
}
/// Creates a new Type and infers its universe by re-typechecking its value.
/// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
/// PiClosure.
pub fn new_infer_universe(
env: &TyEnv,
val: Value,
) -> Result<Self, TypeError> {
let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
let u = match c {
Some(c) => c.to_universe(),
None => unreachable!(
"internal type error: this is not a type: {:?}",
val
),
};
Ok(Type::new(val, u))
}
pub fn from_const(c: Const) -> Self {
Self::new(Value::from_const(c), c.to_universe().next())
Expand All @@ -66,18 +77,8 @@ impl Type {
}

/// Get the type of this type
// TODO: avoid recomputing so much
pub fn ty(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const())
}
/// Get the type of this type
// TODO: avoid recomputing so much
pub fn ty_univ(&self, env: &TyEnv) -> Result<Universe, TypeError> {
Ok(match self.ty(env)? {
Some(c) => c.to_universe(),
// TODO: hack, might explode
None => Const::Sort.to_universe().next(),
})
pub fn ty(&self) -> Universe {
self.univ
}

pub fn to_value(&self) -> Value {
Expand Down Expand Up @@ -184,8 +185,8 @@ impl TyExpr {
}
}

impl From<Value> for Type {
fn from(x: Value) -> Type {
Type { val: x }
impl From<Const> for Universe {
fn from(x: Const) -> Universe {
Universe::from_const(x)
}
}
73 changes: 45 additions & 28 deletions dhall/src/semantics/tck/typecheck.rs
View file
Expand Up @@ -136,24 +136,30 @@ fn type_one_layer(
return span_err("InvalidListElement");
}
}
if x.ty().ty(env)? != Some(Const::Type) {
if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidListType");
}

let t = x.ty().to_value();
Value::from_builtin(Builtin::List).app(t).to_type()
Value::from_builtin(Builtin::List)
.app(t)
.to_type(Const::Type)
}
ExprKind::SomeLit(x) => {
if x.ty().ty(env)? != Some(Const::Type) {
if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidOptionalType");
}

let t = x.ty().to_value();
Value::from_builtin(Builtin::Optional).app(t).to_type()
Value::from_builtin(Builtin::Optional)
.app(t)
.to_type(Const::Type)
}
ExprKind::RecordLit(kvs) => {
use std::collections::hash_map::Entry;
let mut kts = HashMap::new();
// An empty record type has type Type
let mut k = Const::Type;
for (x, v) in kvs {
// Check for duplicated entries
match kts.entry(x.clone()) {
Expand All @@ -164,13 +170,13 @@ fn type_one_layer(
};

// Check that the fields have a valid kind
match v.ty().ty(env)? {
Some(_) => {}
match v.ty().ty().as_const() {
Some(c) => k = max(k, c),
None => return span_err("InvalidFieldType"),
}
}

Value::from_kind(ValueKind::RecordType(kts)).to_type()
Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
Expand Down Expand Up @@ -226,29 +232,31 @@ fn type_one_layer(
ExprKind::Field(scrut, x) => {
match scrut.ty().kind() {
ValueKind::RecordType(kts) => match kts.get(&x) {
Some(val) => val.clone().to_type(),
Some(val) => Type::new_infer_universe(env, val.clone())?,
None => return span_err("MissingRecordField"),
},
// TODO: branch here only when scrut.ty() is a Const
_ => {
let scrut_nf = scrut.eval(env);
match scrut_nf.kind() {
ValueKind::Const(_) => {
let scrut = scrut.eval_to_type(env)?;
match scrut.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
Value::from_kind(ValueKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
closure: Closure::new_constant(scrut_nf),
closure: Closure::new_constant(
scrut.to_value(),
),
})
.to_type()
.to_type(scrut.ty())
}
Some(None) => scrut_nf.to_type(),
Some(None) => scrut,
None => return span_err("MissingUnionField"),
},
_ => return span_err("NotARecord"),
}
} // _ => span_err("NotARecord"),
}
_ => return span_err("NotARecord"),
}
}
ExprKind::Assert(t) => {
Expand Down Expand Up @@ -295,7 +303,7 @@ fn type_one_layer(
}

let arg_nf = arg.eval(env);
closure.apply(arg_nf).to_type()
Type::new_infer_universe(env, closure.apply(arg_nf))?
}
_ => return mkerr(
ErrorBuilder::new(format!(
Expand All @@ -314,7 +322,7 @@ fn type_one_layer(
if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
if y.ty().ty(env)? != Some(Const::Type) {
if y.ty().ty().as_const() != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
if y.ty() != z.ty() {
Expand Down Expand Up @@ -344,7 +352,8 @@ fn type_one_layer(
Ok(r_t.clone())
})?;

Value::from_kind(ValueKind::RecordType(kts)).to_type()
let u = max(x.ty().ty(), y.ty().ty());
Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
Expand All @@ -357,8 +366,8 @@ fn type_one_layer(
)),
span.clone(),
);
let x_u = x.ty().ty_univ(env)?;
let y_u = y.ty().ty_univ(env)?;
let x_u = x.ty().ty();
let y_u = y.ty().ty();
Type::new(hir.eval(env), max(x_u, y_u))
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
Expand Down Expand Up @@ -388,7 +397,7 @@ fn type_one_layer(
if l.ty() != r.ty() {
return span_err("EquivalenceTypeMismatch");
}
if l.ty().ty(env)? != Some(Const::Type) {
if l.ty().ty().as_const() != Some(Const::Type) {
return span_err("EquivalenceArgumentsMustBeTerms");
}

Expand Down Expand Up @@ -480,8 +489,11 @@ fn type_one_layer(
);
}

// TODO: this actually doesn't check anything yet
match closure.remove_binder() {
Ok(v) => v.to_type(),
Ok(v) => {
Type::new_infer_universe(env, v.clone())?
}
Err(()) => {
return span_err(
"MergeReturnTypeIsDependent",
Expand Down Expand Up @@ -525,7 +537,9 @@ fn type_one_layer(
}
},
// Union alternative without type
Some(None) => handler_type.clone().to_type(),
Some(None) => {
Type::new_infer_universe(env, handler_type.clone())?
}
None => return span_err("MergeHandlerMissingVariant"),
};
match &inferred_type {
Expand Down Expand Up @@ -560,7 +574,7 @@ fn type_one_layer(
}
}
ExprKind::ToMap(record, annot) => {
if record.ty().ty(env)? != Some(Const::Type) {
if record.ty().ty().as_const() != Some(Const::Type) {
return span_err("`toMap` only accepts records of type `Type`");
}
let record_t = record.ty();
Expand Down Expand Up @@ -623,7 +637,7 @@ fn type_one_layer(
kts.insert("mapValue".into(), entry_type);
let output_type: Type = Value::from_builtin(Builtin::List)
.app(Value::from_kind(ValueKind::RecordType(kts)))
.to_type();
.to_type(Const::Type);
if let Some(annot) = annot {
let annot_val = annot.eval_to_type(env)?;
if output_type != annot_val {
Expand Down Expand Up @@ -656,7 +670,10 @@ fn type_one_layer(
};
}

Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
Type::new_infer_universe(
env,
Value::from_kind(ValueKind::RecordType(new_kts)),
)?
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.ty();
Expand Down Expand Up @@ -721,7 +738,7 @@ pub(crate) fn type_with(
let body = type_with(&body_env, body, None)?;

let u_annot = annot.ty().as_const().unwrap();
let u_body = match body.ty().ty(&body_env)? {
let u_body = match body.ty().ty().as_const() {
Some(k) => k,
_ => return mk_span_err(hir.span(), "Invalid output type"),
};
Expand Down
7 changes: 6 additions & 1 deletion dhall/tests/type-inference/failure/recordOfKind.txt
View file
@@ -1 +1,6 @@
Type error: error: Sort does not have a type
Type error: error: InvalidFieldType
--> <current file>:1:0
|
1 | { a = Kind }
| ^^^^^^^^^^^^ InvalidFieldType
|
7 changes: 6 additions & 1 deletion dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
View file
@@ -1 +1,6 @@
Type error: error: Sort does not have a type
Type error: error: InvalidFieldType
--> <current file>:1:0
|
1 | { x = Type, y = Kind }
| ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
|
7 changes: 6 additions & 1 deletion dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
View file
@@ -1 +1,6 @@
Type error: error: Sort does not have a type
Type error: error: InvalidFieldType
--> <current file>:1:15
|
1 | { x = Bool } ⫽ { x = Kind }
| ^^^^^^^^^^^^ InvalidFieldType
|
7 changes: 6 additions & 1 deletion dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
View file
@@ -1 +1,6 @@
Type error: error: Sort does not have a type
Type error: error: InvalidFieldType
--> <current file>:1:14
|
1 | { x = {=} } ⫽ { x = Kind }
| ^^^^^^^^^^^^ InvalidFieldType
|

0 comments on commit c451c18

Please sign in to comment.