diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 925bc5b384..08ff915da5 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -312,6 +312,8 @@ private void generate(Stmt stmt, EnclosingScope scope) { generate((Break) stmt, scope); } else if (stmt instanceof Continue) { generate((Continue) stmt, scope); + } else if (stmt instanceof NamedBlock) { + generate((NamedBlock) stmt, scope); } else if (stmt instanceof While) { generate((While) stmt, scope); } else if (stmt instanceof DoWhile) { @@ -974,6 +976,15 @@ private void checkNoDuplicateLabels(List cases, EnclosingScope scope) } + /** + * Translate a named block into WyIL bytecodes. + */ + private void generate(Stmt.NamedBlock s, EnclosingScope scope) { + for (Stmt st : s.body) { + generate(st, scope); + } + } + /** * Translate a while loop into WyIL bytecodes. Consider the following use of * a while statement: @@ -1675,7 +1686,8 @@ private Type.FunctionOrMethod determineLambdaParametersAndOperands(Expr.Lambda e if(lambdaType instanceof Nominal.Function) { return Type.Function(rawLambdaType.returns(),rawParamTypes); } else { - return Type.Method(rawLambdaType.returns(),rawParamTypes); + return Type.Method(rawLambdaType.returns(),rawLambdaType.contextLifetimes(), + rawLambdaType.lifetimeParams(),rawParamTypes); } } diff --git a/modules/wyc/src/wyc/builder/FlowTypeChecker.java b/modules/wyc/src/wyc/builder/FlowTypeChecker.java index d7f420c644..c3e77d7c7f 100644 --- a/modules/wyc/src/wyc/builder/FlowTypeChecker.java +++ b/modules/wyc/src/wyc/builder/FlowTypeChecker.java @@ -54,6 +54,8 @@ import wyil.lang.Type; import wyil.lang.WyilFile; import wyil.util.TypeExpander; +import wyil.util.type.LifetimeRelation; +import wyil.util.type.LifetimeSubstitution; /** * Propagates type information in a flow-sensitive fashion from declared @@ -246,7 +248,8 @@ public void propagate(WhileyFile.Constant cd) throws IOException, ResolveError { public void propagate(WhileyFile.FunctionOrMethod d) throws IOException { // Resolve the types of all parameters and construct an appropriate // environment for use in the flow-sensitive type propagation. - Environment environment = addDeclaredParameters(d.parameters, new Environment(), d); + Environment environment = new Environment().declareLifetimeParameters(d.lifetimeParameters); + environment = addDeclaredParameters(d.parameters, environment, d); environment = addDeclaredParameters(d.returns, environment, d); // Resolve types for any preconditions (i.e. requires clauses) provided. propagateConditions(d.requires, environment, d); @@ -262,6 +265,9 @@ public void propagate(WhileyFile.FunctionOrMethod d) throws IOException { m.resolvedType = resolveAsType(m.unresolvedType(), d); } + // Add the "this" lifetime + environment = environment.startNamedBlock("this"); + // Finally, propagate type information throughout all statements in the // function / method body. Environment last = propagate(d.statements, environment, d); @@ -362,6 +368,8 @@ private Environment propagate(Stmt stmt, Environment environment, Context contex return propagate((Stmt.Return) stmt, environment, context); } else if (stmt instanceof Stmt.IfElse) { return propagate((Stmt.IfElse) stmt, environment, context); + } else if (stmt instanceof Stmt.NamedBlock) { + return propagate((Stmt.NamedBlock) stmt, environment, context); } else if (stmt instanceof Stmt.While) { return propagate((Stmt.While) stmt, environment, context); } else if (stmt instanceof Stmt.Switch) { @@ -410,7 +418,7 @@ private Environment propagate(Stmt stmt, Environment environment, Context contex */ private Environment propagate(Stmt.Assert stmt, Environment environment, Context context) { stmt.expr = propagate(stmt.expr, environment, context); - checkIsSubtype(Type.T_BOOL, stmt.expr); + checkIsSubtype(Type.T_BOOL, stmt.expr, environment); return environment; } @@ -427,7 +435,7 @@ private Environment propagate(Stmt.Assert stmt, Environment environment, Context */ private Environment propagate(Stmt.Assume stmt, Environment environment, Context context) { stmt.expr = propagate(stmt.expr, environment, context); - checkIsSubtype(Type.T_BOOL, stmt.expr); + checkIsSubtype(Type.T_BOOL, stmt.expr, environment); return environment; } @@ -472,7 +480,7 @@ private Environment propagate(Stmt.VariableDeclaration stmt, Environment environ // to the newly declared variable. if (stmt.expr != null) { stmt.expr = propagate(stmt.expr, environment, context); - checkIsSubtype(stmt.type, stmt.expr); + checkIsSubtype(stmt.type, stmt.expr, environment); } // Third, update environment accordingly. Observe that we can safely @@ -527,15 +535,15 @@ private Environment propagate(Stmt.Assign stmt, Environment environment, Context for (int i = 0; i != valuesProduced.size(); ++i) { Expr.LVal lval = stmt.lvals.get(i); Nominal rval = valuesProduced.get(i).second(); - Expr.AssignedVariable av = inferAfterType(lval, rval); - checkIsSubtype(environment.getDeclaredType(av.var), av.afterType, av); + Expr.AssignedVariable av = inferAfterType(lval, rval, environment); + checkIsSubtype(environment.getDeclaredType(av.var), av.afterType, av, environment); environment = environment.update(av.var, av.afterType); } return environment; } - private Expr.AssignedVariable inferAfterType(Expr.LVal lv, Nominal afterType) { + private Expr.AssignedVariable inferAfterType(Expr.LVal lv, Nominal afterType, Environment environment) { if (lv instanceof Expr.AssignedVariable) { Expr.AssignedVariable v = (Expr.AssignedVariable) lv; v.afterType = afterType; @@ -544,20 +552,20 @@ private Expr.AssignedVariable inferAfterType(Expr.LVal lv, Nominal afterType) { Expr.Dereference pa = (Expr.Dereference) lv; // The before and after types are the same since an assignment // through a reference does not change its type. - checkIsSubtype(pa.srcType.element(), afterType, lv); - return inferAfterType((Expr.LVal) pa.src, pa.srcType); + checkIsSubtype(pa.srcType.element(), afterType, lv, environment); + return inferAfterType((Expr.LVal) pa.src, pa.srcType, environment); } else if (lv instanceof Expr.IndexOf) { Expr.IndexOf la = (Expr.IndexOf) lv; Nominal.Array srcType = la.srcType; afterType = (Nominal) srcType.update(la.index.result(), afterType); - return inferAfterType((Expr.LVal) la.src, afterType); + return inferAfterType((Expr.LVal) la.src, afterType, environment); } else if (lv instanceof Expr.FieldAccess) { Expr.FieldAccess la = (Expr.FieldAccess) lv; Nominal.Record srcType = la.srcType; // I know I can modify this hash map, since it's created fresh // in Nominal.Record.fields(). afterType = (Nominal) srcType.update(la.name, afterType); - return inferAfterType((Expr.LVal) la.src, afterType); + return inferAfterType((Expr.LVal) la.src, afterType, environment); } else { internalFailure("unknown lval: " + lv.getClass().getName(), filename, lv); return null; // deadcode @@ -611,7 +619,7 @@ private Environment propagate(Stmt.Continue stmt, Environment environment, Conte */ private Environment propagate(Stmt.Debug stmt, Environment environment, Context context) { stmt.expr = propagate(stmt.expr, environment, context); - checkIsSubtype(Type.Array(Type.T_INT, false), stmt.expr); + checkIsSubtype(Type.Array(Type.T_INT, false), stmt.expr, environment); return environment; } @@ -636,7 +644,7 @@ private Environment propagate(Stmt.DoWhile stmt, Environment environment, Contex Expr invariant = stmt_invariants.get(i); invariant = propagate(invariant, environment, context); stmt_invariants.set(i, invariant); - checkIsSubtype(Type.T_BOOL, invariant); + checkIsSubtype(Type.T_BOOL, invariant, environment); } // Type condition assuming its false to represent the terminated loop. @@ -756,7 +764,7 @@ private Environment propagate(Stmt.Return stmt, Environment environment, Context for(int i=0;i!=current_returns.size();++i) { Pair p = stmt_types.get(i); Nominal t = current_returns.get(i); - checkIsSubtype(t, p.second(), p.first()); + checkIsSubtype(t, p.second(), p.first(), environment); } environment.free(); @@ -873,6 +881,22 @@ private Environment propagate(Stmt.Switch stmt, Environment environment, Context return finalEnv; } + /** + * Type check a NamedBlock statement. + * + * @param stmt + * Statement to type check + * @param environment + * Determines the type of all variables immediately going into + * this block + * @return + */ + private Environment propagate(Stmt.NamedBlock stmt, Environment environment, Context context) { + environment = environment.startNamedBlock(stmt.name); + environment = propagate(stmt.body, environment, context); + return environment.endNamedBlock(stmt.name); + } + /** * Type check a whiley statement. * @@ -894,7 +918,7 @@ private Environment propagate(Stmt.While stmt, Environment environment, Context Expr invariant = stmt_invariants.get(i); invariant = propagate(invariant, environment, context); stmt_invariants.set(i, invariant); - checkIsSubtype(Type.T_BOOL, invariant); + checkIsSubtype(Type.T_BOOL, invariant, environment); } // Type condition assuming its false to represent the terminated loop. @@ -1020,7 +1044,7 @@ public Pair propagateCondition(Expr expr, boolean sign, Envir // For non-compound forms, can just default back to the base rules // for general expressions. expr = propagate(expr, environment, context); - checkIsSubtype(Type.T_BOOL, expr, context); + checkIsSubtype(Type.T_BOOL, expr, context, environment); return new Pair(expr, environment); } } @@ -1054,7 +1078,7 @@ private Pair propagateCondition(Expr.UnOp expr, boolean sign, if (uop.op == Expr.UOp.NOT) { Pair p = propagateCondition(uop.mhs, !sign, environment, context); uop.mhs = p.first(); - checkIsSubtype(Type.T_BOOL, uop.mhs, context); + checkIsSubtype(Type.T_BOOL, uop.mhs, context, environment); uop.type = Nominal.T_BOOL; return new Pair(uop, p.second()); } else { @@ -1173,8 +1197,8 @@ private Pair resolveNonLeafCondition(Expr.BinOp bop, boolean environment = local.merge(local.keySet(), p.second()); } - checkIsSubtype(Type.T_BOOL, bop.lhs, context); - checkIsSubtype(Type.T_BOOL, bop.rhs, context); + checkIsSubtype(Type.T_BOOL, bop.lhs, context, environment); + checkIsSubtype(Type.T_BOOL, bop.rhs, context, environment); bop.srcType = Nominal.T_BOOL; return new Pair(bop, environment); @@ -1273,7 +1297,7 @@ private Pair resolveLeafCondition(Expr.BinOp bop, boolean sig // we don't know anything about the rhs. It may be possible // to support bounds here in order to do that, but frankly // that's future work :) - checkIsSubtype(Type.T_META, rhs, context); + checkIsSubtype(Type.T_META, rhs, context, environment); } bop.srcType = lhs.result(); @@ -1282,8 +1306,8 @@ private Pair resolveLeafCondition(Expr.BinOp bop, boolean sig case LTEQ: case GTEQ: case GT: - checkSuptypes(lhs, context, Nominal.T_INT); - checkSuptypes(rhs, context, Nominal.T_INT); + checkSuptypes(lhs, context, environment, Nominal.T_INT); + checkSuptypes(rhs, context, environment, Nominal.T_INT); // if (!lhsRawType.equals(rhsRawType)) { syntaxError(errorMessage(INCOMPARABLE_OPERANDS, lhsRawType, rhsRawType), filename, bop); @@ -1318,9 +1342,9 @@ private Pair resolveLeafCondition(Expr.BinOp bop, boolean sig environment = environment.update(lv.var, newType); } else { // handle general case - if (Type.isSubtype(lhsRawType, rhsRawType)) { + if (Type.isSubtype(lhsRawType, rhsRawType, environment.getLifetimeRelation())) { bop.srcType = lhs.result(); - } else if (Type.isSubtype(rhsRawType, lhsRawType)) { + } else if (Type.isSubtype(rhsRawType, lhsRawType, environment.getLifetimeRelation())) { bop.srcType = rhs.result(); } else { syntaxError(errorMessage(INCOMPARABLE_OPERANDS, lhsRawType, rhsRawType), context, bop); @@ -1444,30 +1468,30 @@ private Expr propagate(Expr.BinOp expr, Environment environment, Context context case BITWISEAND: case BITWISEOR: case BITWISEXOR: - checkIsSubtype(Type.T_BYTE, lhs, context); - checkIsSubtype(Type.T_BYTE, rhs, context); + checkIsSubtype(Type.T_BYTE, lhs, context, environment); + checkIsSubtype(Type.T_BYTE, rhs, context, environment); srcType = Type.T_BYTE; break; case LEFTSHIFT: case RIGHTSHIFT: - checkIsSubtype(Type.T_BYTE, lhs, context); - checkIsSubtype(Type.T_INT, rhs, context); + checkIsSubtype(Type.T_BYTE, lhs, context, environment); + checkIsSubtype(Type.T_INT, rhs, context, environment); srcType = Type.T_BYTE; break; case RANGE: - checkIsSubtype(Type.T_INT, lhs, context); - checkIsSubtype(Type.T_INT, rhs, context); + checkIsSubtype(Type.T_INT, lhs, context, environment); + checkIsSubtype(Type.T_INT, rhs, context, environment); srcType = Type.Array(Type.T_INT, false); break; case REM: - checkIsSubtype(Type.T_INT, lhs, context); - checkIsSubtype(Type.T_INT, rhs, context); + checkIsSubtype(Type.T_INT, lhs, context, environment); + checkIsSubtype(Type.T_INT, rhs, context, environment); srcType = Type.T_INT; break; default: // all other operations go through here - checkSuptypes(lhs, context, Nominal.T_INT); - checkSuptypes(rhs, context, Nominal.T_INT); + checkSuptypes(lhs, context, environment, Nominal.T_INT); + checkSuptypes(rhs, context, environment, Nominal.T_INT); // if (!lhsRawType.equals(rhsRawType)) { syntaxError(errorMessage(INCOMPARABLE_OPERANDS, lhsRawType, rhsRawType), filename, expr); @@ -1495,10 +1519,10 @@ private Expr propagate(Expr.UnOp expr, Environment environment, Context context) switch (expr.op) { case NEG: - checkSuptypes(src, context, Nominal.T_INT); + checkSuptypes(src, context, environment, Nominal.T_INT); break; case INVERT: - checkIsSubtype(Type.T_BYTE, src, context); + checkIsSubtype(Type.T_BYTE, src, context, environment); break; case ARRAYLENGTH: { expr.type = expandAsEffectiveArray(expr.mhs, context); @@ -1523,7 +1547,7 @@ private Expr propagate(Expr.Quantifier expr, Environment environment, Context co Expr start = propagate(p.second(), local, context); Expr end = propagate(p.third(), local, context); sources.set(i, new Triple(p.first(), start, end)); - checkIsSubtype(Type.T_INT, start, context); + checkIsSubtype(Type.T_INT, start, context, environment); local = local.declare(p.first(), Nominal.T_INT, Nominal.T_INT); } @@ -1547,7 +1571,7 @@ private Expr propagate(Expr.Cast c, Environment environment, Context context) th c.type = resolveAsType(c.unresolvedType, context); Type from = c.expr.result().raw(); Type to = c.type.raw(); - if (!Type.isExplicitCoerciveSubtype(to, from)) { + if (!Type.isExplicitCoerciveSubtype(to, from, environment.getLifetimeRelation())) { syntaxError(errorMessage(SUBTYPE_ERROR, to, from), context, c); } return c; @@ -1560,7 +1584,7 @@ private Expr propagate(Expr.AbstractFunctionOrMethod expr, Environment environme return expr; } - Pair p; + Triple> p; if (expr.paramTypes != null) { ArrayList paramTypes = new ArrayList(); @@ -1568,18 +1592,19 @@ private Expr propagate(Expr.AbstractFunctionOrMethod expr, Environment environme paramTypes.add(resolveAsType(t, context)); } // FIXME: clearly a bug here in the case of message reference - p = (Pair) resolveAsFunctionOrMethod(expr.name, paramTypes, context); + p = (Triple>) resolveAsFunctionOrMethod(expr.name, paramTypes, + expr.lifetimeParameters, context, environment); } else { - p = resolveAsFunctionOrMethod(expr.name, context); + p = resolveAsFunctionOrMethod(expr.name, context, environment); } - expr = new Expr.FunctionOrMethod(p.first(), expr.paramTypes, expr.attributes()); + expr = new Expr.FunctionOrMethod(p.first(), expr.paramTypes, p.third, expr.attributes()); expr.type = p.second(); return expr; } private Expr propagate(Expr.Lambda expr, Environment environment, Context context) throws IOException { - environment = environment.clone(); + environment = environment.startLambda(expr.contextLifetimes, expr.lifetimeParameters); Type.FunctionOrMethod rawResultType; Type.FunctionOrMethod nomResultType; ArrayList rawParameterTypes = new ArrayList(); @@ -1618,8 +1643,8 @@ private Expr propagate(Expr.Lambda expr, Environment environment, Context contex rawResultType = Type.Function(rawReturnTypes, rawParameterTypes); nomResultType = Type.Function(nomReturnTypes, nomParameterTypes); } else { - rawResultType = Type.Method(rawReturnTypes, rawParameterTypes); - nomResultType = Type.Method(nomReturnTypes, nomParameterTypes); + rawResultType = Type.Method(rawReturnTypes, expr.contextLifetimes, expr.lifetimeParameters, rawParameterTypes); + nomResultType = Type.Method(nomReturnTypes, expr.contextLifetimes, expr.lifetimeParameters, nomParameterTypes); } expr.type = (Nominal.FunctionOrMethod) Nominal.construct(nomResultType, rawResultType); @@ -1629,25 +1654,96 @@ private Expr propagate(Expr.Lambda expr, Environment environment, Context contex private Expr propagate(Expr.AbstractIndirectInvoke expr, Environment environment, Context context) throws IOException, ResolveError { + // We can only invoke functions and methods expr.src = propagate(expr.src, environment, context); Nominal.FunctionOrMethod funType = expandAsFunctionOrMethod(expr.src.result()); if (funType == null) { syntaxError("function or method type expected", context, expr.src); } + // Do we have matching argument count? List paramTypes = funType.params(); ArrayList exprArgs = expr.arguments; - if (paramTypes.size() != exprArgs.size()) { syntaxError("insufficient arguments for function or method invocation", context, expr.src); } + // resolve through arguments + ArrayList argTypes = new ArrayList(); for (int i = 0; i != exprArgs.size(); ++i) { - Nominal pt = paramTypes.get(i); Expr arg = propagate(exprArgs.get(i), environment, context); - checkIsSubtype(pt, arg, context); exprArgs.set(i, arg); + argTypes.add(arg.result()); + } + // Handle lifetime arguments + List lifetimeParameters = funType.raw().lifetimeParams(); + List lifetimeArguments = expr.lifetimeArguments; + if (lifetimeArguments == null) { + // First consider the case where no lifetime arguments are specified. + if (lifetimeParameters.isEmpty()) { + // No lifetime arguments needed! + lifetimeArguments = Collections.emptyList(); + } else { + // We have to guess proper lifetime arguments. + List rawArgTypes = stripNominal(argTypes); + List validCandidates = new ArrayList(); + guessLifetimeArguments( + extractLifetimesFromArguments(rawArgTypes), + lifetimeParameters, + funType.raw().params(), + rawArgTypes, + null, // don't need a name id + funType, + validCandidates, + environment); + + if (validCandidates.isEmpty()) { + // We were not able to guess lifetime arguments + syntaxError("no lifetime arguments specified and unable to infer them", context, expr.src); + } + if (validCandidates.size() == 1) { + // All right, we found proper lifetime arguments. + // Note that at this point we indeed have a method + // (not a function), because functions don't have + // lifetime parameters. + Expr.IndirectMethodCall imc = new Expr.IndirectMethodCall( + expr.src, exprArgs, + validCandidates.get(0).lifetimeArguments, + expr.attributes()); + imc.methodType = (Nominal.Method) funType; + return imc; + } + + // Arriving here means we have more than one possible solution. + // That is an ambiguity error, but we're nice and also print all + // solutions. + StringBuilder msg = new StringBuilder( + "no lifetime arguments specified and unable to infer a unique solution"); + List solutions = new ArrayList(validCandidates.size()); + for (ValidCandidate vc : validCandidates) { + solutions.add(vc.lifetimeArguments.toString()); + } + Collections.sort(solutions); // make error message deterministic! + for (String s : solutions) { + msg.append("\nfound solution: "); + msg.append(s); + } + syntaxError(msg.toString(), context, expr.src); + } + } + if (lifetimeParameters.size() != lifetimeArguments.size()) { + // Lifetime arguments specified, but number doesn't match + syntaxError("insufficient lifetime arguments for method invocation", context, expr.src); + } + + // Check argument types with respect to specified lifetime arguments + Map substitution = buildSubstitution(lifetimeParameters, lifetimeArguments); + for (int i = 0; i != exprArgs.size(); ++i) { + Nominal pt = paramTypes.get(i); + Expr arg = propagate(exprArgs.get(i), environment, context); + checkIsSubtype(applySubstitution(substitution, pt), arg, context, environment); + exprArgs.set(i, arg); } if (funType instanceof Nominal.Function) { @@ -1655,11 +1751,10 @@ private Expr propagate(Expr.AbstractIndirectInvoke expr, Environment environment ifc.functionType = (Nominal.Function) funType; return ifc; } else { - Expr.IndirectMethodCall imc = new Expr.IndirectMethodCall(expr.src, exprArgs, expr.attributes()); + Expr.IndirectMethodCall imc = new Expr.IndirectMethodCall(expr.src, exprArgs, lifetimeArguments, expr.attributes()); imc.methodType = (Nominal.Method) funType; return imc; } - } private Expr propagate(Expr.AbstractInvoke expr, Environment environment, Context context) @@ -1669,6 +1764,7 @@ private Expr propagate(Expr.AbstractInvoke expr, Environment environment, Contex Path.ID qualification = expr.qualification; ArrayList exprArgs = expr.arguments; + ArrayList lifetimeArgs = expr.lifetimeArguments; ArrayList paramTypes = new ArrayList(); for (int i = 0; i != exprArgs.size(); ++i) { Expr arg = propagate(exprArgs.get(i), environment, context); @@ -1689,14 +1785,14 @@ private Expr propagate(Expr.AbstractInvoke expr, Environment environment, Contex // third, lookup the appropriate function or method based on the name // and given parameter types. - Nominal.FunctionOrMethod funType = resolveAsFunctionOrMethod(name, paramTypes, context); - if (funType instanceof Nominal.Function) { + Triple> triple = resolveAsFunctionOrMethod(name, paramTypes, lifetimeArgs, context, environment); + if (triple.second() instanceof Nominal.Function) { Expr.FunctionCall r = new Expr.FunctionCall(name, qualification, exprArgs, expr.attributes()); - r.functionType = (Nominal.Function) funType; + r.functionType = (Nominal.Function) triple.second(); return r; } else { - Expr.MethodCall r = new Expr.MethodCall(name, qualification, exprArgs, expr.attributes()); - r.methodType = (Nominal.Method) funType; + Expr.MethodCall r = new Expr.MethodCall(name, qualification, exprArgs, triple.third(), expr.attributes()); + r.methodType = (Nominal.Method) triple.second(); return r; } } @@ -1713,7 +1809,7 @@ private Expr propagate(Expr.IndexOf expr, Environment environment, Context conte expr.srcType = srcType; } - checkIsSubtype(srcType.key(), expr.index, context); + checkIsSubtype(srcType.key(), expr.index, context, environment); return expr; } @@ -1744,7 +1840,7 @@ private Expr propagate(Expr.ArrayGenerator expr, Environment environment, Contex expr.element = propagate(expr.element, environment, context); expr.count = propagate(expr.count, environment, context); expr.type = Nominal.Array(expr.element.result(), true); - checkIsSubtype(Type.T_INT, expr.count); + checkIsSubtype(Type.T_INT, expr.count, environment); return expr; } @@ -1813,13 +1909,17 @@ private Expr propagate(Expr.Dereference expr, Environment environment, Context c if (srcType == null) { syntaxError("invalid reference expression", context, src); } + String lifetime = srcType.raw().lifetime(); + if (!environment.canDereferenceLifetime(lifetime)) { + syntaxError("lifetime '" + lifetime + "' cannot be dereferenced here", context, expr); + } expr.srcType = srcType; return expr; } private Expr propagate(Expr.New expr, Environment environment, Context context) { expr.expr = propagate(expr.expr, environment, context); - expr.type = Nominal.Reference(expr.expr.result()); + expr.type = Nominal.Reference(expr.expr.result(), expr.lifetime); return expr; } @@ -1954,13 +2054,17 @@ private Environment computeFixedPoint(Environment environment, ArrayList b * * @param nid * @param parameters - * @return + * @param lifetimeArgs + * --- lifetime arguments passed on method invocation, + * or null if none are passed and the compiler has to figure it out + * @return nameid, type, given/inferred lifetime arguments * @throws IOException */ - public Nominal.FunctionOrMethod resolveAsFunctionOrMethod(NameID nid, List parameters, Context context) + public Triple> resolveAsFunctionOrMethod(NameID nid, + List parameters, List lifetimeArgs, Context context, Environment environment) throws IOException, ResolveError { - // Thet set of candidate names and types for this function or method. + // The set of candidate names and types for this function or method. HashSet> candidates = new HashSet>(); // First, add all valid candidates to the list without considering which @@ -1969,7 +2073,7 @@ public Nominal.FunctionOrMethod resolveAsFunctionOrMethod(NameID nid, List resolveAsFunctionOrMethod(String name, Context context) + public Triple> resolveAsFunctionOrMethod(String name, + Context context, Environment environment) throws IOException, ResolveError { - return resolveAsFunctionOrMethod(name, null, context); + return resolveAsFunctionOrMethod(name, null, null, context, environment); } /** @@ -1999,13 +2104,16 @@ public Pair resolveAsFunctionOrMethod(String n * --- name of function or method whose type to determine. * @param parameters * --- required parameter types for the function or method. + * @param lifetimeArgs + * --- lifetime arguments passed on method invocation, + * or null if none are passed and the compiler has to figure it out * @param context * --- context in which to resolve this name. - * @return + * @return nameid, type, given/inferred lifetime arguments * @throws IOException */ - public Pair resolveAsFunctionOrMethod(String name, List parameters, - Context context) throws IOException, ResolveError { + public Triple> resolveAsFunctionOrMethod(String name, List parameters, + List lifetimeArgs, Context context, Environment environment) throws IOException, ResolveError { HashSet> candidates = new HashSet>(); // first, try to find the matching message @@ -2026,35 +2134,22 @@ public Pair resolveAsFunctionOrMethod(String n } } - return selectCandidateFunctionOrMethod(name, parameters, candidates, context); + return selectCandidateFunctionOrMethod(name, parameters, lifetimeArgs, candidates, context, environment); } - private boolean paramSubtypes(Type.FunctionOrMethod f1, Type.FunctionOrMethod f2) { - List f1_params = f1.params(); - List f2_params = f2.params(); - if (f1_params.size() == f2_params.size()) { - for (int i = 0; i != f1_params.size(); ++i) { - Type f1_param = f1_params.get(i); - Type f2_param = f2_params.get(i); - if (!Type.isSubtype(f1_param, f2_param)) { - return false; - } - } - - return true; - } - return false; - } - - private boolean paramStrictSubtypes(Type.FunctionOrMethod f1, Type.FunctionOrMethod f2) { - List f1_params = f1.params(); - List f2_params = f2.params(); + /** + * @param f1_params + * @param f2_params + * @param environment + * @return whether f2_params are strict subtypes of f1_params + */ + private boolean paramStrictSubtypes(List f1_params, List f2_params, Environment environment) { if (f1_params.size() == f2_params.size()) { boolean allEqual = true; for (int i = 0; i != f1_params.size(); ++i) { Type f1_param = f1_params.get(i); Type f2_param = f2_params.get(i); - if (!Type.isSubtype(f1_param, f2_param)) { + if (!Type.isSubtype(f1_param, f2_param, environment.getLifetimeRelation())) { return false; } allEqual &= f1_param.equals(f2_param); @@ -2085,88 +2180,343 @@ private String parameterString(List paramTypes) { return paramStr + ")"; } - private Pair selectCandidateFunctionOrMethod(String name, - List parameters, Collection> candidates, Context context) - throws IOException, ResolveError { + private String foundCandidatesString(Collection> candidates) { + ArrayList candidateStrings = new ArrayList(); + for (Pair c : candidates) { + candidateStrings.add(c.first() + " : " + c.second().nominal()); + } + Collections.sort(candidateStrings); // make error message deterministic! + StringBuilder msg = new StringBuilder(); + for (String s : candidateStrings) { + msg.append("\n\tfound: "); + msg.append(s); + } + return msg.toString(); + } - List rawParameters; - Type.Function target; + /** + * Extract all lifetime names from the types in the given list. + * + * We just walk through the type automata and collect the lifetime for each + * encountered reference. + * + * The result set will always contain the default lifetime "*". + * + * @param types + * the types to get the lifetimes from + * @return a set of all extracted lifetime names, without "*" + */ + private List extractLifetimesFromArguments(Iterable types) { + Set result = new HashSet(); + for (Type t : types) { + Automaton automaton = Type.destruct(t); + for (Automaton.State s : automaton.states) { + if (s.kind == Type.K_REFERENCE) { + String lifetime = (String) s.data; + if (!lifetime.equals("*")) { + result.add(lifetime); + } + } + } + } + result.add("*"); + return new ArrayList(result); + } - if (parameters != null) { - // FIXME: this seems to be fundamentally broken in that the number - // of expected return values is completely unknown. - ArrayList rawReturns = new ArrayList(); - rawReturns.add(Type.T_ANY); - rawParameters = stripNominal(parameters); - target = (Type.Function) Type.Function(rawReturns, rawParameters); - } else { - rawParameters = null; - target = null; + /** + * Container for a function/method candidate during method resolution. + */ + private static class ValidCandidate { + private final NameID id; + private final Nominal.FunctionOrMethod type; + + // Either given (lifetimeArgs) or inferred + private final List lifetimeArguments; + + // Lifetime parameters substituted with (inferred) arguments + private final List parameterTypesSubstituted; + + private ValidCandidate(NameID id, Nominal.FunctionOrMethod type, List lifetimeArguments, List parameterTypesSubstituted) { + this.id = id; + this.type = type; + this.lifetimeArguments = lifetimeArguments; + this.parameterTypesSubstituted = parameterTypesSubstituted; } + } - NameID candidateID = null; - Nominal.FunctionOrMethod candidateType = null; - for (Pair p : candidates) { - Nominal.FunctionOrMethod nft = p.second(); - Type.FunctionOrMethod ft = nft.raw(); - if (parameters == null || paramSubtypes(ft, target)) { - // this is now a genuine candidate - if (candidateType == null || paramStrictSubtypes(candidateType.raw(), ft)) { - candidateType = nft; - candidateID = p.first(); - } else if (!paramStrictSubtypes(ft, candidateType.raw())) { - // this is an ambiguous error - StringBuilder msg = new StringBuilder(name + parameterString(parameters) + " is ambiguous"); - // FIXME: should report all ambiguous matches here - List candidateStrings = new ArrayList(); - candidateStrings.add(candidateID + " : " + candidateType.nominal()); - candidateStrings.add(p.first() + " : " + p.second().nominal()); - Collections.sort(candidateStrings);// make error message deterministic! - for (String s : candidateStrings) { - msg.append("\n\tfound: "); - msg.append(s); + /** + * Highly optimized method to validate a function/method candidate. + * + * @param candidateId + * @param candidateType + * @param candidateParameterTypes + * @param targetParameterTypes + * @param lifetimeParameters + * @param lifetimeArguments + * @param environment + * @return + */ + private static ValidCandidate validateCandidate(NameID candidateId, Nominal.FunctionOrMethod candidateType, + List candidateParameterTypes, List targetParameterTypes, + List lifetimeParameters, List lifetimeArguments, Environment environment) { + if (!lifetimeParameters.isEmpty()) { + // Here we *might* need a substitution + Map substitution = buildSubstitution(lifetimeParameters, lifetimeArguments); + if (!substitution.isEmpty()) { + // OK, substitution is necessary. + Iterator itC = candidateParameterTypes.iterator(); + Iterator itT = targetParameterTypes.iterator(); + List parameterTypesSubstituted = new ArrayList(candidateParameterTypes.size()); + while (itC.hasNext()) { + Type c = itC.next(); + Type t = itT.next(); + c = applySubstitution(substitution, c); + if (!Type.isSubtype(c, t, environment.getLifetimeRelation())) { + return null; } - throw new ResolveError(msg.toString()); + parameterTypesSubstituted.add(c); } + return new ValidCandidate(candidateId, candidateType, lifetimeArguments, parameterTypesSubstituted); + } + } + + // No substitution necessary, just do the check + Iterator itC = candidateParameterTypes.iterator(); + Iterator itT = targetParameterTypes.iterator(); + while (itC.hasNext()) { + Type c = itC.next(); + Type t = itT.next(); + if (!Type.isSubtype(c, t, environment.getLifetimeRelation())) { + return null; } } + return new ValidCandidate(candidateId, candidateType, Collections. emptyList(), candidateParameterTypes); + } - if (candidateType == null) { - // second, didn't find matching message so generate error message - String msg = "no match for " + name + parameterString(parameters); + private Triple> selectCandidateFunctionOrMethod(String name, + List parameters, List lifetimeArgs, + Collection> candidates, + Context context, Environment environment) + throws IOException, ResolveError { - for (Pair p : candidates) { - msg += "\n\tfound: " + p.first() + " : " + p.second().nominal(); + // We cannot do anything here without candidates + if (candidates.isEmpty()) { + throw new ResolveError("no match for " + name + parameterString(parameters)); + } + + // If we don't match parameters, then we don't need to bother about + // lifetimes. Handle it separately to avoid null checks in further + // logic. + if (parameters == null) { + if (candidates.size() == 1) { + Pair p = candidates.iterator().next(); + return new Triple<>(p.first(), p.second(), null); } - throw new ResolveError(msg); - } else { + // More than one candidate and all will match. Clearly ambiguous! + throw new ResolveError(name + parameterString(parameters) + " is ambiguous" + + foundCandidatesString(candidates)); + } + + // We chose a method based only on the parameter types, as return + // type(s) are unknown. + List targetParameterTypes = stripNominal(parameters); + + // In case we don't get lifetime arguments, we have to pick a possible + // substitution by guessing. To do so, we need all lifetime names that + // occur in the passed argument types. We will cache it here once we + // compute it (only compute it if needed. + List lifetimesUsedInArguments = null; + + // Check each candidate to see if it is valid. + List validCandidates = new LinkedList(); + for (Pair p : candidates) { + Nominal.FunctionOrMethod candidateType = p.second(); + List candidateParameterTypes = candidateType.raw().params(); + + // We need a matching parameter count + if (candidateParameterTypes.size() != targetParameterTypes.size()) { + continue; + } + + // If we got lifetime arguments: Lifetime parameter count must match + List candidateLifetimeParams = candidateType.raw().lifetimeParams(); + if (lifetimeArgs != null && candidateLifetimeParams.size() != lifetimeArgs.size()) { + continue; + } + + if (candidateLifetimeParams.isEmpty()) { + // We don't need lifetime arguments, so just provide an empty list. + ValidCandidate vc = validateCandidate(p.first(), + candidateType, candidateParameterTypes, + targetParameterTypes, candidateLifetimeParams, + Collections. emptyList(), + environment); + if (vc != null) { + validCandidates.add(vc); + } + } else if (lifetimeArgs != null) { + // We got some lifetime arguments. Just check it with them. + ValidCandidate vc = validateCandidate(p.first(), + candidateType, candidateParameterTypes, + targetParameterTypes, candidateLifetimeParams, + lifetimeArgs, + environment); + if (vc != null) { + validCandidates.add(vc); + } + } else { + // Here it is a bit tricky: + // We need to "guess" suitable lifetime arguments. + + // Make sure we know all lifetime names from our arguments, and + // cache the result for the next candidate. + if (lifetimesUsedInArguments == null) { + lifetimesUsedInArguments = extractLifetimesFromArguments(targetParameterTypes); + } + + // Guess the lifetime arguments. + guessLifetimeArguments(lifetimesUsedInArguments, candidateLifetimeParams, + candidateParameterTypes, targetParameterTypes, + p.first(), candidateType, validCandidates, environment); + } + } + + // See if we have valid candidates + if (validCandidates.isEmpty()) { + // No valid candidates + throw new ResolveError("no match for " + name + parameterString(parameters) + + foundCandidatesString(candidates)); + } + + // More than one candidate + if (validCandidates.size() != 1) { + // Idea: We iterate through the list and delete a valid candidate, + // if there is another one that is a strict subtype. + // The outer iterator is used to actually modify the list by + // removing candidates. + ListIterator it = validCandidates.listIterator(); + + // we know that the list is not empty, so do-while is perfectly fine + // here + do { + ValidCandidate c1 = it.next(); + + // Let the inner iterator start at the next entry. Note that the + // list initially had > 1 elements and the outer do-while also + // checks that there is one more element left, so we can again + // use do-while here. + for (ValidCandidate c2 : validCandidates) { + if (c1 != c2 && paramStrictSubtypes(c1.parameterTypesSubstituted, c2.parameterTypesSubstituted, environment)) { + it.remove(); + break; + } + } + } while (it.hasNext()); + } + + if (validCandidates.size() == 1) { // now check protection modifier - WhileyFile wf = builder.getSourceFile(candidateID.module()); + ValidCandidate winner = validCandidates.get(0); + NameID winnerId = winner.id; + Nominal.FunctionOrMethod winnerType = winner.type; + WhileyFile wf = builder.getSourceFile(winnerId.module()); if (wf != null) { if (wf != context.file()) { - for (WhileyFile.FunctionOrMethod d : wf.declarations(WhileyFile.FunctionOrMethod.class, - candidateID.name())) { - if (d.parameters.equals(candidateType.params())) { + for (WhileyFile.FunctionOrMethod d : wf.declarations(WhileyFile.FunctionOrMethod.class, winnerId.name())) { + if (d.parameters.equals(winnerType.params())) { if (!d.hasModifier(Modifier.PUBLIC)) { - String msg = candidateID.module() + "." + name + parameterString(parameters) - + " is not visible"; + String msg = winnerId.module() + "." + name + parameterString(parameters) + " is not visible"; throw new ResolveError(msg); } } } } } else { - WyilFile m = builder.getModule(candidateID.module()); - WyilFile.FunctionOrMethod d = m.functionOrMethod(candidateID.name(), candidateType.nominal()); + WyilFile m = builder.getModule(winnerId.module()); + WyilFile.FunctionOrMethod d = m.functionOrMethod(winnerId.name(), winnerType.nominal()); if (!d.hasModifier(Modifier.PUBLIC)) { - String msg = candidateID.module() + "." + name + parameterString(parameters) + " is not visible"; + String msg = winnerId.module() + "." + name + parameterString(parameters) + " is not visible"; throw new ResolveError(msg); } } + + return new Triple>(winnerId, winnerType, winner.lifetimeArguments); } - return new Pair(candidateID, candidateType); + // this is an ambiguous error + StringBuilder msg = new StringBuilder(name + parameterString(parameters) + " is ambiguous"); + ArrayList candidateStrings = new ArrayList(); + for (ValidCandidate c : validCandidates) { + String s = c.id + " : " + c.type.nominal(); + if (!c.lifetimeArguments.isEmpty()) { + s += " instantiated with <"; + boolean first = true; + for (String lifetime : c.lifetimeArguments) { + if (!first) { + s += ", "; + } else { + first = false; + } + s += lifetime; + } + s += ">"; + } + candidateStrings.add(s); + } + Collections.sort(candidateStrings); // make error message deterministic! + for (String s : candidateStrings) { + msg.append("\n\tfound: "); + msg.append(s); + } + throw new ResolveError(msg.toString()); + } + + /** + * Guess lifetime arguments for a method call. + * + * @param lifetimesUsedInArguments + * possible choices for lifetimes to be used as argument + * @param candidateLifetimeParams + * lifetime parameters to be assigned with an argument + * @param candidateParameterTypes + * parameter types of the actual declared method + * @param targetParameterTypes + * parameter types as needed (extracted from caller arguments) + * @param candidateName + * @param candidateType + * @param validCandidates + * the set where we can put valid substitutions + * @param environment + */ + private static void guessLifetimeArguments( + List lifetimesUsedInArguments, List candidateLifetimeParams, + List candidateParameterTypes, List targetParameterTypes, + NameID candidateName, Nominal.FunctionOrMethod candidateType, + List validCandidates, Environment environment) { + // Assume we have "exp" lifetime parameters to be filled and + // "base" choices for each one. + // That makes base^exp possibilities! + int base = lifetimesUsedInArguments.size(); + int exp = candidateLifetimeParams.size(); + long count = (long) Math.pow(base, exp); + for (long guessNumber = 0; guessNumber < count; guessNumber++) { + // Here we generate a guessed list of lifetime arguments. + // Basically it is the algorithm to transform guessNumber to + // base size(lifetimesUsedInArguments). + List guessedLifetimeArgs = new ArrayList(candidateLifetimeParams.size()); + for (int i = 0; i < exp; i++) { + int guessed = (int) ((guessNumber / (long) Math.pow(base, i)) % base); + guessedLifetimeArgs.add(lifetimesUsedInArguments.get(guessed)); + } + + // Now we can check the candidate with our guess + ValidCandidate vc = validateCandidate(candidateName, candidateType, candidateParameterTypes, + targetParameterTypes, candidateLifetimeParams, guessedLifetimeArgs, environment); + if (vc != null) { + validCandidates.add(vc); + } + } } /** @@ -2238,6 +2588,56 @@ private static List stripNominal(List types) { return r; } + /** + * Apply a lifetime substitution: Substitute all parameters in original by + * their arguments. + * + * @param lifetimeParameters + * @param lifetimeArguments + * @param original + * @return + */ + public static Nominal applySubstitution(List lifetimeParameters, List lifetimeArguments, Nominal original) { + if (lifetimeParameters.size() != lifetimeArguments.size()) { + throw new IllegalArgumentException("lifetime parameter/argument size mismatch!" + lifetimeParameters + " vs. " + lifetimeArguments); + } + Map substitution = buildSubstitution(lifetimeParameters, lifetimeArguments); + if (substitution.isEmpty()) { + return original; + } + return applySubstitution(substitution, original); + } + + private static Type applySubstitution(Map substitution, Type original) { + if (substitution.isEmpty()) { + return original; + } + return new LifetimeSubstitution(original, substitution).getType(); + } + + private static Nominal applySubstitution(Map substitution, Nominal original) { + if (substitution.isEmpty()) { + return original; + } + Type nominal = new LifetimeSubstitution(original.nominal(), substitution).getType(); + Type raw = new LifetimeSubstitution(original.raw(), substitution).getType(); + return Nominal.construct(nominal, raw); + } + + private static Map buildSubstitution(List lifetimeParameters, List lifetimeArguments) { + Map substitution = new HashMap(); + Iterator itP = lifetimeParameters.iterator(); + Iterator itA = lifetimeArguments.iterator(); + while (itP.hasNext()) { + String param = itP.next(); + String arg = itA.next(); + if (!arg.equals(param)) { + substitution.put(param, arg); + } + } + return substitution; + } + // ========================================================================= // ResolveAsName // ========================================================================= @@ -2595,12 +2995,15 @@ private int resolveAsType(SyntacticType type, Context context, ArrayList utParamTypes = ut.paramTypes; ArrayList utReturnTypes = ut.returnTypes; + ArrayList utContextLifetimes = ut.contextLifetimes; + ArrayList utLifetimeParameters = ut.lifetimeParameters; if (ut instanceof SyntacticType.Method) { myKind = Type.K_METHOD; @@ -2619,7 +3022,7 @@ private int resolveAsType(SyntacticType type, Context context, ArrayList(utContextLifetimes), utLifetimeParameters); } states.set(myIndex, new Automaton.State(myKind, myData, myDeterministic, myChildren)); @@ -3247,22 +3650,22 @@ private Environment addDeclaredParameter(WhileyFile.Parameter parameter, Environ // ========================================================================= // Check t1 :> t2 - private void checkIsSubtype(Nominal t1, Nominal t2, SyntacticElement elem) { - if (!Type.isSubtype(t1.raw(), t2.raw())) { + private void checkIsSubtype(Nominal t1, Nominal t2, SyntacticElement elem, Environment environment) { + if (!Type.isSubtype(t1.raw(), t2.raw(), environment.getLifetimeRelation())) { syntaxError(errorMessage(SUBTYPE_ERROR, t1.nominal(), t2.nominal()), filename, elem); } } - private void checkIsSubtype(Nominal t1, Expr t2) { - if (!Type.isSubtype(t1.raw(), t2.result().raw())) { + private void checkIsSubtype(Nominal t1, Expr t2, Environment environment) { + if (!Type.isSubtype(t1.raw(), t2.result().raw(), environment.getLifetimeRelation())) { // We use the nominal type for error reporting, since this includes // more helpful names. syntaxError(errorMessage(SUBTYPE_ERROR, t1.nominal(), t2.result().nominal()), filename, t2); } } - private void checkIsSubtype(Type t1, Expr t2) { - if (!Type.isSubtype(t1, t2.result().raw())) { + private void checkIsSubtype(Type t1, Expr t2, Environment environment) { + if (!Type.isSubtype(t1, t2.result().raw(), environment.getLifetimeRelation())) { // We use the nominal type for error reporting, since this includes // more helpful names. syntaxError(errorMessage(SUBTYPE_ERROR, t1, t2.result().nominal()), filename, t2); @@ -3270,22 +3673,22 @@ private void checkIsSubtype(Type t1, Expr t2) { } // Check t1 :> t2 - private void checkIsSubtype(Nominal t1, Nominal t2, SyntacticElement elem, Context context) { - if (!Type.isSubtype(t1.raw(), t2.raw())) { + private void checkIsSubtype(Nominal t1, Nominal t2, SyntacticElement elem, Context context, Environment environment) { + if (!Type.isSubtype(t1.raw(), t2.raw(), environment.getLifetimeRelation())) { syntaxError(errorMessage(SUBTYPE_ERROR, t1.nominal(), t2.nominal()), context, elem); } } - private void checkIsSubtype(Nominal t1, Expr t2, Context context) { - if (!Type.isSubtype(t1.raw(), t2.result().raw())) { + private void checkIsSubtype(Nominal t1, Expr t2, Context context, Environment environment) { + if (!Type.isSubtype(t1.raw(), t2.result().raw(), environment.getLifetimeRelation())) { // We use the nominal type for error reporting, since this includes // more helpful names. syntaxError(errorMessage(SUBTYPE_ERROR, t1.nominal(), t2.result().nominal()), context, t2); } } - private void checkIsSubtype(Type t1, Expr t2, Context context) { - if (!Type.isSubtype(t1, t2.result().raw())) { + private void checkIsSubtype(Type t1, Expr t2, Context context, Environment environment) { + if (!Type.isSubtype(t1, t2.result().raw(), environment.getLifetimeRelation())) { // We use the nominal type for error reporting, since this includes // more helpful names. syntaxError(errorMessage(SUBTYPE_ERROR, t1, t2.result().nominal()), context, t2); @@ -3293,10 +3696,10 @@ private void checkIsSubtype(Type t1, Expr t2, Context context) { } // Check t1 <: t2 or t1 <: t3 ... - private void checkSuptypes(Expr e, Context context, Nominal... types) { + private void checkSuptypes(Expr e, Context context, Environment environment, Nominal... types) { Nominal t1 = e.result(); for (Nominal t : types) { - if (Type.isSubtype(t.raw(), t1.raw())) { + if (Type.isSubtype(t.raw(), t1.raw(), environment.getLifetimeRelation())) { return; // OK } } @@ -3357,6 +3760,23 @@ private static final class Environment { */ private int count; // refCount + /** + * Whether we are currently inside a Lambda body + */ + private boolean inLambda; + + /** + * The lifetimes that are allowed to be dereferenced in a lambda body. + * These are lifetime parameters to the lambda expression and declared context lifetimes. + */ + private final HashSet lambdaLifetimes; + + /** + * The lifetime relation remembers how lifetimes are ordered (they are + * in a partial order). + */ + private final LifetimeRelation lifetimeRelation; + /** * Construct an empty environment. Initially the reference count is 1. */ @@ -3364,6 +3784,9 @@ public Environment() { count = 1; currentTypes = new HashMap(); declaredTypes = new HashMap(); + inLambda = false; + lambdaLifetimes = new HashSet(); + lifetimeRelation = new LifetimeRelation(); } /** @@ -3374,6 +3797,9 @@ private Environment(Environment environment) { count = 1; this.currentTypes = (HashMap) environment.currentTypes.clone(); this.declaredTypes = (HashMap) environment.declaredTypes.clone(); + inLambda = environment.inLambda; + lambdaLifetimes = (HashSet) environment.lambdaLifetimes.clone(); + lifetimeRelation = new LifetimeRelation(environment.lifetimeRelation); } /** @@ -3437,6 +3863,7 @@ public Set keySet() { * association. */ public Environment declare(String variable, Nominal declared, Nominal initial) { + // TODO: check that lifetimes and variables are disjoint if (declaredTypes.containsKey(variable)) { throw new RuntimeException("Variable already declared - " + variable); } @@ -3453,6 +3880,77 @@ public Environment declare(String variable, Nominal declared, Nominal initial) { } } + /** + * Declare lifetime parameters for a method. In the case that this + * environment has a reference count of 1, then an "in place" update is + * performed. Otherwise, a fresh copy of this environment is returned + * with the given variable associated with the given type, whilst this + * environment is unchanged. + * + * @param lifetimeParameters + * @return An updated version of the environment which contains the + * lifetime parameters. + */ + public Environment declareLifetimeParameters(List lifetimeParameters) { + // TODO: check duplicated variable/lifetime names + if (count == 1) { + this.lifetimeRelation.addParameters(lifetimeParameters); + return this; + } else { + Environment nenv = new Environment(this); + nenv.lifetimeRelation.addParameters(lifetimeParameters); + count--; + return nenv; + } + } + + /** + * Declare a lifetime for a named block. In the case that this + * environment has a reference count of 1, then an "in place" update is + * performed. Otherwise, a fresh copy of this environment is returned + * with the given variable associated with the given type, whilst this + * environment is unchanged. + * + * @param lifetime + * @return An updated version of the environment which contains the + * named block. + */ + public Environment startNamedBlock(String lifetime) { + // TODO: check duplicated variable/lifetime names + if (count == 1) { + this.lifetimeRelation.startNamedBlock(lifetime); + return this; + } else { + Environment nenv = new Environment(this); + nenv.lifetimeRelation.startNamedBlock(lifetime); + count--; + return nenv; + } + } + + /** + * End the last named block, i.e. remove its declared lifetime. In the + * case that this environment has a reference count of 1, then an + * "in place" update is performed. Otherwise, a fresh copy of this + * environment is returned with the given variable associated with the + * given type, whilst this environment is unchanged. + * + * @param lifetime + * @return An updated version of the environment without the given named + * block. + */ + public Environment endNamedBlock(String lifetime) { + if (count == 1) { + this.lifetimeRelation.endNamedBlock(lifetime); + return this; + } else { + Environment nenv = new Environment(this); + nenv.lifetimeRelation.endNamedBlock(lifetime); + count--; + return nenv; + } + } + /** * Update the current type of a given variable. If that variable already * had a current type, then this is overwritten. In the case that this @@ -3509,6 +4007,46 @@ public Environment remove(String key) { } } + /** + * Create a fresh copy of this environment, but set the lambda flag and + * remember the given context lifetimes and lifetime parameters. + * + * @param contextLifetimes + * the declared context lifetimes + * @param lifetimeParameters + * The lifetime names that are allowed to be dereferenced + * inside the lambda. + */ + public Environment startLambda(Collection contextLifetimes, Collection lifetimeParameters) { + Environment nenv = new Environment(this); + nenv.inLambda = true; + nenv.lambdaLifetimes.clear(); + nenv.lambdaLifetimes.addAll(contextLifetimes); + nenv.lambdaLifetimes.addAll(lifetimeParameters); + return nenv; + } + + /** + * Check whether we are allowed to dereference the given lifetime. + * Inside a lambda, only "*", the declared context lifetimes and the + * lifetime parameters can be dereferenced. + * + * @param lifetime + * @return + */ + public boolean canDereferenceLifetime(String lifetime) { + return !inLambda || lifetime.equals("*") || lambdaLifetimes.contains(lifetime); + } + + /** + * Get the current lifetime relation. + * + * @return + */ + public LifetimeRelation getLifetimeRelation() { + return this.lifetimeRelation; + } + /** * Merge a given environment with this environment to produce an * environment representing their join. Only variables from a given set @@ -3546,6 +4084,7 @@ public final Environment merge(Set declared, Environment env) { Nominal rhs_t = env.getCurrentType(variable); result.declare(variable, this.getDeclaredType(variable), Nominal.Union(lhs_t, rhs_t)); } + result.lifetimeRelation.replaceWithMerge(this.lifetimeRelation, env.lifetimeRelation); return result; } @@ -3572,13 +4111,14 @@ public String toString() { } public int hashCode() { - return currentTypes.hashCode(); + return 31 * currentTypes.hashCode() + lambdaLifetimes.hashCode(); } public boolean equals(Object o) { if (o instanceof Environment) { Environment r = (Environment) o; - return currentTypes.equals(r.currentTypes); + return currentTypes.equals(r.currentTypes) + && lambdaLifetimes.equals(r.lambdaLifetimes); } return false; } diff --git a/modules/wyc/src/wyc/io/WhileyFileLexer.java b/modules/wyc/src/wyc/io/WhileyFileLexer.java index 12cf696da0..df0379ddea 100755 --- a/modules/wyc/src/wyc/io/WhileyFileLexer.java +++ b/modules/wyc/src/wyc/io/WhileyFileLexer.java @@ -563,6 +563,8 @@ private void syntaxError(String msg, int index) { put("export", Token.Kind.Export); put("method", Token.Kind.Method); put("package", Token.Kind.Package); + // lifetimes + put("this", Token.Kind.This); } }; @@ -627,6 +629,8 @@ public enum Kind { Export("export"), Function("function"), Method("method"), + // Lifetimes + This("this"), // Expressions All("all"), No("no"), diff --git a/modules/wyc/src/wyc/io/WhileyFileParser.java b/modules/wyc/src/wyc/io/WhileyFileParser.java index be2b94c3f4..28ab0955c3 100644 --- a/modules/wyc/src/wyc/io/WhileyFileParser.java +++ b/modules/wyc/src/wyc/io/WhileyFileParser.java @@ -36,8 +36,6 @@ import java.util.List; import java.util.Set; -import com.sun.org.apache.bcel.internal.Constants; - import wyc.lang.*; import wyc.lang.Expr.ConstantAccess; import wyc.io.WhileyFileLexer.Token; @@ -154,7 +152,7 @@ private void parseImportDeclaration(WhileyFile wf) { // First, parse "from" usage (if applicable) Token token = tryAndMatch(true, Identifier, Star); if (token == null) { - syntaxError("expected identifier or '*' here", token); + syntaxError("expected identifier or '*' here", tokens.get(index)); } String name = token.text; // NOTE: we don't specify "from" as a keyword because this prevents it @@ -278,16 +276,22 @@ private void parseFunctionOrMethodDeclaration(WhileyFile wf, List modifiers, boolean isFunction) { int start = index; + EnclosingScope scope = new EnclosingScope(); + List lifetimeParameters; + if (isFunction) { match(Function); + lifetimeParameters = Collections.emptyList(); } else { match(Method); + + // Lifetime parameters + lifetimeParameters = parseOptionalLifetimeParameters(scope); } Token name = match(Identifier); // Parse function or method parameters - EnclosingScope scope = new EnclosingScope(); List parameters = parseParameters(wf,scope); // Parse (optional) return type @@ -334,6 +338,7 @@ private void parseFunctionOrMethodDeclaration(WhileyFile wf, match(Colon); end = index; matchEndLine(); + scope.declareThisLifetime(); stmts = parseBlock(wf, scope, false); } @@ -342,8 +347,8 @@ private void parseFunctionOrMethodDeclaration(WhileyFile wf, declaration = wf.new Function(modifiers, name.text, returns, parameters, requires, ensures, stmts, sourceAttr(start, end - 1)); } else { - declaration = wf.new Method(modifiers, name.text, returns, parameters, requires, ensures, stmts, - sourceAttr(start, end - 1)); + declaration = wf.new Method(modifiers, name.text, returns, parameters, + lifetimeParameters, requires, ensures, stmts, sourceAttr(start, end - 1)); } wf.add(declaration); } @@ -358,13 +363,9 @@ public List parseParameters(WhileyFile wf, EnclosingScope scope) { } firstTime = false; int pStart = index; - Pair p = parseMixedType(); + Pair p = parseMixedType(scope); Token id = p.second(); - if (scope.contains(id.text)) { - syntaxError("parameter already declared", id); - } else { - scope.add(id.text); - } + scope.declareVariable(id); parameters.add(wf.new Parameter(p.first(), id.text, sourceAttr( pStart, index - 1))); } @@ -390,17 +391,13 @@ public Parameter parseOptionalParameter(WhileyFile wf, EnclosingScope scope) { SyntacticType type; String name; if(tryAndMatch(true,LeftBrace) != null) { - Pair p = parseMixedType(); + Pair p = parseMixedType(scope); type = p.first(); - name = p.second().text; - if (scope.contains(name)) { - syntaxError("parameter already declared",p.second()); - } else { - scope.add(name); - } + name = p.second().text; + scope.declareVariable(p.second()); match(RightBrace); } else { - type = parseType(); + type = parseType(scope); name = null; } return wf.new Parameter(type, name, sourceAttr(start, index - 1)); @@ -646,7 +643,9 @@ private Stmt parseStatement(WhileyFile wf, EnclosingScope scope) { } // At this point, we have three possibilities remaining: variable - // declaration, invocation or assignment. To disambiguate these, we + // declaration, invocation, assignment, or a named block. + // The latter one can be detected easily as it is just an identifier + // followed by a colon. To disambiguate the remaining cases, we // first determine whether or not what follows *must* be parsed as a // type (i.e. parsing it as an expression would fail). If so, then it // must be a variable declaration that follows. Otherwise, it can still @@ -658,8 +657,8 @@ private Stmt parseStatement(WhileyFile wf, EnclosingScope scope) { /** * A headless statement is one which has no identifying keyword. The set of - * headless statements include assignments, invocations and variable - * declarations. + * headless statements include assignments, invocations, variable + * declarations and named blocks. * * @param wf * @param scope @@ -670,7 +669,25 @@ private Stmt parseStatement(WhileyFile wf, EnclosingScope scope) { */ private Stmt parseHeadlessStatement(WhileyFile wf, EnclosingScope scope) { int start = index; - SyntacticType type = parseDefiniteType(); + + // See if it is a named block + Token blockName = tryAndMatch(true, Identifier); + if (blockName != null) { + if (tryAndMatch(true, Colon) != null && isAtEOL()) { + int end = index; + matchEndLine(); + scope = scope.newEnclosingScope(); + scope.declareLifetime(blockName); + + List body = parseBlock(wf, scope, false); + return new Stmt.NamedBlock(blockName.text, body, sourceAttr(start, end - 1)); + } else { + index = start; // backtrack + } + } + + // Remaining cases: assignments, invocations and variable declarations + SyntacticType type = parseDefiniteType(scope); if (type == null) { // Can still be a variable declaration, assignment or invocation. @@ -698,7 +715,7 @@ private Stmt parseHeadlessStatement(WhileyFile wf, EnclosingScope scope) { // Therefore, we backtrack and parse the expression again as a // type. index = start; // backtrack - type = parseType(); + type = parseType(scope); } } // Must be a variable declaration here. @@ -738,11 +755,7 @@ private Stmt.VariableDeclaration parseVariableDeclaration(int start, // Ensure at least one variable is defined by this pattern. // Check that declared variables are not already defined. - if (scope.contains(parameter.name)) { - syntaxError("variable already declared", parameter); - } else { - - } + scope.checkNameAvailable(parameter); // A variable declaration may optionally be assigned an initialiser // expression. @@ -756,7 +769,7 @@ private Stmt.VariableDeclaration parseVariableDeclaration(int start, // Finally, register the new variable in the enclosing scope. This // should be done after parsing the initialiser expression to prevent it // from referring to this variable. - scope.add(parameter.name); + scope.declareVariable(parameter); // Done. return new Stmt.VariableDeclaration(parameter, initialiser, sourceAttr( start, end - 1)); @@ -1887,7 +1900,7 @@ private Expr parseConditionExpression(WhileyFile wf, bop = Expr.BOp.NEQ; break; case Is: - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); Expr.TypeVal rhs = new Expr.TypeVal(type, sourceAttr(start, index - 1)); return new Expr.BinOp(Expr.BOp.IS, lhs, rhs, sourceAttr(start, @@ -1968,16 +1981,13 @@ private Expr parseQuantifierExpression(Token lookahead, WhileyFile wf, } firstTime = false; Token id = match(Identifier); - if (scope.contains(id.text)) { - // It is already defined which is a syntax error - syntaxError("variable already declared", id); - } + scope.checkNameAvailable(id); match(In); Expr lhs = parseAdditiveExpression(wf, scope, terminated); match(DotDot); Expr rhs = parseAdditiveExpression(wf, scope, terminated); srcs.add(new Triple(id.text, lhs, rhs)); - scope.add(id.text); + scope.declareVariable(id); } while (eventuallyMatch(VerticalBar) == null); // Parse condition over source variables @@ -2278,7 +2288,32 @@ private Expr parseAccessExpression(WhileyFile wf, // is not a declared variable name. Path.ID id = parsePossiblePathID(lhs, scope); + // First we have to see if it is a method invocation. We can + // have optional lifetime arguments in angle brackets. + boolean isInvocation = false; + List lifetimeArguments = null; if (tryAndMatch(terminated, LeftBrace) != null) { + isInvocation = true; + } else if (lookaheadSequence(terminated, LeftAngle)) { + // This one is a little tricky, as we need some lookahead + // effort. We want to see whether it is a method invocation with + // lifetime arguments. But "Identifier < ..." can also be a + // boolean expression! + int oldindex = index; + match(LeftAngle); + Token lifetime = tryAndMatch(terminated, RightAngle, Identifier, This, Star); + if (lifetime != null && ( + lifetime.kind != Identifier // then it's definitely a lifetime + || scope.isLifetime(lifetime.text))) { + isInvocation = true; + index--; // don't forget the first argument! + lifetimeArguments = parseLifetimeArguments(wf, scope); + match(LeftBrace); + } else { + index = oldindex; // backtrack + } + } + if (isInvocation) { // This indicates a direct or indirect invocation. First, // parse arguments to invocation ArrayList arguments = parseInvocationArguments(wf,scope); @@ -2288,11 +2323,11 @@ private Expr parseAccessExpression(WhileyFile wf, lhs = new Expr.FieldAccess(lhs, name, sourceAttr( start, index - 1)); lhs = new Expr.AbstractIndirectInvoke(lhs, arguments, - sourceAttr(start, index - 1)); + lifetimeArguments, sourceAttr(start, index - 1)); } else { // This indicates we have an direct invocation lhs = new Expr.AbstractInvoke(name, id, arguments, - sourceAttr(start, index - 1)); + lifetimeArguments, sourceAttr(start, index - 1)); } } else if(id != null) { @@ -2378,13 +2413,38 @@ private Expr parseTermExpression(WhileyFile wf, case LeftBrace: return parseBracketedExpression(wf, scope, terminated); case New: + case This: return parseNewExpression(wf, scope, terminated); case Identifier: match(Identifier); if (tryAndMatch(terminated, LeftBrace) != null) { return parseInvokeExpression(wf, scope, start, token, - terminated); - } else if (scope.contains(token.text)) { + terminated, null); + } else if (lookaheadSequence(terminated, Colon, New)) { + // Identifier is lifetime name in "new" expression + index = start; + return parseNewExpression(wf, scope, terminated); + } else if (lookaheadSequence(terminated, LeftAngle)) { + // This one is a little tricky, as we need some lookahead + // effort. We want to see whether it is a method invocation with + // lifetime arguments. But "Identifier < ..." can also be a + // boolean expression! + int oldindex = index; + match(LeftAngle); + Token lifetime = tryAndMatch(terminated, RightAngle, Identifier, This, Star); + if (lifetime != null && ( + lifetime.kind != Identifier // then it's definitely a lifetime + || scope.isLifetime(lifetime.text))) { + index--; // don't forget the first argument! + List lifetimeArguments = parseLifetimeArguments(wf, scope); + match(LeftBrace); + return parseInvokeExpression( + wf, scope, start, token, terminated, lifetimeArguments); + } else { + index = oldindex; // backtrack + } + } // no else if, in case the former one didn't return + if (scope.isVariable(token.text)) { // Signals a local variable access return new Expr.LocalVariable(token.text, sourceAttr(start, index - 1)); @@ -2436,6 +2496,10 @@ private Expr parseTermExpression(WhileyFile wf, case Shreak: return parseLogicalNotExpression(wf, scope, terminated); case Star: + if (lookaheadSequence(terminated, Star, Colon, New)) { + // Star is default lifetime + return parseNewExpression(wf, scope, terminated); + } return parseDereferenceExpression(wf, scope, terminated); case Tilde: return parseBitwiseComplementExpression(wf, scope, terminated); @@ -2534,7 +2598,7 @@ private Expr parseBracketedExpression(WhileyFile wf, // "(nat,nat)" could either be a tuple type (if "nat" is a type) or a // tuple expression (if "nat" is a variable or constant). - SyntacticType t = parseDefiniteType(); + SyntacticType t = parseDefiniteType(scope); if (t != null) { // At this point, it's looking likely that we have a cast. However, @@ -2594,7 +2658,7 @@ private Expr parseBracketedExpression(WhileyFile wf, // Ok, this must be cast so back tract and reparse // expression as a type. index = start; // backtrack - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); // Now, parse cast expression e = parseExpression(wf, scope, terminated); return new Expr.Cast(type, e, sourceAttr(start, index - 1)); @@ -2822,6 +2886,7 @@ private Expr parseRecordExpression(WhileyFile wf, * 
 	 * TermExpr::= ...
 	 *                 |  "new" Expr
+	 *                 |  Lifetime ":" "new" Identifier Expr
 	 *
* * @param wf @@ -2849,9 +2914,21 @@ private Expr parseRecordExpression(WhileyFile wf, private Expr parseNewExpression(WhileyFile wf, EnclosingScope scope, boolean terminated) { int start = index; + + // try to match a lifetime + String lifetime; + Token lifetimeIdentifier = tryAndMatch(terminated, Identifier, This, Star); + if (lifetimeIdentifier != null) { + scope.mustBeLifetime(lifetimeIdentifier); + lifetime = lifetimeIdentifier.text; + match(Colon); + } else { + lifetime = "*"; + } + match(New); Expr e = parseExpression(wf, scope, terminated); - return new Expr.New(e, sourceAttr(start, index - 1)); + return new Expr.New(e, lifetime, sourceAttr(start, index - 1)); } /** @@ -2970,23 +3047,23 @@ private Expr parseNegationExpression(WhileyFile wf, * @return */ private Expr parseInvokeExpression(WhileyFile wf, EnclosingScope scope, int start, Token name, - boolean terminated) { + boolean terminated, List lifetimeArguments) { // First, parse the arguments to this invocation. ArrayList args = parseInvocationArguments(wf, scope); // Second, determine what kind of invocation we have. If the name of the // method is a local variable, then it must be an indirect invocation on // this variable. - if (scope.contains(name.text)) { + if (scope.isVariable(name.text)) { // indirect invocation on local variable Expr.LocalVariable lv = new Expr.LocalVariable(name.text, sourceAttr(start, start)); - return new Expr.AbstractIndirectInvoke(lv, args, sourceAttr(start, - index - 1)); + return new Expr.AbstractIndirectInvoke(lv, args, lifetimeArguments, + sourceAttr(start, index - 1)); } else { // unqualified direct invocation - return new Expr.AbstractInvoke(name.text, null, args, sourceAttr( - start, index - 1)); + return new Expr.AbstractInvoke(name.text, null, args, lifetimeArguments, + sourceAttr(start, index - 1)); } } @@ -3046,6 +3123,39 @@ private ArrayList parseInvocationArguments(WhileyFile wf, return args; } + /** + * Parse a sequence of lifetime arguments separated by commas that ends in a + * right-angle: + * + * 
+	 * LifetimeArguments ::= [ Lifetime (',' Lifetime)* ] '>'
+	 *
+ * + * Note, when this function is called we're assuming the left angle was + * already parsed. + * + * @param wf + * @param scope + * @return + */ + private ArrayList parseLifetimeArguments(WhileyFile wf, EnclosingScope scope) { + boolean firstTime = true; + ArrayList lifetimeArgs = new ArrayList(); + while (eventuallyMatch(RightAngle) == null) { + if (!firstTime) { + match(Comma); + } else { + firstTime = false; + } + + // termindated by '>' + String lifetime = parseLifetime(scope, true); + + lifetimeArgs.add(lifetime); + } + return lifetimeArgs; + } + /** * Parse a logical not expression, which has the form: * @@ -3120,8 +3230,10 @@ private Expr parseDereferenceExpression(WhileyFile wf, * * 
 	 * TermExpr::= ...
-	 *                 | '&' '(' [Type Identifier (',' Type Identifier)*] '->' Expr ')'
-	 *                 | '&' Identifier [ '(' Type Identifier (',' Type Identifier)* ')']
+	 *                 | '&' [ '[' [ Lifetime   (',' Lifetime  )* ] ']' ]
+	 *                       [ '<' [ Identifier (',' Identifier)* ] '>' ]
+	 *                   '(' [Type Identifier (',' Type Identifier)*] '->' Expr ')'
+	 *                 | '&' Identifier [ '(' Type (',' Type)* ')']
 	 *
* * Disambiguating these two forms is relatively straightforward, and we just @@ -3153,7 +3265,7 @@ private Expr parseLambdaOrAddressExpression(WhileyFile wf, EnclosingScope scope, boolean terminated) { int start = index; match(Ampersand); - if (tryAndMatch(terminated, LeftBrace) != null) { + if (tryAndMatch(terminated, LeftBrace, LeftSquare, LeftAngle) != null) { index = start; // backtrack return parseLambdaExpression(wf, scope, terminated); } else { @@ -3167,7 +3279,9 @@ private Expr parseLambdaOrAddressExpression(WhileyFile wf, * * 
 	 * TermExpr::= ...
-	 *                 |  '&' '(' [Type Identifier (',' Type Identifier)*] '->' Expr ')'
+	 *                 | '&' [ '[' [ Lifetime   (',' Lifetime  )* ] ']' ]
+	 *                       [ '<' [ Identifier (',' Identifier)* ] '>' ]
+	 *                   '(' [Type Identifier (',' Type Identifier)*] '->' Expr ')'
 	 *
* * @param wf @@ -3196,11 +3310,21 @@ private Expr parseLambdaExpression(WhileyFile wf, EnclosingScope scope, boolean terminated) { int start = index; match(Ampersand); + + // First parse the context lifetimes with the original scope + Set contextLifetimes = parseOptionalContextLifetimes(scope); + + // Now we create a new scope for this lambda expression. + // It keeps all variables but only the given context lifetimes. + // But it keeps all unavailable names, i.e. unaccessible lifetimes + // from the outer scope cannot be redeclared. + scope = scope.newEnclosingScope(contextLifetimes); + + // Parse the optional lifetime parameters + List lifetimeParameters = parseOptionalLifetimeParameters(scope); + match(LeftBrace); ArrayList parameters = new ArrayList(); - // Clone the environment so we can update it with those declared - // parameters. - scope = scope.newEnclosingScope(); boolean firstTime = true; while (eventuallyMatch(MinusGreater) == null) { int p_start = index; @@ -3208,12 +3332,9 @@ private Expr parseLambdaExpression(WhileyFile wf, match(Comma); } firstTime = false; - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); Token id = match(Identifier); - if (scope.contains(id.text)) { - syntaxError("duplicate variable or parameter name", id); - } - scope.add(id.text); + scope.declareVariable(id); parameters.add(wf.new Parameter(type, id.text, sourceAttr(p_start, index - 1))); } @@ -3222,7 +3343,7 @@ private Expr parseLambdaExpression(WhileyFile wf, Expr body = parseExpression(wf, scope, true); match(RightBrace); - return new Expr.Lambda(parameters, body, sourceAttr(start, index - 1)); + return new Expr.Lambda(parameters, contextLifetimes, lifetimeParameters, body, sourceAttr(start, index - 1)); } /** @@ -3230,7 +3351,7 @@ private Expr parseLambdaExpression(WhileyFile wf, * * 
 	 * TermExpr::= ...
-	 *                 | '&' Identifier [ '(' Type Identifier (',' Type Identifier)* ')']
+	 *                 | '&' Identifier [ '(' Type (',' Type)* ')']
 	 *
* * @param wf @@ -3273,15 +3394,15 @@ private Expr parseAddressExpression(WhileyFile wf, match(Comma); } firstTime = false; - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); parameters.add(type); } return new Expr.AbstractFunctionOrMethod(id.text, parameters, - sourceAttr(start, index - 1)); + null, sourceAttr(start, index - 1)); } else { // No, parameters are not supplied. - return new Expr.AbstractFunctionOrMethod(id.text, null, sourceAttr( - start, index - 1)); + return new Expr.AbstractFunctionOrMethod(id.text, null, null, + sourceAttr(start, index - 1)); } } @@ -3330,10 +3451,10 @@ private Expr parseBitwiseComplementExpression(WhileyFile wf, * * @return An instance of SyntacticType or null. */ - public SyntacticType parseDefiniteType() { + public SyntacticType parseDefiniteType(EnclosingScope scope) { int start = index; // backtrack point try { - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); if (mustParseAsType(type)) { return type; } @@ -3393,6 +3514,12 @@ private boolean mustParseAsType(SyntacticType type) { return false; // always can be an expression } else if (type instanceof SyntacticType.Reference) { SyntacticType.Reference tt = (SyntacticType.Reference) type; + if (tt.lifetime.equals("this") || + tt.lifetime.equals("*") && tt.lifetimeWasExplicit) { + // &this and &* is not a valid expression because "this" is keyword + // &ident could also be an address expression + return true; + } return mustParseAsType(tt.element); } else if (type instanceof SyntacticType.Union) { SyntacticType.Union tt = (SyntacticType.Union) type; @@ -3487,7 +3614,7 @@ private boolean mustParseAsExpr(Expr e) { return false; // dead-code } } - + /** * Parse a top-level type, which is of the form: * @@ -3498,8 +3625,8 @@ private boolean mustParseAsExpr(Expr e) { * @see wyc.lang.SyntacticType.Tuple * @return */ - private SyntacticType parseType() { - return parseUnionType(); + private SyntacticType parseType(EnclosingScope scope) { + return parseUnionType(scope); } /** @@ -3511,9 +3638,9 @@ private SyntacticType parseType() { * * @return */ - private SyntacticType parseUnionType() { + private SyntacticType parseUnionType(EnclosingScope scope) { int start = index; - SyntacticType t = parseIntersectionType(); + SyntacticType t = parseIntersectionType(scope); // Now, attempt to look for union and/or intersection types if (tryAndMatch(true, VerticalBar) != null) { @@ -3521,7 +3648,7 @@ private SyntacticType parseUnionType() { ArrayList types = new ArrayList(); types.add(t); do { - types.add(parseIntersectionType()); + types.add(parseIntersectionType(scope)); } while (tryAndMatch(true, VerticalBar) != null); return new SyntacticType.Union(types, sourceAttr(start, index - 1)); } else { @@ -3538,9 +3665,9 @@ private SyntacticType parseUnionType() { * * @return */ - private SyntacticType parseIntersectionType() { + private SyntacticType parseIntersectionType(EnclosingScope scope) { int start = index; - SyntacticType t = parseArrayType(); + SyntacticType t = parseArrayType(scope); // Now, attempt to look for union and/or intersection types if (tryAndMatch(true, Ampersand) != null) { @@ -3548,7 +3675,7 @@ private SyntacticType parseIntersectionType() { ArrayList types = new ArrayList(); types.add(t); do { - types.add(parseArrayType()); + types.add(parseArrayType(scope)); } while (tryAndMatch(true, Ampersand) != null); return new SyntacticType.Intersection(types, sourceAttr(start, index - 1)); @@ -3566,9 +3693,9 @@ private SyntacticType parseIntersectionType() { * * @return */ - private SyntacticType parseArrayType() { + private SyntacticType parseArrayType(EnclosingScope scope) { int start = index; - SyntacticType element = parseBaseType(); + SyntacticType element = parseBaseType(scope); while (tryAndMatch(true, LeftSquare) != null) { match(RightSquare); @@ -3578,7 +3705,7 @@ private SyntacticType parseArrayType() { return element; } - private SyntacticType parseBaseType() { + private SyntacticType parseBaseType(EnclosingScope scope) { checkNotEof(); int start = index; Token token = tokens.get(index); @@ -3598,19 +3725,19 @@ private SyntacticType parseBaseType() { case Int: return new SyntacticType.Int(sourceAttr(start, index++)); case LeftBrace: - return parseBracketedType(); + return parseBracketedType(scope); case LeftCurly: - return parseRecordType(); + return parseRecordType(scope); case Shreak: - return parseNegationType(); + return parseNegationType(scope); case Ampersand: - return parseReferenceType(); + return parseReferenceType(scope); case Identifier: return parseNominalType(); case Function: - return parseFunctionOrMethodType(true); + return parseFunctionOrMethodType(true, scope); case Method: - return parseFunctionOrMethodType(false); + return parseFunctionOrMethodType(false, scope); default: syntaxError("unknown type encountered", token); return null; @@ -3626,10 +3753,10 @@ private SyntacticType parseBaseType() { * * @return */ - private SyntacticType parseNegationType() { + private SyntacticType parseNegationType(EnclosingScope scope) { int start = index; match(Shreak); - SyntacticType element = parseArrayType(); + SyntacticType element = parseArrayType(scope); return new SyntacticType.Negation(element, sourceAttr(start, index - 1)); } @@ -3638,18 +3765,57 @@ private SyntacticType parseNegationType() { * * 
 	 * ReferenceType ::= '&' Type
+	 *                 | '&' Lifetime ':' Type
+	 *      Lifetime ::= Identifier | 'this' | '*'
 	 *
* * @return */ - private SyntacticType parseReferenceType() { + private SyntacticType parseReferenceType(EnclosingScope scope) { int start = index; match(Ampersand); - SyntacticType element = parseArrayType(); - return new SyntacticType.Reference(element, - sourceAttr(start, index - 1)); + + // Try to parse an annotated lifetime + int backtrack = index; + Token lifetimeIdentifier = tryAndMatch(true, Identifier, This, Star); + if (lifetimeIdentifier != null) { + // We cannot allow a newline after the colon, as it would + // unintentionally match a return type that happens to be reference + // type without lifetime annotation (return type in method signature + // is always followed by colon and newline). + if (tryAndMatch(true, Colon) != null && !isAtEOL()) { + // Now we know that there is an annotated lifetime + scope.mustBeLifetime(lifetimeIdentifier); + SyntacticType element = parseArrayType(scope); + return new SyntacticType.Reference(element, lifetimeIdentifier.text, true, + sourceAttr(start, index - 1)); + } + } + index = backtrack; + + SyntacticType element = parseArrayType(scope); + return new SyntacticType.Reference(element, "*", false, sourceAttr(start, index - 1)); } + /** + * Parse a currently declared lifetime. + * + * @return the matched lifetime name + */ + private String parseLifetime(EnclosingScope scope, boolean terminated) { + int next = terminated ? skipWhiteSpace(index) : skipLineSpace(index); + if (next < tokens.size()) { + Token t = tokens.get(next); + if (t.kind == Identifier || t.kind == This || t.kind == Star) { + index = next + 1; + scope.mustBeLifetime(t); + return t.text; + } + syntaxError("expectiong a lifetime identifier here", t); + } + syntaxError("unexpected end-of-file", tokens.get(next - 1)); + throw new RuntimeException("deadcode"); // dead-code + } /** * Parse a bracketed type, which is of the form: @@ -3660,10 +3826,10 @@ private SyntacticType parseReferenceType() { * * @return */ - private SyntacticType parseBracketedType() { + private SyntacticType parseBracketedType(EnclosingScope scope) { int start = index; match(LeftBrace); - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); match(RightBrace); return type; } @@ -3685,12 +3851,12 @@ private SyntacticType parseBracketedType() { * * @return */ - private SyntacticType parseRecordType() { + private SyntacticType parseRecordType(EnclosingScope scope) { int start = index; match(LeftCurly); HashMap types = new HashMap(); - Pair p = parseMixedType(); + Pair p = parseMixedType(scope); types.put(p.second().text, p.first()); // Now, we continue to parse any remaining fields. @@ -3704,7 +3870,7 @@ private SyntacticType parseRecordType() { isOpen = true; break; } else { - p = parseMixedType(); + p = parseMixedType(scope); Token id = p.second(); if (types.containsKey(id.text)) { syntaxError("duplicate record key", id); @@ -3755,18 +3921,25 @@ private SyntacticType parseNominalType() { * * @return */ - private SyntacticType parseFunctionOrMethodType(boolean isFunction) { + private SyntacticType parseFunctionOrMethodType(boolean isFunction, EnclosingScope scope) { int start = index; + List lifetimeParameters; + Set contextLifetimes; if (isFunction) { match(Function); + contextLifetimes = Collections.emptySet(); + lifetimeParameters = Collections.emptyList(); } else { match(Method); + contextLifetimes = parseOptionalContextLifetimes(scope); + scope = scope.newEnclosingScope(); + lifetimeParameters = parseOptionalLifetimeParameters(scope); } // First, parse the parameter type(s). - List paramTypes = parseParameterTypes(); - List returnTypes = Collections.EMPTY_LIST; + List paramTypes = parseParameterTypes(scope); + List returnTypes = Collections.emptyList(); // Second, parse the right arrow. if (isFunction) { @@ -3774,18 +3947,19 @@ private SyntacticType parseFunctionOrMethodType(boolean isFunction) { // nops) match(MinusGreater); // Third, parse the return types. - returnTypes = parseOptionalParameterTypes(); + returnTypes = parseOptionalParameterTypes(scope); } else if (tryAndMatch(true, MinusGreater) != null) { // Methods have an optional return type // Third, parse the return type - returnTypes = parseOptionalParameterTypes(); + returnTypes = parseOptionalParameterTypes(scope); } // Done if (isFunction) { return new SyntacticType.Function(returnTypes, paramTypes, sourceAttr(start, index - 1)); } else { - return new SyntacticType.Method(returnTypes, paramTypes, sourceAttr(start, index - 1)); + return new SyntacticType.Method(returnTypes, paramTypes, contextLifetimes, + lifetimeParameters, sourceAttr(start, index - 1)); } } @@ -3800,7 +3974,7 @@ private SyntacticType parseFunctionOrMethodType(boolean isFunction) { * * @return */ - private Pair parseMixedType() { + private Pair parseMixedType(EnclosingScope scope) { Token lookahead; int start = index; @@ -3808,21 +3982,32 @@ private Pair parseMixedType() { // At this point, we *might* have a mixed function / method type // definition. To disambiguate, we need to see whether an identifier // follows or not. + // Similar to normal method declarations, the lifetime parameters + // go before the method name. We do not allow to have context lifetimes + // for mixed method types. + List lifetimeParameters = Collections.emptyList(); + if (lookahead.kind == Method && tryAndMatch(true, LeftAngle) != null) { + // mixed method type with lifetime parameters + scope = scope.newEnclosingScope(); + lifetimeParameters = parseLifetimeParameters(scope); + } + + // Now try to parse the identifier Token id = tryAndMatch(true, Identifier); if (id != null) { // Yes, we have found a mixed function / method type definition. // Therefore, we continue to pass the remaining type parameters. - List paramTypes = parseParameterTypes(); - List returnTypes = Collections.EMPTY_LIST; + List paramTypes = parseParameterTypes(scope); + List returnTypes = Collections.emptyList(); if (lookahead.kind == Function) { // Functions require a return type (since otherwise they are // just nops) match(MinusGreater); // Third, parse the return type - returnTypes = parseOptionalParameterTypes(); + returnTypes = parseOptionalParameterTypes(scope); } else if (tryAndMatch(true, MinusGreater) != null) { // Third, parse the (optional) return type. Observe that // this is forced to be a @@ -3831,7 +4016,7 @@ private Pair parseMixedType() { // may be part of an enclosing record type and we must // disambiguate // this. - returnTypes = parseOptionalParameterTypes(); + returnTypes = parseOptionalParameterTypes(scope); } // Done @@ -3839,7 +4024,8 @@ private Pair parseMixedType() { if (lookahead.kind == Token.Kind.Function) { type = new SyntacticType.Function(returnTypes, paramTypes, sourceAttr(start, index - 1)); } else { - type = new SyntacticType.Method(returnTypes, paramTypes, sourceAttr(start, index - 1)); + type = new SyntacticType.Method(returnTypes, paramTypes, Collections.emptySet(), + lifetimeParameters, sourceAttr(start, index - 1)); } return new Pair(type, id); } else { @@ -3852,24 +4038,24 @@ private Pair parseMixedType() { // This is the normal case, where we expect an identifier to follow the // type. - SyntacticType type = parseType(); + SyntacticType type = parseType(scope); Token id = match(Identifier); return new Pair(type, id); } - public List parseOptionalParameterTypes() { + public List parseOptionalParameterTypes(EnclosingScope scope) { int next = skipWhiteSpace(index); if(next < tokens.size() && tokens.get(next).kind == LeftBrace) { - return parseParameterTypes(); + return parseParameterTypes(scope); } else { - SyntacticType t = parseType(); + SyntacticType t = parseType(scope); ArrayList rs = new ArrayList(); rs.add(t); return rs; } } - public List parseParameterTypes() { + public List parseParameterTypes(EnclosingScope scope) { ArrayList paramTypes = new ArrayList(); match(LeftBrace); @@ -3879,12 +4065,60 @@ public List parseParameterTypes() { match(Comma); } firstTime = false; - paramTypes.add(parseType()); + paramTypes.add(parseType(scope)); } return paramTypes; } - + + /** + * Attention: Enters the lifetime names to the passed scope! + * @param scope + * @return + */ + public List parseOptionalLifetimeParameters(EnclosingScope scope) { + if (tryAndMatch(true, LeftAngle) != null && tryAndMatch(true, RightAngle) == null) { + // The if above skips an empty list of identifiers "<>"! + return parseLifetimeParameters(scope); + } + return Collections.emptyList(); + } + + /** + * Attention: Enters the lifetime names to the passed scope! + * Assumes that '<' has already been matched. + * @param scope + * @return + */ + private List parseLifetimeParameters(EnclosingScope scope) { + List lifetimeParameters = new ArrayList(); + do { + Token lifetimeIdentifier = match(Identifier); + scope.declareLifetime(lifetimeIdentifier); + lifetimeParameters.add(lifetimeIdentifier.text); + } while (tryAndMatch(true, Comma) != null); + match(RightAngle); + return lifetimeParameters; + } + + + /** + * @param scope + * @return + */ + public Set parseOptionalContextLifetimes(EnclosingScope scope) { + if (tryAndMatch(true, LeftSquare) != null && tryAndMatch(true, RightSquare) == null) { + // The if above skips an empty list of identifiers "[]"! + Set contextLifetimes = new HashSet(); + do { + contextLifetimes.add(parseLifetime(scope, true)); + } while (tryAndMatch(true, Comma) != null); + match(RightSquare); + return contextLifetimes; + } + return Collections.emptySet(); + } + public boolean mustParseAsMixedType() { int start = index; if (tryAndMatch(true, Function, Method) != null @@ -4030,6 +4264,44 @@ private Token tryAndMatch(boolean terminated, Token.Kind... kinds) { return null; } + /** + * Attempt to match a given sequence of tokens in the given order, whilst + * ignoring any whitespace in between. Note that, in any case, the index + * will be unchanged! + * + * @param terminated + * Indicates whether or not this function should be concerned + * with new lines. The terminated flag indicates whether or not + * the current construct being parsed is known to be terminated. + * If so, then we don't need to worry about newlines and can + * greedily consume them (i.e. since we'll eventually run into + * the terminating symbol). + * @param kinds + * + * @return whether the sequence matches + */ + private boolean lookaheadSequence(boolean terminated, Token.Kind... kinds) { + int next = index; + for (Token.Kind k : kinds) { + next = terminated ? skipWhiteSpace(next) : skipLineSpace(next); + if (next >= tokens.size() || tokens.get(next++).kind != k) { + return false; + } + } + return true; + } + + /** + * Check whether the current index is, after skipping all line spaces, at + * the end of a line. This method does not change the state! + * + * @return whether index is at end of line + */ + private boolean isAtEOL() { + int next = skipLineSpace(index); + return next >= tokens.size() || tokens.get(next).kind == NewLine; + } + /** * Attempt to match a given token on the *same* line, whilst ignoring any * whitespace in between. Note that, in the case it fails to match, then the @@ -4399,7 +4671,7 @@ public boolean equivalent(Indent other) { * @author David J. Pearce * */ - private static class EnclosingScope { + private class EnclosingScope { /** * The indent level of the enclosing scope. */ @@ -4408,7 +4680,20 @@ private static class EnclosingScope { /** * The set of declared variables in the enclosing scope. */ - private final HashSet environment; + private final HashSet variables; + + /** + * The set of declared lifetimes in the enclosing scope. + */ + private final HashSet lifetimes; + + /** + * The set of all names that cannot be used for variables or lifetimes. + * They are either in the variables or lifetimes set, or a special lifetime, + * or they are unavailable because it is an unaccessible lifetime from + * an outer scope. + */ + private final HashSet unavailableNames; /** * A simple flag that tells us whether or not we are currently within a @@ -4419,13 +4704,22 @@ private static class EnclosingScope { public EnclosingScope() { this.indent = ROOT_INDENT; - this.environment = new HashSet(); + this.variables = new HashSet(); + this.lifetimes = new HashSet(); + this.unavailableNames = new HashSet(); this.inLoop = false; + + // prevent declaring these lifetimes + this.unavailableNames.add("*"); + this.unavailableNames.add("this"); } - private EnclosingScope(Indent indent, Set environment, boolean inLoop) { + private EnclosingScope(Indent indent, Set variables, Set lifetimes, + Set unavailableNames, boolean inLoop) { this.indent = indent; - this.environment = new HashSet(environment); + this.variables = new HashSet(variables); + this.lifetimes = new HashSet(lifetimes); + this.unavailableNames = new HashSet(unavailableNames); this.inLoop = inLoop; } @@ -4436,7 +4730,7 @@ public Indent getIndent() { public boolean isInLoop() { return inLoop; } - + /** * Check whether a given name corresponds to a declared variable in this * scope. @@ -4444,19 +4738,119 @@ public boolean isInLoop() { * @param name * @return */ - public boolean contains(String name) { - return environment.contains(name); + public boolean isVariable(String name) { + return this.variables.contains(name); } - + /** - * Declare a new variable in this scope. + * Check whether a given name corresponds to a declared lifetime in this + * scope. * * @param name + * @return */ - public void add(String name) { - environment.add(name); + public boolean isLifetime(String name) { + return name.equals("*") || this.lifetimes.contains(name); } - + + /** + * Checks that the given identifier is a declared lifetime. + * + * @param id + * @throws SyntaxError + * if the given identifier is not a lifetime + */ + public void mustBeLifetime(Token id) { + if (!this.isLifetime(id.text)) { + syntaxError("use of undeclared lifetime", id); + } + } + + /** + * Check whether a given name is available, i.e. can be declared. + * + * @param id + * identifier that holds the name to check + * @throws SyntaxError + * if the name is unavailable (already declared) + */ + public void checkNameAvailable(Token id) { + if (this.unavailableNames.contains(id.text)) { + // name is not available! + syntaxError("name already declared", id); + } + } + + /** + * Check whether a given name is available, i.e. can be declared. + * + * @param p + * parameter that holds the name to check + * @throws SyntaxError + * if the name is unavailable (already declared) + */ + public void checkNameAvailable(Parameter p) { + if (this.unavailableNames.contains(p.name)) { + // name is not available! + syntaxError("name already declared", p); + } + } + + /** + * Declare a new variable in this scope. + * + * @param id + * identifier that holds the name to declare + * @throws SyntaxError + * if the name is already declared + */ + public void declareVariable(Token id) { + if (!this.unavailableNames.add(id.text)) { + // name is not available! + syntaxError("name already declared", id); + } + this.variables.add(id.text); + } + + /** + * Declare a new variable in this scope. + * + * @param p + * parameter that holds the name to declare + * @throws SyntaxError + * if the name is already declared + */ + public void declareVariable(Parameter p) { + if (!this.unavailableNames.add(p.name)) { + // name is not available! + syntaxError("name already declared", p); + } + this.variables.add(p.name); + } + + /** + * Declare a new lifetime in this scope. + * + * @param id + * identifier that holds the name to declare + * @throws SyntaxError + * if the name is already declared + */ + public void declareLifetime(Token id) { + if (!this.unavailableNames.add(id.text)) { + // name is not available! + syntaxError("name already declared", id); + } + this.lifetimes.add(id.text); + } + + /** + * Make lifetime "this" available. + */ + public void declareThisLifetime() { + this.lifetimes.add("this"); + } + /** * Create a new enclosing scope in which variables can be declared which * are remain invisible to this enclosing scope. All variables declared @@ -4468,7 +4862,7 @@ public void add(String name) { * @return */ public EnclosingScope newEnclosingScope() { - return new EnclosingScope(indent,environment,inLoop); + return new EnclosingScope(indent,variables,lifetimes,unavailableNames,inLoop); } /** @@ -4482,7 +4876,7 @@ public EnclosingScope newEnclosingScope() { * @return */ public EnclosingScope newEnclosingScope(Indent indent) { - return new EnclosingScope(indent,environment,inLoop); + return new EnclosingScope(indent,variables,lifetimes,unavailableNames,inLoop); } /** @@ -4496,7 +4890,21 @@ public EnclosingScope newEnclosingScope(Indent indent) { * @return */ public EnclosingScope newEnclosingScope(Indent indent, boolean inLoop) { - return new EnclosingScope(indent,environment,inLoop); + return new EnclosingScope(indent,variables,lifetimes,unavailableNames,inLoop); + } + + /** + * Create a new enclosing scope in which variables can be declared which + * are remain invisible to this enclosing scope. All variables declared + * in this enclosing scope remain declared in the new enclosing scope. + * + * @param indent + * the indent level for the new scope + * + * @return + */ + public EnclosingScope newEnclosingScope(Set contextLifetimes) { + return new EnclosingScope(indent,variables,contextLifetimes,unavailableNames,false); } } } diff --git a/modules/wyc/src/wyc/io/WhileyFilePrinter.java b/modules/wyc/src/wyc/io/WhileyFilePrinter.java index c24e0fe2b1..f86cad3bc9 100644 --- a/modules/wyc/src/wyc/io/WhileyFilePrinter.java +++ b/modules/wyc/src/wyc/io/WhileyFilePrinter.java @@ -160,6 +160,8 @@ public void print(Stmt stmt, int indent) { print((Stmt.Skip) stmt); } else if(stmt instanceof Stmt.Switch) { print((Stmt.Switch) stmt, indent); + } else if(stmt instanceof Stmt.NamedBlock) { + print((Stmt.NamedBlock) stmt, indent); } else if(stmt instanceof Stmt.While) { print((Stmt.While) stmt, indent); } else if(stmt instanceof Stmt.VariableDeclaration) { @@ -255,6 +257,11 @@ public void print(Stmt.DoWhile s, int indent) { out.println(); } + public void print(Stmt.NamedBlock s, int indent) { + out.println(s.name + ":"); + print(s.body,indent+1); + } + public void print(Stmt.While s, int indent) { out.print("while "); print(s.condition); @@ -455,6 +462,18 @@ public void print(Expr.AbstractInvoke e) { out.print("."); } out.print(e.name); + if (!e.lifetimeArguments.isEmpty()) { + out.print("<"); + boolean firstTime = true; + for (String lifetime : e.lifetimeArguments) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print(">"); + } out.print("("); boolean firstTime = true; for(Expr i : e.arguments) { @@ -469,6 +488,18 @@ public void print(Expr.AbstractInvoke e) { public void print(Expr.IndirectFunctionCall e) { print(e.src); + if (!e.lifetimeArguments.isEmpty()) { + out.print("<"); + boolean firstTime = true; + for (String lifetime : e.lifetimeArguments) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print(">"); + } out.print("("); boolean firstTime = true; for(Expr i : e.arguments) { @@ -483,6 +514,18 @@ public void print(Expr.IndirectFunctionCall e) { public void print(Expr.IndirectMethodCall e) { print(e.src); + if (!e.lifetimeArguments.isEmpty()) { + out.print("<"); + boolean firstTime = true; + for (String lifetime : e.lifetimeArguments) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print(">"); + } out.print("("); boolean firstTime = true; for(Expr i : e.arguments) { @@ -571,7 +614,32 @@ public void print(Expr.AbstractFunctionOrMethod e) { } public void print(Expr.Lambda e) { - out.print("&("); + out.print("&"); + if (!e.contextLifetimes.isEmpty()) { + out.print("["); + boolean firstTime = true; + for (String lifetime : e.contextLifetimes) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print("]"); + } + if (!e.lifetimeParameters.isEmpty()) { + out.print("<"); + boolean firstTime = true; + for (String lifetime : e.lifetimeParameters) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print(">"); + } + out.print("("); boolean firstTime = true; for(WhileyFile.Parameter p : e.parameters) { if(!firstTime) { @@ -666,6 +734,30 @@ public void print(SyntacticType t) { } else { out.print("function "); } + if (!tt.contextLifetimes.isEmpty()) { + out.print("["); + boolean firstTime = true; + for (String lifetime : tt.contextLifetimes) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print("]"); + } + if (!tt.lifetimeParameters.isEmpty()) { + out.print("<"); + boolean firstTime = true; + for (String lifetime : tt.lifetimeParameters) { + if (!firstTime) { + out.print(", "); + } + firstTime = false; + out.print(lifetime); + } + out.print(">"); + } printParameterTypes(tt.paramTypes); out.print("->"); printParameterTypes(tt.returnTypes); diff --git a/modules/wyc/src/wyc/lang/Expr.java b/modules/wyc/src/wyc/lang/Expr.java index 17c43059d6..bd9e622173 100755 --- a/modules/wyc/src/wyc/lang/Expr.java +++ b/modules/wyc/src/wyc/lang/Expr.java @@ -27,6 +27,7 @@ import java.util.*; +import wyc.builder.FlowTypeChecker; import wyc.io.WhileyFileLexer; import wycc.lang.Attribute; import wycc.lang.NameID; @@ -207,9 +208,11 @@ public Nominal result() { public static class AbstractFunctionOrMethod extends SyntacticElement.Impl implements Expr { public final String name; public final ArrayList paramTypes; + public final ArrayList lifetimeParameters; public Nominal.FunctionOrMethod type; - public AbstractFunctionOrMethod(String name, Collection paramTypes, Attribute... attributes) { + public AbstractFunctionOrMethod(String name, Collection paramTypes, + Collection lifetimeParameters, Attribute... attributes) { super(attributes); this.name = name; if(paramTypes != null) { @@ -217,10 +220,16 @@ public AbstractFunctionOrMethod(String name, Collection paramType } else { this.paramTypes = null; } + if(lifetimeParameters != null) { + this.lifetimeParameters = new ArrayList(lifetimeParameters); + } else { + this.lifetimeParameters = null; + } } public AbstractFunctionOrMethod(String name, Collection paramTypes, + Collection lifetimeParameters, Collection attributes) { super(attributes); this.name = name; @@ -229,6 +238,11 @@ public AbstractFunctionOrMethod(String name, } else { this.paramTypes = null; } + if(lifetimeParameters != null) { + this.lifetimeParameters = new ArrayList(lifetimeParameters); + } else { + this.lifetimeParameters = null; + } } public Nominal.FunctionOrMethod result() { @@ -240,34 +254,40 @@ public static class FunctionOrMethod extends AbstractFunctionOrMethod { public final NameID nid; public FunctionOrMethod(NameID nid, Collection paramTypes, - Attribute... attributes) { - super(nid.name(), paramTypes, attributes); + Collection lifetimeParameters, Attribute... attributes) { + super(nid.name(), paramTypes, lifetimeParameters, attributes); this.nid = nid; } public FunctionOrMethod(NameID nid, Collection paramTypes, - Collection attributes) { - super(nid.name(), paramTypes, attributes); + Collection lifetimeParameters, Collection attributes) { + super(nid.name(), paramTypes, lifetimeParameters, attributes); this.nid = nid; } } public static class Lambda extends SyntacticElement.Impl implements Expr { public final ArrayList parameters; + public final HashSet contextLifetimes; + public final ArrayList lifetimeParameters; public Expr body; public Nominal.FunctionOrMethod type; - public Lambda(Collection parameters, Expr body, - Attribute... attributes) { + public Lambda(Collection parameters, Collection contextLifetimes, + Collection lifetimeParameters, Expr body, Attribute... attributes) { super(attributes); this.parameters = new ArrayList(parameters); + this.contextLifetimes = new HashSet(contextLifetimes); + this.lifetimeParameters = new ArrayList(lifetimeParameters); this.body = body; } - public Lambda(Collection parameters, Expr body, - Collection attributes) { + public Lambda(Collection parameters, Collection contextLifetimes, + Collection lifetimeParameters, Expr body, Collection attributes) { super(attributes); this.parameters = new ArrayList(parameters); + this.contextLifetimes = new HashSet(contextLifetimes); + this.lifetimeParameters = new ArrayList(lifetimeParameters); this.body = body; } @@ -564,22 +584,34 @@ public static class AbstractInvoke extends SyntacticElement.Impl implements Expr public final String name; public Path.ID qualification; public final ArrayList arguments; + public final ArrayList lifetimeArguments; public AbstractInvoke(String name, Path.ID receiver, - Collection arguments, Attribute... attributes) { + Collection arguments, Collection lifetimeArguments, + Attribute... attributes) { super(attributes); this.name = name; this.qualification = receiver; this.arguments = new ArrayList(arguments); + if (lifetimeArguments != null) { + this.lifetimeArguments = new ArrayList(lifetimeArguments); + } else { + this.lifetimeArguments = null; + } } public AbstractInvoke(String name, Path.ID receiver, - Collection arguments, + Collection arguments, Collection lifetimeArguments, Collection attributes) { super(attributes); this.name = name; this.qualification = receiver; this.arguments = new ArrayList(arguments); + if (lifetimeArguments != null) { + this.lifetimeArguments = new ArrayList(lifetimeArguments); + } else { + this.lifetimeArguments = null; + } } public Nominal result() { @@ -591,14 +623,14 @@ public static abstract class FunctionOrMethodCall extends AbstractInvoke impleme public final NameID nid; public FunctionOrMethodCall(NameID nid, Path.ID qualification, Collection arguments, - Attribute... attributes) { - super(nid.name(),qualification,arguments,attributes); + Collection lifetimeArguments, Attribute... attributes) { + super(nid.name(),qualification,arguments,lifetimeArguments,attributes); this.nid = nid; } public FunctionOrMethodCall(NameID nid, Path.ID qualification, Collection arguments, - Collection attributes) { - super(nid.name(),qualification,arguments,attributes); + Collection lifetimeArguments, Collection attributes) { + super(nid.name(),qualification,arguments,lifetimeArguments,attributes); this.nid = nid; } @@ -617,13 +649,13 @@ public static class MethodCall extends FunctionOrMethodCall { public Nominal.Method methodType; public MethodCall(NameID nid, Path.ID qualification, Collection arguments, - Attribute... attributes) { - super(nid,qualification,arguments,attributes); + Collection lifetimeArguments, Attribute... attributes) { + super(nid,qualification,arguments,lifetimeArguments,attributes); } public MethodCall(NameID nid, Path.ID qualification, Collection arguments, - Collection attributes) { - super(nid,qualification,arguments,attributes); + Collection lifetimeArguments, Collection attributes) { + super(nid,qualification,arguments,lifetimeArguments,attributes); } public Nominal.Method type() { @@ -632,7 +664,11 @@ public Nominal.Method type() { public Nominal result() { if (methodType.returns().size() == 1) { - return methodType.returns().get(0); + Nominal returnType = methodType.returns().get(0); + if (this.lifetimeArguments == null || this.lifetimeArguments.isEmpty()) { + return returnType; + } + return FlowTypeChecker.applySubstitution(methodType.raw().lifetimeParams(), this.lifetimeArguments, returnType); } else { throw new IllegalArgumentException("incorrect number of returns for function call"); } @@ -654,12 +690,12 @@ public static class FunctionCall extends FunctionOrMethodCall { public FunctionCall(NameID nid, Path.ID qualification, Collection arguments, Attribute... attributes) { - super(nid,qualification,arguments,attributes); + super(nid,qualification,arguments,Collections.emptyList(),attributes); } public FunctionCall(NameID nid, Path.ID qualification, Collection arguments, Collection attributes) { - super(nid,qualification,arguments,attributes); + super(nid,qualification,arguments,Collections.emptyList(),attributes); } public Nominal.Function type() { @@ -679,21 +715,26 @@ public static class AbstractIndirectInvoke extends SyntacticElement.Impl impleme Stmt { public Expr src; public final ArrayList arguments; + public final ArrayList lifetimeArguments; public AbstractIndirectInvoke(Expr src, Collection arguments, + Collection lifetimeArguments, Attribute... attributes) { super(attributes); this.src = src; this.arguments = new ArrayList(arguments); + this.lifetimeArguments = lifetimeArguments == null ? null : new ArrayList(lifetimeArguments); } public AbstractIndirectInvoke(Expr src, Collection arguments, + Collection lifetimeArguments, Collection attributes) { super(attributes); this.src = src; this.arguments = new ArrayList(arguments); + this.lifetimeArguments = lifetimeArguments == null ? null : new ArrayList(lifetimeArguments); } public Nominal result() { @@ -703,13 +744,13 @@ public Nominal result() { public static abstract class IndirectFunctionOrMethodCall extends AbstractIndirectInvoke implements Multi { public IndirectFunctionOrMethodCall(Expr src, Collection arguments, - Attribute... attributes) { - super(src,arguments,attributes); + Collection lifetimeArguments, Attribute... attributes) { + super(src,arguments,lifetimeArguments,attributes); } public IndirectFunctionOrMethodCall(Expr src, Collection arguments, - Collection attributes) { - super(src,arguments,attributes); + Collection lifetimeArguments, Collection attributes) { + super(src,arguments,lifetimeArguments,attributes); } public abstract Nominal.FunctionOrMethod type(); @@ -723,18 +764,22 @@ public static class IndirectMethodCall extends IndirectFunctionOrMethodCall { public Nominal.Method methodType; public IndirectMethodCall(Expr src, Collection arguments, - Attribute... attributes) { - super(src,arguments,attributes); + Collection lifetimeArguments, Attribute... attributes) { + super(src,arguments,lifetimeArguments,attributes); } public IndirectMethodCall(Expr src, Collection arguments, - Collection attributes) { - super(src,arguments,attributes); + Collection lifetimeArguments, Collection attributes) { + super(src,arguments,lifetimeArguments,attributes); } public Nominal result() { if(methodType.returns().size() == 1) { - return methodType.returns().get(0); + Nominal returnType = methodType.returns().get(0); + if (this.lifetimeArguments == null || this.lifetimeArguments.isEmpty()) { + return returnType; + } + return FlowTypeChecker.applySubstitution(methodType.raw().lifetimeParams(), this.lifetimeArguments, returnType); } else { throw new IllegalArgumentException("incorrect number of returns for indirect method call"); } @@ -750,12 +795,12 @@ public static class IndirectFunctionCall extends IndirectFunctionOrMethodCall { public IndirectFunctionCall(Expr src, Collection arguments, Attribute... attributes) { - super(src,arguments,attributes); + super(src,arguments,Collections.emptyList(),attributes); } public IndirectFunctionCall(Expr src, Collection arguments, Collection attributes) { - super(src,arguments,attributes); + super(src,arguments,Collections.emptyList(),attributes); } public Nominal result() { @@ -774,9 +819,11 @@ public Nominal.FunctionOrMethod type() { public static class New extends SyntacticElement.Impl implements Expr,Stmt { public Expr expr; public Nominal.Reference type; + public String lifetime; - public New(Expr expr, Attribute... attributes) { + public New(Expr expr, String lifetime, Attribute... attributes) { super(attributes); + this.lifetime = lifetime; this.expr = expr; } diff --git a/modules/wyc/src/wyc/lang/Nominal.java b/modules/wyc/src/wyc/lang/Nominal.java index 34ab1b19ed..b31f0d0585 100755 --- a/modules/wyc/src/wyc/lang/Nominal.java +++ b/modules/wyc/src/wyc/lang/Nominal.java @@ -56,9 +56,9 @@ public static Nominal intersect(Nominal lhs, Nominal rhs) { return Nominal.construct(nominal, raw); } - public static Reference Reference(Nominal element) { - Type.Reference nominal = Type.Reference(element.nominal()); - Type.Reference raw = Type.Reference(element.raw()); + public static Reference Reference(Nominal element, String lifetime) { + Type.Reference nominal = Type.Reference(element.nominal(), lifetime); + Type.Reference raw = Type.Reference(element.raw(), lifetime); return new Reference(nominal,raw); } diff --git a/modules/wyc/src/wyc/lang/Stmt.java b/modules/wyc/src/wyc/lang/Stmt.java index a7ac25abac..8fb618cbe9 100755 --- a/modules/wyc/src/wyc/lang/Stmt.java +++ b/modules/wyc/src/wyc/lang/Stmt.java @@ -260,6 +260,59 @@ public String toString() { } } + /** + * Represents a named block, which has the form: + * + * 
+	 * NamedBlcok ::= LifetimeIdentifier ':' NewLine Block
+	 *
+ * + * As an example: + * + * 
+	 * function sum():
+	 *   &this:int x = new:this x
+	 *   myblock:
+	 *     &myblock:int y = new:myblock y
+	 *
+ */ + public static final class NamedBlock extends SyntacticElement.Impl implements Stmt { + public final String name; + public final ArrayList body; + + /** + * Construct a named block from a given name and body of statements. + * + * @param name + * name of this named block. + * @param body + * non-null collection which contains zero or more + * statements. + * @param attributes + */ + public NamedBlock(String name, Collection body, Attribute... attributes) { + super(attributes); + this.name = name; + this.body = new ArrayList(body); + } + + /** + * Construct a named block from a given name and body of statements. + * + * @param name + * name of this named block. + * @param body + * non-null collection which contains zero or more + * statements. + * @param attributes + */ + public NamedBlock(String name, Collection body, Collection attributes) { + super(attributes); + this.name = name; + this.body = new ArrayList(body); + } + } + /** * Represents a while statement, which has the form: * diff --git a/modules/wyc/src/wyc/lang/SyntacticType.java b/modules/wyc/src/wyc/lang/SyntacticType.java index ff008fc97b..61e20fb393 100755 --- a/modules/wyc/src/wyc/lang/SyntacticType.java +++ b/modules/wyc/src/wyc/lang/SyntacticType.java @@ -291,8 +291,12 @@ public Intersection(ArrayList bounds, */ public static final class Reference extends SyntacticElement.Impl implements NonUnion { public final SyntacticType element; - public Reference(SyntacticType element, Attribute... attributes) { + public final String lifetime; + public final boolean lifetimeWasExplicit; + public Reference(SyntacticType element, String lifetime, boolean lifetimeWasExplicit, Attribute... attributes) { this.element = element; + this.lifetime = lifetime; + this.lifetimeWasExplicit = lifetimeWasExplicit; } } @@ -338,12 +342,16 @@ public abstract static class FunctionOrMethod extends SyntacticElement.Impl implements NonUnion { public final ArrayList returnTypes; public final ArrayList paramTypes; + public final ArrayList contextLifetimes; + public final ArrayList lifetimeParameters; public FunctionOrMethod(Collection returnTypes, Collection paramTypes, - Attribute... attributes) { + Collection contextLifetimes, Collection lifetimeParameters, Attribute... attributes) { super(attributes); this.returnTypes = new ArrayList(returnTypes); this.paramTypes = new ArrayList(paramTypes); + this.contextLifetimes = new ArrayList(contextLifetimes); + this.lifetimeParameters = new ArrayList(lifetimeParameters); for(SyntacticType t : paramTypes) { if(t == null) { throw new IllegalArgumentException("parameter cannot be null"); @@ -354,13 +362,20 @@ public FunctionOrMethod(Collection returnTypes, Collection returnTypes, Collection paramTypes, - Collection attributes) { + Collection contextLifetimes, Collection lifetimeParameters, Collection attributes) { super(attributes); this.returnTypes = new ArrayList(returnTypes); this.paramTypes = new ArrayList(paramTypes); + this.contextLifetimes = new ArrayList(contextLifetimes); + this.lifetimeParameters = new ArrayList(lifetimeParameters); for(SyntacticType t : paramTypes) { if(t == null) { throw new IllegalArgumentException("parameter cannot be null"); @@ -371,6 +386,11 @@ public FunctionOrMethod(Collection returnTypes, Collection returnTypes, Collection paramTypes, Attribute... attributes) { - super(returnTypes,paramTypes,attributes); + super(returnTypes,paramTypes,Collections.emptySet(),Collections.emptyList(),attributes); } public Function(Collection returnTypes, Collection paramTypes, Collection attributes) { - super(returnTypes,paramTypes,attributes); + super(returnTypes,paramTypes,Collections.emptySet(),Collections.emptyList(),attributes); } } public static class Method extends FunctionOrMethod implements NonUnion { - public Method(Collection returnTypes, Collection paramTypes, - Attribute... attributes) { - super(returnTypes,paramTypes,attributes); + public Method(Collection returnTypes, Collection paramTypes, + Collection contextLifetimes, Collection lifetimeParameters, Attribute... attributes) { + super(returnTypes,paramTypes,contextLifetimes,lifetimeParameters,attributes); } public Method(Collection returnTypes, Collection paramTypes, - Collection attributes) { - super(returnTypes,paramTypes,attributes); + Collection contextLifetimes, Collection lifetimeParameters, Collection attributes) { + super(returnTypes,paramTypes,contextLifetimes,lifetimeParameters,attributes); } } } diff --git a/modules/wyc/src/wyc/lang/WhileyFile.java b/modules/wyc/src/wyc/lang/WhileyFile.java index ecc75799c2..503549e8a9 100755 --- a/modules/wyc/src/wyc/lang/WhileyFile.java +++ b/modules/wyc/src/wyc/lang/WhileyFile.java @@ -422,6 +422,7 @@ public Type(List modifiers, Parameter type, */ public abstract class FunctionOrMethod extends NamedDeclaration { public final ArrayList parameters; + public final ArrayList lifetimeParameters; public final ArrayList returns; public final ArrayList statements; public List requires; @@ -446,12 +447,14 @@ public abstract class FunctionOrMethod extends NamedDeclaration { */ public FunctionOrMethod(List modifiers, String name, List returns, List parameters, + List lifetimeParameters, List requires, List ensures, List statements, Attribute... attributes) { super(name, modifiers,attributes); this.returns = new ArrayList(returns); this.parameters = new ArrayList(parameters); + this.lifetimeParameters = lifetimeParameters == null ? new ArrayList() : new ArrayList(lifetimeParameters); this.requires = new ArrayList(requires); this.ensures = new ArrayList(ensures); this.statements = new ArrayList(statements); @@ -503,8 +506,7 @@ public Function(List modifiers, String name, List returns, List parameters, List requires, List ensures, List statements, Attribute... attributes) { - super(modifiers, name, returns, parameters, requires, ensures, - statements, attributes); + super(modifiers, name, returns, parameters, null, requires, ensures, statements, attributes); } public SyntacticType.Function unresolvedType() { @@ -560,8 +562,9 @@ public final class Method extends FunctionOrMethod { public Nominal.Method resolvedType; public Method(List modifiers, String name, List returns, List parameters, - List requires, List ensures, List statements, Attribute... attributes) { - super(modifiers, name, returns, parameters, requires, ensures, statements, attributes); + List lifetimeParameters, List requires, List ensures, + List statements, Attribute... attributes) { + super(modifiers, name, returns, parameters, lifetimeParameters, requires, ensures, statements, attributes); } public SyntacticType.Method unresolvedType() { @@ -573,7 +576,8 @@ public SyntacticType.Method unresolvedType() { for (Parameter r : returns) { returnTypes.add(r.type); } - return new SyntacticType.Method(returnTypes, parameterTypes, attributes()); + return new SyntacticType.Method(returnTypes, parameterTypes, + Collections.emptySet(), lifetimeParameters, attributes()); } public Nominal.Method resolvedType() { diff --git a/modules/wyc/src/wyc/testing/AllInvalidTests.java b/modules/wyc/src/wyc/testing/AllInvalidTests.java index 5aea055c2e..8904e3d7bf 100755 --- a/modules/wyc/src/wyc/testing/AllInvalidTests.java +++ b/modules/wyc/src/wyc/testing/AllInvalidTests.java @@ -198,7 +198,7 @@ protected void runTest(String name) { fail("Test compiled when it shouldn't have!"); } else if (r == WycMain.INTERNAL_FAILURE) { // This indicates some other kind of internal failure. - fail("Test caused internal failure!"); + fail("Test caused internal failure!\n" + output); } else { // Now, let's check the expected output against the file which // contains the sample output for this test diff --git a/modules/wyc/src/wyc/testing/AllValidTests.java b/modules/wyc/src/wyc/testing/AllValidTests.java index a9d4ca4e3b..cc4f165614 100644 --- a/modules/wyc/src/wyc/testing/AllValidTests.java +++ b/modules/wyc/src/wyc/testing/AllValidTests.java @@ -89,6 +89,7 @@ public class AllValidTests { IGNORED.put("Import_Valid_5", "#492"); IGNORED.put("Intersection_Valid_1", "Issue ???"); IGNORED.put("Intersection_Valid_2", "Issue ???"); + IGNORED.put("Lifetime_Lambda_Valid_4", "#641"); IGNORED.put("ListAccess_Valid_6", "Issue ???"); IGNORED.put("ListAccess_Valid_7", "Issue ???"); IGNORED.put("NegationType_Valid_3", "Issue ???"); diff --git a/modules/wyc/src/wyc/testing/AllValidVerificationTests.java b/modules/wyc/src/wyc/testing/AllValidVerificationTests.java index 327be731d7..b3ace5b91a 100644 --- a/modules/wyc/src/wyc/testing/AllValidVerificationTests.java +++ b/modules/wyc/src/wyc/testing/AllValidVerificationTests.java @@ -121,6 +121,7 @@ public class AllValidVerificationTests { IGNORED.put("Lambda_Valid_3", "#344"); IGNORED.put("Lambda_Valid_4", "#344"); IGNORED.put("Lambda_Valid_7", "#344"); + IGNORED.put("Lifetime_Lambda_Valid_4", "#298"); IGNORED.put("ListAccess_Valid_6", "Known Issue"); IGNORED.put("ListAssign_Valid_1", "#233"); IGNORED.put("ListAssign_Valid_6", "#233"); diff --git a/modules/wyc/src/wyc/testing/TestUtils.java b/modules/wyc/src/wyc/testing/TestUtils.java index 75f8b79f75..5c24ec792c 100644 --- a/modules/wyc/src/wyc/testing/TestUtils.java +++ b/modules/wyc/src/wyc/testing/TestUtils.java @@ -102,7 +102,8 @@ public static Pair compile(String... args) { * @throws IOException */ public static void execWyil(String wyilDir, Path.ID id) throws IOException { - Type.Method sig = Type.Method(Collections.EMPTY_LIST, Collections.EMPTY_LIST); + Type.Method sig = Type.Method(Collections.emptyList(), Collections.emptySet(), + Collections.emptyList(), Collections.emptyList()); NameID name = new NameID(id,"test"); Build.Project project = initialiseProject(wyilDir); new Interpreter(project,null).execute(name,sig); diff --git a/modules/wyil/src/wyil/Main.java b/modules/wyil/src/wyil/Main.java index 7267717b52..381e3df2dc 100644 --- a/modules/wyil/src/wyil/Main.java +++ b/modules/wyil/src/wyil/Main.java @@ -89,7 +89,8 @@ public static void main(String[] args) { WyilFile wf = new WyilFileReader(args[0]).read(); new WyilFilePrinter(System.out).apply(wf); // FIXME: this is all a hack for now - Type.Method sig = Type.Method(Collections.EMPTY_LIST, Collections.EMPTY_LIST); + Type.Method sig = Type.Method(Collections.emptyList(), Collections.emptySet(), + Collections.emptyList(), Collections.emptyList()); NameID name = new NameID(wf.id(),"test"); Build.Project project = initialiseProject("."); Constant[] returns = new Interpreter(project,System.out).execute(name,sig); diff --git a/modules/wyil/src/wyil/lang/Type.java b/modules/wyil/src/wyil/lang/Type.java index 9d50edb152..0b79d75a9b 100755 --- a/modules/wyil/src/wyil/lang/Type.java +++ b/modules/wyil/src/wyil/lang/Type.java @@ -83,7 +83,7 @@ public abstract class Type { // the following are strictly unnecessary, but since they occur very // commonly it is helpful to provide them as constants. - public static final Reference T_REF_ANY = Reference(T_ANY); + // public static final Reference T_REF_ANY = Reference(T_ANY); /** * The type representing all possible list types. @@ -95,8 +95,8 @@ public abstract class Type { * * @param element */ - public static final Type.Reference Reference(Type element) { - Type r = construct(K_REFERENCE, null, element); + public static final Type.Reference Reference(Type element, String lifetime) { + Type r = construct(K_REFERENCE, lifetime, element); if (r instanceof Type.Reference) { return (Type.Reference) r; } else { @@ -163,8 +163,10 @@ public static final Type.Function Function(List returns, } for(int i=0;i!=returns.size();++i) { rparams[i+params_size] = returns.get(i); - } - Type r = construct(K_FUNCTION, params_size, rparams); + } + Type.FunctionOrMethod.Data data = new Type.FunctionOrMethod.Data(params_size, + Collections.emptySet(), Collections.emptyList()); + Type r = construct(K_FUNCTION, data, rparams); if (r instanceof Type.Function) { return (Type.Function) r; } else { @@ -183,7 +185,9 @@ public static final Type.Function Function(Type[] returns, Type[] rparams = new Type[params.length+returns.length]; System.arraycopy(params, 0, rparams, 0, params.length); System.arraycopy(returns, 0, rparams, params.length, returns.length); - Type r = construct(K_FUNCTION, params.length, rparams); + Type.FunctionOrMethod.Data data = new Type.FunctionOrMethod.Data(params.length, + Collections.emptySet(), Collections.emptyList()); + Type r = construct(K_FUNCTION, data, rparams); if (r instanceof Type.Function) { return (Type.Function) r; } else { @@ -197,7 +201,8 @@ public static final Type.Function Function(Type[] returns, * * @param element */ - public static final Type.Method Method(List returns, List params) { + public static final Type.Method Method(List returns, Set contextLifetimes, + List lifetimeParameters, List params) { Type[] rparams = new Type[params.size()+returns.size()]; int params_size = params.size(); for(int i=0;i!=params_size;++i) { @@ -205,8 +210,10 @@ public static final Type.Method Method(List returns, List params) { } for(int i=0;i!=returns.size();++i) { rparams[i+params_size] = returns.get(i); - } - Type r = construct(K_METHOD, params_size, rparams); + } + Type.FunctionOrMethod.Data data = new Type.FunctionOrMethod.Data(params_size, + contextLifetimes, lifetimeParameters); + Type r = construct(K_METHOD, data, rparams); if (r instanceof Type.Method) { return (Type.Method) r; } else { @@ -220,11 +227,14 @@ public static final Type.Method Method(List returns, List params) { * * @param element */ - public static final Type.Method Method(Type[] returns, Type... params) { + public static final Type.Method Method(Type[] returns, Set contextLifetimes, + List lifetimeParameters, Type... params) { Type[] rparams = new Type[params.length+returns.length]; System.arraycopy(params, 0, rparams, 0, params.length); System.arraycopy(returns, 0, rparams, params.length, returns.length); - Type r = construct(K_METHOD, params.length, rparams); + Type.FunctionOrMethod.Data data = new Type.FunctionOrMethod.Data(params.length, + contextLifetimes, lifetimeParameters); + Type r = construct(K_METHOD, data, rparams); if (r instanceof Type.Method) { return (Type.Method) r; } else { @@ -400,22 +410,36 @@ public Automaton.State readState() throws IOException { fields.add(readString()); } state.data = fields; - } else if(state.kind == Type.K_LIST || state.kind == Type.K_SET) { + } else if(state.kind == Type.K_REFERENCE) { + state.data = readString(); // lifetime + } else if(state.kind == Type.K_LIST || state.kind == Type.K_SET) { boolean nonEmpty = reader.read_bit(); state.data = nonEmpty; } else if(state.kind == Type.K_FUNCTION || state.kind == Type.K_METHOD) { + ArrayList contextLifetimes = readStringList(); + ArrayList lifetimeParameters = readStringList(); int numParameters = reader.read_uv(); - state.data = numParameters; + state.data = new Type.FunctionOrMethod.Data(numParameters, + new HashSet(contextLifetimes), lifetimeParameters); } return state; } private String readString() throws IOException { - String r = ""; + StringBuilder r = new StringBuilder(); int nchars = reader.read_uv(); for(int i=0;i!=nchars;++i) { char c = (char) reader.read_u16(); - r = r + c; + r.append(c); + } + return r.toString(); + } + + private ArrayList readStringList() throws IOException { + int len = reader.read_uv(); + ArrayList r = new ArrayList(len); + for(int i=0;i!=len;++i) { + r.add(readString()); } return r; } @@ -456,10 +480,15 @@ public void write(Automaton.State state) throws IOException { for(String field : fields) { writeString(field); } + } else if(state.kind == Type.K_REFERENCE) { + writeString((String) state.data); // lifetime } else if(state.kind == Type.K_LIST || state.kind == Type.K_SET) { writer.write_bit((Boolean) state.data); } else if(state.kind == Type.K_FUNCTION || state.kind == Type.K_METHOD) { - writer.write_uv((Integer) state.data); + Type.FunctionOrMethod.Data data = (Type.FunctionOrMethod.Data) state.data; + writeStringList(data.contextLifetimes); + writeStringList(data.lifetimeParameters); + writer.write_uv(data.numParams); } } @@ -469,6 +498,13 @@ private void writeString(String str) throws IOException { writer.write_u16(str.charAt(i)); } } + + private void writeStringList(List strl) throws IOException { + writer.write_uv(strl.size()); + for (String str : strl) { + writeString(str); + } + } } // ============================================================= @@ -479,26 +515,44 @@ private void writeString(String str) throws IOException { * Determine whether type t2 is an explicit coercive * subtype of type t1. */ - public static boolean isExplicitCoerciveSubtype(Type t1, Type t2) { + public static boolean isExplicitCoerciveSubtype(Type t1, Type t2, LifetimeRelation lr) { Automaton a1 = destruct(t1); Automaton a2 = destruct(t2); - ExplicitCoercionOperator relation = new ExplicitCoercionOperator(a1,a2); + ExplicitCoercionOperator relation = new ExplicitCoercionOperator(a1,a2,lr); return relation.isSubtype(0, 0); } + /** + * Determine whether type t2 is an explicit coercive + * subtype of type t1. + */ + public static boolean isExplicitCoerciveSubtype(Type t1, Type t2) { + return isExplicitCoerciveSubtype(t1, t2, LifetimeRelation.EMPTY); + } + /** * Determine whether type t2 is a subtype of type * t1 (written t1 :> t2). In other words, whether the set of * all possible values described by the type t2 is a subset of * that described by t1. */ - public static boolean isSubtype(Type t1, Type t2) { + public static boolean isSubtype(Type t1, Type t2, LifetimeRelation lr) { Automaton a1 = destruct(t1); Automaton a2 = destruct(t2); - SubtypeOperator relation = new SubtypeOperator(a1,a2); + SubtypeOperator relation = new SubtypeOperator(a1,a2,lr); return relation.isSubtype(0, 0); } + /** + * Determine whether type t2 is a subtype of type + * t1 (written t1 :> t2). In other words, whether the set of + * all possible values described by the type t2 is a subset of + * that described by t1. + */ + public static boolean isSubtype(Type t1, Type t2) { + return isSubtype(t1, t2, LifetimeRelation.EMPTY); + } + /** *

* Contractive types are types which cannot accept value because they have @@ -874,6 +928,9 @@ public Type element() { int elemIdx = automaton.states[0].children[0]; return construct(Automata.extract(automaton,elemIdx)); } + public String lifetime() { + return (String) automaton.states[0].data; + } } /** @@ -1154,16 +1211,79 @@ public abstract static class FunctionOrMethod extends Compound { FunctionOrMethod(Automaton automaton) { super(automaton); } - + + public static final class Data implements Comparable { + public final int numParams; + public final List contextLifetimes; + public final List lifetimeParameters; + + public Data(int numParams, Set contextLifetimes, List lifetimeParameters) { + this.numParams = numParams; + this.contextLifetimes = new ArrayList(contextLifetimes); + this.contextLifetimes.remove("*"); + Collections.sort(this.contextLifetimes); + this.lifetimeParameters = new ArrayList(lifetimeParameters); + } + + @Override + public int hashCode() { + return 31 * (31 * numParams + contextLifetimes.hashCode()) + lifetimeParameters.hashCode(); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) return true; + if (obj == null) return false; + if (this.getClass() != obj.getClass()) return false; + Data other = (Data) obj; + if (this.numParams != other.numParams) return false; + if (!this.contextLifetimes.equals(other.contextLifetimes)) { + return false; + } + if (!this.lifetimeParameters.equals(other.lifetimeParameters)) { + return false; + } + return true; + } + + @Override + public int compareTo(Data other) { + int r = Integer.compare(this.numParams, other.numParams); + if (r != 0) return r; + r = compareLists(this.contextLifetimes, other.contextLifetimes); + if (r != 0) return r; + return compareLists(this.lifetimeParameters, other.lifetimeParameters); + } + + private static int compareLists(List my, List other) { + Iterator it1 = my.iterator(); + Iterator it2 = other.iterator(); + while (true) { + if (it1.hasNext()) { + if (it2.hasNext()) { + int r = it1.next().compareTo(it2.next()); + if (r != 0) return r; + } else { + return 1; + } + } else if (it2.hasNext()) { + return -1; + } else { + return 0; + } + } + } + } + /** - * Get the parameter types of this function or method type. + * Get the return types of this function or method type. * * @return */ public ArrayList returns() { Automaton.State state = automaton.states[0]; int[] fields = state.children; - int numParams = (Integer) state.data; + int numParams = ((Data) state.data).numParams; ArrayList r = new ArrayList(); for(int i=numParams;i returns() { public ArrayList params() { Automaton.State state = automaton.states[0]; int[] fields = state.children; - int numParams = (Integer) state.data; + int numParams = ((Data) state.data).numParams; ArrayList r = new ArrayList(); for(int i=0;i contextLifetimes() { + Automaton.State state = automaton.states[0]; + Data data = (Data) state.data; + return new LinkedHashSet(data.contextLifetimes); + } + + /** + * Get the lifetime parameters of this function or method type. + * + * @return + */ + public ArrayList lifetimeParams() { + Automaton.State state = automaton.states[0]; + Data data = (Data) state.data; + return new ArrayList(data.lifetimeParameters); + } } /** @@ -1303,7 +1445,12 @@ private final static String toString(int index, BitSet visited, middle = state.data.toString(); break; case K_REFERENCE: - middle = "&" + toString(state.children[0], visited, headers, automaton); + middle = "&"; + String lifetime = (String) state.data; + if (!"*".equals(lifetime)) { + middle += lifetime + ":"; + } + middle += toString(state.children[0], visited, headers, automaton); break; case K_NEGATION: { middle = "!" + toBracesString(state.children[0], visited, headers, automaton); @@ -1364,8 +1511,9 @@ private final static String toString(int index, BitSet visited, case K_METHOD: case K_FUNCTION: { String parameters = ""; - int[] children = state.children; ; - int numParameters = (Integer) state.data; + int[] children = state.children; + Type.FunctionOrMethod.Data data = (Type.FunctionOrMethod.Data) state.data; + int numParameters = data.numParams; for (int i = 0; i != numParameters; ++i) { if (i!=0) { parameters += ","; @@ -1379,11 +1527,40 @@ private final static String toString(int index, BitSet visited, } returns += toString(children[i], visited, headers, automaton); } - if(state.kind == K_FUNCTION) { - middle = "function(" + parameters + ")->(" + returns + ")"; - } else { - middle = "method(" + parameters + ")->(" + returns + ")"; - } + StringBuilder sb = new StringBuilder(); + sb.append(state.kind == K_FUNCTION ? "function" : "method"); + if (!data.contextLifetimes.isEmpty()) { + sb.append('['); + boolean first = true; + for (String l : data.contextLifetimes) { + if (!first) { + sb.append(','); + } else { + first = false; + } + sb.append(l); + } + sb.append(']'); + } + if (!data.lifetimeParameters.isEmpty()) { + sb.append('<'); + boolean first = true; + for (String l : data.lifetimeParameters) { + if (!first) { + sb.append(','); + } else { + first = false; + } + sb.append(l); + } + sb.append('>'); + } + sb.append('('); + sb.append(parameters); + sb.append(")->("); + sb.append(returns); + sb.append(')'); + middle = sb.toString(); break; } default: @@ -1764,33 +1941,33 @@ private static T get(T type) { } } - public static void main(String[] args) { - //Type from = fromString("(null,null)"); - //Type to = fromString("X<[X]>"); - Type from = fromString("!(!{int x,int z} | !{int x,int y})"); - Type to = fromString("{string name,...}"); - System.out.println(from + " :> " + to + " = " + isSubtype(from, to)); - System.out.println(from + " & " + to + " = " + intersect(from,to)); - //System.out.println(from + " - " + to + " = " + intersect(from,Type.Negation(to))); - //System.out.println(to + " - " + from + " = " + intersect(to,Type.Negation(from))); - //System.out.println("!" + from + " & !" + to + " = " - // + intersect(Type.Negation(from), Type.Negation(to))); - } - - public static Type linkedList(int n) { - NameID label = new NameID(Trie.fromString(""),"X"); - return Recursive(label,innerLinkedList(n)); - } - - public static Type innerLinkedList(int n) { - if(n == 0) { - return Nominal(new NameID(Trie.fromString(""),"X")); - } else { - Type leaf = Reference(innerLinkedList(n-1)); - HashMap fields = new HashMap(); - fields.put("next", Union(T_NULL,leaf)); - fields.put("data", T_BOOL); - return Record(false,fields); - } - } +// public static void main(String[] args) { +// //Type from = fromString("(null,null)"); +// //Type to = fromString("X<[X]>"); +// Type from = fromString("!(!{int x,int z} | !{int x,int y})"); +// Type to = fromString("{string name,...}"); +// System.out.println(from + " :> " + to + " = " + isSubtype(from, to)); +// System.out.println(from + " & " + to + " = " + intersect(from,to)); +// //System.out.println(from + " - " + to + " = " + intersect(from,Type.Negation(to))); +// //System.out.println(to + " - " + from + " = " + intersect(to,Type.Negation(from))); +// //System.out.println("!" + from + " & !" + to + " = " +// // + intersect(Type.Negation(from), Type.Negation(to))); +// } +// +// public static Type linkedList(int n) { +// NameID label = new NameID(Trie.fromString(""),"X"); +// return Recursive(label,innerLinkedList(n)); +// } +// +// public static Type innerLinkedList(int n) { +// if(n == 0) { +// return Nominal(new NameID(Trie.fromString(""),"X")); +// } else { +// Type leaf = Reference(innerLinkedList(n-1)); +// HashMap fields = new HashMap(); +// fields.put("next", Union(T_NULL,leaf)); +// fields.put("data", T_BOOL); +// return Record(false,fields); +// } +// } } diff --git a/modules/wyil/src/wyil/util/TypeExpander.java b/modules/wyil/src/wyil/util/TypeExpander.java index d04b421634..5cae2e2f8c 100644 --- a/modules/wyil/src/wyil/util/TypeExpander.java +++ b/modules/wyil/src/wyil/util/TypeExpander.java @@ -237,7 +237,7 @@ public int getTypeHelper(Type type, boolean maximallyConsumed, for(int i=0;i!=tt_returns_size;++i) { myChildren[i+tt_params_size] = getTypeHelper(tt_returns.get(i),maximallyConsumed,states,roots); } - myData = tt_params_size; + myData = new Type.FunctionOrMethod.Data(tt_params_size, tt.contextLifetimes(), tt.lifetimeParams()); myKind = tt instanceof Type.Function ? Type.K_FUNCTION : Type.K_METHOD; }else { diff --git a/modules/wyil/src/wyil/util/interpreter/Interpreter.java b/modules/wyil/src/wyil/util/interpreter/Interpreter.java index 264c74faf0..216ebe6463 100644 --- a/modules/wyil/src/wyil/util/interpreter/Interpreter.java +++ b/modules/wyil/src/wyil/util/interpreter/Interpreter.java @@ -299,8 +299,12 @@ private Constant convert(Constant value, Type to, Context context) { // In this case, we don't need to do anything because the value is // already of the correct type. return value; - } - if (to instanceof Type.Record) { + } else if (type instanceof Type.Reference && to instanceof Type.Reference) { + if (Type.isSubtype(((Type.Reference) to).element(), ((Type.Reference) type).element())) { + // OK, it's just the lifetime that differs. + return value; + } + } else if (to instanceof Type.Record) { return convert(value, (Type.Record) to, context); } else if (to instanceof Type.Array) { return convert(value, (Type.Array) to, context); @@ -941,7 +945,8 @@ public int compareTo(Constant o) { @Override public wyil.lang.Type type() { - return wyil.lang.Type.Reference(value.type()); + // TODO: extend wyil.lang.Codes.NewObject with a lifetime and use it + return wyil.lang.Type.Reference(value.type(), "*"); } } diff --git a/modules/wyil/src/wyil/util/type/ExplicitCoercionOperator.java b/modules/wyil/src/wyil/util/type/ExplicitCoercionOperator.java index 06c1501b51..2d1933ac2b 100644 --- a/modules/wyil/src/wyil/util/type/ExplicitCoercionOperator.java +++ b/modules/wyil/src/wyil/util/type/ExplicitCoercionOperator.java @@ -59,8 +59,8 @@ */ public class ExplicitCoercionOperator extends SubtypeOperator { - public ExplicitCoercionOperator(Automaton fromAutomata, Automaton toAutomata) { - super(fromAutomata,toAutomata); + public ExplicitCoercionOperator(Automaton fromAutomata, Automaton toAutomata, LifetimeRelation lr) { + super(fromAutomata,toAutomata,lr); } @Override diff --git a/modules/wyil/src/wyil/util/type/LifetimeRelation.java b/modules/wyil/src/wyil/util/type/LifetimeRelation.java new file mode 100644 index 0000000000..71831cf0f9 --- /dev/null +++ b/modules/wyil/src/wyil/util/type/LifetimeRelation.java @@ -0,0 +1,140 @@ +package wyil.util.type; + +import java.util.Collection; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Set; +import java.util.Stack; + +/** + * This relation tracks the partial order among lifetimes. + */ +public class LifetimeRelation { + + /** + * These are all lifetime parameters to the current method. There is no + * order between lifetimes in this set. + */ + private final Set parameters; + + /** + * These are lifetimes declared by named blocks. These lifetimes are totally + * ordered according to their position in the stack. Each lifetime in + * {@link #parameters} outlives all block lifetimes. + */ + private final Stack blocks; + + /** + * Create a new and empty lifetime relation. + */ + public LifetimeRelation() { + this.parameters = new HashSet(); + this.blocks = new Stack(); + } + + /** + * Create an independent copy of the given lifetime relation. + * + * @param lifetimeRelation + */ + public LifetimeRelation(LifetimeRelation lifetimeRelation) { + this.parameters = new HashSet(lifetimeRelation.parameters); + this.blocks = new Stack(); + this.blocks.addAll(lifetimeRelation.blocks); + } + + /** + * Check whether the first (outer) lifetime outlives the second (inner) + * lifetime. + * + * @param outerLifetime + * @param innerLifetime + * @return + */ + public boolean outlives(String outerLifetime, String innerLifetime) { + if (outerLifetime.equals("*")) { + // * outlives everything + return true; + } + + if (outerLifetime.equals(innerLifetime)) { + return true; + } + + // Check whether the inner lifetime is from a named block. + int innerIndex = this.blocks.indexOf(innerLifetime); + if (innerIndex != -1) { + // All parameters are ordered before blocks. + if (this.parameters.contains(outerLifetime)) { + return true; + } + + // Maybe another block at lower stack position? + int outerIndex = this.blocks.indexOf(outerLifetime); + if (outerIndex != -1 && outerIndex < innerIndex) { + return true; + } + } + + return false; + } + + /** + * Add a method's lifetime parameters to this relation. + * + * @param lifetimeParameters + */ + public void addParameters(Collection lifetimeParameters) { + this.parameters.addAll(lifetimeParameters); + } + + /** + * Enter a named block to this relation. + * + * @param lifetime + */ + public void startNamedBlock(String lifetime) { + this.blocks.push(lifetime); + } + + /** + * Remove the named block with the given name from this relation. It also + * removes inner blocks in case that the given block is not the latest one. + * + * @param lifetime + */ + public void endNamedBlock(String lifetime) { + int i = this.blocks.lastIndexOf(lifetime); + if (i != -1) { + this.blocks.subList(i, this.blocks.size()).clear(); + } + } + + /** + * Replace this lifetime relation with the merge result of the given two + * relations. + * + * @param first + * @param second + */ + public void replaceWithMerge(LifetimeRelation first, LifetimeRelation second) { + this.parameters.clear(); + this.blocks.clear(); + + this.parameters.addAll(first.parameters); + this.parameters.retainAll(second.parameters); + Iterator it1 = first.blocks.iterator(); + Iterator it2 = second.blocks.iterator(); + while (it1.hasNext() && it2.hasNext()) { + String b1 = it1.next(); + String b2 = it2.next(); + if (b1.equals(b2)) { + this.blocks.push(b1); + } else { + break; + } + } + } + + public final static LifetimeRelation EMPTY = new LifetimeRelation(); +} diff --git a/modules/wyil/src/wyil/util/type/LifetimeSubstitution.java b/modules/wyil/src/wyil/util/type/LifetimeSubstitution.java new file mode 100644 index 0000000000..ae712323b0 --- /dev/null +++ b/modules/wyil/src/wyil/util/type/LifetimeSubstitution.java @@ -0,0 +1,262 @@ +package wyil.util.type; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.ListIterator; +import java.util.Map; +import java.util.Set; + +import wyautl_old.lang.Automaton; +import wyautl_old.lang.Automaton.State; +import wyil.lang.Type; + +/** + * This class can be used to substitute lifetimes, i.e. instantiate lifetime + * parameters with actual lifetime arguments. + * + * It is not a trivial task, as you must take care to not capture lifetime + * parameters within nested method types. This is especially difficult when + * types are recursive. + * + * The method type defined by + * + * 

+ * type mymethod is method(&*:mymethod)->(&a:mymethod)
+ *
+ * + * returns + * + * 
+ * X<&a:Y(&Y)->(X)>>
+ *
+ * + * Assume the argument for parameter "a" is "b". You cannot just replace "&a:" + * with "&b:", because it would also affect the nested return type. Instead, we + * need this type here: + * + * 
+ * &b:X(&X)->( Y<&a:Z(&Z)->(Y)>> )>
+ *
+ * + * It can be further simplified to + * + * 
+ * &b:X(&X)->(&a:X)>
+ *
+ * + * Note that the original type has two different references, but the substituted + * and minimized type has three reference types with different lifetimes. They + * cannot be mapped to the same automaton state. Substitution might yield an + * automaton with more states! + */ +public class LifetimeSubstitution { + + /** + * The substitution to apply + */ + private final Map substitution; + + /** + * The substituted type + */ + private final Type substituted; + + /** + * The states in the original automaton + */ + private final State[] originalStates; + + /** + * The states in our new automaton + */ + private final List substitutedStates; + + /** + * For each old state we can have several new states. They differ in the set + * of lifetimes that had to be substituted. + */ + private final Map> mapping; + + /** + * Apply the substitution. + * + * @param original + * the original automaton + * @param substitution + * the substitution to apply + */ + public LifetimeSubstitution(Type original, Map substitution) { + this.substitution = substitution; + + if (substitution.isEmpty()) { + // easy! + substituted = original; + + // we do not need those fields + originalStates = null; + substitutedStates = null; + mapping = null; + } else { + // initialize all fields + originalStates = Type.destruct(original).states; + substitutedStates = new ArrayList(originalStates.length); + mapping = new HashMap<>(originalStates.length); + + // Start with the root state + SubstitutedState newRootState = copy(0, Collections.emptySet()); + if (newRootState.substitutedLiffetimes.isEmpty()) { + // nothing got substituted! + substituted = original; + } else { + // Construct the resulting type. + substituted = Type.construct(new Automaton(substitutedStates)); + } + } + } + + /** + * Get the substituted type. + * + * @return the substituted type + */ + public Type getType() { + return substituted; + } + + /** + * Copy the given state into our new automaton while applying the + * substitution but ignoring the given lifetimes. + * + * @param index + * the state index from the original automaton + * @param ignored + * do not apply substitution for these lifetimes + * @return + */ + private SubstitutedState copy(int index, Set ignored) { + List mapped = mapping.get(index); + if (mapped == null) { + mapped = new LinkedList<>(); + mapping.put(index, mapped); + } else { + outer: for (SubstitutedState entry : mapped) { + if (ignored.containsAll(entry.ignoredLifetimes)) { + // This entry might be suitable for us, but only if it did + // not substitute any lifetime that should be ignored now. + for (String substitutedLifetime : entry.substitutedLiffetimes) { + if (ignored.contains(substitutedLifetime)) { + // no, cannot re-use that one + continue outer; + } + } + return entry; + } + } + } + + // OK, we need to copy that state. + SubstitutedState substitutedState = new SubstitutedState( + substitutedStates.size(), // next available index + ignored, + new HashSet() + ); + mapped.add(substitutedState); + State state = new State(originalStates[index]); + substitutedStates.add(state); + + switch (state.kind) { + case Type.K_REFERENCE: + // If it is a reference, then we might have to fix the lifetime + String lifetime = (String) state.data; + if (!ignored.contains(lifetime)) { + String replacement = substitution.get(lifetime); + if (replacement != null) { + // OK, we need to replace + substitutedState.substitutedLiffetimes.add(lifetime); + state.data = replacement; + } + } + break; + + case Type.K_FUNCTION: + case Type.K_METHOD: + // We need to apply the substitution to the context lifetimes + Type.FunctionOrMethod.Data data = (Type.FunctionOrMethod.Data) state.data; + if (!data.contextLifetimes.isEmpty()) { + ListIterator it = data.contextLifetimes.listIterator(); + boolean updated = false; + while (it.hasNext()) { + String lifetime2 = it.next(); + if (!ignored.contains(lifetime2)) { + String replacement = substitution.get(lifetime2); + if (replacement != null) { + // OK, we need to replace + substitutedState.substitutedLiffetimes.add(lifetime2); + it.set(replacement); + updated = true; + } + } + } + if (updated) { + // Context lifetimes should be sorted + Collections.sort(data.contextLifetimes); + } + } + + // We need to ignore lifetime parameters when recursing to the children children. + if (!data.lifetimeParameters.isEmpty()) { + ignored = new HashSet(ignored); + ignored.addAll(data.lifetimeParameters); + } + break; + + default: + } + + if (state.children.length != 0) { + // We cannot yet know which lifetimes will be substituted, but need + // to specify something before we enter the children. + // Overestimating does not harm, so we assume that all lifetimes + // that should be substituted actually will be substituted + // But we keep track of which lifetimes got substituted in the children. + Set childSubstituted = new HashSet(substitutedState.substitutedLiffetimes); + substitutedState.substitutedLiffetimes.addAll(substitution.keySet()); + substitutedState.substitutedLiffetimes.removeAll(ignored); + + // Now copy all children + for (int i = 0; i < state.children.length; ++i) { + SubstitutedState child = copy(state.children[i], ignored); + if (child != substitutedState) { + // remember the substituted lifetimes + // but only if that child is not directly recursively + // referring to us :) + childSubstituted.addAll(child.substitutedLiffetimes); + } + + // fix the index + state.children[i] = child.newStateIndex; + } + + // Update the substituted lifetimes + substitutedState.substitutedLiffetimes.retainAll(childSubstituted); + } + + return substitutedState; + } + + private static class SubstitutedState { + private final int newStateIndex; + private final Set ignoredLifetimes; + private final Set substitutedLiffetimes; + + private SubstitutedState(int newStateIndex, Set ignoredLifetimes, Set substitutedLiffetimes) { + this.newStateIndex = newStateIndex; + this.ignoredLifetimes = ignoredLifetimes; + this.substitutedLiffetimes = substitutedLiffetimes; + } + } +} diff --git a/modules/wyil/src/wyil/util/type/SubtypeOperator.java b/modules/wyil/src/wyil/util/type/SubtypeOperator.java index 01611853dd..7407b07de7 100644 --- a/modules/wyil/src/wyil/util/type/SubtypeOperator.java +++ b/modules/wyil/src/wyil/util/type/SubtypeOperator.java @@ -78,17 +78,37 @@ public class SubtypeOperator { protected final Automaton from; protected final Automaton to; + private final Map fromLifetimeSubstitution; + private final Map toLifetimeSubstitution; + private final LifetimeRelation lifetimeRelation; private final BitSet assumptions; - public SubtypeOperator(Automaton from, Automaton to) { + public SubtypeOperator(Automaton from, Automaton to, LifetimeRelation lr) { this.from = from; this.to = to; + this.lifetimeRelation = lr; + this.fromLifetimeSubstitution = Collections.emptyMap(); + this.toLifetimeSubstitution = Collections.emptyMap(); // matrix is twice the size to accommodate positive and negative signs this.assumptions = new BitSet((2*from.size()) * (to.size()*2)); //System.out.println("FROM: " + from); //System.out.println("TO: " + to); } + private SubtypeOperator(SubtypeOperator sto, Map fromLifetimeSubstitution, + Map toLifetimeSubstitution) { + this.from = sto.from; + this.to = sto.to; + this.fromLifetimeSubstitution = new HashMap(sto.fromLifetimeSubstitution); + prependLifetimes(this.fromLifetimeSubstitution); + this.fromLifetimeSubstitution.putAll(fromLifetimeSubstitution); + this.toLifetimeSubstitution = new HashMap(sto.toLifetimeSubstitution); + prependLifetimes(this.toLifetimeSubstitution); + this.toLifetimeSubstitution.putAll(toLifetimeSubstitution); + this.lifetimeRelation = sto.lifetimeRelation; + this.assumptions = sto.assumptions; + } + /** * Test whether from :> to * @param fromIndex @@ -194,9 +214,50 @@ protected boolean isIntersectionInner(int fromIndex, boolean fromSign, int toInd if(fromSign || toSign) { int fromChild = fromState.children[0]; int toChild = toState.children[0]; - return isIntersection(fromChild, fromSign, toChild, toSign) - || isIntersection(fromChild, !fromSign, toChild, !toSign); + + if (fromSign && toSign) { + // "Is there any value in both &a:A and &b:B ?" + // + // This is equivalent to the question "Is there any value in both &A and &B?" + // If there is a value in both &a:A and &b:B, then we can take that value + // and change its lifetime to *. It will then be in both &A and &B. + // If there is a value in both &A and &B, then it is also in both &a:A and &b:B + // because the lifetime * outlives a and b. + // + // Finally, there is a value in both &A and &B iff the types A and B intersect. + return isIntersection(fromChild, true, toChild, true); + } else { + String fromLifetime = applyFromLifetimeSubstitution((String) fromState.data); + String toLifetime = applyToLifetimeSubstitution((String) toState.data); + + if (fromSign) { + // Equivalent to the negation of "is &a:A (fromType) a subtype of &b:B (toType)?" + return !( + // &a:A is a subtype of &b:B iff all these are true: + // a outlives b + lifetimeRelation.outlives(fromLifetime, toLifetime) + // A is a subtype of B + && !isIntersection(fromChild, true, toChild, false) + // B is a subtype of A + && !isIntersection(fromChild, false, toChild, true) + ); + } else { + // Equivalent to the negation of "is &b:B (toType) a subtype of &a:A (fromType)?" + return !( + // &b:B is a subtype of &a:A iff all these are true: + // b outlives a + lifetimeRelation.outlives(toLifetime, fromLifetime) + // B is a subtype of A + && !isIntersection(fromChild, false, toChild, true) + // A is a subtype of B + && !isIntersection(fromChild, true, toChild, false) + ); + } + } } + + // An inverted reference type always contains the value "null". + // Both are inverted, so they intersect with "null". return true; case K_MAP: case K_TUPLE: { @@ -239,49 +300,85 @@ protected boolean isIntersectionInner(int fromIndex, boolean fromSign, int toInd // nary nodes int[] fromChildren = fromState.children; int[] toChildren = toState.children; - int fromNumParams = (Integer) fromState.data; - int toNumParams = (Integer) toState.data; + Type.FunctionOrMethod.Data fromData = (Type.FunctionOrMethod.Data) fromState.data; + Type.FunctionOrMethod.Data toData = (Type.FunctionOrMethod.Data) toState.data; + int fromNumParams = fromData.numParams; + int toNumParams = toData.numParams; + List fromLifetimeParameters = fromData.lifetimeParameters; + List toLifetimeParameters = toData.lifetimeParameters; if (fromSign && toSign) { // Two intersecting method types must have the same number - // of parameters and returns. - if (fromChildren.length != toChildren.length || fromNumParams != toNumParams) { + // of parameters, returns and lifetime parameters. + if (fromChildren.length != toChildren.length + || fromNumParams != toNumParams + || fromLifetimeParameters.size() != toLifetimeParameters.size()){ return false; } + // Context lifetimes do not matter, because we can always choose + // a method without context lifetimes to find an intersecting method. + } else { + // Now we have one of the following: + // fromSign == true: negation of "is fromType a subtype of toType?" + // toSign == true: negation of "is toType a subtype of fromType?" + + // Two method types can only be subtypes of each other if they have + // the same number of parameters, returns and lifetime parameters. + if (fromChildren.length != toChildren.length + || fromNumParams != toNumParams + || fromLifetimeParameters.size() != toLifetimeParameters.size()){ + return true; // true means "not subtype" + } + // The supertype must contain all context lifetimes of the subtype + List fromContextLifetimes = applyFromLifetimeSubstitution(fromData.contextLifetimes); + List toContextLifetimes = applyToLifetimeSubstitution(toData.contextLifetimes); + if (fromSign) { + if (!toContextLifetimes.containsAll(fromContextLifetimes)) { + return true; + } + } else { + if (!fromContextLifetimes.containsAll(toContextLifetimes)) { + return true; + } + } + } + + // Calculate the substitutions for lifetime parameters + Map fromLifetimeSubstitution = buildLifetimeSubstitution(fromLifetimeParameters); + Map toLifetimeSubstitution = buildLifetimeSubstitution(toLifetimeParameters); + SubtypeOperator sto = this; + if (!fromLifetimeSubstitution.isEmpty() || !toLifetimeSubstitution.isEmpty()) { + sto = new SubtypeOperator(this, fromLifetimeSubstitution, toLifetimeSubstitution); + } + + if (fromSign && toSign) { // Two intersecting method types must have intersecting return types. // Parameter types can always be chosen as "any". for (int i = fromNumParams; i < fromChildren.length; ++i) { - if (!isIntersection(fromChildren[i], true, toChildren[i], true)) { + if (!sto.isIntersection(fromChildren[i], true, toChildren[i], true)) { return false; } } return true; } - // Now we have one of the following: - // fromSign == true: negation of "is fromType a subtype of toType?" - // toSign == true: negation of "is toType a subtype of fromType?" - - // Two method types can only be subtypes of each other if they have - // the same number of parameters and returns. - if (fromChildren.length != toChildren.length || fromNumParams != toNumParams) { - return true; // true means "not subtype" - } + // here we have the subtype test again... // Parameter types are contra-variant for (int i = 0; i < fromNumParams; ++i) { - if (isIntersection(fromChildren[i], !fromSign, toChildren[i], !toSign)) { + if (sto.isIntersection(fromChildren[i], !fromSign, toChildren[i], !toSign)) { return true; } } // Return types are co-variant for (int i = fromNumParams; i < fromChildren.length; ++i) { - if (isIntersection(fromChildren[i], fromSign, toChildren[i], toSign)) { + if (sto.isIntersection(fromChildren[i], fromSign, toChildren[i], toSign)) { return true; } } + return false; } return true; @@ -343,6 +440,62 @@ protected boolean isIntersectionInner(int fromIndex, boolean fromSign, int toInd return !fromSign || !toSign; } + private static Map buildLifetimeSubstitution(List lifetimeParameters) { + if (lifetimeParameters.isEmpty()) { + return Collections.emptyMap(); + } + Map substitution = new HashMap(); + int i = 0; + for (String lifetime : lifetimeParameters) { + substitution.put(lifetime, "$" + (i++)); + } + return substitution; + } + + private static void prependLifetimes(Map substitution) { + for (Map.Entry entry : substitution.entrySet()) { + entry.setValue("$" + entry.getValue()); + } + } + + private String applyFromLifetimeSubstitution(String lifetime) { + String replacement = fromLifetimeSubstitution.get(lifetime); + if (replacement != null) { + return replacement; + } + return lifetime; + } + + private String applyToLifetimeSubstitution(String lifetime) { + String replacement = toLifetimeSubstitution.get(lifetime); + if (replacement != null) { + return replacement; + } + return lifetime; + } + + private List applyFromLifetimeSubstitution(List lifetimes) { + if (lifetimes.isEmpty() || fromLifetimeSubstitution.isEmpty()) { + return lifetimes; + } + List replacement = new ArrayList(lifetimes.size()); + for (String lifetime : lifetimes) { + replacement.add(applyFromLifetimeSubstitution(lifetime)); + } + return replacement; + } + + private List applyToLifetimeSubstitution(List lifetimes) { + if (lifetimes.isEmpty() || toLifetimeSubstitution.isEmpty()) { + return lifetimes; + } + List replacement = new ArrayList(lifetimes.size()); + for (String lifetime : lifetimes) { + replacement.add(applyToLifetimeSubstitution(lifetime)); + } + return replacement; + } + /** *

* Check for intersection between two states with kind K_RECORD. The diff --git a/modules/wyil/src/wyil/util/type/TypeAlgorithms.java b/modules/wyil/src/wyil/util/type/TypeAlgorithms.java index 9b37301301..f9cb69536f 100755 --- a/modules/wyil/src/wyil/util/type/TypeAlgorithms.java +++ b/modules/wyil/src/wyil/util/type/TypeAlgorithms.java @@ -108,9 +108,9 @@ public int compare(Automaton.State s1, Automaton.State s2) { Boolean nid2 = (Boolean) s2.data; return nid1.toString().compareTo(nid2.toString()); } else if(s1.kind == Type.K_FUNCTION || s1.kind == Type.K_METHOD) { - int s1NumParams = (Integer) s1.data; - int s2NumParams = (Integer) s2.data; - return Integer.compare(s1NumParams, s2NumParams); + Type.FunctionOrMethod.Data s1Data = (Type.FunctionOrMethod.Data) s1.data; + Type.FunctionOrMethod.Data s2Data = (Type.FunctionOrMethod.Data) s2.data; + return s1Data.compareTo(s2Data); } else { String str1 = (String) s1.data; String str2 = (String) s2.data; @@ -772,7 +772,7 @@ private static boolean simplifyUnion_2(int index, Automaton.State state, private static boolean isSubtype(int fromIndex, int toIndex, Automaton automaton) { - SubtypeOperator op = new SubtypeOperator(automaton,automaton); + SubtypeOperator op = new SubtypeOperator(automaton,automaton,LifetimeRelation.EMPTY); return op.isSubtype(fromIndex, toIndex); } @@ -1057,6 +1057,7 @@ private static int intersectSameKind(int fromIndex, boolean fromSign, Automaton case Type.K_SET: return intersectSetsOrLists(fromIndex,fromSign,from,toIndex,toSign,to,allocations,states); case Type.K_REFERENCE: + return intersectCompounds(fromIndex,fromSign,from,toIndex,toSign,to,fromState.data,allocations,states); case Type.K_MAP: return intersectCompounds(fromIndex,fromSign,from,toIndex,toSign,to,null,allocations,states); case Type.K_NEGATION: diff --git a/modules/wyil/src/wyil/util/type/TypeTester.java b/modules/wyil/src/wyil/util/type/TypeTester.java index 6b15b7bf67..047d38a2b5 100755 --- a/modules/wyil/src/wyil/util/type/TypeTester.java +++ b/modules/wyil/src/wyil/util/type/TypeTester.java @@ -97,7 +97,8 @@ public boolean accepts(int index, Automaton automaton, Term value) { return false; } int length = schildren.length; - int sNumParams = (Integer) state.data; + Type.FunctionOrMethod.Data data = (Type.FunctionOrMethod.Data) state.data; + int sNumParams = data.numParams; // First, do parameters (which are contravariant). for(int i=0;iemptySet(), + Collections.emptyList(), WHILEY_SYSTEM_T); JvmType.Function ft3 = convertFunType(wyft); codes.add(new Bytecode.Invoke(owner, nameMangle("main", wyft), ft3, Bytecode.InvokeMode.STATIC)); diff --git a/modules/wyrt/src/whiley/io/File.whiley b/modules/wyrt/src/whiley/io/File.whiley index 909bbfff89..33fe027032 100755 --- a/modules/wyrt/src/whiley/io/File.whiley +++ b/modules/wyrt/src/whiley/io/File.whiley @@ -55,13 +55,13 @@ public type Reader is { } public method Reader(string fileName) -> Reader: - NativeFile this = NativeFileReader(fileName) + NativeFile reader = NativeFileReader(fileName) return { - readAll: &( -> read(this)), - read: &(uint n -> read(this,n)), - hasMore: &( -> hasMore(this)), - close: &( -> close(this)), - available: &( -> available(this)) + readAll: &( -> read(reader)), + read: &(uint n -> read(reader,n)), + hasMore: &( -> hasMore(reader)), + close: &( -> close(reader)), + available: &( -> available(reader)) } // ==================================================== @@ -70,11 +70,11 @@ public method Reader(string fileName) -> Reader: type Writer is whiley.io.Writer.Writer public method Writer(string fileName) -> Writer: - NativeFile this = NativeFileWriter(fileName) + NativeFile reader = NativeFileWriter(fileName) return { - write: &(byte[] data -> write(this,data)), - close: &( -> close(this)), - flush: &( -> flush(this)) + write: &(byte[] data -> write(reader,data)), + close: &( -> close(reader)), + flush: &( -> flush(reader)) } // ==================================================== diff --git a/modules/wyrt/src/whiley/lang/Stack.whiley b/modules/wyrt/src/whiley/lang/Stack.whiley index cca66e9845..7351c97d88 100755 --- a/modules/wyrt/src/whiley/lang/Stack.whiley +++ b/modules/wyrt/src/whiley/lang/Stack.whiley @@ -36,31 +36,31 @@ public function create(int max) -> Stack: length: 0 } -public function size(Stack this) -> int: - return this.length +public function size(Stack stack) -> int: + return stack.length /** * Return the top element of the "stack". */ -public function top(Stack this) -> int: +public function top(Stack stack) -> int: // - return this.items[this.length-1] + return stack.items[stack.length-1] /** * Push an element onto the "stack". */ -public function push(Stack this, int element) -> (Stack r): +public function push(Stack stack, int element) -> (Stack r): // - this.items[this.length] = element - this.length = this.length + 1 - return this + stack.items[stack.length] = element + stack.length = stack.length + 1 + return stack /** * Pop an element off the "stack". */ -public function pop(Stack this) -> (Stack r): +public function pop(Stack stack) -> (Stack r): // - this.length = this.length - 1 + stack.length = stack.length - 1 // - return this + return stack diff --git a/tests/invalid/ConstrainedRecord_Invalid_1.whiley b/tests/invalid/ConstrainedRecord_Invalid_1.whiley index 822636db9c..e5710c1af8 100644 --- a/tests/invalid/ConstrainedRecord_Invalid_1.whiley +++ b/tests/invalid/ConstrainedRecord_Invalid_1.whiley @@ -1,7 +1,7 @@ type tup is {int y, int x} -type point is ({int y, int x} this) where (this.x > 0) && (this.y > 0) +type point is ({int y, int x} _this) where (_this.x > 0) && (_this.y > 0) function f(point p) -> point: return p diff --git a/tests/invalid/DefiniteAssign_Invalid_4.whiley b/tests/invalid/DefiniteAssign_Invalid_4.whiley index 3d24e46bd5..cebab57928 100644 --- a/tests/invalid/DefiniteAssign_Invalid_4.whiley +++ b/tests/invalid/DefiniteAssign_Invalid_4.whiley @@ -1,5 +1,5 @@ -method f(any this) : - debug this +method f(any _this) : + debug _this method g() : f(x) diff --git a/tests/invalid/FunctionRef_Invalid_5.whiley b/tests/invalid/FunctionRef_Invalid_5.whiley index d79c0f0ff6..c2be32b6b1 100644 --- a/tests/invalid/FunctionRef_Invalid_5.whiley +++ b/tests/invalid/FunctionRef_Invalid_5.whiley @@ -1,6 +1,6 @@ type Proc is &{int data} -method read(Proc this, int x) -> int: +method read(Proc _this, int x) -> int: return x + 1 type Func is { diff --git a/tests/invalid/FunctionRef_Invalid_7.sysout b/tests/invalid/FunctionRef_Invalid_7.sysout index 0ac8eb7ded..abffbcb04c 100644 --- a/tests/invalid/FunctionRef_Invalid_7.sysout +++ b/tests/invalid/FunctionRef_Invalid_7.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/FunctionRef_Invalid_7.whiley:6: insufficient arguments for function or method invocation - return this->func(arg) - ^^^^^^^^^^^^^^^ + return _this->func(arg) + ^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/FunctionRef_Invalid_7.whiley b/tests/invalid/FunctionRef_Invalid_7.whiley index 055297462a..5334ca1f76 100644 --- a/tests/invalid/FunctionRef_Invalid_7.whiley +++ b/tests/invalid/FunctionRef_Invalid_7.whiley @@ -2,5 +2,5 @@ type Proc is &{ function func(bool,int)->bool } -method test(Proc this, bool arg) -> bool: - return this->func(arg) +method test(Proc _this, bool arg) -> bool: + return _this->func(arg) diff --git a/tests/invalid/Lifetime_Invalid_1.sysout b/tests/invalid/Lifetime_Invalid_1.sysout new file mode 100644 index 0000000000..6a9ed1ad58 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_1.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Invalid_1.whiley:2: expected type &int, found &this:int + &*:int ptr1 = this:new 42 + ^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_1.whiley b/tests/invalid/Lifetime_Invalid_1.whiley new file mode 100644 index 0000000000..0bfad4b10c --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_1.whiley @@ -0,0 +1,2 @@ +public export method test(): + &*:int ptr1 = this:new 42 diff --git a/tests/invalid/Lifetime_Invalid_2.sysout b/tests/invalid/Lifetime_Invalid_2.sysout new file mode 100644 index 0000000000..b6a23c9438 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_2.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Invalid_2.whiley:4: expected type &this:int, found &myblock:int + x = myblock:new 1 + ^ diff --git a/tests/invalid/Lifetime_Invalid_2.whiley b/tests/invalid/Lifetime_Invalid_2.whiley new file mode 100644 index 0000000000..d9ab74f5b0 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_2.whiley @@ -0,0 +1,4 @@ +public export method test(): + &this:int x = this:new 1 + myblock: + x = myblock:new 1 diff --git a/tests/invalid/Lifetime_Invalid_3.sysout b/tests/invalid/Lifetime_Invalid_3.sysout new file mode 100644 index 0000000000..b2a6203d5a --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_3.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Invalid_3.whiley:1: use of undeclared lifetime +method foo() -> &this:int: + ^^^^ diff --git a/tests/invalid/Lifetime_Invalid_3.whiley b/tests/invalid/Lifetime_Invalid_3.whiley new file mode 100644 index 0000000000..afb6491ace --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_3.whiley @@ -0,0 +1,5 @@ +method foo() -> &this:int: + return this:new 1 + +public export method test(): + foo() diff --git a/tests/invalid/Lifetime_Invalid_4.sysout b/tests/invalid/Lifetime_Invalid_4.sysout new file mode 100644 index 0000000000..4899a2d063 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_4.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Invalid_4.whiley:2: expected type &int, found &this:int + return this:new 1 + ^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_4.whiley b/tests/invalid/Lifetime_Invalid_4.whiley new file mode 100644 index 0000000000..40002aefe2 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_4.whiley @@ -0,0 +1,5 @@ +method foo() -> &*:int: + return this:new 1 + +public export method test(): + foo() diff --git a/tests/invalid/Lifetime_Invalid_5.sysout b/tests/invalid/Lifetime_Invalid_5.sysout new file mode 100644 index 0000000000..2e2329ebbe --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_5.sysout @@ -0,0 +1,6 @@ +../../tests/invalid/Lifetime_Invalid_5.whiley:16: unable to resolve name (m(&int,&int) is ambiguous + found: Lifetime_Invalid_5:m : method(&a:int,&a:int)->(int) instantiated with <*> + found: Lifetime_Invalid_5:m : method(&a:int,&int)->(int) instantiated with <*> + found: Lifetime_Invalid_5:m : method(&int,&a:int)->(int) instantiated with <*>) + m(new 1, new 2) + ^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_5.whiley b/tests/invalid/Lifetime_Invalid_5.whiley new file mode 100644 index 0000000000..b361227376 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_5.whiley @@ -0,0 +1,16 @@ +// test lifetime inference with lifetime overloading but same types + +method m(&a:int x, &a:int y) -> int: + return 1 + +method m(&a:int x, &*:int y) -> int: + return 2 + +method m(&*:int x, &a:int y) -> int: + return 3 + +public export method test(): + // variant1: (&*:int, &*:int) <-- + // variant2: (&*:int, &*:int) <-- + // variant3: (&*:int, &*:int) <-- + m(new 1, new 2) diff --git a/tests/invalid/Lifetime_Invalid_6.sysout b/tests/invalid/Lifetime_Invalid_6.sysout new file mode 100644 index 0000000000..eec939dd70 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_6.sysout @@ -0,0 +1,5 @@ +../../tests/invalid/Lifetime_Invalid_6.whiley:12: unable to resolve name (m(&this:int,&this:int) is ambiguous + found: Lifetime_Invalid_6:m : method(&a:int,&b:int)->(int) instantiated with + found: Lifetime_Invalid_6:m : method(&a:int,&a:int)->(int) instantiated with ) + m(this:new 1, this:new 2) + ^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_6.whiley b/tests/invalid/Lifetime_Invalid_6.whiley new file mode 100644 index 0000000000..04ee77d2c0 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_6.whiley @@ -0,0 +1,12 @@ +// test lifetime inference with lifetime overloading but same types + +method m(&a:int x, &a:int y) -> int: + return 1 + +method m(&a:int x, &b:int y) -> int: + return 2 + +public export method test(): + // variant1: (&this:int, &this:int) <-- + // variant2: (&this:int, &this:int) <-- + m(this:new 1, this:new 2) diff --git a/tests/invalid/Lifetime_Invalid_7.sysout b/tests/invalid/Lifetime_Invalid_7.sysout new file mode 100644 index 0000000000..b9135cb95e --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_7.sysout @@ -0,0 +1,5 @@ +../../tests/invalid/Lifetime_Invalid_7.whiley:16: unable to resolve name (m(&int,&this:int,bool) is ambiguous + found: Lifetime_Invalid_7:m : method(&a:int|&b:bool,&a:int,bool)->(&b:int) instantiated with + found: Lifetime_Invalid_7:m : method(&int,&a:int,int|bool)->(&a:int) instantiated with ) + m(new 1, this:new 2, true) + ^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_7.whiley b/tests/invalid/Lifetime_Invalid_7.whiley new file mode 100644 index 0000000000..a1226a2c06 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_7.whiley @@ -0,0 +1,16 @@ +// test lifetime inference with lifetime overloading and different types + +method m((&a:int)|(&b:bool) x, &a:int y, bool z) -> &b:int: + return b:new 1 + +method m(&a:bool x, &a:int y, bool z) -> &a:int: + return a:new 2 + +method m(&*:int x, &a:int y, int|bool z) -> &a:int: + return a:new 3 + +public export method test(): + // variant1: ((&this:int)|(&*:bool) x, &this:int, bool z) + // variant2: no + // variant3: (&this:int x, &this:int y, int|bool z) + m(new 1, this:new 2, true) diff --git a/tests/invalid/Lifetime_Invalid_8.sysout b/tests/invalid/Lifetime_Invalid_8.sysout new file mode 100644 index 0000000000..fcdbe8c789 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_8.sysout @@ -0,0 +1,5 @@ +../../tests/invalid/Lifetime_Invalid_8.whiley:10: unable to resolve name (m(&int,&this:int) is ambiguous + found: Lifetime_Invalid_8:m : method(&a:int|&b:bool,&a:int|&b:int)->() instantiated with <*, this> + found: Lifetime_Invalid_8:m : method(&a:int|&b:bool,&a:int|&b:int)->() instantiated with ) + m(x, y) + ^^^^^^^ diff --git a/tests/invalid/Lifetime_Invalid_8.whiley b/tests/invalid/Lifetime_Invalid_8.whiley new file mode 100644 index 0000000000..5e83f899b3 --- /dev/null +++ b/tests/invalid/Lifetime_Invalid_8.whiley @@ -0,0 +1,10 @@ +// test lifetime inference with lifetime overloading and different types + +method m((&a:int)|(&b:bool) x, (&a:int)|(&b:int) y): + +public export method test(): + // --> ((&this:int)|(&*:bool), &this:int) + // <*, this> --> ((&*:int)|(&this:bool), &this:int) + (&*:int)|(&*:bool) x = *:new 1 + &this:int y = this:new 1 + m(x, y) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_1.sysout b/tests/invalid/Lifetime_Lambda_Invalid_1.sysout new file mode 100644 index 0000000000..14eb3ca605 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_1.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_1.whiley:4: expected type method(&a:int,&a:int)->(&a:int), found method(&a:int,&int)->(&a:int) + method(&a:int, &a:int)->(&a:int) m = &(&a:int x, &int y -> a:new 1) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_1.whiley b/tests/invalid/Lifetime_Lambda_Invalid_1.whiley new file mode 100644 index 0000000000..1feb0990ca --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_1.whiley @@ -0,0 +1,4 @@ +// wrong method type + +public export method test(): + method(&a:int, &a:int)->(&a:int) m = &(&a:int x, &int y -> a:new 1) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_2.sysout b/tests/invalid/Lifetime_Lambda_Invalid_2.sysout new file mode 100644 index 0000000000..d92433987a --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_2.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_2.whiley:4: expected type method(&a:int,&int)->(&int), found method(&a:int,&int)->(&a:int) + method(&a:int, &int)->(&*:int) m = &(&a:int x, &int y -> a:new 1) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_2.whiley b/tests/invalid/Lifetime_Lambda_Invalid_2.whiley new file mode 100644 index 0000000000..f5a5c88284 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_2.whiley @@ -0,0 +1,4 @@ +// wrong method type + +public export method test(): + method(&a:int, &int)->(&*:int) m = &(&a:int x, &int y -> a:new 1) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_3.sysout b/tests/invalid/Lifetime_Lambda_Invalid_3.sysout new file mode 100644 index 0000000000..21de4ae53e --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_3.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_3.whiley:4: expected type method()->(&int), found method()->(&int) + method()->(&int) m = &(-> new 1) + ^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_3.whiley b/tests/invalid/Lifetime_Lambda_Invalid_3.whiley new file mode 100644 index 0000000000..653767e2bd --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_3.whiley @@ -0,0 +1,4 @@ +// wrong method type + +public export method test(): + method()->(&int) m = &(-> new 1) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_4.sysout b/tests/invalid/Lifetime_Lambda_Invalid_4.sysout new file mode 100644 index 0000000000..ca75e48b38 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_4.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_4.whiley:4: use of undeclared lifetime + method()->(&this:int) m = &(-> this:new 1) + ^^^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_4.whiley b/tests/invalid/Lifetime_Lambda_Invalid_4.whiley new file mode 100644 index 0000000000..517b1158b8 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_4.whiley @@ -0,0 +1,4 @@ +// missing context lifetime + +public export method test(): + method()->(&this:int) m = &(-> this:new 1) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_5.sysout b/tests/invalid/Lifetime_Lambda_Invalid_5.sysout new file mode 100644 index 0000000000..88d32511c4 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_5.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_5.whiley:7: lifetime 'this' cannot be dereferenced here + return &(->*x) + ^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_5.whiley b/tests/invalid/Lifetime_Lambda_Invalid_5.whiley new file mode 100644 index 0000000000..a7d772131f --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_5.whiley @@ -0,0 +1,7 @@ +// missing context lifetime + +type mymethod is method()->(int) + +public export method test()->mymethod: + &this:int x = this:new 1 + return &(->*x) diff --git a/tests/invalid/Lifetime_Lambda_Invalid_6.sysout b/tests/invalid/Lifetime_Lambda_Invalid_6.sysout new file mode 100644 index 0000000000..21590fbaef --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_6.sysout @@ -0,0 +1,3 @@ +../../tests/invalid/Lifetime_Lambda_Invalid_6.whiley:7: expected type Lifetime_Lambda_Invalid_6:mymethod, found method[this]()->(int) + return &[this](-> (*x) + (*(new 1))) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Lifetime_Lambda_Invalid_6.whiley b/tests/invalid/Lifetime_Lambda_Invalid_6.whiley new file mode 100644 index 0000000000..d7acf31da3 --- /dev/null +++ b/tests/invalid/Lifetime_Lambda_Invalid_6.whiley @@ -0,0 +1,7 @@ +// missing context lifetime + +type mymethod is method()->(int) + +public export method test()->mymethod: + &this:int x = new 1 + return &[this](-> (*x) + (*(new 1))) diff --git a/tests/invalid/MethodCall_Invalid_1.sysout b/tests/invalid/MethodCall_Invalid_1.sysout index ee15fa7964..2b1fc6f92a 100644 --- a/tests/invalid/MethodCall_Invalid_1.sysout +++ b/tests/invalid/MethodCall_Invalid_1.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/MethodCall_Invalid_1.whiley:5: unable to resolve name (no match for f(&int,int)) - f(this, 1) - ^^^^^^^^^^ + f(_this, 1) + ^^^^^^^^^^^ diff --git a/tests/invalid/MethodCall_Invalid_1.whiley b/tests/invalid/MethodCall_Invalid_1.whiley index 2548ebd4c5..477cccc403 100644 --- a/tests/invalid/MethodCall_Invalid_1.whiley +++ b/tests/invalid/MethodCall_Invalid_1.whiley @@ -1,5 +1,5 @@ method f(int x) -> int: return 1 -method main(&int this): - f(this, 1) +method main(&int _this): + f(_this, 1) diff --git a/tests/invalid/MethodCall_Invalid_2.sysout b/tests/invalid/MethodCall_Invalid_2.sysout index cb4ddb1af4..b72463589f 100644 --- a/tests/invalid/MethodCall_Invalid_2.sysout +++ b/tests/invalid/MethodCall_Invalid_2.sysout @@ -1,4 +1,4 @@ ../../tests/invalid/MethodCall_Invalid_2.whiley:7: unable to resolve name (no match for f(&int,int) found: MethodCall_Invalid_2:f : method(MethodCall_Invalid_2:dummy,int)->(int)) - f(this, 1) - ^^^^^^^^^^ + f(_this, 1) + ^^^^^^^^^^^ diff --git a/tests/invalid/MethodCall_Invalid_2.whiley b/tests/invalid/MethodCall_Invalid_2.whiley index cad59547e0..a20777b837 100644 --- a/tests/invalid/MethodCall_Invalid_2.whiley +++ b/tests/invalid/MethodCall_Invalid_2.whiley @@ -1,7 +1,7 @@ type dummy is &{int x} -method f(dummy this, int x) -> int: +method f(dummy _this, int x) -> int: return 1 -method main(&int this) : - f(this, 1) +method main(&int _this) : + f(_this, 1) diff --git a/tests/invalid/MethodCall_Invalid_3.sysout b/tests/invalid/MethodCall_Invalid_3.sysout index 042ffbc899..e52594be18 100644 --- a/tests/invalid/MethodCall_Invalid_3.sysout +++ b/tests/invalid/MethodCall_Invalid_3.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/MethodCall_Invalid_3.whiley:2: record required, got: int[] - this.f(1) - ^^^^^^^^^ + _this.f(1) + ^^^^^^^^^^ diff --git a/tests/invalid/MethodCall_Invalid_3.whiley b/tests/invalid/MethodCall_Invalid_3.whiley index 9c9600463d..e57d389f1a 100644 --- a/tests/invalid/MethodCall_Invalid_3.whiley +++ b/tests/invalid/MethodCall_Invalid_3.whiley @@ -1,2 +1,2 @@ -method main(int[] this) : - this.f(1) +method main(int[] _this) : + _this.f(1) diff --git a/tests/invalid/Parameter_Invalid_1.sysout b/tests/invalid/Parameter_Invalid_1.sysout index 36d4e04b46..ac91ba609c 100644 --- a/tests/invalid/Parameter_Invalid_1.sysout +++ b/tests/invalid/Parameter_Invalid_1.sysout @@ -1,3 +1,3 @@ -../../tests/invalid/Parameter_Invalid_1.whiley:1: parameter already declared +../../tests/invalid/Parameter_Invalid_1.whiley:1: name already declared function f(int x, int x) -> int: ^ diff --git a/tests/invalid/Parsing_Invalid_5.sysout b/tests/invalid/Parsing_Invalid_5.sysout index 6fc18f1769..f152eb6c3c 100644 --- a/tests/invalid/Parsing_Invalid_5.sysout +++ b/tests/invalid/Parsing_Invalid_5.sysout @@ -1,3 +1,3 @@ -../../tests/invalid/Parsing_Invalid_5.whiley:2: variable already declared +../../tests/invalid/Parsing_Invalid_5.whiley:2: name already declared int x = x ^^^^^ diff --git a/tests/invalid/Parsing_Invalid_6.sysout b/tests/invalid/Parsing_Invalid_6.sysout index ba47ce4e03..f20fb796ea 100644 --- a/tests/invalid/Parsing_Invalid_6.sysout +++ b/tests/invalid/Parsing_Invalid_6.sysout @@ -1,3 +1,3 @@ -../../tests/invalid/Parsing_Invalid_6.whiley:3: variable already declared +../../tests/invalid/Parsing_Invalid_6.whiley:3: name already declared int x = x ^^^^^ diff --git a/tests/invalid/ProcessAccess_Invalid_1.sysout b/tests/invalid/ProcessAccess_Invalid_1.sysout index 09a6d711af..a9e40d1621 100644 --- a/tests/invalid/ProcessAccess_Invalid_1.sysout +++ b/tests/invalid/ProcessAccess_Invalid_1.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/ProcessAccess_Invalid_1.whiley:6: invalid assignment expression - this.op = 1 - ^^^^^^^ + _this.op = 1 + ^^^^^^^^ diff --git a/tests/invalid/ProcessAccess_Invalid_1.whiley b/tests/invalid/ProcessAccess_Invalid_1.whiley index 64c106eb04..6f10f01ae8 100644 --- a/tests/invalid/ProcessAccess_Invalid_1.whiley +++ b/tests/invalid/ProcessAccess_Invalid_1.whiley @@ -2,6 +2,6 @@ type etype is {int mode, ...} type Ptype is &etype -method get(Ptype this) -> int: - this.op = 1 - return this.mode +method get(Ptype _this) -> int: + _this.op = 1 + return _this.mode diff --git a/tests/invalid/ProcessAccess_Invalid_2.sysout b/tests/invalid/ProcessAccess_Invalid_2.sysout index c2528fe7f0..b54465f384 100644 --- a/tests/invalid/ProcessAccess_Invalid_2.sysout +++ b/tests/invalid/ProcessAccess_Invalid_2.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/ProcessAccess_Invalid_2.whiley:6: expected type ProcessAccess_Invalid_2:pState, found &{int x,int z} - this = new {z: 4, x: 3} - ^^^^ + _this = new {z: 4, x: 3} + ^^^^^ diff --git a/tests/invalid/ProcessAccess_Invalid_2.whiley b/tests/invalid/ProcessAccess_Invalid_2.whiley index 26169c52ef..fbade3ddf8 100644 --- a/tests/invalid/ProcessAccess_Invalid_2.whiley +++ b/tests/invalid/ProcessAccess_Invalid_2.whiley @@ -2,5 +2,5 @@ type state is {int y, int x} type pState is &state -method f(pState this) : - this = new {z: 4, x: 3} +method f(pState _this) : + _this = new {z: 4, x: 3} diff --git a/tests/invalid/ProcessAccess_Invalid_3.sysout b/tests/invalid/ProcessAccess_Invalid_3.sysout index 82800bdab2..9ab5ce1848 100644 --- a/tests/invalid/ProcessAccess_Invalid_3.sysout +++ b/tests/invalid/ProcessAccess_Invalid_3.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/ProcessAccess_Invalid_3.whiley:4: invalid assignment expression - p.data = this.data + p.data = _this.data ^^^^^^ diff --git a/tests/invalid/ProcessAccess_Invalid_3.whiley b/tests/invalid/ProcessAccess_Invalid_3.whiley index 856e6339f3..7a229e3e0c 100644 --- a/tests/invalid/ProcessAccess_Invalid_3.whiley +++ b/tests/invalid/ProcessAccess_Invalid_3.whiley @@ -1,7 +1,7 @@ type MyProc is &{int data} -method copy(MyProc this, MyProc p): - p.data = this.data +method copy(MyProc _this, MyProc p): + p.data = _this.data method create(int data) -> MyProc: return new {data: data} diff --git a/tests/invalid/Process_Invalid_1.sysout b/tests/invalid/Process_Invalid_1.sysout index 10c009a77c..9e5a7bea28 100644 --- a/tests/invalid/Process_Invalid_1.sysout +++ b/tests/invalid/Process_Invalid_1.sysout @@ -1,3 +1,3 @@ ../../tests/invalid/Process_Invalid_1.whiley:5: invalid assignment expression - this.data = d - ^^^^^^^^^ + _this.data = d + ^^^^^^^^^^ diff --git a/tests/invalid/Process_Invalid_1.whiley b/tests/invalid/Process_Invalid_1.whiley index 69f097a5c2..2ce16487f1 100644 --- a/tests/invalid/Process_Invalid_1.whiley +++ b/tests/invalid/Process_Invalid_1.whiley @@ -1,11 +1,11 @@ type MyProc1 is &{int data} type MyProc2 is &{any data} -method set(MyProc2 this, any d) : - this.data = d +method set(MyProc2 _this, any d) : + _this.data = d -method get(MyProc1 this) -> int: - return this.data +method get(MyProc1 _this) -> int: + return _this.data method create(int data) -> MyProc1: return new {data: data} diff --git a/tests/invalid/Subtype_Invalid_6.whiley b/tests/invalid/Subtype_Invalid_6.whiley index 53febce133..46d8e01bbb 100644 --- a/tests/invalid/Subtype_Invalid_6.whiley +++ b/tests/invalid/Subtype_Invalid_6.whiley @@ -1,7 +1,7 @@ type scf6nat is (int n) where n > 0 -type scf6tup is ({scf6nat f, int g} this) where this.g > this.f +type scf6tup is ({scf6nat f, int g} _this) where _this.g > _this.f function f(scf6tup x) -> int: return x.f diff --git a/tests/invalid/TupleAssign_Invalid_1.whiley b/tests/invalid/TupleAssign_Invalid_1.whiley index cab7436296..a45f58c340 100644 --- a/tests/invalid/TupleAssign_Invalid_1.whiley +++ b/tests/invalid/TupleAssign_Invalid_1.whiley @@ -1,5 +1,5 @@ -type tac1tup is ({int f1, int f2} this) where this.f1 < this.f2 +type tac1tup is ({int f1, int f2} _this) where _this.f1 < _this.f2 method main() : tac1tup x = {f1: 1, f2: 3} diff --git a/tests/invalid/TupleAssign_Invalid_2.whiley b/tests/invalid/TupleAssign_Invalid_2.whiley index d5da147024..63a20e62c1 100644 --- a/tests/invalid/TupleAssign_Invalid_2.whiley +++ b/tests/invalid/TupleAssign_Invalid_2.whiley @@ -1,7 +1,7 @@ -type tac2ta is ({int f1, int f2} this) where this.f1 < this.f2 +type tac2ta is ({int f1, int f2} _this) where _this.f1 < _this.f2 -type tac2tb is ({int f1, int f2} this) where (this.f1 + 1) < this.f2 +type tac2tb is ({int f1, int f2} _this) where (_this.f1 + 1) < _this.f2 function f(tac2tb y) -> tac2tb: return y diff --git a/tests/invalid/TupleAssign_Invalid_3.whiley b/tests/invalid/TupleAssign_Invalid_3.whiley index 2e9899f245..94e18e979c 100644 --- a/tests/invalid/TupleAssign_Invalid_3.whiley +++ b/tests/invalid/TupleAssign_Invalid_3.whiley @@ -1,5 +1,5 @@ -type tac3ta is ({int f1, int f2} this) where this.f1 < this.f2 +type tac3ta is ({int f1, int f2} _this) where _this.f1 < _this.f2 method main(): {int f1, int f2} x = {f1: 2, f2: 3} diff --git a/tests/invalid/TupleDefine_Invalid_2.whiley b/tests/invalid/TupleDefine_Invalid_2.whiley index e38aa6ec41..02c16757ed 100644 --- a/tests/invalid/TupleDefine_Invalid_2.whiley +++ b/tests/invalid/TupleDefine_Invalid_2.whiley @@ -1,4 +1,4 @@ -type point is ({int y, int x} this) where (this.x > 0) && (this.y > 0) +type point is ({int y, int x} _this) where (_this.x > 0) && (_this.y > 0) function f(point p) -> point: return p diff --git a/tests/invalid/UnionType_Invalid_7.whiley b/tests/invalid/UnionType_Invalid_7.whiley index 93362db63c..8fb42e0bc0 100644 --- a/tests/invalid/UnionType_Invalid_7.whiley +++ b/tests/invalid/UnionType_Invalid_7.whiley @@ -7,7 +7,7 @@ constant MUL is 3 constant DIV is 4 -type bop is ({int op, int rhs, int lhs} this) where ADD <= this.op && this.op <= DIV +type bop is ({int op, int rhs, int lhs} _this) where ADD <= _this.op && _this.op <= DIV function f(bop b) -> bop: return b diff --git a/tests/valid/ConstrainedList_Valid_11.whiley b/tests/valid/ConstrainedList_Valid_11.whiley index 308285eece..889a6cc037 100644 --- a/tests/valid/ConstrainedList_Valid_11.whiley +++ b/tests/valid/ConstrainedList_Valid_11.whiley @@ -1,8 +1,8 @@ type state is ({ int[] input, int pos -} this) -where (this.pos >= 0) && (this.pos <= |this.input|) +} _this) +where (_this.pos >= 0) && (_this.pos <= |_this.input|) public function isLetter(int c) -> bool: return ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') diff --git a/tests/valid/FunctionRef_Valid_12.whiley b/tests/valid/FunctionRef_Valid_12.whiley index 60c8adf291..55f9f6a422 100644 --- a/tests/valid/FunctionRef_Valid_12.whiley +++ b/tests/valid/FunctionRef_Valid_12.whiley @@ -8,7 +8,7 @@ function f(null|SizeGetter x) -> int: else: return 0 -function getSize(Sized this) -> int: +function getSize(Sized _this) -> int: return 1 public export method test(): diff --git a/tests/valid/FunctionRef_Valid_13.whiley b/tests/valid/FunctionRef_Valid_13.whiley index f1bd116b6a..5cc1361b1e 100644 --- a/tests/valid/FunctionRef_Valid_13.whiley +++ b/tests/valid/FunctionRef_Valid_13.whiley @@ -9,10 +9,10 @@ function f((SizeSetter|SizeGetter) x) -> int: else: return 0 -function getSize(Sized this) -> int: - return this.value +function getSize(Sized _this) -> int: + return _this.value -function setSize(Sized this, int value) -> Sized: +function setSize(Sized _this, int value) -> Sized: return { value: value } public export method test(): diff --git a/tests/valid/FunctionRef_Valid_7.whiley b/tests/valid/FunctionRef_Valid_7.whiley index 0b1b94696c..3a750cb6b0 100644 --- a/tests/valid/FunctionRef_Valid_7.whiley +++ b/tests/valid/FunctionRef_Valid_7.whiley @@ -2,8 +2,8 @@ type Proc is &{int data} -method read(Proc this, int x) -> int: - return x + this->data +method read(Proc _this, int x) -> int: + return x + _this->data public export method test(Proc p, int arg) -> int: return read(p,arg) diff --git a/tests/valid/FunctionRef_Valid_9.whiley b/tests/valid/FunctionRef_Valid_9.whiley index 87b6ca6335..f09ee414a6 100644 --- a/tests/valid/FunctionRef_Valid_9.whiley +++ b/tests/valid/FunctionRef_Valid_9.whiley @@ -4,11 +4,11 @@ type Proc is &{ function func(int) -> int } -method func(Proc this, int x) -> int: +method func(Proc _this, int x) -> int: return x + 1 -public export method test(Proc this, int arg) -> int: - return (*this).func(arg) +public export method test(Proc _this, int arg) -> int: + return (*_this).func(arg) function id(int x) -> int: return x diff --git a/tests/valid/Lambda_Valid_3.whiley b/tests/valid/Lambda_Valid_3.whiley index 642290eece..45224c11bd 100644 --- a/tests/valid/Lambda_Valid_3.whiley +++ b/tests/valid/Lambda_Valid_3.whiley @@ -54,8 +54,8 @@ requires amount >= 0: // Construct buffer from list of bytes public method BufferInputStream(byte[] buffer) -> InputStream: - BufferState this = new {bytes: buffer, pos: 0} - return {read: &(int x -> read(this, x))} + BufferState _this = new {bytes: buffer, pos: 0} + return {read: &(int x -> read(_this, x))} public export method test() : InputStream bis = BufferInputStream(toBytes("hello")) diff --git a/tests/valid/Lambda_Valid_4.whiley b/tests/valid/Lambda_Valid_4.whiley index 6c83a75e79..bbd54c9d50 100644 --- a/tests/valid/Lambda_Valid_4.whiley +++ b/tests/valid/Lambda_Valid_4.whiley @@ -59,10 +59,10 @@ method eof(BufferState state) -> bool: // Construct buffer from list of bytes public method BufferInputStream(byte[] buffer) -> InputStream: - BufferState this = new {bytes: buffer, pos: 0} + BufferState _this = new {bytes: buffer, pos: 0} return { - read: &(int x -> read(this, x)), - eof: &( -> eof(this)) + read: &(int x -> read(_this, x)), + eof: &( -> eof(_this)) } method read(string s) -> byte[]: diff --git a/tests/valid/Lifetime_Lambda_Valid_1.whiley b/tests/valid/Lifetime_Lambda_Valid_1.whiley new file mode 100644 index 0000000000..76d7943059 --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_1.whiley @@ -0,0 +1,5 @@ +type meth is method(&a:int, &b:int)->(&a:int) + +public export method test(): + meth m = &(&a:int x, &b:int y -> a:new 1) + m = &(&a:int x, &b:int y -> new 1) diff --git a/tests/valid/Lifetime_Lambda_Valid_2.whiley b/tests/valid/Lifetime_Lambda_Valid_2.whiley new file mode 100644 index 0000000000..247c99c467 --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_2.whiley @@ -0,0 +1,9 @@ +// Test that lifetime parameters are replaced without capturing nested parameters in return types + +type meth1 is method(&a:int, &b:int)->(&b:meth2) +type meth2 is method(&a:int, &b:int)->(int) + +public export method test(): + meth2 m2 = &(&aa:int x, &bb:int y -> *(new 1)) + meth1 m1 = &(&bb:int x, &aa:int y -> aa:new m2) + &*:meth2 m3 = m1(this:new 2, new 3) diff --git a/tests/valid/Lifetime_Lambda_Valid_3.whiley b/tests/valid/Lifetime_Lambda_Valid_3.whiley new file mode 100644 index 0000000000..dceaf4722a --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_3.whiley @@ -0,0 +1,12 @@ +// Test that variable declarations are parsed correctly +// (tricky because of headless statements and definite types) + +type myint is int + +public export method test(): + method()->(&myint) m = &(-> new 1) + &myint a = m() + &*:myint b = m() + &this:myint c = m() + myblock: + &myblock:myint d = m() diff --git a/tests/valid/Lifetime_Lambda_Valid_4.whiley b/tests/valid/Lifetime_Lambda_Valid_4.whiley new file mode 100644 index 0000000000..fe232c1b39 --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_4.whiley @@ -0,0 +1,16 @@ +// Test recursive types + +type mymethod is method(&*:mymethod)->(&a:mymethod) + +method m (&*:mymethod x) -> &a:mymethod: + return a:new &m + +public export method test(): + &mymethod x = m<*>(new &m) + mymethod xx = &(&mymethod y -> *(new y)) + xx = &(&mymethod y -> *(new y)) + &this:mymethod y = m(new &m) + mymethod yy = &(&mymethod z -> *(new z)) + yy = &(&mymethod z -> *(new z)) + a: + &a:mymethod z = m(new &m) diff --git a/tests/valid/Lifetime_Lambda_Valid_5.whiley b/tests/valid/Lifetime_Lambda_Valid_5.whiley new file mode 100644 index 0000000000..48fdc0f73c --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_5.whiley @@ -0,0 +1,6 @@ +// Test contra-variant parameter types + +public export method test(): + method(&a:int, &int)->(&int) m1 = &(&b:int x, &b:int y -> new 1) + method(&a:int, &int)->(&int) m2 = &(&b:int x, &b:int y -> new 1) + method(&a:int, &b:int)->(&a:int) m3 = &(&b:int x, &a:int y -> b:new 1) diff --git a/tests/valid/Lifetime_Lambda_Valid_6.whiley b/tests/valid/Lifetime_Lambda_Valid_6.whiley new file mode 100644 index 0000000000..7c15d2c706 --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_6.whiley @@ -0,0 +1,11 @@ +// Test co-variant return types + +public export method test(): + method(&a:int)->(&a:int) m1 = &(&b:int x -> new 1) + &int xx = m1(new 2) + assume (*xx) == 1 + method(&a:int)->(&a:int|&b:bool) m2 = &(&b:int x -> c:new true) + c: + d: + &this:bool yy = m2(c:new 1) + assume (*yy) == true diff --git a/tests/valid/Lifetime_Lambda_Valid_7.whiley b/tests/valid/Lifetime_Lambda_Valid_7.whiley new file mode 100644 index 0000000000..dd83bc5a6d --- /dev/null +++ b/tests/valid/Lifetime_Lambda_Valid_7.whiley @@ -0,0 +1,26 @@ +// Test context lifetimes + +public export method test(): + &this:int x = this:new 2 + function()->(&this:int) m1 = &(->x) + int i = *m1() + assume i == 2 + + method[this]()->(int) m2 = &[this](->*x) + i = m2() + assume i == 2 + *x = 3 + i = m2() + assume i == 3 + + a: + &a:int y = a:new 4 + method[this,a]()->(int) m3 = &[this](->*x) + i = m3() + assume i == 3 + m3 = &[this,a](->*x) + i = m3() + assume i == 3 + method[this,a]()->(int) m4 = &[this,a](->*y) + i = m4() + assume i == 4 diff --git a/tests/valid/Lifetime_Valid_1.whiley b/tests/valid/Lifetime_Valid_1.whiley new file mode 100644 index 0000000000..f63beb625c --- /dev/null +++ b/tests/valid/Lifetime_Valid_1.whiley @@ -0,0 +1,45 @@ +// test different lifetimes without subtyping + +public export method test(): + &int ptr1 = new 1 + assume (*ptr1) == 1 + + &*:int ptr2 = new 2 + assume (*ptr2) == 2 + + &int ptr3 = *:new 3 + assume (*ptr3) == 3 + + &this:int ptr4 = this:new 4 + assume (*ptr4) == 4 + + myblock: + &myblock:int ptr5 = myblock:new 5 + assume (*ptr5) == 5 + + mynestedblock: + &mynestedblock:int ptr6 = mynestedblock:new 6 + assume (*ptr6) == 6 + + &myblock:int ptr7 = myblock:new 7 + assume (*ptr7) == 7 + + &int ptr8 = *:new 8 + assume (*ptr8) == 8 + + &this:int ptr9 = this:new 9 + assume (*ptr9) == 9 + + &myblock:int ptr10 = myblock:new 10 + assume (*ptr10) == 10 + + &*:int ptr11 = *:new 11 + assume (*ptr11) == 11 + + // name should be available again + mynestedblock: + &mynestedblock:int ptr12 = mynestedblock:new 12 + assume (*ptr12) == 12 + + &this:int ptr13 = this:new 13 + assume (*ptr13) == 13 diff --git a/tests/valid/Lifetime_Valid_10.whiley b/tests/valid/Lifetime_Valid_10.whiley new file mode 100644 index 0000000000..f90fa2e80f --- /dev/null +++ b/tests/valid/Lifetime_Valid_10.whiley @@ -0,0 +1,12 @@ +// test that substitution does not accidentaly substitute already substituted values + +method m(&a:int x, &b:int y) -> &a:int: + return x + +public export method test(): + a: + b: + &a:int x = a:new 1 + &b:int y = b:new 2 + &a:int z = m(x, y) + assume x == z diff --git a/tests/valid/Lifetime_Valid_2.whiley b/tests/valid/Lifetime_Valid_2.whiley new file mode 100644 index 0000000000..106eadd561 --- /dev/null +++ b/tests/valid/Lifetime_Valid_2.whiley @@ -0,0 +1,22 @@ +// test subtyping (outlives) with different lifetimes + +public export method test(): + &this:int ptr1 = *:new 1 + assume (*ptr1) == 1 + + myblock: + &myblock:int ptr2 = this:new 2 + assume (*ptr2) == 2 + + &myblock:int ptr3 = *:new 3 + assume (*ptr3) == 3 + + mynestedblock: + &mynestedblock:int ptr4 = myblock:new 4 + assume (*ptr4) == 4 + + &mynestedblock:int ptr5 = this:new 5 + assume (*ptr5) == 5 + + &mynestedblock:int ptr6 = *:new 6 + assume (*ptr6) == 6 diff --git a/tests/valid/Lifetime_Valid_3.whiley b/tests/valid/Lifetime_Valid_3.whiley new file mode 100644 index 0000000000..755dc3a9f4 --- /dev/null +++ b/tests/valid/Lifetime_Valid_3.whiley @@ -0,0 +1,61 @@ +// test subtyping (outlives) combined with lifetime parameters + +method m(&a:int x, &b:int y, &*:int z): + &a:int ptr1 = x + ptr1 = a:new 1 + assume (*ptr1) == 1 + + &b:int ptr2 = y + ptr2 = b:new 2 + assume (*ptr2) == 2 + + &a:int ptr3 = *:new 3 + assume (*ptr3) == 3 + + &b:int ptr4 = *:new 4 + assume (*ptr4) == 4 + + &this:int ptr5 = a:new 5 + assume (*ptr5) == 5 + ptr5 = x + ptr5 = y + + &this:int ptr6 = b:new 6 + assume (*ptr6) == 6 + ptr6 = y + ptr6 = x + +public export method test(): + &this:int ptr1 = this:new 1 + assume (*ptr1) == 1 + + m(ptr1, ptr1, new 99) + + myblock: + &myblock:int ptr2 = myblock:new 2 + assume (*ptr2) == 2 + + m(ptr1, ptr2, new 99) + m(ptr2, ptr1, new 99) + m(ptr2, ptr2, new 99) + + &myblock:int ptr3 = *:new 3 + assume (*ptr3) == 3 + + m(ptr1, ptr3, new 99) + m(ptr2, ptr3, new 99) + m(ptr3, ptr1, new 99) + m(ptr3, ptr2, new 99) + m(ptr3, ptr3, new 99) + + mynestedblock: + &mynestedblock:int ptr4 = mynestedblock:new 4 + assume (*ptr4) == 4 + + m(ptr1, ptr4, new 99) + m(ptr2, ptr4, new 99) + m(ptr3, ptr4, new 99) + m(ptr4, ptr1, new 99) + m(ptr4, ptr2, new 99) + m(ptr4, ptr3, new 99) + m(ptr4, ptr4, new 99) diff --git a/tests/valid/Lifetime_Valid_4.whiley b/tests/valid/Lifetime_Valid_4.whiley new file mode 100644 index 0000000000..5b887e1d47 --- /dev/null +++ b/tests/valid/Lifetime_Valid_4.whiley @@ -0,0 +1,19 @@ +// test subtyping (outlives) for method parameters and return types + +method m(&a:int x, &a:int y) -> &*:int: + return new 3 + +public export method test(): + &this:int ptr1 = this:new 1 + &*:int ptr2 = *:new 2 + + &this:int ptr3 = m(ptr1, ptr1) + assume (*ptr3) == 3 + ptr3 = m<*>(ptr2, ptr2) + assume (*ptr3) == 3 + ptr3 = m(ptr2, ptr2) + assume (*ptr3) == 3 + ptr3 = m(ptr1, ptr2) + assume (*ptr3) == 3 + ptr3 = m(ptr2, ptr1) + assume (*ptr3) == 3 diff --git a/tests/valid/Lifetime_Valid_5.whiley b/tests/valid/Lifetime_Valid_5.whiley new file mode 100644 index 0000000000..2d85676817 --- /dev/null +++ b/tests/valid/Lifetime_Valid_5.whiley @@ -0,0 +1,34 @@ +// test lifetime substitution for method calls + +method m1(&a:int x, &b:int y) -> &a:int: + *x = (*x)+1 + &a:int result = a:new (*y) + return result + +method m2(&a:int x, &b:int y) -> &b:int: + *y = (*y)+1 + &b:int result = *:new (*x) + return result + +public export method test(): + test: + &this:int ptr1 = this:new 1 + &test:int ptr2 = test:new 2 + + &this:int ptr3 = m1(ptr1, ptr2) + assume (*ptr1) == 2 + assume (*ptr2) == 2 + assume (*ptr3) == 2 + + &test:int ptr4 = m2(ptr1, ptr2) + assume (*ptr1) == 2 + assume (*ptr2) == 3 + assume (*ptr3) == 2 + assume (*ptr4) == 2 + + &test:int ptr5 = m1(ptr2, ptr2) + assume (*ptr1) == 2 + assume (*ptr2) == 4 + assume (*ptr3) == 2 + assume (*ptr4) == 2 + assume (*ptr5) == 4 diff --git a/tests/valid/Lifetime_Valid_6.whiley b/tests/valid/Lifetime_Valid_6.whiley new file mode 100644 index 0000000000..82e433a0f3 --- /dev/null +++ b/tests/valid/Lifetime_Valid_6.whiley @@ -0,0 +1,33 @@ +// test lifetime inference without overloading + +method m1(&a:int x, &a:int y, &b:int z) -> &a:int: + return new 3 + +method m2(&a:int x, &b:int y, &b:int z) -> &b:int: + return new 4 + +public export method test(): + test: + &this:int ptr1 = this:new 1 + &test:int ptr2 = test:new 2 + &*:int ptr3 = *:new 2 + + // + &test:int ptr4 = m1(ptr1, ptr2, ptr3) + + // + &this:int ptr5 = m1(ptr1, ptr3, ptr2) + + // <*, this> + &*:int ptr6 = m1(ptr3, ptr3, ptr1) + + // -- + + // + &test:int ptr7 = m2(ptr1, ptr2, ptr3) + + // + &this:int ptr8 = m2(ptr1, ptr3, ptr1) + + // + &*:int ptr9 = m2(ptr1, ptr3, ptr3) diff --git a/tests/valid/Lifetime_Valid_7.whiley b/tests/valid/Lifetime_Valid_7.whiley new file mode 100644 index 0000000000..d934ffc401 --- /dev/null +++ b/tests/valid/Lifetime_Valid_7.whiley @@ -0,0 +1,45 @@ +// test lifetime inference with lifetime overloading but same types + +method m(&a:int x, &a:int y) -> int: + return 1 + +method m(&a:int x, &*:int y) -> int: + return 2 + +method m(&*:int x, &a:int y) -> int: + return 3 + +method m2(&a:int x, &a:int y) -> int: + return 4 + +method m2(&a:int x, &b:int y) -> int: + return 5 + +public export method test(): + test: + &this:int ptr1 = this:new 1 + &test:int ptr2 = test:new 2 + &*:int ptr3 = *:new 2 + + // variant1: (&test:int, &test:int) <-- + // variant2: no + // variant3: no + int r = m(ptr1, ptr2) + assume r == 1 + + // variant1: (&this:int, &this:int) + // variant2: no + // variant3: (&*:int, &this:int) <-- + r = m(ptr3, ptr1) + assume r == 3 + + // variant1: (&test:int, &test:int) + // variant2: (&test:int, &*:int) <-- + // variant3: no + r = m(ptr2, ptr3) + assume r == 2 + + // variant4: (&test:int, &test:int) + // variant5: (&test:int, &this:int) <-- + r = m2(ptr2, ptr3) + assume r == 5 diff --git a/tests/valid/Lifetime_Valid_8.whiley b/tests/valid/Lifetime_Valid_8.whiley new file mode 100644 index 0000000000..5ef621971e --- /dev/null +++ b/tests/valid/Lifetime_Valid_8.whiley @@ -0,0 +1,28 @@ +// test lifetime inference with lifetime overloading and different types + +method m((&a:int)|(&b:bool) x, &a:int y, bool z) -> &b:int: + return b:new 1 + +method m(&a:bool x, &a:int y, bool z) -> &a:int: + return a:new 2 + +method m(&*:int x, &a:int y, int|bool z) -> &a:int: + return a:new 3 + +method m(&*:int x, &a:int y, bool z) -> &a:int: + return a:new 4 + +public export method test(): + // variant1: ((&this:int)|(&*:bool), &this:int, bool z) + // variant2: no + // variant3: no + // variant4: no + &*:int p1 = m(this:new 1, this:new 2, true) + assume (*p1) == 1 + + // variant1: ((&this:int)|(&*:bool), &this:int, bool z) + // variant2: no + // variant3: (&*:int, &this:int, int|bool) + // variant4: (&*:int, &this:int, bool) <-- + &this:int p2 = m(*:new 1, this:new 2, true) + assume (*p2) == 4 diff --git a/tests/valid/Lifetime_Valid_9.whiley b/tests/valid/Lifetime_Valid_9.whiley new file mode 100644 index 0000000000..d9030b5a22 --- /dev/null +++ b/tests/valid/Lifetime_Valid_9.whiley @@ -0,0 +1,14 @@ +// use lifetime arguments to disambiguate (see also Lifetime_Invalid_8) + +method m((&a:int)|(&b:bool) x, (&a:int)|(&b:int) y) -> &a:int: + return a:new 1 + +public export method test(): + // --> ((&this:int)|(&*:bool), &this:int) + // <*, this> --> ((&*:int)|(&this:bool), &this:int) + (&*:int)|(&*:bool) x = *:new 1 + &this:int y = this:new 1 + + &this:int p1 = m(x, y) + &*:int p2 = m<*, this>(x, y) + &this:int p3 = m(x, y) diff --git a/tests/valid/MessageRef_Valid_1.whiley b/tests/valid/MessageRef_Valid_1.whiley index 77e1a59626..cebc90ecda 100644 --- a/tests/valid/MessageRef_Valid_1.whiley +++ b/tests/valid/MessageRef_Valid_1.whiley @@ -4,7 +4,7 @@ type MyProc is &{int position} type MyMeth is method(MyProc, int) -> int -method read(MyProc this, int x) -> int: +method read(MyProc _this, int x) -> int: return x + 123 public export method test(MyMeth m, MyProc proc) -> int: diff --git a/tests/valid/MessageRef_Valid_2.whiley b/tests/valid/MessageRef_Valid_2.whiley index 2b23331e2b..5f125209a4 100644 --- a/tests/valid/MessageRef_Valid_2.whiley +++ b/tests/valid/MessageRef_Valid_2.whiley @@ -7,8 +7,8 @@ type Reader is { method read(FileReader, int) -> int } -method read(FileReader this, int amount) -> int: - int r = amount + this->position +method read(FileReader _this, int amount) -> int: + int r = amount + _this->position return r method openReader() -> Reader: diff --git a/tests/valid/MessageSend_Valid_1.whiley b/tests/valid/MessageSend_Valid_1.whiley index 0fbb2a4a9a..9348c5b5bf 100644 --- a/tests/valid/MessageSend_Valid_1.whiley +++ b/tests/valid/MessageSend_Valid_1.whiley @@ -2,7 +2,7 @@ type MyObject is &{int field} -method f(MyObject this, int x) : +method f(MyObject _this, int x) : assume x == 1 public export method test() : diff --git a/tests/valid/MessageSend_Valid_2.whiley b/tests/valid/MessageSend_Valid_2.whiley index b1dd660be7..570b67afee 100644 --- a/tests/valid/MessageSend_Valid_2.whiley +++ b/tests/valid/MessageSend_Valid_2.whiley @@ -2,8 +2,8 @@ type Proc is &{int state} -method get(Proc this) -> int: - return this->state +method get(Proc _this) -> int: + return _this->state method f(Proc x) -> int: return get(x) diff --git a/tests/valid/MessageSend_Valid_3.whiley b/tests/valid/MessageSend_Valid_3.whiley index 208cda363b..eb8e53c094 100644 --- a/tests/valid/MessageSend_Valid_3.whiley +++ b/tests/valid/MessageSend_Valid_3.whiley @@ -2,8 +2,8 @@ type Proc is &{int state} -method get(Proc this) -> int: - return this->state +method get(Proc _this) -> int: + return _this->state method f(Proc x) -> int[]: return [1, 2, 3, get(x)] diff --git a/tests/valid/MessageSend_Valid_4.whiley b/tests/valid/MessageSend_Valid_4.whiley index 3ec5bc69b4..757cee2b2b 100644 --- a/tests/valid/MessageSend_Valid_4.whiley +++ b/tests/valid/MessageSend_Valid_4.whiley @@ -4,8 +4,8 @@ type wmcr6tup is {int y, int x} type Proc is &{int state} -method get(Proc this) -> int: - return this->state +method get(Proc _this) -> int: + return _this->state method f(Proc x, int y) -> wmcr6tup: return {y: get(x), x: y} diff --git a/tests/valid/MessageSend_Valid_5.whiley b/tests/valid/MessageSend_Valid_5.whiley index 6c3a585f85..937e5804b0 100644 --- a/tests/valid/MessageSend_Valid_5.whiley +++ b/tests/valid/MessageSend_Valid_5.whiley @@ -2,17 +2,17 @@ type Sum is &{int result, int[] items} -method start(Sum this) : +method start(Sum _this) : int sum = 0 int i = 0 - int[] items = this->items + int[] items = _this->items while i < |items| where i >= 0: sum = sum + items[i] i = i + 1 - this->result = sum + _this->result = sum -method get(Sum this) -> int: - return this->result +method get(Sum _this) -> int: + return _this->result method create(int[] items) -> Sum: return new {result: 0, items: items} diff --git a/tests/valid/MethodCall_Valid_4.whiley b/tests/valid/MethodCall_Valid_4.whiley index 8f0c884410..75c14a92f7 100644 --- a/tests/valid/MethodCall_Valid_4.whiley +++ b/tests/valid/MethodCall_Valid_4.whiley @@ -1,16 +1,16 @@ type Sum is &{int result, int[] items} -method start(Sum this) : +method start(Sum _this) : int sum = 0 int i = 0 - int[] items = this->items + int[] items = _this->items while i < |items| where i >= 0: sum = sum + items[i] i = i + 1 - this->result = sum + _this->result = sum -method get(Sum this) -> int: - return this->result +method get(Sum _this) -> int: + return _this->result method create(int[] items) -> Sum: return new {result: 0, items: items} diff --git a/tests/valid/ProcessAccess_Valid_1.whiley b/tests/valid/ProcessAccess_Valid_1.whiley index e76b483646..603e56f483 100644 --- a/tests/valid/ProcessAccess_Valid_1.whiley +++ b/tests/valid/ProcessAccess_Valid_1.whiley @@ -1,10 +1,10 @@ type etype is {int rest, int mode} type Ptype is &etype -method get(Ptype this) -> int: - this->mode = 1 - this->rest = 123 - return this->mode +method get(Ptype _this) -> int: + _this->mode = 1 + _this->rest = 123 + return _this->mode public export method test() : Ptype p = new {rest: 2, mode: 2} diff --git a/tests/valid/ProcessAccess_Valid_2.whiley b/tests/valid/ProcessAccess_Valid_2.whiley index 3176f7fd62..88c6b5501f 100644 --- a/tests/valid/ProcessAccess_Valid_2.whiley +++ b/tests/valid/ProcessAccess_Valid_2.whiley @@ -2,9 +2,9 @@ type state is {int y, int x} type pState is &state -method send(pState this, int z) : - assume this->x == 1 - assume this->y == 2 +method send(pState _this, int z) : + assume _this->x == 1 + assume _this->y == 2 assume z == 1 public export method test() : diff --git a/tests/valid/Process_Valid_1.whiley b/tests/valid/Process_Valid_1.whiley index 6b9c87512e..b1506efaec 100644 --- a/tests/valid/Process_Valid_1.whiley +++ b/tests/valid/Process_Valid_1.whiley @@ -4,10 +4,10 @@ type state is {int y, int x} type pState is &state -method send(pState this, int x) : - this->x = x - assert this->x == x - assume (*this) == {x: 3, y: 2} +method send(pState _this, int x) : + _this->x = x + assert _this->x == x + assume (*_this) == {x: 3, y: 2} public export method test() : pState ps = new {y: 2, x: 1} diff --git a/tests/valid/Process_Valid_10.whiley b/tests/valid/Process_Valid_10.whiley index 519ece4278..a21b1238eb 100644 --- a/tests/valid/Process_Valid_10.whiley +++ b/tests/valid/Process_Valid_10.whiley @@ -2,16 +2,16 @@ type Queue is {int[] items, int length} -method get(&Queue this) -> int: - this->length = this->length - 1 - return this->items[this->length] +method get(&Queue _this) -> int: + _this->length = _this->length - 1 + return _this->items[_this->length] -method put(&Queue this, int item) : - this->items[this->length] = item - this->length = this->length + 1 +method put(&Queue _this, int item) : + _this->items[_this->length] = item + _this->length = _this->length + 1 -method isEmpty(&Queue this) -> bool: - return this->length == 0 +method isEmpty(&Queue _this) -> bool: + return _this->length == 0 public export method test() : int[] items = [1, 2, 3, 4, 5] diff --git a/tests/valid/Process_Valid_11.whiley b/tests/valid/Process_Valid_11.whiley index bbc7f6ccf5..3e7b97fb7f 100644 --- a/tests/valid/Process_Valid_11.whiley +++ b/tests/valid/Process_Valid_11.whiley @@ -4,8 +4,8 @@ type state is ({int y, int x} s) where s.x < s.y type pState is &state -method send2(pState this, int x) -> int: - return this->x + this->y +method send2(pState _this, int x) -> int: + return _this->x + _this->y public export method test() : int x = send2(new {y: 2, x: 1},1) diff --git a/tests/valid/Process_Valid_12.whiley b/tests/valid/Process_Valid_12.whiley index 9c694dfe78..5f1389995b 100644 --- a/tests/valid/Process_Valid_12.whiley +++ b/tests/valid/Process_Valid_12.whiley @@ -4,8 +4,8 @@ type state is {int y, int x} type pState is &state -method send2(pState this, int x) -> int: - return this->x + this->y +method send2(pState _this, int x) -> int: + return _this->x + _this->y public export method test() : int x = send2(new {y: 2, x: 1},1) diff --git a/tests/valid/Process_Valid_4.whiley b/tests/valid/Process_Valid_4.whiley index 882c1a2c94..896d829ca3 100644 --- a/tests/valid/Process_Valid_4.whiley +++ b/tests/valid/Process_Valid_4.whiley @@ -2,8 +2,8 @@ type MyProc is &{int x} -method inc(MyProc this, int i) : - this->x = this->x + i +method inc(MyProc _this, int i) : + _this->x = _this->x + i public export method test() : MyProc mproc = new {x: 1} diff --git a/tests/valid/Process_Valid_5.whiley b/tests/valid/Process_Valid_5.whiley index 704d1647dd..0392e3e483 100644 --- a/tests/valid/Process_Valid_5.whiley +++ b/tests/valid/Process_Valid_5.whiley @@ -2,8 +2,8 @@ type MyProc is &{bool flag} -method run(MyProc this) -> bool: - if this->flag: +method run(MyProc _this) -> bool: + if _this->flag: return true else: return false diff --git a/tests/valid/Process_Valid_6.whiley b/tests/valid/Process_Valid_6.whiley index 02b7c048ed..c5550c113c 100644 --- a/tests/valid/Process_Valid_6.whiley +++ b/tests/valid/Process_Valid_6.whiley @@ -1,7 +1,7 @@ type Actor is {int data} -method get(&Actor this) -> int: - return this->data +method get(&Actor _this) -> int: + return _this->data method createActor(int n) -> &Actor: return new {data: n} diff --git a/tests/valid/Process_Valid_7.whiley b/tests/valid/Process_Valid_7.whiley index 22af37a9e9..22b9b0fa35 100644 --- a/tests/valid/Process_Valid_7.whiley +++ b/tests/valid/Process_Valid_7.whiley @@ -2,11 +2,11 @@ type MyProc2 is &{any data} -method set(MyProc2 this, int d) : - this->data = (any)d +method set(MyProc2 _this, int d) : + _this->data = (any)d -method get(MyProc2 this) -> any: - return this->data +method get(MyProc2 _this) -> any: + return _this->data method create(any data) -> MyProc2: return new {data: data} diff --git a/tests/valid/Process_Valid_8.whiley b/tests/valid/Process_Valid_8.whiley index 09fa89bf9c..acc9944953 100644 --- a/tests/valid/Process_Valid_8.whiley +++ b/tests/valid/Process_Valid_8.whiley @@ -2,11 +2,11 @@ type MyProc2 is {any data} -method set(&MyProc2 this, int d) : - this->data = (any)d +method set(&MyProc2 _this, int d) : + _this->data = (any)d -method get(&MyProc2 this) -> any: - return this->data +method get(&MyProc2 _this) -> any: + return _this->data method create(any data) -> &MyProc2: return new {data: data} diff --git a/tests/valid/Process_Valid_9.whiley b/tests/valid/Process_Valid_9.whiley index 40116c4351..f2da3306ab 100644 --- a/tests/valid/Process_Valid_9.whiley +++ b/tests/valid/Process_Valid_9.whiley @@ -1,15 +1,15 @@ type Queue is {int[] items, int length} -method get(&Queue this) -> int: - this->length = this->length - 1 - return this->items[this->length] +method get(&Queue _this) -> int: + _this->length = _this->length - 1 + return _this->items[_this->length] -method put(&Queue this, int item) : - this->items[this->length] = item - this->length = this->length + 1 +method put(&Queue _this, int item) : + _this->items[_this->length] = item + _this->length = _this->length + 1 -method isEmpty(&Queue this) -> bool: - return this->length == 0 +method isEmpty(&Queue _this) -> bool: + return _this->length == 0 method Queue(int capacity) -> &Queue: int[] slots = [0; capacity] diff --git a/tests/valid/RecordAccess_Valid_1.whiley b/tests/valid/RecordAccess_Valid_1.whiley index 1ace8158aa..47386ff15e 100644 --- a/tests/valid/RecordAccess_Valid_1.whiley +++ b/tests/valid/RecordAccess_Valid_1.whiley @@ -4,9 +4,9 @@ type etype is {int mode, ...} type Ptype is &etype -method get(Ptype this) -> int: - this->mode = 1 - return this->mode +method get(Ptype _this) -> int: + _this->mode = 1 + return _this->mode public export method test() : assume get(new (etype) {mode:2}) == 1 diff --git a/tests/valid/RecordAssign_Valid_1.whiley b/tests/valid/RecordAssign_Valid_1.whiley index fa83a8f147..8986b1febe 100644 --- a/tests/valid/RecordAssign_Valid_1.whiley +++ b/tests/valid/RecordAssign_Valid_1.whiley @@ -1,6 +1,6 @@ -type tac1tup is ({int f1, int f2} this) where this.f1 < this.f2 +type tac1tup is ({int f1, int f2} _this) where _this.f1 < _this.f2 function f() -> tac1tup: return {f1: 2, f2: 3} diff --git a/tests/valid/RecordAssign_Valid_4.whiley b/tests/valid/RecordAssign_Valid_4.whiley index 70691fe9f6..f0d903b810 100644 --- a/tests/valid/RecordAssign_Valid_4.whiley +++ b/tests/valid/RecordAssign_Valid_4.whiley @@ -1,8 +1,8 @@ -type tac2ta is ({int f1, int f2} this) where this.f1 < this.f2 +type tac2ta is ({int f1, int f2} _this) where _this.f1 < _this.f2 -type tac2tb is ({int f1, int f2} this) where (this.f1 + 1) < this.f2 +type tac2tb is ({int f1, int f2} _this) where (_this.f1 + 1) < _this.f2 function f(tac2ta x) -> tac2tb: return {f1: x.f1 - 1, f2: x.f2} diff --git a/tests/valid/RecursiveType_Valid_11.whiley b/tests/valid/RecursiveType_Valid_11.whiley index dcc8a92fa2..bceb5b8a1d 100644 --- a/tests/valid/RecursiveType_Valid_11.whiley +++ b/tests/valid/RecursiveType_Valid_11.whiley @@ -5,8 +5,8 @@ constant SUB is 2 constant MUL is 3 constant DIV is 4 -type binop is ({int op, expr left, expr right} this) -where this.op == ADD || this.op == SUB || this.op == MUL || this.op == DIV +type binop is ({int op, expr left, expr right} _this) +where _this.op == ADD || _this.op == SUB || _this.op == MUL || _this.op == DIV type expr is int | binop diff --git a/tests/valid/RecursiveType_Valid_12.whiley b/tests/valid/RecursiveType_Valid_12.whiley index 0bbc51fe26..bc6f787770 100644 --- a/tests/valid/RecursiveType_Valid_12.whiley +++ b/tests/valid/RecursiveType_Valid_12.whiley @@ -2,8 +2,8 @@ type Tree is null | Node -type Node is ({int data, Tree rhs, Tree lhs} this) -where ((this.lhs == null) || (this.lhs.data < this.data)) && ((this.rhs == null) || (this.rhs.data > this.data)) +type Node is ({int data, Tree rhs, Tree lhs} _this) +where ((_this.lhs == null) || (_this.lhs.data < _this.data)) && ((_this.rhs == null) || (_this.rhs.data > _this.data)) function Tree(int data, Tree left, Tree right) -> Tree requires ((left == null) || (left.data < data)) && ((right == null) || (right.data > data)): diff --git a/tests/valid/RecursiveType_Valid_14.whiley b/tests/valid/RecursiveType_Valid_14.whiley index b7081a2a68..90b46251c9 100644 --- a/tests/valid/RecursiveType_Valid_14.whiley +++ b/tests/valid/RecursiveType_Valid_14.whiley @@ -8,9 +8,9 @@ constant MUL is 3 constant DIV is 4 -type binop is ({int op, Expr left, Expr right} this) where this.op == ADD || this.op == SUB || this.op == MUL || this.op == DIV +type binop is ({int op, Expr left, Expr right} _this) where _this.op == ADD || _this.op == SUB || _this.op == MUL || _this.op == DIV -type asbinop is ({int op, Expr left, Expr right} this) where this.op == ADD || this.op == SUB +type asbinop is ({int op, Expr left, Expr right} _this) where _this.op == ADD || _this.op == SUB type Expr is int | binop diff --git a/tests/valid/RecursiveType_Valid_22.whiley b/tests/valid/RecursiveType_Valid_22.whiley index 3370cc3146..cccf5b7b09 100644 --- a/tests/valid/RecursiveType_Valid_22.whiley +++ b/tests/valid/RecursiveType_Valid_22.whiley @@ -2,8 +2,8 @@ type SortedList is null | SortedListNode -type SortedListNode is ({SortedList next, int data} this) -where (this.next == null) || (this.data < this.next.data) +type SortedListNode is ({SortedList next, int data} _this) +where (_this.next == null) || (_this.data < _this.next.data) function SortedList(int head, SortedList tail) -> SortedList requires (tail == null) || (head < tail.data): diff --git a/tests/valid/UnionType_Valid_18.whiley b/tests/valid/UnionType_Valid_18.whiley index a4ee1305e8..a49db53a19 100644 --- a/tests/valid/UnionType_Valid_18.whiley +++ b/tests/valid/UnionType_Valid_18.whiley @@ -4,7 +4,7 @@ type utr12nat is (int x) where x >= 0 type intList is utr12nat | int[] -type tupper is ({int op, intList il} this) where (this.op >= 0) && (this.op <= 5) +type tupper is ({int op, intList il} _this) where (_this.op >= 0) && (_this.op <= 5) function f(tupper y) -> (int result) ensures result >= 0: