summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-01-29 18:48:19 +0000
committerNadrieril2020-01-29 19:11:48 +0000
commit1e466a20533d936f44430b1bc18508cd00e5ccd2 (patch)
tree20c025af6ed539a600ec8db9e1339c9c4e7c9112 /dhall/src/semantics/tck
parentf88880004c7dcf5e67c4d5e2330e6e879523f27b (diff)
Use TyExpr in Typed
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs9
1 files changed, 8 insertions, 1 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a83f175..5880d92 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -677,7 +677,7 @@ pub(crate) fn type_with(
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
ExprKind::Embed(p) => {
- return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+ return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
@@ -692,3 +692,10 @@ pub(crate) fn type_with(
pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
type_with(&TyEnv::new(), e)
}
+
+pub(crate) fn typecheck_with(
+ expr: &Expr<Normalized>,
+ ty: Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+ typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+}