diff options
author | Nadrieril | 2019-05-06 22:09:55 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-06 22:09:55 +0200 |
commit | 423fdeebe9247b16744fae4b50df415bbd08be04 (patch) | |
tree | f2f16407d7e365e6fecee400a1959ca08b2a5156 /dhall/src/normalize.rs | |
parent | 2075cba6d883278a534afd2d8fe8f0a5e9b2f0d0 (diff) |
Reorganize dhall into a phase structure
Diffstat (limited to '')
-rw-r--r-- | dhall/src/phase/normalize.rs (renamed from dhall/src/normalize.rs) | 37 |
1 files changed, 8 insertions, 29 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/phase/normalize.rs index 1d306bc..2340bbd 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -6,34 +6,13 @@ use dhall_proc_macros as dhall; use dhall_syntax::context::Context; use dhall_syntax::{ rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - Natural, Span, SubExpr, V, X, + Natural, V, X, }; -use crate::expr::{Normalized, Type, Typed}; - -type InputSubExpr = SubExpr<Span, Normalized>; -type OutputSubExpr = SubExpr<X, X>; - -impl Typed { - /// Reduce an expression to its normal form, performing beta reduction - /// - /// `normalize` does not type-check the expression. You may want to type-check - /// expressions before normalizing them since normalization can convert an - /// ill-typed expression into a well-typed expression. - /// - /// However, `normalize` will not fail if the expression is ill-typed and will - /// leave ill-typed sub-expressions unevaluated. - /// - pub fn normalize(self) -> Normalized { - match &self { - Typed::Sort => {} - Typed::Value(thunk, _) => { - thunk.normalize_nf(); - } - } - Normalized(self) - } -} +use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Type, Typed}; + +type InputSubExpr = ResolvedSubExpr; +type OutputSubExpr = NormalizedSubExpr; /// Stores a pair of variables: a normal one and if relevant one /// that corresponds to the alpha-normalized version of the first one. @@ -186,9 +165,9 @@ impl NormalizationContext { } } pub(crate) fn from_typecheck_ctx( - tc_ctx: &crate::typecheck::TypecheckContext, + tc_ctx: &crate::phase::typecheck::TypecheckContext, ) -> Self { - use crate::typecheck::EnvItem::*; + use crate::phase::typecheck::EnvItem::*; let mut ctx = Context::new(); for (k, vs) in tc_ctx.0.iter_keys() { for v in vs.iter() { @@ -718,7 +697,7 @@ mod thunk { apply_any, normalize_whnf, AlphaVar, InputSubExpr, NormalizationContext, OutputSubExpr, Value, }; - use crate::expr::Typed; + use crate::phase::Typed; use std::cell::{Ref, RefCell}; use std::rc::Rc; |