Skip to content

Commit 705d2f6

Browse files
uncomputableuncomputable
committed
Give names to variables
1 parent 576a62c commit 705d2f6

File tree

2 files changed

+60
-25
lines changed

2 files changed

+60
-25
lines changed

‎src/core/types.rs

Lines changed: 37 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
use crate::merkle::common::{MerkleRoot, TypeMerkleRoot};
22
use crate::merkle::tmr::Tmr;
3+
use std::collections::VecDeque;
4+
use std::iter::FromIterator;
35
use std::{cell::RefCell, cmp, fmt, rc::Rc, sync::Arc};
46

57
/// Finalized Simplicity type.
@@ -140,9 +142,9 @@ pub(crate) struct Variable {
140142

141143
impl Variable {
142144
/// Return a free variable.
143-
pub fn free() -> RcVar {
145+
pub fn free(id: String) -> RcVar {
144146
Rc::new(RefCell::new(Self {
145-
inner: VariableInner::Free,
147+
inner: VariableInner::Free(id),
146148
rank: 0,
147149
}))
148150
}
@@ -183,8 +185,8 @@ impl fmt::Debug for Variable {
183185
/// Unification variable without metadata (see [`Variable`])
184186
#[derive(Clone)]
185187
pub(crate) enum VariableInner {
186-
/// Free variable
187-
Free,
188+
/// Free variable with some identifier
189+
Free(String),
188190
/// Variable bound to some variable type.
189191
/// Contains a Boolean to check if this variable already occurred _(occurs check)_
190192
Bound(VariableType, bool),
@@ -198,10 +200,40 @@ pub(crate) enum VariableInner {
198200
impl fmt::Debug for VariableInner {
199201
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
200202
match self {
201-
VariableInner::Free => f.write_str("?"),
203+
VariableInner::Free(id) => fmt::Debug::fmt(id, f),
202204
VariableInner::Bound(ty, b) => write!(f, "[{:?}/{}]", ty, b),
203205
VariableInner::EqualTo(parent) => write!(f, "={:?}", parent),
204206
VariableInner::Finalized(ty) => fmt::Debug::fmt(ty, f),
205207
}
206208
}
207209
}
210+
211+
/// Factory for creating free variables with fresh names.
212+
/// Identifiers are assigned sequentially as follows:
213+
/// `A`, `B`, `C`, ... `Z`, `AA`, `AB`, `AC`, ...
214+
pub(crate) struct VariableFactory {
215+
next_id: usize,
216+
}
217+
218+
impl VariableFactory {
219+
/// Create a new factory.
220+
pub fn new() -> Self {
221+
Self { next_id: 1 }
222+
}
223+
224+
/// Return a free variable with a fresh name.
225+
pub fn free_variable(&mut self) -> RcVar {
226+
let mut n = self.next_id;
227+
self.next_id += 1;
228+
let mut ascii_bytes = VecDeque::new();
229+
230+
while n / 26 > 0 {
231+
ascii_bytes.push_front((n % 26) as u8 + 65);
232+
n /= 26;
233+
}
234+
235+
ascii_bytes.push_front((n % 26) as u8 + 64);
236+
let id = String::from_utf8(Vec::from_iter(ascii_bytes.into_iter())).unwrap();
237+
Variable::free(id)
238+
}
239+
}

‎src/inference.rs

Lines changed: 23 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use crate::core::types::{RcVar, Type, Variable, VariableInner, VariableType};
1+
use crate::core::types::{RcVar, Type, Variable, VariableFactory, VariableInner, VariableType};
22
use crate::core::{Term, TypedNode, TypedProgram, UntypedProgram};
33
use crate::jet::Application;
44
use crate::merkle::cmr;
@@ -53,7 +53,7 @@ fn unify(mut alpha: RcVar, mut beta: RcVar) -> Result<(), Error> {
5353
mem::replace(&mut be_borr.inner, VariableInner::EqualTo(alpha.clone()))
5454
};
5555
match be_var {
56-
VariableInner::Free => {} // nothing to do
56+
VariableInner::Free(_) => {} // nothing to do
5757
VariableInner::Bound(be_type, _) => bind(&alpha, be_type)?,
5858
VariableInner::EqualTo(..) => unreachable!(),
5959
VariableInner::Finalized(..) => unreachable!(),
@@ -67,7 +67,7 @@ fn bind(rcvar: &RcVar, ty: VariableType) -> Result<(), Error> {
6767
// hold `Rc`s
6868
let self_var = rcvar.borrow().inner.clone();
6969
match self_var {
70-
VariableInner::Free => {
70+
VariableInner::Free(_) => {
7171
rcvar.borrow_mut().inner = VariableInner::Bound(ty, false);
7272
Ok(())
7373
}
@@ -109,7 +109,7 @@ fn finalize(var: RcVar) -> Result<Arc<Type>, Error> {
109109
let mut var_borr = var.borrow_mut();
110110

111111
let existing_type = match var_borr.inner {
112-
VariableInner::Free => VariableType::Unit,
112+
VariableInner::Free(_) => VariableType::Unit,
113113
VariableInner::Bound(ref ty, ref mut occurs_check) => {
114114
if *occurs_check {
115115
return Err(Error::OccursCheck);
@@ -137,7 +137,7 @@ fn finalize(var: RcVar) -> Result<Arc<Type>, Error> {
137137

138138
let sub1_borr = sub1.borrow_mut();
139139
let final1 = match sub1_borr.inner {
140-
VariableInner::Free => {
140+
VariableInner::Free(_) => {
141141
drop(sub1_borr);
142142
Type::unit()
143143
}
@@ -155,7 +155,7 @@ fn finalize(var: RcVar) -> Result<Arc<Type>, Error> {
155155
// drop(sub1_borr);
156156
let sub2_borr = sub2.borrow_mut();
157157
let final2 = match sub2_borr.inner {
158-
VariableInner::Free => {
158+
VariableInner::Free(_) => {
159159
drop(sub2_borr);
160160
Type::unit()
161161
}
@@ -199,12 +199,13 @@ pub(crate) fn type_check<Witness, App: Application>(
199199
let mut rcs = Vec::<Rc<UnificationArrow>>::with_capacity(vec_nodes.len());
200200
let mut finals = Vec::<TypedNode<Witness, App>>::with_capacity(vec_nodes.len());
201201
let pow2s = Variable::powers_of_two();
202+
let mut naming = VariableFactory::new();
202203

203204
// Compute most general unifier for all types in the DAG
204205
for (idx, program_node) in vec_nodes.iter().enumerate() {
205206
let node = UnificationArrow {
206-
source: Variable::free(),
207-
target: Variable::free(),
207+
source: naming.free_variable(),
208+
target: naming.free_variable(),
208209
};
209210

210211
match program_node {
@@ -213,25 +214,27 @@ pub(crate) fn type_check<Witness, App: Application>(
213214
Term::InjL(i) => {
214215
let i = idx - i;
215216
unify(node.source.clone(), rcs[i].source.clone())?;
216-
let target_type = VariableType::Sum(rcs[i].target.clone(), Variable::free());
217+
let target_type = VariableType::Sum(rcs[i].target.clone(), naming.free_variable());
217218
bind(&node.target, target_type)?;
218219
}
219220
Term::InjR(i) => {
220221
let i = idx - i;
221222
unify(node.source.clone(), rcs[i].source.clone())?;
222-
let target_type = VariableType::Sum(Variable::free(), rcs[i].target.clone());
223+
let target_type = VariableType::Sum(naming.free_variable(), rcs[i].target.clone());
223224
bind(&node.target, target_type)?;
224225
}
225226
Term::Take(i) => {
226227
let i = idx - i;
227228
unify(node.target.clone(), rcs[i].target.clone())?;
228-
let target_type = VariableType::Product(rcs[i].source.clone(), Variable::free());
229+
let target_type =
230+
VariableType::Product(rcs[i].source.clone(), naming.free_variable());
229231
bind(&node.source, target_type)?;
230232
}
231233
Term::Drop(i) => {
232234
let i = idx - i;
233235
unify(node.target.clone(), rcs[i].target.clone())?;
234-
let target_type = VariableType::Product(Variable::free(), rcs[i].source.clone());
236+
let target_type =
237+
VariableType::Product(naming.free_variable(), rcs[i].source.clone());
235238
bind(&node.source, target_type)?;
236239
}
237240
Term::Comp(i, j) => {
@@ -242,12 +245,12 @@ pub(crate) fn type_check<Witness, App: Application>(
242245
}
243246
Term::Case(i, j) | Term::AssertL(i, j) | Term::AssertR(i, j) => {
244247
let (i, j) = (idx - i, idx - j);
245-
let var1 = Variable::free();
246-
let var2 = Variable::free();
247-
let var3 = Variable::free();
248+
let var1 = naming.free_variable();
249+
let var2 = naming.free_variable();
250+
let var3 = naming.free_variable();
248251

249252
let sum12_ty = VariableType::Sum(var1.clone(), var2.clone());
250-
let sum12_var = Variable::free();
253+
let sum12_var = naming.free_variable();
251254
bind(&sum12_var, sum12_ty)?;
252255

253256
let source_ty = VariableType::Product(sum12_var, var3.clone());
@@ -282,10 +285,10 @@ pub(crate) fn type_check<Witness, App: Application>(
282285
let (i, j) = (idx - i, idx - j);
283286
// See chapter 6 (Delegation) of TR
284287
// Be careful, this order changed! https://github.com/ElementsProject/simplicity/pull/46
285-
let var_a = Variable::free();
286-
let var_b = Variable::free();
287-
let var_c = Variable::free();
288-
let var_d = Variable::free();
288+
let var_a = naming.free_variable();
289+
let var_b = naming.free_variable();
290+
let var_c = naming.free_variable();
291+
let var_d = naming.free_variable();
289292

290293
let s_source =
291294
Variable::bound(VariableType::Product(pow2s[8].clone(), var_a.clone()));

0 commit comments

Comments
 (0)