1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System.ComponentModel;
namespace Microsoft.Boogie
{
using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
public class AlphaEquality : IEqualityComparer<Expr>
{
private readonly DeBruijnRenamer deBruijn = new DeBruijnRenamer();
bool IEqualityComparer<Expr>.Equals(Expr x, Expr y) {
var nx = deBruijn.Rename(x);
var ny = deBruijn.Rename(y);
return BinderExpr.EqualWithAttributesAndTriggers(nx, ny);
}
int IEqualityComparer<Expr>.GetHashCode(Expr obj) {
return 0;
// Best we can do because GetHashCode for Expression don't respect its equality.
// When it does, we can instead use:
// return deBruijn.Rename(obj).GetHashCode();
}
// Renames expressions into deBruijn indicies, such as
// (lambda x : int :: x + a)
// into
// (lambda bv#0 : int :: bv#0 + fv#0)
// It does not handle type variables yet, but it could be added.
//
// This class could be made public, but it is not since the Rename method
// could then leak FreeVariables out of here.
private class DeBruijnRenamer : Duplicator
{
// Maps from index positions and types to new variables
private readonly TypeDict<BoundVariable> boundVars =
new TypeDict<BoundVariable>("bv", ti => new BoundVariable(Token.NoToken, ti));
private readonly TypeDict<FreeVariable> freeVars =
new TypeDict<FreeVariable>("fv", ti => new FreeVariable(ti));
// These three variables are reset at the beginning of every renaming
private int boundVarCount, freeVarCount;
private Dictionary<Variable, FreeVariable> freeVarMap;
// Cached, previous results
private readonly Dictionary<Expr, Expr> cache = new Dictionary<Expr, Expr>();
public Expr Rename(Expr e) {
Expr ne;
if (!cache.TryGetValue(e, out ne)) {
boundVarCount = 0;
freeVarCount = 0;
freeVarMap = new Dictionary<Variable, FreeVariable>();
ne = VisitExpr(e);
cache[e] = ne;
#if DEBUG_ALPHA_RENAMING
var wr = new TokenTextWriter("<console>", Console.Out, true);
Console.Write("nm( ");
e.Emit(wr);
Console.WriteLine(" )");
Console.Write(" = ");
ne.Emit(wr);
Console.WriteLine("");
Console.WriteLine("h = " + ne.GetHashCode());
#endif
}
return ne;
}
public override BinderExpr VisitBinderExpr(BinderExpr node) {
var subst = new Dictionary<Variable, Expr>();
var newBound = new List<Variable>();
foreach (var bv in node.Dummies) {
var bvNew = boundVars[boundVarCount++, bv.TypedIdent.Type];
newBound.Add(bvNew);
subst[bv] = new IdentifierExpr(Token.NoToken, bvNew);
}
node.Dummies = this.VisitVariableSeq(newBound);
node.Body = this.VisitExpr(Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), node.Body));
return node;
}
public override Variable VisitVariable(Variable node) {
FreeVariable fv;
var bv = node as BoundVariable;
if (boundVars.ContainsValue(bv)) {
return node;
} else if (freeVarMap.TryGetValue(node, out fv)) {
return fv;
} else {
return freeVarMap[node] = freeVars[freeVarCount++, node.TypedIdent.Type];
}
}
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
var ie = (IdentifierExpr) base.VisitIdentifierExpr(node);
// Need to fix up the name, since IdentifierExpr's equality also checks the name
ie.Name = ie.Decl.TypedIdent.Name;
return ie;
}
private class TypeDict<A>
{
private readonly Dictionary<Tuple<int, Type>, A> vars = new Dictionary<Tuple<int, Type>, A>();
private readonly string Prefix; // either "bv" or "fv"
private readonly Func<TypedIdent, A> Mk; // either new BoundVar or new FreeVar
public TypeDict(string prefix, Func<TypedIdent, A> mk) {
Prefix = prefix;
Mk = mk;
}
// For debugging purposes, we create unique names when types differ, but the index are the same.
private int created = 0;
// Make sure that this index and this type is always mapped to the same variable
public A this[int i, Type t] {
get {
A v;
if (!vars.TryGetValue(Tuple.Create(i, t), out v)) {
v = Mk(new TypedIdent(Token.NoToken, Prefix + i + "#" + created++, t));
vars[Tuple.Create(i, t)] = v;
}
return v;
}
}
public bool ContainsValue(A a) {
return vars.ContainsValue(a);
}
}
private class FreeVariable : Variable
{
public FreeVariable(TypedIdent ti) : base(Token.NoToken, ti) {}
public override bool IsMutable {
get { throw new cce.UnreachableException(); }
}
public override void Register(ResolutionContext rc) {
throw new cce.UnreachableException();
}
}
}
}
}
|
