From 8ac62bde1a298e6d07f3855d08801ecc3ffc86eb Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 22 Jan 2025 13:05:13 -0500
Subject: [PATCH] cli, concurrency, syntax: Pretty-print syntax errors

---
 crucible-cli/src/Lang/Crucible/CLI.hs            | 7 ++++---
 crucible-concurrency/crucible-concurrency.cabal  | 1 +
 crucible-concurrency/src/Cruces/CrucesMain.hs    | 4 ++--
 crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs | 5 ++---
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index 13fde1727..6bd0c8e27 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -27,6 +27,8 @@ import Data.Map (Map)
 import Data.Text (Text)
 import Data.String (IsString(..))
 import qualified Data.Text.IO as T
+import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.Text as PP
 import System.IO
 import System.Exit
 import Text.Megaparsec as MP
@@ -43,7 +45,6 @@ import Lang.Crucible.CFG.SSAConversion
 
 import Lang.Crucible.Syntax.Atoms
 import Lang.Crucible.Syntax.Concrete
-import Lang.Crucible.Syntax.ExprParse (printSyntaxError)
 import Lang.Crucible.Syntax.Prog (doParseCheck, assertNoExterns, assertNoForwardDecs)
 import Lang.Crucible.Syntax.SExpr
 
@@ -139,8 +140,8 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
             let hdls = [ (SomeHandle h, p) | (FnBinding h _,p) <- ovrs ]
             parseResult <- top ng ha hdls $ prog v
             case parseResult of
-              Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
-              Left err -> hPutStrLn outh $ show err
+              Left e ->
+                T.hPutStrLn outh (PP.renderStrict (PP.layoutPretty PP.defaultLayoutOptions (PP.pretty e)))
               Right (ParsedProgram{ parsedProgCFGs = cs
                                   , parsedProgExterns = externs
                                   , parsedProgForwardDecs = fds
diff --git a/crucible-concurrency/crucible-concurrency.cabal b/crucible-concurrency/crucible-concurrency.cabal
index 1f4e07031..0c3122cb2 100644
--- a/crucible-concurrency/crucible-concurrency.cabal
+++ b/crucible-concurrency/crucible-concurrency.cabal
@@ -39,6 +39,7 @@ library
                      , megaparsec
                      , mtl
                      , parameterized-utils
+                     , prettyprinter
                      , simple-get-opt < 0.5
                      , text
                      , vector
diff --git a/crucible-concurrency/src/Cruces/CrucesMain.hs b/crucible-concurrency/src/Cruces/CrucesMain.hs
index a5604f072..e493bd1d9 100644
--- a/crucible-concurrency/src/Cruces/CrucesMain.hs
+++ b/crucible-concurrency/src/Cruces/CrucesMain.hs
@@ -20,6 +20,7 @@ import Data.List (find)
 import qualified Data.Map as Map
 import Data.Text (pack)
 import Data.String (IsString(..))
+import qualified Prettyprinter as PP
 import System.Exit
 import Text.Megaparsec as MP
 
@@ -138,8 +139,7 @@ run (cruxOpts, opts) =
                      let ?parserHooks = defaultParserHooks
                      parseResult <- top nonceGen ha builtins $ prog v
                      case parseResult of
-                       Left (SyntaxParseError e) -> error $ show $ printSyntaxError e
-                       Left err -> error $ show err
+                       Left err -> error (show (PP.pretty err))
                        Right (ParsedProgram
                                { parsedProgGlobals = gs
                                , parsedProgExterns = externs
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
index 93395a967..d19f41ee4 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
@@ -17,6 +17,7 @@ import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Text (Text)
 import qualified Data.Text.IO as T
+import qualified Prettyprinter as PP
 import System.IO
 import System.Exit
 import Text.Megaparsec as MP
@@ -31,7 +32,6 @@ import Lang.Crucible.CFG.SSAConversion
 
 import Lang.Crucible.Syntax.Concrete
 import Lang.Crucible.Syntax.SExpr
-import Lang.Crucible.Syntax.ExprParse (printSyntaxError)
 import Lang.Crucible.Syntax.Atoms
 
 import Lang.Crucible.Analysis.Postdom
@@ -72,8 +72,7 @@ doParseCheck fn theInput pprint outh =
                 \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh ""
             cs <- top ng ha [] $ prog v
             case cs of
-              Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
-              Left err -> hPutStrLn outh $ show err
+              Left err -> hPutStrLn outh (show (PP.pretty err))
               Right (ParsedProgram{ parsedProgCFGs = ok
                                   , parsedProgExterns = externs
                                   , parsedProgForwardDecs = fds