saw-central/Yosys: Reindent and lay out code.

For readability, 'do' and 'case' go on the left.

Author: brianhuffman

saw-central/src/SAWCentral/Yosys.hs

@@ -10,7 +10,6 @@ Stability   : experimental
 {-# Language OverloadedStrings #-}
 {-# Language RecordWildCards #-}
 {-# Language ViewPatterns #-}
-{-# Language LambdaCase #-}
 {-# Language MultiWayIf #-}
 {-# Language TupleSections #-}
 {-# Language ScopedTypeVariables #-}
@@ -93,62 +92,62 @@ convertYosysIR ::
   SC.SharedContext ->
   YosysIR ->
   IO (Map Text ConvertedModule)
-convertYosysIR sc ir = do
-  let mg = yosysIRModgraph ir
-  let sorted = reverseTopSort $ mg ^. modgraphGraph
-  foldM
-    (\env v -> do
-        let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
-        cm <- convertModule sc env m
-        _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
-        n <- Nonce.freshNonce Nonce.globalNonceGenerator
-        let frag = Text.pack . show $ Nonce.indexValue n
-        let uri = URI.URI
-              { URI.uriScheme = URI.mkScheme "yosys"
-              , URI.uriAuthority = Left True
-              , URI.uriPath = (False,) <$> mapM URI.mkPathPiece (nm NE.:| [])
-              , URI.uriQuery = []
-              , URI.uriFragment = URI.mkFragment frag
-              }
-        let ni = SC.ImportedName uri [nm]
-        tc <- SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
-        let cm' = cm { _convertedModuleTerm = tc }
-        pure $ Map.insert nm cm' env
-    )
-    Map.empty
-    sorted
+convertYosysIR sc ir =
+  do let mg = yosysIRModgraph ir
+     let sorted = reverseTopSort $ mg ^. modgraphGraph
+     foldM
+       (\env v ->
+          do let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
+             cm <- convertModule sc env m
+             _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
+             n <- Nonce.freshNonce Nonce.globalNonceGenerator
+             let frag = Text.pack . show $ Nonce.indexValue n
+             let uri = URI.URI
+                   { URI.uriScheme = URI.mkScheme "yosys"
+                   , URI.uriAuthority = Left True
+                   , URI.uriPath = (False,) <$> mapM URI.mkPathPiece (nm NE.:| [])
+                   , URI.uriQuery = []
+                   , URI.uriFragment = URI.mkFragment frag
+                   }
+             let ni = SC.ImportedName uri [nm]
+             tc <- SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
+             let cm' = cm { _convertedModuleTerm = tc }
+             pure $ Map.insert nm cm' env
+       )
+       Map.empty
+       sorted
 
 -- | Given a Yosys IR, construct a map from module names to TypedTerms
 yosysIRToTypedTerms ::
   SC.SharedContext ->
   YosysIR ->
   IO (Map Text SC.TypedTerm)
-yosysIRToTypedTerms sc ir = do
-  env <- convertYosysIR sc ir
-  pure . flip fmap env $ \cm ->
-    SC.TypedTerm
-    (SC.TypedTermSchema $ C.tMono $ cm ^. convertedModuleCryptolType)
-    $ cm ^. convertedModuleTerm
+yosysIRToTypedTerms sc ir =
+  do env <- convertYosysIR sc ir
+     pure $ flip fmap env $ \cm ->
+       SC.TypedTerm
+       (SC.TypedTermSchema $ C.tMono $ cm ^. convertedModuleCryptolType)
+       $ cm ^. convertedModuleTerm
 
 -- | Given a Yosys IR, construct a SAWCore record containing terms for each module
 yosysIRToRecordTerm ::
   SC.SharedContext ->
   YosysIR ->
   IO SC.TypedTerm
-yosysIRToRecordTerm sc ir = do
-  env <- convertYosysIR sc ir
-  record <- cryptolRecord sc $ view convertedModuleTerm <$> env
-  let cty = C.tRec . C.recordFromFields $ (\(nm, cm) -> (C.mkIdent nm, cm ^. convertedModuleCryptolType)) <$> Map.assocs env
-  let tt = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) record
-  pure tt
+yosysIRToRecordTerm sc ir =
+  do env <- convertYosysIR sc ir
+     record <- cryptolRecord sc $ view convertedModuleTerm <$> env
+     let cty = C.tRec . C.recordFromFields $ (\(nm, cm) -> (C.mkIdent nm, cm ^. convertedModuleCryptolType)) <$> Map.assocs env
+     let tt = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) record
+     pure tt
 
 -- | Given a Yosys IR, construct a value representing a specific module with all submodules inlined
 yosysIRToSequential ::
   SC.SharedContext ->
   YosysIR ->
   Text ->
   IO YosysSequential
-yosysIRToSequential sc ir nm = do
+yosysIRToSequential sc ir nm =
   case Map.lookup nm $ ir ^. yosysModules of
     Nothing -> throw . YosysError $ mconcat
       [ "Could not find module: "
@@ -167,12 +166,12 @@ yosysIRToSequential sc ir nm = do
 -- Each HDL module is in turn represented by a function from a record
 -- of input port values to a record of output port values.
 yosys_import :: FilePath -> TopLevel SC.TypedTerm
-yosys_import path = do
-  sc <- getSharedContext
-  ir <- liftIO $ loadYosysIR path
-  tt <- liftIO $ yosysIRToRecordTerm sc ir
-  _ <- liftIO $ validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
-  pure tt
+yosys_import path =
+  do sc <- getSharedContext
+     ir <- liftIO $ loadYosysIR path
+     tt <- liftIO $ yosysIRToRecordTerm sc ir
+     _ <- liftIO $ validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
+     pure tt
 
 -- | Proves equality between a combinational HDL module and a
 -- specification. Note that terms derived from HDL modules are first
@@ -187,31 +186,32 @@ yosys_verify ::
   [YosysTheorem] {- ^ Overrides to apply -} ->
   ProofScript () ->
   TopLevel YosysTheorem
-yosys_verify ymod preconds other specs tactic = do
-  sc <- getSharedContext
-  newmod <- liftIO $ foldM (flip $ applyOverride sc)
-    (SC.ttTerm ymod)
-    specs
-  mpc <- case preconds of
-    [] -> pure Nothing
-    (pc:pcs) -> do
-      t <- foldM (\a b -> liftIO $ SC.scAnd sc a b) (SC.ttTerm pc) (SC.ttTerm <$> pcs)
-      pure . Just $ SC.TypedTerm (SC.ttType pc) t
-  thm <- liftIO $ buildTheorem sc ymod newmod mpc other
-  prop <- liftIO $ theoremProp sc thm
-  _ <- Builtins.provePrintPrim tactic prop
-  pure thm
+yosys_verify ymod preconds other specs tactic =
+  do sc <- getSharedContext
+     newmod <- liftIO $ foldM (flip $ applyOverride sc)
+       (SC.ttTerm ymod)
+       specs
+     mpc <-
+       case preconds of
+         [] -> pure Nothing
+         (pc:pcs) ->
+           do t <- foldM (\a b -> liftIO $ SC.scAnd sc a b) (SC.ttTerm pc) (SC.ttTerm <$> pcs)
+              pure . Just $ SC.TypedTerm (SC.ttType pc) t
+     thm <- liftIO $ buildTheorem sc ymod newmod mpc other
+     prop <- liftIO $ theoremProp sc thm
+     _ <- Builtins.provePrintPrim tactic prop
+     pure thm
 
 -- | Import a single sequential HDL module. N.B. SAW expects the
 -- sequential module to exist entirely within a single Yosys module.
 yosys_import_sequential ::
   Text {- ^ Name of the HDL module -} ->
   FilePath {- ^ Path to the Yosys JSON file -} ->
   TopLevel YosysSequential
-yosys_import_sequential nm path = do
-  sc <- getSharedContext
-  ir <- liftIO $ loadYosysIR path
-  liftIO $ yosysIRToSequential sc ir nm
+yosys_import_sequential nm path =
+  do sc <- getSharedContext
+     ir <- liftIO $ loadYosysIR path
+     liftIO $ yosysIRToSequential sc ir nm
 
 -- | Extracts a term from the given sequential module with the state
 -- eliminated by iterating the term over the given concrete number of
@@ -223,23 +223,23 @@ yosys_extract_sequential ::
   YosysSequential ->
   Integer {- ^ Number of cycles to iterate term -} ->
   TopLevel SC.TypedTerm
-yosys_extract_sequential s n = do
-  sc <- getSharedContext
-  tt <- liftIO $ composeYosysSequential sc s n
-  _ <- liftIO $ validateTerm sc "composing a sequential term" $ SC.ttTerm tt
-  pure tt
+yosys_extract_sequential s n =
+  do sc <- getSharedContext
+     tt <- liftIO $ composeYosysSequential sc s n
+     _ <- liftIO $ validateTerm sc "composing a sequential term" $ SC.ttTerm tt
+     pure tt
 
 -- | Like `yosys_extract_sequential`, but the resulting term has an
 -- additional parameter to specify the initial state.
 yosys_extract_sequential_with_state ::
   YosysSequential ->
   Integer {- ^ Number of cycles to iterate term -} ->
   TopLevel SC.TypedTerm
-yosys_extract_sequential_with_state s n = do
-  sc <- getSharedContext
-  tt <- liftIO $ composeYosysSequentialWithState sc s n
-  _ <- liftIO $ validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
-  pure tt
+yosys_extract_sequential_with_state s n =
+  do sc <- getSharedContext
+     tt <- liftIO $ composeYosysSequentialWithState sc s n
+     _ <- liftIO $ validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
+     pure tt
 
 -- | Extracts a term from the given sequential module. This term has
 -- explicit fields for the state of the circuit in the input and
@@ -254,7 +254,7 @@ yosys_verify_sequential_sally ::
   SC.TypedTerm {- ^ A boolean function of three parameters: an 8-bit cycle counter, a record of "fixed" inputs, and a record of circuit outputs -} ->
   [Text] {- ^ Names of circuit inputs that are fixed -} ->
   TopLevel ()
-yosys_verify_sequential_sally s path q fixed = do
-  sc <- getSharedContext
-  sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
-  liftIO $ queryModelChecker sym sc s path q $ Set.fromList fixed
+yosys_verify_sequential_sally s path q fixed =
+  do sc <- getSharedContext
+     sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
+     liftIO $ queryModelChecker sym sc s path q $ Set.fromList fixed