Skip to content

Commit 576a62c

Browse files
committed
Refactor types
- rename FinalType to Type as it is used the most - rename Type to VariableType - rename UnificationVar to Variable - rename Variable to VariableInner - add documentation
1 parent 5807df7 commit 576a62c

File tree

9 files changed

+245
-228
lines changed

9 files changed

+245
-228
lines changed

src/bit_machine/exec.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ use std::cmp;
2222
use std::error;
2323
use std::fmt;
2424

25-
use crate::core::types::FinalTypeInner;
25+
use crate::core::types::TypeInner;
2626
use crate::core::{LinearProgram, Program, Term, Value};
2727
use crate::decode;
2828
use crate::jet::{AppError, Application};
@@ -309,7 +309,7 @@ impl BitMachine {
309309
Term::Iden => self.copy(ip.source_ty.bit_width),
310310
Term::InjL(t) => {
311311
self.write_bit(false);
312-
if let FinalTypeInner::Sum(ref a, _) = ip.target_ty.ty {
312+
if let TypeInner::Sum(ref a, _) = ip.target_ty.ty {
313313
let aw = a.bit_width;
314314
self.skip(ip.target_ty.bit_width - aw - 1);
315315
call_stack.push(CallStack::Goto(ip.index - t));
@@ -319,7 +319,7 @@ impl BitMachine {
319319
}
320320
Term::InjR(t) => {
321321
self.write_bit(true);
322-
if let FinalTypeInner::Sum(_, ref b) = ip.target_ty.ty {
322+
if let TypeInner::Sum(_, ref b) = ip.target_ty.ty {
323323
let bw = b.bit_width;
324324
self.skip(ip.target_ty.bit_width - bw - 1);
325325
call_stack.push(CallStack::Goto(ip.index - t));
@@ -369,7 +369,7 @@ impl BitMachine {
369369
}
370370
Term::Take(t) => call_stack.push(CallStack::Goto(ip.index - t)),
371371
Term::Drop(t) => {
372-
if let FinalTypeInner::Product(ref a, _) = ip.source_ty.ty {
372+
if let TypeInner::Product(ref a, _) = ip.source_ty.ty {
373373
let aw = a.bit_width;
374374
self.fwd(aw);
375375
call_stack.push(CallStack::Back(aw));
@@ -382,8 +382,8 @@ impl BitMachine {
382382
let sw = self.read[self.read.len() - 1].peek_bit(&self.data);
383383
let aw;
384384
let bw;
385-
if let FinalTypeInner::Product(ref a, _) = ip.source_ty.ty {
386-
if let FinalTypeInner::Sum(ref a, ref b) = a.ty {
385+
if let TypeInner::Product(ref a, _) = ip.source_ty.ty {
386+
if let TypeInner::Sum(ref a, ref b) = a.ty {
387387
aw = a.bit_width;
388388
bw = b.bit_width;
389389
} else {

src/core/program.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ use std::collections::{HashMap, HashSet};
2323
use std::{fmt, io};
2424

2525
use crate::bititer::BitIter;
26-
use crate::core::types::FinalType;
26+
use crate::core::types::Type;
2727
use crate::core::{iter, LinearProgram, Term, TypedNode, TypedProgram, Value};
2828
use crate::encode::BitWriter;
2929
use crate::jet::Application;
@@ -58,12 +58,12 @@ impl<App: Application> ProgramNode<App> {
5858
}
5959

6060
/// Return the source type of the node.
61-
pub fn source_ty(&self) -> &FinalType {
61+
pub fn source_ty(&self) -> &Type {
6262
&self.typed.source_ty
6363
}
6464

6565
/// Return the target type of the node.
66-
pub fn target_ty(&self) -> &FinalType {
66+
pub fn target_ty(&self) -> &Type {
6767
&self.typed.target_ty
6868
}
6969

src/core/typed.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
//
1414

1515
use crate::bititer::BitIter;
16-
use crate::core::types::FinalType;
16+
use crate::core::types::Type;
1717
use crate::core::{iter, LinearProgram, Program, ProgramNode, Term, UntypedProgram, Value};
1818
use crate::encode::BitWriter;
1919
use crate::jet::Application;
@@ -29,9 +29,9 @@ pub struct TypedNode<Witness, App: Application> {
2929
/// Underlying term
3030
pub term: Term<Witness, App>,
3131
/// Source type of the node
32-
pub source_ty: Arc<FinalType>,
32+
pub source_ty: Arc<Type>,
3333
/// Target type of the node
34-
pub target_ty: Arc<FinalType>,
34+
pub target_ty: Arc<Type>,
3535
/// Index of the node inside the surrounding program
3636
pub index: usize,
3737
/// Commitment Merkle root of the node
@@ -127,7 +127,7 @@ impl<Witness, App: Application> TypedProgram<Witness, App> {
127127
}
128128

129129
/// Return a vector of the types of values that make up a valid witness for the program.
130-
pub fn get_witness_types(&self) -> Vec<&FinalType> {
130+
pub fn get_witness_types(&self) -> Vec<&Type> {
131131
let mut witness_types = Vec::new();
132132

133133
for node in &self.0 {

src/core/types.rs

Lines changed: 128 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -2,67 +2,63 @@ use crate::merkle::common::{MerkleRoot, TypeMerkleRoot};
22
use crate::merkle::tmr::Tmr;
33
use std::{cell::RefCell, cmp, fmt, rc::Rc, sync::Arc};
44

5-
#[derive(Clone, Debug)]
6-
pub(crate) enum Type {
7-
Unit,
8-
Sum(RcVar, RcVar),
9-
Product(RcVar, RcVar),
10-
}
11-
12-
impl Type {
13-
pub(crate) fn into_rcvar(self) -> RcVar {
14-
Rc::new(RefCell::new(UnificationVar::concrete(self)))
15-
}
16-
}
17-
18-
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)]
19-
pub enum FinalTypeInner {
20-
Unit,
21-
Sum(Arc<FinalType>, Arc<FinalType>),
22-
Product(Arc<FinalType>, Arc<FinalType>),
23-
}
24-
5+
/// Finalized Simplicity type.
6+
///
7+
/// _Unit_ is the base type and is for _unit_ values.
8+
///
9+
/// The _sum_ of types A and B is for values
10+
/// that are the _left sum_ of a value of type A or the _right sum_ of a value of type B.
11+
///
12+
/// The _product_ of types A and B is for values
13+
/// that are the _product_ of a value of type A and a value of type B.
14+
///
15+
/// _(see [`crate::core::Value`])_
2516
#[derive(Clone, PartialOrd, Ord, Debug)]
26-
pub struct FinalType {
27-
pub ty: FinalTypeInner,
17+
pub struct Type {
18+
/// Underlying type with references to sub-types
19+
pub ty: TypeInner,
20+
/// Bit width of the type
2821
pub bit_width: usize,
29-
/// The annotated type merkle root of the type
22+
/// Annotated Type Merkle root of the type
3023
pub tmr: Tmr,
31-
/// cached display result in order to avoid repeat computation
24+
/// Cached display result in order to avoid repeat computation
3225
pub display: String,
3326
}
3427

35-
impl FinalType {
36-
pub fn unit() -> Self {
37-
let ty = FinalTypeInner::Unit;
28+
impl Type {
29+
/// Return a unit type.
30+
pub fn unit() -> Arc<Self> {
31+
let ty = TypeInner::Unit;
3832

39-
Self {
33+
Arc::new(Self {
4034
tmr: Tmr::get_iv(&ty),
4135
ty,
4236
bit_width: 0,
4337
display: "1".to_owned(),
44-
}
38+
})
4539
}
4640

47-
pub fn sum(a: Arc<Self>, b: Arc<Self>) -> Self {
48-
let ty = FinalTypeInner::Sum(a.clone(), b.clone());
41+
/// Return the sum of the given two types.
42+
pub fn sum(a: Arc<Self>, b: Arc<Self>) -> Arc<Self> {
43+
let ty = TypeInner::Sum(a.clone(), b.clone());
4944

50-
Self {
45+
Arc::new(Self {
5146
tmr: Tmr::get_iv(&ty).update(a.tmr, b.tmr),
5247
ty,
5348
bit_width: 1 + cmp::max(a.bit_width, b.bit_width),
54-
display: if a.ty == FinalTypeInner::Unit && b.ty == FinalTypeInner::Unit {
49+
display: if a.ty == TypeInner::Unit && b.ty == TypeInner::Unit {
5550
"2".to_owned()
5651
} else {
5752
format!("({} + {})", a.display, b.display)
5853
},
59-
}
54+
})
6055
}
6156

62-
pub fn prod(a: Arc<Self>, b: Arc<Self>) -> Self {
63-
let ty = FinalTypeInner::Product(a.clone(), b.clone());
57+
/// Return the product of the given two types.
58+
pub fn product(a: Arc<Self>, b: Arc<Self>) -> Arc<Self> {
59+
let ty = TypeInner::Product(a.clone(), b.clone());
6460

65-
Self {
61+
Arc::new(Self {
6662
tmr: Tmr::get_iv(&ty).update(a.tmr, b.tmr),
6763
ty,
6864
bit_width: a.bit_width + b.bit_width,
@@ -81,81 +77,131 @@ impl FinalType {
8177
} else {
8278
format!("({} × {})", a.display, b.display)
8379
},
84-
}
80+
})
8581
}
8682
}
8783

88-
impl fmt::Display for FinalType {
84+
impl fmt::Display for Type {
8985
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
90-
write!(f, "{}", self.display)
86+
f.write_str(&self.display)
9187
}
9288
}
9389

94-
impl PartialEq for FinalType {
90+
impl PartialEq for Type {
9591
fn eq(&self, other: &Self) -> bool {
9692
self.tmr.eq(&other.tmr)
9793
}
9894
}
9995

100-
impl Eq for FinalType {}
96+
impl Eq for Type {}
10197

102-
impl std::hash::Hash for FinalType {
98+
impl std::hash::Hash for Type {
10399
fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
104100
self.tmr.hash(state)
105101
}
106102
}
107103

108-
#[derive(Clone)]
109-
pub(crate) enum Variable {
110-
/// Free variable
111-
Free,
112-
/// Bound to some type (which may itself contain other free variables,
113-
/// or not). Contains a boolean which is only used by the finalization
114-
/// function, for the occurs-check
115-
Bound(Type, bool),
116-
/// Equal to another variable (the included `RcVar` is the "parent"
117-
/// pointer in union-find terms)
118-
EqualTo(RcVar),
119-
/// Complete type has been set in place
120-
Finalized(Arc<FinalType>),
104+
/// Finalized Simplicity type without metadata (see [`Type`])
105+
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)]
106+
pub enum TypeInner {
107+
/// Unit type
108+
Unit,
109+
/// Sum of two types
110+
Sum(Arc<Type>, Arc<Type>),
111+
/// Product of two types
112+
Product(Arc<Type>, Arc<Type>),
121113
}
122114

123-
impl fmt::Debug for Variable {
124-
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
125-
match *self {
126-
Variable::Free => f.write_str("?"),
127-
Variable::Bound(ref ty, b) => write!(f, "[{:?}/{}]", ty, b),
128-
Variable::EqualTo(ref other) => write!(f, "={:?}", other),
129-
Variable::Finalized(..) => unimplemented!(),
130-
}
131-
}
115+
/// Variable Simplicity type.
116+
///
117+
/// In contrast to [`Type`],
118+
/// a [`VariableType`] contains variables that can be internally mutated.
119+
#[derive(Clone, Debug)]
120+
pub(crate) enum VariableType {
121+
/// Unit type
122+
Unit,
123+
/// Sum of two types
124+
Sum(RcVar, RcVar),
125+
/// Product of two types
126+
Product(RcVar, RcVar),
132127
}
133128

134-
pub(crate) struct UnificationVar {
135-
pub var: Variable,
129+
/// Variable that can be cheaply cloned and internally mutated
130+
pub(crate) type RcVar = Rc<RefCell<Variable>>;
131+
132+
/// Unification variable
133+
#[derive(Clone)]
134+
pub(crate) struct Variable {
135+
/// Underlying variable
136+
pub inner: VariableInner,
137+
/// Rank for union-first algorithm
136138
pub rank: usize,
137139
}
138140

139-
impl fmt::Debug for UnificationVar {
140-
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
141-
write!(f, "[{}]{:?}", self.rank, self.var)
141+
impl Variable {
142+
/// Return a free variable.
143+
pub fn free() -> RcVar {
144+
Rc::new(RefCell::new(Self {
145+
inner: VariableInner::Free,
146+
rank: 0,
147+
}))
142148
}
143-
}
144149

145-
pub(crate) type RcVar = Rc<RefCell<UnificationVar>>;
146-
147-
impl UnificationVar {
148-
pub fn free() -> UnificationVar {
149-
UnificationVar {
150-
var: Variable::Free,
150+
/// Return a variable that is bound to the given type.
151+
pub fn bound(ty: VariableType) -> RcVar {
152+
Rc::new(RefCell::new(Self {
153+
inner: VariableInner::Bound(ty, false),
151154
rank: 0,
152-
}
155+
}))
153156
}
154157

155-
pub fn concrete(ty: Type) -> UnificationVar {
156-
UnificationVar {
157-
var: Variable::Bound(ty, false),
158-
rank: 0,
158+
/// Return an array `pow2s` of types such that `pow2s[i] = 2^i` holds for 0 ≤ `i` < 9.
159+
pub fn powers_of_two() -> [RcVar; 9] {
160+
let two_0 = Variable::bound(VariableType::Unit);
161+
let two_1 = Variable::bound(VariableType::Sum(two_0.clone(), two_0));
162+
let two_2 = Variable::bound(VariableType::Product(two_1.clone(), two_1.clone()));
163+
let two_4 = Variable::bound(VariableType::Product(two_2.clone(), two_2.clone()));
164+
let two_8 = Variable::bound(VariableType::Product(two_4.clone(), two_4.clone()));
165+
let two_16 = Variable::bound(VariableType::Product(two_8.clone(), two_8.clone()));
166+
let two_32 = Variable::bound(VariableType::Product(two_16.clone(), two_16.clone()));
167+
let two_64 = Variable::bound(VariableType::Product(two_32.clone(), two_32.clone()));
168+
let two_128 = Variable::bound(VariableType::Product(two_64.clone(), two_64.clone()));
169+
let two_256 = Variable::bound(VariableType::Product(two_128.clone(), two_128.clone()));
170+
171+
[
172+
two_1, two_2, two_4, two_8, two_16, two_32, two_64, two_128, two_256,
173+
]
174+
}
175+
}
176+
177+
impl fmt::Debug for Variable {
178+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
179+
write!(f, "[{}]{:?}", self.rank, self.inner)
180+
}
181+
}
182+
183+
/// Unification variable without metadata (see [`Variable`])
184+
#[derive(Clone)]
185+
pub(crate) enum VariableInner {
186+
/// Free variable
187+
Free,
188+
/// Variable bound to some variable type.
189+
/// Contains a Boolean to check if this variable already occurred _(occurs check)_
190+
Bound(VariableType, bool),
191+
/// Variable equal to another variable.
192+
/// In the union-find algorithm, this is the _parent_
193+
EqualTo(RcVar),
194+
/// Variable bound to some finalized type
195+
Finalized(Arc<Type>),
196+
}
197+
198+
impl fmt::Debug for VariableInner {
199+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
200+
match self {
201+
VariableInner::Free => f.write_str("?"),
202+
VariableInner::Bound(ty, b) => write!(f, "[{:?}/{}]", ty, b),
203+
VariableInner::EqualTo(parent) => write!(f, "={:?}", parent),
204+
VariableInner::Finalized(ty) => fmt::Debug::fmt(ty, f),
159205
}
160206
}
161207
}

0 commit comments

Comments
 (0)