Skip to content

Commit

Permalink
Merge #87
Browse files Browse the repository at this point in the history 
87: Spanned name for Var Definition r=adjivas a=adjivas

Short PR to prepare EnumDef check cases of issue #5 .

Co-authored-by: adjivas <[email protected]>
  • Loading branch information
@bors @adjivas
bors[bot] and adjivas committed Jul 26, 2018
2 parents 1fd4501 + 3be819c commit d01cf63
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 62 deletions.
38 changes: 0 additions & 38 deletions telamon-gen/src/ast/constraint.rs
View file

This file was deleted.

83 changes: 64 additions & 19 deletions telamon-gen/src/ast/context.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ impl TypingContext {
quotient: Option<Quotient>) {
trace!("defining set {}", name);
let mut var_map = VarMap::default();
let arg_name = arg_def.as_ref().map(|var| "$".to_string() + &var.name);
let arg_name = arg_def.as_ref().map(|var| "$".to_string() + &var.name.data);
let arg = arg_def.clone().map(|arg| var_map.decl_argument(&self.ir_desc, arg));
let superset = superset.map(|set| set.type_check(&self.ir_desc, &var_map));
for disjoint in &disjoints { self.ir_desc.get_set_def(disjoint); }
Expand All @@ -99,7 +99,7 @@ impl TypingContext {
// Handle the optional forall.
if key == ir::SetDefKey::Reverse {
let var_def = var.as_ref().unwrap();
let var_name = "$".to_string() + &var_def.name;
let var_name = "$".to_string() + &var_def.name.data;
value = value.replace(&var_name, "$var");
env.push("var");
} else { assert!(var.is_none()); }
Expand Down Expand Up @@ -146,17 +146,29 @@ impl TypingContext {
let forall_vars = arg.clone().into_iter()
.chain(std::iter::once(quotient.item)).collect_vec();
let counter_name = self.create_repr_counter(
set.name().clone(), &repr_name, arg.clone(), item_name.clone(),
set.name().clone(), &repr_name, arg.clone(), item_name.data.clone(),
forall_vars.clone(),
RcStr::new(quotient.equiv_relation.0),
quotient.equiv_relation.1);
// Generate the code that set an item as representant.
let trigger_code = print::add_to_quotient(
set, &repr_name, &counter_name, &item_name, &arg_name);
set, &repr_name, &counter_name, &item_name.data,
&arg_name.clone().map(|n| n.data)
);
// Constraint the representative value.
let forall_names = forall_vars.iter().map(|x| x.name.clone()).collect_vec();
let repr_instance = ChoiceInstance { name: repr_name, vars: forall_names.clone() };
let counter_instance = ChoiceInstance { name: counter_name, vars: forall_names };
let repr_instance = ChoiceInstance {
name: repr_name,
vars: forall_names.iter()
.map(|n| n.data.clone())
.collect::<Vec<_>>()
};
let counter_instance = ChoiceInstance {
name: counter_name,
vars: forall_names.iter()
.map(|n| n.data.clone())
.collect::<Vec<_>>()
};
let not_repr = Condition::new_is_bool(repr_instance.clone(), false);
let counter_leq_zero = Condition::CmpCode {
lhs: counter_instance, rhs: "0".into(), op: ir::CmpOp::Leq
Expand Down Expand Up @@ -185,7 +197,7 @@ impl TypingContext {
// Add the constraint `item in set => repr is TRUE`.
let quotient_item_def = VarDef {
name: item_name,
set: SetRef { name: set.name().clone(), var: arg_name }
set: SetRef { name: set.name().clone(), var: arg_name.map(|n| n.data) }
};
let item_in_set_foralls = arg.into_iter()
.chain(std::iter::once(quotient_item_def)).collect();
Expand All @@ -202,15 +214,18 @@ impl TypingContext {
fn create_repr_choice(&mut self, name: RcStr,
set: &ir::SetDef,
arg: Option<VarDef>,
item_name: RcStr) {
item_name: Spanned<RcStr>) {
let bool_str: RcStr = "Bool".into();
let def = ir::ChoiceDef::Enum(bool_str.clone());
let mut vars = Vec::new();
if let Some(arg) = arg.as_ref() {
vars.push((arg.name.clone(), set.arg().unwrap().clone()));
}
vars.push((item_name, set.superset().unwrap().clone()));
let args = ir::ChoiceArguments::new(vars, false, false);
let args = ir::ChoiceArguments::new(vars.into_iter()
.map(|(n, s)| (n.data, s))
.collect(),
false, false);
let mut repr = ir::Choice::new(name, None, args, def);
let false_value_set = std::iter::once("FALSE".into()).collect();
repr.add_fragile_values(ir::ValueSet::enum_values(bool_str, false_value_set));
Expand All @@ -233,7 +248,7 @@ impl TypingContext {
let rhs_name = RcStr::new(format!("{}_repr", item_name));
let rhs_set = SetRef {
name: set_name,
var: arg.as_ref().map(|d| d.name.clone())
var: arg.as_ref().map(|d| d.name.data.clone())
};
let equiv_choice = ChoiceInstance {
name: equiv_choice_name,
Expand All @@ -246,7 +261,11 @@ impl TypingContext {
let body = CounterBody {
base: "0".to_string(),
conditions: vec![condition],
iter_vars: vec![VarDef { name: rhs_name, set: rhs_set }],
iter_vars: vec![VarDef { name: Spanned {
data: rhs_name,
beg: Default::default(),
end: Default::default()
}, set: rhs_set }],
kind: ir::CounterKind::Add,
value: CounterVal::Code("1".to_string()),
};
Expand Down Expand Up @@ -280,8 +299,12 @@ impl TypingContext {
let vars = vars.into_iter().map(|v| {
let name = v.name.clone();
(name, var_map.decl_argument(&self.ir_desc, v))
}).collect();
let arguments = ir::ChoiceArguments::new(vars, symmetric, inverse);
}).collect::<Vec<_>>();
let arguments = ir::ChoiceArguments::new(vars.into_iter()
.map(|(n, s)| (n.data, s))
.collect::<Vec<_>>(),
symmetric,
inverse);
let inverse = if let Some(Symmetry::AntiSymmetric(mapping)) = stmts.symmetry {
{
let mut mapped = HashSet::default();
Expand Down Expand Up @@ -330,8 +353,11 @@ impl TypingContext {
let vars = def.variables.into_iter().map(|v| {
let name = v.name.clone();
(name, var_map.decl_argument(&self.ir_desc, v))
}).collect();
let arguments = ir::ChoiceArguments::new(vars, false, false);
}).collect::<Vec<_>>();
let arguments = ir::ChoiceArguments::new(vars.into_iter()
.map(|(n, s)| (n.data, s))
.collect::<Vec<_>>(),
false, false);
let universe = type_check_code(def.code.into(), &var_map);
let choice_def = ir::ChoiceDef::Number { universe };
self.ir_desc.add_choice(ir::Choice::new(choice_name, doc, arguments, choice_def));
Expand All @@ -340,8 +366,14 @@ impl TypingContext {
/// Register a constraint on an enum value.
fn register_value_constraint(&mut self, choice: RcStr, args: Vec<VarDef>,
value: RcStr, mut constraint: Constraint) {
let choice_args = args.iter().map(|def| def.name.clone()).collect();
let self_instance = ChoiceInstance { name: choice, vars: choice_args };
let choice_args =
args.iter().map(|def| def.name.clone())
.collect::<Vec<_>>();
let self_instance = ChoiceInstance {
name: choice, vars: choice_args.into_iter()
.map(|n| n.data)
.collect::<Vec<_>>()
};
let condition = Condition::Is { lhs: self_instance, rhs: vec![value], is: false };
constraint.forall_vars.extend(args);
for disjunction in &mut constraint.disjunctions {
Expand Down Expand Up @@ -372,7 +404,18 @@ impl TypingContext {
}).collect_vec();
let doc = doc.map(RcStr::new);
let (incr, incr_condition) = self.gen_increment(
&counter_name, &vars, &iter_vars, all_var_defs, body.conditions, &var_map);
&counter_name,
vars.iter()
.cloned()
.map(|(n, s)| (n.data, s))
.collect::<Vec<_>>()
.as_slice(),
iter_vars.iter()
.cloned()
.map(|(n, s)| (n.data, s))
.collect::<Vec<_>>()
.as_slice(),
all_var_defs, body.conditions, &var_map);
// Type check the value.
let value = match body.value {
CounterVal::Code(code) =>
Expand All @@ -394,7 +437,9 @@ impl TypingContext {
let counter_def = ir::ChoiceDef::Counter {
incr_iter, kind, value, incr, incr_condition, visibility, base
};
let counter_args = ir::ChoiceArguments::new(vars, false, false);
let counter_args = ir::ChoiceArguments::new(vars.into_iter()
.map(|(n, s)| (n.data, s))
.collect(), false, false);
let mut counter_choice = ir::Choice::new(
counter_name, doc, counter_args, counter_def);
// Filter the counter itself after an update, because the filter actually acts on
Expand Down
6 changes: 3 additions & 3 deletions telamon-gen/src/ast/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ impl SetRef {
/// Defines a variable.
#[derive(Debug, Clone)]
pub struct VarDef {
pub name: RcStr,
pub name: Spanned<RcStr>,
pub set: SetRef,
}

Expand Down Expand Up @@ -339,9 +339,9 @@ impl VarMap {
fn decl_var(&mut self, ir_desc: &ir::IrDesc, var_def: VarDef,
var: ir::Variable) -> ir::Set {
let set = var_def.set.type_check(ir_desc, self);
match self.map.entry(var_def.name.clone()) {
match self.map.entry(var_def.name.data.clone()) {
hash_map::Entry::Occupied(..) =>
panic!("variable {} defined twice", var_def.name),
panic!("variable {} defined twice", var_def.name.data),
hash_map::Entry::Vacant(entry) => { entry.insert((var, set.clone())); },
};
set
Expand Down
8 changes: 6 additions & 2 deletions telamon-gen/src/parser.lalrpop
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,13 @@ set_disjoint: Vec<String> = {

choice_vars = { list<var_def, ","> };

rc_var: RcStr = {
<name: var> => RcStr::new(name),
};

var_def: ast::VarDef = {
<name: var> in_ <set: set_ref> => {
ast::VarDef { name: RcStr::new(name), set }
<spanned_name: spanned<rc_var>> in_ <set: set_ref> => {
ast::VarDef { name: spanned_name, set }
},
};

Expand Down

0 comments on commit d01cf63

Please sign in to comment.