diff options
author | Nadrieril | 2019-04-19 19:17:59 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-19 19:17:59 +0200 |
commit | 12552383aa469b587b72b82337e5e17c6174ff9c (patch) | |
tree | 96341f5ef118b916a35b3b29555eab9a8750da13 /dhall/src | |
parent | 897a1da43bda583b570b0a8818945167fc0e2240 (diff) |
Store Values in the context
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/normalize.rs | 46 |
1 files changed, 36 insertions, 10 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index dd47e88..3242fb0 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -247,6 +247,13 @@ impl Value { Value::Expr(e) => e, } } + + fn shift0(self, delta: isize, label: &Label) -> Self { + match self { + Value::Closure(c) => Value::Closure(c.shift0(delta, label)), + Value::Expr(e) => Value::Expr(shift0(delta, label, &e)), + } + } } #[derive(Debug, Clone)] @@ -260,7 +267,7 @@ impl Closure { fn app(self, val: Value) -> Value { match self { Closure::Lam(ctx, x, _, e) => { - let ctx2 = ctx.insert(&x, val.normalize_to_expr(&ctx)); + let ctx2 = ctx.insert(&x, val); normalize_value(&ctx2, e) } Closure::AppliedBuiltin(ctx, b, mut args) => { @@ -305,11 +312,27 @@ impl Closure { } } } + + fn shift0(self, delta: isize, label: &Label) -> Self { + match self { + Closure::Lam(ctx, x, t, e) => Closure::Lam( + ctx, + x, + shift0(delta, label, &t), + shift(delta, &V(label.clone(), 1), &e), + ), + Closure::AppliedBuiltin(ctx, b, args) => Closure::AppliedBuiltin( + ctx, + b, + args.into_iter().map(|e| e.shift0(delta, label)).collect(), + ), + } + } } #[derive(Debug, Clone)] enum EnvItem { - Expr(OutputSubExpr), + Expr(Value), Skip(usize), } @@ -320,7 +343,7 @@ impl NormalizationContext { fn new() -> NormalizationContext { NormalizationContext(Context::new()) } - fn insert(&self, x: &Label, e: OutputSubExpr) -> NormalizationContext { + fn insert(&self, x: &Label, e: Value) -> NormalizationContext { NormalizationContext(self.0.insert(x.clone(), EnvItem::Expr(e))) } fn skip(&self, x: &Label) -> NormalizationContext { @@ -329,7 +352,7 @@ impl NormalizationContext { .map(|l, e| { use EnvItem::*; match e { - Expr(e) => Expr(shift0(1, x, e)), + Expr(e) => Expr(e.clone().shift0(1, x)), Skip(n) if l == x => Skip(*n + 1), Skip(n) => Skip(*n), } @@ -337,12 +360,14 @@ impl NormalizationContext { .insert(x.clone(), EnvItem::Skip(0)), ) } - fn lookup(&self, var: &V<Label>) -> OutputSubExpr { + fn lookup(&self, var: &V<Label>) -> Value { let V(x, n) = var; match self.0.lookup(x, *n) { Some(EnvItem::Expr(e)) => e.clone(), - Some(EnvItem::Skip(m)) => rc(ExprF::Var(V(x.clone(), *m))), - None => rc(ExprF::Var(V(x.clone(), *n))), + Some(EnvItem::Skip(m)) => { + Value::Expr(rc(ExprF::Var(V(x.clone(), *m)))) + } + None => Value::Expr(rc(ExprF::Var(V(x.clone(), *n)))), } } } @@ -395,8 +420,8 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value { let e = match expr.as_ref() { Let(x, _, r, b) => { - let r = normalize_value(ctx, r.clone()).normalize_to_expr(ctx); - return normalize_value(&ctx.insert(x, r.clone()), b.clone()); + let r = normalize_value(ctx, r.clone()); + return normalize_value(&ctx.insert(x, r), b.clone()); } Lam(x, t, e) => { return Value::Closure(Closure::Lam( @@ -427,6 +452,7 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value { ); let expr = match expr { + Var(v) => return ctx.lookup(&v), App(Value::Closure(c), a) => { return c.app(a); } @@ -445,9 +471,9 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value { use WhatNext::*; let what_next = match &expr { Embed(e) => DoneRefSub(&e.0), - Var(v) => DoneSub(ctx.lookup(v)), Annot(x, _) => DoneRef(x), Note(_, e) => DoneRef(e), + Var(_) => unreachable!(), Let(_, _, _, _) => unreachable!(), Lam(_, _, _) => unreachable!(), App(Builtin(_), _) => unreachable!(), |