diff options
author | Nadrieril | 2019-05-04 16:50:38 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-04 16:50:38 +0200 |
commit | 0e5c93c398645d39fceb98d054f1a7e67025b4fd (patch) | |
tree | c5a093c8d9a05cb50e83966fe4923c134f5c3515 | |
parent | 408bba76bd95a2aabd49046443950a37771f6008 (diff) |
Keep Spans through normalization and typechecking
-rw-r--r-- | dhall/src/expr.rs | 7 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 14 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 54 |
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`) |