path: root/Source/Core/Inline.ssc

//-----------------------------------------------------------------------------
//
// 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;
    private TypecheckingContext! checkingCtx;
  
    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(TypecheckingContext! ctx, InlineCallback cb) {        
      inlinedProcLblMap = new Dictionary<string!,int>();
      recursiveProcUnrollMap = new Dictionary<string!,int>();
      codeCopier = new CodeCopier();
      inlineCallback = cb;
      checkingCtx = ctx;
    }
    
    public static void ProcessImplementation(TypecheckingContext! ctx, Program! program, Implementation! impl, InlineCallback cb)
      requires impl.Proc != null;
    {
      Inliner inliner = new Inliner(ctx, 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(TypecheckingContext! ctx, Program! program, Implementation! impl)
      requires impl.Proc != null;
    {
      
      ProcessImplementation(ctx, 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 = -1;
      if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
        return c;
      }
      
      bool findattr = false;      
      
      QKeyValue kv = null;
      // try proc attributes
      if(impl.Proc != null) {
        kv = impl.Proc.Attributes;
        while(kv != null) {
          if(kv.Key.Equals("inline")) {
            findattr = true;
            break;
          }
          kv = kv.Next;     
        }
      }     
      // try impl attributes
      if(!findattr) {
        kv = impl.Attributes;
        while(kv != null) {
          if(kv.Key.Equals("inline")) {
            findattr = true;  
            break;
          }
          kv = kv.Next;     
        }
      }
      
      if (findattr) {
        assert(kv != null && kv.Key.Equals("inline"));
        if (kv.Params.Count == 1) {
          LiteralExpr lit = kv.Params[0] as LiteralExpr;
          if (lit != null && lit.isBigNum)
            c = lit.asBigNum.ToIntSafe;
        }
      }
      
      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