fixes for splitFields option

2 files changed, 31 insertions, 93 deletions

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 9018884b..e023d300 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -109,15 +109,6 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

-    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

-    /// on its type based on the heap representation. I.e., the value of this

-    /// variable represents the value of the expression "typeof(type)".

-    /// </summary>

-    public override Bpl.Variable CreateTypeVariable(ITypeReference type) {

-      return null;

-    }

-

-    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -146,16 +137,6 @@ procedure {:inline 1} Alloc() returns (x: int)
           Bpl.Cmd.MapAssign(tok,

           new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), value);

     }

-

-    /// <summary>

-    /// Returns the BPL expression that corresponds to the value of the dynamic type

-    /// of the object represented by the expression <paramref name="o"/>.

-    /// </summary>

-    public override Bpl.Expr DynamicType(Bpl.Expr o) {

-      // $DymamicType(o)

-      return null;

-    }

-

   }

 

   /// <summary>

@@ -191,6 +172,9 @@ procedure {:inline 1} Alloc() returns (x: int)
       program = null;

       string prelude = this.InitialPreludeText + this.DelegateEncodingText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

+      if (b) {

+        this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());

+      }

       return b;

     }

 

@@ -235,15 +219,6 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

-    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

-    /// on its type based on the heap representation. I.e., the value of this

-    /// variable represents the value of the expression "typeof(type)".

-    /// </summary>

-    public override Bpl.Variable CreateTypeVariable(ITypeReference type) {

-      return null;

-    }

-

-    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -259,15 +234,6 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

-    /// Returns the BPL expression that corresponds to the value of the dynamic type

-    /// of the object represented by the expression <paramref name="o"/>.

-    /// </summary>

-    public override Bpl.Expr DynamicType(Bpl.Expr o) {

-      // $DymamicType(o)

-      return null;

-    }

-

-    /// <summary>

     /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>

     /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static

@@ -379,15 +345,6 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

-    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

-    /// on its type based on the heap representation. I.e., the value of this

-    /// variable represents the value of the expression "typeof(type)".

-    /// </summary>

-    public override Bpl.Variable CreateTypeVariable(ITypeReference type) {

-      return null;

-    }

-

-    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -451,15 +408,6 @@ procedure {:inline 1} Alloc() returns (x: int)
       }

     }

 

-    /// <summary>

-    /// Returns the BPL expression that corresponds to the value of the dynamic type

-    /// of the object represented by the expression <paramref name="o"/>.

-    /// </summary>

-    public override Bpl.Expr DynamicType(Bpl.Expr o) {

-      // $DymamicType(o)

-      return null;

-    }

-

   }

 

   /// <summary>

@@ -471,10 +419,6 @@ procedure {:inline 1} Alloc() returns (x: int)
 

     #region Fields

 

-    [RepresentationFor("Type", "type Type;")]

-    private Bpl.TypeCtorDecl TypeTypeDecl = null;

-    private Bpl.CtorType TypeType;

-

     [RepresentationFor("Field", "type Field;")]

     private Bpl.TypeCtorDecl FieldTypeDecl = null;

     private Bpl.CtorType FieldType;

@@ -500,9 +444,6 @@ procedure {:inline 1} Alloc() returns (x: int)
     [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:ref, f:Field, v:box): HeapType { H[o,f := v] }")]

     private Bpl.Function Write = null;

 

-    [RepresentationFor("$DynamicType", "function $DynamicType(ref): Type;")]

-    public Bpl.Function DymamicType = null;

-

     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

@@ -585,21 +526,6 @@ procedure {:inline 1} Alloc() returns (x: ref)
     }

 

     /// <summary>

-    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

-    /// on its type based on the heap representation. I.e., the value of this

-    /// variable represents the value of the expression "typeof(type)".

-    /// </summary>

-    public override Bpl.Variable CreateTypeVariable(ITypeReference type) {

-      Bpl.Variable v;

-      string typename = TypeHelper.GetTypeName(type);

-      Bpl.IToken tok = type.Token();

-      Bpl.Type t = this.TypeType;

-      Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, t);

-      v = new Bpl.Constant(tok, tident, true);

-      return v;

-    }

-

-    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -673,20 +599,6 @@ procedure {:inline 1} Alloc() returns (x: ref)
       }

     }

 

-    /// <summary>

-    /// Returns the BPL expression that corresponds to the value of the dynamic type

-    /// of the object represented by the expression <paramref name="o"/>.

-    /// </summary>

-    public override Bpl.Expr DynamicType(Bpl.Expr o) {

-      // $DymamicType(o)

-      var callDynamicType = new Bpl.NAryExpr(

-        o.tok,

-        new Bpl.FunctionCall(this.DymamicType),

-        new Bpl.ExprSeq(o)

-        );

-      return callDynamicType;

-    }

-

   }

 

   internal class RepresentationFor : Attribute {

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 482058e9..e0c4124f 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -71,11 +71,26 @@ namespace BytecodeTranslator {
   {

     public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);

 

+    [RepresentationFor("Type", "type Type;")]

+    protected Bpl.TypeCtorDecl TypeTypeDecl = null;

+    protected Bpl.CtorType TypeType;

+    

+    /// <summary>

     /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

     /// on its type based on the heap representation. I.e., the value of this

     /// variable represents the value of the expression "typeof(type)".

     /// </summary>

-    public abstract Bpl.Variable CreateTypeVariable(ITypeReference type);

+    public Bpl.Variable CreateTypeVariable(ITypeReference type)

+    {

+        Bpl.Variable v;

+        string typename = TypeHelper.GetTypeName(type);

+        Bpl.IToken tok = type.Token();

+        Bpl.Type t = this.TypeType;

+        Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, t);

+        tident.Type = this.TypeType;

+        v = new Bpl.Constant(tok, tident, true);

+        return v;

+    }

 

     public abstract Bpl.Variable CreateEventVariable(IEventDefinition e);

 

@@ -83,11 +98,22 @@ namespace BytecodeTranslator {
 

     public abstract Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr o, Bpl.IdentifierExpr f, Bpl.Expr value);

 

+    [RepresentationFor("$DynamicType", "function $DynamicType(ref): Type;")]

+    protected Bpl.Function DynamicTypeFunction = null;

+

     /// <summary>

     /// Returns the BPL expression that corresponds to the value of the dynamic type

     /// of the object represented by the expression <paramref name="o"/>.

     /// </summary>

-    public abstract Bpl.Expr DynamicType(Bpl.Expr o);

+    public Bpl.Expr DynamicType(Bpl.Expr o) {

+      // $DymamicType(o)

+      var callDynamicType = new Bpl.NAryExpr(

+        o.tok,

+        new Bpl.FunctionCall(this.DynamicTypeFunction),

+        new Bpl.ExprSeq(o)

+        );

+      return callDynamicType;

+    }

 

     protected readonly string DelegateEncodingText =

       @"procedure DelegateAdd(a: int, b: int) returns (c: int)