diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 28 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 1 |
2 files changed, 21 insertions, 8 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 500cb0ca..7ff0af6c 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -213,8 +213,8 @@ namespace Microsoft.Boogie { Emitter.Declarations(this.TopLevelDeclarations, stream);
}
- void CreateDatatypeSelectorsAndTesters() {
- Dictionary<string, Function> constructors = new Dictionary<string, Function>();
+ public void ProcessDatatypeConstructors() {
+ Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();
List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();
foreach (Declaration decl in TopLevelDeclarations) {
Function func = decl as Function;
@@ -223,17 +223,20 @@ namespace Microsoft.Boogie { continue;
}
if (constructors.ContainsKey(func.Name)) continue;
- constructors.Add(func.Name, func);
- prunedTopLevelDeclarations.Add(func);
+ DatatypeConstructor constructor = new DatatypeConstructor(func);
+ constructors.Add(func.Name, constructor);
+ prunedTopLevelDeclarations.Add(constructor);
}
TopLevelDeclarations = prunedTopLevelDeclarations;
-
- foreach (Function f in constructors.Values) {
+
+ foreach (DatatypeConstructor f in constructors.Values) {
for (int i = 0; i < f.InParams.Length; i++) {
DatatypeSelector selector = new DatatypeSelector(f, i);
+ f.selectors.Add(selector);
TopLevelDeclarations.Add(selector);
}
DatatypeMembership membership = new DatatypeMembership(f);
+ f.membership = membership;
TopLevelDeclarations.Add(membership);
}
}
@@ -256,8 +259,6 @@ namespace Microsoft.Boogie { //Contract.Requires(rc != null);
Helpers.ExtraTraceInformation("Starting resolution");
- CreateDatatypeSelectorsAndTesters();
-
foreach (Declaration d in TopLevelDeclarations) {
d.Register(rc);
}
@@ -1791,6 +1792,17 @@ namespace Microsoft.Boogie { }
}
+ public class DatatypeConstructor : Function {
+ public List<DatatypeSelector> selectors;
+ public DatatypeMembership membership;
+
+ public DatatypeConstructor(Function func)
+ : base(func.tok, func.Name, func.TypeParameters, func.InParams, func.OutParams[0], func.Comment, func.Attributes)
+ {
+ selectors = new List<DatatypeSelector>();
+ }
+ }
+
public class DatatypeSelector : Function {
public Function constructor;
public int index;
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 3602339e..fe77bcc1 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -85,6 +85,7 @@ Contract.Requires(cce.NonNullElements(defines,true)); if (parser.errors.count == 0)
{
program = Pgm;
+ program.ProcessDatatypeConstructors();
return 0;
}
else
|