Scaffolding for persisting resolution of logic names

liquidhaskell-boot/liquidhaskell-boot.cabal

@@ -125,6 +125,7 @@ library
                     , Diff                 >= 0.3 && < 0.6
                     , array
                     , aeson
+                    , base64
                     , binary
                     , bytestring           >= 0.10
                     , Cabal

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -506,6 +506,7 @@ import GHC.Tc.Types                   as Ghc
     , TcGblEnv
         ( tcg_anns
         , tcg_exports
+        , tcg_imports
         , tcg_insts
         , tcg_mod
         , tcg_rdr_env
@@ -641,6 +642,11 @@ import GHC.Types.Name                 as Ghc
     , occNameString
     , stableNameCmp
     )
+import GHC.Types.Name.Env             as Ghc
+    ( NameEnv
+    , lookupNameEnv
+    , mkNameEnvWith
+    )
 import GHC.Types.Name.Set             as Ghc
     ( NameSet
     , elemNameSet
@@ -757,6 +763,7 @@ import GHC.Unit.Module                as Ghc
     , IsBootInterface(NotBoot, IsBoot)
     , ModuleNameWithIsBoot
     , UnitId
+    , lookupModuleEnv
     , stableModuleCmp
     , fsToUnit
     , mkModuleNameFS
@@ -765,6 +772,13 @@ import GHC.Unit.Module                as Ghc
     , toUnitId
     , unitString
     )
+import GHC.Unit.Module.Deps       as Ghc
+    ( ImportAvails(imp_mods) )
+import GHC.Unit.Module.Imported       as Ghc
+    ( ImportedMods
+    , ImportedModsVal(imv_name, imv_qualified)
+    , importedByUser
+    )
 import GHC.Unit.Module.ModGuts        as Ghc
     ( ModGuts
       ( mg_binds
@@ -776,6 +790,10 @@ import GHC.Unit.Module.ModGuts        as Ghc
       , mg_usages
       )
     )
+import GHC.Unit.Types                 as Ghc
+    ( moduleUnitId
+    , unitIdString
+    )
 import GHC.Utils.Binary               as Ghc
     ( Binary(get, put_)
     , getByte

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -35,6 +35,7 @@ import qualified Language.Haskell.Liquid.Misc               as Misc -- (nubHashO
 import qualified Language.Haskell.Liquid.GHC.Misc           as GM
 import qualified Liquid.GHC.API            as Ghc
 import           Language.Haskell.Liquid.GHC.Types          (StableName)
+import           Language.Haskell.Liquid.LHNameResolution   (LogicNameEnv, toBareSpecLHName)
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Names
@@ -84,12 +85,13 @@ to disk so that we can retrieve it later without having to re-check the relevant
 -- to treat warnings and errors).
 makeTargetSpec :: Config
                -> Bare.LocalVars
+               -> LogicNameEnv
                -> LogicMap
                -> TargetSrc
                -> BareSpec
                -> TargetDependencies
                -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
-makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
+makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
   let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
   let bareSpecDiagnostics = Bare.checkBareSpec bareSpec
@@ -104,14 +106,15 @@ makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
       case diagOrSpec of
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
-          let (targetSpec, liftedSpec) = toTargetSpec ghcSpec
+          let targetSpec = toTargetSpec ghcSpec
+              liftedSpec = ghcSpecToLiftedSpec ghcSpec
           liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
-    toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
-    toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), unsafeFromLiftedSpec ls)
+    toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, BareSpec)
+    toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), fromBareSpecLHName $ unsafeFromLiftedSpec ls)
 
-    legacyDependencies :: [(ModName, Ms.BareSpec)]
+    legacyDependencies :: [(ModName, BareSpec)]
     legacyDependencies = map toLegacyDep . M.toList . getDependencies $ dependencies
 
     -- Assumptions about local functions that are not exported aren't useful for
@@ -127,6 +130,9 @@ makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do
           exportedAssumption _ = True
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
+    ghcSpecToLiftedSpec = toLiftedSpec . toBareSpecLHName cfg lnameEnv . _gsLSpec
+
+
 -------------------------------------------------------------------------------------
 -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
 --   validates it using @checkGhcSpec@.
@@ -149,7 +155,7 @@ makeGhcSpec cfg localVars src lmap targetSpec dependencySpecs = do
                                          (toTargetSrc src)
                                          (ghcSpecEnv sp)
                                          (_giCbs src)
-                                         (fst . toTargetSpec $ sp)
+                                         (toTargetSpec sp)
   pure $ if not (noErrors dg0) then Left dg0 else
            case diagnostics of
              Left dg1
@@ -476,7 +482,7 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
                    ++ (fst <$> Bare.meSyms measEnv)
                    ++ (fst <$> Bare.meClassSyms measEnv)
 
-makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty) -> [F.Qualifier]
+makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec F.Symbol ty) -> [F.Qualifier]
 makeQualifiers env tycEnv (modn, spec)
   = fmap        (Bare.qualifyTopDummy env        modn)
   . Mb.mapMaybe (resolveQParams       env tycEnv modn)
@@ -574,7 +580,7 @@ makeRewrite env spec =
 makeRewriteWith :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
 makeRewriteWith env spec = M.fromList <$> makeRewriteWith' env spec
 
-makeRewriteWith' :: Bare.Env -> Spec ty -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
+makeRewriteWith' :: Bare.Env -> Spec lname ty -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
 makeRewriteWith' env spec =
   forM (M.toList $ Ms.rewriteWith spec) $ \(x, xs) -> do
     xv  <- Bare.lookupGhcIdLHName env x
@@ -917,7 +923,9 @@ allAsmSigs env myName specs = do
       -- constraints should account instead for what logic functions are used in
       -- the constraints, which should be easier to do when precise renaming has
       -- been implemented for expressions and reflected functions.
-    , isUsedExternalVar v || isInScope v || isLocalVar v
+    , isUsedExternalVar v ||
+      isInScope v ||
+      isNonTopLevelVar v -- Keep assumptions about non-top-level bindings
     ]
   where
     isUsedExternalVar :: Ghc.Var -> Bool
@@ -942,7 +950,7 @@ allAsmSigs env myName specs = do
             Ghc.DataConWorkId dc -> inScope dc
             _ -> inScope v0
 
-    isLocalVar = Mb.isNothing . Ghc.nameModule_maybe . Ghc.getName
+    isNonTopLevelVar = Mb.isNothing . Ghc.nameModule_maybe . Ghc.getName
 
 getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, Located LHName, LocBareType)]
 getAsmSigs myName name spec

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs

@@ -23,7 +23,6 @@ import           Liquid.GHC.API                   as Ghc hiding ( Located
                                                                                  , empty
                                                                                  )
 import           Control.Applicative                       ((<|>))
-import           Control.Arrow                             ((&&&))
 import           Data.Maybe
 import           Data.Function                             (on)
 import           Text.PrettyPrint.HughesPJ                 hiding ((<>))
@@ -41,7 +40,6 @@ import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.PredType
-import           Language.Haskell.Liquid.Types.PrettyPrint
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Types.RefType
 import           Language.Haskell.Liquid.Types.RTypeOp
@@ -249,15 +247,6 @@ checkSigTExpr allowHO bsc emb tcEnv env (x, (t, es))
     mbErr2 = maybe emptyDiagnostics (checkTerminationExpr emb env . (x, t,)) es
     -- mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es
 
-_checkQualifiers :: F.SEnv F.SortedReft -> [F.Qualifier] -> [Error]
-_checkQualifiers = mapMaybe . checkQualifier
-
-checkQualifier       :: F.SEnv F.SortedReft -> F.Qualifier -> Maybe Error
-checkQualifier env q =  mkE <$> checkSortFull (F.srcSpan q) γ F.boolSort  (F.qBody q)
-  where
-    γ                = L.foldl' (\e (x, s) -> F.insertSEnv x (F.RR s mempty) e) env (F.qualBinds q ++ wiredSortedSyms)
-    mkE              = ErrBadQual (GM.fSrcSpan q) (pprint $ F.qName q)
-
 -- | Used for termination checking. If we have no \"len\" defined /yet/ (for example we are checking
 -- 'GHC.Prim') then we want to skip this check.
 checkSizeFun :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [TyConP] -> Diagnostics
@@ -283,41 +272,6 @@ checkSizeFun emb env tys = mkDiagnostics mempty (map mkError (mapMaybe go tys))
     isWiredInLenFn IdSizeFun           = False
     isWiredInLenFn (SymSizeFun locSym) = isWiredIn locSym
 
-_checkRefinedClasses :: [RClass LocBareType] -> [RInstance LocBareType] -> [Error]
-_checkRefinedClasses definitions instances
-  = mkError <$> duplicates
-  where
-    duplicates
-      = mapMaybe (checkCls . rcName) definitions
-    checkCls cls
-      = case findConflicts cls of
-          []        -> Nothing
-          conflicts -> Just (cls, conflicts)
-    findConflicts cls
-      = filter ((== cls) . riclass) instances
-    mkError (cls, conflicts)
-      = ErrRClass (GM.sourcePosSrcSpan $ loc $ btc_tc cls)
-                  (pprint cls) (ofConflict <$> conflicts)
-    ofConflict
-      = GM.sourcePosSrcSpan . loc . btc_tc . riclass &&& pprint . ritype
-
-_checkDuplicateFieldNames :: [(DataCon, DataConP)]  -> [Error]
-_checkDuplicateFieldNames = mapMaybe go
-  where
-    go (d, dts)          = checkNoDups (dcpLoc dts) d (fst <$> dcpTyArgs dts)
-    checkNoDups l d xs   = mkError l d <$> _firstDuplicate xs
-
-    mkError l d x = ErrBadData (GM.sourcePosSrcSpan l)
-                             (pprint d)
-                             (text "Multiple declarations of record selector" <+> pprintSymbol x)
-
-_firstDuplicate :: Ord a => [a] -> Maybe a
-_firstDuplicate = go . L.sort
-  where
-    go (y:x:xs) | x == y    = Just x
-                | otherwise = go (x:xs)
-    go _                    = Nothing
-
 checkInv :: Bool
          -> BScope
          -> F.TCEmb TyCon

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -40,10 +40,9 @@ import qualified Text.PrettyPrint.HughesPJ as PJ
 import qualified Language.Fixpoint.Types               as F
 -- import qualified Language.Fixpoint.Types.Visitor       as F
 import qualified Language.Fixpoint.Misc                as Misc
-import           Language.Fixpoint.Types (Expr(..)) -- , Symbol, symbol)
+import           Language.Fixpoint.Types (Expr, ExprV(..), SourcePos) -- , Symbol, symbol)
 import qualified Language.Haskell.Liquid.GHC.Misc      as GM
 import qualified Liquid.GHC.API       as Ghc
-import           Language.Haskell.Liquid.LHNameResolution (exprArg)
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Names
@@ -58,6 +57,7 @@ import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare
 import qualified Language.Haskell.Liquid.Bare.Types    as Bare
 import qualified Language.Haskell.Liquid.Bare.Plugged  as Bare
 import           Language.Haskell.Liquid.UX.Config
+import qualified Text.Printf                           as Printf
 
 --------------------------------------------------------------------------------
 -- | `makeRTEnv` initializes the env needed to `expand` refinements and types,
@@ -422,9 +422,9 @@ expandRTAliasApp l (Loc la _ rta) args r = case isOK of
   where
     tsu       = zipWith (\α t -> (α, toRSort t, t)) αs ts
     esu       = F.mkSubst $ zip (F.symbol <$> εs) es
-    es        = exprArg l msg <$> es0
+    es        = exprArgFromBareType l msg <$> es0
     (ts, es0) = splitAt nαs args
-    (αs, εs)  = (BTV <$> rtTArgs rta, rtVArgs rta)
+    (αs, εs)  = (BTV . dummyLoc <$> rtTArgs rta, rtVArgs rta)
     targs     = takeWhile (not . isRExprArg) args
     eargs     = dropWhile (not . isRExprArg) args
 
@@ -447,6 +447,20 @@ expandRTAliasApp l (Loc la _ rta) args r = case isOK of
       | otherwise
       = Nothing
 
+-- | A copy of 'LHNameResolution.exprArg' tailored to the types needed in this
+-- module.
+exprArgFromBareType :: SourcePos -> String -> BareType -> Expr
+exprArgFromBareType l msg = go
+  where
+    go :: BareType -> Expr
+    go (RExprArg e)     = val e
+    go (RVar x _)       = EVar $ F.symbol x
+    go (RApp x [] [] _) = EVar (getLHNameSymbol $ val $ btc_tc x)
+    go (RApp f ts [] _) = F.eApps (EVar (getLHNameSymbol $ val $ btc_tc f)) (go <$> ts)
+    go (RAppTy t1 t2 _) = EApp (go t1) (go t2)
+    go z                = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg
+    sp                  = Just (GM.sourcePosSrcSpan l)
+
 isRExprArg :: RType c tv r -> Bool
 isRExprArg (RExprArg _) = True
 isRExprArg _            = False