remove typestate from code, tests, and docs
This commit is contained in:
Niko Matsakis
parent
1fbb9d035d
commit
41a21f053c
331
doc/rust.md
331
doc/rust.md
@ -211,7 +211,7 @@ The keywords in [source files](#source-files) are the following strings:
|
||||
~~~~~~~~ {.keyword}
|
||||
alt again assert
|
||||
break
|
||||
check claim class const copy
|
||||
check class const copy
|
||||
drop
|
||||
else enum export extern
|
||||
fail false fn for
|
||||
@ -1926,10 +1926,6 @@ an optional reference slot to serve as the function's output, bound to the
|
||||
`lval` on the right hand side of the call. If the function eventually returns,
|
||||
then the expression completes.
|
||||
|
||||
A call expression statically requires that the precondition declared in the
|
||||
callee's signature is satisfied by the expression prestate. In this way,
|
||||
typestates propagate through function boundaries.
|
||||
|
||||
An example of a call expression:
|
||||
|
||||
~~~~
|
||||
@ -2354,117 +2350,6 @@ library. It is best to use the macro forms of logging (*#error*,
|
||||
when it is changed.
|
||||
|
||||
|
||||
### Check expressions
|
||||
|
||||
~~~~~~~~{.ebnf .gram}
|
||||
check_expr : "check" call_expr ;
|
||||
~~~~~~~~
|
||||
|
||||
A `check` expression connects dynamic assertions made at run-time to the
|
||||
static [typestate system](#typestate-system). A `check` expression takes a
|
||||
constraint to check at run-time. If the constraint holds at run-time, control
|
||||
passes through the `check` and on to the next expression in the enclosing
|
||||
block. If the condition fails to hold at run-time, the `check` expression
|
||||
behaves as a `fail` expression.
|
||||
|
||||
The typestate algorithm is built around `check` expressions, and in particular
|
||||
the fact that control *will not pass* a check expression with a condition that
|
||||
fails to hold. The typestate algorithm can therefore assume that the (static)
|
||||
postcondition of a `check` expression includes the checked constraint
|
||||
itself. From there, the typestate algorithm can perform dataflow calculations
|
||||
on subsequent expressions, propagating [conditions](#conditions) forward and
|
||||
statically comparing implied states and their specifications.
|
||||
|
||||
~~~~~~~~
|
||||
# fn print(i: int) { }
|
||||
|
||||
pure fn even(x: int) -> bool {
|
||||
ret x & 1 == 0;
|
||||
}
|
||||
|
||||
fn print_even(x: int) : even(x) {
|
||||
print(x);
|
||||
}
|
||||
|
||||
fn test() {
|
||||
let y: int = 8;
|
||||
|
||||
// Cannot call print_even(y) here.
|
||||
|
||||
check even(y);
|
||||
|
||||
// Can call print_even(y) here, since even(y) now holds.
|
||||
print_even(y);
|
||||
}
|
||||
~~~~~~~~
|
||||
|
||||
### Prove expressions
|
||||
|
||||
**Note: Prove expressions are not yet supported by the compiler.**
|
||||
|
||||
~~~~~~~~{.ebnf .gram}
|
||||
prove_expr : "prove" call_expr ;
|
||||
~~~~~~~~
|
||||
|
||||
A `prove` expression has no run-time effect. Its purpose is to statically
|
||||
check (and document) that its argument constraint holds at its expression
|
||||
entry point. If its argument typestate does not hold, under the typestate
|
||||
algorithm, the program containing it will fail to compile.
|
||||
|
||||
### Claim expressions
|
||||
|
||||
~~~~~~~~{.ebnf .gram}
|
||||
claim_expr : "claim" call_expr ;
|
||||
~~~~~~~~
|
||||
|
||||
A `claim` expression is an unsafe variant on a `check` expression that is not
|
||||
actually checked at runtime. Thus, using a `claim` implies a proof obligation
|
||||
to ensure---without compiler assistance---that an assertion always holds.
|
||||
|
||||
Setting a runtime flag can turn all `claim` expressions into `check`
|
||||
expressions in a compiled Rust program, but the default is to not check the
|
||||
assertion contained in a `claim`. The idea behind `claim` is that performance
|
||||
profiling might identify a few bottlenecks in the code where actually checking
|
||||
a given callee's predicate is too expensive; `claim` allows the code to
|
||||
typecheck without removing the predicate check at every other call site.
|
||||
|
||||
|
||||
|
||||
### If-Check expressions
|
||||
|
||||
An `if check` expression combines a `if` expression and a `check`
|
||||
expression in an indivisible unit that can be used to build more complex
|
||||
conditional control-flow than the `check` expression affords.
|
||||
|
||||
In fact, `if check` is a "more primitive" expression than `check`;
|
||||
instances of the latter can be rewritten as instances of the former. The
|
||||
following two examples are equivalent:
|
||||
|
||||
Example using `check`:
|
||||
|
||||
~~~~
|
||||
# pure fn even(x: int) -> bool { true }
|
||||
# fn print_even(x: int) { }
|
||||
# let x = 0;
|
||||
|
||||
check even(x);
|
||||
print_even(x);
|
||||
~~~~
|
||||
|
||||
Equivalent example using `if check`:
|
||||
|
||||
~~~~
|
||||
# pure fn even(x: int) -> bool { true }
|
||||
# fn print_even(x: int) { }
|
||||
# let x = 0;
|
||||
|
||||
if check even(x) {
|
||||
print_even(x);
|
||||
} else {
|
||||
fail;
|
||||
}
|
||||
~~~~
|
||||
|
||||
### Assert expressions
|
||||
|
||||
~~~~~~~~{.ebnf .gram}
|
||||
@ -2813,220 +2698,6 @@ Sending operations are not part of the Rust language, but are
|
||||
implemented in the library. Generic functions that send values bound
|
||||
the kind of these values to sendable.
|
||||
|
||||
|
||||
|
||||
## Typestate system
|
||||
|
||||
|
||||
Rust programs have a static semantics that determine the types of values
|
||||
produced by each expression, as well as the *predicates* that hold over
|
||||
slots in the environment at each point in time during execution.
|
||||
|
||||
The latter semantics -- the dataflow analysis of predicates holding over slots
|
||||
-- is called the *typestate* system.
|
||||
|
||||
### Points
|
||||
|
||||
Control flows from statement to statement in a block, and through the
|
||||
evaluation of each expression, from one sub-expression to another. This
|
||||
sequential control flow is specified as a set of _points_, each of which
|
||||
has a set of points before and after it in the implied control flow.
|
||||
|
||||
For example, this code:
|
||||
|
||||
~~~~~~~~
|
||||
# let mut s;
|
||||
|
||||
s = ~"hello, world";
|
||||
io::println(s);
|
||||
~~~~~~~~
|
||||
|
||||
Consists of 2 statements, 3 expressions and 12 points:
|
||||
|
||||
|
||||
* the point before the first statement
|
||||
* the point before evaluating the static initializer `"hello, world"`
|
||||
* the point after evaluating the static initializer `"hello, world"`
|
||||
* the point after the first statement
|
||||
* the point before the second statement
|
||||
* the point before evaluating the function value `println`
|
||||
* the point after evaluating the function value `println`
|
||||
* the point before evaluating the arguments to `println`
|
||||
* the point before evaluating the symbol `s`
|
||||
* the point after evaluating the symbol `s`
|
||||
* the point after evaluating the arguments to `println`
|
||||
* the point after the second statement
|
||||
|
||||
|
||||
Whereas this code:
|
||||
|
||||
|
||||
~~~~~~~~
|
||||
# fn x() -> ~str { ~"" }
|
||||
# fn y() -> ~str { ~"" }
|
||||
|
||||
io::println(x() + y());
|
||||
~~~~~~~~
|
||||
|
||||
Consists of 1 statement, 7 expressions and 14 points:
|
||||
|
||||
|
||||
* the point before the statement
|
||||
* the point before evaluating the function value `println`
|
||||
* the point after evaluating the function value `println`
|
||||
* the point before evaluating the arguments to `println`
|
||||
* the point before evaluating the arguments to `+`
|
||||
* the point before evaluating the function value `x`
|
||||
* the point after evaluating the function value `x`
|
||||
* the point before evaluating the arguments to `x`
|
||||
* the point after evaluating the arguments to `x`
|
||||
* the point before evaluating the function value `y`
|
||||
* the point after evaluating the function value `y`
|
||||
* the point before evaluating the arguments to `y`
|
||||
* the point after evaluating the arguments to `y`
|
||||
* the point after evaluating the arguments to `+`
|
||||
* the point after evaluating the arguments to `println`
|
||||
|
||||
|
||||
The typestate system reasons over points, rather than statements or
|
||||
expressions. This may seem counter-intuitive, but points are the more
|
||||
primitive concept. Another way of thinking about a point is as a set of
|
||||
*instants in time* at which the state of a task is fixed. By contrast, a
|
||||
statement or expression represents a *duration in time*, during which the
|
||||
state of the task changes. The typestate system is concerned with constraining
|
||||
the possible states of a task's memory at *instants*; it is meaningless to
|
||||
speak of the state of a task's memory "at" a statement or expression, as each
|
||||
statement or expression is likely to change the contents of memory.
|
||||
|
||||
|
||||
### Control flow graph
|
||||
|
||||
Each *point* can be considered a vertex in a directed *graph*. Each
|
||||
kind of expression or statement implies a number of points *and edges* in
|
||||
this graph. The edges connect the points within each statement or expression,
|
||||
as well as between those points and those of nearby statements and expressions
|
||||
in the program. The edges between points represent *possible* indivisible
|
||||
control transfers that might occur during execution.
|
||||
|
||||
This implicit graph is called the _control-flow graph_, or _CFG_.
|
||||
|
||||
|
||||
### Constraints
|
||||
|
||||
A [_predicate_](#predicate-functions) is a pure boolean function declared with
|
||||
the keywords `pure fn`.
|
||||
|
||||
A _constraint_ is a predicate applied to specific slots.
|
||||
|
||||
For example, consider the following code:
|
||||
|
||||
~~~~~~~~
|
||||
pure fn is_less_than(a: int, b: int) -> bool {
|
||||
ret a < b;
|
||||
}
|
||||
|
||||
fn test() {
|
||||
let x: int = 10;
|
||||
let y: int = 20;
|
||||
check is_less_than(x,y);
|
||||
}
|
||||
~~~~~~~~
|
||||
|
||||
This example defines the predicate `is_less_than`, and applies it to the slots
|
||||
`x` and `y`. The constraint being checked on the third line of the function is
|
||||
`is_less_than(x,y)`.
|
||||
|
||||
Predicates can only apply to slots holding immutable values. The slots a
|
||||
predicate applies to can themselves be mutable, but the types of values held
|
||||
in those slots must be immutable.
|
||||
|
||||
### Conditions
|
||||
|
||||
A _condition_ is a set of zero or more constraints.
|
||||
|
||||
Each *point* has an associated *condition*:
|
||||
|
||||
* The _precondition_ of a statement or expression is the condition required at
|
||||
in the point before it.
|
||||
* The _postcondition_ of a statement or expression is the condition enforced
|
||||
in the point after it.
|
||||
|
||||
Any constraint present in the precondition and *absent* in the postcondition
|
||||
is considered to be *dropped* by the statement or expression.
|
||||
|
||||
|
||||
### Calculated typestates
|
||||
|
||||
The typestate checking system *calculates* an additional condition for each
|
||||
point called its _typestate_. For a given statement or expression, we call the
|
||||
two typestates associated with its two points the prestate and a poststate.
|
||||
|
||||
* The _prestate_ of a statement or expression is the typestate of the
|
||||
point before it.
|
||||
* The _poststate_ of a statement or expression is the typestate of the
|
||||
point after it.
|
||||
|
||||
A _typestate_ is a condition that has _been determined by the typestate
|
||||
algorithm_ to hold at a point. This is a subtle but important point to
|
||||
understand: preconditions and postconditions are *inputs* to the typestate
|
||||
algorithm; prestates and poststates are *outputs* from the typestate
|
||||
algorithm.
|
||||
|
||||
The typestate algorithm analyses the preconditions and postconditions of every
|
||||
statement and expression in a block, and computes a condition for each
|
||||
typestate. Specifically:
|
||||
|
||||
|
||||
* Initially, every typestate is empty.
|
||||
* Each statement or expression's poststate is given the union of the its
|
||||
prestate, precondition, and postcondition.
|
||||
* Each statement or expression's poststate has the difference between its
|
||||
precondition and postcondition removed.
|
||||
* Each statement or expression's prestate is given the intersection of the
|
||||
poststates of every predecessor point in the CFG.
|
||||
* The previous three steps are repeated until no typestates in the
|
||||
block change.
|
||||
|
||||
The typestate algorithm is a very conventional dataflow calculation, and can
|
||||
be performed using bit-set operations, with one bit per predicate and one
|
||||
bit-set per condition.
|
||||
|
||||
After the typestates of a block are computed, the typestate algorithm checks
|
||||
that every constraint in the precondition of a statement is satisfied by its
|
||||
prestate. If any preconditions are not satisfied, the mismatch is considered a
|
||||
static (compile-time) error.
|
||||
|
||||
|
||||
### Typestate checks
|
||||
|
||||
The key mechanism that connects run-time semantics and compile-time analysis
|
||||
of typestates is the use of [`check` expressions](#check-expressions). A
|
||||
`check` expression guarantees that *if* control were to proceed past it, the
|
||||
predicate associated with the `check` would have succeeded, so the constraint
|
||||
being checked *statically* holds in subsequent points.^[A `check` expression
|
||||
is similar to an `assert` call in a C program, with the significant difference
|
||||
that the Rust compiler *tracks* the constraint that each `check` expression
|
||||
enforces. Naturally, `check` expressions cannot be omitted from a "production
|
||||
build" of a Rust program the same way `asserts` are frequently disabled in
|
||||
deployed C programs.}
|
||||
|
||||
It is important to understand that the typestate system has *no insight* into
|
||||
the meaning of a particular predicate. Predicates and constraints are not
|
||||
evaluated in any way at compile time. Predicates are treated as specific (but
|
||||
unknown) functions applied to specific (also unknown) slots. All the typestate
|
||||
system does is track which of those predicates -- whatever they calculate --
|
||||
*must have been checked already* in order for program control to reach a
|
||||
particular point in the CFG. The fundamental building block, therefore, is the
|
||||
`check` statement, which tells the typestate system "if control passes this
|
||||
point, the checked predicate holds".
|
||||
|
||||
From this building block, constraints can be propagated to function signatures
|
||||
and constrained types, and the responsibility to `check` a constraint
|
||||
pushed further and further away from the site at which the program requires it
|
||||
to hold in order to execute properly.
|
||||
|
||||
|
||||
|
||||
# Memory and concurrency models
|
||||
|
||||
Rust has a memory model centered around concurrently-executing _tasks_. Thus
|
||||
|
||||
@ -763,7 +763,6 @@ fn rustc_sysroot() -> ~str {
|
||||
alt os::self_exe_path() {
|
||||
some(path) {
|
||||
let path = ~[path, ~"..", ~"bin", ~"rustc"];
|
||||
check vec::is_not_empty(path);
|
||||
let rustc = path::normalize(path::connect_many(path));
|
||||
#debug(" rustc: %s", rustc);
|
||||
rustc
|
||||
|
||||
@ -39,7 +39,7 @@ fn parse_config(args: ~[~str]) -> config {
|
||||
getopts::optflag(~"verbose"),
|
||||
getopts::optopt(~"logfile")];
|
||||
|
||||
check (vec::is_not_empty(args));
|
||||
assert (vec::is_not_empty(args));
|
||||
let args_ = vec::tail(args);
|
||||
let match =
|
||||
alt getopts::getopts(args_, opts) {
|
||||
|
||||
@ -121,7 +121,6 @@ fn run_pretty_test(config: config, props: test_props, testfile: ~str) {
|
||||
if option::is_some(props.pp_exact) {
|
||||
// Now we have to care about line endings
|
||||
let cr = ~"\r";
|
||||
check (str::is_not_empty(cr));
|
||||
actual = str::replace(actual, cr, ~"");
|
||||
expected = str::replace(expected, cr, ~"");
|
||||
}
|
||||
|
||||
@ -69,7 +69,6 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
|
||||
// position, the pretty-printer can't preserve this even by
|
||||
// parenthesizing!! See email to marijn.
|
||||
ast::expr_if(_, _, _) { false }
|
||||
ast::expr_if_check(_, _, _) { false }
|
||||
ast::expr_block(_) { false }
|
||||
ast::expr_alt(_, _, _) { false }
|
||||
ast::expr_while(_, _) { false }
|
||||
@ -87,10 +86,6 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
|
||||
// https://github.com/mozilla/rust/issues/953
|
||||
ast::expr_fail(option::some(_)) { false }
|
||||
|
||||
// https://github.com/mozilla/rust/issues/927
|
||||
//ast::expr_assert(_) { false }
|
||||
ast::expr_check(_, _) { false }
|
||||
|
||||
// https://github.com/mozilla/rust/issues/928
|
||||
//ast::expr_cast(_, _) { false }
|
||||
|
||||
@ -105,13 +100,8 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
|
||||
}
|
||||
|
||||
fn safe_to_steal_ty(t: @ast::ty, tm: test_mode) -> bool {
|
||||
alt t.node {
|
||||
// https://github.com/mozilla/rust/issues/971
|
||||
ast::ty_constr(_, _) { false }
|
||||
|
||||
// Other restrictions happen to be the same.
|
||||
_ { safe_to_replace_ty(t.node, tm) }
|
||||
}
|
||||
// Restrictions happen to be the same.
|
||||
safe_to_replace_ty(t.node, tm)
|
||||
}
|
||||
|
||||
// Not type-parameterized: https://github.com/mozilla/rust/issues/898 (FIXED)
|
||||
|
||||
@ -217,7 +217,7 @@ fn normalize(p: path) -> path {
|
||||
let s = strip_dots(s);
|
||||
let s = rollup_doubledots(s);
|
||||
|
||||
let s = if check vec::is_not_empty(s) {
|
||||
let s = if vec::is_not_empty(s) {
|
||||
connect_many(s)
|
||||
} else {
|
||||
~""
|
||||
|
||||
@ -289,9 +289,9 @@ fn map_opt<T,U:copy,V:copy>(
|
||||
* to accommodate an error like the vectors being of different lengths.
|
||||
*/
|
||||
fn map_vec2<S,T,U:copy,V:copy>(ss: ~[S], ts: ~[T],
|
||||
op: fn(S,T) -> result<V,U>)
|
||||
: vec::same_length(ss, ts) -> result<~[V],U> {
|
||||
op: fn(S,T) -> result<V,U>) -> result<~[V],U> {
|
||||
|
||||
assert vec::same_length(ss, ts);
|
||||
let n = vec::len(ts);
|
||||
let mut vs = ~[];
|
||||
vec::reserve(vs, n);
|
||||
@ -312,10 +312,9 @@ fn map_vec2<S,T,U:copy,V:copy>(ss: ~[S], ts: ~[T],
|
||||
* on its own as no result vector is built.
|
||||
*/
|
||||
fn iter_vec2<S,T,U:copy>(ss: ~[S], ts: ~[T],
|
||||
op: fn(S,T) -> result<(),U>)
|
||||
: vec::same_length(ss, ts)
|
||||
-> result<(),U> {
|
||||
op: fn(S,T) -> result<(),U>) -> result<(),U> {
|
||||
|
||||
assert vec::same_length(ss, ts);
|
||||
let n = vec::len(ts);
|
||||
let mut i = 0u;
|
||||
while i < n {
|
||||
|
||||
@ -284,9 +284,6 @@ type field = spanned<field_>;
|
||||
#[auto_serialize]
|
||||
enum blk_check_mode { default_blk, unchecked_blk, unsafe_blk, }
|
||||
|
||||
#[auto_serialize]
|
||||
enum expr_check_mode { claimed_expr, checked_expr, }
|
||||
|
||||
#[auto_serialize]
|
||||
type expr = {id: node_id, callee_id: node_id, node: expr_, span: span};
|
||||
// Extra node ID is only used for index, assign_op, unary, binary
|
||||
@ -322,10 +319,6 @@ enum expr_ {
|
||||
expr_do_body(@expr),
|
||||
expr_block(blk),
|
||||
|
||||
/*
|
||||
* FIXME (#34): many of these @exprs should be constrained with
|
||||
* is_lval once we have constrained types working.
|
||||
*/
|
||||
expr_copy(@expr),
|
||||
expr_move(@expr, @expr),
|
||||
expr_assign(@expr, @expr),
|
||||
@ -348,9 +341,6 @@ enum expr_ {
|
||||
/* just an assert, no significance to typestate */
|
||||
expr_assert(@expr),
|
||||
|
||||
/* preds that typestate is aware of */
|
||||
expr_check(expr_check_mode, @expr),
|
||||
expr_if_check(@expr, blk, option<@expr>),
|
||||
expr_mac(mac),
|
||||
}
|
||||
|
||||
@ -365,15 +355,6 @@ type capture_item = @{
|
||||
#[auto_serialize]
|
||||
type capture_clause = @~[capture_item];
|
||||
|
||||
/*
|
||||
// Says whether this is a block the user marked as
|
||||
// "unchecked"
|
||||
enum blk_sort {
|
||||
blk_unchecked, // declared as "exception to effect-checking rules"
|
||||
blk_checked, // all typing rules apply
|
||||
}
|
||||
*/
|
||||
|
||||
#[auto_serialize]
|
||||
#[doc="For macro invocations; parsing is delegated to the macro"]
|
||||
enum token_tree {
|
||||
@ -384,8 +365,6 @@ enum token_tree {
|
||||
tt_interpolate(span, ident)
|
||||
}
|
||||
|
||||
|
||||
|
||||
#[auto_serialize]
|
||||
type matcher = spanned<matcher_>;
|
||||
|
||||
@ -502,7 +481,6 @@ enum ty_ {
|
||||
ty_fn(proto, fn_decl),
|
||||
ty_tup(~[@ty]),
|
||||
ty_path(@path, node_id),
|
||||
ty_constr(@ty, ~[@ty_constr]),
|
||||
ty_fixed_length(@ty, option<uint>),
|
||||
ty_mac(mac),
|
||||
// ty_infer means the type should be inferred instead of it having been
|
||||
@ -511,59 +489,6 @@ enum ty_ {
|
||||
ty_infer,
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
A constraint arg that's a function argument is referred to by its position
|
||||
rather than name. This is so we could have higher-order functions that have
|
||||
constraints (potentially -- right now there's no way to write that), and also
|
||||
so that the typestate pass doesn't have to map a function name onto its decl.
|
||||
So, the constr_arg type is parameterized: it's instantiated with uint for
|
||||
declarations, and ident for uses.
|
||||
*/
|
||||
#[auto_serialize]
|
||||
enum constr_arg_general_<T> { carg_base, carg_ident(T), carg_lit(@lit), }
|
||||
|
||||
#[auto_serialize]
|
||||
type fn_constr_arg = constr_arg_general_<uint>;
|
||||
|
||||
#[auto_serialize]
|
||||
type sp_constr_arg<T> = spanned<constr_arg_general_<T>>;
|
||||
|
||||
#[auto_serialize]
|
||||
type ty_constr_arg = sp_constr_arg<@path>;
|
||||
|
||||
#[auto_serialize]
|
||||
type constr_arg = spanned<fn_constr_arg>;
|
||||
|
||||
// Constrained types' args are parameterized by paths, since
|
||||
// we refer to paths directly and not by indices.
|
||||
// The implicit root of such path, in the constraint-list for a
|
||||
// constrained type, is * (referring to the base record)
|
||||
|
||||
#[auto_serialize]
|
||||
type constr_general_<ARG, ID> =
|
||||
{path: @path, args: ~[@sp_constr_arg<ARG>], id: ID};
|
||||
|
||||
// In the front end, constraints have a node ID attached.
|
||||
// Typeck turns this to a def_id, using the output of resolve.
|
||||
#[auto_serialize]
|
||||
type constr_general<ARG> = spanned<constr_general_<ARG, node_id>>;
|
||||
|
||||
#[auto_serialize]
|
||||
type constr_ = constr_general_<uint, node_id>;
|
||||
|
||||
#[auto_serialize]
|
||||
type constr = spanned<constr_general_<uint, node_id>>;
|
||||
|
||||
#[auto_serialize]
|
||||
type ty_constr_ = constr_general_<@path, node_id>;
|
||||
|
||||
#[auto_serialize]
|
||||
type ty_constr = spanned<ty_constr_>;
|
||||
|
||||
/* The parser generates ast::constrs; resolve generates
|
||||
a mapping from each function to a list of ty::constr_defs,
|
||||
corresponding to these. */
|
||||
#[auto_serialize]
|
||||
type arg = {mode: mode, ty: @ty, ident: ident, id: node_id};
|
||||
|
||||
@ -572,8 +497,7 @@ type fn_decl =
|
||||
{inputs: ~[arg],
|
||||
output: @ty,
|
||||
purity: purity,
|
||||
cf: ret_style,
|
||||
constraints: ~[@constr]};
|
||||
cf: ret_style};
|
||||
|
||||
#[auto_serialize]
|
||||
enum purity {
|
||||
|
||||
@ -213,14 +213,6 @@ pure fn is_call_expr(e: @expr) -> bool {
|
||||
alt e.node { expr_call(_, _, _) { true } _ { false } }
|
||||
}
|
||||
|
||||
fn is_constraint_arg(e: @expr) -> bool {
|
||||
alt e.node {
|
||||
expr_lit(_) { ret true; }
|
||||
expr_path(_) { ret true; }
|
||||
_ { ret false; }
|
||||
}
|
||||
}
|
||||
|
||||
fn eq_ty(&&a: @ty, &&b: @ty) -> bool { ret box::ptr_eq(a, b); }
|
||||
|
||||
fn hash_ty(&&t: @ty) -> uint {
|
||||
@ -381,8 +373,8 @@ fn dtor_dec() -> fn_decl {
|
||||
let nil_t = @{id: 0, node: ty_nil, span: dummy_sp()};
|
||||
// dtor has one argument, of type ()
|
||||
{inputs: ~[{mode: ast::expl(ast::by_ref),
|
||||
ty: nil_t, ident: @~"_", id: 0}],
|
||||
output: nil_t, purity: impure_fn, cf: return_val, constraints: ~[]}
|
||||
ty: nil_t, ident: @~"_", id: 0}],
|
||||
output: nil_t, purity: impure_fn, cf: return_val}
|
||||
}
|
||||
|
||||
// ______________________________________________________________________
|
||||
@ -467,10 +459,6 @@ fn id_visitor(vfn: fn@(node_id)) -> visit::vt<()> {
|
||||
vec::iter(ps, |p| vfn(p.id))
|
||||
},
|
||||
|
||||
visit_constr: fn@(_p: @path, _sp: span, id: node_id) {
|
||||
vfn(id);
|
||||
},
|
||||
|
||||
visit_fn: fn@(fk: visit::fn_kind, d: ast::fn_decl,
|
||||
_b: ast::blk, _sp: span, id: ast::node_id) {
|
||||
vfn(id);
|
||||
|
||||
@ -162,8 +162,7 @@ impl helpers for ext_ctxt {
|
||||
node: ast::ty_fn(ast::proto_any, {inputs: args,
|
||||
output: output,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]}),
|
||||
cf: ast::return_val}),
|
||||
span: span}
|
||||
}
|
||||
|
||||
@ -466,10 +465,6 @@ fn ser_ty(cx: ext_ctxt, tps: ser_tps_map,
|
||||
}
|
||||
}
|
||||
|
||||
ast::ty_constr(ty, _) {
|
||||
ser_ty(cx, tps, ty, s, v)
|
||||
}
|
||||
|
||||
ast::ty_mac(_) {
|
||||
cx.span_err(ty.span, ~"cannot serialize macro types");
|
||||
~[]
|
||||
@ -573,8 +568,7 @@ fn mk_ser_fn(cx: ext_ctxt, span: span, name: ast::ident,
|
||||
node: ast::item_fn({inputs: ser_inputs,
|
||||
output: ser_output,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]},
|
||||
cf: ast::return_val},
|
||||
ser_tps,
|
||||
ser_blk),
|
||||
vis: ast::public,
|
||||
@ -697,10 +691,6 @@ fn deser_ty(cx: ext_ctxt, tps: deser_tps_map,
|
||||
}
|
||||
}
|
||||
|
||||
ast::ty_constr(ty, constrs) {
|
||||
deser_ty(cx, tps, ty, d)
|
||||
}
|
||||
|
||||
ast::ty_mac(_) {
|
||||
#ast{ fail }
|
||||
}
|
||||
@ -783,8 +773,7 @@ fn mk_deser_fn(cx: ext_ctxt, span: span,
|
||||
node: ast::item_fn({inputs: deser_inputs,
|
||||
output: v_ty,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]},
|
||||
cf: ast::return_val},
|
||||
deser_tps,
|
||||
deser_blk),
|
||||
vis: ast::public,
|
||||
|
||||
@ -89,10 +89,7 @@ impl ast_builder for ext_ctxt {
|
||||
{inputs: inputs,
|
||||
output: output,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
// FIXME #2886: we'll probably want a variant that does constrained
|
||||
// types.
|
||||
constraints: ~[]}
|
||||
cf: ast::return_val}
|
||||
}
|
||||
|
||||
fn item(name: ident,
|
||||
|
||||
@ -33,8 +33,6 @@ iface ast_fold {
|
||||
fn fold_decl(&&@decl) -> @decl;
|
||||
fn fold_expr(&&@expr) -> @expr;
|
||||
fn fold_ty(&&@ty) -> @ty;
|
||||
fn fold_constr(&&@constr) -> @constr;
|
||||
fn fold_ty_constr(&&@ty_constr) -> @ty_constr;
|
||||
fn fold_mod(_mod) -> _mod;
|
||||
fn fold_foreign_mod(foreign_mod) -> foreign_mod;
|
||||
fn fold_variant(variant) -> variant;
|
||||
@ -66,9 +64,6 @@ type ast_fold_precursor = @{
|
||||
fold_decl: fn@(decl_, span, ast_fold) -> (decl_, span),
|
||||
fold_expr: fn@(expr_, span, ast_fold) -> (expr_, span),
|
||||
fold_ty: fn@(ty_, span, ast_fold) -> (ty_, span),
|
||||
fold_constr: fn@(ast::constr_, span, ast_fold) -> (constr_, span),
|
||||
fold_ty_constr: fn@(ast::ty_constr_, span, ast_fold)
|
||||
-> (ty_constr_, span),
|
||||
fold_mod: fn@(_mod, ast_fold) -> _mod,
|
||||
fold_foreign_mod: fn@(foreign_mod, ast_fold) -> foreign_mod,
|
||||
fold_variant: fn@(variant_, span, ast_fold) -> (variant_, span),
|
||||
@ -135,8 +130,7 @@ fn fold_fn_decl(decl: ast::fn_decl, fld: ast_fold) -> ast::fn_decl {
|
||||
ret {inputs: vec::map(decl.inputs, |x| fold_arg_(x, fld) ),
|
||||
output: fld.fold_ty(decl.output),
|
||||
purity: decl.purity,
|
||||
cf: decl.cf,
|
||||
constraints: vec::map(decl.constraints, |x| fld.fold_constr(x))}
|
||||
cf: decl.cf}
|
||||
}
|
||||
|
||||
fn fold_ty_param_bound(tpb: ty_param_bound, fld: ast_fold) -> ty_param_bound {
|
||||
@ -200,10 +194,7 @@ fn noop_fold_foreign_item(&&ni: @foreign_item, fld: ast_fold)
|
||||
foreign_item_fn({inputs: vec::map(fdec.inputs, fold_arg),
|
||||
output: fld.fold_ty(fdec.output),
|
||||
purity: fdec.purity,
|
||||
cf: fdec.cf,
|
||||
constraints:
|
||||
vec::map(fdec.constraints,
|
||||
|x| fld.fold_constr(x))},
|
||||
cf: fdec.cf},
|
||||
fold_ty_params(typms, fld))
|
||||
}
|
||||
},
|
||||
@ -474,11 +465,6 @@ fn noop_fold_expr(e: expr_, fld: ast_fold) -> expr_ {
|
||||
expr_log(i, lv, e) { expr_log(i, fld.fold_expr(lv),
|
||||
fld.fold_expr(e)) }
|
||||
expr_assert(e) { expr_assert(fld.fold_expr(e)) }
|
||||
expr_check(m, e) { expr_check(m, fld.fold_expr(e)) }
|
||||
expr_if_check(cond, tr, fl) {
|
||||
expr_if_check(fld.fold_expr(cond), fld.fold_block(tr),
|
||||
option::map(fl, |x| fld.fold_expr(x)))
|
||||
}
|
||||
expr_mac(mac) { expr_mac(fold_mac(mac)) }
|
||||
}
|
||||
}
|
||||
@ -504,24 +490,11 @@ fn noop_fold_ty(t: ty_, fld: ast_fold) -> ty_ {
|
||||
ty_fn(proto, decl) {ty_fn(proto, fold_fn_decl(decl, fld))}
|
||||
ty_tup(tys) {ty_tup(vec::map(tys, |ty| fld.fold_ty(ty)))}
|
||||
ty_path(path, id) {ty_path(fld.fold_path(path), fld.new_id(id))}
|
||||
ty_constr(ty, constrs) {ty_constr(fld.fold_ty(ty),
|
||||
vec::map(constrs, |x| fld.fold_ty_constr(x)))}
|
||||
ty_fixed_length(t, vs) {ty_fixed_length(fld.fold_ty(t), vs)}
|
||||
ty_mac(mac) {ty_mac(fold_mac(mac))}
|
||||
}
|
||||
}
|
||||
|
||||
fn noop_fold_constr(c: constr_, fld: ast_fold) -> constr_ {
|
||||
{path: fld.fold_path(c.path), args: /* FIXME (#2543) */ copy c.args,
|
||||
id: fld.new_id(c.id)}
|
||||
}
|
||||
|
||||
fn noop_fold_ty_constr(c: ty_constr_, fld: ast_fold) -> ty_constr_ {
|
||||
let rslt: ty_constr_ =
|
||||
{path: fld.fold_path(c.path), args: /* FIXME (#2543) */ copy c.args,
|
||||
id: fld.new_id(c.id)};
|
||||
rslt
|
||||
}
|
||||
// ...nor do modules
|
||||
fn noop_fold_mod(m: _mod, fld: ast_fold) -> _mod {
|
||||
ret {view_items: vec::map(m.view_items, |x| fld.fold_view_item(x)),
|
||||
@ -606,8 +579,6 @@ fn default_ast_fold() -> ast_fold_precursor {
|
||||
fold_decl: wrap(noop_fold_decl),
|
||||
fold_expr: wrap(noop_fold_expr),
|
||||
fold_ty: wrap(noop_fold_ty),
|
||||
fold_constr: wrap(noop_fold_constr),
|
||||
fold_ty_constr: wrap(noop_fold_ty_constr),
|
||||
fold_mod: noop_fold_mod,
|
||||
fold_foreign_mod: noop_fold_foreign_mod,
|
||||
fold_variant: wrap(noop_fold_variant),
|
||||
@ -697,17 +668,6 @@ impl of ast_fold for ast_fold_precursor {
|
||||
let (n, s) = self.fold_ty(x.node, x.span, self as ast_fold);
|
||||
ret @{id: self.new_id(x.id), node: n, span: self.new_span(s)};
|
||||
}
|
||||
fn fold_constr(&&x: @ast::constr) ->
|
||||
@ast::constr {
|
||||
let (n, s) = self.fold_constr(x.node, x.span, self as ast_fold);
|
||||
ret @{node: n, span: self.new_span(s)};
|
||||
}
|
||||
fn fold_ty_constr(&&x: @ast::ty_constr) ->
|
||||
@ast::ty_constr {
|
||||
let (n, s) : (ty_constr_, span) =
|
||||
self.fold_ty_constr(x.node, x.span, self as ast_fold);
|
||||
ret @{node: n, span: self.new_span(s)};
|
||||
}
|
||||
fn fold_mod(x: _mod) -> _mod {
|
||||
ret self.fold_mod(x, self as ast_fold);
|
||||
}
|
||||
|
||||
@ -6,8 +6,7 @@ import ast_util::operator_prec;
|
||||
|
||||
fn expr_requires_semi_to_be_stmt(e: @ast::expr) -> bool {
|
||||
alt e.node {
|
||||
ast::expr_if(_, _, _) | ast::expr_if_check(_, _, _)
|
||||
| ast::expr_alt(_, _, _) | ast::expr_block(_)
|
||||
ast::expr_if(_, _, _) | ast::expr_alt(_, _, _) | ast::expr_block(_)
|
||||
| ast::expr_while(_, _) | ast::expr_loop(_)
|
||||
| ast::expr_call(_, _, true) {
|
||||
false
|
||||
@ -44,7 +43,6 @@ fn need_parens(expr: @ast::expr, outer_prec: uint) -> bool {
|
||||
ast::expr_assign_op(_, _, _) { true }
|
||||
ast::expr_ret(_) { true }
|
||||
ast::expr_assert(_) { true }
|
||||
ast::expr_check(_, _) { true }
|
||||
ast::expr_log(_, _, _) { true }
|
||||
_ { !parse::classify::expr_requires_semi_to_be_stmt(expr) }
|
||||
}
|
||||
@ -64,8 +62,9 @@ fn ends_in_lit_int(ex: @ast::expr) -> bool {
|
||||
ast::expr_move(_, sub) | ast::expr_copy(sub) |
|
||||
ast::expr_assign(_, sub) |
|
||||
ast::expr_assign_op(_, _, sub) | ast::expr_swap(_, sub) |
|
||||
ast::expr_log(_, _, sub) | ast::expr_assert(sub) |
|
||||
ast::expr_check(_, sub) { ends_in_lit_int(sub) }
|
||||
ast::expr_log(_, _, sub) | ast::expr_assert(sub) {
|
||||
ends_in_lit_int(sub)
|
||||
}
|
||||
ast::expr_fail(osub) | ast::expr_ret(osub) {
|
||||
alt osub {
|
||||
some(ex) { ends_in_lit_int(ex) }
|
||||
|
||||
@ -20,14 +20,14 @@ import ast::{_mod, add, alt_check, alt_exhaustive, arg, arm, attribute,
|
||||
by_mutbl_ref, by_ref, by_val, capture_clause, capture_item,
|
||||
carg_base, carg_ident, cdir_dir_mod, cdir_src_mod,
|
||||
cdir_view_item, checked_expr, claimed_expr, class_immutable,
|
||||
class_member, class_method, class_mutable, constr, constr_arg,
|
||||
constr_general, crate, crate_cfg, crate_directive, decl,
|
||||
class_member, class_method, class_mutable,
|
||||
crate, crate_cfg, crate_directive, decl,
|
||||
decl_item, decl_local, default_blk, deref, div, expl, expr,
|
||||
expr_, expr_addr_of, expr_alt, expr_again, expr_assert,
|
||||
expr_assign, expr_assign_op, expr_binary, expr_block, expr_break,
|
||||
expr_call, expr_cast, expr_check, expr_copy, expr_do_body,
|
||||
expr_call, expr_cast, expr_copy, expr_do_body,
|
||||
expr_fail, expr_field, expr_fn, expr_fn_block, expr_if,
|
||||
expr_if_check, expr_index, expr_lit, expr_log, expr_loop,
|
||||
expr_index, expr_lit, expr_log, expr_loop,
|
||||
expr_loop_body, expr_mac, expr_move, expr_new, expr_path,
|
||||
expr_rec, expr_ret, expr_swap, expr_tup, expr_unary, expr_vec,
|
||||
expr_vstore, expr_while, extern_fn, field, fn_decl, foreign_item,
|
||||
@ -265,15 +265,9 @@ class parser {
|
||||
{mode: mode, ty: p.parse_ty(false), ident: name,
|
||||
id: p.get_id()}
|
||||
};
|
||||
// FIXME (#34): constrs is empty because right now, higher-order
|
||||
// functions can't have constrained types. Not sure whether
|
||||
// that would be desirable anyway. See bug for the story on
|
||||
// constrained types.
|
||||
let constrs: ~[@constr] = ~[];
|
||||
let (ret_style, ret_ty) = self.parse_ret_ty();
|
||||
ret {inputs: inputs, output: ret_ty,
|
||||
purity: purity, cf: ret_style,
|
||||
constraints: constrs};
|
||||
purity: purity, cf: ret_style};
|
||||
}
|
||||
|
||||
fn parse_trait_methods() -> ~[trait_method] {
|
||||
@ -341,79 +335,6 @@ class parser {
|
||||
ret spanned(lo, ty.span.hi, {ident: id, mt: {ty: ty, mutbl: mutbl}});
|
||||
}
|
||||
|
||||
// if i is the jth ident in args, return j
|
||||
// otherwise, fail
|
||||
fn ident_index(args: ~[arg], i: ident) -> uint {
|
||||
let mut j = 0u;
|
||||
for args.each |a| { if a.ident == i { ret j; } j += 1u; }
|
||||
self.fatal(~"unbound variable `" + *i + ~"` in constraint arg");
|
||||
}
|
||||
|
||||
fn parse_type_constr_arg() -> @ty_constr_arg {
|
||||
let sp = self.span;
|
||||
let mut carg = carg_base;
|
||||
self.expect(token::BINOP(token::STAR));
|
||||
if self.token == token::DOT {
|
||||
// "*..." notation for record fields
|
||||
self.bump();
|
||||
let pth = self.parse_path_without_tps();
|
||||
carg = carg_ident(pth);
|
||||
}
|
||||
// No literals yet, I guess?
|
||||
ret @{node: carg, span: sp};
|
||||
}
|
||||
|
||||
fn parse_constr_arg(args: ~[arg]) -> @constr_arg {
|
||||
let sp = self.span;
|
||||
let mut carg = carg_base;
|
||||
if self.token == token::BINOP(token::STAR) {
|
||||
self.bump();
|
||||
} else {
|
||||
let i: ident = self.parse_value_ident();
|
||||
carg = carg_ident(self.ident_index(args, i));
|
||||
}
|
||||
ret @{node: carg, span: sp};
|
||||
}
|
||||
|
||||
fn parse_ty_constr(fn_args: ~[arg]) -> @constr {
|
||||
let lo = self.span.lo;
|
||||
let path = self.parse_path_without_tps();
|
||||
let args = self.parse_unspanned_seq(
|
||||
token::LPAREN, token::RPAREN,
|
||||
seq_sep_trailing_disallowed(token::COMMA),
|
||||
|p| p.parse_constr_arg(fn_args));
|
||||
ret @spanned(lo, self.span.hi,
|
||||
{path: path, args: args, id: self.get_id()});
|
||||
}
|
||||
|
||||
fn parse_constr_in_type() -> @ty_constr {
|
||||
let lo = self.span.lo;
|
||||
let path = self.parse_path_without_tps();
|
||||
let args: ~[@ty_constr_arg] = self.parse_unspanned_seq(
|
||||
token::LPAREN, token::RPAREN,
|
||||
seq_sep_trailing_disallowed(token::COMMA),
|
||||
|p| p.parse_type_constr_arg());
|
||||
let hi = self.span.lo;
|
||||
let tc: ty_constr_ = {path: path, args: args, id: self.get_id()};
|
||||
ret @spanned(lo, hi, tc);
|
||||
}
|
||||
|
||||
|
||||
fn parse_constrs<T: copy>(pser: fn(parser) -> @constr_general<T>) ->
|
||||
~[@constr_general<T>] {
|
||||
let mut constrs: ~[@constr_general<T>] = ~[];
|
||||
loop {
|
||||
let constr = pser(self);
|
||||
vec::push(constrs, constr);
|
||||
if self.token == token::COMMA { self.bump(); }
|
||||
else { ret constrs; }
|
||||
};
|
||||
}
|
||||
|
||||
fn parse_type_constraints() -> ~[@ty_constr] {
|
||||
ret self.parse_constrs(|p| p.parse_constr_in_type());
|
||||
}
|
||||
|
||||
fn parse_ret_ty() -> (ret_style, @ty) {
|
||||
ret if self.eat(token::RARROW) {
|
||||
let lo = self.span.lo;
|
||||
@ -519,16 +440,7 @@ class parser {
|
||||
if vec::len(elems) == 0u {
|
||||
self.unexpected_last(token::RBRACE);
|
||||
}
|
||||
let hi = self.span.hi;
|
||||
|
||||
let t = ty_rec(elems);
|
||||
if self.token == token::COLON {
|
||||
self.bump();
|
||||
ty_constr(@{id: self.get_id(),
|
||||
node: t,
|
||||
span: mk_sp(lo, hi)},
|
||||
self.parse_type_constraints())
|
||||
} else { t }
|
||||
ty_rec(elems)
|
||||
} else if self.token == token::LBRACKET {
|
||||
self.expect(token::LBRACKET);
|
||||
let t = ty_vec(self.parse_mt());
|
||||
@ -970,21 +882,6 @@ class parser {
|
||||
let e = self.parse_expr();
|
||||
ex = expr_assert(e);
|
||||
hi = e.span.hi;
|
||||
} else if self.eat_keyword(~"check") {
|
||||
/* Should be a predicate (pure boolean function) applied to
|
||||
arguments that are all either slot variables or literals.
|
||||
but the typechecker enforces that. */
|
||||
let e = self.parse_expr();
|
||||
hi = e.span.hi;
|
||||
ex = expr_check(checked_expr, e);
|
||||
} else if self.eat_keyword(~"claim") {
|
||||
/* Same rules as check, except that if check-claims
|
||||
is enabled (a command-line flag), then the parser turns
|
||||
claims into check */
|
||||
|
||||
let e = self.parse_expr();
|
||||
hi = e.span.hi;
|
||||
ex = expr_check(claimed_expr, e);
|
||||
} else if self.eat_keyword(~"ret") {
|
||||
if can_begin_expr(self.token) {
|
||||
let e = self.parse_expr();
|
||||
@ -1457,12 +1354,7 @@ class parser {
|
||||
ret lhs;
|
||||
}
|
||||
|
||||
fn parse_if_expr_1() ->
|
||||
{cond: @expr,
|
||||
then: blk,
|
||||
els: option<@expr>,
|
||||
lo: uint,
|
||||
hi: uint} {
|
||||
fn parse_if_expr() -> @expr {
|
||||
let lo = self.last_span.lo;
|
||||
let cond = self.parse_expr();
|
||||
let thn = self.parse_block();
|
||||
@ -1473,18 +1365,8 @@ class parser {
|
||||
els = some(elexpr);
|
||||
hi = elexpr.span.hi;
|
||||
}
|
||||
ret {cond: cond, then: thn, els: els, lo: lo, hi: hi};
|
||||
}
|
||||
|
||||
fn parse_if_expr() -> @expr {
|
||||
if self.eat_keyword(~"check") {
|
||||
let q = self.parse_if_expr_1();
|
||||
ret self.mk_expr(q.lo, q.hi,
|
||||
expr_if_check(q.cond, q.then, q.els));
|
||||
} else {
|
||||
let q = self.parse_if_expr_1();
|
||||
ret self.mk_expr(q.lo, q.hi, expr_if(q.cond, q.then, q.els));
|
||||
}
|
||||
let q = {cond: cond, then: thn, els: els, lo: lo, hi: hi};
|
||||
ret self.mk_expr(q.lo, q.hi, expr_if(q.cond, q.then, q.els));
|
||||
}
|
||||
|
||||
fn parse_fn_expr(proto: proto) -> @expr {
|
||||
@ -1520,8 +1402,7 @@ class parser {
|
||||
span: self.span
|
||||
},
|
||||
purity: impure_fn,
|
||||
cf: return_val,
|
||||
constraints: ~[]
|
||||
cf: return_val
|
||||
}
|
||||
},
|
||||
@~[])
|
||||
@ -2083,20 +1964,11 @@ class parser {
|
||||
let inputs = either::lefts(args_or_capture_items);
|
||||
let capture_clause = @either::rights(args_or_capture_items);
|
||||
|
||||
// Use the args list to translate each bound variable
|
||||
// mentioned in a constraint to an arg index.
|
||||
// Seems weird to do this in the parser, but I'm not sure how else to.
|
||||
let mut constrs = ~[];
|
||||
if self.token == token::COLON {
|
||||
self.bump();
|
||||
constrs = self.parse_constrs(|p| p.parse_ty_constr(inputs));
|
||||
}
|
||||
let (ret_style, ret_ty) = self.parse_ret_ty();
|
||||
ret ({inputs: inputs,
|
||||
output: ret_ty,
|
||||
purity: purity,
|
||||
cf: ret_style,
|
||||
constraints: constrs}, capture_clause);
|
||||
cf: ret_style}, capture_clause);
|
||||
}
|
||||
|
||||
fn parse_fn_block_decl() -> (fn_decl, capture_clause) {
|
||||
@ -2118,8 +1990,7 @@ class parser {
|
||||
ret ({inputs: either::lefts(inputs_captures),
|
||||
output: output,
|
||||
purity: impure_fn,
|
||||
cf: return_val,
|
||||
constraints: ~[]},
|
||||
cf: return_val},
|
||||
@either::rights(inputs_captures));
|
||||
}
|
||||
|
||||
|
||||
@ -306,7 +306,7 @@ fn restricted_keyword_table() -> hashmap<~str, ()> {
|
||||
let keys = ~[
|
||||
~"alt", ~"again", ~"assert",
|
||||
~"break",
|
||||
~"check", ~"claim", ~"class", ~"const", ~"copy",
|
||||
~"check", ~"class", ~"const", ~"copy",
|
||||
~"do", ~"drop",
|
||||
~"else", ~"enum", ~"export", ~"extern",
|
||||
~"fail", ~"false", ~"fn", ~"for",
|
||||
|
||||
@ -128,8 +128,7 @@ fn test_fun_to_str() {
|
||||
node: ast::ty_nil,
|
||||
span: ast_util::dummy_sp()},
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]
|
||||
cf: ast::return_val
|
||||
};
|
||||
assert fun_to_str(decl, "a", ~[]) == "fn a()";
|
||||
}
|
||||
@ -373,11 +372,6 @@ fn print_type_ex(s: ps, &&ty: @ast::ty, print_colons: bool) {
|
||||
print_ty_fn(s, some(proto), d, none, none);
|
||||
}
|
||||
ast::ty_path(path, _) { print_path(s, path, print_colons); }
|
||||
ast::ty_constr(t, cs) {
|
||||
print_type(s, t);
|
||||
space(s.s);
|
||||
word(s.s, constrs_str(cs, ty_constr_to_str));
|
||||
}
|
||||
ast::ty_fixed_length(t, v) {
|
||||
print_type(s, t);
|
||||
word(s.s, ~"/");
|
||||
@ -977,9 +971,6 @@ fn print_expr(s: ps, &&expr: @ast::expr) {
|
||||
ast::expr_if(test, blk, elseopt) {
|
||||
print_if(s, test, blk, elseopt, false);
|
||||
}
|
||||
ast::expr_if_check(test, blk, elseopt) {
|
||||
print_if(s, test, blk, elseopt, true);
|
||||
}
|
||||
ast::expr_while(test, blk) {
|
||||
head(s, ~"while");
|
||||
print_maybe_parens_discrim(s, test);
|
||||
@ -1131,15 +1122,6 @@ fn print_expr(s: ps, &&expr: @ast::expr) {
|
||||
}
|
||||
}
|
||||
}
|
||||
ast::expr_check(m, expr) {
|
||||
alt m {
|
||||
ast::claimed_expr { word_nbsp(s, ~"claim"); }
|
||||
ast::checked_expr { word_nbsp(s, ~"check"); }
|
||||
}
|
||||
popen(s);
|
||||
print_expr(s, expr);
|
||||
pclose(s);
|
||||
}
|
||||
ast::expr_assert(expr) {
|
||||
word_nbsp(s, ~"assert");
|
||||
print_expr(s, expr);
|
||||
@ -1166,7 +1148,7 @@ fn print_expr_parens_if_not_bot(s: ps, ex: @ast::expr) {
|
||||
ast::expr_assign_op(_, _, _) | ast::expr_swap(_, _) |
|
||||
ast::expr_log(_, _, _) | ast::expr_assert(_) |
|
||||
ast::expr_call(_, _, true) |
|
||||
ast::expr_check(_, _) | ast::expr_vstore(_, _) { true }
|
||||
ast::expr_vstore(_, _) { true }
|
||||
_ { false }
|
||||
};
|
||||
if parens { popen(s); }
|
||||
@ -1348,9 +1330,6 @@ fn print_fn_args_and_ret(s: ps, decl: ast::fn_decl,
|
||||
popen(s);
|
||||
print_fn_args(s, decl, cap_items);
|
||||
pclose(s);
|
||||
word(s.s, constrs_str(decl.constraints, |c| {
|
||||
ast_fn_constr_to_str(decl, c)
|
||||
}));
|
||||
|
||||
maybe_print_comment(s, decl.output.span.lo);
|
||||
if decl.output.node != ast::ty_nil {
|
||||
@ -1552,7 +1531,6 @@ fn print_ty_fn(s: ps, opt_proto: option<ast::proto>,
|
||||
else { print_type(s, decl.output); }
|
||||
end(s);
|
||||
}
|
||||
word(s.s, constrs_str(decl.constraints, ast_ty_fn_constr_to_str));
|
||||
end(s);
|
||||
}
|
||||
|
||||
@ -1736,67 +1714,6 @@ fn next_comment(s: ps) -> option<comments::cmnt> {
|
||||
}
|
||||
}
|
||||
|
||||
fn constr_args_to_str<T>(f: fn@(T) -> ~str,
|
||||
args: ~[@ast::sp_constr_arg<T>]) ->
|
||||
~str {
|
||||
let mut comma = false;
|
||||
let mut s = ~"(";
|
||||
for args.each |a| {
|
||||
if comma { s += ~", "; } else { comma = true; }
|
||||
s += constr_arg_to_str::<T>(f, a.node);
|
||||
}
|
||||
s += ~")";
|
||||
ret s;
|
||||
}
|
||||
|
||||
fn constr_arg_to_str<T>(f: fn@(T) -> ~str, c: ast::constr_arg_general_<T>) ->
|
||||
~str {
|
||||
alt c {
|
||||
ast::carg_base { ret ~"*"; }
|
||||
ast::carg_ident(i) { ret f(i); }
|
||||
ast::carg_lit(l) { ret lit_to_str(l); }
|
||||
}
|
||||
}
|
||||
|
||||
// needed b/c constr_args_to_str needs
|
||||
// something that takes an alias
|
||||
// (argh)
|
||||
fn uint_to_str(&&i: uint) -> ~str { ret uint::str(i); }
|
||||
|
||||
fn ast_ty_fn_constr_to_str(&&c: @ast::constr) -> ~str {
|
||||
ret path_to_str(c.node.path) +
|
||||
constr_args_to_str(uint_to_str, c.node.args);
|
||||
}
|
||||
|
||||
fn ast_fn_constr_to_str(decl: ast::fn_decl, &&c: @ast::constr) -> ~str {
|
||||
let arg_to_str = |a| fn_arg_idx_to_str(decl, a);
|
||||
ret path_to_str(c.node.path) +
|
||||
constr_args_to_str(arg_to_str, c.node.args);
|
||||
}
|
||||
|
||||
fn ty_constr_to_str(&&c: @ast::ty_constr) -> ~str {
|
||||
fn ty_constr_path_to_str(&&p: @ast::path) -> ~str {
|
||||
~"*." + path_to_str(p)
|
||||
}
|
||||
|
||||
ret path_to_str(c.node.path) +
|
||||
constr_args_to_str::<@ast::path>(ty_constr_path_to_str,
|
||||
c.node.args);
|
||||
}
|
||||
|
||||
fn constrs_str<T>(constrs: ~[T], elt: fn(T) -> ~str) -> ~str {
|
||||
let mut s = ~"", colon = true;
|
||||
for constrs.each |c| {
|
||||
if colon { s += ~" : "; colon = false; } else { s += ~", "; }
|
||||
s += elt(c);
|
||||
}
|
||||
ret s;
|
||||
}
|
||||
|
||||
fn fn_arg_idx_to_str(decl: ast::fn_decl, &&idx: uint) -> ~str {
|
||||
*decl.inputs[idx].ident
|
||||
}
|
||||
|
||||
fn opt_proto_to_str(opt_p: option<ast::proto>) -> ~str {
|
||||
alt opt_p {
|
||||
none { ~"fn" }
|
||||
|
||||
@ -44,8 +44,6 @@ fn tps_of_fn(fk: fn_kind) -> ~[ty_param] {
|
||||
}
|
||||
|
||||
type visitor<E> =
|
||||
// takes the components so that one function can be
|
||||
// generic over constr and ty_constr
|
||||
@{visit_mod: fn@(_mod, span, node_id, E, vt<E>),
|
||||
visit_view_item: fn@(@view_item, E, vt<E>),
|
||||
visit_foreign_item: fn@(@foreign_item, E, vt<E>),
|
||||
@ -59,7 +57,6 @@ type visitor<E> =
|
||||
visit_expr: fn@(@expr, E, vt<E>),
|
||||
visit_ty: fn@(@ty, E, vt<E>),
|
||||
visit_ty_params: fn@(~[ty_param], E, vt<E>),
|
||||
visit_constr: fn@(@path, span, node_id, E, vt<E>),
|
||||
visit_fn: fn@(fn_kind, fn_decl, blk, span, node_id, E, vt<E>),
|
||||
visit_ty_method: fn@(ty_method, E, vt<E>),
|
||||
visit_trait_method: fn@(trait_method, E, vt<E>),
|
||||
@ -79,7 +76,6 @@ fn default_visitor<E>() -> visitor<E> {
|
||||
visit_expr: |a,b,c|visit_expr::<E>(a, b, c),
|
||||
visit_ty: |a,b,c|skip_ty::<E>(a, b, c),
|
||||
visit_ty_params: |a,b,c|visit_ty_params::<E>(a, b, c),
|
||||
visit_constr: |a,b,c,d,e|visit_constr::<E>(a, b, c, d, e),
|
||||
visit_fn: |a,b,c,d,e,f,g|visit_fn::<E>(a, b, c, d, e, f, g),
|
||||
visit_ty_method: |a,b,c|visit_ty_method::<E>(a, b, c),
|
||||
visit_trait_method: |a,b,c|visit_trait_method::<E>(a, b, c),
|
||||
@ -194,21 +190,12 @@ fn visit_ty<E>(t: @ty, e: E, v: vt<E>) {
|
||||
ty_tup(ts) { for ts.each |tt| { v.visit_ty(tt, e, v); } }
|
||||
ty_fn(_, decl) {
|
||||
for decl.inputs.each |a| { v.visit_ty(a.ty, e, v); }
|
||||
for decl.constraints.each |c| {
|
||||
v.visit_constr(c.node.path, c.span, c.node.id, e, v);
|
||||
}
|
||||
v.visit_ty(decl.output, e, v);
|
||||
}
|
||||
ty_path(p, _) { visit_path(p, e, v); }
|
||||
ty_fixed_length(t, _) {
|
||||
v.visit_ty(t, e, v);
|
||||
}
|
||||
ty_constr(t, cs) {
|
||||
v.visit_ty(t, e, v);
|
||||
for cs.each |tc| {
|
||||
v.visit_constr(tc.node.path, tc.span, tc.node.id, e, v);
|
||||
}
|
||||
}
|
||||
ty_nil |
|
||||
ty_bot |
|
||||
ty_mac(_) |
|
||||
@ -217,11 +204,6 @@ fn visit_ty<E>(t: @ty, e: E, v: vt<E>) {
|
||||
}
|
||||
}
|
||||
|
||||
fn visit_constr<E>(_operator: @path, _sp: span, _id: node_id, _e: E,
|
||||
_v: vt<E>) {
|
||||
// default
|
||||
}
|
||||
|
||||
fn visit_path<E>(p: @path, e: E, v: vt<E>) {
|
||||
for p.types.each |tp| { v.visit_ty(tp, e, v); }
|
||||
}
|
||||
@ -272,9 +254,6 @@ fn visit_ty_params<E>(tps: ~[ty_param], e: E, v: vt<E>) {
|
||||
|
||||
fn visit_fn_decl<E>(fd: fn_decl, e: E, v: vt<E>) {
|
||||
for fd.inputs.each |a| { v.visit_ty(a.ty, e, v); }
|
||||
for fd.constraints.each |c| {
|
||||
v.visit_constr(c.node.path, c.span, c.node.id, e, v);
|
||||
}
|
||||
v.visit_ty(fd.output, e, v);
|
||||
}
|
||||
|
||||
@ -394,9 +373,7 @@ fn visit_expr<E>(ex: @expr, e: E, v: vt<E>) {
|
||||
expr_binary(_, a, b) { v.visit_expr(a, e, v); v.visit_expr(b, e, v); }
|
||||
expr_addr_of(_, x) | expr_unary(_, x) |
|
||||
expr_loop_body(x) | expr_do_body(x) |
|
||||
expr_check(_, x) | expr_assert(x) {
|
||||
v.visit_expr(x, e, v);
|
||||
}
|
||||
expr_assert(x) { v.visit_expr(x, e, v); }
|
||||
expr_lit(_) { }
|
||||
expr_cast(x, t) { v.visit_expr(x, e, v); v.visit_ty(t, e, v); }
|
||||
expr_if(x, b, eo) {
|
||||
@ -404,11 +381,6 @@ fn visit_expr<E>(ex: @expr, e: E, v: vt<E>) {
|
||||
v.visit_block(b, e, v);
|
||||
visit_expr_opt(eo, e, v);
|
||||
}
|
||||
expr_if_check(x, b, eo) {
|
||||
v.visit_expr(x, e, v);
|
||||
v.visit_block(b, e, v);
|
||||
visit_expr_opt(eo, e, v);
|
||||
}
|
||||
expr_while(x, b) { v.visit_expr(x, e, v); v.visit_block(b, e, v); }
|
||||
expr_loop(b) { v.visit_block(b, e, v); }
|
||||
expr_alt(x, arms, _) {
|
||||
@ -460,8 +432,6 @@ fn visit_arm<E>(a: arm, e: E, v: vt<E>) {
|
||||
// calls the given functions on the nodes.
|
||||
|
||||
type simple_visitor =
|
||||
// takes the components so that one function can be
|
||||
// generic over constr and ty_constr
|
||||
@{visit_mod: fn@(_mod, span, node_id),
|
||||
visit_view_item: fn@(@view_item),
|
||||
visit_foreign_item: fn@(@foreign_item),
|
||||
@ -475,7 +445,6 @@ type simple_visitor =
|
||||
visit_expr: fn@(@expr),
|
||||
visit_ty: fn@(@ty),
|
||||
visit_ty_params: fn@(~[ty_param]),
|
||||
visit_constr: fn@(@path, span, node_id),
|
||||
visit_fn: fn@(fn_kind, fn_decl, blk, span, node_id),
|
||||
visit_ty_method: fn@(ty_method),
|
||||
visit_trait_method: fn@(trait_method),
|
||||
@ -497,7 +466,6 @@ fn default_simple_visitor() -> simple_visitor {
|
||||
visit_expr: fn@(_e: @expr) { },
|
||||
visit_ty: simple_ignore_ty,
|
||||
visit_ty_params: fn@(_ps: ~[ty_param]) {},
|
||||
visit_constr: fn@(_p: @path, _sp: span, _id: node_id) { },
|
||||
visit_fn: fn@(_fk: fn_kind, _d: fn_decl, _b: blk, _sp: span,
|
||||
_id: node_id) { },
|
||||
visit_ty_method: fn@(_m: ty_method) { },
|
||||
@ -572,11 +540,6 @@ fn mk_simple_visitor(v: simple_visitor) -> vt<()> {
|
||||
f(ps);
|
||||
visit_ty_params(ps, e, v);
|
||||
}
|
||||
fn v_constr(f: fn@(@path, span, node_id), pt: @path, sp: span,
|
||||
id: node_id, &&e: (), v: vt<()>) {
|
||||
f(pt, sp, id);
|
||||
visit_constr(pt, sp, id, e, v);
|
||||
}
|
||||
fn v_fn(f: fn@(fn_kind, fn_decl, blk, span, node_id),
|
||||
fk: fn_kind, decl: fn_decl, body: blk, sp: span,
|
||||
id: node_id, &&e: (), v: vt<()>) {
|
||||
@ -610,8 +573,6 @@ fn mk_simple_visitor(v: simple_visitor) -> vt<()> {
|
||||
visit_ty: visit_ty,
|
||||
visit_ty_params: |a,b,c|
|
||||
v_ty_params(v.visit_ty_params, a, b, c),
|
||||
visit_constr: |a,b,c,d,e|
|
||||
v_constr(v.visit_constr, a, b, c, d, e),
|
||||
visit_fn: |a,b,c,d,e,f,g|
|
||||
v_fn(v.visit_fn, a, b, c, d, e, f, g),
|
||||
visit_ty_method: |a,b,c|
|
||||
|
||||
@ -97,7 +97,6 @@ fn get_rpaths_relative_to_output(os: session::os,
|
||||
output: path::path,
|
||||
libs: ~[path::path]) -> ~[~str] {
|
||||
vec::map(libs, |a| {
|
||||
check not_win32(os);
|
||||
get_rpath_relative_to_output(os, cwd, output, a)
|
||||
})
|
||||
}
|
||||
@ -105,7 +104,9 @@ fn get_rpaths_relative_to_output(os: session::os,
|
||||
fn get_rpath_relative_to_output(os: session::os,
|
||||
cwd: path::path,
|
||||
output: path::path,
|
||||
&&lib: path::path) : not_win32(os) -> ~str {
|
||||
&&lib: path::path) -> ~str {
|
||||
assert not_win32(os);
|
||||
|
||||
// Mac doesn't appear to support $ORIGIN
|
||||
let prefix = alt os {
|
||||
session::os_linux { ~"$ORIGIN" + path::path_sep() }
|
||||
@ -147,7 +148,7 @@ fn get_relative_to(abs1: path::path, abs2: path::path) -> path::path {
|
||||
// FIXME (#2880): use view here.
|
||||
vec::push_all(path, vec::slice(split2, start_idx, len2 - 1u));
|
||||
|
||||
if check vec::is_not_empty(path) {
|
||||
if vec::is_not_empty(path) {
|
||||
ret path::connect_many(path);
|
||||
} else {
|
||||
ret ~".";
|
||||
@ -314,18 +315,16 @@ mod test {
|
||||
#[test]
|
||||
#[cfg(target_os = "linux")]
|
||||
fn test_rpath_relative() {
|
||||
let o = session::os_linux;
|
||||
check not_win32(o);
|
||||
let res = get_rpath_relative_to_output(o,
|
||||
let o = session::os_linux;
|
||||
let res = get_rpath_relative_to_output(o,
|
||||
~"/usr", ~"bin/rustc", ~"lib/libstd.so");
|
||||
assert res == ~"$ORIGIN/../lib";
|
||||
assert res == ~"$ORIGIN/../lib";
|
||||
}
|
||||
|
||||
#[test]
|
||||
#[cfg(target_os = "freebsd")]
|
||||
fn test_rpath_relative() {
|
||||
let o = session::os_freebsd;
|
||||
check not_win32(o);
|
||||
let res = get_rpath_relative_to_output(o,
|
||||
~"/usr", ~"bin/rustc", ~"lib/libstd.so");
|
||||
assert res == ~"$ORIGIN/../lib";
|
||||
@ -336,7 +335,6 @@ mod test {
|
||||
fn test_rpath_relative() {
|
||||
// this is why refinements would be nice
|
||||
let o = session::os_macos;
|
||||
check not_win32(o);
|
||||
let res = get_rpath_relative_to_output(o, ~"/usr", ~"bin/rustc",
|
||||
~"lib/libstd.so");
|
||||
assert res == ~"@executable_path/../lib";
|
||||
|
||||
@ -207,9 +207,6 @@ fn compile_upto(sess: session, cfg: ast::crate_cfg,
|
||||
let last_use_map = time(time_passes, ~"liveness checking", ||
|
||||
middle::liveness::check_crate(ty_cx, method_map, crate));
|
||||
|
||||
time(time_passes, ~"typestate checking", ||
|
||||
middle::tstate::ck::check_crate(ty_cx, crate));
|
||||
|
||||
let (root_map, mutbl_map) = time(time_passes, ~"borrow checking", ||
|
||||
middle::borrowck::check_crate(ty_cx, method_map,
|
||||
last_use_map, crate));
|
||||
|
||||
@ -221,8 +221,7 @@ fn mk_tests(cx: test_ctxt) -> @ast::item {
|
||||
{inputs: ~[],
|
||||
output: ret_ty,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]};
|
||||
cf: ast::return_val};
|
||||
|
||||
// The vector of test_descs for this crate
|
||||
let test_descs = mk_test_desc_vec(cx);
|
||||
@ -382,8 +381,7 @@ fn mk_test_wrapper(cx: test_ctxt,
|
||||
inputs: ~[],
|
||||
output: @{id: cx.sess.next_node_id(), node: ast::ty_nil, span: span},
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]
|
||||
cf: ast::return_val
|
||||
};
|
||||
|
||||
let wrapper_body: ast::blk = nospan({
|
||||
@ -436,8 +434,7 @@ fn mk_main(cx: test_ctxt) -> @ast::item {
|
||||
{inputs: ~[args_arg],
|
||||
output: @ret_ty,
|
||||
purity: ast::impure_fn,
|
||||
cf: ast::return_val,
|
||||
constraints: ~[]};
|
||||
cf: ast::return_val};
|
||||
|
||||
let test_main_call_expr = mk_test_main_call(cx);
|
||||
|
||||
|
||||
@ -63,31 +63,6 @@ fn parse_ret_ty(st: @pstate, conv: conv_did) -> (ast::ret_style, ty::t) {
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_constrs_gen<T: copy>(st: @pstate, conv: conv_did,
|
||||
pser: fn(@pstate)
|
||||
-> ast::constr_arg_general_<T>) -> ~[@ty::constr_general<T>] {
|
||||
let mut rslt: ~[@ty::constr_general<T>] = ~[];
|
||||
alt peek(st) {
|
||||
':' {
|
||||
loop {
|
||||
next(st);
|
||||
vec::push(rslt, parse_constr(st, conv, pser));
|
||||
if peek(st) != ';' { break; }
|
||||
}
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
rslt
|
||||
}
|
||||
|
||||
fn parse_constrs(st: @pstate, conv: conv_did) -> ~[@ty::constr] {
|
||||
parse_constrs_gen(st, conv, parse_constr_arg)
|
||||
}
|
||||
|
||||
fn parse_ty_constrs(st: @pstate, conv: conv_did) -> ~[@ty::type_constr] {
|
||||
parse_constrs_gen(st, conv, parse_ty_constr_arg)
|
||||
}
|
||||
|
||||
fn parse_path(st: @pstate) -> @ast::path {
|
||||
let mut idents: ~[ast::ident] = ~[];
|
||||
fn is_last(c: char) -> bool { ret c == '(' || c == ':'; }
|
||||
@ -106,59 +81,6 @@ fn parse_path(st: @pstate) -> @ast::path {
|
||||
};
|
||||
}
|
||||
|
||||
fn parse_constr_arg(st: @pstate) -> ast::fn_constr_arg {
|
||||
alt peek(st) {
|
||||
'*' { st.pos += 1u; ret ast::carg_base; }
|
||||
c {
|
||||
|
||||
/* how will we disambiguate between
|
||||
an arg index and a lit argument? */
|
||||
if c >= '0' && c <= '9' {
|
||||
next(st);
|
||||
// FIXME #877
|
||||
ret ast::carg_ident((c as uint) - 48u);
|
||||
} else {
|
||||
#error("Lit args are unimplemented");
|
||||
fail; // FIXME #877
|
||||
}
|
||||
/*
|
||||
else {
|
||||
auto lit = parse_lit(st, conv, ',');
|
||||
vec::push(args, respan(st.span, ast::carg_lit(lit)));
|
||||
}
|
||||
*/
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_ty_constr_arg(st: @pstate) -> ast::constr_arg_general_<@path> {
|
||||
alt peek(st) {
|
||||
'*' { st.pos += 1u; ret ast::carg_base; }
|
||||
c { ret ast::carg_ident(parse_path(st)); }
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_constr<T: copy>(st: @pstate, conv: conv_did,
|
||||
pser: fn(@pstate) -> ast::constr_arg_general_<T>)
|
||||
-> @ty::constr_general<T> {
|
||||
// FIXME: use real spans and not a bogus one (#2407)
|
||||
let sp = ast_util::dummy_sp();
|
||||
let mut args: ~[@sp_constr_arg<T>] = ~[];
|
||||
let pth = parse_path(st);
|
||||
let mut ignore: char = next(st);
|
||||
assert (ignore == '(');
|
||||
let def = parse_def(st, conv);
|
||||
let mut an_arg: constr_arg_general_<T>;
|
||||
loop {
|
||||
an_arg = pser(st);
|
||||
vec::push(args, @respan(sp, an_arg));
|
||||
ignore = next(st);
|
||||
if ignore != ';' { break; }
|
||||
}
|
||||
assert (ignore == ')');
|
||||
ret @respan(sp, {path: pth, args: args, id: def});
|
||||
}
|
||||
|
||||
fn parse_ty_rust_fn(st: @pstate, conv: conv_did) -> ty::t {
|
||||
ret ty::mk_fn(st.tcx, parse_ty_fn(st, conv));
|
||||
}
|
||||
@ -363,13 +285,6 @@ fn parse_ty(st: @pstate, conv: conv_did) -> ty::t {
|
||||
}
|
||||
}
|
||||
}
|
||||
'A' {
|
||||
assert (next(st) == '[');
|
||||
let tt = parse_ty(st, conv);
|
||||
let tcs = parse_ty_constrs(st, conv);
|
||||
assert (next(st) == ']');
|
||||
ret ty::mk_constr(st.tcx, tt, tcs);
|
||||
}
|
||||
'"' {
|
||||
let def = parse_def(st, conv);
|
||||
let inner = parse_ty(st, conv);
|
||||
@ -457,10 +372,9 @@ fn parse_ty_fn(st: @pstate, conv: conv_did) -> ty::fn_ty {
|
||||
vec::push(inputs, {mode: ast::expl(mode), ty: parse_ty(st, conv)});
|
||||
}
|
||||
st.pos += 1u; // eat the ']'
|
||||
let cs = parse_constrs(st, conv);
|
||||
let (ret_style, ret_ty) = parse_ret_ty(st, conv);
|
||||
ret {purity: purity, proto: proto, inputs: inputs, output: ret_ty,
|
||||
ret_style: ret_style, constraints: cs};
|
||||
ret_style: ret_style};
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -285,12 +285,6 @@ fn enc_sty(w: io::writer, cx: @ctxt, st: ty::sty) {
|
||||
ty::ty_opaque_closure_ptr(ty::ck_block) { w.write_str(&"C&"); }
|
||||
ty::ty_opaque_closure_ptr(ty::ck_box) { w.write_str(&"C@"); }
|
||||
ty::ty_opaque_closure_ptr(ty::ck_uniq) { w.write_str(&"C~"); }
|
||||
ty::ty_constr(ty, cs) {
|
||||
w.write_str(&"A[");
|
||||
enc_ty(w, cx, ty);
|
||||
for cs.each |tc| { enc_ty_constr(w, cx, tc); }
|
||||
w.write_char(']');
|
||||
}
|
||||
ty::ty_opaque_box { w.write_char('B'); }
|
||||
ty::ty_class(def, substs) {
|
||||
#debug("~~~~ %s", ~"a[");
|
||||
@ -344,55 +338,12 @@ fn enc_ty_fn(w: io::writer, cx: @ctxt, ft: ty::fn_ty) {
|
||||
enc_ty(w, cx, arg.ty);
|
||||
}
|
||||
w.write_char(']');
|
||||
let mut colon = true;
|
||||
for ft.constraints.each |c| {
|
||||
if colon {
|
||||
w.write_char(':');
|
||||
colon = false;
|
||||
} else { w.write_char(';'); }
|
||||
enc_constr(w, cx, c);
|
||||
}
|
||||
alt ft.ret_style {
|
||||
noreturn { w.write_char('!'); }
|
||||
_ { enc_ty(w, cx, ft.output); }
|
||||
}
|
||||
}
|
||||
|
||||
fn enc_constr_gen<T>(w: io::writer, cx: @ctxt,
|
||||
c: @ty::constr_general<T>,
|
||||
write_arg: fn(@sp_constr_arg<T>)) {
|
||||
w.write_str(path_to_str(c.node.path));
|
||||
w.write_char('(');
|
||||
w.write_str(cx.ds(c.node.id));
|
||||
w.write_char('|');
|
||||
let mut semi = false;
|
||||
for c.node.args.each |a| {
|
||||
if semi { w.write_char(';'); } else { semi = true; }
|
||||
write_arg(a);
|
||||
}
|
||||
w.write_char(')');
|
||||
}
|
||||
|
||||
fn enc_constr(w: io::writer, cx: @ctxt, c: @ty::constr) {
|
||||
enc_constr_gen(w, cx, c, |a| {
|
||||
alt a.node {
|
||||
carg_base { w.write_char('*'); }
|
||||
carg_ident(i) { w.write_uint(i); }
|
||||
carg_lit(l) { w.write_str(lit_to_str(l)); }
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
fn enc_ty_constr(w: io::writer, cx: @ctxt, c: @ty::type_constr) {
|
||||
enc_constr_gen(w, cx, c, |a| {
|
||||
alt a.node {
|
||||
carg_base { w.write_char('*'); }
|
||||
carg_ident(p) { w.write_str(path_to_str(p)); }
|
||||
carg_lit(l) { w.write_str(lit_to_str(l)); }
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
fn enc_bounds(w: io::writer, cx: @ctxt, bs: @~[ty::param_bound]) {
|
||||
for vec::each(*bs) |bound| {
|
||||
alt bound {
|
||||
|
||||
@ -167,11 +167,11 @@ impl public_methods for borrowck_ctxt {
|
||||
ast::expr_addr_of(*) | ast::expr_call(*) |
|
||||
ast::expr_swap(*) | ast::expr_move(*) | ast::expr_assign(*) |
|
||||
ast::expr_assign_op(*) | ast::expr_fn(*) | ast::expr_fn_block(*) |
|
||||
ast::expr_assert(*) | ast::expr_check(*) | ast::expr_ret(*) |
|
||||
ast::expr_assert(*) | ast::expr_ret(*) |
|
||||
ast::expr_loop_body(*) | ast::expr_do_body(*) | ast::expr_unary(*) |
|
||||
ast::expr_copy(*) | ast::expr_cast(*) | ast::expr_fail(*) |
|
||||
ast::expr_vstore(*) | ast::expr_vec(*) | ast::expr_tup(*) |
|
||||
ast::expr_if_check(*) | ast::expr_if(*) | ast::expr_log(*) |
|
||||
ast::expr_if(*) | ast::expr_log(*) |
|
||||
ast::expr_new(*) | ast::expr_binary(*) | ast::expr_while(*) |
|
||||
ast::expr_block(*) | ast::expr_loop(*) | ast::expr_alt(*) |
|
||||
ast::expr_lit(*) | ast::expr_break | ast::expr_mac(*) |
|
||||
|
||||
@ -453,8 +453,7 @@ fn visit_expr(expr: @expr, &&self: @ir_maps, vt: vt<@ir_maps>) {
|
||||
}
|
||||
|
||||
// live nodes required for interesting control flow:
|
||||
expr_if_check(*) | expr_if(*) | expr_alt(*) |
|
||||
expr_while(*) | expr_loop(*) {
|
||||
expr_if(*) | expr_alt(*) | expr_while(*) | expr_loop(*) {
|
||||
(*self).add_live_node_for_node(expr.id, lnk_expr(expr.span));
|
||||
visit::visit_expr(expr, self, vt);
|
||||
}
|
||||
@ -467,7 +466,7 @@ fn visit_expr(expr: @expr, &&self: @ir_maps, vt: vt<@ir_maps>) {
|
||||
expr_index(*) | expr_field(*) | expr_vstore(*) |
|
||||
expr_vec(*) | expr_rec(*) | expr_call(*) | expr_tup(*) |
|
||||
expr_new(*) | expr_log(*) | expr_binary(*) |
|
||||
expr_assert(*) | expr_check(*) | expr_addr_of(*) | expr_copy(*) |
|
||||
expr_assert(*) | expr_addr_of(*) | expr_copy(*) |
|
||||
expr_loop_body(*) | expr_do_body(*) | expr_cast(*) |
|
||||
expr_unary(*) | expr_fail(*) |
|
||||
expr_break | expr_again | expr_lit(_) | expr_ret(*) |
|
||||
@ -936,7 +935,6 @@ class liveness {
|
||||
}
|
||||
}
|
||||
|
||||
expr_if_check(cond, then, els) |
|
||||
expr_if(cond, then, els) {
|
||||
//
|
||||
// (cond)
|
||||
@ -1098,7 +1096,6 @@ class liveness {
|
||||
}
|
||||
|
||||
expr_assert(e) |
|
||||
expr_check(_, e) |
|
||||
expr_addr_of(_, e) |
|
||||
expr_copy(e) |
|
||||
expr_loop_body(e) |
|
||||
@ -1449,12 +1446,12 @@ fn check_expr(expr: @expr, &&self: @liveness, vt: vt<@liveness>) {
|
||||
}
|
||||
|
||||
// no correctness conditions related to liveness
|
||||
expr_if_check(*) | expr_if(*) | expr_alt(*) |
|
||||
expr_if(*) | expr_alt(*) |
|
||||
expr_while(*) | expr_loop(*) |
|
||||
expr_index(*) | expr_field(*) | expr_vstore(*) |
|
||||
expr_vec(*) | expr_rec(*) | expr_tup(*) |
|
||||
expr_new(*) | expr_log(*) | expr_binary(*) |
|
||||
expr_assert(*) | expr_check(*) | expr_copy(*) |
|
||||
expr_assert(*) | expr_copy(*) |
|
||||
expr_loop_body(*) | expr_do_body(*) |
|
||||
expr_cast(*) | expr_unary(*) | expr_fail(*) |
|
||||
expr_ret(*) | expr_break | expr_again | expr_lit(_) |
|
||||
|
||||
@ -428,7 +428,6 @@ fn resolve_names(e: @env, c: @ast::crate) {
|
||||
visit_expr: |a,b,c| walk_expr(e, a, b ,c),
|
||||
visit_ty: |a,b,c| walk_ty(e, a, b, c),
|
||||
visit_ty_params: |a,b,c| walk_tps(e, a, b, c),
|
||||
visit_constr: |a,b,c,d,f| walk_constr(e, a, b, c, d, f),
|
||||
visit_fn: |a,b,c,d,f,g,h| {
|
||||
visit_fn_with_scope(e, a, b, c, d, f, g, h)
|
||||
}
|
||||
@ -662,7 +661,6 @@ fn visit_fn_with_scope(e: @env, fk: visit::fn_kind, decl: ast::fn_decl,
|
||||
|
||||
// here's where we need to set up the mapping
|
||||
// for f's constrs in the table.
|
||||
for decl.constraints.each |c| { resolve_constr(e, c, sc, v); }
|
||||
let scope = alt fk {
|
||||
visit::fk_item_fn(_, tps) | visit::fk_method(_, tps, _)
|
||||
| visit::fk_ctor(_, tps, _, _) | visit::fk_dtor(tps, _, _) {
|
||||
@ -767,19 +765,6 @@ fn follow_import(e: env, &&sc: scopes, path: ~[ident], sp: span) ->
|
||||
} else { ret none; }
|
||||
}
|
||||
|
||||
fn resolve_constr(e: @env, c: @ast::constr, &&sc: scopes, _v: vt<scopes>) {
|
||||
alt lookup_path_strict(*e, sc, c.span, c.node.path, ns_val) {
|
||||
some(d@ast::def_fn(_,ast::pure_fn)) {
|
||||
e.def_map.insert(c.node.id, d);
|
||||
}
|
||||
_ {
|
||||
let s = path_to_str(c.node.path);
|
||||
e.sess.span_err(c.span, #fmt("%s is not declared pure. Try \
|
||||
`pure fn %s` instead of `fn %s`.", s, s, s));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Import resolution
|
||||
fn resolve_import(e: env, n_id: node_id, name: ast::ident,
|
||||
ids: ~[ast::ident], sp: codemap::span, &&sc: scopes) {
|
||||
|
||||
@ -20,7 +20,7 @@ import syntax::ast::{item_ty, local, local_crate, method, node_id, pat};
|
||||
import syntax::ast::{pat_enum, pat_ident, path, prim_ty, stmt_decl, ty,
|
||||
pat_box, pat_uniq, pat_lit, pat_range, pat_rec,
|
||||
pat_tup, pat_wild};
|
||||
import syntax::ast::{ty_bool, ty_char, ty_constr, ty_f, ty_f32, ty_f64};
|
||||
import syntax::ast::{ty_bool, ty_char, ty_f, ty_f32, ty_f64};
|
||||
import syntax::ast::{ty_float, ty_i, ty_i16, ty_i32, ty_i64, ty_i8, ty_int};
|
||||
import syntax::ast::{ty_param, ty_path, ty_str, ty_u, ty_u16, ty_u32, ty_u64};
|
||||
import syntax::ast::{ty_u8, ty_uint, variant, view_item, view_item_export};
|
||||
@ -3163,21 +3163,6 @@ class Resolver {
|
||||
}
|
||||
|
||||
self.resolve_type(declaration.output, visitor);
|
||||
|
||||
// Resolve constraints.
|
||||
for declaration.constraints.each |constraint| {
|
||||
alt self.resolve_path(constraint.node.path, ValueNS,
|
||||
false, visitor) {
|
||||
none {
|
||||
self.session.span_err(constraint.span,
|
||||
#fmt("unresolved name: %s",
|
||||
*constraint.node.path.idents.last()));
|
||||
}
|
||||
some(def) {
|
||||
self.record_def(constraint.node.id, def);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -3560,25 +3545,6 @@ class Resolver {
|
||||
}
|
||||
}
|
||||
|
||||
ty_constr(base_type, constraints) {
|
||||
self.resolve_type(base_type, visitor);
|
||||
|
||||
for constraints.each |constraint| {
|
||||
alt self.resolve_path(constraint.node.path, ValueNS,
|
||||
false, visitor) {
|
||||
none {
|
||||
self.session.span_err(constraint.span,
|
||||
~"(resolving function) \
|
||||
use of undeclared \
|
||||
constraint");
|
||||
}
|
||||
some(def) {
|
||||
self.record_def(constraint.node.id, def);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
_ {
|
||||
// Just resolve embedded types.
|
||||
visit_ty(ty, (), visitor);
|
||||
|
||||
@ -2002,19 +2002,23 @@ fn trans_external_path(ccx: @crate_ctxt, did: ast::def_id, t: ty::t)
|
||||
fn normalize_for_monomorphization(tcx: ty::ctxt, ty: ty::t) -> option<ty::t> {
|
||||
// FIXME[mono] could do this recursively. is that worthwhile? (#2529)
|
||||
alt ty::get(ty).struct {
|
||||
ty::ty_box(mt) { some(ty::mk_opaque_box(tcx)) }
|
||||
ty::ty_fn(fty) { some(ty::mk_fn(tcx, {purity: ast::impure_fn,
|
||||
proto: fty.proto,
|
||||
inputs: ~[],
|
||||
output: ty::mk_nil(tcx),
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]})) }
|
||||
ty::ty_trait(_, _) { some(ty::mk_fn(tcx, {purity: ast::impure_fn,
|
||||
proto: ast::proto_box,
|
||||
inputs: ~[],
|
||||
output: ty::mk_nil(tcx),
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]})) }
|
||||
ty::ty_box(mt) {
|
||||
some(ty::mk_opaque_box(tcx))
|
||||
}
|
||||
ty::ty_fn(fty) {
|
||||
some(ty::mk_fn(tcx, {purity: ast::impure_fn,
|
||||
proto: fty.proto,
|
||||
inputs: ~[],
|
||||
output: ty::mk_nil(tcx),
|
||||
ret_style: ast::return_val}))
|
||||
}
|
||||
ty::ty_trait(_, _) {
|
||||
some(ty::mk_fn(tcx, {purity: ast::impure_fn,
|
||||
proto: ast::proto_box,
|
||||
inputs: ~[],
|
||||
output: ty::mk_nil(tcx),
|
||||
ret_style: ast::return_val}))
|
||||
}
|
||||
ty::ty_ptr(_) { some(ty::mk_uint(tcx)) }
|
||||
_ { none }
|
||||
}
|
||||
@ -3525,7 +3529,7 @@ fn trans_expr(bcx: block, e: @ast::expr, dest: dest) -> block {
|
||||
fn unrooted(bcx: block, e: @ast::expr, dest: dest) -> block {
|
||||
let tcx = bcx.tcx();
|
||||
alt e.node {
|
||||
ast::expr_if(cond, thn, els) | ast::expr_if_check(cond, thn, els) {
|
||||
ast::expr_if(cond, thn, els) {
|
||||
ret trans_if(bcx, cond, thn, els, dest);
|
||||
}
|
||||
ast::expr_alt(expr, arms, mode) {
|
||||
@ -3631,23 +3635,6 @@ fn trans_expr(bcx: block, e: @ast::expr, dest: dest) -> block {
|
||||
assert dest == ignore;
|
||||
ret trans_check_expr(bcx, e, a, ~"Assertion");
|
||||
}
|
||||
ast::expr_check(ast::checked_expr, a) {
|
||||
assert dest == ignore;
|
||||
ret trans_check_expr(bcx, e, a, ~"Predicate");
|
||||
}
|
||||
ast::expr_check(ast::claimed_expr, a) {
|
||||
assert dest == ignore;
|
||||
/* Claims are turned on and off by a global variable
|
||||
that the RTS sets. This case generates code to
|
||||
check the value of that variable, doing nothing
|
||||
if it's set to false and acting like a check
|
||||
otherwise. */
|
||||
let c = get_extern_const(bcx.ccx().externs, bcx.ccx().llmod,
|
||||
~"check_claims", T_bool());
|
||||
ret do with_cond(bcx, Load(bcx, c)) |bcx| {
|
||||
trans_check_expr(bcx, e, a, ~"Claim")
|
||||
};
|
||||
}
|
||||
ast::expr_while(cond, body) {
|
||||
assert dest == ignore;
|
||||
ret trans_while(bcx, cond, body);
|
||||
|
||||
@ -976,8 +976,7 @@ fn trans_intrinsic(ccx: @crate_ctxt, decl: ValueRef, item: @ast::foreign_item,
|
||||
ty::mk_mach_uint(bcx.tcx(), ast::ty_u8))
|
||||
}],
|
||||
output: ty::mk_nil(bcx.tcx()),
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]
|
||||
ret_style: ast::return_val
|
||||
});
|
||||
bcx = trans_call_inner(bcx, none, fty, ty::mk_nil(bcx.tcx()),
|
||||
|bcx| lval_no_env(
|
||||
|
||||
@ -276,7 +276,6 @@ impl methods for reflector {
|
||||
ty::ty_self { self.leaf(~"self") }
|
||||
ty::ty_type { self.leaf(~"type") }
|
||||
ty::ty_opaque_box { self.leaf(~"opaque_box") }
|
||||
ty::ty_constr(t, _) { self.visit(~"constr", ~[self.c_tydesc(t)]) }
|
||||
ty::ty_opaque_closure_ptr(ck) {
|
||||
let ckval = alt ck {
|
||||
ty::ck_block { 0u }
|
||||
|
||||
@ -357,7 +357,6 @@ fn shape_of(ccx: @crate_ctxt, t: ty::t) -> ~[u8] {
|
||||
ty::ty_fn({proto: ast::proto_any, _}) { ~[shape_stack_fn] }
|
||||
ty::ty_fn({proto: ast::proto_bare, _}) { ~[shape_bare_fn] }
|
||||
ty::ty_opaque_closure_ptr(_) { ~[shape_opaque_closure_ptr] }
|
||||
ty::ty_constr(inner_t, _) { shape_of(ccx, inner_t) }
|
||||
ty::ty_var(_) | ty::ty_var_integral(_) | ty::ty_self {
|
||||
ccx.sess.bug(~"shape_of: unexpected type struct found");
|
||||
}
|
||||
|
||||
@ -148,7 +148,6 @@ fn type_of(cx: @crate_ctxt, t: ty::t) -> TypeRef {
|
||||
T_struct(tys)
|
||||
}
|
||||
ty::ty_opaque_closure_ptr(_) { T_opaque_box_ptr(cx) }
|
||||
ty::ty_constr(subt,_) { type_of(cx, subt) }
|
||||
ty::ty_class(*) {
|
||||
// Only create the named struct, but don't fill it in. We fill it
|
||||
// in *after* placing it into the type cache. This prevents
|
||||
|
||||
@ -243,8 +243,8 @@ fn mark_for_expr(cx: ctx, e: @expr) {
|
||||
}
|
||||
expr_alt(_, _, _) | expr_block(_) | expr_if(_, _, _) |
|
||||
expr_while(_, _) | expr_fail(_) | expr_break | expr_again |
|
||||
expr_unary(_, _) | expr_lit(_) | expr_assert(_) | expr_check(_, _) |
|
||||
expr_if_check(_, _, _) | expr_mac(_) | expr_addr_of(_, _) |
|
||||
expr_unary(_, _) | expr_lit(_) | expr_assert(_) |
|
||||
expr_mac(_) | expr_addr_of(_, _) |
|
||||
expr_ret(_) | expr_loop(_) |
|
||||
expr_loop_body(_) | expr_do_body(_) {}
|
||||
}
|
||||
|
||||
@ -1,186 +0,0 @@
|
||||
import syntax::ast::*;
|
||||
import syntax::visit;
|
||||
import option::*;
|
||||
import aux::*;
|
||||
import tstate::ann::{pre_and_post, precond, postcond, prestate, poststate,
|
||||
relax_prestate, relax_precond, relax_poststate,
|
||||
pps_len, true_precond,
|
||||
difference, union, clone,
|
||||
set_in_postcond, set_in_poststate, set_in_poststate_,
|
||||
clear_in_poststate, clear_in_prestate,
|
||||
clear_in_poststate_};
|
||||
import tritv::*;
|
||||
import driver::session::session;
|
||||
import std::map::hashmap;
|
||||
|
||||
fn bit_num(fcx: fn_ctxt, c: tsconstr) -> uint {
|
||||
let d = c.def_id;
|
||||
assert (fcx.enclosing.constrs.contains_key(d));
|
||||
let rslt = fcx.enclosing.constrs.get(d);
|
||||
match_args(fcx, rslt.descs, c.args)
|
||||
}
|
||||
|
||||
fn promises(fcx: fn_ctxt, p: poststate, c: tsconstr) -> bool {
|
||||
ret promises_(bit_num(fcx, c), p);
|
||||
}
|
||||
|
||||
fn promises_(n: uint, p: poststate) -> bool {
|
||||
ret tritv_get(p, n) == ttrue;
|
||||
}
|
||||
|
||||
// v "happens after" u
|
||||
fn seq_trit(u: trit, v: trit) -> trit {
|
||||
alt v { ttrue { ttrue } tfalse { tfalse } dont_care { u } }
|
||||
}
|
||||
|
||||
// idea: q "happens after" p -- so if something is
|
||||
// 1 in q and 0 in p, it's 1 in the result; however,
|
||||
// if it's 0 in q and 1 in p, it's 0 in the result
|
||||
fn seq_tritv(p: postcond, q: postcond) {
|
||||
let mut i = 0u;
|
||||
assert (p.nbits == q.nbits);
|
||||
while i < p.nbits {
|
||||
tritv_set(i, p, seq_trit(tritv_get(p, i), tritv_get(q, i)));
|
||||
i += 1u;
|
||||
}
|
||||
}
|
||||
|
||||
fn seq_postconds(fcx: fn_ctxt, ps: ~[postcond]) -> postcond {
|
||||
let sz = vec::len(ps);
|
||||
if sz >= 1u {
|
||||
let prev = tritv_clone(ps[0]);
|
||||
vec::iter_between(ps, 1u, sz, |p| seq_tritv(prev, p) );
|
||||
ret prev;
|
||||
} else { ret ann::empty_poststate(num_constraints(fcx.enclosing)); }
|
||||
}
|
||||
|
||||
// Given a list of pres and posts for exprs e0 ... en,
|
||||
// return the precondition for evaluating each expr in order.
|
||||
// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
|
||||
// precondition shouldn't include x.
|
||||
fn seq_preconds(fcx: fn_ctxt, pps: ~[pre_and_post]) -> precond {
|
||||
let sz: uint = vec::len(pps);
|
||||
let num_vars: uint = num_constraints(fcx.enclosing);
|
||||
|
||||
fn seq_preconds_go(fcx: fn_ctxt, pps: ~[pre_and_post],
|
||||
idx: uint, first: pre_and_post)
|
||||
-> precond {
|
||||
let mut idx = idx;
|
||||
let mut first = first;
|
||||
loop {
|
||||
let sz: uint = vec::len(pps) - idx;
|
||||
if sz >= 1u {
|
||||
let second = pps[0];
|
||||
assert (pps_len(second) == num_constraints(fcx.enclosing));
|
||||
let second_pre = clone(second.precondition);
|
||||
difference(second_pre, first.postcondition);
|
||||
let next_first = clone(first.precondition);
|
||||
union(next_first, second_pre);
|
||||
let next_first_post = clone(first.postcondition);
|
||||
seq_tritv(next_first_post, second.postcondition);
|
||||
idx += 1u;
|
||||
first = {precondition: next_first,
|
||||
postcondition: next_first_post};
|
||||
} else { ret first.precondition; }
|
||||
}
|
||||
}
|
||||
|
||||
if sz >= 1u {
|
||||
let first = pps[0];
|
||||
assert (pps_len(first) == num_vars);
|
||||
ret seq_preconds_go(fcx, pps, 1u, first);
|
||||
} else { ret true_precond(num_vars); }
|
||||
}
|
||||
|
||||
fn intersect_states(p: prestate, q: prestate) -> prestate {
|
||||
let rslt = tritv_clone(p);
|
||||
tritv_intersect(rslt, q);
|
||||
ret rslt;
|
||||
}
|
||||
|
||||
fn gen(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
||||
ret set_in_postcond(bit_num(fcx, c),
|
||||
node_id_to_ts_ann(fcx.ccx, id).conditions);
|
||||
}
|
||||
|
||||
fn declare_var(fcx: fn_ctxt, c: tsconstr, pre: prestate) -> prestate {
|
||||
let rslt = clone(pre);
|
||||
relax_prestate(bit_num(fcx, c), rslt);
|
||||
// idea is this is scoped
|
||||
relax_poststate(bit_num(fcx, c), rslt);
|
||||
ret rslt;
|
||||
}
|
||||
|
||||
fn relax_precond_expr(e: @expr, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
|
||||
relax_precond(cx.i as uint, expr_precond(cx.fcx.ccx, e));
|
||||
visit::visit_expr(e, cx, vt);
|
||||
}
|
||||
|
||||
fn relax_precond_stmt(s: @stmt, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
|
||||
relax_precond(cx.i as uint, stmt_precond(cx.fcx.ccx, *s));
|
||||
visit::visit_stmt(s, cx, vt);
|
||||
}
|
||||
|
||||
type relax_ctxt = {fcx: fn_ctxt, i: node_id};
|
||||
|
||||
fn relax_precond_block_inner(b: blk, cx: relax_ctxt,
|
||||
vt: visit::vt<relax_ctxt>) {
|
||||
relax_precond(cx.i as uint, block_precond(cx.fcx.ccx, b));
|
||||
visit::visit_block(b, cx, vt);
|
||||
}
|
||||
|
||||
fn relax_precond_block(fcx: fn_ctxt, i: node_id, b: blk) {
|
||||
let cx = {fcx: fcx, i: i};
|
||||
let visitor = visit::default_visitor::<relax_ctxt>();
|
||||
let visitor =
|
||||
@{visit_block: relax_precond_block_inner,
|
||||
visit_expr: relax_precond_expr,
|
||||
visit_stmt: relax_precond_stmt,
|
||||
visit_item:
|
||||
fn@(_i: @item, _cx: relax_ctxt, _vt: visit::vt<relax_ctxt>) { },
|
||||
visit_fn: do_nothing
|
||||
with *visitor};
|
||||
let v1 = visit::mk_vt(visitor);
|
||||
v1.visit_block(b, cx, v1);
|
||||
}
|
||||
|
||||
fn gen_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
||||
#debug("gen_poststate");
|
||||
ret set_in_poststate(bit_num(fcx, c),
|
||||
node_id_to_ts_ann(fcx.ccx, id).states);
|
||||
}
|
||||
|
||||
fn kill_prestate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
||||
ret clear_in_prestate(bit_num(fcx, c),
|
||||
node_id_to_ts_ann(fcx.ccx, id).states);
|
||||
}
|
||||
|
||||
fn kill_all_prestate(fcx: fn_ctxt, id: node_id) {
|
||||
tritv::tritv_kill(node_id_to_ts_ann(fcx.ccx, id).states.prestate);
|
||||
}
|
||||
|
||||
|
||||
fn kill_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
|
||||
#debug("kill_poststate");
|
||||
ret clear_in_poststate(bit_num(fcx, c),
|
||||
node_id_to_ts_ann(fcx.ccx, id).states);
|
||||
}
|
||||
|
||||
fn kill_poststate_(fcx: fn_ctxt, c: tsconstr, post: poststate) -> bool {
|
||||
#debug("kill_poststate_");
|
||||
ret clear_in_poststate_(bit_num(fcx, c), post);
|
||||
}
|
||||
|
||||
fn set_in_prestate_constr(fcx: fn_ctxt, c: tsconstr, t: prestate) -> bool {
|
||||
ret set_in_poststate_(bit_num(fcx, c), t);
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -15,7 +15,7 @@ import middle::lint::{get_warning_level, vecs_not_implicitly_copyable,
|
||||
ignore};
|
||||
import syntax::ast::*;
|
||||
import syntax::print::pprust::*;
|
||||
import util::ppaux::{ty_to_str, tys_to_str, ty_constr_to_str};
|
||||
import util::ppaux::{ty_to_str, tys_to_str};
|
||||
|
||||
export tv_vid, tvi_vid, region_vid, vid;
|
||||
export br_hashmap;
|
||||
@ -24,12 +24,8 @@ export node_id_to_type;
|
||||
export node_id_to_type_params;
|
||||
export arg;
|
||||
export args_eq;
|
||||
export ast_constr_to_constr;
|
||||
export block_ty;
|
||||
export class_items_as_fields, class_items_as_mutable_fields;
|
||||
export constr;
|
||||
export constr_general;
|
||||
export constr_table;
|
||||
export ctxt;
|
||||
export deref, deref_sty;
|
||||
export index, index_sty;
|
||||
@ -76,10 +72,8 @@ export ty_param_bounds_and_ty;
|
||||
export ty_bool, mk_bool, type_is_bool;
|
||||
export ty_bot, mk_bot, type_is_bot;
|
||||
export ty_box, mk_box, mk_imm_box, type_is_box, type_is_boxed;
|
||||
export ty_constr, mk_constr;
|
||||
export ty_opaque_closure_ptr, mk_opaque_closure_ptr;
|
||||
export ty_opaque_box, mk_opaque_box;
|
||||
export ty_constr_arg;
|
||||
export ty_float, mk_float, mk_mach_float, type_is_fp;
|
||||
export ty_fn, fn_ty, mk_fn;
|
||||
export ty_fn_proto, ty_fn_ret, ty_fn_ret_style, tys_in_fn_ty;
|
||||
@ -113,7 +107,6 @@ export tbox_has_flag;
|
||||
export ty_var_id;
|
||||
export ty_to_def_id;
|
||||
export ty_fn_args;
|
||||
export type_constr;
|
||||
export kind, kind_implicitly_copyable, kind_sendable, kind_copyable;
|
||||
export kind_noncopyable, kind_const;
|
||||
export kind_can_be_copied, kind_can_be_sent, kind_can_be_implicitly_copied;
|
||||
@ -168,7 +161,7 @@ export terr_no_integral_type, terr_ty_param_size, terr_self_substs;
|
||||
export terr_in_field, terr_record_fields, terr_vstores_differ, terr_arg_count;
|
||||
export terr_sorts, terr_vec, terr_str, terr_record_size, terr_tuple_size;
|
||||
export terr_regions_differ, terr_mutability, terr_purity_mismatch;
|
||||
export terr_constr_mismatch, terr_constr_len, terr_proto_mismatch;
|
||||
export terr_proto_mismatch;
|
||||
export terr_ret_style_mismatch;
|
||||
|
||||
// Data types
|
||||
@ -187,8 +180,6 @@ type method = {ident: ast::ident,
|
||||
purity: ast::purity,
|
||||
vis: ast::visibility};
|
||||
|
||||
type constr_table = hashmap<ast::node_id, ~[constr]>;
|
||||
|
||||
type mt = {ty: t, mutbl: ast::mutability};
|
||||
|
||||
enum vstore {
|
||||
@ -316,8 +307,7 @@ type fn_ty = {purity: ast::purity,
|
||||
proto: ast::proto,
|
||||
inputs: ~[arg],
|
||||
output: t,
|
||||
ret_style: ret_style,
|
||||
constraints: ~[@constr]};
|
||||
ret_style: ret_style};
|
||||
|
||||
// See discussion at head of region.rs
|
||||
enum region {
|
||||
@ -379,7 +369,6 @@ enum sty {
|
||||
// integral types only
|
||||
ty_param(uint, def_id), // type parameter
|
||||
ty_self, // special, implicit `self` type parameter
|
||||
ty_constr(t, ~[@type_constr]),
|
||||
|
||||
// "Fake" types, used for trans purposes
|
||||
ty_type, // type_desc*
|
||||
@ -388,12 +377,6 @@ enum sty {
|
||||
ty_unboxed_vec(mt),
|
||||
}
|
||||
|
||||
// In the middle end, constraints have a def_id attached, referring
|
||||
// to the definition of the operator in the constraint.
|
||||
type constr_general<ARG> = spanned<constr_general_<ARG, def_id>>;
|
||||
type type_constr = constr_general<@path>;
|
||||
type constr = constr_general<uint>;
|
||||
|
||||
enum terr_vstore_kind {
|
||||
terr_vec, terr_str
|
||||
}
|
||||
@ -416,8 +399,6 @@ enum type_err {
|
||||
terr_record_fields(ast::ident, ast::ident),
|
||||
terr_arg_count,
|
||||
terr_mode_mismatch(mode, mode),
|
||||
terr_constr_len(uint, uint),
|
||||
terr_constr_mismatch(@type_constr, @type_constr),
|
||||
terr_regions_differ(region, region),
|
||||
terr_vstores_differ(terr_vstore_kind, vstore, vstore),
|
||||
terr_in_field(@type_err, ast::ident),
|
||||
@ -607,9 +588,6 @@ fn mk_t_with_id(cx: ctxt, st: sty, o_def_id: option<ast::def_id>) -> t {
|
||||
for f.inputs.each |a| { flags |= get(a.ty).flags; }
|
||||
flags |= get(f.output).flags;
|
||||
}
|
||||
ty_constr(tt, _) {
|
||||
flags |= get(tt).flags;
|
||||
}
|
||||
}
|
||||
let t = @{struct: st, id: cx.next_id, flags: flags, o_def_id: o_def_id};
|
||||
cx.interner.insert(key, t);
|
||||
@ -700,10 +678,6 @@ fn mk_mut_unboxed_vec(cx: ctxt, ty: t) -> t {
|
||||
|
||||
fn mk_rec(cx: ctxt, fs: ~[field]) -> t { mk_t(cx, ty_rec(fs)) }
|
||||
|
||||
fn mk_constr(cx: ctxt, t: t, cs: ~[@type_constr]) -> t {
|
||||
mk_t(cx, ty_constr(t, cs))
|
||||
}
|
||||
|
||||
fn mk_tup(cx: ctxt, ts: ~[t]) -> t { mk_t(cx, ty_tup(ts)) }
|
||||
|
||||
fn mk_fn(cx: ctxt, fty: fn_ty) -> t { mk_t(cx, ty_fn(fty)) }
|
||||
@ -790,7 +764,6 @@ fn maybe_walk_ty(ty: t, f: fn(t) -> bool) {
|
||||
for ft.inputs.each |a| { maybe_walk_ty(a.ty, f); }
|
||||
maybe_walk_ty(ft.output, f);
|
||||
}
|
||||
ty_constr(sub, _) { maybe_walk_ty(sub, f); }
|
||||
ty_uniq(tm) { maybe_walk_ty(tm.ty, f); }
|
||||
}
|
||||
}
|
||||
@ -851,9 +824,6 @@ fn fold_sty(sty: sty, fldop: fn(t) -> t) -> sty {
|
||||
ty_rptr(r, tm) {
|
||||
ty_rptr(r, {ty: fldop(tm.ty), mutbl: tm.mutbl})
|
||||
}
|
||||
ty_constr(subty, cs) {
|
||||
ty_constr(fldop(subty), cs)
|
||||
}
|
||||
ty_class(did, substs) {
|
||||
ty_class(did, fold_substs(substs, fldop))
|
||||
}
|
||||
@ -1589,7 +1559,6 @@ fn type_kind(cx: ctxt, ty: t) -> kind {
|
||||
ty_param(_, did) {
|
||||
param_bounds_to_kind(cx.ty_param_bounds.get(did.node))
|
||||
}
|
||||
ty_constr(t, _) { type_kind(cx, t) }
|
||||
// FIXME (#2663): is self ever const?
|
||||
ty_self { kind_noncopyable() }
|
||||
ty_var(_) | ty_var_integral(_) {
|
||||
@ -1651,11 +1620,6 @@ fn is_instantiable(cx: ctxt, r_ty: t) -> bool {
|
||||
ty_unboxed_vec(_) {
|
||||
false
|
||||
}
|
||||
|
||||
ty_constr(t, _) {
|
||||
type_requires(cx, seen, r_ty, t)
|
||||
}
|
||||
|
||||
ty_box(mt) |
|
||||
ty_uniq(mt) |
|
||||
ty_rptr(_, mt) {
|
||||
@ -1836,7 +1800,6 @@ fn type_is_pod(cx: ctxt, ty: t) -> bool {
|
||||
ty_evec(mt, vstore_fixed(_)) | ty_unboxed_vec(mt) {
|
||||
result = type_is_pod(cx, mt.ty);
|
||||
}
|
||||
ty_constr(subt, _) { result = type_is_pod(cx, subt); }
|
||||
ty_param(_, _) { result = false; }
|
||||
ty_opaque_closure_ptr(_) { result = true; }
|
||||
ty_class(did, substs) {
|
||||
@ -1967,18 +1930,6 @@ fn hash_type_structure(st: sty) -> uint {
|
||||
for subtys.each |s| { h = (h << 2u) + type_id(s) }
|
||||
h
|
||||
}
|
||||
fn hash_type_constr(id: uint, c: @type_constr) -> uint {
|
||||
let mut h = id;
|
||||
h = (h << 2u) + hash_def(h, c.node.id);
|
||||
for c.node.args.each |a| {
|
||||
alt a.node {
|
||||
carg_base { h += h << 2u; }
|
||||
carg_lit(_) { fail ~"lit args not implemented yet"; }
|
||||
carg_ident(p) { h += h << 2u; }
|
||||
}
|
||||
}
|
||||
h
|
||||
}
|
||||
fn hash_region(r: region) -> uint {
|
||||
alt r { // no idea if this is any good
|
||||
re_bound(br) { (hash_bound_region(br)) << 2u | 0u }
|
||||
@ -2036,11 +1987,6 @@ fn hash_type_structure(st: sty) -> uint {
|
||||
ty_type { 32u }
|
||||
ty_bot { 34u }
|
||||
ty_ptr(mt) { hash_subty(35u, mt.ty) }
|
||||
ty_constr(t, cs) {
|
||||
let mut h = hash_subty(36u, t);
|
||||
for cs.each |c| { h = (h << 2u) + hash_type_constr(h, c); }
|
||||
h
|
||||
}
|
||||
ty_uniq(mt) { hash_subty(37u, mt.ty) }
|
||||
ty_trait(did, substs) {
|
||||
let mut h = hash_def(40u, did);
|
||||
@ -2061,49 +2007,6 @@ fn hash_type_structure(st: sty) -> uint {
|
||||
}
|
||||
}
|
||||
|
||||
fn arg_eq<T>(eq: fn(T, T) -> bool,
|
||||
a: @sp_constr_arg<T>,
|
||||
b: @sp_constr_arg<T>)
|
||||
-> bool {
|
||||
alt a.node {
|
||||
ast::carg_base {
|
||||
alt b.node { ast::carg_base { ret true; } _ { ret false; } }
|
||||
}
|
||||
ast::carg_ident(s) {
|
||||
alt b.node { ast::carg_ident(t) { ret eq(s, t); } _ { ret false; } }
|
||||
}
|
||||
ast::carg_lit(l) {
|
||||
alt b.node {
|
||||
ast::carg_lit(m) { ret const_eval::lit_eq(l, m); } _ { ret false; }
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn args_eq<T>(eq: fn(T, T) -> bool,
|
||||
a: ~[@sp_constr_arg<T>],
|
||||
b: ~[@sp_constr_arg<T>]) -> bool {
|
||||
let mut i: uint = 0u;
|
||||
for a.each |arg| {
|
||||
if !arg_eq(eq, arg, b[i]) { ret false; }
|
||||
i += 1u;
|
||||
}
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn constr_eq(c: @constr, d: @constr) -> bool {
|
||||
fn eq_int(&&x: uint, &&y: uint) -> bool { ret x == y; }
|
||||
ret path_to_str(c.node.path) == path_to_str(d.node.path) &&
|
||||
args_eq(eq_int, c.node.args, d.node.args);
|
||||
}
|
||||
|
||||
fn constrs_eq(cs: ~[@constr], ds: ~[@constr]) -> bool {
|
||||
if vec::len(cs) != vec::len(ds) { ret false; }
|
||||
let mut i = 0u;
|
||||
for cs.each |c| { if !constr_eq(c, ds[i]) { ret false; } i += 1u; }
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn node_id_to_type(cx: ctxt, id: ast::node_id) -> t {
|
||||
alt smallintmap::find(*cx.node_types, id as uint) {
|
||||
some(t) { t }
|
||||
@ -2385,7 +2288,6 @@ fn ty_sort_str(cx: ctxt, t: t) -> ~str {
|
||||
ty_var_integral(_) { ~"integral variable" }
|
||||
ty_param(_, _) { ~"type parameter" }
|
||||
ty_self { ~"self" }
|
||||
ty_constr(t, _) { ty_sort_str(cx, t) }
|
||||
}
|
||||
}
|
||||
|
||||
@ -2443,16 +2345,6 @@ fn type_err_to_str(cx: ctxt, err: type_err) -> ~str {
|
||||
ret ~"expected argument mode " + mode_to_str(e_mode) +
|
||||
~" but found " + mode_to_str(a_mode);
|
||||
}
|
||||
terr_constr_len(e_len, a_len) {
|
||||
ret ~"expected a type with " + uint::str(e_len) +
|
||||
~" constraints, but found one with " + uint::str(a_len) +
|
||||
~" constraints";
|
||||
}
|
||||
terr_constr_mismatch(e_constr, a_constr) {
|
||||
ret ~"expected a type with constraint " + ty_constr_to_str(e_constr) +
|
||||
~" but found one with constraint " +
|
||||
ty_constr_to_str(a_constr);
|
||||
}
|
||||
terr_regions_differ(subregion, superregion) {
|
||||
ret #fmt("references with lifetime %s do not necessarily \
|
||||
outlive references with lifetime %s",
|
||||
@ -2784,22 +2676,6 @@ pure fn is_public(f: field_ty) -> bool {
|
||||
}
|
||||
}
|
||||
|
||||
// Look up the list of method names and IDs for a given class
|
||||
// Fails if the id is not bound to a class.
|
||||
fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
|
||||
: is_local(did) -> ~[{name: ident, id: node_id, vis: visibility}] {
|
||||
alt cx.items.find(did.node) {
|
||||
some(ast_map::node_item(@{node: item_class(_,_,items,_,_), _}, _)) {
|
||||
let (_,ms) = split_class_items(items);
|
||||
vec::map(ms, |m| {name: m.ident, id: m.id,
|
||||
vis: m.vis})
|
||||
}
|
||||
_ {
|
||||
cx.sess.bug(~"lookup_class_method_ids: id not bound to a class");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* Given a class def_id and a method name, return the method's
|
||||
def_id. Needed so we can do static dispatch for methods
|
||||
Doesn't care about the method's privacy. (It's assumed that
|
||||
@ -2807,7 +2683,26 @@ fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
|
||||
*/
|
||||
fn lookup_class_method_by_name(cx:ctxt, did: ast::def_id, name: ident,
|
||||
sp: span) -> def_id {
|
||||
if check is_local(did) {
|
||||
|
||||
// Look up the list of method names and IDs for a given class
|
||||
// Fails if the id is not bound to a class.
|
||||
fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
|
||||
-> ~[{name: ident, id: node_id, vis: visibility}] {
|
||||
|
||||
assert is_local(did);
|
||||
alt cx.items.find(did.node) {
|
||||
some(ast_map::node_item(@{node: item_class(_,_,items,_,_), _}, _)) {
|
||||
let (_,ms) = split_class_items(items);
|
||||
vec::map(ms, |m| {name: m.ident, id: m.id,
|
||||
vis: m.vis})
|
||||
}
|
||||
_ {
|
||||
cx.sess.bug(~"lookup_class_method_ids: id not bound to a class");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if is_local(did) {
|
||||
let ms = lookup_class_method_ids(cx, did);
|
||||
for ms.each |m| {
|
||||
if m.name == name {
|
||||
@ -2939,24 +2834,6 @@ fn is_binopable(_cx: ctxt, ty: t, op: ast::binop) -> bool {
|
||||
ret tbl[tycat(ty)][opcat(op)];
|
||||
}
|
||||
|
||||
fn ast_constr_to_constr<T>(tcx: ctxt, c: @ast::constr_general<T>) ->
|
||||
@constr_general<T> {
|
||||
alt tcx.def_map.find(c.node.id) {
|
||||
some(ast::def_fn(pred_id, ast::pure_fn)) {
|
||||
ret @ast_util::respan(c.span,
|
||||
{path: c.node.path,
|
||||
args: c.node.args,
|
||||
id: pred_id});
|
||||
}
|
||||
_ {
|
||||
tcx.sess.span_fatal(c.span,
|
||||
~"predicate " + path_to_str(c.node.path) +
|
||||
~" is unbound or bound to a non-function or an \
|
||||
impure function");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn ty_params_to_tys(tcx: ty::ctxt, tps: ~[ast::ty_param]) -> ~[t] {
|
||||
vec::from_fn(tps.len(), |i| {
|
||||
ty::mk_param(tcx, i, ast_util::local_def(tps[i].id))
|
||||
|
||||
@ -240,7 +240,7 @@ fn check_main_fn_ty(ccx: @crate_ctxt,
|
||||
let main_t = ty::node_id_to_type(tcx, main_id);
|
||||
alt ty::get(main_t).struct {
|
||||
ty::ty_fn({purity: ast::impure_fn, proto: ast::proto_bare,
|
||||
inputs, output, ret_style: ast::return_val, constraints}) {
|
||||
inputs, output, ret_style: ast::return_val}) {
|
||||
alt tcx.items.find(main_id) {
|
||||
some(ast_map::node_item(it,_)) {
|
||||
alt it.node {
|
||||
@ -254,8 +254,7 @@ fn check_main_fn_ty(ccx: @crate_ctxt,
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
let mut ok = vec::len(constraints) == 0u;
|
||||
ok &= ty::type_is_nil(output);
|
||||
let mut ok = ty::type_is_nil(output);
|
||||
let num_args = vec::len(inputs);
|
||||
ok &= num_args == 0u || num_args == 1u &&
|
||||
arg_is_argv_ty(tcx, inputs[0]);
|
||||
|
||||
@ -332,13 +332,6 @@ fn ast_ty_to_ty<AC: ast_conv, RS: region_scope copy>(
|
||||
ast_ty.span,
|
||||
~"implied fixed length for bound");
|
||||
}
|
||||
ast::ty_constr(t, cs) {
|
||||
let mut out_cs = ~[];
|
||||
for cs.each |constr| {
|
||||
vec::push(out_cs, ty::ast_constr_to_constr(tcx, constr));
|
||||
}
|
||||
ty::mk_constr(tcx, ast_ty_to_ty(self, rscope, t), out_cs)
|
||||
}
|
||||
ast::ty_infer {
|
||||
// ty_infer should only appear as the type of arguments or return
|
||||
// values in a fn_expr, or as the type of local variables. Both of
|
||||
@ -429,12 +422,8 @@ fn ty_of_fn_decl<AC: ast_conv, RS: region_scope copy>(
|
||||
_ {ast_ty_to_ty(self, rb, decl.output)}
|
||||
};
|
||||
|
||||
let out_constrs = vec::map(decl.constraints, |constr| {
|
||||
ty::ast_constr_to_constr(self.tcx(), constr)
|
||||
});
|
||||
|
||||
{purity: decl.purity, proto: proto, inputs: input_tys,
|
||||
output: output_ty, ret_style: decl.cf, constraints: out_constrs}
|
||||
output: output_ty, ret_style: decl.cf}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -225,7 +225,6 @@ fn check_fn(ccx: @crate_ctxt,
|
||||
};
|
||||
|
||||
gather_locals(fcx, decl, body, arg_tys);
|
||||
check_constraints(fcx, decl.constraints, decl.inputs);
|
||||
check_block(fcx, body);
|
||||
|
||||
// We unify the tail expr's type with the
|
||||
@ -1342,15 +1341,6 @@ fn check_expr_with_unifier(fcx: @fn_ctxt,
|
||||
check_expr(fcx, e, none);
|
||||
fcx.write_nil(id);
|
||||
}
|
||||
ast::expr_check(_, e) {
|
||||
bot = check_pred_expr(fcx, e);
|
||||
fcx.write_nil(id);
|
||||
}
|
||||
ast::expr_if_check(cond, thn, elsopt) {
|
||||
bot =
|
||||
check_pred_expr(fcx, cond) |
|
||||
check_then_else(fcx, thn, elsopt, id, expr.span);
|
||||
}
|
||||
ast::expr_assert(e) {
|
||||
bot = check_expr_with(fcx, e, ty::mk_bool(tcx));
|
||||
fcx.write_nil(id);
|
||||
@ -1643,8 +1633,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt,
|
||||
proto: ast::proto_any,
|
||||
inputs: ~[{mode: m, ty: ty_nilp}],
|
||||
output: ty_nilp,
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]})
|
||||
ret_style: ast::return_val})
|
||||
};
|
||||
|
||||
demand::suptype(fcx, expr.span,
|
||||
@ -1893,119 +1882,6 @@ fn check_enum_variants(ccx: @crate_ctxt,
|
||||
check_instantiable(ccx.tcx, sp, id);
|
||||
}
|
||||
|
||||
// A generic function for checking the pred in a check
|
||||
// or if-check
|
||||
fn check_pred_expr(fcx: @fn_ctxt, e: @ast::expr) -> bool {
|
||||
let bot = check_expr_with(fcx, e, ty::mk_bool(fcx.ccx.tcx));
|
||||
|
||||
/* e must be a call expr where all arguments are either
|
||||
literals or slots */
|
||||
alt e.node {
|
||||
ast::expr_call(operator, operands, _) {
|
||||
if !ty::is_pred_ty(fcx.expr_ty(operator)) {
|
||||
fcx.ccx.tcx.sess.span_err
|
||||
(operator.span,
|
||||
~"operator in constraint has non-boolean return type");
|
||||
}
|
||||
|
||||
alt operator.node {
|
||||
ast::expr_path(oper_name) {
|
||||
alt fcx.ccx.tcx.def_map.find(operator.id) {
|
||||
some(ast::def_fn(_, ast::pure_fn)) {
|
||||
// do nothing
|
||||
}
|
||||
_ {
|
||||
fcx.ccx.tcx.sess.span_err(operator.span,
|
||||
~"impure function as operator \
|
||||
in constraint");
|
||||
}
|
||||
}
|
||||
for operands.each |operand| {
|
||||
if !ast_util::is_constraint_arg(operand) {
|
||||
let s =
|
||||
~"constraint args must be slot variables or literals";
|
||||
fcx.ccx.tcx.sess.span_err(e.span, s);
|
||||
}
|
||||
}
|
||||
}
|
||||
_ {
|
||||
let s = ~"in a constraint, expected the \
|
||||
constraint name to be an explicit name";
|
||||
fcx.ccx.tcx.sess.span_err(e.span, s);
|
||||
}
|
||||
}
|
||||
}
|
||||
_ { fcx.ccx.tcx.sess.span_err(e.span, ~"check on non-predicate"); }
|
||||
}
|
||||
ret bot;
|
||||
}
|
||||
|
||||
fn check_constraints(fcx: @fn_ctxt, cs: ~[@ast::constr],
|
||||
args: ~[ast::arg]) {
|
||||
let num_args = vec::len(args);
|
||||
for cs.each |c| {
|
||||
let mut c_args = ~[];
|
||||
for c.node.args.each |a| {
|
||||
vec::push(c_args,
|
||||
// "base" should not occur in a fn type thing, as of
|
||||
// yet, b/c we don't allow constraints on the return type
|
||||
|
||||
// Works b/c no higher-order polymorphism
|
||||
/*
|
||||
This is kludgy, and we probably shouldn't be assigning
|
||||
node IDs here, but we're creating exprs that are
|
||||
ephemeral, just for the purposes of typechecking. So
|
||||
that's my justification.
|
||||
*/
|
||||
@alt a.node {
|
||||
ast::carg_base {
|
||||
fcx.ccx.tcx.sess.span_bug(a.span,
|
||||
~"check_constraints:\
|
||||
unexpected carg_base");
|
||||
}
|
||||
ast::carg_lit(l) {
|
||||
let tmp_node_id = fcx.ccx.tcx.sess.next_node_id();
|
||||
{id: tmp_node_id,
|
||||
callee_id: fcx.ccx.tcx.sess.next_node_id(),
|
||||
node: ast::expr_lit(l), span: a.span}
|
||||
}
|
||||
ast::carg_ident(i) {
|
||||
if i < num_args {
|
||||
let p = @{span: a.span, global: false,
|
||||
idents: ~[args[i].ident],
|
||||
rp: none, types: ~[]};
|
||||
let arg_occ_node_id =
|
||||
fcx.ccx.tcx.sess.next_node_id();
|
||||
fcx.ccx.tcx.def_map.insert
|
||||
(arg_occ_node_id,
|
||||
ast::def_arg(args[i].id, args[i].mode));
|
||||
{id: arg_occ_node_id,
|
||||
callee_id: fcx.ccx.tcx.sess.next_node_id(),
|
||||
node: ast::expr_path(p),
|
||||
span: a.span}
|
||||
} else {
|
||||
fcx.ccx.tcx.sess.span_bug(
|
||||
a.span, ~"check_constraints:\
|
||||
carg_ident index out of bounds");
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
let p_op: ast::expr_ = ast::expr_path(c.node.path);
|
||||
let oper: @ast::expr = @{id: c.node.id,
|
||||
callee_id: fcx.ccx.tcx.sess.next_node_id(),
|
||||
node: p_op, span: c.span};
|
||||
// Another ephemeral expr
|
||||
let call_expr_id = fcx.ccx.tcx.sess.next_node_id();
|
||||
let call_expr =
|
||||
@{id: call_expr_id,
|
||||
callee_id: fcx.ccx.tcx.sess.next_node_id(),
|
||||
node: ast::expr_call(oper, c_args, false),
|
||||
span: c.span};
|
||||
check_pred_expr(fcx, call_expr);
|
||||
}
|
||||
}
|
||||
|
||||
// Determines whether the given node ID is a use of the def of
|
||||
// the self ID for the current method, if there is one
|
||||
// self IDs in an outer scope count. so that means that you can
|
||||
@ -2305,8 +2181,7 @@ fn check_intrinsic_type(ccx: @crate_ctxt, it: @ast::foreign_item) {
|
||||
ty::mk_mach_uint(ccx.tcx, ast::ty_u8))
|
||||
}],
|
||||
output: ty::mk_nil(ccx.tcx),
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]
|
||||
ret_style: ast::return_val
|
||||
});
|
||||
(0u, ~[arg(ast::by_ref, fty)], ty::mk_nil(tcx))
|
||||
}
|
||||
@ -2319,8 +2194,7 @@ fn check_intrinsic_type(ccx: @crate_ctxt, it: @ast::foreign_item) {
|
||||
let fty = ty::mk_fn(tcx, {purity: ast::impure_fn,
|
||||
proto: ast::proto_bare,
|
||||
inputs: inputs, output: output,
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]});
|
||||
ret_style: ast::return_val});
|
||||
let i_ty = ty::lookup_item_type(ccx.tcx, local_def(it.id));
|
||||
let i_n_tps = (*i_ty.bounds).len();
|
||||
if i_n_tps != n_tps {
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
import middle::typeck::infer::methods; // next_ty_var,
|
||||
// resolve_type_vars_if_possible
|
||||
import syntax::print::pprust;
|
||||
|
||||
fn check_alt(fcx: @fn_ctxt,
|
||||
expr: @ast::expr,
|
||||
@ -124,6 +125,7 @@ fn check_pat_variant(pcx: pat_ctxt, pat: @ast::pat, path: @ast::path,
|
||||
fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
|
||||
let fcx = pcx.fcx;
|
||||
let tcx = pcx.fcx.ccx.tcx;
|
||||
|
||||
alt pat.node {
|
||||
ast::pat_wild {
|
||||
fcx.write_ty(pat.id, expected);
|
||||
|
||||
@ -8,7 +8,7 @@ import middle::ty::{get, t, ty_box, ty_uniq, ty_ptr, ty_rptr, ty_enum};
|
||||
import middle::ty::{ty_class, ty_nil, ty_bot, ty_bool, ty_int, ty_uint};
|
||||
import middle::ty::{ty_float, ty_estr, ty_evec, ty_rec};
|
||||
import middle::ty::{ty_fn, ty_trait, ty_tup, ty_var, ty_var_integral};
|
||||
import middle::ty::{ty_param, ty_self, ty_constr, ty_type, ty_opaque_box};
|
||||
import middle::ty::{ty_param, ty_self, ty_type, ty_opaque_box};
|
||||
import middle::ty::{ty_opaque_closure_ptr, ty_unboxed_vec, new_ty_hash};
|
||||
import middle::ty::{subst};
|
||||
import middle::typeck::infer::{infer_ctxt, mk_subty, new_infer_ctxt};
|
||||
@ -173,7 +173,7 @@ class CoherenceChecker {
|
||||
ty_nil | ty_bot | ty_bool | ty_int(*) | ty_uint(*) | ty_float(*) |
|
||||
ty_estr(*) | ty_evec(*) | ty_rec(*) |
|
||||
ty_fn(*) | ty_tup(*) | ty_var(*) | ty_var_integral(*) |
|
||||
ty_param(*) | ty_self | ty_constr(*) | ty_type | ty_opaque_box |
|
||||
ty_param(*) | ty_self | ty_type | ty_opaque_box |
|
||||
ty_opaque_closure_ptr(*) | ty_unboxed_vec(*) {
|
||||
none
|
||||
}
|
||||
|
||||
@ -126,8 +126,7 @@ fn get_enum_variant_types(ccx: @crate_ctxt,
|
||||
proto: ast::proto_box,
|
||||
inputs: args,
|
||||
output: enum_ty,
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]})
|
||||
ret_style: ast::return_val})
|
||||
};
|
||||
let tpt = {bounds: ty_param_bounds(ccx, ty_params),
|
||||
rp: rp,
|
||||
@ -363,8 +362,7 @@ fn convert(ccx: @crate_ctxt, it: @ast::item) {
|
||||
proto: ast::proto_any,
|
||||
inputs: t_args,
|
||||
output: t_res,
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]}); // FIXME (#2813): allow ctors to have
|
||||
ret_style: ast::return_val});
|
||||
// constraints, or remove constraints from the language
|
||||
write_ty_to_tcx(tcx, ctor.node.id, t_ctor);
|
||||
tcx.tcache.insert(local_def(ctor.node.id),
|
||||
@ -618,8 +616,7 @@ fn ty_of_foreign_fn_decl(ccx: @crate_ctxt,
|
||||
proto: ast::proto_bare,
|
||||
inputs: input_tys,
|
||||
output: output_ty,
|
||||
ret_style: ast::return_val,
|
||||
constraints: ~[]});
|
||||
ret_style: ast::return_val});
|
||||
let tpt = {bounds: bounds, rp: false, ty: t_fn};
|
||||
ccx.tcx.tcache.insert(def_id, tpt);
|
||||
ret tpt;
|
||||
|
||||
@ -974,49 +974,6 @@ impl unify_methods for infer_ctxt {
|
||||
uok()
|
||||
}
|
||||
|
||||
fn constrs(
|
||||
expected: @ty::type_constr,
|
||||
actual_constr: @ty::type_constr) -> ures {
|
||||
|
||||
let err_res =
|
||||
err(ty::terr_constr_mismatch(expected, actual_constr));
|
||||
|
||||
if expected.node.id != actual_constr.node.id { ret err_res; }
|
||||
let expected_arg_len = vec::len(expected.node.args);
|
||||
let actual_arg_len = vec::len(actual_constr.node.args);
|
||||
if expected_arg_len != actual_arg_len { ret err_res; }
|
||||
let mut i = 0u;
|
||||
for expected.node.args.each |a| {
|
||||
let actual = actual_constr.node.args[i];
|
||||
alt a.node {
|
||||
ast::carg_base {
|
||||
alt actual.node {
|
||||
ast::carg_base { }
|
||||
_ { ret err_res; }
|
||||
}
|
||||
}
|
||||
ast::carg_lit(l) {
|
||||
alt actual.node {
|
||||
ast::carg_lit(m) {
|
||||
if l != m { ret err_res; }
|
||||
}
|
||||
_ { ret err_res; }
|
||||
}
|
||||
}
|
||||
ast::carg_ident(p) {
|
||||
alt actual.node {
|
||||
ast::carg_ident(q) {
|
||||
if p.idents != q.idents { ret err_res; }
|
||||
}
|
||||
_ { ret err_res; }
|
||||
}
|
||||
}
|
||||
}
|
||||
i += 1u;
|
||||
}
|
||||
ret uok();
|
||||
}
|
||||
|
||||
fn bnds<T:copy to_str st>(
|
||||
a: bound<T>, b: bound<T>) -> ures {
|
||||
|
||||
@ -1035,18 +992,6 @@ impl unify_methods for infer_ctxt {
|
||||
}
|
||||
}
|
||||
|
||||
fn constrvecs(
|
||||
as: ~[@ty::type_constr], bs: ~[@ty::type_constr]) -> ures {
|
||||
|
||||
if check vec::same_length(as, bs) {
|
||||
do iter_vec2(as, bs) |a,b| {
|
||||
self.constrs(a, b)
|
||||
}
|
||||
} else {
|
||||
err(ty::terr_constr_len(bs.len(), as.len()))
|
||||
}
|
||||
}
|
||||
|
||||
fn sub_tys(a: ty::t, b: ty::t) -> ures {
|
||||
sub(self).tys(a, b).chain(|_t| ok(()) )
|
||||
}
|
||||
@ -1584,7 +1529,7 @@ fn super_tps<C:combine>(
|
||||
// future we could allow type parameters to declare a
|
||||
// variance.
|
||||
|
||||
if check vec::same_length(as, bs) {
|
||||
if vec::same_length(as, bs) {
|
||||
iter_vec2(as, bs, |a, b| {
|
||||
self.infcx().eq_tys(a, b)
|
||||
}).then(|| ok(as) )
|
||||
@ -1674,7 +1619,7 @@ fn super_fns<C:combine>(
|
||||
fn argvecs<C:combine>(self: C, a_args: ~[ty::arg],
|
||||
b_args: ~[ty::arg]) -> cres<~[ty::arg]> {
|
||||
|
||||
if check vec::same_length(a_args, b_args) {
|
||||
if vec::same_length(a_args, b_args) {
|
||||
map_vec2(a_args, b_args, |a, b| self.args(a, b) )
|
||||
} else {
|
||||
err(ty::terr_arg_count)
|
||||
@ -1693,8 +1638,7 @@ fn super_fns<C:combine>(
|
||||
proto: p,
|
||||
inputs: inputs,
|
||||
output: output,
|
||||
ret_style: rs,
|
||||
constraints: a_f.constraints})
|
||||
ret_style: rs})
|
||||
// }
|
||||
}
|
||||
}
|
||||
@ -1824,7 +1768,7 @@ fn super_tys<C:combine>(
|
||||
}
|
||||
|
||||
(ty::ty_rec(as), ty::ty_rec(bs)) {
|
||||
if check vec::same_length(as, bs) {
|
||||
if vec::same_length(as, bs) {
|
||||
map_vec2(as, bs, |a,b| {
|
||||
self.flds(a, b)
|
||||
}).chain(|flds| ok(ty::mk_rec(tcx, flds)) )
|
||||
@ -1834,7 +1778,7 @@ fn super_tys<C:combine>(
|
||||
}
|
||||
|
||||
(ty::ty_tup(as), ty::ty_tup(bs)) {
|
||||
if check vec::same_length(as, bs) {
|
||||
if vec::same_length(as, bs) {
|
||||
map_vec2(as, bs, |a, b| self.tys(a, b) )
|
||||
.chain(|ts| ok(ty::mk_tup(tcx, ts)) )
|
||||
} else {
|
||||
@ -1848,14 +1792,6 @@ fn super_tys<C:combine>(
|
||||
}
|
||||
}
|
||||
|
||||
(ty::ty_constr(a_t, a_constrs), ty::ty_constr(b_t, b_constrs)) {
|
||||
do self.tys(a_t, b_t).chain |t| {
|
||||
do self.infcx().constrvecs(a_constrs, b_constrs).then {
|
||||
ok(ty::mk_constr(tcx, t, a_constrs))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
_ { err(ty::terr_sorts(b, a)) }
|
||||
}
|
||||
}
|
||||
|
||||
@ -89,19 +89,6 @@ mod middle {
|
||||
mod region;
|
||||
mod const_eval;
|
||||
mod astencode;
|
||||
|
||||
mod tstate {
|
||||
mod ck;
|
||||
mod annotate;
|
||||
#[path = "auxiliary.rs"]
|
||||
mod aux;
|
||||
mod bitvectors;
|
||||
mod collect_locals;
|
||||
mod pre_post_conditions;
|
||||
mod states;
|
||||
mod ann;
|
||||
mod tritv;
|
||||
}
|
||||
}
|
||||
|
||||
mod front {
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
import std::map::hashmap;
|
||||
import middle::ty;
|
||||
import middle::ty::{arg, bound_region, br_anon, br_named, canon_mode};
|
||||
import middle::ty::{ck_block, ck_box, ck_uniq, constr, ctxt, field, method};
|
||||
import middle::ty::{ck_block, ck_box, ck_uniq, ctxt, field, method};
|
||||
import middle::ty::{mt, re_bound, re_free, re_scope, re_var, region, t};
|
||||
import middle::ty::{ty_bool, ty_bot, ty_box, ty_class, ty_constr, ty_enum};
|
||||
import middle::ty::{ty_bool, ty_bot, ty_box, ty_class, ty_enum};
|
||||
import middle::ty::{ty_estr, ty_evec, ty_float, ty_fn, ty_trait, ty_int};
|
||||
import middle::ty::{ty_nil, ty_opaque_box, ty_opaque_closure_ptr, ty_param};
|
||||
import middle::ty::{ty_ptr, ty_rec, ty_rptr, ty_self, ty_tup};
|
||||
@ -12,7 +12,7 @@ import middle::ty::{ty_unboxed_vec, vid};
|
||||
import metadata::encoder;
|
||||
import syntax::codemap;
|
||||
import syntax::print::pprust;
|
||||
import syntax::print::pprust::{path_to_str, constr_args_to_str, proto_to_str,
|
||||
import syntax::print::pprust::{path_to_str, proto_to_str,
|
||||
mode_to_str, purity_to_str};
|
||||
import syntax::{ast, ast_util};
|
||||
import syntax::ast_map;
|
||||
@ -134,8 +134,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
|
||||
}
|
||||
fn fn_to_str(cx: ctxt, purity: ast::purity, proto: ast::proto,
|
||||
ident: option<ast::ident>,
|
||||
inputs: ~[arg], output: t, cf: ast::ret_style,
|
||||
constrs: ~[@constr]) -> ~str {
|
||||
inputs: ~[arg], output: t, cf: ast::ret_style) -> ~str {
|
||||
let mut s;
|
||||
|
||||
s = alt purity {
|
||||
@ -156,13 +155,12 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
|
||||
ast::return_val { s += ty_to_str(cx, output); }
|
||||
}
|
||||
}
|
||||
s += constrs_str(constrs);
|
||||
ret s;
|
||||
}
|
||||
fn method_to_str(cx: ctxt, m: method) -> ~str {
|
||||
ret fn_to_str(
|
||||
cx, m.fty.purity, m.fty.proto, some(m.ident), m.fty.inputs,
|
||||
m.fty.output, m.fty.ret_style, m.fty.constraints) + ~";";
|
||||
m.fty.output, m.fty.ret_style) + ~";";
|
||||
}
|
||||
fn field_to_str(cx: ctxt, f: field) -> ~str {
|
||||
ret *f.ident + ~": " + mt_to_str(cx, f.mt);
|
||||
@ -211,7 +209,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
|
||||
}
|
||||
ty_fn(f) {
|
||||
fn_to_str(cx, f.purity, f.proto, none, f.inputs,
|
||||
f.output, f.ret_style, f.constraints)
|
||||
f.output, f.ret_style)
|
||||
}
|
||||
ty_var(v) { v.to_str() }
|
||||
ty_var_integral(v) { v.to_str() }
|
||||
@ -234,7 +232,6 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
|
||||
}
|
||||
ty_estr(vs) { vstore_ty_to_str(cx, ~"str", vs) }
|
||||
ty_opaque_box { ~"@?" }
|
||||
ty_constr(t, _) { ~"@?" }
|
||||
ty_opaque_closure_ptr(ck_block) { ~"closure&" }
|
||||
ty_opaque_closure_ptr(ck_box) { ~"closure@" }
|
||||
ty_opaque_closure_ptr(ck_uniq) { ~"closure~" }
|
||||
@ -267,27 +264,6 @@ fn ty_to_short_str(cx: ctxt, typ: t) -> ~str {
|
||||
ret s;
|
||||
}
|
||||
|
||||
fn constr_to_str(c: @constr) -> ~str {
|
||||
ret path_to_str(c.node.path) +
|
||||
pprust::constr_args_to_str(pprust::uint_to_str, c.node.args);
|
||||
}
|
||||
|
||||
fn constrs_str(constrs: ~[@constr]) -> ~str {
|
||||
let mut s = ~"";
|
||||
let mut colon = true;
|
||||
for constrs.each |c| {
|
||||
if colon { s += ~" : "; colon = false; } else { s += ~", "; }
|
||||
s += constr_to_str(c);
|
||||
}
|
||||
ret s;
|
||||
}
|
||||
|
||||
fn ty_constr_to_str<Q>(c: @ast::spanned<ast::constr_general_<@ast::path, Q>>)
|
||||
-> ~str {
|
||||
ret path_to_str(c.node.path) +
|
||||
constr_args_to_str::<@ast::path>(path_to_str, c.node.args);
|
||||
}
|
||||
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
|
||||
@ -60,7 +60,7 @@ fn unindent(s: ~str) -> ~str {
|
||||
}
|
||||
};
|
||||
|
||||
if check vec::is_not_empty(lines) {
|
||||
if vec::is_not_empty(lines) {
|
||||
let unindented = ~[str::trim(vec::head(lines))]
|
||||
+ do par::anymap(vec::tail(lines)) |line| {
|
||||
if str::is_whitespace(line) {
|
||||
|
||||
@ -1,10 +0,0 @@
|
||||
// error-pattern:precondition constraint (for example, uint::le(a, b)
|
||||
use std;
|
||||
import str::*;
|
||||
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 4u;
|
||||
let b: uint = 1u;
|
||||
log(error, foo(a, b));
|
||||
}
|
||||
@ -1,12 +0,0 @@
|
||||
// error-pattern:unsatisfied precondition constraint
|
||||
pure fn even(x: uint) -> bool {
|
||||
if x < 2u {
|
||||
ret false;
|
||||
} else if x == 2u { ret true; } else { ret even(x - 2u); }
|
||||
}
|
||||
|
||||
fn print_even(x: uint) : even(x) { log(debug, x); }
|
||||
|
||||
fn foo(x: uint) { if check even(x) { fail; } else { print_even(x); } }
|
||||
|
||||
fn main() { foo(3u); }
|
||||
@ -1,14 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
fn g() { }
|
||||
|
||||
pure fn f(_q: int) -> bool {
|
||||
g(); //~ ERROR access to impure function prohibited in pure context
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let x = 0;
|
||||
|
||||
check (f(x));
|
||||
}
|
||||
@ -35,10 +35,12 @@ fn f4() {
|
||||
}
|
||||
|
||||
// leave this in here just to trigger compile-fail:
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
fn main() {
|
||||
let i: int = 4;
|
||||
log(debug, false && { check is_even(i); true });
|
||||
even(i); //~ ERROR unsatisfied precondition
|
||||
class r {
|
||||
let x: ();
|
||||
new() { self.x = (); }
|
||||
drop {}
|
||||
}
|
||||
fn main() {
|
||||
let x = r();
|
||||
fn@() { copy x; }; //~ ERROR copying a noncopyable value
|
||||
}
|
||||
|
||||
@ -1,16 +0,0 @@
|
||||
// https://github.com/mozilla/rust/issues/2374
|
||||
// error-pattern:unsatisfied precondition constraint (for example, even(y
|
||||
|
||||
|
||||
fn print_even(y: int) : even(y) { log(debug, y); }
|
||||
|
||||
pure fn even(y: int) -> bool { true }
|
||||
|
||||
fn main() {
|
||||
let mut y = 42;
|
||||
check (even(y));
|
||||
loop {
|
||||
print_even(y);
|
||||
loop { y += 1; break; }
|
||||
}
|
||||
}
|
||||
@ -1,18 +0,0 @@
|
||||
// error-pattern:unsatisfied precondition constraint (for example, uint::le
|
||||
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let mut a: uint = 1u;
|
||||
let mut b: uint = 4u;
|
||||
let mut c: uint = 5u;
|
||||
// make sure that the constraint le(b, a) exists...
|
||||
check (uint::le(b, a));
|
||||
// ...invalidate it...
|
||||
b += 1u;
|
||||
check (uint::le(c, a));
|
||||
// ...and check that it doesn't get set in the poststate of
|
||||
// the next statement, since it's not true in the
|
||||
// prestate.
|
||||
let d <- a;
|
||||
log(debug, foo(b, d));
|
||||
}
|
||||
@ -1,13 +0,0 @@
|
||||
// Tests that the typechecker checks constraints
|
||||
// error-pattern:mismatched types: expected `uint` but found `u8`
|
||||
use std;
|
||||
import uint;
|
||||
|
||||
fn enum_chars(start: u8, end: u8) : uint::le(start, end) -> ~[char] {
|
||||
let i = start;
|
||||
let r = ~[];
|
||||
while i <= end { r += ~[i as char]; i += 1u as u8; }
|
||||
ret r;
|
||||
}
|
||||
|
||||
fn main() { log(debug, enum_chars('a' as u8, 'z' as u8)); }
|
||||
@ -1,14 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern: non-predicate
|
||||
|
||||
fn main() {
|
||||
check (1 ==
|
||||
2); // should fail to typecheck, as (a == b)
|
||||
// is not a manifest call
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
@ -1,10 +0,0 @@
|
||||
// -*- rust -*-
|
||||
// error-pattern:impure function as operator
|
||||
|
||||
fn f(q: int) -> bool { ret true; }
|
||||
|
||||
fn main() {
|
||||
let x = 0;
|
||||
|
||||
check (f(x));
|
||||
}
|
||||
@ -1,11 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern:constraint args must be
|
||||
|
||||
pure fn f(q: int) -> bool { ret true; }
|
||||
|
||||
fn main() {
|
||||
// should fail to typecheck, as pred args must be slot variables
|
||||
// or literals
|
||||
check (f(42 * 17));
|
||||
}
|
||||
@ -1,16 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern:unsatisfied precondition constraint (for example, lt(a, b)
|
||||
|
||||
fn f(a: int, b: int) : lt(a, b) { }
|
||||
|
||||
pure fn lt(a: int, b: int) -> bool { ret a < b; }
|
||||
|
||||
fn main() {
|
||||
let mut a: int = 10;
|
||||
let mut b: int = 23;
|
||||
let mut c: int = 77;
|
||||
check (lt(a, b));
|
||||
a = 24;
|
||||
f(a, b);
|
||||
}
|
||||
@ -1,17 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern: lt(a, c)
|
||||
|
||||
fn f(a: int, b: int) : lt(a, b) { }
|
||||
|
||||
pure fn lt(a: int, b: int) -> bool { ret a < b; }
|
||||
|
||||
fn main() {
|
||||
let a: int = 10;
|
||||
let b: int = 23;
|
||||
let c: int = 77;
|
||||
check (lt(a, b));
|
||||
check (lt(b, c));
|
||||
f(a, b);
|
||||
f(a, c);
|
||||
}
|
||||
@ -1,16 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern:unsatisfied precondition constraint (for example, lt(a, b)
|
||||
|
||||
fn f(a: int, b: int) : lt(a, b) { }
|
||||
|
||||
pure fn lt(a: int, b: int) -> bool { ret a < b; }
|
||||
|
||||
fn main() {
|
||||
let mut a: int = 10;
|
||||
let mut b: int = 23;
|
||||
let mut c: int = 77;
|
||||
check (lt(a, b));
|
||||
b <-> a;
|
||||
f(a, b);
|
||||
}
|
||||
@ -1,12 +0,0 @@
|
||||
// -*- rust -*-
|
||||
// error-pattern: unresolved name: lt
|
||||
|
||||
fn f(a: int, b: int) : lt(a, b) { }
|
||||
|
||||
fn main() {
|
||||
let lt: int;
|
||||
let a: int = 10;
|
||||
let b: int = 23;
|
||||
check (lt(a, b));
|
||||
f(a, b);
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
fn main() {
|
||||
let i: int = 4;
|
||||
log(debug, false && { check is_even(i); true });
|
||||
even(i); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,11 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn force(f: fn()) { f(); }
|
||||
|
||||
fn main() {
|
||||
let x: int = 4;
|
||||
force(fn&() {
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
});
|
||||
}
|
||||
@ -1,16 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn foo() -> int {
|
||||
let x: int = 4;
|
||||
|
||||
while 1 != 2 {
|
||||
break;
|
||||
check is_even(x); //~ WARNING unreachable statement
|
||||
}
|
||||
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
ret 17;
|
||||
}
|
||||
|
||||
fn main() { log(debug, foo()); }
|
||||
@ -1,16 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn foo() -> int {
|
||||
let x: int = 4;
|
||||
|
||||
loop {
|
||||
break;
|
||||
check is_even(x); //~ WARNING unreachable statement
|
||||
}
|
||||
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
ret 17;
|
||||
}
|
||||
|
||||
fn main() { log(debug, foo()); }
|
||||
@ -1,25 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
class cat {
|
||||
priv {
|
||||
let mut meows : uint;
|
||||
}
|
||||
|
||||
let how_hungry : int;
|
||||
|
||||
fn eat() {
|
||||
self.how_hungry -= 5;
|
||||
}
|
||||
|
||||
new(in_x : uint, in_y : int) {
|
||||
let foo = 3;
|
||||
self.meows = in_x + (in_y as uint);
|
||||
self.how_hungry = even(foo); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let nyan : cat = cat(52u, 99);
|
||||
nyan.eat();
|
||||
}
|
||||
@ -1,14 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
type point = {x: int, y: int};
|
||||
|
||||
pure fn test(_p: point) -> bool { true }
|
||||
fn tested(p: point) : test(p) -> point { p }
|
||||
|
||||
fn main() {
|
||||
let origin: point;
|
||||
origin = {x: 0, y: 0};
|
||||
let right: point = {x: 10 with tested(origin)};
|
||||
//~^ ERROR precondition
|
||||
copy right;
|
||||
}
|
||||
@ -1,10 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn foo(x: int) { log(debug, x); }
|
||||
|
||||
fn main() {
|
||||
let x: int = 10;
|
||||
if 1 > 2 { check is_even(x); }
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,14 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn foo(x: int) { log(debug, x); }
|
||||
|
||||
fn main() {
|
||||
let x: int = 10;
|
||||
if 1 > 2 {
|
||||
#debug("whoops");
|
||||
} else {
|
||||
check is_even(x);
|
||||
}
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,19 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn main() {
|
||||
|
||||
let mut x: int = 42;
|
||||
loop {
|
||||
loop {
|
||||
loop {
|
||||
check is_even(x);
|
||||
even(x); // OK
|
||||
loop {
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
x = 11;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
fn main() {
|
||||
let i: int = 4;
|
||||
log(debug, false || { check is_even(i); true });
|
||||
even(i); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,9 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn f() -> int {
|
||||
let x: int = 4;
|
||||
ret even(x); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
|
||||
fn main() { f(); }
|
||||
@ -1,9 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn main() {
|
||||
let x = 4;
|
||||
fn baz(_x: int) { }
|
||||
baz(even(x)); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
|
||||
@ -1,9 +0,0 @@
|
||||
fn foo(v: ~[int]) : vec::is_empty(v) { #debug("%d", v[0]); }
|
||||
|
||||
fn main() {
|
||||
let f = fn@() {
|
||||
let v = ~[1];
|
||||
foo(v); //~ ERROR unsatisfied precondition constraint
|
||||
}();
|
||||
log(error, f);
|
||||
}
|
||||
@ -1,9 +0,0 @@
|
||||
fn foo(v: ~[int]) : vec::is_empty(v) { #debug("%d", v[0]); }
|
||||
|
||||
fn main() {
|
||||
let f = fn@() {
|
||||
let v = ~[1];
|
||||
foo(v); //~ ERROR unsatisfied precondition constraint
|
||||
};
|
||||
log(error, f());
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn main() {
|
||||
let x: int = 4;
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,15 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn test(cond: bool) {
|
||||
let v = 4;
|
||||
while cond {
|
||||
check is_even(v);
|
||||
break;
|
||||
}
|
||||
even(v); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
|
||||
fn main() {
|
||||
test(true);
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn main() {
|
||||
let x: int = 4;
|
||||
while even(x) != 0 { } //~ ERROR unsatisfied precondition
|
||||
}
|
||||
@ -1,16 +0,0 @@
|
||||
// error-pattern:unsatisfied precondition constraint (for example, even(y
|
||||
|
||||
fn print_even(y: int) : even(y) { log(debug, y); }
|
||||
|
||||
pure fn even(y: int) -> bool { true }
|
||||
|
||||
fn main() {
|
||||
|
||||
let mut y: int = 42;
|
||||
let mut x: int = 1;
|
||||
check (even(y));
|
||||
loop {
|
||||
print_even(y);
|
||||
while true { while true { while true { y += x; } } }
|
||||
}
|
||||
}
|
||||
@ -1,10 +0,0 @@
|
||||
pure fn is_even(i: int) -> bool { (i%2) == 0 }
|
||||
fn even(i: int) : is_even(i) -> int { i }
|
||||
|
||||
fn f() {
|
||||
let mut x: int = 10;
|
||||
while 1 == 1 { x = 10; }
|
||||
even(x); //~ ERROR unsatisfied precondition
|
||||
}
|
||||
|
||||
fn main() { f(); }
|
||||
@ -1,7 +0,0 @@
|
||||
// error-pattern:quux
|
||||
use std;
|
||||
import uint::*;
|
||||
|
||||
fn nop(a: uint, b: uint) : le(a, b) { fail ~"quux"; }
|
||||
|
||||
fn main() { let a: uint = 5u; let b: uint = 4u; claim (le(a, b)); nop(a, b); }
|
||||
@ -1,9 +0,0 @@
|
||||
// error-pattern:Predicate uint::le(a, b) failed
|
||||
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 4u;
|
||||
let b: uint = 1u;
|
||||
check (uint::le(a, b));
|
||||
log(error, foo(a, b));
|
||||
}
|
||||
@ -6,7 +6,7 @@ pure fn even(x: uint) -> bool {
|
||||
}
|
||||
|
||||
fn foo(x: uint) {
|
||||
if check even(x) {
|
||||
if even(x) {
|
||||
log(debug, x);
|
||||
} else {
|
||||
fail ~"Number is odd";
|
||||
|
||||
@ -1,7 +0,0 @@
|
||||
// -*- rust -*-
|
||||
// error-pattern:Predicate lt(b, a) failed
|
||||
fn f(a: int, b: int) { }
|
||||
|
||||
pure fn lt(a: int, b: int) -> bool { ret a < b; }
|
||||
|
||||
fn main() { let a: int = 10; let b: int = 23; check (lt(b, a)); f(b, a); }
|
||||
@ -1,8 +0,0 @@
|
||||
// error-pattern:fail
|
||||
|
||||
pure fn p(a: @int) -> bool { false }
|
||||
|
||||
fn main() {
|
||||
let a = @0;
|
||||
check p(a);
|
||||
}
|
||||
@ -1,6 +1,6 @@
|
||||
// In this case, the code should compile but
|
||||
// the check should fail at runtime
|
||||
// error-pattern:Predicate same_length
|
||||
// the assert should fail at runtime
|
||||
// error-pattern:Assertion same_length(chars, ints) failed
|
||||
use std;
|
||||
import uint;
|
||||
import u8;
|
||||
@ -25,12 +25,12 @@ fn enum_uints(start: uint, end: uint) -> ~[uint] {
|
||||
fn main() {
|
||||
let a = 'a' as u8, j = 'j' as u8, k = 1u, l = 9u;
|
||||
// Silly, but necessary
|
||||
check (u8::le(a, j));
|
||||
check (uint::le(k, l));
|
||||
assert (u8::le(a, j));
|
||||
assert (uint::le(k, l));
|
||||
let chars = enum_chars(a, j);
|
||||
let ints = enum_uints(k, l);
|
||||
|
||||
check (same_length(chars, ints));
|
||||
assert (same_length(chars, ints));
|
||||
let ps = zip(chars, ints);
|
||||
fail ~"the impossible happened";
|
||||
}
|
||||
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn p(j: int) -> bool { true }
|
||||
|
||||
fn f(i: int, j: int) : p(j) -> int { j }
|
||||
|
||||
fn g(i: int, j: int) : p(j) -> int { f(i, j) }
|
||||
|
||||
fn main() { let x = 1; check (p(x)); log(debug, g(x, x)); }
|
||||
@ -1,9 +0,0 @@
|
||||
use std;
|
||||
|
||||
pure fn p(x: int) -> bool { true }
|
||||
|
||||
fn f(x: int) : p(x) { }
|
||||
|
||||
fn main() {
|
||||
alt some(5) { some(y) { check (p(y)); f(y); } _ { fail ~"yuck"; } }
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
// tests that the pred in a claim isn't actually eval'd
|
||||
use std;
|
||||
import uint::*;
|
||||
|
||||
pure fn fails(a: uint) -> bool { fail; }
|
||||
|
||||
fn main() { let b: uint = 4u; claim (fails(b)); }
|
||||
@ -1,11 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
enum list { cons(int, @list), nil, }
|
||||
|
||||
type bubu = {x: int, y: int};
|
||||
|
||||
pure fn less_than(x: int, y: int) -> bool { ret x < y; }
|
||||
|
||||
type ordered_range = {low: int, high: int} : less_than(*.low, *.high);
|
||||
|
||||
fn main() { }
|
||||
@ -1,10 +0,0 @@
|
||||
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 1u;
|
||||
let b: uint = 4u;
|
||||
let mut c: uint = 17u;
|
||||
check (uint::le(a, b));
|
||||
c <- a;
|
||||
log(debug, foo(c, b));
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 1u;
|
||||
let b: uint = 4u;
|
||||
check (uint::le(a, b));
|
||||
let c <- a;
|
||||
log(debug, foo(c, b));
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let mut a: uint = 4u;
|
||||
let mut b: uint = 1u;
|
||||
check (uint::le(b, a));
|
||||
b <-> a;
|
||||
log(debug, foo(a, b));
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 1u;
|
||||
let b: uint = 4u;
|
||||
check uint::le(a, b);
|
||||
let c = b;
|
||||
log(debug, foo(a, c));
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
fn main() unsafe {
|
||||
fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
|
||||
let a: uint = 1u;
|
||||
let b: uint = 4u;
|
||||
check (uint::le(a, b));
|
||||
log(debug, foo(a, b));
|
||||
}
|
||||
@ -1,11 +0,0 @@
|
||||
pure fn even(x: uint) -> bool {
|
||||
if x < 2u {
|
||||
ret false;
|
||||
} else if x == 2u { ret true; } else { ret even(x - 2u); }
|
||||
}
|
||||
|
||||
fn print_even(x: uint) : even(x) { log(debug, x); }
|
||||
|
||||
fn foo(x: uint) { if check even(x) { print_even(x); } else { fail; } }
|
||||
|
||||
fn main() { foo(2u); }
|
||||
@ -5,7 +5,7 @@ pure fn even(x: uint) -> bool {
|
||||
}
|
||||
|
||||
fn foo(x: uint) {
|
||||
if check even(x) {
|
||||
if even(x) {
|
||||
log(debug, x);
|
||||
} else {
|
||||
fail;
|
||||
|
||||
@ -1,2 +0,0 @@
|
||||
pure fn c() -> bool { check c(); true }
|
||||
fn main() {}
|
||||
@ -1,6 +0,0 @@
|
||||
enum maybe_ordered_pair {
|
||||
yes({low: int, high: int} : less_than(*.low, *.high)),
|
||||
no
|
||||
}
|
||||
pure fn less_than(x: int, y: int) -> bool { ret x < y; }
|
||||
fn main() { }
|
||||
@ -10,19 +10,13 @@ pure fn pure_length<T: copy>(ls: @list<T>) -> uint { pure_length_go(ls, 0u) }
|
||||
|
||||
pure fn nonempty_list<T: copy>(ls: @list<T>) -> bool { pure_length(ls) > 0u }
|
||||
|
||||
// Of course, the compiler can't take advantage of the
|
||||
// knowledge that ls is a cons node. Future work.
|
||||
// Also, this is pretty contrived since nonempty_list
|
||||
// could be a "enum refinement", if we implement those.
|
||||
fn safe_head<T: copy>(ls: @list<T>) : nonempty_list(ls) -> T {
|
||||
check is_not_empty(ls);
|
||||
fn safe_head<T: copy>(ls: @list<T>) -> T {
|
||||
assert is_not_empty(ls);
|
||||
ret head(ls);
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let mylist = @cons(@1u, @nil);
|
||||
// Again, a way to eliminate such "obvious" checks seems
|
||||
// desirable. (Tags could have postconditions.)
|
||||
check (nonempty_list(mylist));
|
||||
assert (nonempty_list(mylist));
|
||||
assert (*safe_head(mylist) == 1u);
|
||||
}
|
||||
|
||||
@ -1,4 +0,0 @@
|
||||
// -*- rust -*-
|
||||
pure fn f(q: int) -> bool { ret true; }
|
||||
|
||||
fn main() { let x = 0; check (f(x)); }
|
||||
@ -1,14 +0,0 @@
|
||||
// -*- rust -*-
|
||||
fn f(a: int, b: int) { }
|
||||
|
||||
pure fn lt(a: int, b: int) -> bool { ret a < b; }
|
||||
|
||||
fn main() {
|
||||
let a: int = 10;
|
||||
let b: int = 23;
|
||||
let c: int = 77;
|
||||
check (lt(a, b));
|
||||
check (lt(a, c));
|
||||
f(a, b);
|
||||
f(a, c);
|
||||
}
|
||||
@ -1,7 +0,0 @@
|
||||
pure fn p(i: int) -> bool { true }
|
||||
|
||||
fn f(i: int) : p(i) -> int { i }
|
||||
|
||||
fn g(i: int) : p(i) -> int { f(i) }
|
||||
|
||||
fn main() { }
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
x
Reference in New Issue
Block a user