Allow bare embeds and cmeasures into a LiftedSpec

This commit changes 'makeLiftedSpec0' so that we allow input 'embeds' and 'cmeasures' to survive the lifting process. Something to bear in mind in that probably we would have to adjust the format of the correspondent types, as it might make no sense to talk about a 'LocSymbol' for something serialised into an interface file.
YoshikiTakashima · May 5, 2020 · e705614 · e705614
1 parent d8f8545
commit e705614
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 23 deletions.
diff --git a/liquid-ghc-prim/src/GHC/Prim.hs b/liquid-ghc-prim/src/GHC/Prim.hs
@@ -1,5 +1,17 @@
 module GHC.Prim (module Exports) where
 
-{-@ embed GHC.Prim.Int# as int @-}
-{-@ class measure len :: forall f a. f a -> GHC.Prim.Int# @-}
+{-@ embed GHC.Prim.Int#     as int @-}
+{-@ embed GHC.Prim.Addr#    as Str @-}
+{-@ embed GHC.Prim.Char#    as Char @-}
+{-@ embed GHC.Prim.Double#  as real @-}
+{-@ embed GHC.Prim.Float#   as real @-}
+{-@ embed GHC.Prim.Word#    as int  @-}
+{-@ GHC.Prim.+#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y} @-}
+{-@ GHC.Prim.-#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y} @-}
+{-@ GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x = y} @-}
+{-@ GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x >= y} @-}
+{-@ GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x <= y} @-}
+{-@ GHC.Prim.<#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x < y}  @-}
+{-@ GHC.Prim.>#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x > y}  @-}
+
 import "ghc-prim" GHC.Prim as Exports
diff --git a/liquid-ghc-prim/src/GHC/Types.spec b/liquid-ghc-prim/src/GHC/Types.spec
@@ -12,14 +12,6 @@ embed GHC.Types.Char    as Char
 
 embed GHC.Integer.Type.Integer as int
 
-// Prim types
-embed GHC.Prim.Int#     as int
-embed GHC.Prim.Addr#    as Str
-embed GHC.Prim.Char#    as Char
-embed GHC.Prim.Double#  as real
-embed GHC.Prim.Float#   as real
-embed GHC.Prim.Word#    as int
-
 GHC.Types.True  :: {v:GHC.Types.Bool | v     }
 GHC.Types.False :: {v:GHC.Types.Bool | (~ v) }
 
@@ -37,12 +29,4 @@ type TT      = {v: GHC.Types.Bool | v}
 type FF      = {v: GHC.Types.Bool | not v}
 type String  = [GHC.Types.Char]
 
-assume GHC.Prim.+#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y}
-assume GHC.Prim.-#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y}
-assume GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x = y}
-assume GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x >= y}
-assume GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x <= y}
-assume GHC.Prim.<#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x < y}
-assume GHC.Prim.>#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x > y}
-
 class measure len :: forall f a. f a -> GHC.Types.Int
diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs
@@ -284,6 +284,14 @@ makeLiftedSpec0 cfg src embs lmap mySpec = mempty
   { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines src embs lmap mySpec 
   , Ms.reflects  = Ms.reflects mySpec
   , Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs  
+  , Ms.embeds    = Ms.embeds mySpec
+  -- We do want 'embeds' to survive and to be present into the final 'LiftedSpec'. The
+  -- caveat is to decide which format is more appropriate. We obviously cannot store
+  -- them as a 'TCEmb TyCon' as serialising a 'TyCon' would be fairly exponsive. This
+  -- needs more thinking.
+  , Ms.cmeasures = Ms.cmeasures mySpec
+  -- We do want 'cmeasures' to survive and to be present into the final 'LiftedSpec'. The
+  -- caveat is to decide which format is more appropriate. This needs more thinking.
   }
   where 
     tcs          = uniqNub (_gsTcs src ++ refTcs)

diff --git a/src/Language/Haskell/Liquid/GHC/Plugin.hs b/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -108,7 +108,7 @@ tcStableRef = unsafePerformIO $ newIORef emptyModuleEnv
 
 -- | Set to 'True' to enable debug logging.
 debugLogs :: Bool
-debugLogs = False
+debugLogs = True
 
 ---------------------------------------------------------------------------------
 -- | Useful functions -----------------------------------------------------------
@@ -195,7 +195,7 @@ parseHook _ modSummary parsedModule = do
 
   liftIO $ writeIORef unoptimisedRef (toUnoptimised unoptimisedGuts)
 
-  debugLog $ "Optimised Core:\n" ++ (O.showSDocUnsafe $ O.ppr (mg_binds unoptimisedGuts))
+  --debugLog $ "Optimised Core:\n" ++ (O.showSDocUnsafe $ O.ppr (mg_binds unoptimisedGuts))
 
   -- Resolve names and imports
   env <- askHscEnv
@@ -210,7 +210,7 @@ parseHook _ modSummary parsedModule = do
   let thisModule = ms_mod modSummary
   let stableData = mkTcData typechecked resolvedNames availTyCons availVars
 
-  debugLog $ "Resolved names:\n" ++ (O.showSDocUnsafe $ O.ppr resolvedNames)
+  --debugLog $ "Resolved names:\n" ++ (O.showSDocUnsafe $ O.ppr resolvedNames)
 
   -- Extend the 'ModuleEnv' held by the 'tcStableRef' with the data from this module.
   liftIO $ atomicModifyIORef' tcStableRef (\old -> (extendModuleEnv old thisModule stableData, ()))
@@ -445,8 +445,8 @@ processModule LiquidHaskellContext{..} = do
   forM_ (HM.keys . getDependencies $ dependencies) $ 
     debugLog . moduleStableString . unStableModule
 
-  debugLog $ "mg_exports => " ++ (O.showSDocUnsafe $ O.ppr $ mg_exports modGuts)
-  debugLog $ "mg_tcs => " ++ (O.showSDocUnsafe $ O.ppr $ mg_tcs modGuts)
+  --debugLog $ "mg_exports => " ++ (O.showSDocUnsafe $ O.ppr $ mg_exports modGuts)
+  --debugLog $ "mg_tcs => " ++ (O.showSDocUnsafe $ O.ppr $ mg_tcs modGuts)
 
   targetSrc  <- makeTargetSrc moduleCfg file lhModuleTcData modGuts hscEnv