Allow polymorphic map types created using type constructors

Symbooglix cannot currently run this

// ######################################
// #         HEAP INITIALISATION        #
// ######################################
type Ref;
type Field a;
type Heap = <a> [Ref, Field a] a;

const unique null : Ref;
const unique alloc : Field bool;

var heap : Heap;

// ######################################    
// #          LOCAL VARIABLES           #
// ######################################

var this : Ref;
var time : Field int;
var value : Field int;
var error : Field bool;

// ######################################    
// #             SYMBOOGLIX             #
// ######################################

procedure main(i : int)
{
 var o : int;
 call o := getElapsedTime(i);
}

// ######################################    
// #              METHODS               #
// ######################################

procedure getElapsedTime(t : int) returns (r : int)
 ensures heap == old(heap);
{
 r := heap[this,time] - t;
}

This is not supported by the MapProxy and causes an exception to be raised when type checking

Symbooglix.ExprTypeCheckException: Type mismatch at index 1 expected type Field a but was type Field int
  at Symbooglix.MapProxy.TypeCheckIndices (IList`1 indices) <0x40c3b140 + 0x002c7> in <filename unknown>:0 
  at Symbooglix.MapProxy.ReadMapAt (IList`1 indices) <0x40c3af10 + 0x00037> in <filename unknown>:0 
  at Symbooglix.SimpleVariableStore.ReadMap (Microsoft.Boogie.Variable mapVariable, IList`1 indicies) <0x40c3ae00 + 0x00077> in <filename unknown>:0 
  at Symbooglix.ExecutionState.ReadMapVariableInScopeAt (Microsoft.Boogie.Variable v, IList`1 indices) <0x40c3acf0 + 0x00092> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003db> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0 
  at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c39760 + 0x000ec> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003f7> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) <0x40c38000 + 0x00884> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x40bd47f0 + 0x0053b> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x40bcff40 + 0x001c3> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb46b0 + 0x0059b> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb4040 + 0x0015f> in <filename unknown>:0 
Exiting with EXCEPTION_RAISED

boogie-org / symbooglix

Allow polymorphic map types created using type constructors #19