diff options
Diffstat (limited to 'Test/hofs/ResolveError.dfy')
-rw-r--r-- | Test/hofs/ResolveError.dfy | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy index 410842b3..3c0d7cd9 100644 --- a/Test/hofs/ResolveError.dfy +++ b/Test/hofs/ResolveError.dfy @@ -67,3 +67,44 @@ method Underscores() { var v := (_, _) => 0; var w := (_, _, _) => _; } + +module AritySituations { + // In addition to testing type checking, these tests check that error messages + // print the types correctly + function method F(x: int, b: bool): real // F: (int,bool) -> real + function method G(pair: (int, bool)): real // G: ((int,bool)) -> real + function method V(): real // V: () -> real + function method W(unit: ()): real // W: (()) -> real + + method M() + { + var f: (int, bool) -> real; + var g: ((int, bool)) -> real; + var h: (int, bool) -> real; + f := F; + g := G; + h := G; // error + + var f' := F; + var g' := G; + + var s0 := P(F, 5); // error: F takes 2 arguments, but P expect a function that takes 1 + var s1 := P(G, (2,true)); // fine + + var v: () -> real; + var w: (()) -> real; + v := V; + w := W; + var v': () -> real := V; + var w': (()) -> real := W; + var w'': ((((((())))))) -> real := W; + v := W; // error + w := V; // error + } + + method P(r: T -> U, x: T) returns (u: U) + requires r.requires(x); + { + u := r(x); + } +} |