Commit e3d1dff3 authored by Jeff Smits's avatar Jeff Smits

The amount of type annotations on collects makes me want to cry

parent 1498e079
......@@ -22,7 +22,7 @@ use std::io as stdio;
use try_from::TryInto;
use fnv::FnvHashMap;
use fnv::{FnvHashSet, FnvHashMap};
use strs::io;
use strs::factory::ATermFactory;
......@@ -92,34 +92,6 @@ trait CTreeOptimize {
fn optimize(self, context: &mut Self::Context) -> Self;
}
impl<'s> CTreeOptimize for preprocess_ext::Module<'s> {
type Context = ();
fn optimize(self, _: &mut Self::Context) -> Self {
use preprocess_ext::Module::*;
match self {
Module(name, decls) => {
Module(
name,
decls
.into_iter()
.map(|d| CTreeOptimize::optimize(d, &mut ()))
.collect(),
)
}
Specification(decls) => {
Specification(
decls
.into_iter()
.map(|d| CTreeOptimize::optimize(d, &mut ()))
.collect(),
)
}
}
}
}
// TODO: Add MaybeBoundTo
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
enum Value<'s> {
......@@ -164,6 +136,146 @@ impl<'a, 's> From<&'a Option<&'s str>> for Value<'s> {
}
}
struct Scope<'s> {
strategy: FnvHashMap<&'s str, (::std::result::Result<FnvHashSet<&'s str>, DynamicCall>, usize)>,
term: FnvHashMap<&'s str, Value<'s>>,
is_overlay: bool,
}
impl<'s> Scope<'s> {
fn from_let_defs<'a, I>(no_of_scopes: usize, defs: I) -> Self
where
I: IntoIterator<Item = &'a preprocess::Def<'s>>,
's: 'a,
{
Scope {
term: FnvHashMap::default(),
strategy: defs.into_iter()
.map(|def| {
(def.name, (match_vars_in_strategy(&def.body), no_of_scopes))
})
.collect(),
is_overlay: false,
}
}
fn from_fresh_variables<I>(fresh_vars: I) -> Self
where
I: IntoIterator<Item = &'s str>,
{
Scope {
term: fresh_vars
.into_iter()
.map(|fresh_var| (fresh_var, Value::UnBound))
.collect(),
strategy: FnvHashMap::default(),
is_overlay: false,
}
}
fn overlay() -> Self {
Scope {
term: FnvHashMap::default(),
strategy: FnvHashMap::default(),
is_overlay: true,
}
}
}
struct Scopes<'s>(Vec<Scope<'s>>);
impl<'s> Scopes<'s> {
fn push_scope(&mut self, scope: Scope<'s>) {
self.0.push(scope);
}
fn pop_scope(&mut self) -> Scope<'s> {
self.0.pop().expect(
"pop_scope: Interpreter bug, unexpected end of stack",
)
}
fn push_overlay(&mut self) {
self.0.push(Scope::overlay())
}
fn get_term<'a>(&'a self, term_name: &str) -> Option<&'a Value<'s>> {
self.0
.iter()
.rev()
.flat_map(|scope| scope.term.get(term_name))
.next()
}
fn apply_strategy<'a>(&'a mut self, strat_name: &str) {
let (vars, no_of_scopes) = self.0
.iter()
.rev()
.flat_map(|scope| scope.strategy.get(strat_name))
.cloned()
.next()
.expect("Strategy name was not found in any scope!");
if vars == Err(DynamicCall) {
conservative_maybe_bind(self);
return;
}
let vars = vars.unwrap();
for var in vars {
let mut offset = None;
for (n, scope) in self.0.iter().enumerate().rev().skip(self.0.len() - no_of_scopes).clone() {
if offset == None && scope.is_overlay {
offset = Some(n);
}
if scope.term.get(var) == Some(&Value::UnBound) {
offset = Some(offset.unwrap_or(n));
break;
}
}
self.0[offset.expect("Term name was not found in any scope!")]
.term
.insert(var, Value::MaybeBound);
}
}
fn set_term<'a>(&'a mut self, term_name: &'s str, value: Value<'s>) {
for scope in self.0.iter_mut().rev() {
if scope.term.contains_key(term_name) || scope.is_overlay {
scope.term.insert(term_name, value);
return;
}
}
unreachable!(format!("Name {} was not found in any scope!", term_name));
}
}
impl<'s> CTreeOptimize for preprocess_ext::Module<'s> {
type Context = ();
fn optimize(self, _: &mut Self::Context) -> Self {
use preprocess_ext::Module::*;
match self {
Module(name, decls) => {
Module(
name,
decls
.into_iter()
.map(|d| CTreeOptimize::optimize(d, &mut ()))
.collect(),
)
}
Specification(decls) => {
Specification(
decls
.into_iter()
.map(|d| CTreeOptimize::optimize(d, &mut ()))
.collect(),
)
}
}
}
}
impl<'s> CTreeOptimize for preprocess_ext::Decl<'s> {
type Context = ();
......@@ -192,32 +304,12 @@ impl<'s> CTreeOptimize for preprocess_ext::Def<'s> {
match self {
SDefT(name, sargs, targs, strat) => {
SDefT(
name,
sargs,
targs.clone(),
strat.optimize(&mut (
None,
targs
.into_iter()
.map(|vd| (vd.0, Value::UnBound))
.collect(),
)),
)
let mut context = (None, Scopes(vec![Scope::from_fresh_variables(targs.iter().map(|vd| vd.0))]));
SDefT(name, sargs, targs, strat.optimize(&mut context))
}
ExtSDefInl(name, sargs, targs, strat) => {
ExtSDefInl(
name,
sargs,
targs.clone(),
strat.optimize(&mut (
None,
targs
.into_iter()
.map(|vd| (vd.0, Value::UnBound))
.collect(),
)),
)
let mut context = (None, Scopes(vec![Scope::from_fresh_variables(targs.iter().map(|vd| vd.0))]));
ExtSDefInl(name, sargs, targs, strat.optimize(&mut context))
}
ExtSDef(name, sargs, targs) => ExtSDef(name, sargs, targs),
AnnoDef(annos, def) => AnnoDef(annos, Box::new(def.optimize(&mut ()))),
......@@ -225,17 +317,33 @@ impl<'s> CTreeOptimize for preprocess_ext::Def<'s> {
}
}
fn conservative_maybe_bind<'s>(map: &mut FnvHashMap<&'s str, Value<'s>>) {
for v in map.values_mut() {
if *v == Value::UnBound {
*v = Value::MaybeBound
fn conservative_maybe_bind<'s>(scopes: &mut Scopes<'s>) {
for scope in scopes.0.iter_mut() {
for v in scope.term.values_mut() {
if *v == Value::UnBound {
*v = Value::MaybeBound
}
}
}
}
fn conservative_maybe_bind2<'s, I>(scopes: &mut Scopes<'s>, affected_names: I)
where
I: IntoIterator<Item=&'s str>,
{
for name in affected_names {
for scope in scopes.0.iter_mut().rev() {
if scope.term.get(name) == Some(&Value::UnBound) {
scope.term.insert(name, Value::MaybeBound);
break;
}
}
}
}
// Pay attention, this is where the optimizing starts
impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
type Context = (Option<&'s str>, FnvHashMap<&'s str, Value<'s>>);
type Context = (Option<&'s str>, Scopes<'s>);
fn optimize(self, mut c: &mut Self::Context) -> Self {
use preprocess::Strategy;
......@@ -243,16 +351,32 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
use preprocess::BuildTerm;
match self {
Strategy::Let(defs, body) => Strategy::Let(defs, Box::new(body.optimize(c))),
Strategy::Let(defs, body) => {
let no_of_scopes = (c.1).0.len() + 1;
c.1.push_scope(Scope::from_let_defs(no_of_scopes, &defs));
let result = Strategy::Let(defs, Box::new(body.optimize(c)));
c.1.pop_scope();
result
}
Strategy::CallT(name, sargs, targs) => {
// We don't analyse calls right now, so set all guaranteed UnBound names to
// the conservative MaybeBound
conservative_maybe_bind(&mut c.1);
match sargs.iter().map(match_vars_in_strategy).collect() {
Err(DynamicCall) => {
conservative_maybe_bind(&mut c.1);
}
Ok(affected_names) => {
let affected_names: Vec<_> = affected_names;
c.1.apply_strategy(name);
// Set all affected UnBound names to the conservative MaybeBound
conservative_maybe_bind2(&mut c.1, affected_names.into_iter().flat_map(|s| s));
}
}
// We also don't know the return value of the call
c.0 = None;
Strategy::CallT(name, sargs, targs)
}
Strategy::CallDynamic(name, sargs, targs) => {
// We cannot resolve the name of the strategy during symbolic execution
// So bail out with conservative everything
conservative_maybe_bind(&mut c.1);
c.0 = None;
Strategy::CallDynamic(name, sargs, targs)
......@@ -263,9 +387,9 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
// If we match against a single variable...
if let MatchTerm::Var(v) = mt {
// ...and it's guaranteed to be UnBound at this point...
if c.1.get(v) == Some(&Value::UnBound) {
if c.1.get_term(v) == Some(&Value::UnBound) {
// ...we set the name to be bound to what the current value is
c.1.insert(v, (&c.0).into());
c.1.set_term(v, (&c.0).into());
// if the current value is also a known binding, we've found an alias
// that we can eliminate
if c.0.is_some() {
......@@ -285,7 +409,7 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
// If we build a single variable...
if let BuildTerm::Var(v) = bt {
// ...and the variable is guaranteed to be bound at this point
match c.1.get(v) {
match c.1.get_term(v) {
Some(&Value::Bound) => {
// ...we record that the current term is also this known binding
c.0 = Some(v);
......@@ -302,30 +426,18 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
Strategy::Build(bt)
}
Strategy::Scope(mut names, body) => {
// Here we model the scopes stack again, but this is the lazy (inefficient)
// approach where we just clone and mutate
let mut copy = c.clone();
// Initialise the scoped names
for name in &names {
copy.1.insert(name, Value::UnBound);
}
let new_body = body.optimize(&mut copy);
// copy over the return value
c.0 = copy.0;
// copy over the values from unscope names
for (name, value) in &copy.1 {
if !names.contains(name) {
c.1.insert(name, value.clone());
}
}
c.1.push_scope(Scope::from_fresh_variables(names.iter().map(|&s| s)));
let new_body = body.optimize(&mut c);
let mut scope = c.1.pop_scope();
// cull scoped names that we found to be aliases
copy.1.retain(|_, v| match *v {
scope.term.retain(|_, v| match *v {
Value::BoundTo(_) => true,
_ => false,
});
names.retain(|s| !copy.1.contains_key(s));
names.retain(|s| !scope.term.contains_key(s));
Strategy::Scope(names, Box::new(new_body))
}
......@@ -375,18 +487,21 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
let mut cs = Vec::with_capacity(pairs.len());
// Optimize each branch with a separate context
let mut pairs2 = Vec::with_capacity(pairs.len());
let cur = c.0.clone();
for (cond, then) in pairs.into_vec() {
let mut c = c.clone();
c.1.push_overlay();
let cond = cond.optimize(&mut c);
let then = then.optimize(&mut c);
pairs2.push((cond, then));
cs.push(c);
cs.push((c.0, c.1.pop_scope()));
c.0 = cur.clone();
}
// Same for final_else separately
let final_else = {
let mut c = c.clone();
c.1.push_overlay();
let result = (*final_else).clone().optimize(&mut c);
cs.push(c);
cs.push((c.0, c.1.pop_scope()));
c.0 = cur.clone();
result
};
// Merge contexts
......@@ -394,9 +509,9 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
c.0 = c.0.and_then(
|v| if copy.0 == Some(v) { Some(v) } else { None },
);
for (key, value) in copy.1 {
let new_value = c.1.get(key).map(|v| v.lub(&value)).unwrap_or(value);
c.1.insert(key, new_value);
for (key, value) in copy.1.term {
let new_value = c.1.get_term(key).map(|v| v.lub(&value)).unwrap_or(value);
c.1.set_term(key, new_value);
}
}
Strategy::GuardedLChoice(pairs2.into_boxed_slice(), Rc::new(final_else))
......@@ -406,17 +521,22 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
let mut cs = Vec::with_capacity(map.len());
// Optimize each branch with a separate context
let map = map.into_iter().map(|(cons, strat)| {
let mut c = c.clone();
let strat = strat.optimize(&mut c);
cs.push(c);
(cons, strat)
}).collect();
let cur = c.0.clone();
let map = map.into_iter()
.map(|(cons, strat)| {
c.1.push_overlay();
let strat = strat.optimize(&mut c);
cs.push((c.0, c.1.pop_scope()));
c.0 = cur.clone();
(cons, strat)
})
.collect();
// Same for final_else separately
let final_else = {
let mut c = c.clone();
c.1.push_overlay();
let result = (*final_else).clone().optimize(&mut c);
cs.push(c);
cs.push((c.0, c.1.pop_scope()));
c.0 = cur.clone();
result
};
// Merge contexts
......@@ -424,9 +544,9 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
c.0 = c.0.and_then(
|v| if copy.0 == Some(v) { Some(v) } else { None },
);
for (key, value) in copy.1 {
let new_value = c.1.get(key).map(|v| v.lub(&value)).unwrap_or(value);
c.1.insert(key, new_value);
for (key, value) in copy.1.term {
let new_value = c.1.get_term(key).map(|v| v.lub(&value)).unwrap_or(value);
c.1.set_term(key, new_value);
}
}
Strategy::ConsMatch(map, Rc::new(final_else))
......@@ -467,7 +587,7 @@ impl<'s> CTreeOptimize for preprocess::Strategy<'s> {
}
}
fn all_vars_bound<'s>(bt: &preprocess::BuildTerm<'s>, m: &FnvHashMap<&'s str, Value<'s>>) -> bool {
fn all_vars_bound<'s>(bt: &preprocess::BuildTerm<'s>, m: &Scopes<'s>) -> bool {
use preprocess::BuildTerm::*;
let mut stack = vec![bt];
......@@ -476,7 +596,7 @@ fn all_vars_bound<'s>(bt: &preprocess::BuildTerm<'s>, m: &FnvHashMap<&'s str, Va
while let Some(t) = stack.pop() {
match t {
&Var(v) => {
match m.get(v) {
match m.get_term(v) {
Some(val) => {
combined_value = combined_value.lub(val);
}
......@@ -502,14 +622,14 @@ fn all_vars_bound<'s>(bt: &preprocess::BuildTerm<'s>, m: &FnvHashMap<&'s str, Va
}
impl<'s> CTreeOptimize for preprocess::MatchTerm<'s> {
type Context = (Option<&'s str>, FnvHashMap<&'s str, Value<'s>>);
type Context = (Option<&'s str>, Scopes<'s>);
fn optimize(self, mut c: &mut Self::Context) -> Self {
use preprocess::MatchTerm::*;
match self {
Var(v) => {
if let Some(&Value::BoundTo(v2)) = c.1.get(v) {
if let Some(&Value::BoundTo(v2)) = c.1.get_term(v) {
Var(v2)
} else {
Var(v)
......@@ -528,7 +648,7 @@ impl<'s> CTreeOptimize for preprocess::MatchTerm<'s> {
)
}
As(v, term) => {
if let Some(&Value::BoundTo(v2)) = c.1.get(v) {
if let Some(&Value::BoundTo(v2)) = c.1.get_term(v) {
As(v2, Box::new(term.optimize(c)))
} else {
As(v, Box::new(term.optimize(c)))
......@@ -540,14 +660,14 @@ impl<'s> CTreeOptimize for preprocess::MatchTerm<'s> {
}
impl<'s> CTreeOptimize for preprocess::BuildTerm<'s> {
type Context = (Option<&'s str>, FnvHashMap<&'s str, Value<'s>>);
type Context = (Option<&'s str>, Scopes<'s>);
fn optimize(self, mut c: &mut Self::Context) -> Self {
use preprocess::BuildTerm::*;
match self {
Var(v) => {
if let Some(&Value::BoundTo(v2)) = c.1.get(v) {
if let Some(&Value::BoundTo(v2)) = c.1.get_term(v) {
Var(v2)
} else {
Var(v)
......@@ -569,6 +689,104 @@ impl<'s> CTreeOptimize for preprocess::BuildTerm<'s> {
}
}
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
struct DynamicCall;
fn match_vars_in_strategy<'s>(
strat: &preprocess::Strategy<'s>,
) -> ::std::result::Result<FnvHashSet<&'s str>, DynamicCall> {
use preprocess::Strategy;
match *strat {
Strategy::Let(_, ref body) => match_vars_in_strategy(body),
// TODO: add vars from Call
Strategy::CallT(_, ref sargs, _) => {
let result = sargs.iter().map(match_vars_in_strategy).collect::<::std::result::Result<Vec<FnvHashSet<&'s str>>, DynamicCall>>()?;
Ok(result.into_iter().flat_map(|s| s).collect())
},
Strategy::CallDynamic(_, _, _) => Err(DynamicCall),
Strategy::Fail => Ok(FnvHashSet::default()),
Strategy::Id => Ok(FnvHashSet::default()),
Strategy::Match(ref term) => Ok(match_vars(term)),
Strategy::Build(_) => Ok(FnvHashSet::default()),
Strategy::Scope(ref names, ref body) => {
let name_set: FnvHashSet<&'s str> = names.iter().map(|&s| s).collect();
match match_vars_in_strategy(body) {
Ok(mut v) => {
v.retain(|n| !name_set.contains(n));
Ok(v)
}
Err(e) => Err(e),
}
}
Strategy::Seq(ref strats) => {
let result = strats.iter().map(match_vars_in_strategy).collect::<::std::result::Result<Vec<FnvHashSet<&'s str>>, DynamicCall>>()?;
Ok(result.into_iter().flat_map(|s| s).collect())
},
Strategy::GuardedLChoice(ref pairs, ref s_else) => {
let pairs_names = pairs
.iter()
.map(|&(ref s_if, ref s_then)| {
let one = match_vars_in_strategy(s_if)?;
let two = match_vars_in_strategy(s_then)?;
Ok(one.union(&two).map(|&s| s).collect::<FnvHashSet<&'s str>>())
})
.collect::<::std::result::Result<Vec<FnvHashSet<&'s str>>, DynamicCall>>()?;
let pairs_names: FnvHashSet<&'s str> = pairs_names.into_iter().flat_map(|s| s).collect();
Ok(pairs_names.union(&match_vars_in_strategy(s_else)?).map(|&s| s).collect())
}
Strategy::ConsMatch(ref map, _) => {
let result = map.values().map(match_vars_in_strategy).collect::<::std::result::Result<Vec<FnvHashSet<&'s str>>, DynamicCall>>()?;
Ok(result.into_iter().flat_map(|s| s).collect())
},
Strategy::PrimT(_, ref sargs, _) => {
let result = sargs.iter().map(match_vars_in_strategy).collect::<::std::result::Result<Vec<FnvHashSet<&'s str>>, DynamicCall>>()?;
Ok(result.into_iter().flat_map(|s| s).collect())
},
Strategy::Some(ref s) => match_vars_in_strategy(s),
Strategy::One(ref s) => match_vars_in_strategy(s),
Strategy::All(ref s) => match_vars_in_strategy(s),
Strategy::ImportTerm(_) => Ok(FnvHashSet::default()),
}
}
fn match_vars<'s>(term: &preprocess::MatchTerm<'s>) -> FnvHashSet<&'s str> {
use preprocess::MatchTerm;
let mut result = FnvHashSet::default();
let mut stack = vec![term];
while let Some(term) = stack.pop() {
match *term {
MatchTerm::Var(v) => {
result.insert(v);
}
MatchTerm::Int(_) |
MatchTerm::Real(_) |
MatchTerm::Str(_) |
MatchTerm::Wld => {}
MatchTerm::Anno(ref t1, ref t2) => {
stack.push(&**t1);
stack.push(&**t2);
}
MatchTerm::Op(_, ref ts) => {
for t in ts {
stack.push(t);
}
}
MatchTerm::Explode(ref t1, ref t2) => {
stack.push(&**t1);
stack.push(&**t2);
}
MatchTerm::As(v, ref t) => {
result.insert(v);
stack.push(&**t);
}
MatchTerm::Cached(_, _) => {}
}
}
result
}
#[cfg(test)]
mod test {
use super::*;
......@@ -577,7 +795,10 @@ mod test {
fn string_optimize(program: &'static str) -> String {
let factory = ATermFactory::new();
let program = factory.read_ascii_string(&program).expect("ATerm representation of CTree").0;
let program = factory
.read_ascii_string(&program)
.expect("ATerm representation of CTree")
.0;
let program: ctree::Module = (&program).try_into().expect("Typed CTree");
let program: preprocess_ext::Module = program.try_into().expect("Preprocessed CTree");
......@@ -593,4 +814,4 @@ mod test {
let expected = r#"Specification([Signature([Constructors([OpDecl("Nil",ConstType(Sort("Term",[]))),OpDecl("Cons",FunType([ConstType(Sort("Term",[])),ConstType(Sort("Term",[]))],ConstType(Sort("Term",[]))))])]),Strategies([SDefT("main_0_0",[],[],Scope(["l_0"],Seq(Match(Var("l_0")),Build(Anno(Op("Cons",[Var("l_0"),Anno(Op("Nil",[]),Op("Nil",[]))]),Op("Nil",[]))))))])])"#;
assert_eq!(expected, string_optimize(input));
}
}
\ No newline at end of file
}
......@@ -59,7 +59,6 @@ impl<'d, 'f: 'd> MutContext<'d, 'f> {
result
}
// Should really return a &SDef, but I can't figure out lifetimes that borrowck will accept :(
pub fn get_strategy(&self, strat_name: &str) -> Result<StrategyDef<'d, 'f>> {
self.scopes
.borrow()
......
......@@ -421,14 +421,15 @@ impl<'a> ATermWrite for Strategy<'a> {
write!(writer, "{}", str::repeat(")", pairs.len()))
}
Strategy::ConsMatch(ref map, ref final_else) => {
let strat = map.values().fold(final_else.clone(), |else_strat, glc| {
match *glc {
let strat = map.values().fold(
final_else.clone(),
|else_strat, glc| match *glc {
Strategy::GuardedLChoice(ref pairs, _) => {
Rc::new(Strategy::GuardedLChoice(pairs.clone(), else_strat))
}
_ => unreachable!("ConsMatch should have GuardedLChoices"),
}
});
},
);
strat.to_ascii(writer)
}
Strategy::PrimT(name, ref sargs, ref targs) => {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment