Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions; they might not yet fully work for polymorphic maps.

1 files changed, 0 insertions, 689 deletions

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index ebc594f3..baf12310 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -2209,695 +2209,6 @@ namespace Microsoft.Boogie
     }

   }

 

-  public abstract class QuantifierExpr : Expr

-  {

-    public TypeVariableSeq! TypeParameters;

-    public VariableSeq! Dummies;

-    public QKeyValue Attributes;

-    public Trigger Triggers;

-    public Expr! Body;

-

-    static int SkolemIds = 0;

-    public readonly int SkolemId;

-    

-    public QuantifierExpr(IToken! tok, TypeVariableSeq! typeParameters,

-                          VariableSeq! dummies, QKeyValue kv, Trigger triggers, Expr! body)

-      requires dummies.Length + typeParameters.Length > 0;

-    {

-      base(tok);

-

-      assert (this is ForallExpr) || (this is ExistsExpr);

- 

-      TypeParameters = typeParameters;

-      Dummies = dummies;

-      Attributes = kv;

-      Triggers = triggers;

-      Body = body;

-

-      SkolemId = SkolemIds++;

-    }

-

-    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj)

-    {

-      if (obj == null) return false;

-      if (!(obj is QuantifierExpr) ||

-          (obj is ForallExpr) != (this is ForallExpr)) return false;

-

-      QuantifierExpr other = (QuantifierExpr)obj;

-      // Note, we consider quantifiers equal modulo the Triggers.

-      return object.Equals(this.TypeParameters, other.TypeParameters)

-             && object.Equals(this.Dummies, other.Dummies)

-             && object.Equals(this.Body, other.Body);

-    }

-

-    [Pure] 

-    public override int GetHashCode()

-    {

-      int h = this.Dummies.GetHashCode();

-      // Note, we consider quantifiers equal modulo the Triggers.

-      h ^= this.Body.GetHashCode();

-      h = h*5 + this.TypeParameters.GetHashCode();

-      if (this is ForallExpr) h = h * 3;

-      return h;

-    }

-

-    public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext) 

-    {

-      stream.Write(this, "({0}", this is ForallExpr ? "forall" : "exists");

-      Type.EmitOptionalTypeParams(stream, TypeParameters);

-      stream.Write(this, " ");

-      this.Dummies.Emit(stream);

-      stream.Write(" :: ");

-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

-        kv.Emit(stream);

-        stream.Write(" ");

-      }

-      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {

-        tr.Emit(stream);

-        stream.Write(" ");

-      }

-      

-      this.Body.Emit(stream);

-      stream.Write(")");

-    }

-    // if the user says ( forall x :: forall y :: { f(x,y) } ... ) we transform it to

-    // (forall x, y :: { f(x,y) } ... ) otherwise the prover ignores the trigger

-    private void MergeAdjecentQuantifier()

-    {

-      QuantifierExpr qbody = Body as QuantifierExpr;

-      if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {

-        return;

-      }

-      qbody.MergeAdjecentQuantifier();

-      if (qbody.Triggers == null) {

-        return;

-      }

-      Body = qbody.Body;

-      TypeParameters.AddRange(qbody.TypeParameters);

-      Dummies.AddRange(qbody.Dummies);

-      Triggers = qbody.Triggers;

-      if (qbody.Attributes != null) {

-        if (Attributes == null) {

-          Attributes = qbody.Attributes;

-        } else {

-          QKeyValue p = Attributes;

-          while (p.Next != null) {

-            p = p.Next;

-          }

-          p.Next = qbody.Attributes;

-        }

-      }

-    }

-    public override void Resolve(ResolutionContext! rc) 

-    {

-      int oldErrorCount = rc.ErrorCount;

-      

-      this.MergeAdjecentQuantifier();

-      if (rc.TriggerMode) {

-        rc.Error(this, "quantifiers are not allowed in triggers");

-      }

-

-      int previousTypeBinderState = rc.TypeBinderState;

-      try {

-        foreach (TypeVariable! v in TypeParameters)

-          rc.AddTypeBinder(v);

-

-        rc.PushVarContext();

-        foreach (Variable! v in Dummies) 

-        {

-          v.Register(rc);

-          v.Resolve(rc);

-        }

-        for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

-          kv.Resolve(rc);

-        }

-        for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {

-          int prevErrorCount = rc.ErrorCount;

-          tr.Resolve(rc);

-          if (prevErrorCount == rc.ErrorCount) {

-            // for positive triggers, make sure all bound variables are mentioned

-            if (tr.Pos) {

-              Set /*Variable*/ freeVars = new Set /*Variable*/ ();

-              tr.ComputeFreeVariables(freeVars);

-              foreach (Variable! v in Dummies) {

-                if (!freeVars[v]) {

-                  rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);

-                }

-              }

-            }

-          }

-        }

-        Body.Resolve(rc);

-        rc.PopVarContext();

-      

-        // establish a canonical order of the type parameters

-        this.TypeParameters = Type.SortTypeParams(TypeParameters, Dummies.ToTypeSeq, null);

-

-      } finally {

-        rc.TypeBinderState = previousTypeBinderState;

-      }

-

-      if (oldErrorCount == rc.ErrorCount) {

-        this.ApplyNeverTriggers();

-      }

-    }

-

-    #region never triggers

-    private class NeverTriggerCollector : StandardVisitor

-    {

-      QuantifierExpr! parent;

-      public NeverTriggerCollector(QuantifierExpr! p)

-      {

-        parent = p;

-      }

-

-      public override Expr! VisitNAryExpr(NAryExpr! node)

-      {

-        FunctionCall fn = node.Fun as FunctionCall;

-        if (fn != null && ((!)fn.Func).NeverTrigger) {

-          parent.Triggers = new Trigger(fn.Func.tok, false, new ExprSeq(node), parent.Triggers);

-        }

-        return base.VisitNAryExpr(node);

-      }

-    }

-

-    private bool neverTriggerApplied;

-    private void ApplyNeverTriggers()

-    {

-      if (neverTriggerApplied) {

-        return;

-      }

-      neverTriggerApplied = true;

-

-      for (Trigger t = Triggers; t != null; t = t.Next) {

-        if (t.Pos) { return; }

-      }

-

-      NeverTriggerCollector visitor = new NeverTriggerCollector(this);

-      visitor.VisitExpr(Body);

-    }

-    #endregion

-

-    public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {

-      foreach (Variable! v in Dummies) {

-        assert !freeVars[v];

-      }

-      Body.ComputeFreeVariables(freeVars);

-      foreach (Variable! v in Dummies) {

-        foreach (TypeVariable! w in v.TypedIdent.Type.FreeVariables)

-          freeVars.Add(w);

-      }

-      foreach (Variable! v in Dummies) {

-        freeVars.Remove(v);

-      }

-      foreach (TypeVariable! v in TypeParameters) {

-        freeVars.Remove(v);

-      }

-    }

-    public override void Typecheck(TypecheckingContext! tc) 

-    {

-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

-        kv.Typecheck(tc);

-      }

-      for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {

-        tr.Typecheck(tc);

-      }

-      Body.Typecheck(tc);

-      assert Body.Type != null;  // follows from postcondition of Expr.Typecheck

-      if (!Body.Type.Unify(Type.Bool)) 

-      {

-        tc.Error(this, "quantifier body must be of type bool");

-      }

-      this.Type = Type.Bool;

-

-      // Check that type parameters occur in the types of the

-      // dummies, or otherwise in the triggers. This can only be

-      // done after typechecking

-      TypeVariableSeq! dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);

-      TypeVariableSeq! unmentionedParameters = new TypeVariableSeq ();

-      foreach (TypeVariable! var in TypeParameters)

-        if (!dummyParameters.Has(var))

-          unmentionedParameters.Add(var);

-

-      if (unmentionedParameters.Length > 0) {

-        // all the type parameters that do not occur in dummy types

-        // have to occur in triggers

-

-        for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {

-          // for positive triggers, make sure all bound variables are mentioned

-          if (tr.Pos) {

-            Set /*Variable*/ freeVars = new Set /*Variable*/ ();

-            tr.ComputeFreeVariables(freeVars);

-            foreach (TypeVariable! v in unmentionedParameters) {

-              if (!freeVars[v])

-                tc.Error(tr,

-                         "trigger does not mention {0}, which does not " +

-                         "occur in variables types either",

-                         v);

-            }

-          }

-        }

-      }

-    }

-    public override Type! ShallowType {

-      get {

-        return Type.Bool;

-      }

-    }

-    

-    public abstract AI.IFunctionSymbol! FunctionSymbol { get; }

-    

-    internal sealed class AIQuantifier : AI.IFunApp

-    {

-      internal readonly AIFunctionRep! arg;

-      internal AIQuantifier(QuantifierExpr! realQuantifier, int dummyIndex)

-      : this(new AIFunctionRep(realQuantifier, dummyIndex))

-      {

-      }

-      [Pure][Reads(ReadsAttribute.Reads.Nothing)]

-      public override bool Equals(object obj)

-      {

-        if (obj == null) return false;

-        if (!(obj is AIQuantifier)) return false;

-    

-        AIQuantifier other = (AIQuantifier)obj;

-        return object.Equals(this.arg, other.arg);

-      }

-      [Pure] 

-      public override int GetHashCode()

-      {

-        return this.arg.GetHashCode();

-      }

-      

-      private AIQuantifier(AIFunctionRep! arg)

-      {

-        this.arg = arg;

-        // base();

-      }

-      

-      [Pure]

-      public object DoVisit(AI.ExprVisitor! visitor)

-      {

-        return visitor.VisitFunApp(this);

-      }

-      

-      public AI.IFunctionSymbol! FunctionSymbol { get { return arg.RealQuantifier.FunctionSymbol; } }

-      

-      private IList/*?*/ argCache = null;

-      public IList/*<IExpr!>*/! Arguments

-      {

-        get

-        {

-          if (argCache == null)

-          {

-            IList a = new ArrayList(1);

-            a.Add(arg);

-            argCache = ArrayList.ReadOnly(a);

-          }

-          return argCache;

-        }

-      }

-      

-      public AI.IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)

-      {

-        assume args.Count == 1;

-        

-        AIFunctionRep rep = args[0] as AIFunctionRep;

-        if (rep != null)

-          return new AIQuantifier(rep);

-        else

-          throw new System.NotImplementedException();

-      }

-      

-      [Pure]

-      public override string! ToString()

-      {

-        return string.Format("{0}({1})", FunctionSymbol, arg);

-      }

-    }

-      

-    internal sealed class AIFunctionRep : AI.IFunction

-    {

-      internal readonly QuantifierExpr! RealQuantifier;

-      private readonly int dummyIndex;

-      

-      internal AIFunctionRep(QuantifierExpr! realQuantifier, int dummyIndex)

-      {

-        this.RealQuantifier = realQuantifier;

-        this.dummyIndex = dummyIndex;

-        assert realQuantifier.TypeParameters.Length == 0; // PR: don't know how to handle this yet

-        // base();

-      }

-      [Pure][Reads(ReadsAttribute.Reads.Nothing)]

-      public override bool Equals(object obj)

-      {

-        if (obj == null) return false;

-        if (!(obj is AIFunctionRep)) return false;

-    

-        AIFunctionRep other = (AIFunctionRep)obj;

-        return object.Equals(this.RealQuantifier, other.RealQuantifier) && this.dummyIndex == other.dummyIndex;

-      }

-      [Pure] 

-      public override int GetHashCode()

-      {

-        return this.RealQuantifier.GetHashCode() ^ dummyIndex;

-      }

-      

-      [Pure]

-      public object DoVisit(AI.ExprVisitor! visitor)

-      {

-        return visitor.VisitFunction(this);

-      }

-      

-      public AI.IVariable! Param

-      { 

-        get { return (!)RealQuantifier.Dummies[dummyIndex]; } 

-      }

-      public AI.AIType! ParamType { get { throw new System.NotImplementedException(); } }

-        

-      // We lazily convert to 1 dummy per quantifier representation for AIFramework

-      private AI.IExpr/*?*/ bodyCache = null;

-      public AI.IExpr! Body

-      {

-        get

-        {

-          if (bodyCache == null)

-          {

-            int dummyi = dummyIndex;

-            int dummylen = RealQuantifier.Dummies.Length;

-            assume dummylen > dummyi;

-          

-            // return the actual body if there are no more dummies

-            if (dummyi + 1 == dummylen)

-              bodyCache = RealQuantifier.Body.IExpr;

-            else

-            {

-              AIQuantifier innerquant = new AIQuantifier(RealQuantifier, dummyi + 1);

-              bodyCache = innerquant;

-            }

-          }

-          return bodyCache;

-        }

-      }

-      public AI.IFunction! CloneWithBody(AI.IExpr! body)

-      {

-        QuantifierExpr realquant;

-      

-        AIQuantifier innerquant = body as AIQuantifier;

-        if (innerquant == null)

-        {

-          // new quantifier body, clone the real quantifier

-          realquant = (QuantifierExpr)RealQuantifier.Clone();

-          realquant.Body = BoogieFactory.IExpr2Expr(body);

-        }

-        else

-        {

-          if (innerquant.arg.dummyIndex > 0)

-          {

-            realquant = innerquant.arg.RealQuantifier;

-          }

-          else

-          {

-            realquant = (QuantifierExpr)RealQuantifier.Clone();

-            VariableSeq! newdummies = new VariableSeq();

-            newdummies.Add(Param);

-            newdummies.AddRange(innerquant.arg.RealQuantifier.Dummies);

-            realquant.Dummies = newdummies;

-            realquant.Body = innerquant.arg.RealQuantifier.Body;

-          }

-        }

-        

-        return new AIFunctionRep(realquant, dummyIndex);

-      }

-      [Pure]

-      public override string! ToString()

-      {

-        return string.Format("\\{0} :: {1}", Param, Body);

-      }

-    }

-    

-    private AI.IExpr aiexprCache = null;

-    public override AI.IExpr! IExpr {

-      get {

-        if (TypeParameters.Length > 0)

-          return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "anon", Type.Bool));

-        if (aiexprCache == null)

-        {

-          aiexprCache = new AIQuantifier(this, 0);

-        }

-        return aiexprCache;

-      }

-    } 

-  }

-

-  public class QKeyValue : Absy {

-    public readonly string! Key;

-    public readonly List<object!>! Params;  // each element is either a string or an Expr

-    public QKeyValue Next;

-    

-    public QKeyValue(IToken! tok, string! key, [Captured] List<object!>! parameters, QKeyValue next) 

-    {

-      base(tok);

-      Key = key;

-      Params = parameters;

-      Next = next;

-    }

-    

-    public void Emit(TokenTextWriter! stream) {

-      stream.Write("{:");

-      stream.Write(Key);

-      string sep = " ";

-      foreach (object p in Params) {

-        stream.Write(sep);  sep = ", ";

-        if (p is string) {

-          stream.Write("\"");

-          stream.Write((string)p);

-          stream.Write("\"");

-        } else {

-          ((Expr)p).Emit(stream);

-        }

-      }

-      stream.Write("}");

-    }

-    

-    public override void Resolve(ResolutionContext! rc) {

-      foreach (object p in Params) {

-        if (p is Expr) {

-          ((Expr)p).Resolve(rc);

-        }

-      }

-    }

-    

-    public override void Typecheck(TypecheckingContext! tc) {

-      foreach (object p in Params) {

-        if (p is Expr) {

-          ((Expr)p).Typecheck(tc);

-        }

-      }

-    }

-    public void AddLast(QKeyValue! other){

-      QKeyValue current = this;

-      while(current.Next!=null){

-        current = current.Next;

-      }

-      current.Next = other;

-    }

-    // Look for {:name string} in list of attributes.

-    public static string? FindStringAttribute(QKeyValue? kv, string! name)

-    {

-      for (; kv != null; kv = kv.Next) {

-        if (kv.Key == name) {

-          if (kv.Params.Count == 1 && kv.Params[0] is string) {

-            return (string)kv.Params[0];

-          }

-        }

-      }

-      return null;

-    }

-    // Look for {:name expr} in list of attributes.

-    public static Expr? FindExprAttribute(QKeyValue? kv, string! name)

-    {

-      for (; kv != null; kv = kv.Next) {

-        if (kv.Key == name) {

-          if (kv.Params.Count == 1 && kv.Params[0] is Expr) {

-            return (Expr)kv.Params[0];

-          }

-        }

-      }

-      return null;

-    }

-    // Return 'true' if {:name true} or {:name} is an attribute in 'kv'

-    public static bool FindBoolAttribute(QKeyValue? kv, string! name)

-    {

-      for (; kv != null; kv = kv.Next) {

-        if (kv.Key == name) {

-          return kv.Params.Count == 0 ||

-            (kv.Params.Count == 1 && kv.Params[0] is LiteralExpr && ((LiteralExpr)kv.Params[0]).IsTrue);

-        }

-      }

-      return false;

-    }

-

-    public static int FindIntAttribute(QKeyValue? kv, string! name, int defl)

-    {

-      Expr? e = FindExprAttribute(kv, name);

-      LiteralExpr? l = e as LiteralExpr;

-      if (l != null && l.isBigNum)

-        return l.asBigNum.ToIntSafe;

-      return defl;

-    }

-  }

-  

-  public class Trigger : Absy {

-    public readonly bool Pos;

-    [Rep]

-    public ExprSeq! Tr;

-    invariant 1 <= Tr.Length;

-    invariant !Pos ==> Tr.Length == 1;

-    public Trigger Next;

-    

-    public Trigger(IToken! tok, bool pos, ExprSeq! tr)

-      requires 1 <= tr.Length;

-      requires !pos ==> tr.Length == 1;

-    {

-      this(tok, pos, tr, null);

-    }

-

-    public Trigger(IToken! tok, bool pos, ExprSeq! tr, Trigger next)

-      : base(tok)

-      requires 1 <= tr.Length;

-      requires !pos ==> tr.Length == 1;

-    {

-      this.Pos = pos;

-      this.Tr = tr;

-      this.Next = next;

-      // base(tok);

-    }

-

-    public void Emit(TokenTextWriter! stream) {

-      stream.SetToken(this);

-      assert this.Tr.Length >= 1;

-      string! sep = Pos ? "{ " : "{:nopats ";

-      foreach (Expr! e in this.Tr) {

-        stream.Write(sep);

-        sep = ", ";

-        e.Emit(stream);

-      }

-      stream.Write(" }");

-    }

-    public override void Resolve(ResolutionContext! rc) {

-      rc.TriggerMode = true;

-      foreach (Expr! e in this.Tr) {

-        e.Resolve(rc);

-

-        // just a variable by itself is not allowed

-        if (e is IdentifierExpr) {

-          rc.Error(e, "a matching pattern must be more than just a variable by itself: {0}", e);

-        }

-        

-        // the free-variable check is performed in the surrounding quantifier expression (because that's

-        // where the bound variables are known)

-      }

-      rc.TriggerMode = false;

-    }

-

-    /// <summary>

-    /// Add to "freeVars" the free variables in the triggering expressions.

-    /// </summary>

-    public void ComputeFreeVariables(Set /*Variable*/! freeVars) {

-      foreach (Expr! e in this.Tr) {

-        e.ComputeFreeVariables(freeVars);

-      }

-    }

-

-    public override void Typecheck(TypecheckingContext! tc) {

-      foreach (Expr! e in this.Tr) {

-        e.Typecheck(tc);

-      }

-    }

-

-    public void AddLast(Trigger other){

-        Trigger current = this;

-        while(current.Next!=null){

-            current = current.Next;

-        }

-        current.Next = other;

-    }

-

-    public override Absy! StdDispatch(StandardVisitor! visitor)

-    {

-      return visitor.VisitTrigger(this);

-    }

-  }

-

-  public class ForallExpr : QuantifierExpr 

-  {

-    public ForallExpr(IToken! tok, TypeVariableSeq! typeParams,

-                      VariableSeq! dummies, QKeyValue kv, Trigger triggers, Expr! body)

-      requires dummies.Length + typeParams.Length > 0;

-    {

-      base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons

-    }

-    public ForallExpr(IToken! tok, VariableSeq! dummies, Trigger triggers, Expr! body)

-      requires dummies.Length > 0;

-    {

-      base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons

-    }

-    public ForallExpr(IToken! tok, VariableSeq! dummies, Expr! body)

-      requires dummies.Length > 0;

-    {

-      base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons

-    }

-    public ForallExpr(IToken! tok, TypeVariableSeq! typeParams, VariableSeq! dummies, Expr! body)

-      requires dummies.Length + typeParams.Length > 0;

-    {

-      base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons

-    }

-    public override AI.IFunctionSymbol! FunctionSymbol

-    {

-      get { 

-        return AI.Prop.Forall;

-      }

-    }

-

-    public override Absy! StdDispatch(StandardVisitor! visitor)

-    {

-      return visitor.VisitForallExpr(this);

-    }

-  }

-  public class ExistsExpr : QuantifierExpr 

-  {

-    public ExistsExpr(IToken! tok, TypeVariableSeq! typeParams, VariableSeq! dummies,

-                      QKeyValue kv, Trigger triggers, Expr! body)

-      requires dummies.Length + typeParams.Length > 0;

-    {

-      base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons

-    }

-    public ExistsExpr(IToken! tok, VariableSeq! dummies, Trigger triggers, Expr! body)

-      requires dummies.Length > 0;

-    {

-      base(tok, new TypeVariableSeq (), dummies, null, triggers, body); // here for aesthetic reasons

-    }

-    public ExistsExpr(IToken! tok, VariableSeq! dummies, Expr! body)

-      requires dummies.Length > 0;

-    {

-      base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons

-    }

-    public override AI.IFunctionSymbol! FunctionSymbol

-    {

-      get {

-        return AI.Prop.Exists;

-      }

-    }

-

-    public override Absy! StdDispatch(StandardVisitor! visitor)

-    {

-      return visitor.VisitExistsExpr(this);

-    }

-  }

-

-

 

   public class IfThenElse : IAppliable, AI.IFunctionSymbol {