fix: start trying to get rid of recursion for discharge value
This commit is contained in:
parent
cb8bdac39d
commit
790e8ba680
|
@ -32,6 +32,11 @@ impl TryFrom<Option<MachineStep>> for Term<NamedDeBruijn> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum DischargeStep {
|
||||||
|
DischargeValue(Value),
|
||||||
|
DischargeValueEnv(usize, Rc<Vec<Value>>, Rc<Term<NamedDeBruijn>>),
|
||||||
|
}
|
||||||
|
|
||||||
pub struct Machine {
|
pub struct Machine {
|
||||||
costs: CostModel,
|
costs: CostModel,
|
||||||
pub ex_budget: ExBudget,
|
pub ex_budget: ExBudget,
|
||||||
|
@ -205,15 +210,27 @@ impl Machine {
|
||||||
}
|
}
|
||||||
|
|
||||||
fn discharge_value(&mut self, value: Value) -> Rc<Term<NamedDeBruijn>> {
|
fn discharge_value(&mut self, value: Value) -> Rc<Term<NamedDeBruijn>> {
|
||||||
match value {
|
let mut stack = vec![DischargeStep::DischargeValue(value)];
|
||||||
|
|
||||||
|
while let Some(stack_frame) = stack.pop() {
|
||||||
|
match stack_frame {
|
||||||
|
DischargeStep::DischargeValue(value) => match value {
|
||||||
Value::Con(x) => Rc::new(Term::Constant(x)),
|
Value::Con(x) => Rc::new(Term::Constant(x)),
|
||||||
Value::Builtin { term, .. } => term,
|
Value::Builtin { term, .. } => term,
|
||||||
Value::Delay(body, env) => self.discharge_value_env(env, Rc::new(Term::Delay(body))),
|
Value::Delay(body, env) => {
|
||||||
|
stack.push(DischargeStep::DischargeValueEnv(
|
||||||
|
0,
|
||||||
|
env,
|
||||||
|
Rc::new(Term::Delay(body)),
|
||||||
|
));
|
||||||
|
}
|
||||||
Value::Lambda {
|
Value::Lambda {
|
||||||
parameter_name,
|
parameter_name,
|
||||||
body,
|
body,
|
||||||
env,
|
env,
|
||||||
} => self.discharge_value_env(
|
} => {
|
||||||
|
stack.push(DischargeStep::DischargeValueEnv(
|
||||||
|
0,
|
||||||
env,
|
env,
|
||||||
Rc::new(Term::Lambda {
|
Rc::new(Term::Lambda {
|
||||||
parameter_name: NamedDeBruijn {
|
parameter_name: NamedDeBruijn {
|
||||||
|
@ -222,31 +239,20 @@ impl Machine {
|
||||||
},
|
},
|
||||||
body,
|
body,
|
||||||
}),
|
}),
|
||||||
),
|
));
|
||||||
}
|
}
|
||||||
}
|
},
|
||||||
|
DischargeStep::DischargeValueEnv(lam_cnt, env, term) => match term.as_ref() {
|
||||||
fn discharge_value_env(
|
|
||||||
&mut self,
|
|
||||||
env: Rc<Vec<Value>>,
|
|
||||||
term: Rc<Term<NamedDeBruijn>>,
|
|
||||||
) -> Rc<Term<NamedDeBruijn>> {
|
|
||||||
fn rec(
|
|
||||||
lam_cnt: usize,
|
|
||||||
t: Rc<Term<NamedDeBruijn>>,
|
|
||||||
this: &mut Machine,
|
|
||||||
env: Rc<Vec<Value>>,
|
|
||||||
) -> Rc<Term<NamedDeBruijn>> {
|
|
||||||
match t.as_ref() {
|
|
||||||
Term::Var(name) => {
|
Term::Var(name) => {
|
||||||
let index: usize = name.index.into();
|
let index: usize = name.index.into();
|
||||||
|
|
||||||
if lam_cnt >= index {
|
if lam_cnt >= index {
|
||||||
Rc::new(Term::Var(name.clone()))
|
Rc::new(Term::Var(name.clone()))
|
||||||
} else {
|
} else {
|
||||||
env.get::<usize>(env.len() - (index - lam_cnt))
|
env.get::<usize>(env.len() - (index - lam_cnt))
|
||||||
.cloned()
|
.cloned()
|
||||||
.map_or(Rc::new(Term::Var(name.clone())), |v| {
|
.map_or(Rc::new(Term::Var(name.clone())), |v| {
|
||||||
this.discharge_value(v)
|
self.discharge_value(v)
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -255,19 +261,33 @@ impl Machine {
|
||||||
body,
|
body,
|
||||||
} => Rc::new(Term::Lambda {
|
} => Rc::new(Term::Lambda {
|
||||||
parameter_name: parameter_name.clone(),
|
parameter_name: parameter_name.clone(),
|
||||||
body: rec(lam_cnt + 1, Rc::clone(body), this, env),
|
body: self.discharge_value_env(lam_cnt + 1, env, Rc::clone(body)),
|
||||||
}),
|
}),
|
||||||
Term::Apply { function, argument } => Rc::new(Term::Apply {
|
Term::Apply { function, argument } => Rc::new(Term::Apply {
|
||||||
function: rec(lam_cnt, Rc::clone(function), this, Rc::clone(&env)),
|
function: self.discharge_value_env(
|
||||||
argument: rec(lam_cnt, Rc::clone(argument), this, env),
|
lam_cnt,
|
||||||
|
Rc::clone(&env),
|
||||||
|
Rc::clone(function),
|
||||||
|
),
|
||||||
|
argument: self.discharge_value_env(lam_cnt, env, Rc::clone(argument)),
|
||||||
}),
|
}),
|
||||||
|
|
||||||
Term::Delay(x) => Rc::new(Term::Delay(rec(lam_cnt, Rc::clone(x), this, env))),
|
Term::Delay(x) => Rc::new(Term::Delay(self.discharge_value_env(
|
||||||
Term::Force(x) => Rc::new(Term::Force(rec(lam_cnt, Rc::clone(x), this, env))),
|
lam_cnt,
|
||||||
|
env,
|
||||||
|
Rc::clone(x),
|
||||||
|
))),
|
||||||
|
Term::Force(x) => Rc::new(Term::Force(self.discharge_value_env(
|
||||||
|
lam_cnt,
|
||||||
|
env,
|
||||||
|
Rc::clone(x),
|
||||||
|
))),
|
||||||
rest => Rc::new(rest.clone()),
|
rest => Rc::new(rest.clone()),
|
||||||
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
rec(0, term, self, env)
|
|
||||||
|
todo!()
|
||||||
}
|
}
|
||||||
|
|
||||||
fn force_evaluate(&mut self, context: Rc<Context>, value: Value) -> Result<(), Error> {
|
fn force_evaluate(&mut self, context: Rc<Context>, value: Value) -> Result<(), Error> {
|
||||||
|
|
|
@ -84,6 +84,6 @@
|
||||||
i_0
|
i_0
|
||||||
]
|
]
|
||||||
)
|
)
|
||||||
(con integer 0)
|
(con integer 15)
|
||||||
]
|
]
|
||||||
)
|
)
|
Loading…
Reference in New Issue