diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 5 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 689 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.ssc | 857 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 7 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 1 | ||||
| -rw-r--r-- | Source/Core/Core.sscproj | 10 | ||||
| -rw-r--r-- | Source/Core/Duplicator.ssc | 6 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.ssc | 115 | ||||
| -rw-r--r-- | Source/Core/Parser.ssc | 221 | ||||
| -rw-r--r-- | Source/Core/Scanner.ssc | 18 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.ssc | 16 | ||||
| -rw-r--r-- | Test/test1/Answer | 6 | ||||
| -rw-r--r-- | Test/test1/Lambda.bpl | 19 | ||||
| -rw-r--r-- | Test/test1/runtest.bat | 1 | ||||
| -rw-r--r-- | Test/test2/Answer | 10 | ||||
| -rw-r--r-- | Test/test2/Lambda.bpl | 41 | ||||
| -rw-r--r-- | Test/test2/runtest.bat | 2 |
17 files changed, 1219 insertions, 805 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index f58dbcfd..17132062 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -486,6 +486,11 @@ namespace Microsoft.Boogie program.Emit(new TokenTextWriter(Console.Out));
}
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
// ---------- Verify ------------------------------------------------------------
if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }
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 {
diff --git a/Source/Core/AbsyQuant.ssc b/Source/Core/AbsyQuant.ssc new file mode 100644 index 00000000..af1362c9 --- /dev/null +++ b/Source/Core/AbsyQuant.ssc @@ -0,0 +1,857 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+//---------------------------------------------------------------------------------------------
+// BoogiePL - AbsyQuant.cs
+//---------------------------------------------------------------------------------------------
+
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Collections.Generic;
+ using Microsoft.Boogie.AbstractInterpretation;
+ using AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Contracts;
+ using Microsoft.Basetypes;
+
+
+ //---------------------------------------------------------------------
+ // Quantifiers and general binders
+ //---------------------------------------------------------------------
+
+ public enum BinderKind {
+ Forall,
+ Exists,
+ Lambda
+ }
+
+ public abstract class BinderExpr : Expr
+ {
+ public TypeVariableSeq! TypeParameters;
+ public VariableSeq! Dummies;
+ public QKeyValue Attributes;
+ public Expr! Body;
+
+ public BinderExpr(IToken! tok, TypeVariableSeq! typeParameters,
+ VariableSeq! dummies, QKeyValue kv, Expr! body)
+ requires dummies.Length + typeParameters.Length > 0;
+ {
+ base(tok);
+
+ TypeParameters = typeParameters;
+ Dummies = dummies;
+ Attributes = kv;
+ Body = body;
+ }
+
+ abstract public BinderKind Kind { get; }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj)
+ {
+ if (obj == null) return false;
+ if (!(obj is BinderExpr) ||
+ this.Kind != ((BinderExpr)obj).Kind) return false;
+
+ BinderExpr other = (BinderExpr)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();
+ h *= ((int)Kind + 1);
+ return h;
+ }
+
+ protected virtual void EmitTypeHint(TokenTextWriter! stream)
+ {
+ }
+
+ protected virtual void EmitTriggers(TokenTextWriter! stream)
+ {
+ }
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.Write(this, "({0}", Kind.ToString().ToLower());
+ this.EmitTypeHint(stream);
+ 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(" ");
+ }
+ this.EmitTriggers(stream);
+
+ this.Body.Emit(stream);
+ stream.Write(")");
+ }
+
+ protected virtual void ResolveTriggers(ResolutionContext! rc)
+ {
+ }
+
+ public override void Resolve(ResolutionContext! rc)
+ {
+ 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);
+ }
+ this.ResolveTriggers(rc);
+ 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;
+ }
+ }
+
+ 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);
+ }
+ }
+
+ protected TypeVariableSeq! GetUnmentionedTypeParameters()
+ {
+ TypeVariableSeq! dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);
+ TypeVariableSeq! unmentionedParameters = new TypeVariableSeq ();
+ foreach (TypeVariable! var in TypeParameters)
+ if (!dummyParameters.Has(var))
+ unmentionedParameters.Add(var);
+ return unmentionedParameters;
+ }
+
+
+ public abstract AI.IFunctionSymbol! FunctionSymbol { get; }
+
+ internal sealed class AIQuantifier : AI.IFunApp
+ {
+ internal readonly AIFunctionRep! arg;
+ internal AIQuantifier(BinderExpr! 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 BinderExpr! RealQuantifier;
+ private readonly int dummyIndex;
+
+ internal AIFunctionRep(BinderExpr! 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)
+ {
+ BinderExpr realquant;
+
+ AIQuantifier innerquant = body as AIQuantifier;
+ if (innerquant == null)
+ {
+ // new quantifier body, clone the real quantifier
+ realquant = (BinderExpr)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 override BinderKind Kind { get { return BinderKind.Forall; } }
+ }
+
+
+ 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 override BinderKind Kind { get { return BinderKind.Exists; } }
+ }
+
+
+
+ public abstract class QuantifierExpr : BinderExpr
+ {
+ public Trigger Triggers;
+
+ 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, typeParameters, dummies, kv, body);
+
+ assert (this is ForallExpr) || (this is ExistsExpr);
+
+ Triggers = triggers;
+ SkolemId = SkolemIds++;
+ }
+
+ protected override void EmitTriggers(TokenTextWriter! stream)
+ {
+ for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
+ tr.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;
+ }
+ }
+ }
+
+ #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
+
+ protected override void ResolveTriggers(ResolutionContext! 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);
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public override void Resolve(ResolutionContext! rc)
+ {
+ int oldErrorCount = rc.ErrorCount;
+
+ this.MergeAdjecentQuantifier();
+
+ base.Resolve(rc);
+
+ if (oldErrorCount == rc.ErrorCount) {
+ this.ApplyNeverTriggers();
+ }
+ }
+
+
+ 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! unmentionedParameters = GetUnmentionedTypeParameters();
+
+ 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 class LambdaExpr : BinderExpr
+ {
+ public LambdaExpr(IToken! tok, TypeVariableSeq! typeParameters,
+ VariableSeq! dummies, QKeyValue kv, Expr! body)
+ requires dummies.Length + typeParameters.Length > 0;
+ {
+ base(tok, typeParameters, dummies, kv, body);
+ }
+
+ public override BinderKind Kind { get { return BinderKind.Lambda; } }
+
+ public override void Resolve(ResolutionContext! rc)
+ {
+ base.Resolve(rc);
+ }
+
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ kv.Typecheck(tc);
+ }
+ Body.Typecheck(tc);
+ assert Body.Type != null; // follows from postcondition of Expr.Typecheck
+
+ TypeSeq! argTypes = new TypeSeq();
+ foreach (Variable! v in Dummies) {
+ argTypes.Add(v.TypedIdent.Type);
+ }
+ this.Type = new MapType(this.tok, this.TypeParameters, argTypes, Body.Type);
+
+ this.Type = this.ShallowType;
+
+ // Check that type parameters occur in the types of the
+ // dummies, or otherwise in the triggers. This can only be
+ // done after typechecking
+ TypeVariableSeq! unmentionedParameters = GetUnmentionedTypeParameters();
+
+ if (unmentionedParameters.Length > 0) {
+ tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
+ }
+ }
+
+ private Type? mapType;
+ public override Type! ShallowType {
+ get {
+ if (mapType == null) {
+ TypeSeq! argTypes = new TypeSeq();
+ foreach (Variable! v in Dummies) {
+ argTypes.Add(v.TypedIdent.Type);
+ }
+ mapType = new MapType(this.tok, this.TypeParameters, argTypes, Body.ShallowType);
+ }
+
+ return mapType;
+ }
+ }
+
+ public override AI.IFunctionSymbol! FunctionSymbol
+ {
+ get {
+ return AI.Prop.Exists;
+ }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitLambdaExpr(this);
+ }
+
+ }
+
+
+}
+
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index ab7e6c81..ee9675a5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1289,6 +1289,12 @@ AtomExpression<out Expr! e> QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>
(. if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)
+ | Lambda (. x = token; .)
+ QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>
+ (. if (trig != null)
+ SemErr("triggers not allowed in lambda expressions");
+ if (typeParams.Length + ds.Length > 0)
+ e = new LambdaExpr(x, typeParams, ds, kv, e); .)
)
")"
| IfThenElseExpression<out e>
@@ -1382,6 +1388,7 @@ QuantifierBody<IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds, Forall = "forall" | '\u2200'.
Exists = "exists" | '\u2203'.
+Lambda = "lambda" | '\u03bb'.
QSep = "::" | '\u2022'.
/*------------------------------------------------------------------------*/
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index bed34c63..f9daaaf5 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -152,6 +152,7 @@ namespace Microsoft.Boogie public BvHandling Bitvectors = BvHandling.Z3Native;
public bool UseArrayTheory = false;
+ public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
diff --git a/Source/Core/Core.sscproj b/Source/Core/Core.sscproj index d43dca98..91bbaf47 100644 --- a/Source/Core/Core.sscproj +++ b/Source/Core/Core.sscproj @@ -188,6 +188,10 @@ />
<File BuildAction="Compile"
SubType="Code"
+ RelPath="AbsyQuant.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
RelPath="Xml.ssc"
/>
<File BuildAction="Compile"
@@ -196,6 +200,10 @@ />
<File BuildAction="Compile"
SubType="Code"
+ RelPath="LambdaHelper.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
RelPath="LoopUnroll.ssc"
/>
<File BuildAction="Compile"
@@ -217,4 +225,4 @@ </Include>
</Files>
</XEN>
-</VisualStudioProject>
\ No newline at end of file +</VisualStudioProject>
diff --git a/Source/Core/Duplicator.ssc b/Source/Core/Duplicator.ssc index 08577400..3fde1bf2 100644 --- a/Source/Core/Duplicator.ssc +++ b/Source/Core/Duplicator.ssc @@ -190,9 +190,9 @@ namespace Microsoft.Boogie {
return base.VisitProgram ((Program) node.Clone());
}
- public override QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)
+ public override BinderExpr! VisitBinderExpr(BinderExpr! node)
{
- return base.VisitQuantifierExpr ((QuantifierExpr) node.Clone());
+ return base.VisitBinderExpr ((BinderExpr) node.Clone());
}
public override Cmd! VisitRE(RE! node)
{
@@ -375,4 +375,4 @@ namespace Microsoft.Boogie }
}
#endregion
-}
\ No newline at end of file +}
diff --git a/Source/Core/LambdaHelper.ssc b/Source/Core/LambdaHelper.ssc new file mode 100644 index 00000000..2489b57d --- /dev/null +++ b/Source/Core/LambdaHelper.ssc @@ -0,0 +1,115 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie {
+
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+
+ public static class LambdaHelper
+ {
+ public static Absy! Desugar(Absy! node, out List<Expr!>! axioms, out List<Function!>! functions)
+ {
+ LambdaVisitor v = new LambdaVisitor();
+ node = v.Visit(node);
+ axioms = v.lambdaAxioms;
+ functions = v.lambdaFunctions;
+ return node;
+ }
+
+ public static void ExpandLambdas(Program! prog)
+ {
+ List<Expr!>! axioms;
+ List<Function!>! functions;
+ Desugar(prog, out axioms, out functions);
+ foreach (var f in functions) {
+ prog.TopLevelDeclarations.Add(f);
+ }
+ foreach (var a in axioms) {
+ prog.TopLevelDeclarations.Add(new Axiom(a.tok, a));
+ }
+ }
+
+ private class LambdaVisitor : StandardVisitor
+ {
+ internal List<Expr!>! lambdaAxioms = new List<Expr!>();
+ internal List<Function!>! lambdaFunctions = new List<Function!>();
+ static int lambdaid = 0;
+
+ public override Absy! Visit(Absy! node)
+ {
+ node = base.Visit(node);
+
+ LambdaExpr lambda = node as LambdaExpr;
+ if (lambda != null) {
+ IToken! tok = lambda.tok;
+
+ Set freeVars = new Set();
+ lambda.ComputeFreeVariables(freeVars);
+ // this is ugly, the output will depend on hashing order
+ Hashtable subst = new Hashtable();
+ VariableSeq formals = new VariableSeq();
+ ExprSeq callArgs = new ExprSeq();
+ ExprSeq axCallArgs = new ExprSeq();
+ VariableSeq dummies = new VariableSeq(lambda.Dummies);
+
+ foreach (object o in freeVars) {
+ Variable v = o as Variable;
+ if (v != null) {
+ Formal f = new Formal(v.tok, v.TypedIdent, true);
+ formals.Add(f);
+ BoundVariable b = new BoundVariable(v.tok, v.TypedIdent);
+ dummies.Add(b);
+ callArgs.Add(new IdentifierExpr(v.tok, v));
+ Expr! id = new IdentifierExpr(f.tok, b);
+ subst.Add(v, id);
+ axCallArgs.Add(id);
+ }
+ // TODO: do something about type variables
+ }
+
+ Formal res = new Formal(tok, new TypedIdent(tok, "", (!)lambda.Type), false);
+ Function fn = new Function(tok, "lambda@" + lambdaid++, new TypeVariableSeq(), formals, res, "auto-generated lambda function", lambda.Attributes);
+ IdentifierExpr callId = new IdentifierExpr(tok, fn.Name);
+ FunctionCall fcall = new FunctionCall(callId);
+ fcall.Func = fn;
+
+ List<Expr!> selectArgs = new List<Expr!>();
+ foreach (Variable! v in lambda.Dummies) {
+ selectArgs.Add(new IdentifierExpr(v.tok, v));
+ }
+ NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);
+ axcall.Type = res.TypedIdent.Type;
+ axcall.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ NAryExpr select = Expr.Select(axcall, selectArgs);
+ select.Type = lambda.Body.Type;
+ select.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+
+ Expr body = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambda.Body);
+ body = Expr.Eq(select, body);
+ body.Type = Type.Bool;
+ ((NAryExpr)body).TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ Trigger trig = new Trigger(select.tok, true, new ExprSeq(select));
+
+ body = new ForallExpr(tok, lambda.TypeParameters, dummies, lambda.Attributes, trig, body);
+
+ lambdaFunctions.Add(fn);
+ lambdaAxioms.Add(body);
+
+ Expr call = new NAryExpr(tok, fcall, callArgs);
+
+ return call;
+ }
+
+ return node;
+ }
+ }
+ }
+
+} // end namespace
+
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc index 95eb1a76..d02ccb37 100644 --- a/Source/Core/Parser.ssc +++ b/Source/Core/Parser.ssc @@ -11,7 +11,7 @@ using Microsoft.Contracts; namespace BoogiePL {
public class Parser {
- const int maxT = 86;
+ const int maxT = 88;
const bool T = true;
const bool x = false;
@@ -294,7 +294,7 @@ private class BvBounds : Expr { Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, "", retTy);
- } else Error(87);
+ } else Error(89);
if (t.kind == 25) {
Get();
Expression(out tmp);
@@ -302,7 +302,7 @@ private class BvBounds : Expr { Expect(26);
} else if (t.kind == 7) {
Get();
- } else Error(88);
+ } else Error(90);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));
@@ -446,7 +446,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null);
- } else Error(89);
+ } else Error(91);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -550,7 +550,7 @@ private class BvBounds : Expr { ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
- } else Error(90);
+ } else Error(92);
}
static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
@@ -597,7 +597,7 @@ private class BvBounds : Expr { Get();
Type(out ty);
Expect(9);
- } else Error(91);
+ } else Error(93);
}
static void Ident(out IToken! x) {
@@ -626,7 +626,7 @@ private class BvBounds : Expr { } else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
ts.Add(ty);
- } else Error(92);
+ } else Error(94);
}
static void MapType(out Bpl.Type! ty) {
@@ -798,7 +798,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecPrePost(true, pre, post);
} else if (t.kind == 34 || t.kind == 35) {
SpecPrePost(false, pre, post);
- } else Error(93);
+ } else Error(95);
}
static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
@@ -826,7 +826,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(94);
+ } else Error(96);
} else if (t.kind == 35) {
Get();
tok = token;
@@ -841,8 +841,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(95);
- } else Error(96);
+ } else Error(97);
+ } else Error(98);
}
static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
@@ -893,7 +893,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(token,e));
- } else Error(97);
+ } else Error(99);
Expect(7);
}
@@ -937,7 +937,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { CallCmd(out cn);
Expect(7);
c = cn;
- } else Error(98);
+ } else Error(100);
}
static void StmtList(out StmtList! stmtList) {
@@ -1021,7 +1021,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else Error(99);
+ } else Error(101);
}
static void TransferCmd(out TransferCmd! tc) {
@@ -1039,7 +1039,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 39) {
Get();
tc = new ReturnCmd(token);
- } else Error(100);
+ } else Error(102);
Expect(7);
}
@@ -1064,7 +1064,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
StmtList(out els);
elseOption = els;
- } else Error(101);
+ } else Error(103);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1123,7 +1123,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(102);
+ } else Error(104);
Expect(9);
}
@@ -1161,7 +1161,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(7);
c = new AssignCmd(x, lhss, rhss);
- } else Error(103);
+ } else Error(105);
}
static void CallCmd(out Cmd! c) {
@@ -1224,7 +1224,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(104);
+ } else Error(106);
} else if (t.kind == 51) {
Get();
Ident(out first);
@@ -1278,7 +1278,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(105);
+ } else Error(107);
}
static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {
@@ -1318,7 +1318,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out e);
exprOptional = e;
- } else Error(106);
+ } else Error(108);
}
static void CallOutIdent(out IToken id) {
@@ -1330,7 +1330,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 1) {
Ident(out p);
id = p;
- } else Error(107);
+ } else Error(109);
}
static void Expressions(out ExprSeq! es) {
@@ -1375,7 +1375,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 53) {
Get();
- } else Error(108);
+ } else Error(110);
}
static void LogicalExpression(out Expr! e0) {
@@ -1413,7 +1413,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 55) {
Get();
- } else Error(109);
+ } else Error(111);
}
static void ExpliesOp() {
@@ -1421,7 +1421,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 57) {
Get();
- } else Error(110);
+ } else Error(112);
}
static void RelationalExpression(out Expr! e0) {
@@ -1439,7 +1439,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 59) {
Get();
- } else Error(111);
+ } else Error(113);
}
static void OrOp() {
@@ -1447,7 +1447,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 61) {
Get();
- } else Error(112);
+ } else Error(114);
}
static void BvTerm(out Expr! e0) {
@@ -1514,7 +1514,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { x = token; op=BinaryOperator.Opcode.Ge;
break;
}
- default: Error(113); break;
+ default: Error(115); break;
}
}
@@ -1546,7 +1546,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 72) {
Get();
x = token; op=BinaryOperator.Opcode.Sub;
- } else Error(114);
+ } else Error(116);
}
static void UnaryExpression(out Expr! e) {
@@ -1565,7 +1565,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(12)) {
CoercionExpression(out e);
- } else Error(115);
+ } else Error(117);
}
static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
@@ -1579,7 +1579,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 74) {
Get();
x = token; op=BinaryOperator.Opcode.Mod;
- } else Error(116);
+ } else Error(118);
}
static void NegOp() {
@@ -1587,7 +1587,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 76) {
Get();
- } else Error(117);
+ } else Error(119);
}
static void CoercionExpression(out Expr! e) {
@@ -1611,7 +1611,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else Error(118);
+ } else Error(120);
}
}
@@ -1721,7 +1721,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new NAryExpr(x, new FunctionCall(id), es);
} else if (t.kind == 9) {
e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
- } else Error(119);
+ } else Error(121);
Expect(9);
}
break;
@@ -1754,7 +1754,15 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else Error(120);
+ } else if (t.kind == 84 || t.kind == 85) {
+ Lambda();
+ x = token;
+ QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
+ if (trig != null)
+ SemErr("triggers not allowed in lambda expressions");
+ if (typeParams.Length + ds.Length > 0)
+ e = new LambdaExpr(x, typeParams, ds, kv, e);
+ } else Error(122);
Expect(9);
break;
}
@@ -1762,7 +1770,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { IfThenElseExpression(out e);
break;
}
- default: Error(121); break;
+ default: Error(123); break;
}
}
@@ -1787,7 +1795,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 81) {
Get();
- } else Error(122);
+ } else Error(124);
}
static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
@@ -1804,7 +1812,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
} else if (t.kind == 1) {
BoundVars(q, out ds);
- } else Error(123);
+ } else Error(125);
QSep();
while (t.kind == 25) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1817,7 +1825,15 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (t.kind == 83) {
Get();
- } else Error(124);
+ } else Error(126);
+ }
+
+ static void Lambda() {
+ if (t.kind == 84) {
+ Get();
+ } else if (t.kind == 85) {
+ Get();
+ } else Error(127);
}
static void IfThenElseExpression(out Expr! e) {
@@ -1887,7 +1903,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, true, es, null));
}
- } else Error(125);
+ } else Error(128);
Expect(26);
}
@@ -1901,15 +1917,15 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { } else if (StartOf(5)) {
Expression(out e);
o = e;
- } else Error(126);
+ } else Error(129);
}
static void QSep() {
- if (t.kind == 84) {
+ if (t.kind == 86) {
Get();
- } else if (t.kind == 85) {
+ } else if (t.kind == 87) {
Get();
- } else Error(127);
+ } else Error(130);
}
@@ -2012,50 +2028,53 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { case 81: s = "\\u2200 expected"; break;
case 82: s = "exists expected"; break;
case 83: s = "\\u2203 expected"; break;
- case 84: s = ":: expected"; break;
- case 85: s = "\\u2022 expected"; break;
- case 86: s = "??? expected"; break;
- case 87: s = "invalid Function"; break;
- case 88: s = "invalid Function"; break;
- case 89: s = "invalid Procedure"; break;
- case 90: s = "invalid Type"; break;
- case 91: s = "invalid TypeAtom"; break;
- case 92: s = "invalid TypeArgs"; break;
- case 93: s = "invalid Spec"; break;
- case 94: s = "invalid SpecPrePost"; break;
- case 95: s = "invalid SpecPrePost"; break;
+ case 84: s = "lambda expected"; break;
+ case 85: s = "\\u03bb expected"; break;
+ case 86: s = ":: expected"; break;
+ case 87: s = "\\u2022 expected"; break;
+ case 88: s = "??? expected"; break;
+ case 89: s = "invalid Function"; break;
+ case 90: s = "invalid Function"; break;
+ case 91: s = "invalid Procedure"; break;
+ case 92: s = "invalid Type"; break;
+ case 93: s = "invalid TypeAtom"; break;
+ case 94: s = "invalid TypeArgs"; break;
+ case 95: s = "invalid Spec"; break;
case 96: s = "invalid SpecPrePost"; break;
- case 97: s = "invalid SpecBlock"; break;
- case 98: s = "invalid LabelOrCmd"; break;
- case 99: s = "invalid StructuredCmd"; break;
- case 100: s = "invalid TransferCmd"; break;
- case 101: s = "invalid IfCmd"; break;
- case 102: s = "invalid Guard"; break;
- case 103: s = "invalid LabelOrAssign"; break;
- case 104: s = "invalid CallCmd"; break;
- case 105: s = "invalid CallCmd"; break;
- case 106: s = "invalid CallForallArg"; break;
- case 107: s = "invalid CallOutIdent"; break;
- case 108: s = "invalid EquivOp"; break;
- case 109: s = "invalid ImpliesOp"; break;
- case 110: s = "invalid ExpliesOp"; break;
- case 111: s = "invalid AndOp"; break;
- case 112: s = "invalid OrOp"; break;
- case 113: s = "invalid RelOp"; break;
- case 114: s = "invalid AddOp"; break;
- case 115: s = "invalid UnaryExpression"; break;
- case 116: s = "invalid MulOp"; break;
- case 117: s = "invalid NegOp"; break;
- case 118: s = "invalid CoercionExpression"; break;
- case 119: s = "invalid AtomExpression"; break;
- case 120: s = "invalid AtomExpression"; break;
+ case 97: s = "invalid SpecPrePost"; break;
+ case 98: s = "invalid SpecPrePost"; break;
+ case 99: s = "invalid SpecBlock"; break;
+ case 100: s = "invalid LabelOrCmd"; break;
+ case 101: s = "invalid StructuredCmd"; break;
+ case 102: s = "invalid TransferCmd"; break;
+ case 103: s = "invalid IfCmd"; break;
+ case 104: s = "invalid Guard"; break;
+ case 105: s = "invalid LabelOrAssign"; break;
+ case 106: s = "invalid CallCmd"; break;
+ case 107: s = "invalid CallCmd"; break;
+ case 108: s = "invalid CallForallArg"; break;
+ case 109: s = "invalid CallOutIdent"; break;
+ case 110: s = "invalid EquivOp"; break;
+ case 111: s = "invalid ImpliesOp"; break;
+ case 112: s = "invalid ExpliesOp"; break;
+ case 113: s = "invalid AndOp"; break;
+ case 114: s = "invalid OrOp"; break;
+ case 115: s = "invalid RelOp"; break;
+ case 116: s = "invalid AddOp"; break;
+ case 117: s = "invalid UnaryExpression"; break;
+ case 118: s = "invalid MulOp"; break;
+ case 119: s = "invalid NegOp"; break;
+ case 120: s = "invalid CoercionExpression"; break;
case 121: s = "invalid AtomExpression"; break;
- case 122: s = "invalid Forall"; break;
- case 123: s = "invalid QuantifierBody"; break;
- case 124: s = "invalid Exists"; break;
- case 125: s = "invalid AttributeOrTrigger"; break;
- case 126: s = "invalid AttributeParameter"; break;
- case 127: s = "invalid QSep"; break;
+ case 122: s = "invalid AtomExpression"; break;
+ case 123: s = "invalid AtomExpression"; break;
+ case 124: s = "invalid Forall"; break;
+ case 125: s = "invalid QuantifierBody"; break;
+ case 126: s = "invalid Exists"; break;
+ case 127: s = "invalid Lambda"; break;
+ case 128: s = "invalid AttributeOrTrigger"; break;
+ case 129: s = "invalid AttributeParameter"; break;
+ case 130: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -2063,21 +2082,21 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
static bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index d8e18754..2d977e79 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -238,7 +238,7 @@ public class Scanner { const char LF = '\n';
[Microsoft.Contracts.Verify(false)]
static Scanner() {
- start[0] = 57;
+ start[0] = 58;
start[33] = 41;
start[34] = 6;
start[35] = 2;
@@ -333,7 +333,8 @@ public class Scanner { start[125] = 20;
start[126] = 2;
start[172] = 52;
- start[8226] = 56;
+ start[955] = 55;
+ start[8226] = 57;
start[8656] = 33;
start[8658] = 32;
start[8660] = 29;
@@ -345,7 +346,7 @@ public class Scanner { start[8804] = 45;
start[8805] = 46;
}
- const int noSym = 86;
+ const int noSym = 88;
static short[] start = new short[16385];
@@ -521,6 +522,7 @@ public class Scanner { case "old": t.kind = 79; break;
case "then": t.kind = 80; break;
case "exists": t.kind = 82; break;
+ case "lambda": t.kind = 84; break;
default: break;
}
@@ -574,7 +576,7 @@ public class Scanner { {t.kind = 9; goto done;}
case 13:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 55;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 56;}
else {t.kind = 10; goto done;}
case 14:
{t.kind = 11; goto done;}
@@ -672,10 +674,12 @@ public class Scanner { case 54:
{t.kind = 83; goto done;}
case 55:
- {t.kind = 84; goto done;}
- case 56:
{t.kind = 85; goto done;}
- case 57: {t.kind = 0; goto done;}
+ case 56:
+ {t.kind = 86; goto done;}
+ case 57:
+ {t.kind = 87; goto done;}
+ case 58: {t.kind = 0; goto done;}
}
done:
t.val = buf.ToString();
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index 99bac64e..c6b50b24 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -253,6 +253,11 @@ namespace Microsoft.Boogie node = (ForallExpr) this.VisitQuantifierExpr(node);
return node;
}
+ public virtual LambdaExpr! VisitLambdaExpr(LambdaExpr! node)
+ {
+ node = (LambdaExpr) this.VisitBinderExpr(node);
+ return node;
+ }
public virtual Formal! VisitFormal(Formal! node)
{
return node;
@@ -374,14 +379,19 @@ namespace Microsoft.Boogie node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
return node;
}
+ public virtual BinderExpr! VisitBinderExpr(BinderExpr! node)
+ {
+ node.Body = this.VisitExpr(node.Body);
+ node.Dummies = this.VisitVariableSeq(node.Dummies);
+ //node.Type = this.VisitType(node.Type);
+ return node;
+ }
public virtual QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)
{
+ node = (QuantifierExpr!) this.VisitBinderExpr(node);
if (node.Triggers != null) {
node.Triggers = this.VisitTrigger(node.Triggers);
}
- node.Body = this.VisitExpr(node.Body);
- node.Dummies = this.VisitVariableSeq(node.Dummies);
- //node.Type = this.VisitType(node.Type);
return node;
}
public virtual Cmd! VisitRE(RE! node)
diff --git a/Test/test1/Answer b/Test/test1/Answer index 10ad5494..a8b73b53 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -139,3 +139,9 @@ IfThenElse0.bpl(5,7): Error: the first argument to if-then-else should be bool, IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int
IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)
3 type checking errors detected in IfThenElse0.bpl
+Lambda.bpl(5,2): Error: mismatched types in assignment command (cannot assign [int]int to [int,int]int)
+Lambda.bpl(6,2): Error: mismatched types in assignment command (cannot assign [int]int to [int]bool)
+Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lambda parameters
+Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)
+Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +
+5 type checking errors detected in Lambda.bpl
diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl new file mode 100644 index 00000000..d0ccd3a1 --- /dev/null +++ b/Test/test1/Lambda.bpl @@ -0,0 +1,19 @@ +procedure foo() +{ + var a: [int,int]int; + var b: [int]bool; + a := (lambda y:int :: y + 1); + b := (lambda y:int :: y + 1); +} + +procedure bar() +{ + var a: [int]int; + a := (lambda<T> y:int :: y + 1); +} + +procedure baz() +{ + var a: [bool]int; + a := (lambda y:bool :: y + 1); +} diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index dda3a0af..979c36e4 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -18,3 +18,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify EmptyCallArgs.bpl
%BGEXE% %* /noVerify FunBody.bpl
%BGEXE% %* /noVerify IfThenElse0.bpl
+%BGEXE% %* /noVerify Lambda.bpl
diff --git a/Test/test2/Answer b/Test/test2/Answer index 230a8861..60d76af1 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -333,6 +333,16 @@ Execution trace: IfThenElse1.bpl(33,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
+
+-------------------- Lambda.bpl --------------------
+Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Lambda.bpl(36,5): anon0
+Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Lambda.bpl(36,5): anon0
+
+Boogie program verifier finished with 3 verified, 2 errors
-------------------- sk_hack.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl new file mode 100644 index 00000000..48610ff1 --- /dev/null +++ b/Test/test2/Lambda.bpl @@ -0,0 +1,41 @@ +procedure foo() +{ + var a: [int]int; + var c:int,b:bool; + a := (lambda y:int :: if b then y + c else 7); + assume b; + assert a[3] == c+3; +} + +procedure bar() +{ + assert (lambda x:int :: x > 0)[10]; + +} + +type t1; + +procedure baz() +{ + var m:[int,t1]int; + var t:t1, t2:t1; + + m := (lambda i:int, tt:t1 :: if tt == t then i else 12); + assert m[1,t] == 1; + assert t == t2 || m[1,t2] == 12; + assert m[12,t2] == 12; + +} + + +procedure fail() +{ + var m:[int,t1]int; + var t:t1, t2:t1; + + m := (lambda i:int, tt:t1 :: if tt == t then i else 12); + assert m[1,t2] == 12; + assert m[1,t] == 2; +} + + diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat index ab9ec103..ea4376b6 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl strings-no-where.bpl strings-where.bpl
Structured.bpl Where.bpl UpdateExpr.bpl
NeverPattern.bpl NullaryMaps.bpl Implies.bpl
- IfThenElse1.bpl) do (
+ IfThenElse1.bpl Lambda.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /noinfer %%f
|