Boogie: Renaming core sources in preparation for port commit

1 files changed, 689 insertions, 0 deletions

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
new file mode 100644
index 00000000..0db27d6d
--- /dev/null
+++ b/Source/Core/Inline.cs
@@ -0,0 +1,689 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+namespace Microsoft.Boogie {

+  

+  using System;

+  using System.IO;

+  using System.Collections;

+  using System.Collections.Generic;

+  using BoogiePL;

+  using System.Diagnostics;

+  using System.Text.RegularExpressions; // for procedure inlining

+

+  // this callback is called before inlining a procedure

+  public delegate void InlineCallback(Implementation! impl);

+

+  public class Inliner

+  {   

+    private InlineCallback inlineCallback;

+  

+    protected CodeCopier! codeCopier;

+    

+    protected Dictionary<string!,int>! /* Procedure.Name -> int */ recursiveProcUnrollMap;

+    

+    protected Dictionary<string!,int>! /* Procedure.Name -> int */ inlinedProcLblMap;

+    

+    protected void NextInlinedProcLabel(string! procName) {

+      int currentId;

+      if (inlinedProcLblMap.TryGetValue(procName, out currentId)) {

+        inlinedProcLblMap[procName] = currentId + 1;

+      } else {

+        inlinedProcLblMap.Add(procName, 0);

+      }

+    }

+    

+    protected string! GetInlinedProcLabel(string! procName) {

+      int currentId;

+      if (!inlinedProcLblMap.TryGetValue(procName, out currentId)) {

+        currentId = 0;

+        inlinedProcLblMap.Add(procName, currentId);

+      }

+      return "inline$" + procName + "$" + currentId;

+    }

+    

+    protected string! GetProcVarName(string! procName, string! formalName) {

+      string! prefix = GetInlinedProcLabel(procName);

+      return prefix + "$" + formalName;

+    }   

+    

+    protected Inliner(InlineCallback cb) {        

+      inlinedProcLblMap = new Dictionary<string!,int>();

+      recursiveProcUnrollMap = new Dictionary<string!,int>();

+      codeCopier = new CodeCopier();

+      inlineCallback = cb;

+    }

+    

+    public static void ProcessImplementation(Program! program, Implementation! impl, InlineCallback cb)

+      requires impl.Proc != null;

+    {

+      Inliner inliner = new Inliner(cb);

+      

+      VariableSeq! newInParams = new VariableSeq(impl.InParams);

+      VariableSeq! newOutParams = new VariableSeq(impl.OutParams);

+      VariableSeq! newLocalVars = new VariableSeq(impl.LocVars);

+      

+      IdentifierExprSeq! newModifies = new IdentifierExprSeq(impl.Proc.Modifies);

+      

+      bool inlined = false;

+      List<Block!>! newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);

+

+      if (!inlined) return;

+      

+      impl.InParams = newInParams;

+      impl.OutParams = newOutParams;

+      impl.LocVars = newLocalVars;

+      impl.Blocks = newBlocks;

+      impl.Proc.Modifies = newModifies;

+      

+      impl.ResetImplFormalMap();

+      

+      // we need to resolve the new code

+      inliner.ResolveImpl(program, impl);

+      

+      if(CommandLineOptions.Clo.PrintInlined) {

+        inliner.EmitImpl(impl);

+      }

+    }

+    

+    

+    public static void ProcessImplementation(Program! program, Implementation! impl)

+      requires impl.Proc != null;

+    {

+      ProcessImplementation(program, impl, null);

+    }

+    

+    protected void EmitImpl(Implementation! impl)

+      requires impl.Proc != null;

+    {

+      Console.WriteLine("after inlining procedure calls");

+      impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out), 0);

+      impl.Emit(new TokenTextWriter("<console>", Console.Out), 0);

+    }

+    

+    private sealed class DummyErrorSink : IErrorSink

+    {

+      public void Error(IToken! tok, string! msg) {

+        // FIXME 

+        // noop.

+        // This is required because during the resolution, some resolution errors happen

+        // (such as the ones caused addion of loop invariants J_(block.Label) by the AI package

+      }

+    }

+

+    protected void ResolveImpl(Program! program, Implementation! impl)

+      ensures impl.Proc != null;

+    {

+      ResolutionContext rc = new ResolutionContext(new DummyErrorSink());

+      

+      foreach(Declaration decl in program.TopLevelDeclarations) {

+        decl.Register(rc);

+      }

+      

+      impl.Proc = null; // to force Resolve() redo the operation

+      impl.Resolve(rc);

+      

+      TypecheckingContext tc = new TypecheckingContext(new DummyErrorSink());

+      

+      impl.Typecheck(tc);

+    }

+    

+    

+    // returns true if it is ok to further unroll the procedure

+    // otherwise, the procedure is not inlined at the call site

+    protected int GetInlineCount(Implementation! impl) {

+      string! procName = impl.Name;

+      int c;

+      if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {

+        return c;

+      }

+

+      c = -1; // TryGetValue above always overwrites c

+      impl.CheckIntAttribute("inline", ref c);

+      // procedure attribute overrides implementation

+      if (impl.Proc != null) {

+        impl.Proc.CheckIntAttribute("inline", ref c);

+      }

+      

+      recursiveProcUnrollMap[procName] = c;

+      return c;

+    }

+    

+    void CheckRecursion(Implementation! impl, Stack<Procedure!>! callStack) {

+      foreach (Procedure! p in callStack) {

+        if (p == impl.Proc) {

+          string msg = "";

+          foreach (Procedure! p in callStack) {

+            msg = p.Name + " -> " + msg;

+          }

+          msg += p.Name;

+          //checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg);

+        }

+      }

+    }

+    

+    private List<Block!>! DoInlineBlocks(Stack<Procedure!>! callStack, List<Block!>! blocks, Program! program, 

+                                         VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, ref bool inlinedSomething)

+    {

+      List<Block!>! newBlocks = new List<Block!>();

+

+      foreach(Block block in blocks) {      

+        TransferCmd! transferCmd = (!) block.TransferCmd;
+        CmdSeq cmds = block.Cmds;

+        CmdSeq newCmds = new CmdSeq();

+        Block newBlock;

+        string label = block.Label;

+        int lblCount = 0;

+        

+        for(int i = 0; i < cmds.Length; ++i) {

+          Cmd cmd = cmds[i];
+          CallCmd callCmd = cmd as CallCmd;

+          

+          if(callCmd == null) {

+            // if not call command, leave it as is

+            newCmds.Add(codeCopier.CopyCmd(cmd));
+          } else {

+            assert(callCmd.Proc != null);

+            Procedure proc = null;

+            Implementation impl = null;

+            string calleeName = callCmd.Proc.Name;

+            

+            int inline = -1;

+

+            // *** now we do not allow constructors to be inlined

+            if (!calleeName.Contains("..ctor")) {

+              // FIXME why on earth are we searching by name?!

+              bool implExists = FindProcImpl(program, calleeName, out proc, out impl);

+              assume(!implExists || (proc != null && impl != null));

+              if (implExists) {

+                inline = GetInlineCount((!)impl);

+              }

+            }            

+

+            assert(inline == -1  || impl != null);

+            

+            if (inline > 0) { // at least one block should exist

+              assume(impl != null && proc != null);

+              assert(((!)impl.OriginalBlocks).Count > 0);

+              inlinedSomething = true;

+              

+              // do inline now

+              int nextlblCount = lblCount + 1;

+              string nextBlockLabel = label + "$" + nextlblCount;

+              

+              // run the callback before each inline

+              if(inlineCallback != null) {

+                inlineCallback(impl);

+              }

+              

+              // increment the counter for the procedure to be used in constructing the locals and formals

+              NextInlinedProcLabel(proc.Name);

+              

+              BeginInline(newLocalVars, newModifies, proc, impl);

+              

+              List<Block!>! inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);

+              

+              EndInline();

+

+			  recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;

+              callStack.Push((!)impl.Proc);

+              inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);

+              callStack.Pop();

+              recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;

+              

+              Block! startBlock = inlinedBlocks[0];

+

+              GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new StringSeq(startBlock.Label));

+              newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, gotoCmd);

+              

+              newBlocks.Add(newBlock);

+              newBlocks.AddRange(inlinedBlocks);

+              

+              lblCount = nextlblCount;

+              newCmds = new CmdSeq();
+            } else if (inline == 0) {

+              inlinedSomething = true;

+              if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {

+                // add assert

+                newCmds.Add(new AssertCmd(callCmd.tok, Expr.False));

+              } else if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) {

+                // add assume

+                newCmds.Add(new AssumeCmd(callCmd.tok, Expr.False));

+              } else {

+                // add call

+                newCmds.Add(codeCopier.CopyCmd(callCmd));

+              }

+            } else {

+                newCmds.Add(codeCopier.CopyCmd(callCmd));

+            }         

+          }

+        }

+        

+        newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, codeCopier.CopyTransferCmd(transferCmd));

+        newBlocks.Add(newBlock);

+      }

+

+      return newBlocks;

+    }

+

+    protected List<Block!>! DoInline(List<Block!>! blocks, Program! program, VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, out bool inlined)

+    {

+      inlinedProcLblMap.Clear();

+      recursiveProcUnrollMap.Clear();

+    

+      inlined = false;

+      return DoInlineBlocks(new Stack<Procedure!>(), blocks, program, newLocalVars, newModifies, ref inlined);

+    }

+    

+    protected void BeginInline(VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, Procedure! proc, Implementation! impl) {

+      Hashtable substMap = new Hashtable();

+      

+      foreach(Variable! locVar in (!)impl.OriginalLocVars) {

+        LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, locVar.Name), locVar.TypedIdent.Type, locVar.TypedIdent.WhereExpr));

+        newLocalVars.Add(localVar);

+        IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);

+        substMap.Add(locVar, ie);

+      }

+      

+      for (int i = 0; i < impl.InParams.Length; i++) {

+        Variable inVar = (!) impl.InParams[i];

+        LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, inVar.Name), inVar.TypedIdent.Type, inVar.TypedIdent.WhereExpr));

+        newLocalVars.Add(localVar);

+        IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);

+        substMap.Add(inVar, ie);

+        // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration

+        Variable procInVar = (!)proc.InParams[i];

+        if (procInVar != inVar) {

+          substMap.Add(procInVar, ie);

+        }

+      }

+      

+      for (int i = 0; i < impl.OutParams.Length; i++) {

+        Variable outVar = (!) impl.OutParams[i];

+        LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr));

+        newLocalVars.Add(localVar);

+        IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);

+        substMap.Add(outVar, ie);

+        // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration

+        Variable procOutVar = (!)proc.OutParams[i];

+        if (procOutVar != outVar) {

+          substMap.Add(procOutVar, ie);

+        }

+      }

+      

+      Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();

+     

+      foreach (IdentifierExpr! mie in proc.Modifies) {

+        Variable! mVar = (!) mie.Decl;

+        LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, mVar.Name), mVar.TypedIdent.Type));

+        newLocalVars.Add(localVar);

+        IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);

+        substMapOld.Add(mVar, ie);

+        // FIXME why are we doing this? the modifies list should already include them.

+        // add the modified variable to the modifies list of the procedure

+        if(!newModifies.Has(mie)) {

+          newModifies.Add(mie);

+        }

+      }

+      

+      codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
+      codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
+    }

+    

+    protected void EndInline() {

+      codeCopier.Subst = null;

+      codeCopier.OldSubst = null;

+    }

+    

+   

+    // result[0] is the entry block

+    protected List<Block!>! CreateInlinedBlocks(CallCmd! callCmd, Procedure! proc, Implementation! impl, string! nextBlockLabel)

+      requires (codeCopier.Subst != null);

+      requires (codeCopier.OldSubst != null);

+    {

+      

+      List<Block!>! implBlocks = (!)impl.OriginalBlocks;

+      assert (implBlocks.Count > 0);

+      

+      string startLabel = implBlocks[0].Label;

+      

+      List<Block!>! inlinedBlocks = new List<Block!>();

+      

+      // create in block

+      CmdSeq inCmds = new CmdSeq();

+      

+      // assign in parameters

+      for(int i = 0; i < impl.InParams.Length; ++i) {

+        Cmd cmd = Cmd.SimpleAssign(impl.tok,

+                                   (IdentifierExpr) (!) codeCopier.Subst( (!)impl.InParams[i]),

+                                   (!)callCmd.Ins[i]);

+        inCmds.Add(cmd);

+      }

+      

+      // inject non-free requires

+      for (int i = 0; i < proc.Requires.Length; i++) {

+        Requires! req = (!) proc.Requires[i];

+        if (!req.Free) {

+          Requires! reqCopy = (Requires!) req.Clone();

+          reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

+          AssertCmd! a = new AssertRequiresCmd(callCmd, reqCopy);

+          a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;

+          inCmds.Add(a);

+        }

+      }

+

+      VariableSeq locVars = (!)impl.OriginalLocVars;
+      

+      // add where clauses of local vars as assume

+      for(int i = 0; i < locVars.Length; ++i) {

+        Expr whereExpr = ((!)locVars[i]).TypedIdent.WhereExpr;

+        if(whereExpr != null) {

+          whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);

+          // FIXME we cannot overwrite it, can we?!

+          ((!)locVars[i]).TypedIdent.WhereExpr = whereExpr;

+          AssumeCmd! a = new AssumeCmd(Token.NoToken, whereExpr);

+          inCmds.Add(a);

+        }

+      }

+      

+      // add where clauses of output params as assume

+      for(int i = 0; i < impl.OutParams.Length; ++i) {

+        Expr whereExpr = ((!)impl.OutParams[i]).TypedIdent.WhereExpr;

+        if(whereExpr != null) {

+          whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);

+          // FIXME likewise

+          ((!)impl.OutParams[i]).TypedIdent.WhereExpr = whereExpr;

+          AssumeCmd! a = new AssumeCmd(Token.NoToken, whereExpr);

+          inCmds.Add(a);

+        }

+      }

+      

+      // assign modifies old values

+      foreach (IdentifierExpr! mie in proc.Modifies)

+      {

+        Variable! mvar = (!) mie.Decl;

+        AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr) (!) codeCopier.OldSubst(mvar), mie);

+        inCmds.Add(assign);

+      }

+      

+      GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new StringSeq(GetInlinedProcLabel(proc.Name) + "$" + startLabel));

+      Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd);

+      inlinedBlocks.Add(inBlock);
+      

+      // inject the blocks of the implementation

+      Block intBlock;

+      foreach (Block block in implBlocks) {

+        CmdSeq copyCmds =  codeCopier.CopyCmdSeq(block.Cmds);

+        TransferCmd transferCmd = CreateInlinedTransferCmd((!) block.TransferCmd, GetInlinedProcLabel(proc.Name));

+        intBlock = new Block(block.tok, GetInlinedProcLabel(proc.Name) + "$" + block.Label, copyCmds, transferCmd);

+        inlinedBlocks.Add(intBlock);
+      }

+      

+      // create out block

+      CmdSeq outCmds = new CmdSeq();

+      

+      // inject non-free ensures

+      for (int i = 0; i < proc.Ensures.Length; i++) {

+        Ensures! ens = (!) proc.Ensures[i];

+        if (!ens.Free) {

+          Ensures! ensCopy = (Ensures!) ens.Clone();

+          ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

+          AssertCmd! a = new AssertEnsuresCmd(ensCopy);

+          outCmds.Add(a);

+        }

+      }

+      

+      // assign out params

+      for(int i = 0; i < impl.OutParams.Length; ++i) {

+        Expr! cout_exp = (IdentifierExpr) (!) codeCopier.Subst((!)impl.OutParams[i]);

+        Cmd cmd = Cmd.SimpleAssign(impl.tok, (!)callCmd.Outs[i], cout_exp);

+        outCmds.Add(cmd);

+      }

+      

+      // create out block

+      GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new StringSeq(nextBlockLabel));

+      Block outBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Return", outCmds, outGotoCmd);

+      inlinedBlocks.Add(outBlock);

+      

+      return inlinedBlocks;

+    }

+    

+    protected TransferCmd CreateInlinedTransferCmd(TransferCmd! transferCmd, string! procLabel) {

+      TransferCmd newTransferCmd;

+      

+      GotoCmd gotoCmd = transferCmd as GotoCmd;

+      if(gotoCmd != null) {

+        StringSeq gotoSeq = gotoCmd.labelNames;

+        StringSeq newGotoSeq = new StringSeq();

+        foreach(string! blockLabel in (!) gotoSeq) {

+          newGotoSeq.Add(procLabel + "$" + blockLabel);

+        }

+        newTransferCmd = new GotoCmd(transferCmd.tok, newGotoSeq);

+      } else {

+        newTransferCmd = new GotoCmd(transferCmd.tok, new StringSeq(procLabel + "$Return"));

+      }

+      

+      return newTransferCmd;

+    }

+    

+    protected static bool FindProcImpl(Program! program, string! procName, out Procedure outProc, out Implementation outImpl)

+    {   

+      // this assumes that there is at most one procedure and only one associated implementation in the current context

+      

+      foreach(Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if(impl != null) {

+          if(impl.Name.Equals(procName)) {

+            assert(impl.Proc != null);

+            outProc = impl.Proc;

+            outImpl = impl;

+            return true;

+          }

+        }

+      }

+      

+      foreach(Declaration decl in program.TopLevelDeclarations) {

+        Procedure proc = decl as Procedure;

+        if(proc != null) {

+          if(proc.Name.Equals(procName)) {

+            outProc = proc;

+            outImpl = null;

+            return false;

+          }

+        }

+      }

+      

+      outProc = null;

+      outImpl = null;

+      return false;

+    }

+  }

+  

+  ///////////////////////////////////////////////////////////////////////////////////////////////////////////////

+  

+  public class CodeCopier

+  {

+    public Substitution Subst;

+    public Substitution OldSubst;

+

+    public CodeCopier(Hashtable! substMap) {

+      Subst = Substituter.SubstitutionFromHashtable(substMap);

+    }

+    

+    public CodeCopier(Hashtable! substMap, Hashtable! oldSubstMap) {

+      Subst = Substituter.SubstitutionFromHashtable(substMap);

+      OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap);

+    }

+    

+    public CodeCopier() {

+    }

+    

+    public CmdSeq! CopyCmdSeq(CmdSeq! cmds) {

+      CmdSeq newCmds = new CmdSeq();

+      foreach (Cmd! cmd in cmds) {

+        newCmds.Add(CopyCmd(cmd));

+      }

+      return newCmds;

+    }

+    

+    public TransferCmd! CopyTransferCmd(TransferCmd! cmd) {

+      TransferCmd transferCmd;

+      GotoCmd gotocmd = cmd as GotoCmd;

+      if(gotocmd != null) {

+        assert(gotocmd.labelNames != null);

+        StringSeq labels = new StringSeq();

+        labels.AddRange(gotocmd.labelNames);

+        transferCmd = new GotoCmd(cmd.tok, labels);

+      } else {

+        transferCmd = new ReturnCmd(cmd.tok);

+      }

+      return transferCmd;

+    }

+    

+    public Cmd! CopyCmd(Cmd! cmd) {

+      if (Subst == null) {

+        return cmd;

+      } else if (OldSubst == null) {

+        return Substituter.Apply(Subst, cmd);

+      } else {

+        return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, cmd);

+      }

+    }

+    

+    public Expr! CopyExpr(Expr! expr) {

+      if (Subst == null) {

+        return expr;

+      } else if (OldSubst == null) {

+        return Substituter.Apply(Subst, expr);

+      } else {

+        return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, expr);

+      }

+    }

+  } // end class CodeCopier

+

+

+  public class AxiomExpander : Duplicator

+  {

+    readonly Program! program;

+    readonly TypecheckingContext! tc;

+

+    public AxiomExpander(Program! prog, TypecheckingContext! t)

+    {

+      program = prog;

+      tc = t;

+    }

+

+    public void CollectExpansions()

+    {

+      foreach (Declaration! decl in program.TopLevelDeclarations) {

+        Axiom ax = decl as Axiom;

+        if (ax != null) {

+          bool expand = false;

+          if (!ax.CheckBooleanAttribute("inline", ref expand)) {

+            Error(decl.tok, "{:inline ...} expects either true or false as the argument");

+          }

+          if (expand) {

+            AddExpansion(ax.Expr, ax.FindStringAttribute("ignore"));

+          }

+        }

+        Function f = decl as Function;

+        if (f != null && f.Body != null) {

+          Variable[]! formals = new Variable [f.InParams.Length];

+          for (int i = 0; i < formals.Length; ++i)

+            formals[i] = f.InParams[i];

+          AddExpansion(f, new Expansion(null, f.Body,

+                                        new TypeVariableSeq (f.TypeParameters),

+                                        formals));

+        }

+      }

+    }

+

+    void Error(IToken! tok, string msg)

+    {

+      tc.Error(tok, "expansion: " + msg);

+    }

+

+    void AddExpansion(Expr! axiomBody, string? ignore)

+    {

+      // it would be sooooooooo much easier with pattern matching

+      ForallExpr all = axiomBody as ForallExpr;

+      if (all != null) {

+        NAryExpr nary = all.Body as NAryExpr;

+        BinaryOperator bin = nary == null ? null : nary.Fun as BinaryOperator;

+        //System.Console.WriteLine("{0} {1} {2}", nary==null, bin==null, bin==null?0 : bin.Op);

+        if (nary != null && bin != null && (bin.Op == BinaryOperator.Opcode.Eq || bin.Op == BinaryOperator.Opcode.Iff)) {

+          NAryExpr? func = nary.Args[0] as NAryExpr;

+          //System.Console.WriteLine("{0} {1}", func == null, func == null ? null : func.Fun.GetType());

+          while (func != null && func.Fun is TypeCoercion)

+            func = func.Args[0] as NAryExpr;

+          if (func != null && func.Fun is FunctionCall) {

+            Function fn = (!)((FunctionCall)func.Fun).Func;

+            Expansion exp = new Expansion(ignore, (!)nary.Args[1],

+                                          new TypeVariableSeq (),

+                                          new Variable[func.Args.Length]);

+            int pos = 0;

+            Dictionary<Declaration, bool> parms = new Dictionary<Declaration, bool>();

+            foreach (Expr! e in func.Args) {

+              IdentifierExpr id = e as IdentifierExpr;

+              if (id == null) {

+                Error(e.tok, "only identifiers supported as function arguments");

+                return;

+              }

+              exp.formals[pos++] = id.Decl;

+              if (parms.ContainsKey(id.Decl)) {

+                Error(all.tok, "an identifier was used more than once");

+                return;

+              }

+              parms[id.Decl] = true;

+              if (!all.Dummies.Has(id.Decl)) {

+                Error(all.tok, "identifier was not quantified over");

+                return;

+              }

+            }

+            if (func.Args.Length != all.Dummies.Length) {

+              Error(all.tok, "more variables quantified over, than used in function");

+              return;

+            }

+

+            Dictionary<TypeVariable!, bool> typeVars = new Dictionary<TypeVariable!, bool>();

+            foreach (TypeVariable! v in ((!)func.TypeParameters).FormalTypeParams) {

+              if (!func.TypeParameters[v].IsVariable) {

+                Error(all.tok, "only identifiers supported as type parameters");

+                return;

+              }

+              TypeVariable! formal = func.TypeParameters[v].AsVariable;

+              exp.TypeParameters.Add(formal);

+              if (typeVars.ContainsKey(formal)) {

+                Error(all.tok, "an identifier was used more than once");

+                return;

+              }

+              typeVars[formal] = true;

+              if (!all.TypeParameters.Has(formal)) {

+                Error(all.tok, "identifier was not quantified over");

+                return;

+              }

+            }

+            if (((FunctionCall)func.Fun).Func.TypeParameters.Length != all.TypeParameters.Length) {

+              Error(all.tok, "more variables quantified over, than used in function");

+              return;

+            }

+            AddExpansion(fn, exp);

+            return;

+          }

+        }

+      }

+

+      Error(axiomBody.tok, "axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))");

+    }

+

+    void AddExpansion(Function! fn, Expansion! x) {

+      if (fn.expansions == null) {

+        fn.expansions = new List<Expansion!>();

+      }

+      fn.expansions.Add(x);

+    }

+  }

+} // end namespace

+