<div dir="ltr"><div>Dear subscribers,</div><div><br></div><div>Given Greg's recent collection of Simplicity test vectors, I thought it might be helpful if I created a little Haskell program to pretty-print Simplicity programs.  My main motivation here is to illustrate how to use the Haskell Simplicity library in a small application.</div><div><br></div><div>This program, <span style="font-family:monospace">PrettyPrint.hs</span>, depends on the Simplicity library from commit <a href="https://github.com/ElementsProject/simplicity/tree/cf12c6947c2d6730e31482ec291658f10ccc9207">https://github.com/ElementsProject/simplicity/tree/cf12c6947c2d6730e31482ec291658f10ccc9207</a>.</div><div><br></div><div>----8<----</div><div><span style="font-family:monospace">module Main where<br><br>import Control.Monad<br>import qualified Data.ByteString as BS<br>import Data.Functor.Fixedpoint<br>import Data.Foldable<br>import Data.Sequence (Seq)<br>import Data.Serialize<br>import Data.Void<br>import Lens.Family2<br>import Lens.Family2.Stock<br>import System.IO<br><br>import Simplicity.Elements.Inference<br>import Simplicity.Elements.Serialization.BitString<br>import Simplicity.Serialization<br>import qualified Simplicity.Tensor as Tensor<br>import Simplicity.Ty (Ty, UntypedValue)<br>import qualified Simplicity.Ty as Ty<br><br>-- Printing out raw Simplicity types gets pretty exhausting<br>-- Below we build a custom data type for Simplicity type annotations so we can nicely display common Simplicity types.<br>data PrettyTy = Two Integer -- This constructor represents n bit word types in Simplicity when n is 0 or a power of 2.<br>              | Sum PrettyTy PrettyTy<br>              | Prod PrettyTy PrettyTy<br><br>-- The heart of the 'PrettyTy' pretty printer<br>instance Show PrettyTy where<br>  showsPrec _ (Two 0) = showString "One" -- a 0-bit type is the unit type.<br>  showsPrec _ (Two 1) = showString "Two" -- a 1-bit type<br>  showsPrec _ (Two n) = showString "Two^" . shows n -- an n-bit type<br>  -- One + X is the canonical way to represent the Maybe type, usually denoted by 'S'<br>  showsPrec _ (Sum (Two 0) y) = showParen True (showString "S " . shows y)<br>  showsPrec _ (Sum x y) = showParen True (shows x . showString " + " . shows y)<br>  showsPrec _ (Prod x y) = showParen True (shows x . showString " × " . shows y)<br><br>-- The transformation from a Simplicity type into 'PrettyTy' making it ready for pretty printing.<br>mkPrettyType :: Ty -> PrettyTy<br>mkPrettyType = cata f<br> where<br>  f Ty.One = Two 0<br>  f (Ty.Sum (Two 0) (Two 0)) = Two 1<br>  f (Ty.Sum x y) = Sum x y<br>  f (Ty.Prod (Two i) (Two j)) | i == j && i /= 0 = (Two (i+j))<br>  f (Ty.Prod x y) = Prod x y<br><br>-- The type 'forall m. Monad m => m Void -> m Bool -> m X' is a generic function for parsing bitstreams into a value X.<br>-- The two parameters, 'next' and 'abort', provide generic callbacks for requesting a bit, or indicating a parse failure.<br>--<br>-- In Simplicity, we can only complete parsing of the witness bitstream after type inference.<br>-- In this function we first parse the untyped Simplicity program from the bitstream (using 'abort' and 'next').<br>-- Next we run type typeInference to add Simplicity type annotations to the dag for a Simplicity program.<br>-- which is a Simplicity expression with a type from Unit to Unit.<br>-- Lastly, if typeInference was successful, we parse the witness data bitstream and fill in any witness combinators with their data.<br>getDagAndWitness :: Monad m => m Void -> m Bool -> m (Either String (SimplicityDag Seq Ty UntypedValue))<br>getDagAndWitness abort next = do<br>  uterm <- getDagNoWitnessLengthCode abort next<br>  let tterm = typeInference ((),()) uterm :: Either String (SimplicityDag Seq Ty ())<br>  wterm <- traverse (\term -> getWitnessData term abort next) tterm -- traversing (Either String)<br>  return wterm<br><br>-- The main program reads a Simplicity program encoded as a bitstream from stdin and pretty prints it to stdout.<br>-- Each node in the pretty printed DAG is on its own line, with a line number prefix.<br>-- The nodes have pretty printed type annotations, and references to the line numbers of their children expressions (if any).<br>-- If there is a failure, instead an error message is printed to 'stderr'.<br>main :: IO ()<br>main = do<br>  bs <- BS.getContents -- read all of stdin.<br>  let wterm = flip runGet bs (getEvalBitStream getDagAndWitness) -- parse stdin using the 'getDagAndWitness' parser.<br>  case join wterm of -- join on (Either String) combines the outer errors from runGet with the inner errors from 'getDagAndWitness'<br>    Left err -> hPutStrLn stderr $ "Error: " ++ err<br>    Right term -><br>      -- 'typeCheck' performs a double check on the type annotations.  We ignore any return value.<br>      case typeCheck term :: Either String (Tensor.Unit () ()) of<br>      Left err -> hPutStrLn stderr $ "Error: " ++ err<br>      Right _ -> do<br>        let zippedList = zip [0..] (toList term) -- create line numbers from the list of nodes.<br>        let padding = length (show (length zippedList - 1))<br>        let printNode (i, item) = putStrLn (pad padding (show i) ++ ": "<br>                               ++ show (item & tyAnnotation %~ mkPrettyType -- change the type annotations into pretty printed ones.<br>                                             & mapped %~ (i -))) -- convert the references to children from relative to absolute.<br>        mapM_ printNode zippedList<br> where<br>  pad n str = replicate (n - length str) ' ' ++ str<br></span></div><div>----8<----<br></div><div><br></div><div>Below I give an example run of the above program on one of Greg's test vectors (see <a href="https://lists.ozlabs.org/pipermail/simplicity/2019/000019.html">https://lists.ozlabs.org/pipermail/simplicity/2019/000019.html</a>).</div><div><br></div><div><div>----8<----<br></div><span style="font-family:monospace">$ runhaskell PrettyPrint.hs < assert_9                            <br> 0: Prim (someArrow currentAsset)<br> 1: Prim (someArrow outputNullDatum)<br> 2: Prim (someArrow version)<br> 3: Pair One Two^32 Two^32 2 2<br> 4: Injl Two^64 (S (S ((Two^2 × Two^256) + (Two + Two^4)))) One 1<br> 5: Comp One Two^64 ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One) 3 4<br> 6: Prim (someArrow currentIssuanceContract)<br> 7: Prim (someArrow currentScriptHash)<br> 8: Pair One Two^256 ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One) 7 5<br> 9: Pair One (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) 8 8<br>10: Pair One ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) Two^256 9 7<br>11: Unit ((((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) × Two^256) × ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))))<br>12: Pair One (((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) × Two^256) ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) 10 9<br>13: Comp One ((((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) × Two^256) × ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)))) One 12 11</span></div><div><div>----8<----</div><div><br></div><div>The output above writes "line numbers" for each combinator, given their inferred type annotations, and then references to the line numbers of their child subexpressions.</div><div><br></div><div>When we inspect the test vectors we see many of them have disconnected DAGs, where some lines do not have references (in the above example line 6 is unused).  Some examples are even more extreme with the program ending in <span style="font-family:monospace">Iden One</span> or <span style="font-family:monospace">Unit One<font face="arial,sans-serif">, which makes the root of the DAG disconnected from the rest of the graph.  Eventually these sorts of non-canonically encoded programs will be rejected by the C implementation.  Despite this, the fuzzer does seem to do a reasonable job of exercising the deserializer and the typechecker, both of which operate on the whole DAG, even if it is disconnected.  Some kind of special purpose generator of well-typed Simplicity programs may be needed to exercise the evaluation engine.</font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif"><br></font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif">I hope this example program proves useful.  For me, it has already been useful.  I added the </font>tyAnnotation<font face="arial,sans-serif"> traversal (<a href="https://github.com/ElementsProject/simplicity/blob/cf12c6947c2d6730e31482ec291658f10ccc9207/Haskell/Indef/Simplicity/Inference.hs#L159-L161">https://github.com/ElementsProject/simplicity/blob/cf12c6947c2d6730e31482ec291658f10ccc9207/Haskell/Indef/Simplicity/Inference.hs#L159-L161</a>) in order to pretty print the type annotations, and I now see that it might be helpful to rearrange the parameters to </font>getWitnessData<font face="arial,sans-serif"> to make partial application easier.</font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif"><br></font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif">Keep in mind that the library and even binary format is still under development, and this program and these specific test vectors are not guaranteed to remain fixed at this point in time.</font></span></div></div></div>