2012-07-16 17:27:04 -07:00
|
|
|
/// Correctness for protocols
|
|
|
|
|
|
|
|
/*
|
|
|
|
|
|
|
|
This section of code makes sure the protocol is likely to generate
|
|
|
|
correct code. The correctness criteria include:
|
|
|
|
|
|
|
|
* No protocols transition to states that don't exist.
|
|
|
|
* Messages step to states with the right number of type parameters.
|
|
|
|
|
|
|
|
In addition, this serves as a lint pass. Lint warns for the following
|
|
|
|
things.
|
|
|
|
|
|
|
|
* States with no messages, it's better to step to !.
|
|
|
|
|
|
|
|
It would also be nice to warn about unreachable states, but the
|
|
|
|
visitor infrastructure for protocols doesn't currently work well for
|
|
|
|
that.
|
|
|
|
|
|
|
|
*/
|
|
|
|
|
|
|
|
import dvec::extensions;
|
|
|
|
|
|
|
|
import ext::base::ext_ctxt;
|
|
|
|
|
|
|
|
import ast::{ident};
|
|
|
|
|
|
|
|
import proto::{state, protocol, next_state, methods};
|
|
|
|
import ast_builder::empty_span;
|
|
|
|
|
|
|
|
impl proto_check of proto::visitor<(), (), ()> for ext_ctxt {
|
|
|
|
fn visit_proto(_proto: protocol,
|
|
|
|
_states: &[()]) { }
|
|
|
|
|
|
|
|
fn visit_state(state: state, _m: &[()]) {
|
|
|
|
if state.messages.len() == 0 {
|
|
|
|
self.span_warn(
|
2012-07-24 16:58:48 -07:00
|
|
|
state.span, // use a real span!
|
2012-07-30 16:01:07 -07:00
|
|
|
fmt!{"state %s contains no messages, \
|
2012-07-16 17:27:04 -07:00
|
|
|
consider stepping to a terminal state instead",
|
2012-07-30 16:01:07 -07:00
|
|
|
*state.name})
|
2012-07-16 17:27:04 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2012-07-24 16:58:48 -07:00
|
|
|
fn visit_message(name: ident, _span: span, _tys: &[@ast::ty],
|
2012-07-16 17:27:04 -07:00
|
|
|
this: state, next: next_state) {
|
2012-07-17 12:51:24 -07:00
|
|
|
alt next {
|
2012-08-03 19:59:04 -07:00
|
|
|
some({state: next, tys: next_tys}) => {
|
2012-07-17 12:51:24 -07:00
|
|
|
let proto = this.proto;
|
|
|
|
if !proto.has_state(next) {
|
|
|
|
// This should be a span fatal, but then we need to
|
|
|
|
// track span information.
|
2012-07-16 17:27:04 -07:00
|
|
|
self.span_err(
|
2012-07-24 16:58:48 -07:00
|
|
|
proto.get_state(next).span,
|
2012-07-30 16:01:07 -07:00
|
|
|
fmt!{"message %s steps to undefined state, %s",
|
|
|
|
*name, *next});
|
2012-07-17 12:51:24 -07:00
|
|
|
}
|
|
|
|
else {
|
|
|
|
let next = proto.get_state(next);
|
|
|
|
|
|
|
|
if next.ty_params.len() != next_tys.len() {
|
|
|
|
self.span_err(
|
2012-07-24 16:58:48 -07:00
|
|
|
next.span, // use a real span
|
2012-07-30 16:01:07 -07:00
|
|
|
fmt!{"message %s target (%s) \
|
2012-07-17 12:51:24 -07:00
|
|
|
needs %u type parameters, but got %u",
|
|
|
|
*name, *next.name,
|
|
|
|
next.ty_params.len(),
|
2012-07-30 16:01:07 -07:00
|
|
|
next_tys.len()});
|
2012-07-17 12:51:24 -07:00
|
|
|
}
|
2012-07-16 17:27:04 -07:00
|
|
|
}
|
|
|
|
}
|
2012-08-03 19:59:04 -07:00
|
|
|
none => ()
|
2012-07-16 17:27:04 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|