From 7fc50a9cbb2ca43bb45ae877e95a96285fd9e483 Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Tue, 28 Mar 2017 16:29:21 -0700
Subject: [PATCH] Write out the typechecker prelude when necessary

Bundle the typechecker prelude (CryptolTC.z3) with the executable, so
that it's able to write it out and re-use it when necessary.

Fixes #404
---
 src/Cryptol/ModuleSystem/Base.hs |  2 +-
 src/Cryptol/Prelude.hs           | 25 +++++++++++++++++++++----
 src/Cryptol/TypeCheck/Monad.hs   | 13 ++++++-------
 3 files changed, 28 insertions(+), 12 deletions(-)

diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index b723c3a5..248b30be 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -215,7 +215,7 @@ findModule n = do
 
   handleNotFound =
     case n of
-      m | m == preludeName -> writePreludeContents
+      m | m == preludeName -> io writePreludeContents
       _ -> moduleNotFound n =<< getSearchPath
 
   -- generate all possible search paths
diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs
index 93cb943e..0d0f2aa9 100644
--- a/src/Cryptol/Prelude.hs
+++ b/src/Cryptol/Prelude.hs
@@ -8,13 +8,16 @@
 --
 -- Compile the prelude into the executable as a last resort
 
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Cryptol.Prelude (writePreludeContents) where
+module Cryptol.Prelude (
+  writePreludeContents,
+  writeTcPreludeContents,
+  ) where
 
-import Cryptol.ModuleSystem.Monad
 
 import System.Directory (getTemporaryDirectory)
 import System.IO (hClose, hPutStr, openTempFile)
@@ -25,10 +28,24 @@ preludeContents = [there|lib/Cryptol.cry|]
 
 -- | Write the contents of the Prelude to a temporary file so that
 -- Cryptol can load the module.
-writePreludeContents :: ModuleM FilePath
-writePreludeContents = io $ do
+writePreludeContents :: IO FilePath
+writePreludeContents = do
   tmpdir <- getTemporaryDirectory
   (path, h) <- openTempFile tmpdir "Cryptol.cry"
   hPutStr h preludeContents
   hClose h
   return path
+
+
+cryptolTcContents :: String
+cryptolTcContents = [there|lib/CryptolTC.z3|]
+
+-- | Write the contents of the Prelude to a temporary file so that
+-- Cryptol can load the module.
+writeTcPreludeContents :: IO FilePath
+writeTcPreludeContents = do
+  tmpdir <- getTemporaryDirectory
+  (path, h) <- openTempFile tmpdir "CryptolTC.z3"
+  hPutStr h cryptolTcContents
+  hClose h
+  return path
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
index e6a860a2..ff663f50 100644
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -19,6 +19,7 @@ module Cryptol.TypeCheck.Monad
 import           Cryptol.ModuleSystem.Name (FreshM(..),Supply)
 import           Cryptol.Parser.Position
 import qualified Cryptol.Parser.AST as P
+import           Cryptol.Prelude (writeTcPreludeContents)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Subst
 import           Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
@@ -34,8 +35,7 @@ import qualified Data.Map as Map
 import qualified Data.Set as Set
 import           Data.Map (Map)
 import           Data.Set (Set)
-import           Data.List(find, minimumBy, groupBy, sortBy, foldl',
-                           intercalate)
+import           Data.List(find, minimumBy, groupBy, sortBy, foldl')
 import           Data.Maybe(mapMaybe)
 import           Data.Function(on)
 import           MonadLib hiding (mapM)
@@ -168,11 +168,10 @@ runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
   -- The actual order does not matter
   cmpRange (Range x y z) (Range a b c) = compare (x,y,z) (a,b,c)
 
-  loadCryTCPrel _ [] =
-    panic "runInferM" [ "Failed to find file: CryptolTC.z3"
-                      , "Searched paths: " ++
-                        intercalate ":" (inpSearchPath info)
-                      ]
+  loadCryTCPrel s [] =
+    do file <- writeTcPreludeContents
+       CrySAT.loadFile s file
+
   loadCryTCPrel s (p : ps) =
     do let file = p </> "CryptolTC.z3"
        yes <- doesFileExist file