heapster-saw: Export block entry-point and implication error information for IDE ingestion

heapster-saw/heapster-saw.cabal

@@ -37,22 +37,28 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
+    aeson ^>= 1.5,
+    th-abstraction,
+    template-haskell
   hs-source-dirs: src
   build-tool-depends:
     alex:alex,
     happy:happy,
   exposed-modules:
     Verifier.SAW.Heapster.CruUtil
     Verifier.SAW.Heapster.GenMonad
+    Verifier.SAW.Heapster.IDESupport
     Verifier.SAW.Heapster.Implication
     Verifier.SAW.Heapster.IRTTranslation
     Verifier.SAW.Heapster.Lexer
     Verifier.SAW.Heapster.Located
+    Verifier.SAW.Heapster.JSONExport
     Verifier.SAW.Heapster.ParsedCtx
     Verifier.SAW.Heapster.Parser
     Verifier.SAW.Heapster.Permissions
     Verifier.SAW.Heapster.PermParser
     Verifier.SAW.Heapster.NamePropagation
+    Verifier.SAW.Heapster.NamedMb
     Verifier.SAW.Heapster.RustTypes
     Verifier.SAW.Heapster.SAWTranslation
     Verifier.SAW.Heapster.Token

heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs

@@ -23,6 +23,7 @@ import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Reflection
 import Data.List.NonEmpty (NonEmpty(..))
+import Data.Functor.Constant
 import Data.ByteString
 import Numeric
 import Numeric.Natural
@@ -564,6 +565,15 @@ instance Liftable (KnownReprObj f a) where
 instance LiftableAny1 (KnownReprObj f) where
   mbLiftAny1 = mbLift
 
+instance Liftable a => LiftableAny1 (Constant a) where
+  mbLiftAny1 = mbLift
+
+instance Liftable a => Liftable (Constant a b) where
+  mbLift (mbMatch -> [nuMP| Data.Functor.Constant.Constant x |]) = Data.Functor.Constant.Constant (mbLift x)
+
+instance (Liftable a, Liftable b, Liftable c) => Liftable (a,b,c) where
+  mbLift (mbMatch -> [nuMP| (x,y,z) |]) = (mbLift x, mbLift y, mbLift z)
+
 -- FIXME: this change for issue #28 requires ClosableAny1 to be exported from
 -- Hobbits
 {-

heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs

@@ -8,17 +8,19 @@ module Verifier.SAW.Heapster.GenMonad (
   -- * Core definitions
   GenStateContT(..), (>>>=), (>>>),
   -- * Continuation operations
-  gcaptureCC, gmapRet, gabortM, gparallel, gopenBinding,
+  gcaptureCC, gmapRet, gabortM, gparallel, startBinding, startBinding', gopenBinding, gopenBinding',
   -- * State operations
   gmodify,
   -- * Transformations
   addReader,
   ) where
 
-import Data.Binding.Hobbits ( nuMultiWithElim1, Mb, Name, RAssign )
+import Data.Binding.Hobbits ( nuMulti, nuMultiWithElim1, Mb, Name, RAssign )
 import Control.Monad.State ( ap, MonadState(get, put) )
 import Control.Monad.Trans.Class ( MonadTrans(lift) )
 import Control.Monad.Trans.Reader
+import Data.Proxy
+import Verifier.SAW.Heapster.NamedMb
 
 -- | The generalized state-continuation monad
 newtype GenStateContT s1 r1 s2 r2 m a = GenStateContT {
@@ -107,6 +109,30 @@ gopenBinding f_ret mb_a =
   f_ret $ flip nuMultiWithElim1 mb_a $ \names a ->
   k (names, a)
 
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+gopenBinding' ::
+  (NMb ctx (m b1) -> m r2) ->
+  NMb ctx b2 ->
+  GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
+gopenBinding' f_ret mb_a =
+  gcaptureCC \k ->
+  f_ret $ flip nuMultiWithElim1N mb_a $ \names a ->
+  k (names, a)
+
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+startBinding ::
+  RAssign Proxy ctx ->
+  (Mb ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startBinding tps f_ret = gcaptureCC (f_ret . nuMulti tps)
+
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+startBinding' ::
+  RAssign StringF ctx ->
+  (NMb ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startBinding' tps f_ret = gcaptureCC (f_ret . nuMultiN tps)
+
 addReader :: GenStateContT s1 r1 s2 r2 m a -> GenStateContT s1 r1 s2 r2 (ReaderT e m) a
 addReader (GenStateContT m) =
   GenStateContT \s2 k ->