refactor

ucsd-progsys · Dec 18, 2024 · 8960f82 · 8960f82
1 parent f6e6eca
commit 8960f82
Show file tree

Hide file tree

Showing 9 changed files with 24 additions and 23 deletions.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -64,6 +64,7 @@ import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
 
+
 {- $creatingTargetSpecs
 
 /Liquid Haskell/ operates on 'TargetSpec's, so this module provides a single function called
@@ -106,7 +107,6 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
         Right (warns, ghcSpec) -> do
           let targetSpec = toTargetSpec ghcSpec
               liftedSpec = ghcSpecToLiftedSpec ghcSpec
-
           liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -543,8 +543,12 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
-        depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = HM.map (\l -> LH.lhNameToResolvedSymbol <$> l) $ liftedDefines ls}) mempty $
-                       (HM.elems . getDependencies) dependencies
+        -- add defines from dependencies to the logical map
+        depsLogicMap =
+          foldr (\ls lmp ->
+                     lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
+                mempty $
+            (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -157,9 +157,10 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
               let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
                     makeLogicEnvs impMods thisModule sp2 dependencies
               -- Add resolved local defines to the logic map
-                  lmap1 = lmap <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> ( lhNameToResolvedSymbol $ F.val k
-                                                                                     , (fmap val v) { lmVar = lhNameToResolvedSymbol <$> k }
-                                                                                     )) $ defines sp2 }
+                  lmap1 = lmap <> mkLogicMap (HM.fromList $ (\(k , v) ->
+                                                                let k' = lhNameToResolvedSymbol <$> k in
+                                                                (F.val k', (val <$> v) { lmVar = k' }))
+                                                            <$> defines sp2)
               sp3 <- fromBareSpecLHName <$>
                        resolveLogicNames
                          cfg

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -1133,7 +1133,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
-  , Measure.defines    = [ toLMapV' d | Define d <- xs]
+  , Measure.defines    = [ toLMapV d | Define d <- xs]
   }
 
 -- | Parse a single top level liquid specification

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -43,9 +43,8 @@ import qualified Data.Text                               as Text
 import GHC.Generics
 import GHC.Show
 import GHC.Stack
-
 import Language.Fixpoint.Types
-import Language.Haskell.Liquid.GHC.Misc -- Symbolic GHC.Name
+import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 
 -- RJ: Please add docs

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -1034,5 +1034,5 @@ unsafeFromLiftedSpec a = Spec
   , dsize      = liftedDsize  a
   , bounds     = liftedBounds a
   , axeqs      = S.toList . liftedAxeqs $ a
-  , defines    = map (\p -> first (dummyLoc . makeLocalLHName) p) . M.toList . liftedDefines $ a
+  , defines    = map (first (dummyLoc . makeLocalLHName)) . M.toList . liftedDefines $ a
   }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLMapV, toLMapV', toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
+  , LogicMap(..), toLMapV, mkLogicMap, toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -274,14 +274,17 @@ type LMap = LMapV F.Symbol
 instance (Show v, Ord v, F.Fixpoint v) => Show (LMapV v) where
   show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
-toLMapV' :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
-toLMapV' (x, (ys, e)) = (x, LMap {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
+toLMapV :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
+toLMapV (x, (ys, e)) = (x, LMap {lmVar = getLHNameSymbol <$> x, lmArgs = ys, lmExpr = e})
 
-toLMapV :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
-toLMapV (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
+mkLogicMap :: M.HashMap Symbol LMap -> LogicMap
+mkLogicMap ls = mempty {lmSymDefs = ls}
 
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
-toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMapV ls}
+toLogicMap = mkLogicMap . M.fromList . map toLMapV0
+  where
+  toLMapV0 :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
+  toLMapV0 (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
 
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr

diff --git a/tests/pos/NumRefl.hs b/tests/pos/NumRefl.hs
@@ -1,8 +1,7 @@
 {-
 
 Without the
-  define GHC.Internal.Num.fromInteger x = (x)
-  define GHC.Num.Integer.IS x           = (x)
+  define fromInteger x = (x)
 
 this program crashes with:
 
@@ -21,10 +20,6 @@ Because the result type (Num p) => p cannot be decided to be a numeric type.
 module NumRefl where
 
 {-@ define fromInteger x = (x) @-}
--- {-@ define IS x          = (x) @-}
-
--- {-@ define GHC.Internal.Num.fromInteger x = (x) @-}
--- {-@ define GHC.Num.Integer.IS x           = (x) @-}
 
 {-@ reflect toNum @-}
 toNum :: Num p => () -> p

diff --git a/tests/tests.cabal b/tests/tests.cabal
@@ -1863,7 +1863,6 @@ executable unit-pos-3
 
     other-modules:
                       NumRefl
---                    , WithProofRefl
                     , Streams
                     , StrictPair0
                     , StrictPair1