summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs7
-rw-r--r--dhall/src/normalize.rs14
-rw-r--r--dhall/src/typecheck.rs54
3 files changed, 39 insertions, 36 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index db426ce..5bde68f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -204,16 +204,15 @@ impl Normalized {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
Normalized(TypedInternal::from_thunk_and_type(th, t))
}
- // Deprecated
- pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
- self.0.to_expr()
- }
pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.0.to_expr()
}
pub(crate) fn to_value(&self) -> Value {
self.0.to_value()
}
+ pub(crate) fn to_thunk(&self) -> Thunk {
+ self.0.to_thunk()
+ }
#[allow(dead_code)]
pub(crate) fn unnote(self) -> Normalized {
Normalized(self.0)
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 4d87225..8ae746d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,12 +6,12 @@ use dhall_proc_macros as dhall;
use dhall_syntax::context::Context;
use dhall_syntax::{
rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
- InterpolatedTextContents, Label, Natural, SubExpr, V, X,
+ InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
};
use crate::expr::{Normalized, Type, Typed, TypedInternal};
-type InputSubExpr = SubExpr<X, Normalized>;
+type InputSubExpr = SubExpr<Span, Normalized>;
type OutputSubExpr = SubExpr<X, X>;
impl Typed {
@@ -110,10 +110,7 @@ impl NormalizationContext {
for v in vs.iter() {
let new_item = match v {
Type(var, _) => EnvItem::Skip(var.clone()),
- Value(e) => EnvItem::Thunk(Thunk::new(
- NormalizationContext::new(),
- e.as_expr().embed_absurd(),
- )),
+ Value(e) => EnvItem::Thunk(e.to_thunk()),
};
ctx = ctx.insert(k.clone(), new_item);
}
@@ -736,7 +733,10 @@ mod thunk {
}
pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk {
- Thunk::new(NormalizationContext::new(), e.embed_absurd())
+ Thunk::new(
+ NormalizationContext::new(),
+ e.embed_absurd().note_absurd(),
+ )
}
// Normalizes contents to normal form; faster than `normalize_nf` if
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 732f7bc..8b7f011 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -16,19 +16,19 @@ use self::TypeMessage::*;
impl Resolved {
pub fn typecheck(self) -> Result<Typed, TypeError> {
- type_of(self.0.unnote())
+ type_of(self.0)
}
pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
- let expr: SubExpr<_, _> = self.0.unnote();
- let ty: SubExpr<_, _> = ty.to_expr().embed_absurd();
- type_of(rc(ExprF::Annot(expr, ty)))
+ let expr: SubExpr<_, _> = self.0;
+ let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
+ type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
/// Pretends this expression has been typechecked. Use with care.
#[allow(dead_code)]
pub fn skip_typecheck(self) -> Typed {
Typed::from_thunk_untyped(Thunk::new(
NormalizationContext::new(),
- self.0.unnote(),
+ self.0,
))
}
}
@@ -97,7 +97,7 @@ impl TypeThunk {
TypeThunk::Type(t) => Ok(t.clone()),
TypeThunk::Thunk(th) => {
// TODO: rule out statically
- mktype(ctx, th.normalize_to_expr().embed_absurd())
+ mktype(ctx, th.normalize_to_expr().embed_absurd().note_absurd())
}
}
}
@@ -621,13 +621,16 @@ impl TypeIntermediate {
/// and turn it into a type, typechecking it along the way.
fn mktype(
ctx: &TypecheckContext,
- e: SubExpr<X, Normalized>,
+ e: SubExpr<Span, Normalized>,
) -> Result<Type, TypeError> {
Ok(type_with(ctx, e)?.to_type())
}
fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> {
- mktype(&TypecheckContext::new(), rc(ExprF::Builtin(b)))
+ mktype(
+ &TypecheckContext::new(),
+ SubExpr::from_expr_no_note(ExprF::Builtin(b)),
+ )
}
/// Intermediary return type
@@ -636,18 +639,17 @@ enum Ret {
RetTyped(Typed),
/// Use the contained Type as the type of the input expression
RetType(Type),
- /// Returns an expression that must be typechecked and
- /// turned into a Type first.
- RetExpr(Expr<X, Normalized>),
}
/// Type-check an expression and return the expression alongside its type if type-checking
/// succeeded, or an error if type-checking failed
fn type_with(
ctx: &TypecheckContext,
- e: SubExpr<X, Normalized>,
+ e: SubExpr<Span, Normalized>,
) -> Result<Typed, TypeError> {
- use dhall_syntax::ExprF::*;
+ use dhall_syntax::ExprF::{
+ Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
+ };
use Ret::*;
let ret = match e.as_ref() {
@@ -673,7 +675,7 @@ fn type_with(
}
Let(x, t, v, e) => {
let v = if let Some(t) = t {
- rc(Annot(v.clone(), t.clone()))
+ t.rewrap(Annot(v.clone(), t.clone()))
} else {
v.clone()
};
@@ -684,14 +686,18 @@ fn type_with(
Ok(RetType(e.get_type()?.into_owned()))
}
OldOptionalLit(None, t) => {
- let t = t.clone();
- let e = dhall::subexpr!(None t);
+ let none = SubExpr::from_expr_no_note(ExprF::Builtin(
+ Builtin::OptionalNone,
+ ));
+ let e = e.rewrap(App(none, t.clone()));
return type_with(ctx, e);
}
OldOptionalLit(Some(x), t) => {
- let t = t.clone();
- let x = x.clone();
- let e = dhall::subexpr!(Some x : Optional t);
+ let optional =
+ SubExpr::from_expr_no_note(ExprF::Builtin(Builtin::Optional));
+ let x = x.rewrap(SomeLit(x.clone()));
+ let t = t.rewrap(App(optional, t.clone()));
+ let e = e.rewrap(Annot(x, t));
return type_with(ctx, e);
}
Embed(p) => Ok(RetTyped(p.clone().into())),
@@ -703,10 +709,6 @@ fn type_with(
),
}?;
Ok(match ret {
- RetExpr(ret) => Typed::from_thunk_and_type(
- Thunk::new(ctx.to_normalization_ctx(), e),
- mktype(ctx, rc(ret))?,
- ),
RetType(typ) => Typed::from_thunk_and_type(
Thunk::new(ctx.to_normalization_ctx(), e),
typ,
@@ -935,7 +937,9 @@ fn type_last_layer(
}
}
Const(c) => Ok(RetTyped(const_to_typed(c))),
- Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
+ Builtin(b) => {
+ Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
+ }
BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -994,7 +998,7 @@ fn type_last_layer(
/// `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.
-fn type_of(e: SubExpr<X, Normalized>) -> Result<Typed, TypeError> {
+fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
let ctx = TypecheckContext::new();
let e = type_with(&ctx, e)?;
// Ensure `e` has a type (i.e. `e` is not `Sort`)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 06:03:47 +0000