From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/AIFramework/Expr.cs | 1280 ++++++++++++++++++++++---------------------- 1 file changed, 640 insertions(+), 640 deletions(-) (limited to 'Source/AIFramework/Expr.cs') diff --git a/Source/AIFramework/Expr.cs b/Source/AIFramework/Expr.cs index 58473592..ae2bd4b7 100644 --- a/Source/AIFramework/Expr.cs +++ b/Source/AIFramework/Expr.cs @@ -1,640 +1,640 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -// This file specifies the expression language used by the Abstract -// Interpretation Framework. -// -// expressions e ::= x variables -// | f(e1,...,en) uninterpreted functions -// | \x:t.e lambda expressions -// -// types t ::= b user-defined/built-in base types -// | t1 * ... * tn -> t' function type - -namespace Microsoft.AbstractInterpretationFramework -{ - using System.Collections; - using System; - using System.Diagnostics.Contracts; - - //----------------------------- Expressions ----------------------------- - - /// - /// An interface for expressions. This expression language is specified - /// by interfaces to allow the client to be able to use their existing - /// AST nodes as AIF expressions. - /// - /// This only serves as a place for operations on expressions. Clients - /// should implement directly IVariable, IFunApp, ... - /// - [ContractClass(typeof(IExprContracts))] - public interface IExpr - { - /// - /// Execute a visit over the expression. - /// - /// The expression visitor. - /// The result of the visit. - [Pure] object DoVisit(ExprVisitor/*!*/ visitor); - - // TODO: Type checking of the expressions. - } - [ContractClassFor(typeof(IExpr))] - public abstract class IExprContracts:IExpr{ - #region IExpr Members - -public object DoVisit(ExprVisitor visitor) -{ - Contract.Requires(visitor != null); - throw new System.NotImplementedException(); -} - -#endregion -} - - /// - /// An interface for variables. - /// - /// This interface should be implemented by the client. - /// - [ContractClass(typeof(IVariableContracts))] - public interface IVariable : IExpr - { - string/*!*/ Name { get; } // Each client must define the name for variables - } - [ContractClassFor(typeof(IVariable))] - public abstract class IVariableContracts:IVariable{ - string IVariable.Name{get{Contract.Ensures(Contract.Result() != null);throw new NotImplementedException();} - - } - - #region IExpr Members - - object IExpr.DoVisit(ExprVisitor visitor) { - throw new NotImplementedException(); - } - - #endregion - } - - /// - /// An interface for function applications. - /// - /// This interface should be implemented by the client. - /// - /// - [ContractClass(typeof(IFunAppContracts))] - public interface IFunApp : IExpr - { - IFunctionSymbol/*!*/ FunctionSymbol { get; } - IList/**//*!*/ Arguments - { - [Pure][Rep] get; - - } - - /// - /// Provides a method to create a new uninterpreted function - /// with the same function symbol but with the arguments with - /// args. - /// - /// The new arguments. - /// A copy of the function with the new arguments. - IFunApp/*!*/ CloneWithArguments(IList/**//*!*/ args) - //TODO Contract.Requires(this.Arguments.Count == args.Count); - ; - } - [ContractClassFor(typeof(IFunApp))] -public abstract class IFunAppContracts:IFunApp{ - -#region IFunApp Members - -public IFunctionSymbol FunctionSymbol -{ - get {Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); } -} - -public IList Arguments -{ - get {Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().IsReadOnly); - throw new System.NotImplementedException(); } -} - -public IFunApp CloneWithArguments(IList args) -{ - Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - - - throw new System.NotImplementedException(); -} - -#endregion - -#region IExpr Members - -object IExpr.DoVisit(ExprVisitor visitor) { - throw new NotImplementedException(); -} - -#endregion -} - - /// - /// An interface for anonymous functions (i.e., lambda expressions) - /// - [ContractClass(typeof(IFunctionContracts))] - public interface IFunction : IExpr - { - IVariable/*!*/ Param { get; } - AIType/*!*/ ParamType { get; } - IExpr/*!*/ Body { get; } - - IFunction/*!*/ CloneWithBody(IExpr/*!*/ body); - } - [ContractClassFor(typeof(IFunction))] - public abstract class IFunctionContracts:IFunction{ - - #region IFunction Members - - IVariable IFunction.Param { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - AIType IFunction.ParamType { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - IExpr IFunction.Body { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - IFunction IFunction.CloneWithBody(IExpr body) { - Contract.Requires(body != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - - #endregion - - #region IExpr Members - - object IExpr.DoVisit(ExprVisitor visitor) { - throw new NotImplementedException(); - } - - #endregion - } - - /// - /// An interface representing an expression that at any moment could, in principle, evaluate - /// to a different value. That is, the abstract interpreter should treat these IExpr's - /// as unknown values. They are used when there is no other IExpr corresponding to the - /// expression to be modeled. - /// - public interface IUnknown : IExpr {} - - /// - /// An abstract class that provides an interface for expression visitors. - /// - [ContractClass(typeof(ExprVisitorContracts))] - public abstract class ExprVisitor - { - public abstract object Default(IExpr/*!*/ expr); - - public virtual object VisitVariable(IVariable/*!*/ var){ -Contract.Requires(var != null); - return Default(var); - } - - public virtual object VisitFunApp(IFunApp/*!*/ funapp){ -Contract.Requires(funapp != null); - return Default(funapp); - } - - public virtual object VisitFunction(IFunction/*!*/ fun){ -Contract.Requires(fun != null); - return Default(fun); - } - } - [ContractClassFor(typeof(ExprVisitor))] - public abstract class ExprVisitorContracts:ExprVisitor{ - public override object Default(IExpr expr) -{ - Contract.Requires(expr != null); throw new NotImplementedException(); -}} - - /// - /// A utility class for dealing with expressions. - /// - public sealed class ExprUtil - { - /// - /// Yield an expression that is 'inexpr' with 'var' replaced by 'subst'. - /// - /// The expression to substitute. - /// The variable to substitute for. - /// The expression to substitute into. - public static IExpr/*!*/ Substitute(IExpr/*!*/ subst, IVariable/*!*/ var, IExpr/*!*/ inexpr){ -Contract.Requires(inexpr != null); -Contract.Requires(var != null); -Contract.Requires(subst != null); -Contract.Ensures(Contract.Result() != null); - IExpr result = null; - - if (inexpr is IVariable) - { - result = inexpr.Equals(var) ? subst : inexpr; - } - else if (inexpr is IFunApp) - { - IFunApp/*!*/ funapp = (IFunApp/*!*/)cce.NonNull(inexpr); - IList newargs = null; - - var x = new System.Collections.Generic.List(); - foreach (IExpr arg in funapp.Arguments){ - x.Add(Substitute(subst,var, arg)); - } - newargs = new ArrayList(x); - //newargs = new ArrayList{ IExpr/*!*/ arg in funapp.Arguments; Substitute(subst, var, arg) }; - result = funapp.CloneWithArguments(newargs); - } - else if (inexpr is IFunction) - { - IFunction/*!*/ fun = (IFunction/*!*/)cce.NonNull(inexpr); - - if (fun.Param.Equals(var)) - result = fun; - else - result = fun.CloneWithBody(Substitute(subst, var, fun.Body)); - } - else if (inexpr is IUnknown) - { - result = inexpr; - } - else - { - {Contract.Assert(false);throw new cce.UnreachableException();} - } - - return result; - } - - - // - // Poor man's pattern matching. - // - // The methods below implement pattern matching for AI expressions. - // - // Example Usage: - // Match(e, Prop.Imp, - // (Matcher)delegate (IExpr e) { return Match(e, Prop.And, out x, out y); } - // out z) - // which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees. - // - public delegate bool Matcher(IExpr/*!*/ expr); - - private static IFunApp/*?*/ MatchFunctionSymbol(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f){ -Contract.Requires(f != null); -Contract.Requires(expr != null); - IFunApp app = expr as IFunApp; - if (app != null) - { - if (app.FunctionSymbol.Equals(f)) - return app; - else - return null; - } - else - return null; - } - - public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, params Matcher[]/*!*/ subs){ -Contract.Requires(subs != null); -Contract.Requires(f != null); -Contract.Requires(expr != null); - IFunApp app = MatchFunctionSymbol(expr,f); - if (app != null) - { - int i = 0; // Note ***0*** - foreach(Matcher/*!*/ s in subs){ -Contract.Assert(s != null); - if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; } - i++; - } - return true; - } - else { return false; } - } - - // Unary Binding - public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, params Matcher[]/*!*/ subs){ -Contract.Requires(subs != null); -Contract.Requires(f != null); -Contract.Requires(expr != null); - arg0 = null; - - IFunApp app = MatchFunctionSymbol(expr,f); - if (app != null) - { - arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); - - int i = 1; // Note ***1*** - foreach(Matcher/*!*/ s in subs){ -Contract.Assert(s != null); - if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } - i++; - } - return true; - } - else { return false; } - } - - // Binary Binding - public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, Matcher/*!*/ sub0, out IExpr arg1, params Matcher[]/*!*/ subs){ -Contract.Requires(subs != null); -Contract.Requires(sub0 != null); -Contract.Requires(f != null); -Contract.Requires(expr != null); - arg1 = null; - - IFunApp app = MatchFunctionSymbol(expr,f); - if (app != null) - { - if (!sub0(cce.NonNull((IExpr/*!*/)app.Arguments[0]))) { return false; } - - arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); - - int i = 2; // Note ***2*** - foreach(Matcher/*!*/ s in subs){ -Contract.Assert(s != null); - if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; } - i++; - } - return true; - } - else { return false; } - } - - public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, params Matcher[]/*!*/ subs){ -Contract.Requires(subs != null); -Contract.Requires(f != null); -Contract.Requires(expr != null); - arg0 = null; - arg1 = null; - - IFunApp app = MatchFunctionSymbol(expr,f); - if (app != null) - { - arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); - arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); - - int i = 2; // Note ***2*** - foreach(Matcher/*!*/ s in subs){ -Contract.Assert(s != null); - if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } - i++; - } - return true; - } - else { return false; } - } - - // Ternary Binding - public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]/*!*/ subs){ -Contract.Requires(subs != null); -Contract.Requires(f != null); -Contract.Requires(expr != null); - arg0 = null; - arg1 = null; - arg2 = null; - - IFunApp app = MatchFunctionSymbol(expr,f); - if (app != null) - { - arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); - arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); - arg2 = (IExpr/*!*/)cce.NonNull(app.Arguments[2]); - - int i = 3; // Note ***3*** - foreach(Matcher/*!*/ s in subs){ -Contract.Assert(s != null); - if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } - i++; - } - return true; - } - else { return false; } - } - - /// - /// Not intended to be instantiated. - /// - private ExprUtil() { } - } - - //------------------------------ Symbols -------------------------------- - - /// - /// An interface for function symbols. Constants are represented by - /// 0-ary function symbols. - /// - /// This interface should be implemented by abstract domains, but client - /// expressions need keep track of function symbols. - /// - [ContractClass(typeof(IFunctionSymbolContracts))] - public interface IFunctionSymbol - { - AIType/*!*/ AIType { [Rep][ResultNotNewlyAllocated] - get; } - } - [ContractClassFor(typeof(IFunctionSymbol))] - public abstract class IFunctionSymbolContracts:IFunctionSymbol{ - #region IFunctionSymbol Members - - AIType IFunctionSymbol.AIType { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - #endregion - } - - /// - /// The type of the arguments to ExprUtil.Match, a poor man's pattern - /// matching. - /// - public interface IMatchable - { - } - - //-------------------------------- Types -------------------------------- - - /// - /// Types. - /// - public interface AIType - { - } - - /// - /// Function type constructor. - /// - public sealed class FunctionType : AIType - { - /*[Own]*/ private readonly IList/**//*!*/ argTypes; - /*[Own]*/ private readonly AIType/*!*/ retType; - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(argTypes != null); - Contract.Invariant(retType != null); -} - - - public FunctionType(params AIType[]/*!*/ types){ -Contract.Requires(types != null); - Contract.Requires(types.Length >= 2); - AIType type = types[types.Length-1]; - Contract.Assume(type != null); - this.retType = type; - ArrayList argTypes = new ArrayList(); - for (int i = 0; i < types.Length-1; i++) - { - type = types[i]; - Contract.Assume(type != null); - argTypes.Add(types); - } - this.argTypes = ArrayList.ReadOnly(argTypes); - } - - public IList/**//*!*/ Arguments - { - [Pure][Rep] - get - { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().IsReadOnly); - return argTypes; - } - } - - public int Arity - { - get { return argTypes.Count; } - } - - public AIType/*!*/ ReturnType - { - get {Contract.Ensures(Contract.Result() != null); return retType; } - } - - /* TODO Do we have the invariant that two functions are equal iff they're the same object. - public override bool Equals(object o) - { - if (o != null && o is FunctionType) - { - FunctionType other = (FunctionType) o; - - if (Arity == other.Arity - && ReturnType.Equals(other.ReturnType)) - { - for (int i = 0; i < Arity; i++) - { - if (!argTypes[i].Equals(other.argTypes[i])) - return false; - } - return true; - } - else - return false; - } - else - return false; - } - */ - } - - //------------------------------ Queries ------------------------------- - - public enum Answer { Yes, No, Maybe }; - - /// - /// An interface that specifies a queryable object that can answer - /// whether a predicate holds. - /// - /// - [ContractClass(typeof(IQueryableContracts))] - public interface IQueryable - { - /// - /// Answers the query whether the given predicate holds. - /// - /// The given predicate. - /// Yes, No, or Maybe. - Answer CheckPredicate(IExpr/*!*/ pred); - - /// - /// A simplified interface for disequalities. One can always - /// implement this by calling CheckPredicate, but it may be - /// more efficient with this method. - /// - Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2); - } - [ContractClassFor(typeof(IQueryable))] - public abstract class IQueryableContracts : IQueryable { - #region IQueryable Members - - public Answer CheckPredicate(IExpr pred) { - Contract.Requires(pred != null); - throw new NotImplementedException(); - } - - public Answer CheckVariableDisequality(IVariable var1, IVariable var2) { - Contract.Requires(var1 != null); - Contract.Requires(var2 != null); - throw new NotImplementedException(); - } - - #endregion - } - - public static class QueryUtil - { - public static Answer Negate(Answer ans) - { - switch (ans) - { - case Answer.Yes: - return Answer.No; - case Answer.No: - return Answer.Yes; - default: - return Answer.Maybe; - } - } - } - - //----------------------------- Exceptions ----------------------------- - - public class CheckedException : System.Exception { - } - public class TypeError : CheckedException - { - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +// This file specifies the expression language used by the Abstract +// Interpretation Framework. +// +// expressions e ::= x variables +// | f(e1,...,en) uninterpreted functions +// | \x:t.e lambda expressions +// +// types t ::= b user-defined/built-in base types +// | t1 * ... * tn -> t' function type + +namespace Microsoft.AbstractInterpretationFramework +{ + using System.Collections; + using System; + using System.Diagnostics.Contracts; + + //----------------------------- Expressions ----------------------------- + + /// + /// An interface for expressions. This expression language is specified + /// by interfaces to allow the client to be able to use their existing + /// AST nodes as AIF expressions. + /// + /// This only serves as a place for operations on expressions. Clients + /// should implement directly IVariable, IFunApp, ... + /// + [ContractClass(typeof(IExprContracts))] + public interface IExpr + { + /// + /// Execute a visit over the expression. + /// + /// The expression visitor. + /// The result of the visit. + [Pure] object DoVisit(ExprVisitor/*!*/ visitor); + + // TODO: Type checking of the expressions. + } + [ContractClassFor(typeof(IExpr))] + public abstract class IExprContracts:IExpr{ + #region IExpr Members + +public object DoVisit(ExprVisitor visitor) +{ + Contract.Requires(visitor != null); + throw new System.NotImplementedException(); +} + +#endregion +} + + /// + /// An interface for variables. + /// + /// This interface should be implemented by the client. + /// + [ContractClass(typeof(IVariableContracts))] + public interface IVariable : IExpr + { + string/*!*/ Name { get; } // Each client must define the name for variables + } + [ContractClassFor(typeof(IVariable))] + public abstract class IVariableContracts:IVariable{ + string IVariable.Name{get{Contract.Ensures(Contract.Result() != null);throw new NotImplementedException();} + + } + + #region IExpr Members + + object IExpr.DoVisit(ExprVisitor visitor) { + throw new NotImplementedException(); + } + + #endregion + } + + /// + /// An interface for function applications. + /// + /// This interface should be implemented by the client. + /// + /// + [ContractClass(typeof(IFunAppContracts))] + public interface IFunApp : IExpr + { + IFunctionSymbol/*!*/ FunctionSymbol { get; } + IList/**//*!*/ Arguments + { + [Pure][Rep] get; + + } + + /// + /// Provides a method to create a new uninterpreted function + /// with the same function symbol but with the arguments with + /// args. + /// + /// The new arguments. + /// A copy of the function with the new arguments. + IFunApp/*!*/ CloneWithArguments(IList/**//*!*/ args) + //TODO Contract.Requires(this.Arguments.Count == args.Count); + ; + } + [ContractClassFor(typeof(IFunApp))] +public abstract class IFunAppContracts:IFunApp{ + +#region IFunApp Members + +public IFunctionSymbol FunctionSymbol +{ + get {Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); } +} + +public IList Arguments +{ + get {Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().IsReadOnly); + throw new System.NotImplementedException(); } +} + +public IFunApp CloneWithArguments(IList args) +{ + Contract.Requires(args != null); + Contract.Ensures(Contract.Result() != null); + + + throw new System.NotImplementedException(); +} + +#endregion + +#region IExpr Members + +object IExpr.DoVisit(ExprVisitor visitor) { + throw new NotImplementedException(); +} + +#endregion +} + + /// + /// An interface for anonymous functions (i.e., lambda expressions) + /// + [ContractClass(typeof(IFunctionContracts))] + public interface IFunction : IExpr + { + IVariable/*!*/ Param { get; } + AIType/*!*/ ParamType { get; } + IExpr/*!*/ Body { get; } + + IFunction/*!*/ CloneWithBody(IExpr/*!*/ body); + } + [ContractClassFor(typeof(IFunction))] + public abstract class IFunctionContracts:IFunction{ + + #region IFunction Members + + IVariable IFunction.Param { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + AIType IFunction.ParamType { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + IExpr IFunction.Body { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + IFunction IFunction.CloneWithBody(IExpr body) { + Contract.Requires(body != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + + #endregion + + #region IExpr Members + + object IExpr.DoVisit(ExprVisitor visitor) { + throw new NotImplementedException(); + } + + #endregion + } + + /// + /// An interface representing an expression that at any moment could, in principle, evaluate + /// to a different value. That is, the abstract interpreter should treat these IExpr's + /// as unknown values. They are used when there is no other IExpr corresponding to the + /// expression to be modeled. + /// + public interface IUnknown : IExpr {} + + /// + /// An abstract class that provides an interface for expression visitors. + /// + [ContractClass(typeof(ExprVisitorContracts))] + public abstract class ExprVisitor + { + public abstract object Default(IExpr/*!*/ expr); + + public virtual object VisitVariable(IVariable/*!*/ var){ +Contract.Requires(var != null); + return Default(var); + } + + public virtual object VisitFunApp(IFunApp/*!*/ funapp){ +Contract.Requires(funapp != null); + return Default(funapp); + } + + public virtual object VisitFunction(IFunction/*!*/ fun){ +Contract.Requires(fun != null); + return Default(fun); + } + } + [ContractClassFor(typeof(ExprVisitor))] + public abstract class ExprVisitorContracts:ExprVisitor{ + public override object Default(IExpr expr) +{ + Contract.Requires(expr != null); throw new NotImplementedException(); +}} + + /// + /// A utility class for dealing with expressions. + /// + public sealed class ExprUtil + { + /// + /// Yield an expression that is 'inexpr' with 'var' replaced by 'subst'. + /// + /// The expression to substitute. + /// The variable to substitute for. + /// The expression to substitute into. + public static IExpr/*!*/ Substitute(IExpr/*!*/ subst, IVariable/*!*/ var, IExpr/*!*/ inexpr){ +Contract.Requires(inexpr != null); +Contract.Requires(var != null); +Contract.Requires(subst != null); +Contract.Ensures(Contract.Result() != null); + IExpr result = null; + + if (inexpr is IVariable) + { + result = inexpr.Equals(var) ? subst : inexpr; + } + else if (inexpr is IFunApp) + { + IFunApp/*!*/ funapp = (IFunApp/*!*/)cce.NonNull(inexpr); + IList newargs = null; + + var x = new System.Collections.Generic.List(); + foreach (IExpr arg in funapp.Arguments){ + x.Add(Substitute(subst,var, arg)); + } + newargs = new ArrayList(x); + //newargs = new ArrayList{ IExpr/*!*/ arg in funapp.Arguments; Substitute(subst, var, arg) }; + result = funapp.CloneWithArguments(newargs); + } + else if (inexpr is IFunction) + { + IFunction/*!*/ fun = (IFunction/*!*/)cce.NonNull(inexpr); + + if (fun.Param.Equals(var)) + result = fun; + else + result = fun.CloneWithBody(Substitute(subst, var, fun.Body)); + } + else if (inexpr is IUnknown) + { + result = inexpr; + } + else + { + {Contract.Assert(false);throw new cce.UnreachableException();} + } + + return result; + } + + + // + // Poor man's pattern matching. + // + // The methods below implement pattern matching for AI expressions. + // + // Example Usage: + // Match(e, Prop.Imp, + // (Matcher)delegate (IExpr e) { return Match(e, Prop.And, out x, out y); } + // out z) + // which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees. + // + public delegate bool Matcher(IExpr/*!*/ expr); + + private static IFunApp/*?*/ MatchFunctionSymbol(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f){ +Contract.Requires(f != null); +Contract.Requires(expr != null); + IFunApp app = expr as IFunApp; + if (app != null) + { + if (app.FunctionSymbol.Equals(f)) + return app; + else + return null; + } + else + return null; + } + + public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, params Matcher[]/*!*/ subs){ +Contract.Requires(subs != null); +Contract.Requires(f != null); +Contract.Requires(expr != null); + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + int i = 0; // Note ***0*** + foreach(Matcher/*!*/ s in subs){ +Contract.Assert(s != null); + if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Unary Binding + public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, params Matcher[]/*!*/ subs){ +Contract.Requires(subs != null); +Contract.Requires(f != null); +Contract.Requires(expr != null); + arg0 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); + + int i = 1; // Note ***1*** + foreach(Matcher/*!*/ s in subs){ +Contract.Assert(s != null); + if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Binary Binding + public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, Matcher/*!*/ sub0, out IExpr arg1, params Matcher[]/*!*/ subs){ +Contract.Requires(subs != null); +Contract.Requires(sub0 != null); +Contract.Requires(f != null); +Contract.Requires(expr != null); + arg1 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + if (!sub0(cce.NonNull((IExpr/*!*/)app.Arguments[0]))) { return false; } + + arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); + + int i = 2; // Note ***2*** + foreach(Matcher/*!*/ s in subs){ +Contract.Assert(s != null); + if (!s(cce.NonNull((IExpr)app.Arguments[i]))) { return false; } + i++; + } + return true; + } + else { return false; } + } + + public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, params Matcher[]/*!*/ subs){ +Contract.Requires(subs != null); +Contract.Requires(f != null); +Contract.Requires(expr != null); + arg0 = null; + arg1 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); + arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); + + int i = 2; // Note ***2*** + foreach(Matcher/*!*/ s in subs){ +Contract.Assert(s != null); + if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Ternary Binding + public static bool Match(IExpr/*!*/ expr, IFunctionSymbol/*!*/ f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]/*!*/ subs){ +Contract.Requires(subs != null); +Contract.Requires(f != null); +Contract.Requires(expr != null); + arg0 = null; + arg1 = null; + arg2 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]); + arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]); + arg2 = (IExpr/*!*/)cce.NonNull(app.Arguments[2]); + + int i = 3; // Note ***3*** + foreach(Matcher/*!*/ s in subs){ +Contract.Assert(s != null); + if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; } + i++; + } + return true; + } + else { return false; } + } + + /// + /// Not intended to be instantiated. + /// + private ExprUtil() { } + } + + //------------------------------ Symbols -------------------------------- + + /// + /// An interface for function symbols. Constants are represented by + /// 0-ary function symbols. + /// + /// This interface should be implemented by abstract domains, but client + /// expressions need keep track of function symbols. + /// + [ContractClass(typeof(IFunctionSymbolContracts))] + public interface IFunctionSymbol + { + AIType/*!*/ AIType { [Rep][ResultNotNewlyAllocated] + get; } + } + [ContractClassFor(typeof(IFunctionSymbol))] + public abstract class IFunctionSymbolContracts:IFunctionSymbol{ + #region IFunctionSymbol Members + + AIType IFunctionSymbol.AIType { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + #endregion + } + + /// + /// The type of the arguments to ExprUtil.Match, a poor man's pattern + /// matching. + /// + public interface IMatchable + { + } + + //-------------------------------- Types -------------------------------- + + /// + /// Types. + /// + public interface AIType + { + } + + /// + /// Function type constructor. + /// + public sealed class FunctionType : AIType + { + /*[Own]*/ private readonly IList/**//*!*/ argTypes; + /*[Own]*/ private readonly AIType/*!*/ retType; + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(argTypes != null); + Contract.Invariant(retType != null); +} + + + public FunctionType(params AIType[]/*!*/ types){ +Contract.Requires(types != null); + Contract.Requires(types.Length >= 2); + AIType type = types[types.Length-1]; + Contract.Assume(type != null); + this.retType = type; + ArrayList argTypes = new ArrayList(); + for (int i = 0; i < types.Length-1; i++) + { + type = types[i]; + Contract.Assume(type != null); + argTypes.Add(types); + } + this.argTypes = ArrayList.ReadOnly(argTypes); + } + + public IList/**//*!*/ Arguments + { + [Pure][Rep] + get + { + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().IsReadOnly); + return argTypes; + } + } + + public int Arity + { + get { return argTypes.Count; } + } + + public AIType/*!*/ ReturnType + { + get {Contract.Ensures(Contract.Result() != null); return retType; } + } + + /* TODO Do we have the invariant that two functions are equal iff they're the same object. + public override bool Equals(object o) + { + if (o != null && o is FunctionType) + { + FunctionType other = (FunctionType) o; + + if (Arity == other.Arity + && ReturnType.Equals(other.ReturnType)) + { + for (int i = 0; i < Arity; i++) + { + if (!argTypes[i].Equals(other.argTypes[i])) + return false; + } + return true; + } + else + return false; + } + else + return false; + } + */ + } + + //------------------------------ Queries ------------------------------- + + public enum Answer { Yes, No, Maybe }; + + /// + /// An interface that specifies a queryable object that can answer + /// whether a predicate holds. + /// + /// + [ContractClass(typeof(IQueryableContracts))] + public interface IQueryable + { + /// + /// Answers the query whether the given predicate holds. + /// + /// The given predicate. + /// Yes, No, or Maybe. + Answer CheckPredicate(IExpr/*!*/ pred); + + /// + /// A simplified interface for disequalities. One can always + /// implement this by calling CheckPredicate, but it may be + /// more efficient with this method. + /// + Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2); + } + [ContractClassFor(typeof(IQueryable))] + public abstract class IQueryableContracts : IQueryable { + #region IQueryable Members + + public Answer CheckPredicate(IExpr pred) { + Contract.Requires(pred != null); + throw new NotImplementedException(); + } + + public Answer CheckVariableDisequality(IVariable var1, IVariable var2) { + Contract.Requires(var1 != null); + Contract.Requires(var2 != null); + throw new NotImplementedException(); + } + + #endregion + } + + public static class QueryUtil + { + public static Answer Negate(Answer ans) + { + switch (ans) + { + case Answer.Yes: + return Answer.No; + case Answer.No: + return Answer.Yes; + default: + return Answer.Maybe; + } + } + } + + //----------------------------- Exceptions ----------------------------- + + public class CheckedException : System.Exception { + } + public class TypeError : CheckedException + { + } +} -- cgit v1.2.3