summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/hir.rs4
-rw-r--r--dhall/src/semantics/nze/normalize.rs2
-rw-r--r--dhall/src/semantics/nze/value.rs4
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs12
-rw-r--r--dhall/src/semantics/tck/typecheck.rs118
5 files changed, 88 insertions, 52 deletions
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index e4e2a5f..42f151e 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -76,8 +76,8 @@ impl Hir {
}
/// 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())
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+ Value::new_thunk(env.into(), self.clone())
}
/// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 4111190..c8dd5ae 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -475,7 +475,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
}
HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
- body.eval(&env.insert_value(val, ())).kind().clone()
+ body.eval(env.insert_value(val, ())).kind().clone()
}
HirKind::Expr(e) => {
let e = e.map_ref(|hir| hir.eval(env));
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 0603fb5..3a5b5b5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -87,7 +87,7 @@ pub(crate) enum ValueKind {
UnionLit(Label, Value, HashMap<Label, Option<Value>>),
TextLit(TextLit),
Equivalence(Value, Value),
- /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
+ /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
PartialExpr(ExprKind<Value>),
}
@@ -387,7 +387,7 @@ impl Closure {
pub fn apply(&self, val: Value) -> Value {
match self {
Closure::Closure { env, body, .. } => {
- body.eval(&env.insert_value(val, ()))
+ body.eval(env.insert_value(val, ()))
}
Closure::ConstantClosure { body, .. } => body.clone(),
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c7b8009..dfb4397 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -26,13 +26,15 @@ impl TyExpr {
pub fn ty(&self) -> &Type {
&self.ty
}
- pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
- Ok(self.ty().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)?.ty().as_const())
+ Ok(self
+ .ty()
+ .to_hir(env.as_varenv())
+ .typecheck(env)?
+ .ty()
+ .as_const())
}
pub fn to_hir(&self) -> Hir {
@@ -48,7 +50,7 @@ impl TyExpr {
/// Eval the TyExpr. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
- self.as_hir().eval(&env.into())
+ self.as_hir().eval(env.into())
}
/// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 377b97e..a8a2d95 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -12,6 +12,38 @@ use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
};
+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.clone(),
+ "RecordTypeMergeRequiresRecordType",
+ )
+ }
+ };
+ let kts_y = match y.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => {
+ return mk_span_err(
+ span.clone(),
+ "RecordTypeMergeRequiresRecordType",
+ )
+ }
+ };
+ for (k, tx) in kts_x {
+ if let Some(ty) = kts_y.get(k) {
+ check_rectymerge(span, env, tx.clone(), ty.clone())?;
+ }
+ }
+ Ok(())
+}
+
fn function_check(a: Const, b: Const) -> Const {
if b == Const::Type {
Const::Type
@@ -51,11 +83,39 @@ fn type_one_layer(
| ExprKind::Annot(..) => unreachable!(), // Handled in type_with
ExprKind::Lam(binder, annot, body) => {
- 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, None, Span::Artificial)?.eval(env)
+ if annot.ty().as_const().is_none() {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Invalid input type: `{}`",
+ annot.ty().to_expr_tyenv(env),
+ ))
+ .span_err(
+ annot.span(),
+ format!(
+ "this has type: `{}`",
+ annot.ty().to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "The input type of a function must have type `Type`, \
+ `Kind` or `Sort`",
+ ))
+ .format(),
+ );
+ }
+ let body_env = env.insert_type(&binder, annot.eval(env));
+ if body.get_kind(&body_env)?.is_none() {
+ return span_err("Invalid output type");
+ }
+ Hir::new(
+ HirKind::Expr(ExprKind::Pi(
+ binder.clone(),
+ annot.to_hir(),
+ body.ty().to_hir(body_env.as_varenv()),
+ )),
+ span.clone(),
+ )
+ .eval(env)
}
ExprKind::Pi(_, annot, body) => {
let ks = match annot.ty().as_const() {
@@ -348,45 +408,19 @@ fn type_one_layer(
Value::from_kind(ValueKind::RecordType(kts))
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
- let ekind = ExprKind::BinOp(
- BinOp::RecursiveRecordTypeMerge,
- x.get_type_tyexpr(env)?,
- y.get_type_tyexpr(env)?,
- );
- type_one_layer(env, ekind, None, span.clone())?.eval(env)
+ check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
+
+ Hir::new(
+ HirKind::Expr(ExprKind::BinOp(
+ BinOp::RecursiveRecordTypeMerge,
+ x.ty().to_hir(env.as_varenv()),
+ y.ty().to_hir(env.as_varenv()),
+ )),
+ span.clone(),
+ )
+ .eval(env)
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
- 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.clone(),
- "RecordTypeMergeRequiresRecordType",
- )
- }
- };
- let kts_y = match y.kind() {
- ValueKind::RecordType(kts) => kts,
- _ => {
- return mk_span_err(
- span.clone(),
- "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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:06:03 +0000