From 23adedb23907b24366ae87bdd2b4a424f59d2042 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 20 Apr 2019 12:06:22 +0200 Subject: More cleanup --- dhall/src/normalize.rs | 176 ++++++++++++++----------------------------------- 1 file changed, 51 insertions(+), 125 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 75bc73c..0aaa582 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -25,14 +25,17 @@ impl<'a> Typed<'a> { } } -fn apply_builtin(b: Builtin, args: &[WHNF]) -> WhatNext { +fn apply_builtin( + ctx: &NormalizationContext, + b: Builtin, + args: &[WHNF], +) -> Option { let args: Vec<_> = args .iter() .map(|val| val.clone().normalize_to_expr().unroll()) .collect(); use dhall_core::Builtin::*; use dhall_core::ExprF::*; - use WhatNext::*; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => rc(EmptyOptionalLit(t.roll())), (NaturalIsZero, [NaturalLit(n)]) => rc(BoolLit(*n == 0)), @@ -177,24 +180,52 @@ fn apply_builtin(b: Builtin, args: &[WHNF]) -> WhatNext { // _ => return rc(App(f, args)), // } // } - _ => return DoneAsIs, + _ => return None, }; - Continue(ret.unroll()) + Some(normalize_whnf(ctx, ret.embed_absurd())) +} + +#[derive(Debug, Clone)] +enum EnvItem { + Expr(WHNF), + Skip(usize), } -// #[derive(Debug, Clone)] -// struct ContextualizedSubExpr { -// ctx: NormalizationContext, -// expr: SubExpr>, -// } -// impl ContextualizedSubExpr { -// fn normalize_whnf(self) -> WHNF { -// normalize_whnf(&self.ctx, self.expr) -// } -// fn normalize_expr(self) -> OutputSubExpr { -// normalize_whnf(&self.ctx, self.expr).into_expr(&self.ctx) -// } -// } +#[derive(Debug, Clone)] +struct NormalizationContext(Context); + +impl NormalizationContext { + fn new() -> NormalizationContext { + NormalizationContext(Context::new()) + } + fn insert(&self, x: &Label, e: WHNF) -> NormalizationContext { + NormalizationContext(self.0.insert(x.clone(), EnvItem::Expr(e))) + } + fn skip(&self, x: &Label) -> NormalizationContext { + NormalizationContext( + self.0 + .map(|l, e| { + use EnvItem::*; + match e { + Expr(e) => Expr(e.clone().shift0(1, x)), + Skip(n) if l == x => Skip(*n + 1), + Skip(n) => Skip(*n), + } + }) + .insert(x.clone(), EnvItem::Skip(0)), + ) + } + fn lookup(&self, var: &V