summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2020-02-13 20:17:41 +0000
committerNadrieril2020-02-13 20:17:41 +0000
commitf29a40fb55b898b3a3cc51f198e8522eaecf0777 (patch)
treeba31bed1f166c8fc0f448b477548cceeb5e4f8ef /dhall/src
parent7b649b8647c60f1c02050805520f307edff0a94f (diff)
Simplify conversions to/from TyExpr
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/hir.rs8
-rw-r--r--dhall/src/semantics/nze/value.rs20
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs11
-rw-r--r--dhall/src/semantics/tck/typecheck.rs157
4 files changed, 88 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<TyExpr, TypeError> {
+ 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<Value, TypeError> {
- self.to_tyexpr_tyenv(tyenv).get_type()
- }
-
pub fn to_hir(&self, venv: VarEnv) -> Hir {
let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
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<TyExpr, TypeError> {
- 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<Option<Const>, 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<Item = Cow<'a, TyExpr>>,
-) -> Result<Type, TypeError> {
- 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<T, S: ToString>(x: S) -> Result<T, TypeError> {
- Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
+ Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
+}
+
+pub fn mk_span_err<T, S: ToString>(
+ span: &Span,
+ msg: S,
+) -> Result<T, TypeError> {
+ 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<TyExpr>,
span: Span,
) -> Result<TyExpr, TypeError> {
- 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(