summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/mod.rs16
-rw-r--r--dhall/src/phase/normalize.rs34
-rw-r--r--dhall/src/phase/typecheck.rs40
3 files changed, 49 insertions, 41 deletions
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 0b05227..27a6901 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,7 +4,7 @@ use std::path::Path;
use dhall_syntax::{Const, Import, Span, SubExpr, X};
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -31,7 +31,7 @@ pub struct Resolved(ResolvedSubExpr);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(TypeThunk);
+pub struct Typed(TypedThunk);
/// A normalized expression.
///
@@ -100,18 +100,18 @@ impl Typed {
}
pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Typed(TypeThunk::from_thunk_and_type(th, t))
+ Typed(TypedThunk::from_thunk_and_type(th, t))
}
pub fn from_thunk_untyped(th: Thunk) -> Self {
- Typed(TypeThunk::from_thunk_untyped(th))
+ Typed(TypedThunk::from_thunk_untyped(th))
}
pub fn from_const(c: Const) -> Self {
- Typed(TypeThunk::from_const(c))
+ Typed(TypedThunk::from_const(c))
}
pub fn from_value_untyped(v: Value) -> Self {
- Typed(TypeThunk::from_value_untyped(v))
+ Typed(TypedThunk::from_value_untyped(v))
}
- pub fn from_typethunk(th: TypeThunk) -> Self {
+ pub fn from_typethunk(th: TypedThunk) -> Self {
Typed(th)
}
@@ -135,7 +135,7 @@ impl Typed {
pub fn into_type(self) -> Type {
self
}
- pub fn into_typethunk(self) -> TypeThunk {
+ pub fn into_typethunk(self) -> TypedThunk {
self.0
}
pub fn to_normalized(&self) -> Normalized {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 405677a..644f98c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
};
use crate::core::context::NormalizationContext;
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::Subst;
use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
@@ -22,7 +22,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
// Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
let ret = match (b, args.as_slice()) {
(OptionalNone, [t, r..]) => {
- Ok((r, EmptyOptionalLit(TypeThunk::from_thunk(t.clone()))))
+ Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone()))))
}
(NaturalIsZero, [n, r..]) => match &*n.as_value() {
NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
@@ -144,10 +144,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
let mut kts = HashMap::new();
kts.insert(
"index".into(),
- TypeThunk::from_value(Value::from_builtin(Natural)),
+ TypedThunk::from_value(Value::from_builtin(Natural)),
);
kts.insert("value".into(), t.clone());
- Ok((r, EmptyListLit(TypeThunk::from_value(RecordType(kts)))))
+ Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts)))))
}
NEListLit(xs) => {
let xs = xs
@@ -179,10 +179,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
r,
f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
.app_val(ListConsClosure(
- TypeThunk::from_thunk(t.clone()),
+ TypedThunk::from_thunk(t.clone()),
None,
))
- .app_val(EmptyListLit(TypeThunk::from_thunk(t.clone()))),
+ .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
)),
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
@@ -213,10 +213,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Ok((
r,
f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
- .app_val(OptionalSomeClosure(TypeThunk::from_thunk(
+ .app_val(OptionalSomeClosure(TypedThunk::from_thunk(
t.clone(),
)))
- .app_val(EmptyOptionalLit(TypeThunk::from_thunk(
+ .app_val(EmptyOptionalLit(TypedThunk::from_thunk(
t.clone(),
))),
)),
@@ -618,7 +618,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- TypeThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
+ TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
RecursiveRecordTypeMerge,
v1.to_thunk(),
v2.to_thunk(),
@@ -628,8 +628,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(Equivalence, _, _) => Ret::Value(Value::Equivalence(
- TypeThunk::from_thunk(x.clone()),
- TypeThunk::from_thunk(y.clone()),
+ TypedThunk::from_thunk(x.clone()),
+ TypedThunk::from_thunk(y.clone()),
)),
_ => return None,
@@ -649,12 +649,12 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
ExprF::Annot(x, _) => Ret::Thunk(x),
ExprF::Assert(_) => Ret::Expr(expr),
ExprF::Lam(x, t, e) => {
- Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
+ Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e))
}
ExprF::Pi(x, t, e) => Ret::Value(Pi(
x.into(),
- TypeThunk::from_thunk(t),
- TypeThunk::from_thunk(e),
+ TypedThunk::from_thunk(t),
+ TypedThunk::from_thunk(e),
)),
ExprF::Let(x, _, v, b) => {
let v = Typed::from_thunk_untyped(v);
@@ -673,7 +673,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
let t_borrow = t.as_value();
match &*t_borrow {
AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
- Ret::Value(EmptyListLit(TypeThunk::from_thunk(
+ Ret::Value(EmptyListLit(TypedThunk::from_thunk(
args[0].clone(),
)))
}
@@ -691,12 +691,12 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
}
ExprF::RecordType(kts) => Ret::Value(RecordType(
kts.into_iter()
- .map(|(k, t)| (k, TypeThunk::from_thunk(t)))
+ .map(|(k, t)| (k, TypedThunk::from_thunk(t)))
.collect(),
)),
ExprF::UnionType(kts) => Ret::Value(UnionType(
kts.into_iter()
- .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
+ .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t))))
.collect(),
)),
ExprF::TextLit(elts) => {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 299997a..a19e1ca 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
};
use crate::core::context::{NormalizationContext, TypecheckContext};
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::{Shift, Subst};
use crate::error::{TypeError, TypeMessage};
@@ -44,8 +44,12 @@ fn tck_pi_type(
let k = function_check(ka, kb);
Ok(Typed::from_thunk_and_type(
- Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te))
- .into_thunk(),
+ Value::Pi(
+ x.into(),
+ TypedThunk::from_type(tx),
+ TypedThunk::from_type(te),
+ )
+ .into_thunk(),
Type::from_const(k),
))
}
@@ -77,7 +81,7 @@ fn tck_record_type(
return Err(TypeError::new(ctx, RecordTypeDuplicateField))
}
Entry::Vacant(_) => {
- entry.or_insert_with(|| TypeThunk::from_type(t.clone()))
+ entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
}
};
}
@@ -119,7 +123,7 @@ fn tck_union_type(
return Err(TypeError::new(ctx, UnionTypeDuplicateField))
}
Entry::Vacant(_) => entry.or_insert_with(|| {
- t.as_ref().map(|t| TypeThunk::from_type(t.clone()))
+ t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
}),
};
}
@@ -334,7 +338,7 @@ fn type_with(
let b = type_with(&ctx2, b.clone())?;
let v = Value::Lam(
x.clone().into(),
- TypeThunk::from_type(tx.clone()),
+ TypedThunk::from_type(tx.clone()),
b.to_thunk(),
);
let tb = b.get_type()?.into_owned();
@@ -658,8 +662,8 @@ fn type_last_layer(
// records of records when merging.
fn combine_record_types(
ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypeThunk>,
- kts_r: HashMap<Label, TypeThunk>,
+ kts_l: HashMap<Label, TypedThunk>,
+ kts_r: HashMap<Label, TypedThunk>,
) -> Result<Typed, TypeError> {
use crate::phase::normalize::outer_join;
@@ -667,8 +671,8 @@ fn type_last_layer(
// are records themselves, then we hit the recursive case.
// Otherwise we have a field collision.
let combine = |k: &Label,
- inner_l: &TypeThunk,
- inner_r: &TypeThunk|
+ inner_l: &TypedThunk,
+ inner_r: &TypedThunk|
-> Result<Typed, TypeError> {
match (inner_l.to_value(), inner_r.to_value()) {
(
@@ -686,7 +690,9 @@ fn type_last_layer(
let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
|l| Ok(l.to_type()),
|r| Ok(r.to_type()),
- |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+ |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+ combine(k, l, r)
+ },
&kts_l,
&kts_r,
);
@@ -729,8 +735,8 @@ fn type_last_layer(
// records of records when merging.
fn combine_record_types(
ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypeThunk>,
- kts_r: HashMap<Label, TypeThunk>,
+ kts_l: HashMap<Label, TypedThunk>,
+ kts_r: HashMap<Label, TypedThunk>,
) -> Result<Typed, TypeError> {
use crate::phase::normalize::intersection_with_key;
@@ -738,8 +744,8 @@ fn type_last_layer(
// are records themselves, then we hit the recursive case.
// Otherwise we have a field collision.
let combine = |k: &Label,
- kts_l_inner: &TypeThunk,
- kts_r_inner: &TypeThunk|
+ kts_l_inner: &TypedThunk,
+ kts_r_inner: &TypedThunk|
-> Result<Typed, TypeError> {
match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
(
@@ -755,7 +761,9 @@ fn type_last_layer(
};
let kts = intersection_with_key(
- |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+ |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+ combine(k, l, r)
+ },
&kts_l,
&kts_r,
);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:29:12 +0000