summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2019-04-30 14:45:25 +0200
committerNadrieril2019-04-30 14:45:25 +0200
commite2626a0bfd4b145e7d54c2150457f57e798ba2f7 (patch)
treede56af3215419814df3079c869c2bebd0c5383f5 /dhall/src/typecheck.rs
parent65a242abfa4d881dc17f216b3eeeb8aedc663388 (diff)
Store a Thunk in Typed
Diffstat (limited to 'dhall/src/typecheck.rs')
-rw-r--r--dhall/src/typecheck.rs17
1 files changed, 11 insertions, 6 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d924f41..85de42a 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,7 @@ use std::fmt;
use std::marker::PhantomData;
use crate::expr::*;
-use crate::normalize::{TypeThunk, Value};
+use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
use crate::traits::DynamicType;
use dhall_core;
use dhall_core::context::Context;
@@ -30,7 +30,11 @@ impl<'a> Resolved<'a> {
/// Pretends this expression has been typechecked. Use with care.
#[allow(dead_code)]
pub fn skip_typecheck(self) -> Typed<'a> {
- Typed(self.0.unnote(), None, TypecheckContext::new(), PhantomData)
+ Typed(
+ Thunk::new(NormalizationContext::new(), self.0.unnote()),
+ None,
+ PhantomData,
+ )
}
}
impl<'a> Typed<'a> {
@@ -325,6 +329,9 @@ impl TypecheckContext {
None => None,
}
}
+ fn to_normalization_ctx(&self) -> NormalizationContext {
+ NormalizationContext::from_typecheck_ctx(self)
+ }
}
impl PartialEq for TypecheckContext {
@@ -813,15 +820,13 @@ fn type_with(
}?;
match ret {
RetExpr(ret) => Ok(TypedOrType::Typed(Typed(
- e,
+ Thunk::new(ctx.to_normalization_ctx(), e),
Some(mktype(ctx, rc(ret))?),
- ctx.clone(),
PhantomData,
))),
RetType(typ) => Ok(TypedOrType::Typed(Typed(
- e,
+ Thunk::new(ctx.to_normalization_ctx(), e),
Some(typ),
- ctx.clone(),
PhantomData,
))),
RetTypedOrType(tt) => Ok(tt),