summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-19 19:17:59 +0200
committerNadrieril2019-04-19 19:17:59 +0200
commit12552383aa469b587b72b82337e5e17c6174ff9c (patch)
tree96341f5ef118b916a35b3b29555eab9a8750da13
parent897a1da43bda583b570b0a8818945167fc0e2240 (diff)
Store Values in the context
-rw-r--r--dhall/src/normalize.rs46
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!(),