//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Text;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using Microsoft.Contracts;
using Microsoft.Basetypes;

// A translator from the Boogie AST to the VCExpr AST.
// This was previously realised in the methods AbsyExpr.VCView

namespace Microsoft.Boogie.VCExprAST
{
  using Microsoft.Boogie;

  public class VCGenerationOptions {
    private readonly List<string!>! SupportedProverCommands;

    public bool IsProverCommandSupported(string! kind)
    {
      return SupportedProverCommands.Contains(kind);
    }

    public bool IsAnyProverCommandSupported(string! kinds)
    {
      if (kinds.IndexOf(',') < 0) {
        return IsProverCommandSupported(kinds);
      } else {
        return exists{string k in kinds.Split(',', ' '); IsProverCommandSupported(k)};
      }
    }

    public VCGenerationOptions(List<string!>! supportedProverCommands) {
      this.SupportedProverCommands = supportedProverCommands;
    }
  }

  public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
    // Stack on which the various Visit-methods put the result of the translation
    private readonly Stack<VCExpr!>! SubExpressions = new Stack<VCExpr!> ();

    private void Push(VCExpr! expr) {
      SubExpressions.Push(expr);
    }

    private VCExpr! Pop() {
      return SubExpressions.Pop();
    }

    public VCExpr! Translate(Expr! expr) {
      this.Visit(expr);
      return Pop();
    }

    public List<VCExpr!>! Translate(ExprSeq! exprs) {
      List<VCExpr!>! res = new List<VCExpr!> ();
      foreach(Expr e in exprs)
        res.Add(Translate((!)e));
      return res;
    }

    ///////////////////////////////////////////////////////////////////////////////

    internal readonly VCExpressionGenerator! Gen;

    public Boogie2VCExprTranslator(VCExpressionGenerator! gen,
                                   VCGenerationOptions! genOptions) {
      this.Gen = gen;
      this.GenerationOptions = genOptions;
      UnboundVariables = new VariableMapping<Variable> ();
      BoundVariables = new VariableMapping<BoundVariable> ();
      Formals = new VariableMapping<Formal> ();
    }

    private Boogie2VCExprTranslator(Boogie2VCExprTranslator! tl) {
      this.Gen = tl.Gen;
      this.GenerationOptions = tl.GenerationOptions;
      UnboundVariables =
        (VariableMapping<Variable>)tl.UnboundVariables.Clone();
      BoundVariables = new VariableMapping<BoundVariable> ();
      Formals = new VariableMapping<Formal> ();
    }

    public object! Clone() {
      return new Boogie2VCExprTranslator(this);
    }

    private IAppliableTranslator IAppTranslatorAttr = null;
    private IAppliableTranslator! IAppTranslator { get {
      if (IAppTranslatorAttr == null)
        IAppTranslatorAttr = new IAppliableTranslator (this);
      return IAppTranslatorAttr;
    } }

    ///////////////////////////////////////////////////////////////////////////////
    // Class for handling occurring variables

    private class VariableMapping<VarKind> : ICloneable {
      private readonly List<Dictionary<VarKind!, VCExprVar!>!>! Mapping;

      public VariableMapping() {
        List<Dictionary<VarKind!, VCExprVar!>!>! mapping =
          new List<Dictionary<VarKind!, VCExprVar!>!> ();
        mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());
        this.Mapping = mapping;
      }

      private VariableMapping(VariableMapping<VarKind>! vm) {
        List<Dictionary<VarKind!, VCExprVar!>!>! mapping =
          new List<Dictionary<VarKind!, VCExprVar!>!> ();
        foreach (Dictionary<VarKind!, VCExprVar!>! d in vm.Mapping)
          mapping.Add(new Dictionary<VarKind!, VCExprVar!> (d));
        this.Mapping = mapping;
      }
      
      public object! Clone() {
        return new VariableMapping<VarKind> (this);
      }

      public void PushScope() {
        Mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());        
      }

      public void PopScope() {
        assume Mapping.Count > 0; 
        Mapping.RemoveAt(Mapping.Count - 1);
      }
      
      public void Bind(VarKind! boogieVar, VCExprVar! vcExprVar)
        requires !Contains(boogieVar); {
        Mapping[Mapping.Count - 1].Add(boogieVar, vcExprVar);
      }
      
      public VCExprVar! Lookup(VarKind! boogieVar) {
        VCExprVar res = LookupHelp(boogieVar);
        assume res != null;
        return res;
      }

      [Pure]
      public bool Contains(VarKind! boogieVar) {
        return LookupHelp(boogieVar) != null;
      }

      public bool TryGetValue(VarKind! boogieVar, out VCExprVar res) {
        res = LookupHelp(boogieVar);
        return res != null;
      }

      [Pure]
      private VCExprVar LookupHelp(VarKind! boogieVar) {
        VCExprVar res;
        foreach (Dictionary<VarKind!, VCExprVar!>! d in Mapping) {
          if (d.TryGetValue(boogieVar, out res))
            return res;
        }
        return null;
      }
    }

    //////////////////////////////////////////////////////////////////////////////////

    private readonly VariableMapping<Variable>! UnboundVariables;
    private readonly VariableMapping<BoundVariable>! BoundVariables;
    // used when translating the bodies of function expansions
    private readonly VariableMapping<Formal>! Formals;

    internal void PushBoundVariableScope() {
      BoundVariables.PushScope();
    }
    internal void PopBoundVariableScope() {
      BoundVariables.PopScope();
    }

    internal void PushFormalsScope() {
      Formals.PushScope();
    }
    internal void PopFormalsScope() {
      Formals.PopScope();
    }

    public VCExprVar! BindVariable(Variable! boogieVar) {
      if (boogieVar is BoundVariable) {
        VCExprVar! newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
        BoundVariables.Bind((BoundVariable)boogieVar, newVar);
        return newVar;
      } else if (boogieVar is Formal) {
        VCExprVar! newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
        Formals.Bind((Formal)boogieVar, newVar);
        return newVar;
      } else {
        // only bound variables and formals are declared explicitly
        assert false;
      }
    }

    public VCExprVar! LookupVariable(Variable! boogieVar) {
    
      BoundVariable bv = boogieVar as BoundVariable;
      if (bv != null) {
        return BoundVariables.Lookup(bv);
      }
      VCExprVar res;
      Formal fml = boogieVar as Formal;
      if (fml != null && Formals.TryGetValue(fml, out res))
        return (!)res;

      // global variables, local variables, incarnations, etc. are
      // bound the first time they occur
      if (!UnboundVariables.TryGetValue(boogieVar, out res)) {
        res = new VCExprVar (boogieVar.Name, boogieVar.TypedIdent.Type);
        UnboundVariables.Bind(boogieVar, res);
      }
      return (!)res;
    }

    ///////////////////////////////////////////////////////////////////////////////////
    
    internal readonly VCGenerationOptions! GenerationOptions;

    ///////////////////////////////////////////////////////////////////////////////////

    public override LiteralExpr! VisitLiteralExpr(LiteralExpr! node) {
      Push(TranslateLiteralExpr(node));
      return node;
    }
    private VCExpr! TranslateLiteralExpr(LiteralExpr! node) {
      if ( node.Val is bool )
      {
        bool b = (bool) node.Val;
        if ( b ) {
          return VCExpressionGenerator.True;
        } else {
          return VCExpressionGenerator.False;
        }
      }
      else if ( node.Val is BigNum )
      {
        return Gen.Integer(node.asBigNum);
      }
      else if ( node.Val is BvConst )
      {
        return Gen.Bitvector((BvConst)node.Val);
      }
      else
      {
        System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
        assert false;
      }
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)
    {
      assert false;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {
      assume node.Decl != null;   // the expression has to be resolved
      Push(LookupVariable(node.Decl));
      return node; 
    }

    ///////////////////////////////////////////////////////////////////////////////////

    // Because of our scheme for numbering incarnations of variables, the pre-state
    // value of a variable x is always just "x". (The first update to it in a method
    // causes it to become "x0". So we just remove old expressions with a visitor
    // before transforming it into a VCExpr.
    public override Expr! VisitOldExpr(OldExpr! node)
    {
      assert false;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr! VisitNAryExpr(NAryExpr! node)
    {
      Push(TranslateNAryExpr(node));
      return node;
    }

    private VCExpr! TranslateNAryExpr(NAryExpr! node) {
      int n = node.Args.Length;
      List<VCExpr!>! vcs = new List<VCExpr!> (n);
      for(int i = 0; i < n; i++)
      {
        vcs.Add(Translate((!)node.Args[i]));
      }

      if (node.Type == null) {
        System.Console.WriteLine("*** type is null for {0}", node);
        assert false;
      }

      return IAppTranslator.Translate(node.Fun, node.Type, vcs,
                                      ToList((!)node.TypeParameters));
    }
   

    private static List<Type!>! EMPTY_TYPE_LIST = new List<Type!> ();

    private List<Type!>! ToList(TypeParamInstantiation! insts) {
      if (insts.FormalTypeParams.Count == 0)
        return EMPTY_TYPE_LIST;

      List<Type!>! typeArgs = new List<Type!> ();
      foreach (TypeVariable! var in insts.FormalTypeParams)
        typeArgs.Add(insts[var]);
      return typeArgs;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node) {
      Push(TranslateQuantifierExpr(node));
      return node;
    }

    public override ExistsExpr! VisitExistsExpr(ExistsExpr! node)
    {
      node = (ExistsExpr) this.VisitQuantifierExpr(node);
      return node; 
    }

    public override ForallExpr! VisitForallExpr(ForallExpr! node)
    {
      node = (ForallExpr) this.VisitQuantifierExpr(node);
      return node; 
    }

    private VCExpr! TranslateQuantifierExpr(QuantifierExpr! node)
    {
      List<TypeVariable!>! typeParams = new List<TypeVariable!> ();
      foreach (TypeVariable! v in node.TypeParameters)
        typeParams.Add(v);

      PushBoundVariableScope();

      List<VCExprVar!>! boundVars = new List<VCExprVar!> ();
      foreach (Variable! v in node.Dummies)
        boundVars.Add(BindVariable(v));

      try {
        List<VCTrigger!>! triggers = TranslateTriggers(node.Triggers);
        VCExpr! body = Translate(node.Body);
        VCQuantifierInfos! infos = GenerateQuantifierInfos(node);

        Quantifier quan;
        if (node is ForallExpr)
          quan = Quantifier.ALL;
        else if (node is ExistsExpr)
          quan = Quantifier.EX;
        else
          assert false;

        return Gen.Quantify(quan, typeParams, boundVars, triggers, infos, body);
      } finally {
        PopBoundVariableScope();
      }
    }

    private List<VCTrigger!>! TranslateTriggers(Trigger node)
    {
      List<VCTrigger!>! res = new List<VCTrigger!> ();
      Trigger curTrigger = node;
      while (curTrigger != null) {
        res.Add(Gen.Trigger(curTrigger.Pos, Translate(curTrigger.Tr)));
        curTrigger = curTrigger.Next;
      }
      return res;
    }

    private VCQuantifierInfos! GenerateQuantifierInfos(QuantifierExpr! node) {
      string qid = getQidNameFromQKeyValue(node.Dummies, node.Attributes);
      return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes);
    }

    private string getQidNameFromQKeyValue(VariableSeq! vars, QKeyValue attributes) {
      // Check for a 'qid, name' pair in keyvalues
      string qid = QKeyValue.FindStringAttribute(attributes, "qid");
      if (qid == null && vars.Length != 0){
        // generate default name (line:column position in .bpl file)
        Variable v = vars[0];
        assert v != null; // Rustan's claim!
        // Include the first 8 characters of the filename in QID (helpful in case we use /concat)
        // We limit it to 8, so the SX file doesn't grow too big, and who on earth would need
        // more than 8 characters in a filename anyways.
        int max = 8;
        StringBuilder buf = new StringBuilder(max + 20);
        string filename = v.tok.filename;
        if (filename == null) filename = "unknown";
        for (int i = 0; i < filename.Length; ++i) {
          if (filename[i] == '/' || filename[i] == '\\') buf.Length = 0;
          if (buf.Length < max && char.IsLetterOrDigit(filename[i])) {
            if (buf.Length == 0 && char.IsDigit(filename[i])) {
              // Z3 does not like QID's to start with a digit, so we prepend another character
              buf.Append('_');
            }
            buf.Append(filename[i]);
          }
        }
        buf.Append('.').Append(v.Line).Append(':').Append(v.Col);
        qid = buf.ToString();
      }
      return qid;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
    {
      Push(TranslateBvExtractExpr(node));
      return node;
    }

    private VCExpr! TranslateBvExtractExpr(BvExtractExpr! node)
      requires node.Start <= node.End; {
      VCExpr! bv = Translate(node.Bitvector);
      return Gen.BvExtract(bv, ((!)node.Bitvector.Type).BvBits, node.Start, node.End);
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)
    {
      Push(TranslateBvConcatExpr(node));
      return node;
    }

    private VCExpr! TranslateBvConcatExpr(BvConcatExpr! node) {
      VCExpr! bv0 = Translate(node.E0);
      VCExpr! bv1 = Translate(node.E1);
      return Gen.BvConcat(bv0, bv1);
    }

    ///////////////////////////////////////////////////////////////////////////////////
    // all the other cases should never happen

    public override Cmd! VisitAssertCmd(AssertCmd! node)
    {
      assert false;
    }
    public override Cmd! VisitAssignCmd(AssignCmd! node)
    {
      assert false;
    }
    public override Cmd! VisitAssumeCmd(AssumeCmd! node)
    {
      assert false;
    }
    public override AtomicRE! VisitAtomicRE(AtomicRE! node)
    {
      assert false;
    }
    public override Axiom! VisitAxiom(Axiom! node)
    {
      assert false;
    }
    public override Type! VisitBasicType(BasicType! node)
    {
      assert false;
    }
    public override Type! VisitBvType(BvType! node)
    {
      assert false;
    }
    public override Block! VisitBlock(Block! node)
    {
      assert false;
    }
    public override Expr! VisitBlockExpr(BlockExpr! node)
    {
      assert false;
    }
    public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
    {
      assert false;
    }
    public override List<Block!>! VisitBlockList(List<Block!>! blocks)
    {
      assert false;
    }
    public override BoundVariable! VisitBoundVariable(BoundVariable! node)
    {
      assert false;
    }
    public override Cmd! VisitCallCmd(CallCmd! node)
    {
      assert false;
    }
    public override Cmd! VisitCallForallCmd(CallForallCmd! node)
    {
      assert false;
    }
    public override CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)
    {
      assert false;
    }
    public override Choice! VisitChoice(Choice! node)
    {
      assert false;
    }
    public override Cmd! VisitCommentCmd(CommentCmd! node)
    {
      assert false;
    }
    public override Constant! VisitConstant(Constant! node)
    {
      assert false;
    }
    public override CtorType! VisitCtorType(CtorType! node)
    {
      assert false;
    }
    public override Declaration! VisitDeclaration(Declaration! node)
    {
      assert false;
    }
    public override List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)
    {
      assert false;
    }
    public override DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)
    {
      assert false;
    }
    public override Requires! VisitRequires(Requires! @requires)
    {
      assert false;
    }
    public override RequiresSeq! VisitRequiresSeq(RequiresSeq! requiresSeq)
    {
      assert false;
    }
    public override Ensures! VisitEnsures(Ensures! @ensures)
    {
      assert false;
    }
    public override EnsuresSeq! VisitEnsuresSeq(EnsuresSeq! ensuresSeq)
    {
      assert false;
    }
    public override Formal! VisitFormal(Formal! node)
    {
      assert false;
    }
    public override Function! VisitFunction(Function! node)
    {
      assert false;
    }
    public override GlobalVariable! VisitGlobalVariable(GlobalVariable! node)
    {
      assert false;
    }
    public override GotoCmd! VisitGotoCmd(GotoCmd! node)
    {
      assert false;
    }
    public override Cmd! VisitHavocCmd(HavocCmd! node)
    {
      assert false;
    }
    public override Implementation! VisitImplementation(Implementation! node)
    {
      assert false;
    }
    public override LocalVariable! VisitLocalVariable(LocalVariable! node)
    {
      assert false;
    }
    public override AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
    {
      assert false;
    }
    public override MapType! VisitMapType(MapType! node)
    {
      assert false;
    }
    public override Procedure! VisitProcedure(Procedure! node)
    {
      assert false;
    }
    public override Program! VisitProgram(Program! node)
    {
      assert false;
    }
    public override Cmd! VisitRE(RE! node)
    {
      assert false;
    }
    public override RESeq! VisitRESeq(RESeq! reSeq)
    {
      assert false;
    }
    public override ReturnCmd! VisitReturnCmd(ReturnCmd! node)
    {
      assert false;
    }
    public override ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
    {
      assert false;
    }
    public override Sequential! VisitSequential(Sequential! node)
    {
      assert false;
    }
    public override AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)
    {
      assert false;
    }
    public override Cmd! VisitStateCmd(StateCmd! node)
    {
      assert false;
    }
    public override TransferCmd! VisitTransferCmd(TransferCmd! node)
    {
      assert false;
    }
    public override Trigger! VisitTrigger(Trigger! node)
    {
      assert false;
    }
    public override Type! VisitType(Type! node)
    {
      assert false;
    }
    public override TypedIdent! VisitTypedIdent(TypedIdent! node)
    {
      assert false;
    }
    public override Type! VisitTypeSynonymAnnotation(TypeSynonymAnnotation! node)
    {
      assert false;
    }
    public override Type! VisitTypeVariable(TypeVariable! node)
    {
      assert false;
    }
    public override Variable! VisitVariable(Variable! node)
    {
      assert false;
    }
    public override VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)
    {
      assert false;
    }    
    public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
    {
      assert false;
    }    
    public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
    {
      assert false;
    }

  }


  /////////////////////////////////////////////////////////////////////////////////

  public class IAppliableTranslator : IAppliableVisitor<VCExpr!> {

    private readonly Boogie2VCExprTranslator! BaseTranslator;

    private VCExpressionGenerator! Gen { get {
      return BaseTranslator.Gen;
    } }
    private VCGenerationOptions! GenerationOptions { get {
      return BaseTranslator.GenerationOptions;
    } }

    public IAppliableTranslator(Boogie2VCExprTranslator! baseTranslator) {
      this.BaseTranslator = baseTranslator;
    }

    ///////////////////////////////////////////////////////////////////////////////

    private List<VCExpr!>! args = new List<VCExpr!>();
    private List<Type!>! typeArgs = new List<Type!>();

    public VCExpr! Translate(IAppliable! app, Type! ty, List<VCExpr!>! args, List<Type!>! typeArgs) {
    
      List<VCExpr!>! oldArgs = this.args;
      List<Type!>! oldTypeArgs = this.typeArgs;
      this.args = args;
      this.typeArgs = typeArgs;
      VCExpr! result = app.Dispatch<VCExpr!>(this);
      this.args = oldArgs;
      this.typeArgs = oldTypeArgs;
      return result;
    }

    ///////////////////////////////////////////////////////////////////////////////


    
    public VCExpr! Visit(UnaryOperator! unaryOperator) {
      assert unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1;
      return Gen.Not(this.args);
    }

    public VCExpr! Visit(BinaryOperator! binaryOperator) {
      return TranslateBinaryOperator(binaryOperator, this.args);
    }
    
    public VCExpr! Visit(FunctionCall! functionCall) {
      return TranslateFunctionCall(functionCall, this.args, this.typeArgs);
    }
    
    public VCExpr! Visit(MapSelect! mapSelect) {
      return Gen.Select(this.args, this.typeArgs);
    }
    
    public VCExpr! Visit(MapStore! mapStore) {
      return Gen.Store(this.args, this.typeArgs);
    }
    
    public VCExpr! Visit(TypeCoercion! typeCoercion) {
      assert this.args.Count == 1;
      return this.args[0];
    }

    public VCExpr! Visit(IfThenElse! ite) {
      return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
    }

    ///////////////////////////////////////////////////////////////////////////////

    private VCExpr! TranslateBinaryOperator(BinaryOperator! app, List<VCExpr!>! args) {
      assert args.Count == 2;

      switch (app.Op) {
        case BinaryOperator.Opcode.Add:
          return Gen.Function(VCExpressionGenerator.AddOp, args);
        case BinaryOperator.Opcode.Sub:
          return Gen.Function(VCExpressionGenerator.SubOp, args);
        case BinaryOperator.Opcode.Mul:
          return Gen.Function(VCExpressionGenerator.MulOp, args);
        case BinaryOperator.Opcode.Div:
          return Gen.Function(VCExpressionGenerator.DivOp, args);
        case BinaryOperator.Opcode.Mod:
          return Gen.Function(VCExpressionGenerator.ModOp, args);
        case BinaryOperator.Opcode.Eq:
        case BinaryOperator.Opcode.Iff:
          // we don't distinguish between equality and equivalence at this point
          return Gen.Function(VCExpressionGenerator.EqOp, args);
        case BinaryOperator.Opcode.Neq:
          return Gen.Function(VCExpressionGenerator.NeqOp, args);
        case BinaryOperator.Opcode.Lt:
          return Gen.Function(VCExpressionGenerator.LtOp, args);
        case BinaryOperator.Opcode.Le:
          return Gen.Function(VCExpressionGenerator.LeOp, args);
        case BinaryOperator.Opcode.Ge:
          return Gen.Function(VCExpressionGenerator.GeOp, args);
        case BinaryOperator.Opcode.Gt:
          return Gen.Function(VCExpressionGenerator.GtOp, args);
        case BinaryOperator.Opcode.Imp:
          return Gen.Function(VCExpressionGenerator.ImpliesOp, args);
        case BinaryOperator.Opcode.And:
          return Gen.Function(VCExpressionGenerator.AndOp, args);
        case BinaryOperator.Opcode.Or:
          return Gen.Function(VCExpressionGenerator.OrOp, args);
        case BinaryOperator.Opcode.Subtype:
          return Gen.Function(VCExpressionGenerator.SubtypeOp, args);
        default:
          assert false;  // unexpected binary operator
      }
    }

    ///////////////////////////////////////////////////////////////////////////////

    private VCExpr! TranslateFunctionCall(FunctionCall! app,
                                          List<VCExpr!>! args, List<Type!>! typeArgs) {
      assert app.Func != null;    // resolution must have happened

      VCExpr res = ApplyExpansion(app, args, typeArgs);
      if (res != null)
        return res;

      VCExprOp! functionOp = Gen.BoogieFunctionOp(app.Func);
      return Gen.Function(functionOp, args, typeArgs);
    }

    private VCExpr ApplyExpansion(FunctionCall! app,
                                  List<VCExpr!>! args, List<Type!>! typeArgs) {
      assert app.Func != null;    // resolution must have happened

      if (app.Func.doingExpansion) {
        System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
        return null;
      }

      Expansion exp = FindExpansion(app.Func);
      if (exp == null)
        return null;

      VCExpr! translatedBody;
      VCExprSubstitution! subst = new VCExprSubstitution();
      try {
        BaseTranslator.PushFormalsScope();
        BaseTranslator.PushBoundVariableScope();
        app.Func.doingExpansion = true;

        // first bind the formals to VCExpr variables, which are later
        // substituted with the actual parameters
        for (int i = 0; i < exp.formals.Length; ++i)
          subst[BaseTranslator.BindVariable((!)exp.formals[i])] = args[i];

        // recursively translate the body of the expansion
        translatedBody = BaseTranslator.Translate(exp.body);
      } finally {
        BaseTranslator.PopFormalsScope();
        BaseTranslator.PopBoundVariableScope();
        app.Func.doingExpansion = false;
      }

      // substitute the formals with the actual parameters in the body
      assert typeArgs.Count == exp.TypeParameters.Length;
      for (int i = 0; i < typeArgs.Count; ++i)
        subst[exp.TypeParameters[i]] = typeArgs[i];
      SubstitutingVCExprVisitor! substituter = new SubstitutingVCExprVisitor (Gen);
      return substituter.Mutate(translatedBody, subst);
    }

    private Expansion? FindExpansion(Function! func)
    {
      if (func.expansions == null) return null;

      Expansion? exp = null;
      foreach (Expansion! e in func.expansions) {
        if (e.ignore == null || !GenerationOptions.IsAnyProverCommandSupported(e.ignore)) {
          if (exp == null) {
            exp = e;
          } else {
            System.Console.WriteLine("*** more than one possible expansion for {0}", func);
            return null;
          }
        }
      }

      return exp;
    }
  }
}