summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/error/mod.rs13
-rw-r--r--dhall/src/semantics/core/value.rs3
-rw-r--r--dhall/src/semantics/phase/typecheck.rs42
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs3
-rw-r--r--dhall/src/tests.rs26
5 files changed, 31 insertions, 56 deletions
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<Value, TypeError> {
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<Item = Result<(Label, Value), TypeError>>,
) -> Result<Value, TypeError> {
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<Iter>(ctx: &TyCtx, kts: Iter) -> Result<Value, TypeError>
+fn tck_union_type<Iter>(kts: Iter) -> Result<Value, TypeError>
where
Iter: IntoIterator<Item = Result<(Label, Option<Value>), 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<Normalized>) -> Result<Value, TypeError> {
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<Normalized>) -> Result<Value, TypeError> {
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<Normalized>) -> Result<Value, TypeError> {
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<Type, TypeError> {
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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 02:10:15 +0000