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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
use crate::{
Binder1,
BinderN,
Comp,
IGen,
MatchArm,
Pattern,
Val,
Ident,
VType,
};
impl Binder1 {
fn rename_r(self, igen: &mut IGen) -> Self {
match self {
Self::Eq(pos, vs1, vs2) => Self::Eq(
pos,
vs1.into_iter().map(|v| v.rename_r(igen)).collect(),
vs2.into_iter().map(|v| v.rename_r(igen)).collect(),
),
Self::LogOp1(b, v) => Self::LogOp1(b, v.rename_r(igen)),
Self::LogOpN(op, vs) => {
let vs2 = vs
.into_iter()
.map(|v| v.rename_r(igen))
.collect();
Self::LogOpN(op, vs2)
}
Self::LogQuantifier(q, xs, m) => {
// Start with xs = [(x1,s1), (x2,s2), ...]
// Create ys = [y1, y2, ...]
let ys: Vec<Ident> = igen.next_many(xs.len());
// Then subs = [(x1, Var(y1)), (x2, Var(y2)), ...]
let subs: Vec<(Ident,Val)> = xs
.iter()
.zip(&ys)
.map(|((x,_),y)| (x.clone(), y.clone().val()))
.collect();
// And new_sig = [(y1,s1), (y2,s2), ...]
let new_sig: Vec<(Ident,VType)> = xs
.into_iter()
.zip(ys)
.map(|((_,s),y)| (y, s))
.collect();
Self::LogQuantifier(q, new_sig, Box::new(
m.rename_r(igen).substitute_many(&subs)
))
}
Self::QMode(q, m) => {
Self::QMode(q, Box::new(m.rename_r(igen)))
}
}
}
}
impl BinderN {
fn rename_r(self, igen: &mut IGen) -> Self {
match self {
Self::Call(..) => todo!(),
Self::Seq(mut m) => {
m.content = Box::new(m.content.rename_r(igen));
Self::Seq(m)
}
}
}
}
impl Comp {
/// Replace all variables in a comp with unique auto-generated
/// variables, using the given IGen. The given IGen will
/// be advanced to cover the new names.
pub fn rename(self, igen: &mut IGen) -> Self {
self.advance_igen(igen);
self.rename_r(igen)
}
pub fn rename_r(self, igen: &mut IGen) -> Self {
match self {
Self::Apply(mut e) => {
e.f = Box::new(e.f.rename_r(igen));
e.vals = e.vals.into_iter()
.map(|v| v.rename_r(igen))
.collect();
Self::Apply(e)
}
Self::Return(vs) => {
let vs2 = vs
.into_iter()
.map(|v| v.rename_r(igen))
.collect();
Self::Return(vs2)
}
Self::Bind1(b,x,m) => {
// Rename any vars introduced within the binder.
let b2 = b.rename_r(igen);
// Create a fresh replacement for the bound variable.
let x2 = igen.next();
let m2 = m
// Rename any vars introduced in the sub-comp.
.rename_r(igen)
// Substitute the replacement into the sub-comp.
.substitute(&x, &x2.clone().val());
Self::Bind1(b2,x2,Box::new(m2))
}
Self::BindN(b,ps,m) => {
// Rename any vars introduced within the binder.
let b2 = b.rename_r(igen);
// Create a renamed pattern, and collect all
// substitutions that occured.
let mut ps2 = Vec::new();
let mut subs = Vec::new();
for p in ps {
let (p2, mut ss) = p.rename_r(igen);
ps2.push(p2);
subs.append(&mut ss);
}
let m2 = m
// Rename any vars introduced in the sub-comp.
.rename_r(igen)
// Substitute the replacements into the sub-comp.
.substitute_many(&subs);
Self::BindN(b2, ps2, Box::new(m2))
}
Self::Force(v) => Self::Force(v.rename_r(igen)),
Self::Fun(names, m) => {
let mut new_m = m.rename_r(igen);
let mut new_names = Vec::new();
for (name,t) in names {
let new_name = igen.next();
new_m = new_m.substitute(&name, &new_name.clone().val());
new_names.push((new_name,t));
}
Self::Fun(new_names, Box::new(new_m))
}
Self::Ite(cond, then_b, else_b) => {
Self::ite(
cond.rename_r(igen),
then_b.rename_r(igen),
else_b.rename_r(igen),
)
}
Self::Match(target, arms) => {
let target = target.rename_r(igen);
let arms = arms
.into_iter()
.map(|(a,m)| {
let MatchArm{code, binders} = a;
let mut subs = Vec::new();
// Replace each pattern in 'a', and collect
// the subs that have occured.
let mut binders2 = Vec::new();
for p in binders {
let (p2, mut ss) = p.rename_r(igen);
binders2.push(p2);
subs.append(&mut ss);
}
let m = m
.rename_r(igen)
.substitute_many(&subs);
(MatchArm{code, binders: binders2}, Box::new(m))
})
.collect();
Self::Match(target, arms)
}
}
}
}
impl Pattern {
fn rename_r(self, igen: &mut IGen) -> (Self, Vec<(Ident,Val)>) {
match self {
Self::NoBind => (Self::NoBind, Vec::new()),
Self::Atom(x) => {
let y = igen.next();
(Self::Atom(y.clone()), vec![(x,y.val())])
}
Self::Tuple(ps) => {
let mut ps2 = Vec::new();
let mut ss = Vec::new();
for p in ps.into_iter() {
let (p2, mut ss_p) = p.rename_r(igen);
ps2.push(p2);
ss.append(&mut ss_p);
}
(Self::Tuple(ps2), ss)
}
}
}
}
impl Val {
fn rename_r(self, igen: &mut IGen) -> Self {
match self {
Self::Literal(l) => Self::Literal(l),
Self::OpCode(om,oc) => Self::OpCode(om,oc),
Self::Thunk(m) => Self::Thunk(Box::new(m.rename_r(igen))),
Self::Tuple(vs) => Self::Tuple(
vs.into_iter().map(|v| v.rename_r(igen)).collect()
),
// Remember, vars get renamed at their introduction point,
// not at their use-points. So here, we make no change.
Self::Var(n,ts,p,is_pos) => Self::Var(n,ts,p,is_pos),
}
}
}