Class Property

src/main/java/wyil/lang/WyilFile.java:1056–1108

Represents a property declaration in a Whiley source file. For example: property contains(int[] xs, int x) where some { i in 0..|xs| | xs[i] == x} Here, a property contains is defined which captures the concept of an element being contained in an array.

		 *
		 */
		public static class Property extends Callable {

			public Property(Tuple<Modifier> modifiers, Identifier name, Tuple<Template.Variable> template,
					Tuple<Decl.Variable> parameters, Tuple<Decl.Variable> returns, Tuple<Expr> requires, Stmt.Block body) {
				super(DECL_property, modifiers, name, template, parameters, returns,requires, body);
			}

			@Override
			public WyilFile.Type.Property getType() {
				return new WyilFile.Type.Property(project(getParameters()), project(getReturns()));
			}

			@SuppressWarnings("unchecked")
			public Tuple<Expr> getRequires() {
				return (Tuple<Expr>) get(5);
			}

			@Override
			@SuppressWarnings("unchecked")
			public Stmt.Block getBody() {
				return (Stmt.Block) get(6);
			}

			@SuppressWarnings("unchecked")
			@Override
			public Property clone(Syntactic.Item[] operands) {
				return new Property((Tuple<Modifier>) operands[0], (Identifier) operands[1],
						(Tuple<Template.Variable>) operands[2], (Tuple<Decl.Variable>) operands[3],
						(Tuple<Decl.Variable>) operands[4], (Tuple<Expr>) operands[5], (Stmt.Block) operands[6]);
			}

			public static final Descriptor DESCRIPTOR_0 = new Descriptor(Operands.SIX, Data.ZERO, "DECL_property") {
				@SuppressWarnings("unchecked")
				@Override
				public Syntactic.Item construct(int opcode, Syntactic.Item[] operands, byte[] data) {
					Tuple<Expr> es = (Tuple<Expr>) operands[5];
					Stmt.Block block = new Stmt.Block(new Stmt.Return(new Expr.LogicalAnd(es)));
					return new Property((Tuple<Modifier>) operands[0], (Identifier) operands[1],
							(Tuple<Template.Variable>) operands[2], (Tuple<Decl.Variable>) operands[3],
							(Tuple<Decl.Variable>) operands[4], new Tuple<Expr>(), block);
				}
			};

			public static final Descriptor DESCRIPTOR_1 = new Descriptor(Operands.SEVEN, Data.ZERO, "DECL_property") {
				@SuppressWarnings("unchecked")
				@Override
				public Syntactic.Item construct(int opcode, Syntactic.Item[] operands, byte[] data) {
					return new Property((Tuple<Modifier>) operands[0], (Identifier) operands[1],
							(Tuple<Template.Variable>) operands[2], (Tuple<Decl.Variable>) operands[3],
							(Tuple<Decl.Variable>) operands[4], (Tuple<Expr>) operands[5], (Stmt.Block) operands[5]);
				}
			};
		}

		/**
		 * A variant is a two state property.