Merge #34: Types

f5d7201 Refactor inference (Christian Lewe)
1b510f0 Implement fmt::Display for variable types (Christian Lewe)
705d2f6 Give names to variables (Christian Lewe)
576a62c Refactor types (Christian Lewe)
5807df7 Move inference to separate module (Christian Lewe)
6bebb38 Move TypeName conversion to jet module (Christian Lewe)

Pull request description:

  This PR refactors the type system: Types are kept separate from type inference, identifiers were changed, and documentation was added. The big addition is that variables have `String`s as identifiers and variable types implement `Display` using that. As these types are variable, we cannot use the optimisation of storing formatted strings in the struct. Instead, we create a large string and replace occurrences of powers of two using relatively few allocations. This formatting can be used in a later PR to create helpful type errors.

ACKs for top commit:
  apoelstra:
    ACK f5d7201

Tree-SHA512: e7d2221ab46ab414302962c4c2ed8a335e4724ef2951e95ac4beb50d07aa489aea15cb5e8a46a8685c0ec4104a226cd604a8b7abd1e21c72a4ec64a223a294de

Author: uncomputable

src/analysis.rs

@@ -28,7 +28,7 @@ pub(crate) fn compute_extra_cells_bound<App: Application>(
             program[node.index - i].extra_cells_bound
         }
         Term::Comp(i, j) => {
-            program[node.index - i].target_ty().bit_width()
+            program[node.index - i].target_ty().bit_width
                 + cmp::max(
                     program[node.index - i].extra_cells_bound,
                     program[node.index - j].extra_cells_bound,
@@ -41,8 +41,8 @@ pub(crate) fn compute_extra_cells_bound<App: Application>(
             )
         }
         Term::Disconnect(i, j) => {
-            program[node.index - i].source_ty().bit_width()
-                + program[node.index - i].target_ty().bit_width()
+            program[node.index - i].source_ty().bit_width
+                + program[node.index - i].target_ty().bit_width
                 + cmp::max(
                     program[node.index - i].extra_cells_bound,
                     program[node.index - j].extra_cells_bound,

src/bit_machine/exec.rs

@@ -22,7 +22,7 @@ use std::cmp;
 use std::error;
 use std::fmt;
 
-use crate::core::types::FinalTypeInner;
+use crate::core::types::TypeInner;
 use crate::core::{LinearProgram, Program, Term, Value};
 use crate::decode;
 use crate::jet::{AppError, Application};
@@ -47,7 +47,7 @@ impl BitMachine {
     /// the given program
     pub fn for_program<App: Application>(program: &Program<App>) -> BitMachine {
         let prog = program.root();
-        let io_width = prog.source_ty().bit_width() + prog.target_ty().bit_width();
+        let io_width = prog.source_ty().bit_width + prog.target_ty().bit_width;
         BitMachine {
             data: vec![0; (io_width + prog.extra_cells_bound + 7) / 8],
             next_frame_start: 0,
@@ -286,14 +286,14 @@ impl BitMachine {
         let mut call_stack = vec![];
         let mut iters = 0u64;
 
-        let input_width = ip.source_ty.bit_width();
+        let input_width = ip.source_ty.bit_width;
         if input_width > 0 && self.read.is_empty() {
             panic!(
                 "Pleas call `Program::input` to add an input value for this program {}",
                 ip
             );
         }
-        let output_width = ip.target_ty.bit_width();
+        let output_width = ip.target_ty.bit_width;
         if output_width > 0 {
             self.new_frame(output_width);
         }
@@ -306,22 +306,22 @@ impl BitMachine {
 
             match ip.term {
                 Term::Unit => {}
-                Term::Iden => self.copy(ip.source_ty.bit_width()),
+                Term::Iden => self.copy(ip.source_ty.bit_width),
                 Term::InjL(t) => {
                     self.write_bit(false);
-                    if let FinalTypeInner::Sum(ref a, _) = ip.target_ty.ty {
-                        let aw = a.bit_width();
-                        self.skip(ip.target_ty.bit_width() - aw - 1);
+                    if let TypeInner::Sum(ref a, _) = ip.target_ty.ty {
+                        let aw = a.bit_width;
+                        self.skip(ip.target_ty.bit_width - aw - 1);
                         call_stack.push(CallStack::Goto(ip.index - t));
                     } else {
                         panic!("type error")
                     }
                 }
                 Term::InjR(t) => {
                     self.write_bit(true);
-                    if let FinalTypeInner::Sum(_, ref b) = ip.target_ty.ty {
-                        let bw = b.bit_width();
-                        self.skip(ip.target_ty.bit_width() - bw - 1);
+                    if let TypeInner::Sum(_, ref b) = ip.target_ty.ty {
+                        let bw = b.bit_width;
+                        self.skip(ip.target_ty.bit_width - bw - 1);
                         call_stack.push(CallStack::Goto(ip.index - t));
                     } else {
                         panic!("type error")
@@ -332,7 +332,7 @@ impl BitMachine {
                     call_stack.push(CallStack::Goto(ip.index - s));
                 }
                 Term::Comp(s, t) => {
-                    let size = program.nodes[ip.index - s].target_ty().bit_width();
+                    let size = program.nodes[ip.index - s].target_ty().bit_width;
                     self.new_frame(size);
 
                     call_stack.push(CallStack::DropFrame);
@@ -342,23 +342,22 @@ impl BitMachine {
                 }
                 Term::Disconnect(s, t) => {
                     // Write `t`'s CMR followed by `s` input to a new read frame
-                    let size = program.nodes[ip.index - s].source_ty().bit_width();
+                    let size = program.nodes[ip.index - s].source_ty().bit_width;
                     assert!(size >= 256);
                     self.new_frame(size);
                     self.write_bytes(program.nodes[ip.index - t].cmr().as_ref());
                     self.copy(size - 256);
                     self.move_frame();
 
-                    let s_target_size = program.nodes[ip.index - s].target_ty().bit_width();
+                    let s_target_size = program.nodes[ip.index - s].target_ty().bit_width;
                     self.new_frame(s_target_size);
                     // Then recurse. Remembering that call stack pushes are executed
                     // in reverse order:
 
                     // 3. Delete the two frames we created, which have both moved to the read stack
                     call_stack.push(CallStack::DropFrame);
                     call_stack.push(CallStack::DropFrame);
-                    let b_size =
-                        s_target_size - program.nodes[ip.index - t].source_ty().bit_width();
+                    let b_size = s_target_size - program.nodes[ip.index - t].source_ty().bit_width;
                     // Back not required since we are dropping the frame anyways
                     // call_stack.push(CallStack::Back(b_size));
                     // 2. Copy the first half of `s`s output directly then execute `t` on the second half
@@ -370,8 +369,8 @@ impl BitMachine {
                 }
                 Term::Take(t) => call_stack.push(CallStack::Goto(ip.index - t)),
                 Term::Drop(t) => {
-                    if let FinalTypeInner::Product(ref a, _) = ip.source_ty.ty {
-                        let aw = a.bit_width();
+                    if let TypeInner::Product(ref a, _) = ip.source_ty.ty {
+                        let aw = a.bit_width;
                         self.fwd(aw);
                         call_stack.push(CallStack::Back(aw));
                         call_stack.push(CallStack::Goto(ip.index - t));
@@ -383,10 +382,10 @@ impl BitMachine {
                     let sw = self.read[self.read.len() - 1].peek_bit(&self.data);
                     let aw;
                     let bw;
-                    if let FinalTypeInner::Product(ref a, _) = ip.source_ty.ty {
-                        if let FinalTypeInner::Sum(ref a, ref b) = a.ty {
-                            aw = a.bit_width();
-                            bw = b.bit_width();
+                    if let TypeInner::Product(ref a, _) = ip.source_ty.ty {
+                        if let TypeInner::Sum(ref a, ref b) = a.ty {
+                            aw = a.bit_width;
+                            bw = b.bit_width;
                         } else {
                             panic!("type error");
                         }

src/core/program.rs

@@ -23,7 +23,7 @@ use std::collections::{HashMap, HashSet};
 use std::{fmt, io};
 
 use crate::bititer::BitIter;
-use crate::core::types::FinalType;
+use crate::core::types::Type;
 use crate::core::{iter, LinearProgram, Term, TypedNode, TypedProgram, Value};
 use crate::encode::BitWriter;
 use crate::jet::Application;
@@ -58,12 +58,12 @@ impl<App: Application> ProgramNode<App> {
     }
 
     /// Return the source type of the node.
-    pub fn source_ty(&self) -> &FinalType {
+    pub fn source_ty(&self) -> &Type {
         &self.typed.source_ty
     }
 
     /// Return the target type of the node.
-    pub fn target_ty(&self) -> &FinalType {
+    pub fn target_ty(&self) -> &Type {
         &self.typed.target_ty
     }
 

src/core/term.rs

@@ -26,12 +26,11 @@
 use crate::bititer::BitIter;
 use crate::core::iter::DagIterable;
 use crate::core::typed::TypedProgram;
-use crate::core::{iter, LinearProgram};
-use crate::core::{types, Value};
+use crate::core::{iter, LinearProgram, Value};
 use crate::encode::BitWriter;
 use crate::jet::{Application, JetNode};
 use crate::merkle::cmr::Cmr;
-use crate::{decode, encode, Error};
+use crate::{decode, encode, inference, Error};
 use std::collections::HashMap;
 use std::hash::Hash;
 use std::io;
@@ -246,7 +245,7 @@ impl<Witness, App: Application> UntypedProgram<Witness, App> {
 
     /// Type-check the program and add metadata for the time of commitment.
     pub fn type_check(self) -> Result<TypedProgram<Witness, App>, Error> {
-        types::type_check(self)
+        inference::type_check(self)
     }
 }
 

src/core/typed.rs

@@ -13,13 +13,13 @@
 //
 
 use crate::bititer::BitIter;
-use crate::core::types::FinalType;
-use crate::core::{iter, types, LinearProgram, Program, ProgramNode, Term, UntypedProgram, Value};
+use crate::core::types::Type;
+use crate::core::{iter, LinearProgram, Program, ProgramNode, Term, UntypedProgram, Value};
 use crate::encode::BitWriter;
 use crate::jet::Application;
 use crate::merkle::cmr::Cmr;
 use crate::merkle::imr;
-use crate::{analysis, decode, encode, Error};
+use crate::{analysis, decode, encode, inference, Error};
 use std::sync::Arc;
 use std::{fmt, io};
 
@@ -29,9 +29,9 @@ pub struct TypedNode<Witness, App: Application> {
     /// Underlying term
     pub term: Term<Witness, App>,
     /// Source type of the node
-    pub source_ty: Arc<FinalType>,
+    pub source_ty: Arc<Type>,
     /// Target type of the node
-    pub target_ty: Arc<FinalType>,
+    pub target_ty: Arc<Type>,
     /// Index of the node inside the surrounding program
     pub index: usize,
     /// Commitment Merkle root of the node
@@ -73,7 +73,7 @@ impl<App: Application> TypedProgram<(), App> {
     /// Decode a typed program from bits.
     pub fn decode<I: Iterator<Item = u8>>(iter: &mut BitIter<I>) -> Result<Self, Error> {
         let program = UntypedProgram::<(), App>::decode(iter)?;
-        types::type_check(program)
+        inference::type_check(program)
     }
 
     /// Encode the program into bits.
@@ -127,7 +127,7 @@ impl<Witness, App: Application> TypedProgram<Witness, App> {
     }
 
     /// Return a vector of the types of values that make up a valid witness for the program.
-    pub fn get_witness_types(&self) -> Vec<&FinalType> {
+    pub fn get_witness_types(&self) -> Vec<&Type> {
         let mut witness_types = Vec::new();
 
         for node in &self.0 {