|
/**
|
|
*
|
|
* OOAS Compiler (Deprecated)
|
|
*
|
|
* Copyright 2015, Institute for Software Technology, Graz University of
|
|
* Technology. Portions are copyright 2015 by the AIT Austrian Institute
|
|
* of Technology. All rights reserved.
|
|
*
|
|
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
|
|
*
|
|
* Please notice that this version of the OOAS compiler is considered de-
|
|
* precated. Only the Java version is maintained.
|
|
*
|
|
* Contributors:
|
|
* Willibald Krenn (TU Graz/AIT)
|
|
* Stefan Tiran (TU Graz/AIT)
|
|
*/
|
|
|
|
using System;
|
|
using System.Collections.Generic;
|
|
using Antlr.Runtime;
|
|
|
|
namespace TUG.Mogentes
|
|
{
|
|
public enum ExpressionKind
|
|
{
|
|
/*tern.*/
|
|
conditional,
|
|
/*map binary*/
|
|
domresby, domresto, rngresby, rngresto, munion,
|
|
/*set/list binary*/
|
|
conc, diff, inter, elemin, notelemin, subset, union,
|
|
/*numeric binary*/
|
|
div, greater, greaterequal, idiv, less, lessequal, minus, mod, pow, prod, sum,
|
|
/*bool binary*/
|
|
and, biimplies, implies, or,
|
|
/*other binary*/
|
|
equal, notequal, seqmod_mapoverride,
|
|
/*map unary*/
|
|
dom, range, merge,
|
|
/*set/list unary*/
|
|
card, dconc, dinter, dunion, elems, head, inds, len, tail,
|
|
/*unary numberic*/
|
|
unminus, unplus, not, abs,
|
|
/*unary quantors*/
|
|
forall, exists,
|
|
/*Constructors*/
|
|
ListConstr, SetConstr, MapConstr, TupleConstr, ObjectConstr, QValConstr,
|
|
/* constant, identifier */
|
|
Value, Identifier, UnresolvedIdentifier, Type,
|
|
/* tuple access and method call */
|
|
TupleMapAccess, Call,
|
|
/* point operator */
|
|
Access,
|
|
/* primed */
|
|
Primed,
|
|
/* cast */
|
|
Cast,
|
|
/* fold */
|
|
foldLR, foldRL
|
|
}
|
|
|
|
/*
|
|
public enum UnaryOperatorType { unminus, unplus, not, abs }
|
|
public enum SetListUnaryOperatorType { card, dconc, dinter, dunion, elems, head, inds, len, tail }
|
|
public enum MapUnaryOperatorType { dom, range, merge }
|
|
public enum BinaryOperatorType { equal, notequal, seqmod_mapoverride }
|
|
public enum BoolBinaryOperatorType { and, biimplies, implies, or }
|
|
public enum NumericBinaryOperatorType { div, greater, greaterequal, idiv, less, lessequal, minus, mod, pow, prod, sum }
|
|
public enum SetListBinaryOperatorType { conc, diff, inter, elemin, notelemin, subset, union }
|
|
public enum MapBinaryOperatorType { domresby, domresto, rngresby, rngresto, munion }
|
|
*/
|
|
|
|
///////////////////////////////////////////////
|
|
/// Expressions
|
|
///
|
|
/// Note: Since we allow expression of the form
|
|
/// myTuple(a,b) = hd x, where a and b are newly
|
|
/// introduced placeholders, the expression knows
|
|
/// about local variables.
|
|
/// Scoping: Consider following expression
|
|
/// 3 > a and myTuple(b,d) = hd e and b < 5
|
|
/// which gives
|
|
/// and
|
|
/// / \
|
|
/// / and
|
|
/// / / \
|
|
/// > = <
|
|
/// / \ / \ / \
|
|
/// 3 a (b,d) e b 5
|
|
/// the scope of b and d is defined by the binary
|
|
/// expression that has the leaf within its left child
|
|
/// (== the second 'and').
|
|
/// Local variables may only be introduced in constructors
|
|
/// of sets, lists, and tuples. Therefore the type is
|
|
/// known.
|
|
|
|
|
|
public abstract class Expression : UlyssesBasicClass, IAst
|
|
{
|
|
protected ExpressionKind m_kind;
|
|
protected UlyssesType m_type;
|
|
protected int m_line;
|
|
protected int m_pos;
|
|
protected SymbolTable m_freeVariables;
|
|
protected List<FunctionIdentifier> m_callTargets;
|
|
|
|
public ExpressionKind kind { get { return m_kind; } }
|
|
public UlyssesType type { get { return m_type; } }
|
|
public int line { get { return m_line; } }
|
|
public int pos { get { return m_pos; } }
|
|
public SymbolTable freeVariables { get { return m_freeVariables; } }
|
|
public List<FunctionIdentifier> callTargets { get { return m_callTargets; } }
|
|
|
|
public Expression(ExpressionKind aKind, int line, int pos)
|
|
{
|
|
m_kind = aKind;
|
|
m_line = line;
|
|
m_pos = pos;
|
|
m_callTargets = new List<FunctionIdentifier>();
|
|
}
|
|
|
|
public Expression(Expression toCopy)
|
|
{
|
|
m_kind = toCopy.m_kind;
|
|
m_line = toCopy.m_line;
|
|
m_pos = toCopy.m_pos;
|
|
m_callTargets = new List<FunctionIdentifier>(toCopy.callTargets);
|
|
m_type = toCopy.m_type;
|
|
m_freeVariables = new SymbolTable(toCopy.m_freeVariables);
|
|
}
|
|
|
|
public virtual Expression Clone()
|
|
{
|
|
throw new NotImplementedException();
|
|
}
|
|
|
|
public void SetType(UlyssesType aType)
|
|
{
|
|
if (aType == null)
|
|
throw new ArgumentException();
|
|
m_type = aType;
|
|
}
|
|
|
|
public void SetFreeVariables(SymbolTable aSymTab)
|
|
{
|
|
m_freeVariables = aSymTab;
|
|
}
|
|
|
|
public List<ExpressionVariableIdentifier> GetUninitializedFreeVariables()
|
|
{
|
|
List<ExpressionVariableIdentifier> result = new List<ExpressionVariableIdentifier>();
|
|
if (m_freeVariables != null)
|
|
foreach (var v in m_freeVariables.symbolList)
|
|
{
|
|
ExpressionVariableIdentifier id = (ExpressionVariableIdentifier)v;
|
|
if (id.initialized == false)
|
|
result.Add(id);
|
|
}
|
|
return result;
|
|
}
|
|
|
|
|
|
#region IAst Member
|
|
|
|
public AstNodeTypeEnum nodeType { get { return AstNodeTypeEnum.expression; } }
|
|
|
|
public virtual void Accept(IAstVisitor visitor)
|
|
{
|
|
throw new NotImplementedException();
|
|
}
|
|
|
|
#endregion
|
|
|
|
|
|
/// <summary>
|
|
/// Calculates the arithmetic cover, i.e. the return type of the operation, given two types.
|
|
/// This is different from the cover-method defined at the type level.
|
|
/// Note: We do saturating operations on the type boundaries.
|
|
/// </summary>
|
|
public static UlyssesType ArithmeticCover(UlyssesType type1, UlyssesType type2, ExpressionKind op)
|
|
{
|
|
if (!type1.IsNumeric() || (type2 != null && !type2.IsNumeric()))
|
|
throw new ArgumentException();
|
|
|
|
if (type1 is ValuedEnumType)
|
|
type1 = ((ValuedEnumType)type1).getIntType();
|
|
if (type2 is ValuedEnumType)
|
|
type2 = ((ValuedEnumType)type2).getIntType();
|
|
|
|
AbstractRange result;
|
|
AbstractRange rangeType1 = null;
|
|
AbstractRange rangeType2 = null;
|
|
AbstractOperations operations;
|
|
bool resultIsFloat = type1.kind == TypeKind.FloatType
|
|
|| op == ExpressionKind.div
|
|
|| (type2 != null && type2.kind == TypeKind.FloatType);
|
|
if (resultIsFloat)
|
|
{
|
|
rangeType1 = new DoubleRange(
|
|
type1.kind == TypeKind.IntType ? ((IntType)type1).rangeHigh : ((FloatType)type1).high,
|
|
type1.kind == TypeKind.IntType ? ((IntType)type1).rangeLow : ((FloatType)type1).low);
|
|
if (type2 != null)
|
|
{
|
|
rangeType2 = new DoubleRange(
|
|
type2.kind == TypeKind.IntType ? ((IntType)type2).rangeHigh : ((FloatType)type2).high,
|
|
type2.kind == TypeKind.IntType ? ((IntType)type2).rangeLow : ((FloatType)type2).low);
|
|
}
|
|
operations = new SaturatedDoubleOperations();
|
|
}
|
|
else
|
|
{
|
|
rangeType1 = new IntegerRange(((IntType)type1).rangeHigh, ((IntType)type1).rangeLow);
|
|
rangeType2 = new IntegerRange(((IntType)type2).rangeHigh, ((IntType)type2).rangeLow);
|
|
operations = new SaturatedIntegerOperations();
|
|
}
|
|
|
|
switch (op)
|
|
{
|
|
case ExpressionKind.pow:
|
|
case ExpressionKind.prod:
|
|
case ExpressionKind.unminus:
|
|
case ExpressionKind.unplus:
|
|
case ExpressionKind.minus:
|
|
case ExpressionKind.sum:
|
|
case ExpressionKind.div:
|
|
result = operations.GenericArithmeticCover(rangeType1, rangeType2, op);
|
|
break;
|
|
|
|
case ExpressionKind.idiv:
|
|
if (resultIsFloat)
|
|
throw new ArgumentException();
|
|
System.Diagnostics.Debug.Assert(type2 != null);
|
|
result = operations.GenericArithmeticCover(rangeType1, rangeType2, op);
|
|
break;
|
|
case ExpressionKind.mod:
|
|
if (resultIsFloat)
|
|
throw new ArgumentException();
|
|
System.Diagnostics.Debug.Assert(type2 != null);
|
|
result = new IntegerRange(((IntegerRange)rangeType2).max - 1, 0);
|
|
break;
|
|
|
|
default:
|
|
throw new NotImplementedException();
|
|
}
|
|
|
|
if (resultIsFloat)
|
|
return new FloatType(((DoubleRange)result).min, ((DoubleRange)result).max, FloatType.defaultPrecision, null);
|
|
else
|
|
// this is crude, but see whether it works..
|
|
return new IntType(((IntegerRange)result).min, ((IntegerRange)result).max, null);
|
|
}
|
|
|
|
|
|
public override string ToString()
|
|
{
|
|
OoaPrintVisitor visitor = new OoaPrintVisitor(null);
|
|
this.Accept(visitor);
|
|
return visitor.ToString();
|
|
}
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// === Leaf Expressions ===
|
|
///
|
|
public enum LeafTypeEnum { unset, boolean, integer, real, chr, qval, reference, identifier, type, complex }
|
|
public abstract class LeafExpression : Expression
|
|
{
|
|
protected LeafTypeEnum m_valueType;
|
|
|
|
public LeafTypeEnum valueType { get { return m_valueType; } }
|
|
|
|
public LeafExpression(LeafTypeEnum avalueType, ExpressionKind aKind, int line, int pos)
|
|
: base(aKind, line, pos)
|
|
{
|
|
m_valueType = avalueType;
|
|
}
|
|
|
|
public LeafExpression(LeafExpression toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_valueType = toCopy.m_valueType;
|
|
}
|
|
}
|
|
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Some constant bool, int, float, char,
|
|
/// qval or nil value
|
|
///
|
|
public sealed class ValueExpression<T> : LeafExpression
|
|
{
|
|
private T m_value;
|
|
|
|
public T value { get { return m_value; } }
|
|
|
|
public ValueExpression(T aValue, int line, int pos)
|
|
: base(LeafTypeEnum.unset, ExpressionKind.Value, line, pos)
|
|
{
|
|
m_value = aValue;
|
|
if (typeof(T) == typeof(int))
|
|
m_valueType = LeafTypeEnum.integer;
|
|
else if (typeof(T) == typeof(bool))
|
|
m_valueType = LeafTypeEnum.boolean;
|
|
else if (typeof(T) == typeof(double))
|
|
m_valueType = LeafTypeEnum.real;
|
|
else if (typeof(T) == typeof(char))
|
|
m_valueType = LeafTypeEnum.chr;
|
|
else if (typeof(T).IsSubclassOf(typeof(QrType)))
|
|
m_valueType = LeafTypeEnum.qval;
|
|
else if (typeof(T).IsClass)
|
|
m_valueType = LeafTypeEnum.reference;
|
|
else
|
|
throw new ArgumentException();
|
|
}
|
|
|
|
public ValueExpression(ValueExpression<T> toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_value = toCopy.m_value;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new ValueExpression<T>(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit<T>(this);
|
|
}
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Some identifier
|
|
///
|
|
public class IdentifierExpression : LeafExpression
|
|
{
|
|
protected Identifier m_identifier;
|
|
protected bool m_self;
|
|
|
|
public Identifier identifier { get { return m_identifier; } }
|
|
public bool isSelf { get { return m_self; } }
|
|
|
|
public IdentifierExpression(Identifier anIdentifier, int line, int pos)
|
|
: base(LeafTypeEnum.identifier, ExpressionKind.Identifier, line, pos)
|
|
{
|
|
m_identifier = anIdentifier;
|
|
if (anIdentifier != null)
|
|
m_type = m_identifier.type;
|
|
m_self = false;
|
|
}
|
|
|
|
public IdentifierExpression(IdentifierExpression toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_identifier = toCopy.m_identifier;
|
|
m_self = toCopy.m_self;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new IdentifierExpression(this);
|
|
}
|
|
|
|
public void setIsSelf(bool newValue)
|
|
{
|
|
m_self = newValue;
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetIdentifier(Identifier newIdentifier)
|
|
{
|
|
m_identifier = newIdentifier;
|
|
}
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Some identifier
|
|
///
|
|
public class TypeExpression : LeafExpression
|
|
{
|
|
public TypeExpression(UlyssesType atype, int line, int pos)
|
|
: base(LeafTypeEnum.type, ExpressionKind.Type, line, pos)
|
|
{
|
|
m_type = atype;
|
|
}
|
|
|
|
public TypeExpression(TypeExpression toCopy)
|
|
: base(toCopy)
|
|
{ }
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new TypeExpression(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Some unresolved identifier
|
|
///
|
|
public sealed class UnresolvedIdentifierExpression : IdentifierExpression
|
|
{
|
|
private IScope m_scope;
|
|
private string m_tokenText;
|
|
|
|
|
|
public string tokenText { get { return m_tokenText; } }
|
|
public IScope scope { get { return m_scope; } }
|
|
|
|
public UnresolvedIdentifierExpression(IToken identifier, IScope aScope)
|
|
: base(null, identifier.Line, identifier.CharPositionInLine)
|
|
{
|
|
m_kind = ExpressionKind.UnresolvedIdentifier;
|
|
m_tokenText = identifier.Text;
|
|
m_scope = aScope;
|
|
}
|
|
|
|
public UnresolvedIdentifierExpression(UnresolvedIdentifierExpression toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_scope = toCopy.m_scope;
|
|
m_tokenText = toCopy.m_tokenText;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new UnresolvedIdentifierExpression(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// constructors
|
|
///
|
|
public abstract class TypeConstructionExpression : LeafExpression
|
|
{
|
|
public TypeConstructionExpression(ExpressionKind aKind, int line, int pos)
|
|
: base(LeafTypeEnum.complex, aKind, line, pos)
|
|
{ }
|
|
public TypeConstructionExpression(TypeConstructionExpression toCopy)
|
|
: base(toCopy)
|
|
{ }
|
|
}
|
|
|
|
public sealed class ObjectConstructor : TypeConstructionExpression
|
|
{
|
|
private List<OoActionSystemInstance> m_instances;
|
|
private int m_currentInstance;
|
|
private string m_fixedObjectName;
|
|
|
|
public int currentInstance { get { return m_currentInstance; } }
|
|
public List<OoActionSystemInstance> instances { get { return m_instances; } }
|
|
public string givenObjectName { get { return m_fixedObjectName; } }
|
|
|
|
public void ResetCurrentInstance() { m_currentInstance = 0; }
|
|
|
|
public ObjectConstructor(OpaqueType aType, int line, int pos)
|
|
: base(ExpressionKind.ObjectConstr, line, pos)
|
|
{
|
|
SetType(aType);
|
|
m_instances = new List<OoActionSystemInstance>();
|
|
m_currentInstance = 0;
|
|
}
|
|
|
|
public ObjectConstructor(OpaqueType aType, string aName, int line, int pos)
|
|
: base(ExpressionKind.ObjectConstr, line, pos)
|
|
{
|
|
SetType(aType);
|
|
m_instances = new List<OoActionSystemInstance>();
|
|
m_currentInstance = 0;
|
|
m_fixedObjectName = aName;
|
|
}
|
|
|
|
|
|
public ObjectConstructor(ObjectConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_instances = new List<OoActionSystemInstance>( toCopy.m_instances);
|
|
m_currentInstance = toCopy.m_currentInstance;
|
|
m_fixedObjectName = toCopy.m_fixedObjectName;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new ObjectConstructor(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void AddInstance(OoActionSystemInstance anInstance)
|
|
{
|
|
m_instances.Add(anInstance);
|
|
}
|
|
|
|
public OoActionSystemInstance GetNextInstance()
|
|
{
|
|
OoActionSystemInstance result = m_instances[m_currentInstance];
|
|
m_currentInstance++;
|
|
return result;
|
|
}
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Constructor: List
|
|
///
|
|
public sealed class ListConstructor : TypeConstructionExpression, IScope
|
|
{
|
|
private List<Expression> m_elements;
|
|
private IScope m_parentScope;
|
|
private SymbolTable m_comprehensionVars;
|
|
private Expression m_comprehension;
|
|
private bool m_hasComprehension = false;
|
|
|
|
public List<Expression> elements { get { return m_elements; } }
|
|
public Expression comprehension { get { return m_comprehension; } }
|
|
public bool hasComprehension { get { return m_hasComprehension; } }
|
|
public SymbolTable comprehensionVariables { get { return m_comprehensionVars; } }
|
|
|
|
public ListConstructor(int line, int pos)
|
|
: base(ExpressionKind.ListConstr, line, pos)
|
|
{
|
|
m_elements = new List<Expression>();
|
|
m_comprehensionVars = new SymbolTable();
|
|
}
|
|
|
|
public ListConstructor(ListConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_elements = new List<Expression>(toCopy.m_elements);
|
|
m_parentScope = toCopy.m_parentScope;
|
|
m_comprehensionVars = new SymbolTable(toCopy.m_comprehensionVars);
|
|
m_comprehension = toCopy.m_comprehension;
|
|
m_hasComprehension = toCopy.m_hasComprehension;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new ListConstructor(this);
|
|
}
|
|
|
|
public void AddElement(Expression anElement)
|
|
{
|
|
m_elements.Add(anElement);
|
|
}
|
|
|
|
public void SetComprehension(Expression comprehension)
|
|
{
|
|
m_comprehension = comprehension;
|
|
}
|
|
|
|
public void SetHasComprehension(bool flag)
|
|
{
|
|
m_hasComprehension = flag;
|
|
}
|
|
|
|
public Identifier ResolveIdentifier(string aName)
|
|
{
|
|
if (m_comprehensionVars.Defined(aName))
|
|
return m_comprehensionVars.Get(aName);
|
|
else
|
|
return null;
|
|
}
|
|
|
|
public IScope GetParentScope()
|
|
{
|
|
return m_parentScope;
|
|
}
|
|
|
|
public void SetParentScope(IScope parentScope)
|
|
{
|
|
m_parentScope = parentScope;
|
|
}
|
|
|
|
public void AddIdentifier(Identifier anIdentifier, object tag)
|
|
{
|
|
m_comprehensionVars.AddIdentifier(anIdentifier);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetElements(List<Expression> newElements)
|
|
{
|
|
m_elements = newElements;
|
|
}
|
|
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Constructor: Set
|
|
///
|
|
public sealed class SetConstructor : TypeConstructionExpression, IScope
|
|
{
|
|
private List<Expression> m_items;
|
|
private SymbolTable m_comprehensionVars;
|
|
private IScope m_parentScope;
|
|
private Expression m_comprehension;
|
|
private bool m_hasComprehension = false;
|
|
|
|
public List<Expression> items { get { return m_items; } }
|
|
public Expression comprehension { get { return m_comprehension; } }
|
|
public bool hasComprehension { get { return m_hasComprehension; } }
|
|
public SymbolTable comprehensionVariables { get { return m_comprehensionVars; } }
|
|
|
|
public SetConstructor(int line, int pos)
|
|
: base(ExpressionKind.SetConstr, line, pos)
|
|
{
|
|
m_items = new List<Expression>();
|
|
m_comprehensionVars = new SymbolTable();
|
|
}
|
|
|
|
public SetConstructor(SetConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_items = new List<Expression>(toCopy.m_items);
|
|
m_comprehensionVars = new SymbolTable(toCopy.m_comprehensionVars);
|
|
m_parentScope = toCopy.m_parentScope;
|
|
m_comprehension = toCopy.m_comprehension;
|
|
m_hasComprehension = toCopy.m_hasComprehension;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new SetConstructor(this);
|
|
}
|
|
|
|
public void AddItem(Expression anItem)
|
|
{
|
|
m_items.Add(anItem);
|
|
}
|
|
|
|
public void SetComprehension(Expression anExpr)
|
|
{
|
|
m_comprehension = anExpr;
|
|
}
|
|
|
|
public void SetHasComprehension(bool flag)
|
|
{
|
|
m_hasComprehension = flag;
|
|
}
|
|
|
|
public Identifier ResolveIdentifier(string aName)
|
|
{
|
|
if (m_comprehensionVars.Defined(aName))
|
|
return m_comprehensionVars.Get(aName);
|
|
else
|
|
return null;
|
|
}
|
|
|
|
public IScope GetParentScope()
|
|
{
|
|
return m_parentScope;
|
|
}
|
|
|
|
public void SetParentScope(IScope parentScope)
|
|
{
|
|
m_parentScope = parentScope;
|
|
}
|
|
|
|
public void AddIdentifier(Identifier anIdentifier, object tag)
|
|
{
|
|
m_comprehensionVars.AddIdentifier(anIdentifier);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetItems(List<Expression> newItems)
|
|
{
|
|
m_items = newItems;
|
|
}
|
|
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Constructor: Map
|
|
///
|
|
public sealed class MapConstructor : TypeConstructionExpression
|
|
{
|
|
public sealed class MapItem
|
|
{
|
|
public Expression key;
|
|
public Expression value;
|
|
public MapItem(Expression aKey, Expression aValue)
|
|
{
|
|
key = aKey;
|
|
value = aValue;
|
|
}
|
|
public MapItem(MapItem toCopy)
|
|
{
|
|
key = toCopy.key;
|
|
value = toCopy.value;
|
|
}
|
|
}
|
|
|
|
private List<MapItem> m_items;
|
|
|
|
public List<MapItem> items { get { return m_items; } }
|
|
|
|
public MapConstructor(int line, int pos)
|
|
: base(ExpressionKind.MapConstr, line, pos)
|
|
{
|
|
m_items = new List<MapItem>();
|
|
}
|
|
|
|
public MapConstructor(MapConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_items = new List<MapItem>(toCopy.m_items);
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new MapConstructor(this);
|
|
}
|
|
|
|
public void AddItem(Expression mapFrom, Expression mapTo)
|
|
{
|
|
MapItem newitem = new MapItem(mapFrom, mapTo);
|
|
m_items.Add(newitem);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetItems(List<MapItem> newItems)
|
|
{
|
|
m_items = newItems;
|
|
}
|
|
|
|
}
|
|
|
|
///////////////////////////////////////////////
|
|
/// Constructor: Tuple
|
|
///
|
|
public sealed class TupleConstructor : TypeConstructionExpression
|
|
{
|
|
private List<Expression> m_values;
|
|
private Identifier m_tupleType;
|
|
private bool m_matcher;
|
|
|
|
public List<Expression> values { get { return m_values; } }
|
|
public Identifier tupleType { get { return m_tupleType; } }
|
|
public bool isMatcher { get { return m_matcher; } }
|
|
|
|
|
|
public TupleConstructor(Identifier aType, System.Collections.Generic.List<Expression> exprs, int line, int pos)
|
|
: base(ExpressionKind.TupleConstr, line, pos)
|
|
{
|
|
m_tupleType = aType;
|
|
m_values = new List<Expression>(exprs);
|
|
m_matcher = false;
|
|
}
|
|
|
|
public TupleConstructor(TupleConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_values = new List<Expression>(toCopy.m_values);
|
|
m_tupleType = toCopy.m_tupleType;
|
|
m_matcher = toCopy.m_matcher;
|
|
}
|
|
|
|
public void SetIsMatcher(bool newVal)
|
|
{
|
|
m_matcher = newVal;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new TupleConstructor(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetTupleValues(List<Expression> values)
|
|
{
|
|
m_values = values;
|
|
}
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Constructor: Qualitative Value
|
|
///
|
|
public enum QValDeriv { DonTCare, Dec, Steady, Inc }
|
|
public sealed class QValConstructor : TypeConstructionExpression
|
|
{
|
|
private Expression[] m_value;
|
|
private QValDeriv m_derivValue;
|
|
|
|
public Expression[] value { get { return m_value; } }
|
|
public QValDeriv valueDeriv { get { return m_derivValue; } }
|
|
|
|
|
|
public QValConstructor(int line, int pos) :
|
|
base(ExpressionKind.QValConstr, line, pos)
|
|
{
|
|
m_value = new Expression[1];
|
|
m_value[0] = null;
|
|
m_derivValue = QValDeriv.DonTCare;
|
|
}
|
|
|
|
public QValConstructor(QValConstructor toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_value = new Expression[toCopy.m_value.Length];
|
|
Array.Copy(toCopy.m_value, m_value, m_value.Length);
|
|
m_derivValue = toCopy.m_derivValue;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new QValConstructor(this);
|
|
}
|
|
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetValue(Expression aval)
|
|
{
|
|
m_value[0] = aval;
|
|
}
|
|
|
|
public void AddRange(Expression toRange)
|
|
{
|
|
Expression currVal = m_value[0];
|
|
m_value = new Expression[2];
|
|
m_value[0] = currVal;
|
|
m_value[1] = toRange;
|
|
}
|
|
|
|
public void SetDerivation(QValDeriv newValue)
|
|
{
|
|
m_derivValue = newValue;
|
|
}
|
|
}
|
|
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// === Binary Operator ===
|
|
///
|
|
public class BinaryOperator : Expression
|
|
{
|
|
protected Expression m_left;
|
|
protected Expression m_right;
|
|
|
|
public Expression left { get { return m_left; } }
|
|
public Expression right { get { return m_right; } }
|
|
|
|
|
|
public BinaryOperator(ExpressionKind aKind, Expression left, Expression right, int line, int pos)
|
|
: base(aKind, line, pos)
|
|
{
|
|
m_left = left;
|
|
m_right = right;
|
|
}
|
|
|
|
public BinaryOperator(BinaryOperator toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_left = toCopy.m_left;
|
|
m_right = toCopy.m_right;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new BinaryOperator(this);
|
|
}
|
|
|
|
public void SetRightChild(Expression child)
|
|
{
|
|
m_right = child;
|
|
}
|
|
|
|
public void SetLeftChild(Expression child)
|
|
{
|
|
m_left = child;
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Element Access (Point operator): a.b
|
|
///
|
|
public sealed class AccessExpression : BinaryOperator
|
|
{
|
|
public AccessExpression(IdentifierExpression anIdentifier, Expression child, int line, int pos)
|
|
: base(ExpressionKind.Access, anIdentifier, child, line, pos)
|
|
{ }
|
|
|
|
public AccessExpression(Expression anExpression, Expression child, int line, int pos)
|
|
: base(ExpressionKind.Access, anExpression, child, line, pos)
|
|
{ }
|
|
|
|
public AccessExpression(AccessExpression toCopy)
|
|
: base(toCopy)
|
|
{ }
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new AccessExpression(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// === Ternary Operator ===
|
|
///
|
|
public sealed class TernaryOperator : Expression
|
|
{
|
|
private Expression m_left;
|
|
private Expression m_mid;
|
|
private Expression m_right;
|
|
private IScope m_definingScope;
|
|
|
|
public Expression left { get { return m_left; } }
|
|
public Expression mid { get { return m_mid; } }
|
|
public Expression right { get { return m_right; } }
|
|
public IScope definingScope { get { return m_definingScope; } }
|
|
|
|
public TernaryOperator(ExpressionKind aKind, Expression left, Expression mid, Expression right, int line, int pos, IScope aScope)
|
|
: base(aKind, line, pos)
|
|
{
|
|
m_left = left;
|
|
m_mid = mid;
|
|
m_right = right;
|
|
m_definingScope = aScope;
|
|
}
|
|
|
|
public TernaryOperator(TernaryOperator toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_left = toCopy.m_left;
|
|
m_mid = toCopy.m_mid;
|
|
m_right = toCopy.m_right;
|
|
m_definingScope = toCopy.definingScope;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new TernaryOperator(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetLeftChild(Expression newExpression)
|
|
{
|
|
m_left = newExpression;
|
|
}
|
|
public void SetMidChild(Expression newExpression)
|
|
{
|
|
m_mid = newExpression;
|
|
}
|
|
public void SetRightChild(Expression newExpression)
|
|
{
|
|
m_right = newExpression;
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// === Unary Operators ===
|
|
///
|
|
public class UnaryOperator : Expression
|
|
{
|
|
private Expression m_child;
|
|
|
|
public Expression child { get { return m_child; } }
|
|
|
|
public UnaryOperator(ExpressionKind aKind, Expression child, int line, int pos)
|
|
: base(aKind, line, pos)
|
|
{
|
|
m_child = child;
|
|
}
|
|
|
|
public UnaryOperator(UnaryOperator toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_child = toCopy.m_child;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new UnaryOperator(this);
|
|
}
|
|
|
|
public void SetChild(Expression child)
|
|
{
|
|
m_child = child;
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public static Expression CoerceUp(Expression anExpr, UlyssesType target)
|
|
{
|
|
if (target == null)
|
|
throw new ArgumentException();
|
|
|
|
if (anExpr.kind == ExpressionKind.Value
|
|
&& anExpr.type.kind == target.kind)
|
|
{
|
|
// if we are widening the range of a type assigned to a value, then just set the
|
|
// new type and skip constructing a new node.
|
|
anExpr.SetType(target);
|
|
return anExpr;
|
|
}
|
|
else
|
|
{
|
|
UnaryOperator result = new UnaryOperator(ExpressionKind.Cast, anExpr, anExpr.line, anExpr.pos);
|
|
result.SetType(target);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
public static Expression TryCoerceUp(Expression anExpr, UlyssesType target)
|
|
{
|
|
if (!UlyssesType.TypeEqual(anExpr.type, target))
|
|
{
|
|
return CoerceUp(anExpr, target);
|
|
}
|
|
else
|
|
return anExpr;
|
|
}
|
|
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Tuple and Map Access "[...]"
|
|
///
|
|
public sealed class TupleMapAccessExpression : UnaryOperator
|
|
{
|
|
private Expression m_argument;
|
|
|
|
public Expression argument { get { return m_argument; } }
|
|
|
|
public TupleMapAccessExpression(Expression child, Expression argument, int line, int pos)
|
|
: base(ExpressionKind.TupleMapAccess, child, line, pos)
|
|
{
|
|
m_argument = argument;
|
|
}
|
|
|
|
public TupleMapAccessExpression(TupleMapAccessExpression toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_argument = toCopy.m_argument;
|
|
}
|
|
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new TupleMapAccessExpression(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetArgument(Expression newarg)
|
|
{
|
|
if (newarg == null)
|
|
throw new ArgumentException();
|
|
m_argument = newarg;
|
|
}
|
|
}
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Method call "(....)"
|
|
///
|
|
public sealed class CallExpression : UnaryOperator
|
|
{
|
|
private List<Expression> m_arguments;
|
|
private IScope m_CallScope;
|
|
|
|
public List<Expression> arguments { get { return m_arguments; } }
|
|
public IScope scope { get { return m_CallScope; } }
|
|
|
|
public CallExpression(Expression child, List<Expression> arguments, int line, int pos, IScope aScope)
|
|
: base(ExpressionKind.Call, child, line, pos)
|
|
{
|
|
if (arguments != null)
|
|
m_arguments = arguments;
|
|
else
|
|
m_arguments = new List<Expression>();
|
|
m_CallScope = aScope;
|
|
}
|
|
|
|
public CallExpression(CallExpression toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_arguments = new List<Expression>(toCopy.m_arguments);
|
|
m_CallScope = toCopy.m_CallScope;
|
|
}
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new CallExpression(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
|
|
public void SetArguments(List<Expression> newArgs)
|
|
{
|
|
m_arguments = newArgs;
|
|
}
|
|
}
|
|
|
|
|
|
|
|
///////////////////////////////////////////////
|
|
/// Quantifier
|
|
///
|
|
public abstract class Quantifier : UnaryOperator, IScope
|
|
{
|
|
private SymbolTable m_symbols;
|
|
private IScope m_parentScope;
|
|
|
|
public SymbolTable symbols { get { return m_symbols; } }
|
|
|
|
|
|
public Quantifier(ExpressionKind aKind, Expression child, int line, int pos)
|
|
: base(aKind, child, line, pos)
|
|
{
|
|
m_symbols = new SymbolTable();
|
|
}
|
|
|
|
public Quantifier(Quantifier toCopy)
|
|
: base(toCopy)
|
|
{
|
|
m_symbols = new SymbolTable(toCopy.m_symbols);
|
|
m_parentScope = toCopy.m_parentScope;
|
|
}
|
|
|
|
|
|
public Identifier ResolveIdentifier(string aName)
|
|
{
|
|
if (m_symbols.Defined(aName))
|
|
return m_symbols.Get(aName);
|
|
else
|
|
return null;
|
|
}
|
|
|
|
public IScope GetParentScope()
|
|
{
|
|
return m_parentScope;
|
|
}
|
|
|
|
public void SetParentScope(IScope parentScope)
|
|
{
|
|
m_parentScope = parentScope;
|
|
}
|
|
|
|
public void AddIdentifier(Identifier anIdentifier, object tag)
|
|
{
|
|
m_symbols.AddIdentifier(anIdentifier);
|
|
}
|
|
|
|
|
|
}
|
|
|
|
public sealed class ForallQuantifier : Quantifier
|
|
{
|
|
public ForallQuantifier(Expression child, int line, int pos)
|
|
: base(ExpressionKind.forall, child, line, pos)
|
|
{ }
|
|
|
|
public ForallQuantifier(ForallQuantifier toCopy)
|
|
: base(toCopy) { }
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new ForallQuantifier(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
}
|
|
|
|
public sealed class ExistsQuantifier : Quantifier
|
|
{
|
|
public ExistsQuantifier(Expression child, int line, int pos)
|
|
: base(ExpressionKind.exists, child, line, pos)
|
|
{ }
|
|
public ExistsQuantifier(ExistsQuantifier toCopy)
|
|
: base(toCopy) { }
|
|
|
|
public override Expression Clone()
|
|
{
|
|
return new ExistsQuantifier(this);
|
|
}
|
|
|
|
public override void Accept(IAstVisitor visitor)
|
|
{
|
|
visitor.visit(this);
|
|
}
|
|
}
|
|
|
|
|
|
}
|