summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/expr.rs34
-rw-r--r--dhall/src/normalize.rs10
-rw-r--r--dhall/src/typecheck.rs89
3 files changed, 67 insertions, 66 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index ae52e4d..cc7f064 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,5 +1,4 @@
use crate::imports::ImportRoot;
-use crate::typecheck::TypeError;
use dhall_core::*;
#[derive(Debug, Clone, Eq)]
@@ -9,10 +8,11 @@ pub struct Parsed(pub(crate) SubExpr<X, Import>, pub(crate) ImportRoot);
pub struct Resolved(pub(crate) SubExpr<X, X>);
#[derive(Debug, Clone)]
-pub struct Typed(pub(crate) SubExpr<X, X>, Type);
+pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
-#[derive(Debug, Clone)]
-pub struct Type(pub(crate) Box<Normalized>);
+// #[derive(Debug, Clone)]
+// pub struct Type(pub(crate) Box<Normalized>);
+pub type Type = SubExpr<X, X>;
#[derive(Debug, Clone)]
pub struct Normalized(pub(crate) SubExpr<X, X>);
@@ -28,24 +28,8 @@ impl std::fmt::Display for Parsed {
}
}
-impl Resolved {
- pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
- let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
- self.0.clone(),
- )?)));
- Ok(Typed(self.0, typ))
- }
-}
-impl Typed {
- pub fn normalize(self) -> Normalized {
- Normalized(crate::normalize::normalize(self.0))
- }
- pub fn get_type(&self) -> &Type {
- &self.1
- }
-}
-impl Type {
- pub fn as_expr(&self) -> &Normalized {
- &*self.0
- }
-}
+// impl Type {
+// pub fn as_expr(&self) -> &Normalized {
+// &*self.0
+// }
+// }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 24a8601..8ed2136 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1,8 +1,18 @@
#![allow(non_snake_case)]
+use crate::expr::*;
use dhall_core::*;
use dhall_generator::dhall_expr;
use std::fmt;
+impl Typed {
+ pub fn normalize(self) -> Normalized {
+ Normalized(normalize(self.0))
+ }
+ pub fn get_type(&self) -> &Type {
+ &self.1
+ }
+}
+
fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
where
S: fmt::Debug + Clone,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e63b032..f5dbbbf 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -2,6 +2,7 @@
use std::collections::HashSet;
use std::fmt;
+use crate::expr::*;
use crate::normalize::normalize;
use dhall_core;
use dhall_core::context::Context;
@@ -10,6 +11,17 @@ use dhall_generator as dhall;
use self::TypeMessage::*;
+impl Resolved {
+ pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
+ // let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
+ // self.0.clone(),
+ // )?)));
+ // Ok(Typed(self.0, typ))
+ let typ = crate::typecheck::type_of(self.0.clone())?;
+ Ok(Typed(self.0, typ))
+ }
+}
+
fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
use dhall_core::Const::*;
use dhall_core::ExprF::*;
@@ -199,13 +211,10 @@ where
///
/// `type_with` normalizes the type since while type-checking. It expects the
/// context to contain only normalized expressions.
-pub fn type_with<S>(
- ctx: &Context<Label, SubExpr<S, X>>,
- e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
- S: ::std::fmt::Debug + Clone,
-{
+pub fn type_with(
+ ctx: &Context<Label, SubExpr<X, X>>,
+ e: SubExpr<X, X>,
+) -> Result<Typed, TypeError<X>> {
use dhall_core::BinOp::*;
use dhall_core::Builtin::*;
use dhall_core::Const::*;
@@ -228,19 +237,19 @@ where
let ctx2 = ctx
.insert(x.clone(), t2.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = type_with(&ctx2, b.clone())?;
- let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?;
+ let tB = type_with(&ctx2, b.clone())?.1;
+ let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1;
Ok(Pi(x.clone(), t2, tB))
}
Pi(x, tA, tB) => {
- let ttA = type_with(ctx, tA.clone())?;
+ let ttA = type_with(ctx, tA.clone())?.1;
let tA = normalize(SubExpr::clone(tA));
let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
let ctx2 = ctx
.insert(x.clone(), tA.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = type_with(&ctx2, tB.clone())?;
+ let tB = type_with(&ctx2, tB.clone())?.1;
let kB = match tB.as_ref() {
Const(k) => *k,
_ => {
@@ -264,15 +273,15 @@ where
SubExpr::clone(r)
};
- let tR = type_with(ctx, r)?;
- let ttR = type_with(ctx, tR.clone())?;
+ let tR = type_with(ctx, r)?.1;
+ let ttR = type_with(ctx, tR.clone())?.1;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
let ctx2 = ctx.insert(f.clone(), tR.clone());
- let tB = type_with(&ctx2, b.clone())?;
- let ttB = type_with(ctx, tB.clone())?;
+ let tB = type_with(&ctx2, b.clone())?.1;
+ let ttB = type_with(ctx, tB.clone())?.1;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
@@ -285,7 +294,7 @@ where
}
_ => match e
.as_ref()
- .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
+ .traverse_ref_simple(|e| type_with(ctx, e.clone()))?
{
Lam(_, _, _) => unreachable!(),
Pi(_, _, _) => unreachable!(),
@@ -295,10 +304,10 @@ where
Some(e) => Ok(e.unroll()),
None => Err(mkerr(UnboundVariable)),
},
- App((f, mut tf), args) => {
+ App(Typed(f, mut tf), args) => {
let mut iter = args.into_iter();
let mut seen_args: Vec<SubExpr<_, _>> = vec![];
- while let Some((a, ta)) = iter.next() {
+ while let Some(Typed(a, ta)) = iter.next() {
seen_args.push(a.clone());
let (x, tx, tb) = match tf.as_ref() {
Pi(x, tx, tb) => (x, tx, tb),
@@ -321,18 +330,18 @@ where
}
Ok(tf.unroll())
}
- Annot((x, tx), (t, _)) => {
+ Annot(Typed(x, tx), Typed(t, _)) => {
let t = normalize(t.clone());
ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
AnnotMismatch(x.clone(), t.clone(), tx.clone())
})?;
Ok(t.unroll())
}
- BoolIf((x, tx), (y, ty), (z, tz)) => {
+ BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => {
ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
InvalidPredicate(x.clone(), tx.clone())
})?;
- let tty = type_with(ctx, ty.clone())?;
+ let tty = type_with(ctx, ty.clone())?.1;
ensure_is_type(
tty.clone(),
IfBranchMustBeTerm(
@@ -343,7 +352,7 @@ where
),
)?;
- let ttz = type_with(ctx, tz.clone())?;
+ let ttz = type_with(ctx, tz.clone())?.1;
ensure_is_type(
ttz.clone(),
IfBranchMustBeTerm(
@@ -364,35 +373,35 @@ where
})?;
Ok(ty.unroll())
}
- EmptyListLit((t, tt)) => {
- ensure_is_type(tt, InvalidListType(t.clone()))?;
- let t = normalize(SubExpr::clone(t));
+ EmptyListLit(Typed(t, tt)) => {
+ ensure_is_type(tt.clone(), InvalidListType(t.clone()))?;
+ let t = Typed(t, tt).normalize().0;
Ok(dhall::expr!(List t))
}
NEListLit(xs) => {
let mut iter = xs.into_iter().enumerate();
- let (_, (_, t)) = iter.next().unwrap();
- let s = type_with(ctx, t.clone())?;
+ let (_, Typed(_, t)) = iter.next().unwrap();
+ let s = type_with(ctx, t.clone())?.1;
ensure_is_type(s, InvalidListType(t.clone()))?;
- for (i, (y, ty)) in iter {
+ for (i, Typed(y, ty)) in iter {
ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
InvalidListElement(i, t.clone(), y.clone(), ty.clone())
})?;
}
Ok(dhall::expr!(List t))
}
- EmptyOptionalLit((t, tt)) => {
+ EmptyOptionalLit(Typed(t, tt)) => {
ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
let t = normalize(t.clone());
Ok(dhall::expr!(Optional t))
}
- NEOptionalLit((_, t)) => {
- let s = type_with(ctx, t.clone())?;
+ NEOptionalLit(Typed(_, t)) => {
+ let s = type_with(ctx, t.clone())?.1;
ensure_is_type(s, InvalidOptionalType(t.clone()))?;
Ok(dhall::expr!(Optional t))
}
RecordType(kts) => {
- for (k, (t, tt)) in kts {
+ for (k, Typed(t, tt)) in kts {
ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
}
Ok(Const(Type))
@@ -400,15 +409,15 @@ where
RecordLit(kvs) => {
let kts = kvs
.into_iter()
- .map(|(k, (v, t))| {
- let s = type_with(ctx, t.clone())?;
+ .map(|(k, Typed(v, t))| {
+ let s = type_with(ctx, t.clone())?.1;
ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
Ok((k.clone(), t))
})
.collect::<Result<_, _>>()?;
Ok(RecordType(kts))
}
- Field((r, tr), x) => match tr.as_ref() {
+ Field(Typed(r, tr), x) => match tr.as_ref() {
RecordType(kts) => match kts.get(&x) {
Some(e) => Ok(e.unroll()),
None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
@@ -422,7 +431,7 @@ where
DoubleLit(_) => Ok(Builtin(Double)),
// TODO: check type of interpolations
TextLit(_) => Ok(Builtin(Text)),
- BinOp(o, (l, tl), (r, tr)) => {
+ BinOp(o, Typed(l, tl), Typed(r, tr)) => {
let t = Builtin(match o {
BoolAnd => Bool,
BoolOr => Bool,
@@ -448,17 +457,15 @@ where
_ => panic!("Unimplemented typecheck case: {:?}", e),
},
}?;
- Ok(rc(ret))
+ Ok(Typed(e, rc(ret)))
}
/// `typeOf` is the same as `type_with` with an empty context, meaning that the
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
-pub fn type_of<S: ::std::fmt::Debug + Clone>(
- e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>> {
+pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
let ctx = Context::new();
- type_with(&ctx, e) //.map(|e| e.into_owned())
+ type_with(&ctx, e).map(|e| e.1)
}
/// The specific type error
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:05:01 +0000