Merge pull request #2464 from ucsd-progsys/fd/lhname-measure-names3

Simplify representation of measure names

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

@@ -135,7 +135,7 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
           exportedAssumption _ = True
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
-    ghcSpecToLiftedSpec = toLiftedSpec lnameEnv . toBareSpecLHName cfg lnameEnv . _gsLSpec
+    ghcSpecToLiftedSpec = toLiftedSpec . toBareSpecLHName cfg lnameEnv . _gsLSpec
 
 
 -------------------------------------------------------------------------------------
@@ -1210,12 +1210,14 @@ makeMeasEnv env tycEnv sigEnv specs = do
   let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
   let cms      = Bare.makeClassMeasureSpec measures
   let cms'     = [ (val l, cSort t <$ l)  | (l, t) <- cms ]
-  let ms'      = [ (F.val lx, F.atLoc lx t) | (lx, t) <- ms
-                                            , Mb.isNothing (lookup (val lx) cms') ]
+  let ms'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t)
+                 | (lx, t) <- ms
+                 , Mb.isNothing (lookup (val lx) cms')
+                 ]
   let cs'      = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (datacons ++ cls)]
   return Bare.MeasEnv
     { meMeasureSpec = measures
-    , meClassSyms   = cms'
+    , meClassSyms   = map (first logicNameToSymbol) cms'
     , meSyms        = ms'
     , meDataCons    = cs'
     , meClasses     = cls
@@ -1256,7 +1258,7 @@ addOpaqueReflMeas cfg tycEnv env spec measEnv specs eqs = do
   -- `meSyms` (no class, data constructor or other stuff here).
   let measures = mconcat (Ms.mkMSpec' dcSelectors : measures0)
   let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
-  let ms'      = [ (F.val lx, F.atLoc lx t) | (lx, t) <- ms ]
+  let ms'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t) | (lx, t) <- ms ]
   let cs'      = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (val <$> datacons)]
   return $ measEnv <> mempty
     { Bare.meMeasureSpec = measures

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

@@ -94,7 +94,7 @@ checkBareSpec sp
     inlines   = S.map (fmap getLHNameSymbol) (Ms.inlines sp)
     hmeasures = S.map (fmap getLHNameSymbol) (Ms.hmeas sp)
     reflects  = S.map (fmap getLHNameSymbol) (Ms.reflects sp)
-    measures  = msName    <$> Ms.measures sp
+    measures  = fmap getLHNameSymbol . msName <$> Ms.measures sp
     fields    = concatMap dataDeclFields (Ms.dataDecls sp)
 
 dataDeclFields :: DataDecl -> [F.LocSymbol]

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

@@ -78,10 +78,10 @@ makeMeasureDefinition allowTC tycEnv lmap cbs x =
   case L.find ((x ==) . makeGHCLHNameLocatedFromId . fst) cbs of
     Nothing ->
       Ex.throw $
-        errHMeas (fmap getLHNameSymbol x) "Cannot extract measure from haskell function"
+        errHMeas x "Cannot extract measure from haskell function"
     Just (v, cexp) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted allowTC (Ghc.varType v) mdef)
                      where
-                       vx           = F.atLoc x (F.symbol v)
+                       vx           = reflectLHName (Ghc.nameModule $ Ghc.getName v) <$> x
                        mdef         = coreToDef' allowTC tycEnv lmap vx v cexp
                        vinfo        = GM.varLocInfo (logicType allowTC) v
 
@@ -102,13 +102,14 @@ makeUnSorted allowTC ty defs
     isMeasureType (Ghc.TyConApp _ ts) = all Ghc.isTyVarTy ts
     isMeasureType _                   = False
 
-    defToUnSortedExpr defn = (xx:(fst <$> binds defn),
-                             Ms.bodyPred (F.mkEApp (measure defn) [F.expr xx]) (body defn))
+    defToUnSortedExpr defn =
+      (xx:(fst <$> binds defn),
+       Ms.bodyPred (F.eApps (F.EVar $ logicNameToSymbol $ F.val $ measure defn) [F.expr xx]) (body defn))
 
     xx = F.vv $ Just 10000
     isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred
 
-coreToDef' :: Bool -> Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
+coreToDef' :: Bool -> Bare.TycEnv -> LogicMap -> Located LHName -> Ghc.Var -> Ghc.CoreExpr
            -> [Def LocSpecType Ghc.DataCon]
 coreToDef' allowTC tycEnv lmap vx v defn =
   case runToLogic embs lmap dm (errHMeas vx) (coreToDef allowTC vx v defn) of
@@ -118,7 +119,7 @@ coreToDef' allowTC tycEnv lmap vx v defn =
     embs    = Bare.tcEmbs       tycEnv
     dm      = Bare.tcDataConMap tycEnv
 
-errHMeas :: LocSymbol -> String -> Error
+errHMeas :: Located LHName -> String -> Error
 errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
 
 --------------------------------------------------------------------------------
@@ -136,7 +137,7 @@ makeMeasureInline
   -> (LocSymbol, LMap)
 makeMeasureInline allowTC embs lmap cbs x =
   case L.find ((val x ==) . makeGHCLHNameFromId . fst) cbs of
-    Nothing        -> Ex.throw $ errHMeas (fmap getLHNameSymbol x) "Cannot inline haskell function"
+    Nothing        -> Ex.throw $ errHMeas x "Cannot inline haskell function"
     Just (v, defn) -> (vx, coreToFun' allowTC embs Nothing lmap vx v defn ok)
                      where
                        vx         = F.atLoc x (F.symbol v)
@@ -153,7 +154,7 @@ coreToFun' allowTC embs dmMb lmap x v defn ok = either Ex.throw ok act
   where
     act  = runToLogic embs lmap dm err xFun
     xFun = coreToFun allowTC x v defn
-    err  = errHMeas x
+    err  str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
     dm   = Mb.fromMaybe mempty dmMb
 
 
@@ -273,18 +274,19 @@ makeMeasureSelectors cfg dm (Loc l l' c)
       | isFunTy t && not (higherOrderFlag cfg)
       = Nothing
       | otherwise
-      = Just $ makeMeasureSelector (Loc l l' x) (projT i) dc n i
+        -- TODO: Use as origin module the module where the measure is created
+      = Just $ makeMeasureSelector (Loc l l' (makeGeneratedLogicLHName x)) (projT i) dc n i
 
     go' ((_,t), i)
       -- do not make selectors for functional fields
       | isFunTy t && not (higherOrderFlag cfg)
       = Nothing
       | otherwise
-      = Just $ makeMeasureSelector (Loc l l' (Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i
+      = Just $ makeMeasureSelector (Loc l l' (makeGeneratedLogicLHName $ Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i
 
     fields   = zip (reverse xts) [1..]
     n        = length xts
-    checker  = makeMeasureChecker (Loc l l' (Bare.makeDataConChecker dc)) checkT dc n
+    checker  = makeMeasureChecker (Loc l l' (makeGeneratedLogicLHName $ Bare.makeDataConChecker dc)) checkT dc n
     projT i  = dataConSel permitTC dc n (Proj i)
     checkT   = dataConSel permitTC dc n Check
     permitTC = typeclass cfg
@@ -330,14 +332,14 @@ bareBool = RApp (RTyCon Ghc.boolTyCon [] defaultTyConInfo) [] [] mempty
 
 -}
 
-makeMeasureSelector :: (Show a1) => LocSymbol -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
+makeMeasureSelector :: (Show a1) => Located LHName -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
 makeMeasureSelector x s dc n i = M { msName = x, msSort = s, msEqns = [eqn], msKind = MsSelector, msUnSorted = mempty}
   where
     eqn                        = Def x dc Nothing args (E (F.EVar $ mkx i))
     args                       = (, Nothing) . mkx <$> [1 .. n]
     mkx j                      = F.symbol ("xx" ++ show j)
 
-makeMeasureChecker :: LocSymbol -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
+makeMeasureChecker :: Located LHName -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
 makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns <$> filter (/= dc) dcs), msKind = MsChecker, msUnSorted = mempty }
   where
     s       = F.notracepp ("makeMeasureChecker: " ++ show x) s0
@@ -349,7 +351,7 @@ makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns
 
 
 ----------------------------------------------------------------------------------------------
-makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
+makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(Located LHName, RRType F.Reft)])
 ----------------------------------------------------------------------------------------------
 makeMeasureSpec' allowTC mspec0 = (ctorTys, measTys)
   where
@@ -435,6 +437,7 @@ makeOpaqueReflMeasures :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs ->
 makeOpaqueReflMeasures env measEnv specs eqs =
   unzip $ createMeasureForVar <$> S.toList (varsUndefinedInLogic `S.union` requestedOpaqueRefl)
   where
+    thisModule = Ghc.tcg_mod (Bare.reTcGblEnv env)
     -- Get the set of variables for the requested opaque reflections
     requestedOpaqueRefl = S.unions
       . map (S.map getVar . Ms.opaqueReflects . snd)
@@ -453,7 +456,7 @@ makeOpaqueReflMeasures env measEnv specs eqs =
     createMeasureForVar var =
       (Ms.mkMSpec' [smeas], (var, bmeas))
       where
-        locSym = F.atLoc (loc specType) (F.symbol var)
+        locSym = F.atLoc (loc specType) (reflectLHName thisModule $ makeGHCLHNameFromId var)
         specType = varSpecType var
         bareType = varBareType var
         bmeas = M locSym bareType [] MsReflect []
@@ -604,7 +607,7 @@ isSimpleType :: Ghc.Type -> Bool
 isSimpleType = isFirstOrder . RT.typeSort mempty
 
 makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
-                     -> [(LocSymbol, CMeasure (RType c tv r2))]
+                     -> [(Located LHName, CMeasure (RType c tv r2))]
 makeClassMeasureSpec Ms.MSpec{..} = tx <$> M.elems cmeasMap
   where
     tx (M n s _ _ _) = (n, CM n (mapReft ur_reft s))

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

@@ -136,7 +136,7 @@ getGlobalSyms (_, spec)
       ++ (mbName <$> imeasures spec)
       ++ (mbName <$> omeasures spec)
   where
-    mbName = F.val . msName
+    mbName = logicNameToSymbol . F.val . msName
 
 makeLocalVars :: [Ghc.CoreBind] -> LocalVars
 makeLocalVars = localVarMap . localBinds
@@ -392,7 +392,7 @@ instance Qualify RTyCon where
 
 instance Qualify (Measure SpecType Ghc.DataCon) where
   qualify env name _ bs m = m -- FIXME substEnv env name bs $
-    { msName = qualify env name l bs     lname
+    { msName = updateLHNameSymbol (qualify env name l bs) <$> lname
     , msEqns = qualify env name l bs <$> msEqns m
     }
     where
@@ -951,7 +951,7 @@ lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
       LHNResolved rn _ -> case rn of
         LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a local name: " ++ show c0
         LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a LHRIndex " ++ show i
-        LHRLogic (LogicName s _ _) -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show s
+        LHRLogic _ -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show (logicNameToSymbol c0)
         LHRGHC n ->
           Ghc.reflectGhc (Interface.lookupTyThing (gtleTypeEnv env) n) (gtleSession env)
 

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

@@ -131,22 +131,25 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
             -- A generic traversal that resolves names of Haskell entities
             sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $
                      fixExpressionArgsOfTypeAliases taliases bareSpec0
-            -- Now we do a second traversal to resolve logic names
-            let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
-                  makeLogicEnvs impMods thisModule sp1 dependencies
-            sp2 <- fromBareSpecLHName <$>
-                     resolveLogicNames
-                       cfg
-                       inScopeEnv
-                       globalRdrEnv
-                       unhandledNames
-                       lmap
-                       localVars
-                       logicNameEnv0
-                       privateReflectNames
-                       thisModule
-                       sp1
-            return (sp2, logicNameEnv0)
+            (es0,_) <- get
+            if null es0 then do
+              -- Now we do a second traversal to resolve logic names
+              let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
+                    makeLogicEnvs impMods thisModule sp1 dependencies
+              sp2 <- fromBareSpecLHName <$>
+                       resolveLogicNames
+                         cfg
+                         inScopeEnv
+                         globalRdrEnv
+                         unhandledNames
+                         lmap
+                         localVars
+                         logicNameEnv0
+                         privateReflectNames
+                         sp1
+              return (sp2, logicNameEnv0)
+            else
+              return (error "resolveLHNames: invalid spec", error "resolveLHNames: invalid logic environment")
         logicNameEnv' = extendLogicNameEnv logicNameEnv ns
     if null es then
       Right (bs, logicNameEnv')
@@ -172,8 +175,12 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
         | otherwise ->
             lookupGRELHName ns lname s
               (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
+      LHNUnresolved LHLogicNameBinder s ->
+        pure $ makeLogicLHName s thisModule Nothing
+      n@(LHNUnresolved LHLogicName _) ->
+        -- This one will be resolved by resolveLogicNames
+        pure n
       LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe
-      n@(LHNResolved (LHRLocal _) _) -> pure n
       n -> pure n
 
     lookupGRELHName ns lname s localNameLookup =
@@ -215,6 +222,8 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
       LHDataConName lcl -> lcl == LHThisModuleNameF
       LHVarName lcl -> lcl == LHThisModuleNameF
       LHTcName -> False
+      LHLogicNameBinder -> False
+      LHLogicName -> False
 
     nameSpaceKind :: LHNameSpace -> PJ.Doc
     nameSpaceKind = \case
@@ -223,6 +232,8 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
       LHDataConName LHThisModuleNameF -> "locally-defined data constructor"
       LHVarName LHAnyModuleNameF -> "variable"
       LHVarName LHThisModuleNameF -> "variable from the current module"
+      LHLogicNameBinder -> "logic name binder"
+      LHLogicName -> "logic name"
 
     tupleArity s =
       let a = read $ drop 5 $ symbolString s
@@ -268,11 +279,15 @@ mkLookupGRE ns s =
         , GHC.lookupVariablesForFields = True
         , GHC.lookupTyConsAsWell = False
         }
+      LHLogicNameBinder -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicNameBinder"
+      LHLogicName -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicName"
 
     mkGHCNameSpace = \case
       LHTcName -> GHC.tcName
       LHDataConName _ -> GHC.dataName
       LHVarName _ -> GHC.Types.Name.Occurrence.varName
+      LHLogicNameBinder -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicNameBinder"
+      LHLogicName -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicName"
 
 -- | Changes unresolved names to local resolved names in the body of type
 -- aliases.
@@ -441,8 +456,8 @@ makeLogicEnvs impAvails thisModule spec dependencies =
               , HS.toList (hmeas spec)
               ]
             ]
-          , [ makeLogicLHName (val (msName m)) thisModule Nothing | m <- measures spec ]
-          , [ makeLogicLHName (val (msName m)) thisModule Nothing | m <- cmeasures spec ]
+          , [ val (msName m) | m <- measures spec ]
+          , [ val (msName m) | m <- cmeasures spec ]
           ]
         privateReflectNames =
           mconcat $
@@ -523,8 +538,8 @@ collectUnhandledLiftedSpecLogicNames sp =
 collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
 collectLiftedSpecLogicNames sp = concat
     [ map fst (HS.toList $ liftedExpSigs sp)
-    , map (fst . snd) (HM.toList $ liftedMeasures sp)
-    , map (fst . snd) (HM.toList $ liftedCmeasures sp)
+    , map (val . msName) (HM.elems $ liftedMeasures sp)
+    , map (val . msName) (HM.elems $ liftedCmeasures sp)
     ]
 
 -- | Resolves names in the logic namespace
@@ -541,28 +556,25 @@ resolveLogicNames
   -> LocalVars
   -> LogicNameEnv
   -> HS.HashSet LocSymbol
-  -> GHC.Module
   -> BareSpecParsed
   -> State RenameOutput BareSpecLHName
-resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames thisModule sp = do
+resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames sp = do
     -- Instance measures must be defined for names of class measures.
     -- The names of class measures should be in @env@
-    imeasures <- mapM (mapMeasureNamesM (\lx -> (<$ lx) . logicNameToSymbol <$> resolveLogicName [] lx)) (imeasures sp)
+    imeasures <- mapM (mapMeasureNamesM resolveIMeasLogicName) (imeasures sp)
     emapSpecM
       (bscope cfg)
       (map localVarToSymbol . maybe [] lvdLclEnv . (GHC.lookupNameEnv (lvNames localVars) <=< getLHGHCName))
       resolveLogicName
       (emapBareTypeVM (bscope cfg) resolveLogicName)
-      sp { -- Measures and cmeasures aren't parametric on the type used for
-           -- logic names. We make sure that they are properly qualified here.
-           measures = runIdentity $ mapM (mapMeasureNamesM (return . fmap qualifyName)) (measures sp)
-         , cmeasures = runIdentity $ mapM (mapMeasureNamesM (return . fmap qualifyName)) (cmeasures sp)
-         , imeasures
-         }
+      sp { imeasures }
   where
-    localVarToSymbol = F.symbol . GHC.occNameString . GHC.nameOccName . GHC.varName
+    resolveIMeasLogicName lx =
+      case val lx of
+        LHNUnresolved LHLogicName s -> (<$ lx) <$> resolveLogicName [] (s <$ lx)
+        _ -> panic (Just $ LH.fSrcSpan lx) $ "unexpected name: " ++ show lx
 
-    qualifyName = LH.qualifySymbol (symbol $ GHC.moduleNameString $ GHC.moduleName thisModule)
+    localVarToSymbol = F.symbol . GHC.occNameString . GHC.nameOccName . GHC.varName
 
     resolveLogicName :: [Symbol] -> LocSymbol -> State RenameOutput LHName
     resolveLogicName ss ls
@@ -688,7 +700,7 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
     findReflection :: GHC.Name -> Maybe LHName
     findReflection n = GHC.lookupNameEnv (lneReflected lnameEnv) n
 
-mapMeasureNamesM :: Monad m => (LocSymbol -> m LocSymbol) -> MeasureV v ty ctor -> m (MeasureV v ty ctor)
+mapMeasureNamesM :: Monad m => (Located LHName -> m (Located LHName)) -> MeasureV v ty ctor -> m (MeasureV v ty ctor)
 mapMeasureNamesM f m = do
     msName <- f (msName m)
     msEqns <- mapM mapDefNameM (msEqns m)