}

	@Override
	public boolean isType(Class<? extends Type> typeclass)
	{
		return true;
	}

	@Override
	public boolean isUnknown()
	{
		return true;
	}

	@Override
	public boolean isSeq()
	{
		return true;
	}

	@Override
	public boolean isSet()
	{
		return true;
	}

	@Override
	public boolean isMap()
	{
		return true;
	}

	@Override
	public boolean isRecord()
	{
		return true;
	}

	@Override
	public boolean isClass()
	{
		return true;		// Too much trouble?
	}

	@Override
	public boolean isNumeric()
	{
		return true;
	}

	@Override
	public boolean isProduct()
	{
		return true;
	}

	@Override
	public boolean isProduct(int n)
	{
		return true;
	}

	@Override
	public boolean isFunction()
	{
		return true;
	}

	@Override
	public boolean isOperation()
	{
		return true;
	}

	@Override
	public SeqType getSeq()
	{
		return new SeqType(location);	// empty
	}

	@Override
	public SetType getSet()
	{
		return new SetType(location);	// empty
	}

	@Override
	public MapType getMap()
	{
		return new MapType(location);	// Unknown |-> Unknown
	}

	@Override
	public RecordType getRecord()
	{
		return new RecordType(location, new Vector<Field>());
	}

	@Override
	public ClassType getClassType()
	{
		return new ClassType(location, new ClassDefinition());
	}

	@Override
	public NumericType getNumeric()
	{
		return new RealType(location);
	}

	@Override
	public ProductType getProduct()
	{
		return new ProductType(location, new TypeList());
	}

	@Override
	public ProductType getProduct(int n)
	{
		TypeList tl = new TypeList();

		for (int i=0; i<n; i++)
		{
			tl.add(new UnknownType(location));
		}

		return new ProductType(location, tl);
	}

	@Override
	public FunctionType getFunction()

		return body == null ? null : body.findExpression(lineno);
	}

	@Override
	public Definition findName(LexNameToken sought, NameScope scope)
	{
		if (super.findName(sought, scope) != null)
		{
			return this;
		}

		if (predef != null && predef.findName(sought, scope) != null)
		{
			return predef;
		}

		if (postdef != null && postdef.findName(sought, scope) != null)
		{
			return postdef;
		}

		return null;
	}

	@Override
	public NameValuePairList getNamedValues(Context ctxt)
	{
		NameValuePairList nvl = new NameValuePairList();
		Context free = ctxt.getFreeVariables();

		FunctionValue prefunc =
			(predef == null) ? null : new FunctionValue(predef, null, null, free);

		FunctionValue postfunc =
			(postdef == null) ? null : new FunctionValue(postdef, null, null, free);

		// Note, body may be null if it is really implicit. This is caught
		// when the function is invoked. The value is needed to implement
		// the pre_() expression for implicit functions.

		nvl.add(new NameValuePair(name,
				new FunctionValue(this, prefunc, postfunc, free)));

		if (predef != null)
		{
			nvl.add(new NameValuePair(predef.name, prefunc));
		}

		if (postdef != null)
		{
			nvl.add(new NameValuePair(postdef.name, postfunc));
		}

		if (Settings.dialect == Dialect.VDM_SL)
		{
			// This is needed for recursive local functions
			free.put(nvl);
		}

		return nvl;
	}

		return body == null ? null : body.findStatement(lineno);
	}

	@Override
	public NameValuePairList getNamedValues(Context ctxt)
	{
		NameValuePairList nvl = new NameValuePairList();

		FunctionValue prefunc =
			(predef == null) ? null : new FunctionValue(predef, null, null, null);

		FunctionValue postfunc =
			(postdef == null) ? null : new FunctionValue(postdef, null, null, null);

		// Note, body may be null if it is really implicit. This is caught
		// when the function is invoked. The value is needed to implement
		// the pre_() expression for implicit functions.

		OperationValue op =	new OperationValue(this, prefunc, postfunc, state);
		op.isConstructor = isConstructor;
		op.isStatic = accessSpecifier.isStatic;
		nvl.add(new NameValuePair(name, op));

		if (predef != null)
		{
			prefunc.isStatic = accessSpecifier.isStatic;
			nvl.add(new NameValuePair(predef.name, prefunc));
		}

		if (postdef != null)
		{
			postfunc.isStatic = accessSpecifier.isStatic;
			nvl.add(new NameValuePair(postdef.name, postfunc));
		}

		return nvl;
	}

	@Override
	public DefinitionList getDefinitions()
	{
		DefinitionList defs = new DefinitionList(this);

		if (predef != null)
		{
			defs.add(predef);
		}

		if (postdef != null)
		{
			defs.add(postdef);
		}

		return defs;
	}

	@Override
	public LexNameList getVariableNames()
	{
		return new LexNameList(name);
	}

			plist.add(result.pattern);
		}

		if (state != null)
		{
			plist.add(new IdentifierPattern(state.name.getOldName()));
			plist.add(new IdentifierPattern(state.name));
		}
		else if (base.isVDMPP() && !accessSpecifier.isStatic)
		{
			plist.add(new IdentifierPattern(name.getSelfName().getOldName()));
			plist.add(new IdentifierPattern(name.getSelfName()));
		}

		parameters.add(plist);
		PostOpExpression postop = new PostOpExpression(name, postcondition, state);

		ExplicitFunctionDefinition def = new ExplicitFunctionDefinition(
			name.getPostName(postcondition.location), NameScope.GLOBAL,
			null, type.getPostType(state, classDefinition, accessSpecifier.isStatic),
			parameters, postop, null, null, false, false, null);

		// Operation postcondition functions are effectively not static as
		// their expression can directly refer to instance variables, even
		// though at runtime these are passed via a "self" parameter.

		def.setAccessSpecifier(accessSpecifier.getStatic(false));
		def.classDefinition = classDefinition;
		return def;
	}

	@Override
	public ProofObligationList getProofObligations(POContextStack ctxt)
	{
		ProofObligationList obligations = new ProofObligationList();
		boolean patterns = false;

		for (Pattern p: getParamPatternList())

		if (state != null)
		{
			plist.add(new IdentifierPattern(state.name));
		}
		else if (base.isVDMPP() && !accessSpecifier.isStatic)
		{
			plist.add(new IdentifierPattern(name.getSelfName()));
		}

		parameters.add(plist);
		PreOpExpression preop = new PreOpExpression(name, precondition, state);

		ExplicitFunctionDefinition def = new ExplicitFunctionDefinition(
			name.getPreName(precondition.location), NameScope.GLOBAL,
			null, type.getPreType(state, classDefinition, accessSpecifier.isStatic),
			parameters, preop, null, null, false, false, null);

		// Operation precondition functions are effectively not static as
		// their expression can directly refer to instance variables, even
		// though at runtime these are passed via a "self" parameter.

		def.setAccessSpecifier(accessSpecifier.getStatic(false));
		def.classDefinition = classDefinition;
		return def;
	}

	private ExplicitFunctionDefinition getPostDefinition(Environment base)
	{
		List<PatternList> parameters = new Vector<PatternList>();
		PatternList plist = new PatternList();

		AlternativeTraceNode node = new AlternativeTraceNode();

		QuantifierList quantifiers = new QuantifierList();

		for (MultipleBind mb: def.bindings)
		{
			ValueList bvals = mb.getBindValues(ctxt);

			for (Pattern p: mb.plist)
			{
				Quantifier q = new Quantifier(p, bvals);
				quantifiers.add(q);
			}
		}

		quantifiers.init();

		try
		{
			while (quantifiers.hasNext(ctxt))
			{
				Context evalContext = new Context(location, "let be st statement", ctxt);
				NameValuePairList nvpl = quantifiers.next();
				boolean matches = true;

				for (NameValuePair nvp: nvpl)
				{
					Value v = evalContext.get(nvp.name);

					if (v == null)
					{
						evalContext.put(nvp.name, nvp.value);
					}
					else
					{
						if (!v.equals(nvp.value))
						{
							matches = false;
							break;	// This quantifier set does not match
						}
					}
				}

				if (matches &&
					(stexp == null || stexp.eval(evalContext).boolValue(ctxt)))

   			try
   			{
   				if (file.getName().endsWith(".lib"))
   				{
   					FileInputStream fis = new FileInputStream(file);
   	    	        GZIPInputStream gis = new GZIPInputStream(fis);
   	    	        ObjectInputStream ois = new ObjectInputStream(gis);

   	    	        ClassList loaded = null;
   	    	        long begin = System.currentTimeMillis();

   	    	        try
   	    	        {
   	    	        	loaded = (ClassList)ois.readObject();
   	    	        }
       	 			catch (Exception e)
       				{
       	   				println(file + " is not a valid VDM++ library");
       	   				perrs++;
       	   				continue;
       				}
       	 			finally
       	 			{
       	 				ois.close();
       	 			}

   	    	        long end = System.currentTimeMillis();
   	    	        loaded.setLoaded();
   	    	        classes.addAll(loaded);
   	    	        classes.remap();

   	    	   		infoln("Loaded " + plural(loaded.size(), "class", "es") +
   	    	   			" from " + file + " in " + (double)(end-begin)/1000 + " secs");
   				}
   				else
   				{
   					long before = System.currentTimeMillis();

		return type.isOperation();
	}

	@Override
	public SeqType getSeq()
	{
		return type.getSeq();
	}

	@Override
	public SetType getSet()
	{
		return type.getSet();
	}

	@Override
	public MapType getMap()
	{
		return type.getMap();
	}

	@Override
	public RecordType getRecord()
	{
		return type.getRecord();
	}

	@Override
	public ClassType getClassType()
	{
		return type.getClassType();
	}

	@Override
	public NumericType getNumeric()
	{
		return type.getNumeric();
	}

	@Override
	public ProductType getProduct()
	{
		return type.getProduct();
	}

	@Override
	public ProductType getProduct(int n)
	{
		return type.getProduct(n);
	}

	@Override
	public FunctionType getFunction()
	{
		return type.getFunction();
	}

	@Override
	public OperationType getOperation()
	{
		return type.getOperation();
	}

	@Override
	public String toDisplay()

		return type.isClass();
	}

	@Override
	public boolean isNumeric()
	{
		return type.isNumeric();
	}

	@Override
	public boolean isProduct()
	{
		return type.isProduct();
	}

	@Override
	public boolean isProduct(int n)
	{
		return type.isProduct(n);
	}

	@Override
	public boolean isFunction()
	{
		return type.isFunction();
	}

	@Override
	public boolean isOperation()
	{
		return type.isOperation();
	}

	@Override
	public UnionType getUnion()
	{
		return type.getUnion();
	}

	@Override
	public SeqType getSeq()
	{
		return type.getSeq();
	}

	@Override
	public SetType getSet()
	{
		return type.getSet();
	}

	@Override
	public MapType getMap()
	{
		return type.getMap();
	}

	@Override
	public RecordType getRecord()
	{
		return type.getRecord();
	}

	@Override
	public ClassType getClassType()

	}

	@Override
	public boolean isSeq()
	{
		return type.isSeq();
	}

	@Override
	public boolean isSet()
	{
		return type.isSet();
	}

	@Override
	public boolean isMap()
	{
		return type.isMap();
	}

	@Override
	public boolean isRecord()
	{
		return type.isRecord();
	}

	@Override
	public boolean isClass()
	{
		return type.isClass();
	}

	@Override
	public boolean isNumeric()
	{
		return type.isNumeric();
	}

	@Override
	public boolean isProduct()
	{
		return type.isProduct();
	}

	@Override
	public boolean isProduct(int n)
	{
		return type.isProduct(n);
	}

	@Override
	public boolean isFunction()
	{
		return type.isFunction();
	}

	@Override
	public boolean isOperation()
	{
		return type.isOperation();
	}

	@Override
	public SeqType getSeq()

			predicate.report(3097, "Predicate is not boolean");
		}

		local.unusedCheck();
		return new BooleanType(location);
	}

	@Override
	public Expression findExpression(int lineno)
	{
		Expression found = super.findExpression(lineno);
		if (found != null) return found;

		return predicate.findExpression(lineno);
	}

	@Override
	public Value eval(Context ctxt)
	{
		breakpoint.check(location, ctxt);

		QuantifierList quantifiers = new QuantifierList();

		for (MultipleBind mb: bindList)
		{
			ValueList bvals = mb.getBindValues(ctxt);

			for (Pattern p: mb.plist)
			{
				Quantifier q = new Quantifier(p, bvals);
				quantifiers.add(q);
			}
		}

		quantifiers.init();

		try
		{
			while (quantifiers.hasNext(ctxt))
			{
				Context evalContext = new Context(location, "forall", ctxt);

	private void setTracepoint(String name, String trace)
		throws Exception
	{
		LexTokenReader ltr = new LexTokenReader(name, Dialect.VDM_SL);
		LexToken token = ltr.nextToken();
		ltr.close();

		Value v = null;

		if (token.is(Token.IDENTIFIER))
		{
			LexIdentifierToken id = (LexIdentifierToken)token;
			LexNameToken lnt = new LexNameToken(interpreter.getDefaultName(), id);
			v = interpreter.findGlobal(lnt);
		}
		else if (token.is(Token.NAME))
		{
			v = interpreter.findGlobal((LexNameToken)token);
		}

		if (v instanceof FunctionValue)
		{
			FunctionValue fv = (FunctionValue)v;
			Expression exp = fv.body;
			interpreter.clearBreakpoint(exp.breakpoint.number);
			Breakpoint bp = interpreter.setTracepoint(exp, trace);

	public void abort(int number, String msg, Context ctxt)
	{
		throw new ContextException(number, msg, location, ctxt);
	}

	public Value abort(ValueException ve)
	{
		throw new ContextException(ve, location);
	}

	public void report(int number, String msg)
	{
		TypeChecker.report(number, msg, location);
	}

	public void concern(boolean serious, int number, String msg)
	{
		if (serious)
		{
			TypeChecker.report(number, msg, location);
		}
		else
		{
			TypeChecker.warning(number, msg, location);
		}
	}

	public void detail(String tag, Object obj)
	{
		TypeChecker.detail(tag, obj);
	}

	public void detail2(String tag1, Object obj1, String tag2, Object obj2)

			else if (mdef == null)
			{
				measure.report(3270, "Measure " + mname + " is not in scope");
			}
			else if (!(mdef instanceof ExplicitFunctionDefinition))
			{
				measure.report(3271, "Measure " + mname + " is not an explicit function");
			}
			else
			{
				FunctionType mtype = (FunctionType)mdef.getType();

				if (!(mtype.result instanceof NaturalType))
				{
					if (mtype.result.isProduct())
					{
						ProductType pt = mtype.result.getProduct();

						for (Type t: pt.types)
						{
							if (!(t instanceof NaturalType))
							{
								measure.report(3272,
									"Measure range is not a nat, or a nat tuple");
								measure.detail("Actual", mtype.result);

		sr.setCurrentModule(getDefaultName());
		return sr.readStatement();
	}

	@Override
	public Type typeCheck(Expression expr, Environment env)
		throws Exception
	{
		TypeChecker.clearErrors();
		Type type = expr.typeCheck(env, null, NameScope.NAMESANDSTATE);

		if (TypeChecker.getErrorCount() > 0)
		{
			// TypeChecker.printErrors(Console.out);
			throw new VDMErrorsException(TypeChecker.getErrors());
		}

		return type;
	}

	@Override
	public Type typeCheck(Statement stmt, Environment env)
		throws Exception
	{
		TypeChecker.clearErrors();
		Type type = stmt.typeCheck(env, NameScope.NAMESANDSTATE);

		if (TypeChecker.getErrorCount() > 0)
		{
			// TypeChecker.printErrors(Console.out);
			throw new VDMErrorsException(TypeChecker.getErrors());
		}

		return type;
	}

	}

	public void detail(String tag, Object obj)
	{
		TypeChecker.detail(tag, obj);
	}

	public void detail(boolean serious, String tag, Object obj)
	{
		if (serious)
		{
			TypeChecker.detail(tag, obj);
		}
	}

	public void detail2(String tag1, Object obj1, String tag2, Object obj2)
	{
		TypeChecker.detail2(tag1, obj1, tag2, obj2);
	}

	public void detail2(
		boolean serious, String tag1, Object obj1, String tag2, Object obj2)
	{
		if (serious)
		{
			TypeChecker.detail2(tag1, obj1, tag2, obj2);
		}
	}
}

			return new BooleanValue(lv.type.equals(rv.type));
		}
		catch (ValueException e)
		{
			return abort(e);
		}
	}

	@Override
	public Expression findExpression(int lineno)
	{
		Expression found = super.findExpression(lineno);
		if (found != null) return found;

		found = left.findExpression(lineno);
		if (found != null) return found;

		found = right.findExpression(lineno);
		if (found != null) return found;

		return null;
	}

	@Override
	public ProofObligationList getProofObligations(POContextStack ctxt)
	{
		ProofObligationList list = left.getProofObligations(ctxt);
		list.addAll(right.getProofObligations(ctxt));
		return list;
	}

	@Override
	public String kind()
	{
		return "sameclass";

	public void report(int number, String msg)
	{
		TypeChecker.report(number, msg, location);
	}

	public void abort(int number, String msg, Context ctxt)
	{
		throw new ContextException(number, msg, location, ctxt);
	}

	public void abort(ValueException ve)
	{
		throw new ContextException(ve, location);
	}

	public void detail(String tag, Object obj)
	{
		TypeChecker.detail(tag, obj);
	}

	public void detail2(String tag1, Object obj1, String tag2, Object obj2)
	{
		TypeChecker.detail2(tag1, obj1, tag2, obj2);
	}
}

    					Type pt = op.parameters.get(p);
    					TypeSet pset = params.get(p);

    					if (pset == null)
    					{
    						pset = new TypeSet(pt);
    						params.put(p, pset);
    					}
    					else
    					{
    						pset.add(pt);
    					}
    				}
    			}
    		}

    		if (!result.isEmpty())
    		{
    			Type rtype = result.getType(location);
       			TypeList plist = new TypeList();

    			for (int i=0; i<params.size(); i++)
    			{
    				Type pt = params.get(i).getType(location);
    				plist.add(pt);
    			}

	}

	private ExplicitFunctionDefinition getInvDefinition()
	{
		LexLocation loc = invPattern.location;
		PatternList params = new PatternList();
		params.add(invPattern);

		List<PatternList> parameters = new Vector<PatternList>();
		parameters.add(params);

		TypeList ptypes = new TypeList();
		ptypes.add(new UnresolvedType(name));
		FunctionType ftype =
			new FunctionType(loc, false, ptypes, new BooleanType(loc));

		ExplicitFunctionDefinition def = new ExplicitFunctionDefinition(
			name.getInvName(loc),
			NameScope.GLOBAL, null, ftype, parameters, invExpression,
			null, null, true, false, null);

    		info("Type checked " + plural(n, "module", "s") +
    			" in " + (double)(after-before)/1000 + " secs. ");
      		info(terrs == 0 ? "No type errors" :
      			"Found " + plural(terrs, "type error", "s"));
      		infoln(twarn == 0 ? "" : " and " +
      			(warnings ? "" : "suppressed ") + plural(twarn, "warning", "s"));
   		}

		if (outfile != null && terrs == 0)
		{
			try
			{
				before = System.currentTimeMillis();
    	        FileOutputStream fos = new FileOutputStream(outfile);
    	        GZIPOutputStream gos = new GZIPOutputStream(fos);
    	        ObjectOutputStream oos = new ObjectOutputStream(gos);

    	        oos.writeObject(modules);

	public UnionPattern(Pattern left, LexLocation location, Pattern right)
	{
		super(location);
		this.left = left;
		this.right = right;
	}

	@Override
	public void unResolve()
	{
		left.unResolve();
		right.unResolve();
		resolved = false;
	}

	@Override
	public void typeResolve(Environment env)
	{
		if (resolved) return; else { resolved = true; }

		try
		{
			left.typeResolve(env);
			right.typeResolve(env);
		}
		catch (TypeCheckException e)
		{
			unResolve();
			throw e;
		}
	}

	@Override
	public String toString()
	{
		return left + " union " + right;

	public SameClassExpression(LexLocation start, ExpressionList args)
	{
		super(start);

		left = args.get(0);
		right = args.get(1);
	}

	@Override
	public Value eval(Context ctxt)
	{
		try
		{
			Value l = left.eval(ctxt);
			Value r = right.eval(ctxt);

			if (!l.isType(ObjectValue.class) ||
				!r.isType(ObjectValue.class))
			{
				return new BooleanValue(false);
			}

			ObjectValue lv = l.objectValue(ctxt);
			ObjectValue rv = r.objectValue(ctxt);

		for (Iterator<String> i = largs.iterator(); i.hasNext();)
		{
			String arg = i.next();

    		if (arg.equals("-vdmsl"))
    		{
    			controller = new VDMSL();
    		}
    		else if (arg.equals("-vdmpp"))
    		{
    			controller = new VDMPP();
    		}
    		else if (arg.equals("-vdmrt"))
    		{
    			controller = new VDMRT();
    		}
    		else if (arg.equals("-overture"))
    		{
    			controller = new VDMOV();
    		}
    		else if (arg.equals("-w"))

		for (IOmlPatternBindExpression pbe: pbelist)
		{
			IOmlPatternBind pb = pbe.getPatternBind();
			Expression e = convertExpression(pbe.getExpression());

			if (pb instanceof IOmlPattern)
			{
				Pattern p = convertPattern((IOmlPattern)pb);
				defs.add(new EqualsDefinition(getLocation(pb), p, e));
			}
			else if (pb instanceof IOmlBind)
			{
				MultipleBind mb = convertMultiBind((IOmlBind)pb);
				defs.add(new EqualsDefinition(getLocation(pb), mb.plist.get(0), e));
			}
			else
			{
				throw new InternalException(37, "Unexpected pattern/bind type");

		return new SetValue(set);
	}

	@Override
	public Expression findExpression(int lineno)
	{
		Expression found = super.findExpression(lineno);
		if (found != null) return found;

		found = first.findExpression(lineno);
		if (found != null) return found;

		return predicate == null ? null : predicate.findExpression(lineno);
	}

	@Override
	public ProofObligationList getProofObligations(POContextStack ctxt)
	{
		ProofObligationList obligations = new ProofObligationList();

		ctxt.push(new POForAllPredicateContext(this));
		obligations.addAll(first.getProofObligations(ctxt));
		ctxt.pop();

   	   		infoln("Initialized " + plural(modules.size(), "module", "s") + " in " +
   	   			(double)(after-before)/1000 + " secs. ");
		}
		catch (ContextException e)
		{
			println("Initialization: " + e);
			e.ctxt.printStackTrace(Console.out, true);
			return ExitStatus.EXIT_ERRORS;
		}
		catch (Exception e)
		{
			println("Initialization: " + e);
			return ExitStatus.EXIT_ERRORS;
		}

		try
		{
			if (script != null)
			{
				println(interpreter.execute(script, null).toString());
				return ExitStatus.EXIT_OK;
			}
			else
			{
				infoln("Interpreter started");
				CommandReader reader = new ModuleCommandReader(interpreter, "> ");

		return statement.findExpression(lineno);
	}

	@Override
	public Value eval(Context ctxt)
	{
		breakpoint.check(location, ctxt);
		QuantifierList quantifiers = new QuantifierList();

		for (MultipleBind mb: def.bindings)
		{
			ValueList bvals = mb.getBindValues(ctxt);

			for (Pattern p: mb.plist)
			{
				Quantifier q = new Quantifier(p, bvals);
				quantifiers.add(q);
			}
		}

		quantifiers.init();

		try
		{
			while (quantifiers.hasNext(ctxt))
			{
				Context evalContext = new Context(location, "let be st statement", ctxt);

				if (name.name.equals(classDefinition.name.name))
    			{
    				isConstructor = true;

    				if (accessSpecifier.isAsync)
    				{
    					report(3286, "Constructor cannot be 'async'");
    				}

    				if (type.result.isClass())
    				{
    					ClassType ctype = type.result.getClassType();

    					if (ctype.classdef != classDefinition)
    					{
    						type.result.report(3025,
    							"Constructor operation must have return type " + classDefinition.name.name);
    					}
    				}
    				else
    				{
    					type.result.report(3026,
    						"Constructor operation must have return type " + classDefinition.name.name);
    				}
    			}
			}

		if (c.data != null || c.options.size() > 4)
		{
			throw new DBGPException(DBGPErrorCode.INVALID_OPTIONS, c.toString());
		}

		if (status != DBGPStatus.BREAK && status != DBGPStatus.STOPPING)
		{
			throw new DBGPException(DBGPErrorCode.NOT_AVAILABLE, c.toString());
		}

		DBGPOption option = c.getOption(DBGPOptionType.C);
		int type = 0;

		if (option != null)
		{
			type = Integer.parseInt(option.value);
		}

		DBGPContextType context = DBGPContextType.lookup(type);

		option = c.getOption(DBGPOptionType.D);
		int depth = -1;

			report(3210, "Name is neither a function nor an operation");
			return new UnknownType(location);
		}
	}

	@Override
	public TypeSet exitCheck()
	{
		// TODO We don't know what an operation call will raise
		return new TypeSet(new UnknownType(location));
	}

	private TypeList getArgTypes(Environment env, NameScope scope)
	{
		TypeList types = new TypeList();

		for (Expression a: args)
		{
			types.add(a.typeCheck(env, null, scope));
		}

		return types;
	}

	private void checkArgTypes(TypeList ptypes, TypeList atypes)
	{
		if (ptypes.size() != atypes.size())
		{
			report(3216, "Expecting " + ptypes.size() + " arguments");

				report(3153, "Restriction of map should be set of " + map.to);
			}
		}

		return ltype;
	}

	@Override
	public Value eval(Context ctxt)
	{
		breakpoint.check(location, ctxt);

		ValueSet set = null;
		ValueMap map = null;

		try
		{
			set = right.eval(ctxt).setValue(ctxt);
			map = left.eval(ctxt).mapValue(ctxt);
		}
		catch (ValueException e)
		{
			return abort(e);
		}

		ValueMap modified = new ValueMap(map);

		for (Value k: map.keySet())
		{
			if (!set.contains(map.get(k)))

	public LessExpression(Expression left, LexToken op, Expression right)
	{
		super(left, op, right);
	}

	@Override
	public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope)
	{
		super.typeCheck(env, qualifiers, scope);
		return new BooleanType(location);
	}

	@Override
	public Value eval(Context ctxt)
	{
		breakpoint.check(location, ctxt);

		Value lv = left.eval(ctxt);
		Value rv = right.eval(ctxt);

		try
		{
			return new BooleanValue(lv.realValue(ctxt) < rv.realValue(ctxt));

		Context evalContext = new Context(location, "let statement", ctxt);

		LexNameToken sname = new LexNameToken(location.module, "self", location);
		ObjectValue self = (ObjectValue)ctxt.check(sname);

		for (Definition d: localDefs)
		{
			NameValuePairList values = d.getNamedValues(evalContext);

			if (self != null && d instanceof ExplicitFunctionDefinition)
			{
				for (NameValuePair nvp: values)
				{
					if (nvp.value instanceof FunctionValue)
					{
						FunctionValue fv = (FunctionValue)nvp.value;
						fv.setSelf(self);
					}
				}
			}

			evalContext.put(values);
		}

		return statement.eval(evalContext);

				Context evalContext = new Context(location, "let be st statement", ctxt);
				NameValuePairList nvpl = quantifiers.next();
				boolean matches = true;

				for (NameValuePair nvp: nvpl)
				{
					Value v = evalContext.get(nvp.name);

					if (v == null)
					{
						evalContext.put(nvp.name, nvp.value);
					}
					else
					{
						if (!v.equals(nvp.value))
						{
							matches = false;
							break;	// This quantifier set does not match
						}
					}
				}

				if (matches &&
					(suchThat == null || suchThat.eval(evalContext).boolValue(ctxt)))
				{
					return statement.eval(evalContext);