From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Source/Dafny/Resolver.ssc | 1419 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1419 insertions(+) create mode 100644 Source/Dafny/Resolver.ssc (limited to 'Source/Dafny/Resolver.ssc') diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc new file mode 100644 index 00000000..66cdabe1 --- /dev/null +++ b/Source/Dafny/Resolver.ssc @@ -0,0 +1,1419 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using Microsoft.Contracts; + +namespace Microsoft.Dafny { + public class Resolver { + public int ErrorCount = 0; + void Error(Token! tok, string! msg, params object[] args) { + ConsoleColor col = Console.ForegroundColor; + Console.ForegroundColor = ConsoleColor.Red; + Console.WriteLine("{0}({1},{2}): Error: {3}", + tok.filename, tok.line, tok.col-1, + string.Format(msg, args)); + Console.ForegroundColor = col; + ErrorCount++; + } + void Error(Declaration! d, string! msg, params object[] args) { + Error(d.tok, msg, args); + } + void Error(Statement! s, string! msg, params object[] args) { + Error(s.Tok, msg, args); + } + void Error(NonglobalVariable! v, string! msg, params object[] args) { + Error(v.tok, msg, args); + } + void Error(Expression! e, string! msg, params object[] args) { + Error(e.tok, msg, args); + } + + readonly Dictionary! classes = new Dictionary(); + readonly Dictionary!>! classMembers = new Dictionary!>(); + + public void ResolveProgram(Program! prog) { + foreach (ClassDecl cl in prog.Classes) { + // register the class name + if (classes.ContainsKey(cl.Name)) { + Error(cl, "Duplicate class name: {0}", cl.Name); + } else { + classes.Add(cl.Name, cl); + } + + // register the names of the class members + Dictionary members = new Dictionary(); + classMembers.Add(cl, members); + + foreach (MemberDecl m in cl.Members) { + if (members.ContainsKey(m.Name)) { + Error(m, "Duplicate member name: {0}", m.Name); + } else { + members.Add(m.Name, m); + } + } + } + + // resolve each class + foreach (ClassDecl cl in prog.Classes) { + allTypeParameters.PushMarker(); + ResolveTypeParameters(cl.TypeArgs, true, cl); + ResolveClassMemberTypes(cl); + allTypeParameters.PopMarker(); + } + foreach (ClassDecl cl in prog.Classes) { + allTypeParameters.PushMarker(); + ResolveTypeParameters(cl.TypeArgs, false, cl); + ResolveClassMemberBodies(cl); + allTypeParameters.PopMarker(); + } + } + + ClassDecl currentClass; + readonly Scope! allTypeParameters = new Scope(); + readonly Scope! scope = new Scope(); + readonly Scope! labeledStatements = new Scope(); + + /// + /// Assumes type parameters have already been pushed + /// + void ResolveClassMemberTypes(ClassDecl! cl) + requires currentClass == null; + ensures currentClass == null; + { + currentClass = cl; + foreach (MemberDecl member in cl.Members) { + member.EnclosingClass = cl; + if (member is Field) { + ResolveType(((Field)member).Type); + + } else if (member is Function) { + Function f = (Function)member; + allTypeParameters.PushMarker(); + ResolveTypeParameters(f.TypeArgs, true, f); + ResolveFunctionSignature(f); + allTypeParameters.PopMarker(); + + } else if (member is Method) { + Method m = (Method)member; + allTypeParameters.PushMarker(); + ResolveTypeParameters(m.TypeArgs, true, m); + ResolveMethodSignature(m); + allTypeParameters.PopMarker(); + + } else { + assert false; // unexpected member type + } + } + currentClass = null; + } + + /// + /// Assumes type parameters have already been pushed, and that all types in class members have been resolved + /// + void ResolveClassMemberBodies(ClassDecl! cl) + requires currentClass == null; + ensures currentClass == null; + { + ResolveAttributes(cl.Attributes, false); + currentClass = cl; + foreach (MemberDecl member in cl.Members) { + ResolveAttributes(member.Attributes, false); + if (member is Field) { + // nothing more to do + + } else if (member is Function) { + Function f = (Function)member; + allTypeParameters.PushMarker(); + ResolveTypeParameters(f.TypeArgs, false, f); + ResolveFunction(f); + allTypeParameters.PopMarker(); + + } else if (member is Method) { + Method m = (Method)member; + allTypeParameters.PushMarker(); + ResolveTypeParameters(m.TypeArgs, false, m); + ResolveMethod(m); + allTypeParameters.PopMarker(); + + } else { + assert false; // unexpected member type + } + } + currentClass = null; + } + + void ResolveAttributes(Attributes attrs, bool twoState) { + // order does not matter for resolution, so resolve them in reverse order + for (; attrs != null; attrs = attrs.Prev) { + foreach (Attributes.Argument aa in attrs.Args) { + if (aa.E != null) { + ResolveExpression(aa.E, twoState); + } + } + } + } + + void ResolveTriggers(Triggers trigs, bool twoState) { + // order does not matter for resolution, so resolve them in reverse order + for (; trigs != null; trigs = trigs.Prev) { + foreach (Expression e in trigs.Terms) { + ResolveExpression(e, twoState); + } + } + } + + void ResolveTypeParameters(List! tparams, bool emitErrors, TypeParameter.ParentType! parent) { + // push non-duplicated type parameter names + foreach (TypeParameter tp in tparams) { + if (emitErrors) { + // we're seeing this TypeParameter for the first time + tp.Parent = parent; + } + if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) { + Error(tp, "Duplicate type-parameter name: {0}", tp.Name); + } + } + } + + /// + /// Assumes type parameters have already been pushed + /// + void ResolveFunctionSignature(Function! f) { + scope.PushMarker(); + foreach (Formal p in f.Formals) { + if (!scope.Push(p.Name, p)) { + Error(p, "Duplicate parameter name: {0}", p.Name); + } + ResolveType(p.Type); + } + ResolveType(f.ResultType); + scope.PopMarker(); + } + + /// + /// Assumes type parameters have already been pushed + /// + void ResolveFunction(Function! f) { + scope.PushMarker(); + foreach (Formal p in f.Formals) { + scope.Push(p.Name, p); + } + foreach (Expression r in f.Req) { + ResolveExpression(r, false); + assert r.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(r.Type, Type.Bool)) { + Error(r, "Precondition must be a boolean (got {0})", r.Type); + } + } + foreach (Expression r in f.Reads) { + ResolveExpression(r, false); + Type t = r.Type; + assert t != null; // follows from postcondition of ResolveExpression + if (t is CollectionType) { + t = ((CollectionType)t).Arg; + } + if (t is ObjectType) { + // fine + } else if (ClassType.DenotesClass(t) != null) { + // fine + } else { + Error(r, "a reads-clause expression must denote an object or a collection of objects (instead got {0})", r.Type); + } + } + if (f.Body != null) { + ResolveExpression(f.Body, false); + assert f.Body.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(f.Body.Type, f.ResultType)) { + Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type); + } + } + scope.PopMarker(); + } + + /// + /// Assumes type parameters have already been pushed + /// + void ResolveMethodSignature(Method! m) { + scope.PushMarker(); + // resolve in-parameters + foreach (Formal p in m.Ins) { + if (!scope.Push(p.Name, p)) { + Error(p, "Duplicate parameter name: {0}", p.Name); + } + ResolveType(p.Type); + } + // resolve out-parameters + foreach (Formal p in m.Outs) { + if (!scope.Push(p.Name, p)) { + Error(p, "Duplicate parameter name: {0}", p.Name); + } + ResolveType(p.Type); + } + scope.PopMarker(); + } + + /// + /// Assumes type parameters have already been pushed + /// + void ResolveMethod(Method! m) { + // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported + scope.PushMarker(); + foreach (Formal p in m.Ins) { + scope.Push(p.Name, p); + } + + // Start resolving specification... + foreach (MaybeFreeExpression e in m.Req) { + ResolveExpression(e.E, false); + assert e.E.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.E.Type, Type.Bool)) { + Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type); + } + } + foreach (Expression e in m.Mod) { + ResolveExpression(e, false); + Type t = e.Type; + assert t != null; // follows from postcondition of ResolveExpression + if (t is CollectionType) { + t = ((CollectionType)t).Arg; + } + if (t is ObjectType) { + // fine + } else if (ClassType.DenotesClass(t) != null) { + // fine + } else { + Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type); + } + } + + // Add out-parameters to the scope, but don't care about any duplication errors, since they have already been reported + foreach (Formal p in m.Outs) { + scope.Push(p.Name, p); + } + + // ... continue resolving specification + foreach (MaybeFreeExpression e in m.Ens) { + ResolveExpression(e.E, true); + assert e.E.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.E.Type, Type.Bool)) { + Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); + } + } + + // Resolve body + if (m.Body != null) { + ResolveStatement(m.Body); + } + + scope.PopMarker(); + } + + public void ResolveType(Type! type) { + if (type is BasicType) { + // nothing to resolve + } else if (type is CollectionType) { + ResolveType(((CollectionType)type).Arg); + } else if (type is ClassType) { + ClassType t = (ClassType)type; + foreach (Type tt in t.TypeArgs) { + ResolveType(tt); + } + TypeParameter tp = allTypeParameters.Find(t.Name); + if (tp != null) { + if (t.TypeArgs.Count == 0) { + t.ResolvedParam = tp; + } else { + Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name); + } + } else { + ClassDecl cl; + if (!classes.TryGetValue(t.Name, out cl)) { + Error(t.tok, "Undeclared class type or type parameter: {0}", t.Name); + } else if (((!)cl).TypeArgs.Count == t.TypeArgs.Count) { + t.ResolvedClass = cl; + } else { + Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class: {2}", t.TypeArgs.Count, cl.TypeArgs.Count, t.Name); + } + } + + } else if (type is TypeProxy) { + TypeProxy t = (TypeProxy)type; + if (t.T != null) { + ResolveType(t.T); + } + + } else { + assert false; // unexpected type + } + } + + public bool UnifyTypes(Type! a, Type! b) { + while (a is TypeProxy) { + TypeProxy proxy = (TypeProxy)a; + if (proxy.T == null) { + // merge a and b; to avoid cycles, first get to the bottom of b + while (b is TypeProxy && ((TypeProxy)b).T != null) { + b = ((TypeProxy)b).T; + } + return AssignProxy(proxy, b); + } else { + a = proxy.T; + } + } + + while (b is TypeProxy) { + TypeProxy proxy = (TypeProxy)b; + if (proxy.T == null) { + // merge a and b (we have already got to the bottom of a) + return AssignProxy(proxy, a); + } else { + b = proxy.T; + } + } + +#if !NO_CHEAP_OBJECT_WORKAROUND + if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack + // allow anything with object; this is BOGUS + return true; + } +#endif + // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively. + + if (a is BoolType) { + return b is BoolType; + } else if (a is IntType) { + return b is IntType; + } else if (a is ObjectType) { + return b is ObjectType; + } else if (a is SetType) { + return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg); + } else if (a is SeqType) { + return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg); + } else if (a is ClassType) { + if (!(b is ClassType)) { + return false; + } + ClassType aa = (ClassType)a; + ClassType bb = (ClassType)b; + if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) { + // these are both resolved class types + assert aa.TypeArgs.Count == bb.TypeArgs.Count; + bool successSoFar = true; + for (int i = 0; i < aa.TypeArgs.Count; i++) { + if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) { + successSoFar = false; + } + } + return successSoFar; + } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { + // these are both resolved type parameters + assert aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0; + return true; + } else { + // something is wrong; either aa or bb wasn't properly resolved, or they don't unify + return false; + } + + } else { + assert false; // unexpected type + } + } + + bool AssignProxy(TypeProxy! proxy, Type! t) + requires proxy.T == null; + requires t is TypeProxy ==> ((TypeProxy)t).T == null; + modifies proxy.T, ((TypeProxy)t).T; // might also change t.T if t is a proxy + ensures result ==> proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null); + { + if (proxy == t) { + // they are already in the same equivalence class + return true; + + } else if (proxy is UnrestrictedTypeProxy) { + // it's fine to redirect proxy to t (done below) + + } else if (t is UnrestrictedTypeProxy) { + // merge proxy and t by redirecting t to proxy, rather than the other way around + ((TypeProxy)t).T = proxy; + return true; + + } else if (t is RestrictedTypeProxy) { + // Both proxy and t are restricted type proxies. To simplify unification, order proxy and t + // according to their types. + RestrictedTypeProxy r0 = (RestrictedTypeProxy)proxy; + RestrictedTypeProxy r1 = (RestrictedTypeProxy)t; + if (r0.OrderID <= r1.OrderID) { + return AssignRestrictedProxies(r0, r1); + } else { + return AssignRestrictedProxies(r1, r0); + } + + // In the remaining cases, proxy is a restricted proxy and t is a non-proxy + } else if (proxy is ObjectTypeProxy) { + if (t is ObjectType || ClassType.DenotesClass(t) != null) { + // all is fine, proxy can be redirected to t + } else { + return false; + } + + } else if (proxy is ObjectsTypeProxy) { + if (t is ObjectType || ClassType.DenotesClass(t) != null) { + // all is good + } else if (t is CollectionType) { + proxy.T = new CollectionTypeProxy(new ObjectTypeProxy()); + return UnifyTypes(proxy.T, t); + } + + } else if (proxy is CollectionTypeProxy) { + CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy; + if (t is CollectionType) { + if (!UnifyTypes(collProxy.Arg, ((CollectionType)t).Arg)) { + return false; + } + } else { + return false; + } + + } else if (proxy is OperationTypeProxy) { + OperationTypeProxy opProxy = (OperationTypeProxy)proxy; + if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) { + // this is the expected case + } else { + return false; + } + + } else { + assert false; // unexpected proxy type + } + + // do the merge + proxy.T = t; + return true; + } + + bool AssignRestrictedProxies(RestrictedTypeProxy! a, RestrictedTypeProxy! b) + requires a != b; + requires a.T == null && b.T == null; + requires a.OrderID <= b.OrderID; + modifies a.T, b.T; + ensures result ==> a.T != null || b.T != null; + { + if (a is ObjectTypeProxy) { + if (b is ObjectTypeProxy) { + // all is fine + a.T = b; + return true; + } else if (b is ObjectsTypeProxy) { + // unify a and b by redirecting b to a, since a gives the stronger requirement + b.T = a; + return true; + } else { + return false; + } + + } else if (a is ObjectsTypeProxy) { + if (b is ObjectsTypeProxy) { + // fine + a.T = b; + return true; + } else if (b is CollectionTypeProxy) { + // fine provided b's collection-element-type can be unified with object or a class type + a.T = new ObjectTypeProxy(); + return UnifyTypes(a.T, ((CollectionTypeProxy)b).Arg); + } else if (b is OperationTypeProxy) { + // fine; restrict a to sets of object/class, and restrict b to set/seq of object/class + if (((OperationTypeProxy)b).AllowSeq) { + a.T = new CollectionTypeProxy(new ObjectTypeProxy()); + b.T = a.T; + } else { + a.T = new SetType(new ObjectTypeProxy()); + b.T = a.T; + } + return true; + } else { + assert false; // unexpected restricted-proxy type + } + + } else if (a is CollectionTypeProxy) { + if (b is CollectionTypeProxy) { + a.T = b; + return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg); + } else if (b is OperationTypeProxy) { + if (((OperationTypeProxy)b).AllowSeq) { + b.T = a; // a is a stronger constraint than b + } else { + // a says set,seq and b says int,set; the intersection is set + a.T = new SetType(((CollectionTypeProxy)a).Arg); + b.T = a.T; + } + return true; + } else { + assert false; // unexpected restricted-proxy type + } + + } else if (a is OperationTypeProxy) { + assert b is OperationTypeProxy; // else we we have unexpected restricted-proxy type + if (((OperationTypeProxy)a).AllowSeq ==> ((OperationTypeProxy)b).AllowSeq) { + b.T = a; + } else { + a.T = b; // b has the stronger requirement + } + return true; + + } else { + assert false; // unexpected restricted-proxy type + } + } + + public void ResolveStatement(Statement! stmt) + requires !(stmt is LabelStmt); // these should be handled inside lists of statements + { + if (stmt is UseStmt) { + UseStmt s = (UseStmt)stmt; + ResolveExpression(s.Expr, true); + assert s.Expr.Type != null; // follows from postcondition of ResolveExpression + Expression expr = s.Expr; + while (true) { + if (expr is OldExpr) { + expr = ((OldExpr)expr).E; + } else { + break; + } + } + FunctionCallExpr fce = expr as FunctionCallExpr; + if (fce == null || fce.Function == null || !fce.Function.Use) { + Error(s.Expr, "use statement must indicate a function declared as use"); + } + } else if (stmt is PredicateStmt) { + PredicateStmt s = (PredicateStmt)stmt; + ResolveExpression(s.Expr, true); + assert s.Expr.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Expr.Type, Type.Bool)) { + Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type); + } + + } else if (stmt is BreakStmt) { + BreakStmt s = (BreakStmt)stmt; + if (s.TargetLabel != null) { + Statement target = labeledStatements.Find(s.TargetLabel); + if (target == null) { + Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel); + } else { + s.TargetStmt = target; + } + } + + } else if (stmt is ReturnStmt) { + // nothing to resolve + + } else if (stmt is AssignStmt) { + AssignStmt s = (AssignStmt)stmt; + ResolveExpression(s.Lhs, true); + assert s.Lhs.Type != null; // follows from postcondition of ResolveExpression + // check that LHS denotes a mutable variable or a field + if (s.Lhs is IdentifierExpr) { + IVariable var = ((IdentifierExpr)s.Lhs).Var; + if (var == null) { + // the LHS didn't resolve correctly; some error would already have been reported + } else if (!var.IsMutable) { + Error(stmt, "LHS of assignment must denote a mutable variable or field"); + } + } else if (s.Lhs is FieldSelectExpr) { + // LHS is fine, but restrict the RHS to ExprRhs + if (!(s.Rhs is ExprRhs)) { + Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable"); + } + } else { + Error(stmt, "LHS of assignment must denote a mutable variable or field"); + } + + if (s.Rhs is ExprRhs) { + ExprRhs rr = (ExprRhs)s.Rhs; + ResolveExpression(rr.Expr, true); + assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Lhs.Type, rr.Expr.Type)) { + Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type); + } + } else if (s.Rhs is TypeRhs) { + TypeRhs rr = (TypeRhs)s.Rhs; + ResolveType(rr.Type); + if (!UnifyTypes(s.Lhs.Type, rr.Type)) { + Error(stmt, "type {0} is not assignable to LHS (of type {1})", rr.Type, s.Lhs.Type); + } + } else if (s.Rhs is HavocRhs) { + // nothing else to do + } else { + assert false; // unexpected RHS + } + + } else if (stmt is VarDecl) { + VarDecl s = (VarDecl)stmt; + if (s.OptionalType != null) { + ResolveType(s.OptionalType); + s.type = s.OptionalType; + } + if (s.Rhs != null) { + Type! rhsType; + if (s.Rhs is ExprRhs) { + ExprRhs rr = (ExprRhs)s.Rhs; + ResolveExpression(rr.Expr, true); + assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression + rhsType = rr.Expr.Type; + } else if (s.Rhs is TypeRhs) { + TypeRhs rr = (TypeRhs)s.Rhs; + ResolveType(rr.Type); + rhsType = rr.Type; + } else { + assert false; // unexpected RHS + } + if (s.OptionalType == null) { + s.type = rhsType; + } else if (!UnifyTypes(s.OptionalType, rhsType)) { + Error(stmt, "initialization RHS (of type {0}) not assignable to variable (of type {1})", rhsType, s.OptionalType); + } + } + // now that the declaration has been processed, add the name to the scope + if (!scope.Push(s.Name, s)) { + Error(s, "Duplicate local-variable name: {0}", s.Name); + } + + } else if (stmt is CallStmt) { + CallStmt s = (CallStmt)stmt; + + // resolve left-hand side + Dictionary lhsNameSet = new Dictionary(); + foreach (IdentifierExpr lhs in s.Lhs) { + ResolveExpression(lhs, true); + if (lhsNameSet.ContainsKey(lhs.Name)) { + Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name); + } else { + lhsNameSet.Add(lhs.Name, null); + } + } + // resolve receiver + ResolveExpression(s.Receiver, true); + assert s.Receiver.Type != null; // follows from postcondition of ResolveExpression + // resolve arguments + foreach (Expression e in s.Args) { + ResolveExpression(e, true); + } + + // resolve the method name + ClassType ctype; + MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype); + if (member == null) { + // error has already been reported by ResolveMember + } else if (!(member is Method)) { + Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name); + } else { + Method method = (Method)member; + s.Method = method; + if (method.Ins.Count != s.Args.Count) { + Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count); + } else if (method.Outs.Count != s.Lhs.Count) { + Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count); + } else { + assert ctype != null; // follows from postcondition of ResolveMember + // build the type substitution map + Dictionary subst = new Dictionary(); + for (int i = 0; i < ctype.TypeArgs.Count; i++) { + subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]); + } + foreach (TypeParameter p in method.TypeArgs) { + subst.Add(p, new ParamTypeProxy(p)); + } + // type check the arguments + for (int i = 0; i < method.Ins.Count; i++) { + UnifyTypes((!)s.Args[i].Type, SubstType(method.Ins[i].Type, subst)); + } + for (int i = 0; i < method.Outs.Count; i++) { + UnifyTypes((!)s.Lhs[i].Type, SubstType(method.Outs[i].Type, subst)); + } + } + } + + } else if (stmt is BlockStmt) { + scope.PushMarker(); + int labelsToPop = 0; + foreach (Statement ss in ((BlockStmt)stmt).Body) { + if (ss is LabelStmt) { + LabelStmt ls = (LabelStmt)ss; + labeledStatements.PushMarker(); + bool b = labeledStatements.Push(ls.Label, ls); + assert b; // since we just pushed a marker, we expect the Push to succeed + labelsToPop++; + } else { + ResolveStatement(ss); + for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); } + } + } + for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); } + scope.PopMarker(); + + } else if (stmt is IfStmt) { + IfStmt s = (IfStmt)stmt; + if (s.Guard != null) { + ResolveExpression(s.Guard, true); + assert s.Guard.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Guard.Type, Type.Bool)) { + Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); + } + } + ResolveStatement(s.Thn); + if (s.Els != null) { + ResolveStatement(s.Els); + } + + } else if (stmt is WhileStmt) { + WhileStmt s = (WhileStmt)stmt; + if (s.Guard != null) { + ResolveExpression(s.Guard, true); + assert s.Guard.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Guard.Type, Type.Bool)) { + Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); + } + } + foreach (MaybeFreeExpression inv in s.Invariants) { + ResolveExpression(inv.E, true); + assert inv.E.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(inv.E.Type, Type.Bool)) { + Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type); + } + } + foreach (Expression e in s.Decreases) { + ResolveExpression(e, true); + // any type is fine + } + ResolveStatement(s.Body); + + } else if (stmt is ForeachStmt) { + ForeachStmt s = (ForeachStmt)stmt; + scope.PushMarker(); + bool b = scope.Push(s.BoundVar.Name, s.BoundVar); + assert b; // since we just pushed a marker, we expect the Push to succeed + ResolveType(s.BoundVar.Type); + + ResolveExpression(s.Collection, true); + assert s.Collection.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) { + Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type); + } + + ResolveExpression(s.Range, true); + assert s.Range.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Range.Type, Type.Bool)) { + Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type); + } + + foreach (PredicateStmt ss in s.BodyPrefix) { + ResolveStatement(ss); + } + if (s.BodyAssign != null) { + ResolveStatement(s.BodyAssign); + // check for correct usage of BoundVar in LHS and RHS of this assignment + FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr; + IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr; + if (obj != null && obj.Var == s.BoundVar) { + // exemplary! + } else { + Error(s, "assignment inside foreach must assign to a field of the bound variable of the foreach statement"); + } + } + scope.PopMarker(); + + } else { + assert false; + } + } + + MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out ClassType ctype) + ensures result != null ==> ctype != null && ctype.ResolvedClass != null; + { + ctype = ClassType.DenotesClass(receiverType); + if (ctype == null) { + Error(tok, "receiver (of type {0}) must be of a class type", receiverType); + } else { + assert ctype.ResolvedClass != null; // follows from postcondition of DenotesClass + assert ctype.TypeArgs.Count == ctype.ResolvedClass.TypeArgs.Count; // follows from the fact that ctype was resolved + MemberDecl member; + if (!classMembers[ctype.ResolvedClass].TryGetValue(memberName, out member)) { + Error(tok, "member {0} does not exist in class {1}", memberName, ctype.Name); + } else { + return (!)member; + } + } + ctype = null; + return null; + } + + Type! SubstType(Type! type, Dictionary! subst) { + if (type is BasicType) { + return type; + } else if (type is CollectionType) { + CollectionType t = (CollectionType)type; + Type arg = SubstType(t.Arg, subst); + if (arg == t.Arg) { + return type; + } else if (type is SetType) { + return new SetType(arg); + } else if (type is SeqType) { + return new SeqType(arg); + } else { + assert false; // unexpected collection type + } + } else if (type is ClassType) { + ClassType t = (ClassType)type; + if (t.ResolvedParam != null) { + assert t.TypeArgs.Count == 0; + Type s; + if (subst.TryGetValue(t.ResolvedParam, out s)) { + return (!)s; + } else { + return type; + } + } else if (t.ResolvedClass != null) { + List newArgs = null; // allocate it lazily + for (int i = 0; i < t.TypeArgs.Count; i++) { + Type p = t.TypeArgs[i]; + Type s = SubstType(p, subst); + if (s != p && newArgs == null) { + // lazily construct newArgs + newArgs = new List(); + for (int j = 0; j < i; j++) { + newArgs.Add(t.TypeArgs[j]); + } + } + if (newArgs != null) { + newArgs.Add(s); + } + } + if (newArgs == null) { + // there were no substitutions + return type; + } else { + return new ClassType(t.tok, t.Name, t.ResolvedClass, newArgs); + } + } else { + // there's neither a resolved param nor a resolved class, which means the ClassType wasn't + // properly resolved; just return it + return type; + } + } else if (type is TypeProxy) { + TypeProxy t = (TypeProxy)type; + if (t.T == null) { + return type; + } else { + // bypass the proxy + return SubstType(t.T, subst); + } + } else { + assert false; // unexpected type + } + } + + public static ClassType! GetThisType(Token! tok, ClassDecl! cl) { + List args = new List(); + foreach (TypeParameter tp in cl.TypeArgs) { + args.Add(new ClassType(tok, tp.Name, tp)); + } + return new ClassType(tok, cl.Name, cl, args); + } + + /// + /// "twoState" implies that "old" and "fresh" expressions are allowed + /// + void ResolveExpression(Expression! expr, bool twoState) + requires currentClass != null; + ensures expr.Type != null; + { + if (expr.Type != null) { + // expression has already been resovled + return; + } + + // The following cases will resolve the subexpressions and will attempt to assign a type of expr. However, if errors occur + // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null. In that case, the end + // of this method will assign proxy type to the expression, which reduces the number of error messages that are produced + // while type checking the rest of the program. + + if (expr is LiteralExpr) { + LiteralExpr e = (LiteralExpr)expr; + if (e.Value == null) { + e.Type = new ObjectTypeProxy(); + } else if (e.Value is int) { + e.Type = Type.Int; + } else if (e.Value is bool) { + e.Type = Type.Bool; + } else { + assert false; // unexpected literal type + } + + } else if (expr is ThisExpr) { + expr.Type = GetThisType(expr.tok, currentClass); + + } else if (expr is IdentifierExpr) { + IdentifierExpr e = (IdentifierExpr)expr; + e.Var = scope.Find(e.Name); + if (e.Var == null) { + Error(expr, "Identifier does not denote a local variable, parameter, or bound variable: {0}", e.Name); + } else { + expr.Type = e.Var.Type; + } + + } else if (expr is DisplayExpression) { + DisplayExpression e = (DisplayExpression)expr; + Type elementType = new InferredTypeProxy(); + foreach (Expression ee in e.Elements) { + ResolveExpression(ee, twoState); + assert ee.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(elementType, ee.Type)) { + Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType); + } + } + if (expr is SetDisplayExpr) { + expr.Type = new SetType(elementType); + } else { + expr.Type = new SeqType(elementType); + } + + } else if (expr is FieldSelectExpr) { + FieldSelectExpr e = (FieldSelectExpr)expr; + ResolveExpression(e.Obj, twoState); + assert e.Obj.Type != null; // follows from postcondition of ResolveExpression + ClassType ctype; + MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.FieldName, out ctype); + if (member == null) { + // error has already been reported by ResolveMember + } else if (!(member is Field)) { + Error(expr, "member {0} in class {1} does not refer to a field", e.FieldName, ((!)ctype).Name); + } else { + assert ctype != null && ctype.ResolvedClass != null; // follows from postcondition of ResolveMember + e.Field = (Field)member; + // build the type substitution map + Dictionary subst = new Dictionary(); + for (int i = 0; i < ctype.TypeArgs.Count; i++) { + subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]); + } + e.Type = SubstType(e.Field.Type, subst); + } + + } else if (expr is SeqSelectExpr) { + SeqSelectExpr e = (SeqSelectExpr)expr; + bool seqErr = false; + ResolveExpression(e.Seq, twoState); + assert e.Seq.Type != null; // follows from postcondition of ResolveExpression + Type elementType = new InferredTypeProxy(); + if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) { + Error(expr, "sequence selection requires a sequence (got {0})", e.Seq.Type); + seqErr = true; + } + if (e.E0 != null) { + ResolveExpression(e.E0, twoState); + assert e.E0.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.E0.Type, Type.Int)) { + Error(e.E0, "sequence selections requires integer indices (got {0})", e.E0.Type); + } + } + if (e.E1 != null) { + ResolveExpression(e.E1, twoState); + assert e.E1.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.E1.Type, Type.Int)) { + Error(e.E1, "sequence selections requires integer indices (got {0})", e.E1.Type); + } + } + if (!seqErr) { + if (e.SelectOne) { + expr.Type = elementType; + } else { + expr.Type = e.Seq.Type; + } + } + + } else if (expr is FunctionCallExpr) { + FunctionCallExpr e = (FunctionCallExpr)expr; + ResolveExpression(e.Receiver, twoState); + assert e.Receiver.Type != null; // follows from postcondition of ResolveExpression + ClassType ctype; + MemberDecl member = ResolveMember(expr.tok, e.Receiver.Type, e.Name, out ctype); + if (member == null) { + // error has already been reported by ResolveMember + } else if (!(member is Function)) { + Error(expr, "member {0} in class {1} does not refer to a function", e.Name, ((!)ctype).Name); + } else { + Function function = (Function)member; + e.Function = function; + if (function.Formals.Count != e.Args.Count) { + Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count); + } else { + assert ctype != null; // follows from postcondition of ResolveMember + // build the type substitution map + Dictionary subst = new Dictionary(); + for (int i = 0; i < ctype.TypeArgs.Count; i++) { + subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]); + } + foreach (TypeParameter p in function.TypeArgs) { + subst.Add(p, new ParamTypeProxy(p)); + } + // type check the arguments + for (int i = 0; i < function.Formals.Count; i++) { + Expression farg = e.Args[i]; + ResolveExpression(farg, twoState); + assert farg.Type != null; // follows from postcondition of ResolveExpression + UnifyTypes(farg.Type, SubstType(function.Formals[i].Type, subst)); + } + expr.Type = SubstType(function.ResultType, subst); + } + } + + } else if (expr is OldExpr) { + OldExpr e = (OldExpr)expr; + if (!twoState) { + Error(expr, "old expressions are not allowed in this context"); + } + ResolveExpression(e.E, twoState); + expr.Type = e.E.Type; + + } else if (expr is FreshExpr) { + FreshExpr e = (FreshExpr)expr; + if (!twoState) { + Error(expr, "fresh expressions are not allowed in this context"); + } + ResolveExpression(e.E, twoState); + // the type of e.E must be either an object or a collection of objects + Type t = e.E.Type; + assert t != null; // follows from postcondition of ResolveExpression + if (t is CollectionType) { + t = ((CollectionType)t).Arg; + } + if (t is ObjectType) { + // fine + } else if (ClassType.DenotesClass(t) != null) { + // fine + } else { + Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type); + } + expr.Type = Type.Bool; + + } else if (expr is UnaryExpr) { + UnaryExpr e = (UnaryExpr)expr; + ResolveExpression(e.E, twoState); + assert e.E.Type != null; // follows from postcondition of ResolveExpression + switch (e.Op) { + case UnaryExpr.Opcode.Not: + if (!UnifyTypes(e.E.Type, Type.Bool)) { + Error(expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type); + } + expr.Type = Type.Bool; + break; + case UnaryExpr.Opcode.SeqLength: + if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) { + Error(expr, "sequence-length operator expects a sequence argument (instead got {0})", e.E.Type); + } + expr.Type = Type.Int; + break; + default: + assert false; // unexpected unary operator + } + + } else if (expr is BinaryExpr) { + BinaryExpr e = (BinaryExpr)expr; + ResolveExpression(e.E0, twoState); + assert e.E0.Type != null; // follows from postcondition of ResolveExpression + ResolveExpression(e.E1, twoState); + assert e.E1.Type != null; // follows from postcondition of ResolveExpression + switch (e.Op) { + case BinaryExpr.Opcode.Iff: + case BinaryExpr.Opcode.Imp: + case BinaryExpr.Opcode.And: + case BinaryExpr.Opcode.Or: + if (!UnifyTypes(e.E0.Type, Type.Bool)) { + Error(expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type); + } + if (!UnifyTypes(e.E1.Type, Type.Bool)) { + Error(expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type); + } + expr.Type = Type.Bool; + break; + + case BinaryExpr.Opcode.Eq: + case BinaryExpr.Opcode.Neq: + if (!UnifyTypes(e.E0.Type, e.E1.Type)) { + Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type); + } + expr.Type = Type.Bool; + break; + + case BinaryExpr.Opcode.Disjoint: + if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy()))) { + Error(expr, "arguments must be of a set type (got {0})", e.E0.Type); + } + if (!UnifyTypes(e.E0.Type, e.E1.Type)) { + Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type); + } + expr.Type = Type.Bool; + break; + + case BinaryExpr.Opcode.Lt: + case BinaryExpr.Opcode.Le: + case BinaryExpr.Opcode.Add: + { + bool err = false; + if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) { + Error(expr, "arguments to {0} must be int or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type); + err = true; + } + if (!UnifyTypes(e.E1.Type, e.E0.Type)) { + Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type); + err = true; + } + if (e.Op != BinaryExpr.Opcode.Add) { + expr.Type = Type.Bool; + } else if (!err) { + expr.Type = e.E0.Type; + } + } + break; + + case BinaryExpr.Opcode.Sub: + case BinaryExpr.Opcode.Mul: + case BinaryExpr.Opcode.Gt: + case BinaryExpr.Opcode.Ge: + { + bool err = false; + if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) { + Error(expr, "arguments to {0} must be int or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type); + err = true; + } + if (!UnifyTypes(e.E1.Type, e.E0.Type)) { + Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type); + err = true; + } + if (e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge) { + expr.Type = Type.Bool; + } else if (!err) { + expr.Type = e.E0.Type; + } + } + break; + + case BinaryExpr.Opcode.In: + if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type))) { + Error(expr, "second argument to {0} must be a set or sequence of type {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type); + } + expr.Type = Type.Bool; + break; + + case BinaryExpr.Opcode.Div: + case BinaryExpr.Opcode.Mod: + if (!UnifyTypes(e.E0.Type, Type.Int)) { + Error(expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type); + } + if (!UnifyTypes(e.E1.Type, Type.Int)) { + Error(expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type); + } + expr.Type = Type.Int; + break; + + default: + assert false; // unexpected operator + } + e.ResolvedOp = ResolveOp(e.Op, e.E1.Type); + + } else if (expr is QuantifierExpr) { + QuantifierExpr e = (QuantifierExpr)expr; + scope.PushMarker(); + foreach (BoundVar v in e.BoundVars) { + if (!scope.Push(v.Name, v)) { + Error(v, "Duplicate parameter name: {0}", v.Name); + } + ResolveType(v.Type); + } + ResolveExpression(e.Body, twoState); + assert e.Body.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.Body.Type, Type.Bool)) { + Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type); + } + // Since the body is more likely to infer the types of the bound variables, resolve it + // first (above) and only then resolve the attributes and triggers (below). + ResolveAttributes(e.Attributes, twoState); + ResolveTriggers(e.Trigs, twoState); + scope.PopMarker(); + expr.Type = Type.Bool; + + } else if (expr is ITEExpr) { + ITEExpr e = (ITEExpr)expr; + assert !twoState; + ResolveExpression(e.Test, twoState); + assert e.Test.Type != null; // follows from postcondition of ResolveExpression + ResolveExpression(e.Thn, twoState); + assert e.Thn.Type != null; // follows from postcondition of ResolveExpression + ResolveExpression(e.Els, twoState); + assert e.Els.Type != null; // follows from postcondition of ResolveExpression + if (!UnifyTypes(e.Test.Type, Type.Bool)) { + Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type); + } + if (!UnifyTypes(e.Thn.Type, Type.Bool)) { + Error(expr, "the then branch of an if-then-else expression must be a boolean (instead got {0})", e.Thn.Type); + } + if (!UnifyTypes(e.Els.Type, Type.Bool)) { + Error(expr, "the else branch of an if-then-else expression must be a boolean (instead got {0})", e.Els.Type); + } + expr.Type = Type.Bool; + + } else { + assert false; // unexpected expression + } + + if (expr.Type == null) { + // some resolution error occurred + expr.Type = Type.Flexible; + } + } + + /// + /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if + /// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned. + /// + BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type! operandType) { + switch (op) { + case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff; + case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp; + case BinaryExpr.Opcode.And: return BinaryExpr.ResolvedOpcode.And; + case BinaryExpr.Opcode.Or: return BinaryExpr.ResolvedOpcode.Or; + case BinaryExpr.Opcode.Eq: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.SetEq; + } else if (operandType is SeqType) { + return BinaryExpr.ResolvedOpcode.SeqEq; + } else { + return BinaryExpr.ResolvedOpcode.EqCommon; + } + case BinaryExpr.Opcode.Neq: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.SetNeq; + } else if (operandType is SeqType) { + return BinaryExpr.ResolvedOpcode.SeqNeq; + } else { + return BinaryExpr.ResolvedOpcode.NeqCommon; + } + case BinaryExpr.Opcode.Disjoint: return BinaryExpr.ResolvedOpcode.Disjoint; + case BinaryExpr.Opcode.Lt: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.ProperSubset; + } else if (operandType is SeqType) { + return BinaryExpr.ResolvedOpcode.ProperPrefix; + } else { + return BinaryExpr.ResolvedOpcode.Lt; + } + case BinaryExpr.Opcode.Le: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.Subset; + } else if (operandType is SeqType) { + return BinaryExpr.ResolvedOpcode.Prefix; + } else { + return BinaryExpr.ResolvedOpcode.Le; + } + case BinaryExpr.Opcode.Add: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.Union; + } else if (operandType is SeqType) { + return BinaryExpr.ResolvedOpcode.Concat; + } else { + return BinaryExpr.ResolvedOpcode.Add; + } + case BinaryExpr.Opcode.Sub: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.SetDifference; + } else { + return BinaryExpr.ResolvedOpcode.Sub; + } + case BinaryExpr.Opcode.Mul: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.Intersection; + } else { + return BinaryExpr.ResolvedOpcode.Mul; + } + case BinaryExpr.Opcode.Gt: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.ProperSuperset; + } else { + return BinaryExpr.ResolvedOpcode.Gt; + } + case BinaryExpr.Opcode.Ge: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.Superset; + } else { + return BinaryExpr.ResolvedOpcode.Ge; + } + case BinaryExpr.Opcode.In: + if (operandType is SetType) { + return BinaryExpr.ResolvedOpcode.InSet; + } else { + return BinaryExpr.ResolvedOpcode.InSeq; + } + case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div; + case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod; + default: + assert false; // unexpected operator + } + } + } + + class Scope where Thing : class { + [Rep] readonly List! names = new List(); // a null means a marker + [Rep] readonly List! things = new List(); + invariant names.Count == things.Count; + + public void PushMarker() { + names.Add(null); + things.Add(null); + } + + public void PopMarker() { + int n = names.Count; + while (true) { + n--; + if (names[n] == null) { + break; + } + } + names.RemoveRange(n, names.Count - n); + things.RemoveRange(n, things.Count - n); + } + + // Pushes name-->var association and returns "true", if name has not already been pushed since the last marker. + // If name already has been pushed since the last marker, does nothing and returns "false". + public bool Push(string! name, Thing! thing) { + if (Find(name, true) != null) { + return false; + } else { + names.Add(name); + things.Add(thing); + return true; + } + } + + Thing? Find(string! name, bool topScopeOnly) { + for (int n = names.Count; 0 <= --n; ) { + if (names[n] == null) { + if (topScopeOnly) { + return null; // no present + } + } else if (names[n] == name) { + Thing t = things[n]; + assert t != null; + return t; + } + } + return null; // not present + } + + public Thing? Find(string! name) { + return Find(name, false); + } + } +} -- cgit v1.2.3