| Package | Description |
|---|---|
| wyc.builder |
Provides the classes responsible for actually translating WhileyFiles into WyilFiles.
|
| wyc.lang |
Provides core classes for the Abstract Syntax Tree (AST) used to represent Whiley source files.
|
| wyil.checks |
Provides classes responsible for validity checking of WYIL modules.
|
| wyil.lang |
Provides core classes for representing WYIL modules and bytecodes.
|
| wyil.util | |
| wyil.util.interpreter | |
| wyil.util.type |
| Modifier and Type | Method and Description |
|---|---|
static Type |
FlowTypeChecker.applySubstitution(List<String> lifetimeParameters,
List<String> lifetimeArguments,
Type original)
Apply a lifetime substitution: Substitute all parameters in original by
their arguments.
|
Type |
CompileTask.toSemanticType(wyal.lang.WyalFile.Type type,
WhileyFile.Context context)
Convert a Whiley "syntactic" type into a wyil type.
|
| Modifier and Type | Method and Description |
|---|---|
wycc.util.Pair<Constant,Type> |
FlowTypeChecker.resolveAsConstant(Expr e,
WhileyFile.Context context)
Resolve a given constant expression as a constant value.
|
wycc.util.Pair<Constant,Type> |
FlowTypeChecker.resolveAsConstant(wybs.lang.NameID nid)
Resolve a given name as a constant value.
|
| Modifier and Type | Method and Description |
|---|---|
static Type |
FlowTypeChecker.applySubstitution(List<String> lifetimeParameters,
List<String> lifetimeArguments,
Type original)
Apply a lifetime substitution: Substitute all parameters in original by
their arguments.
|
Type.EffectiveArray |
FlowTypeChecker.expandAsEffectiveArray(Type type,
wybs.lang.SyntacticElement element,
WhileyFile.Context context) |
Type.FunctionOrMethod |
FlowTypeChecker.expandAsEffectiveFunctionOrMethod(Type type,
wybs.lang.SyntacticElement element,
WhileyFile.Context context) |
Type.EffectiveRecord |
FlowTypeChecker.expandAsEffectiveRecord(Type type,
wybs.lang.SyntacticElement element,
WhileyFile.Context context) |
Type.Reference |
FlowTypeChecker.expandAsEffectiveReference(Type type,
wybs.lang.SyntacticElement element,
WhileyFile.Context context) |
| Modifier and Type | Method and Description |
|---|---|
wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>> |
FlowTypeChecker.resolveAsFunctionOrMethod(wybs.lang.NameID nid,
List<Type> parameters,
List<String> lifetimeArgs,
WhileyFile.Context context,
wyc.builder.FlowTypeChecker.Environment environment)
Responsible for determining the true type of a method or function being
invoked.
|
wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>> |
FlowTypeChecker.resolveAsFunctionOrMethod(String name,
List<Type> parameters,
List<String> lifetimeArgs,
WhileyFile.Context context,
wyc.builder.FlowTypeChecker.Environment environment)
Responsible for determining the true type of a method or function being
invoked.
|
| Modifier and Type | Field and Description |
|---|---|
Type |
Expr.AssignedVariable.afterType |
Type |
WhileyFile.Type.resolvedType |
Type |
Expr.BinOp.srcType |
Type |
Stmt.VariableDeclaration.type |
Type |
Expr.LocalVariable.type |
Type |
Expr.Cast.type |
Type |
Expr.TypeVal.type |
Type |
Expr.UnOp.type |
Type |
Expr.Quantifier.type |
Type |
Expr.ConstantAccess.type |
Type |
Expr.Record.type |
| Modifier and Type | Method and Description |
|---|---|
Type |
Expr.result()
Get the type that this expression will evaluate to.
|
Type |
Expr.AbstractVariable.result() |
Type |
Expr.LocalVariable.result() |
Type |
Expr.Constant.result() |
Type |
Expr.Cast.result() |
Type |
Expr.TypeVal.result() |
Type |
Expr.BinOp.result() |
Type |
Expr.IndexOf.result() |
Type |
Expr.UnOp.result() |
Type |
Expr.Quantifier.result() |
Type |
Expr.FieldAccess.result() |
Type |
Expr.ConstantAccess.result() |
Type |
Expr.Dereference.result() |
Type |
Expr.Record.result() |
Type |
Expr.AbstractInvoke.result() |
Type |
Expr.MethodCall.result() |
Type |
Expr.FunctionCall.result() |
Type |
Expr.PropertyCall.result() |
Type |
Expr.AbstractIndirectInvoke.result() |
Type |
Expr.IndirectMethodCall.result() |
Type |
Expr.IndirectFunctionCall.result() |
Type |
Expr.BinOp.srcType() |
| Modifier and Type | Method and Description |
|---|---|
List<Type> |
Expr.Multi.returns()
Get all the return types this expression can produce.
|
List<Type> |
Expr.FunctionOrMethodCall.returns() |
List<Type> |
Expr.IndirectFunctionOrMethodCall.returns() |
static HashSet<wycc.util.Pair<Type,String>> |
Exprs.uses(Expr expr,
WhileyFile.Context context)
Determine the set of variable names (and their types) used in a given expression.
|
| Modifier and Type | Method and Description |
|---|---|
protected void |
CoercionCheck.check(Type from,
Type to,
HashSet<wycc.util.Pair<Type,Type>> visited,
wybs.lang.SyntacticElement element)
Recursively check that there is no ambiguity in coercing type from into
type to.
|
| Modifier and Type | Method and Description |
|---|---|
protected void |
CoercionCheck.check(Type from,
Type to,
HashSet<wycc.util.Pair<Type,Type>> visited,
wybs.lang.SyntacticElement element)
Recursively check that there is no ambiguity in coercing type from into
type to.
|
protected void |
CoercionCheck.check(Type from,
Type to,
HashSet<wycc.util.Pair<Type,Type>> visited,
wybs.lang.SyntacticElement element)
Recursively check that there is no ambiguity in coercing type from into
type to.
|
| Modifier and Type | Interface and Description |
|---|---|
static interface |
Type.Array
An array type describes array values whose elements are subtypes of the
element type.
|
static interface |
Type.EffectiveArray
An effective array is a type which looks like an array, but is not
exactly an array.
|
static interface |
Type.EffectiveRecord
An effective record is a type which looks like a record, but is not
exactly a record.
|
static interface |
Type.EffectiveReference
An effective reference is a type which looks like an reference, but is
not exactly an reference.
|
static interface |
Type.Function
Represents the set of all function values.
|
static interface |
Type.FunctionOrMethod
Represents the set of all functions or methods.
|
static interface |
Type.Intersection
Represents the intersection of one or more types together.
|
static interface |
Type.Leaf
Represents a type which constitutes a "leaf" node in the type tree.
|
static interface |
Type.Method
Represents the set of all method values.
|
static interface |
Type.Negation
Represents the set of types which are not in a given type.
|
static interface |
Type.Nominal
Represents a named type within the system.
|
static interface |
Type.Primitive
Represents a primitive type (e.g.
|
static interface |
Type.Property
Represents the set of all proeprty values.
|
static interface |
Type.Record
A record is made up of a number of fields, each of which has a unique
name.
|
static interface |
Type.Reference
Represents a reference to an object in Whiley.
|
static interface |
Type.Union
Represents the union of one or more types together.
|
| Modifier and Type | Class and Description |
|---|---|
static class |
Type.Impl |
static class |
Type.Impl.Atom
An atom represents an indivisible type.
|
static class |
Type.Impl.Conjunctable
Represents either an atom or a conjunct
|
static class |
Type.Impl.Function
A function type, consisting of a list of zero or more parameters and
a return type.
|
static class |
Type.Impl.FunctionOrMethod |
static class |
Type.Impl.Method |
static class |
Type.Impl.PositiveAtom
A positive atom is any atom except a negation
|
static class |
Type.Impl.Primitive |
static class |
Type.Impl.Property |
| Modifier and Type | Field and Description |
|---|---|
static Type |
Type.T_ANY
The type any represents the type whose variables may hold any possible
value.
|
static Type |
Type.T_BOOL
Represents the set of boolean values (i.e.
|
static Type |
Type.T_BYTE
Represents a sequence of 8 bits.
|
static Type |
Type.T_INT
Represents the set of (unbound) integer values.
|
static Type |
Type.T_META
The type meta represents the type of types.
|
static Type |
Type.T_NULL
The null type is a special type which should be used to show the absence
of something.
|
static Type |
Type.T_VOID
A void type represents the type whose variables cannot exist! That is,
they cannot hold any possible value.
|
| Modifier and Type | Method and Description |
|---|---|
static Type |
Type.Array(Type element) |
Type[] |
Type.Intersection.bounds() |
Type[] |
Type.Union.bounds() |
Type |
Type.Array.element()
Get the element type of this array.
|
Type |
Type.Reference.element()
Return the type of the location that this reference refers to.
|
Type |
Type.Negation.element()
Get the element type of this array.
|
static Type |
Type.fromString(String str) |
static Type |
Type.Function(Type[] parameters,
Type[] returns) |
Type |
Type.Record.getField(String name)
Get the type of a given field in this record
|
Type |
Type.EffectiveArray.getReadableElementType()
Get the element type which could be read from this array.
|
Type |
Type.EffectiveReference.getReadableElementType()
Get the element type which could be read from this array.
|
Type |
Type.EffectiveRecord.getReadableFieldType(String field)
Get the element type which could be read from this array.
|
Type |
SyntaxTree.Location.getType()
Get the declared type of this location.
|
Type |
SyntaxTree.Location.getType(int i)
Get a specific type of this location.
|
Type[] |
SyntaxTree.Location.getTypes()
Get the types for this location.
|
Type |
Type.EffectiveArray.getWriteableElementType()
Get the element type which could be written to this array.
|
Type |
Type.EffectiveReference.getWriteableElementType()
Get the element type which could be written to this array.
|
Type |
Type.EffectiveRecord.getWriteableFieldType(String field)
Get the element type which could be written to this array.
|
static Type |
Type.Impl.intersectClosedClosedRecord(wyil.lang.Type.Impl.Record ith,
wyil.lang.Type.Impl.Record jth)
When intersecting two closed records, we require they both have the
same set of fields.
|
static Type |
Type.Intersection(Type... types)
Construct the intersection of one or more types together.
|
static Type |
Type.Impl.intersectOpenClosedRecord(wyil.lang.Type.Impl.Record open,
wyil.lang.Type.Impl.Record closed)
When intersecting an open record with a closed record.
|
static Type |
Type.Impl.intersectOpenOpenRecord(wyil.lang.Type.Impl.Record ith,
wyil.lang.Type.Impl.Record jth)
When intersecting an open record with another open record, there is
always a resulting intersection.
|
static Type |
Type.Method(Collection<String> lifetimeParameters,
Collection<String> contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(String[] lifetimeParameters,
String[] contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(Type[] parameters,
Type[] returns) |
static Type |
Type.Negation(Type type)
Construct the negation of a given type.
|
static Type |
Type.Nominal(wybs.lang.NameID name) |
Type |
Type.FunctionOrMethod.parameter(int i)
Get the ith parameter type
|
Type[] |
Type.FunctionOrMethod.params()
Get the list of parameter types which are accepted by this function
or method.
|
static Type |
Type.Property(Type[] parameters) |
static Type |
Type.Record(boolean isOpen,
List<wycc.util.Pair<Type,String>> fields) |
static Type |
Type.Record(boolean isOpen,
wycc.util.Pair<Type,String>... fields) |
static Type |
Type.Reference(String lifetime,
Type element) |
Type[] |
Type.FunctionOrMethod.returns()
Get the list of types which are returned by this function or method.
|
Type |
WyilFile.Type.type() |
abstract Type |
Constant.type() |
Type |
Constant.Null.type() |
Type |
Constant.Bool.type() |
Type |
Constant.Byte.type() |
Type |
Constant.Integer.type() |
Type |
Constant.Array.type() |
Type |
Constant.Record.type() |
Type |
Constant.Type.type() |
static Type |
Type.Union(Type... types)
Construct the union of one or more types together.
|
Type |
Constant.Type.value() |
| Modifier and Type | Method and Description |
|---|---|
static Type |
Type.Array(Type element) |
static Type |
Type.Function(Type[] parameters,
Type[] returns) |
static Type |
Type.Function(Type[] parameters,
Type[] returns) |
static Type |
Type.Intersection(Type... types)
Construct the intersection of one or more types together.
|
static Type |
Type.Method(Collection<String> lifetimeParameters,
Collection<String> contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(Collection<String> lifetimeParameters,
Collection<String> contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(String[] lifetimeParameters,
String[] contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(String[] lifetimeParameters,
String[] contextLifetimes,
Type[] parameters,
Type[] returns) |
static Type |
Type.Method(Type[] parameters,
Type[] returns) |
static Type |
Type.Method(Type[] parameters,
Type[] returns) |
static Type |
Type.Negation(Type type)
Construct the negation of a given type.
|
static Type |
Type.Property(Type[] parameters) |
static Type |
Type.Reference(String lifetime,
Type element) |
static Type.Impl[] |
Type.toImplOrVoid(Type[] types) |
static Type |
Type.Union(Type... types)
Construct the union of one or more types together.
|
Type.EffectiveRecord |
Type.EffectiveRecord.update(String field,
Type type)
Get an updated version of this record type after a given field has
been assigned a given type.
|
Type.EffectiveArray |
Type.EffectiveArray.update(Type element)
Determine a new type for this array after an assignment to a given
element.
|
| Modifier and Type | Method and Description |
|---|---|
static Type |
Type.Record(boolean isOpen,
List<wycc.util.Pair<Type,String>> fields) |
| Constructor and Description |
|---|
Location(SyntaxTree parent,
Type[] types,
T bytecode,
wybs.lang.Attribute... attributes) |
Location(SyntaxTree parent,
Type[] types,
T bytecode,
List<wybs.lang.Attribute> attributes) |
Location(SyntaxTree parent,
Type type,
T bytecode,
wybs.lang.Attribute... attributes) |
Location(SyntaxTree parent,
Type type,
T bytecode,
List<wybs.lang.Attribute> attributes) |
Type(Type type) |
Type(WyilFile parent,
Collection<Modifier> modifiers,
String name,
Type type,
wybs.lang.Attribute... attributes) |
Type(WyilFile parent,
Collection<Modifier> modifiers,
String name,
Type type,
Collection<wybs.lang.Attribute> attributes) |
| Modifier and Type | Method and Description |
|---|---|
Type |
TypeSystem.expandOneLevel(Type type)
Expand a given syntactic type by exactly one level.
|
| Modifier and Type | Method and Description |
|---|---|
static String |
ErrorMessages.errorMessage(wyil.util.ErrorMessages.MsgWithTypeParams msg,
Type t1,
Type t2)
Return the error message for an error with two type parameters.
|
static String |
ErrorMessages.errorMessage(wyil.util.ErrorMessages.MsgWithTypeParam msg,
Type t1)
Return the error message for an error with a single type parameter.
|
Type.EffectiveArray |
TypeSystem.expandAsEffectiveArray(Type type)
Assuming given type is an effective array of some sort, expand to ensure
array structure is visible.
|
Type.EffectiveRecord |
TypeSystem.expandAsEffectiveRecord(Type type)
Assuming given type is an effective record of some sort, expand to ensure
record structure is visible.
|
Type.FunctionOrMethod |
TypeSystem.expandAsFunctionOrMethod(Type type)
Assuming given type is an effective function or method type of some sort,
expand to ensure structure is visible.
|
Type.Reference |
TypeSystem.expandAsReference(Type type)
Assuming given type is an effective reference of some sort, expand to
ensure reference structure is visible.
|
Type |
TypeSystem.expandOneLevel(Type type)
Expand a given syntactic type by exactly one level.
|
boolean |
TypeSystem.isContractive(Type type)
Contractive types are types which cannot accept value because they have
an unterminated cycle.
|
boolean |
TypeSystem.isEmpty(Type type)
Determine whether or not this type corresponds to the empty type or not.
|
boolean |
TypeSystem.isExplicitCoerciveSubtype(Type t1,
Type t2)
Determine whether type
t2 is an explicit coercive
subtype of type t1. |
boolean |
TypeSystem.isExplicitCoerciveSubtype(Type t1,
Type t2,
LifetimeRelation lr)
Determine whether type
t2 is an explicit coercive
subtype of type t1. |
boolean |
TypeSystem.isSubtype(Type t1,
Type t2)
Determine whether type
t2 is a subtype of type
t1 (written t1 :> t2). |
boolean |
TypeSystem.isSubtype(Type t1,
Type t2,
LifetimeRelation lr)
Determine whether type
t2 is a subtype of type
t1 (written t1 :> t2). |
Automaton |
TypeSystem.toAutomaton(Type type)
Expand a given type by inlining all visible nominal information.
|
| Modifier and Type | Method and Description |
|---|---|
Type |
Interpreter.ConstantObject.type() |
Type |
Interpreter.ConstantLambda.type() |
| Modifier and Type | Method and Description |
|---|---|
boolean |
Interpreter.isMemberOfType(Constant value,
Type type,
wybs.lang.SyntacticElement context)
Determine whether a given value is a member of a given type.
|
| Modifier and Type | Method and Description |
|---|---|
Type |
TypeParser.parse() |
Type |
TypeParser.parse(HashSet<String> typeVariables) |
Type |
TypeParser.parseBraceTerm(HashSet<String> typeVariables) |
Type |
TypeParser.parseNotTerm(HashSet<String> typeVariables) |
Type |
TypeParser.parseTerm(HashSet<String> typeVariables) |
Copyright © 2017. All rights reserved.