From b5d6715b21b5263e10cdb7cac20e4844c255efed Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Mon, 10 Jul 2017 16:58:33 -0700
Subject: [PATCH] Add support for comments; panic on completely bogus inputs.

Note that we still do not check for errors in commands, perhaps we should?
---
 src/Cryptol/TypeCheck/Solver/CrySAT.hs | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
index 6c0c290c..64c8c680 100644
--- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs
+++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
@@ -45,6 +45,7 @@ import           MonadLib
 import           Data.Maybe ( fromMaybe )
 import           Data.Map (Map)
 import qualified Data.Map as Map
+import           Data.Char(isSpace)
 import           Data.Foldable ( any, all )
 import qualified Data.Set as Set
 import           Data.IORef ( IORef, newIORef, readIORef, modifyIORef',
@@ -287,11 +288,20 @@ data Solver = Solver
 loadFile :: Solver -> FilePath -> IO ()
 loadFile s file = do -- txt <- readFile file
                      -- mapM_ putStrLn (lines txt)
-                     go =<< readFile file
+                     go . dropComments =<< readFile file
   where
-  go txt = case SMT.readSExpr txt of
-             Just (e,rest) -> SMT.command (solver s) e >> go rest
-             Nothing       -> return ()
+  go txt
+    | all isSpace txt = return ()
+    | otherwise = case SMT.readSExpr txt of
+                    Just (e,rest) -> SMT.command (solver s) e >> go rest
+                    Nothing       -> panic "loadFile" [ "Failed to parse SMT file."
+                                                      , txt
+                                                      ]
+
+  dropComments = unlines . map dropComment . lines
+  dropComment xs = case break (== ';') xs of
+                     (as,_:_) -> as
+                     _ -> xs
 
 rawSolver :: Solver -> SMT.Solver
 rawSolver = solver