Merge pull request #2466 from ucsd-progsys/fd/resolve-field-names

Persist name resolution for field names

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

@@ -250,13 +250,13 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     , _gsRefl   = refl
     , _gsData   = sData
     , _gsQual   = qual
-    , _gsName   = makeSpecName env     tycEnv measEnv   name
+    , _gsName   = makeSpecName env     tycEnv measEnv
     , _gsVars   = spcVars
     , _gsTerm   = spcTerm
 
     , _gsLSpec  = finalLiftedSpec
                 { expSigs   =
-                    [ (logicNameToSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
+                    [ (lhNameToResolvedSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
                     | v <- gsReflects refl
                     ]
                 , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
@@ -317,14 +317,8 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
     simplifier = pure -- no simplification
     allowTC  = typeclass cfg
-    mySpec2  = Bare.qualifyExpand env name rtEnv l [] mySpec1    where l = F.dummyPos "expand-mySpec2"
-    iSpecs2  = Bare.qualifyExpand
-                 env
-                 name
-                 rtEnv
-                 (F.dummyPos "expand-iSpecs2")
-                 []
-                 (M.fromList dependencySpecs)
+    mySpec2  = Bare.expand rtEnv (F.dummyPos "expand-mySpec2") mySpec1
+    iSpecs2  = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs)
     rtEnv    = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap
     mspecs   = (name, mySpec0) : dependencySpecs
     (mySpec0, instMethods)  = if allowTC
@@ -436,7 +430,7 @@ reflectedVars spec cbs =
   where
     isReflSym x =
       S.member x (Ms.reflects spec) ||
-      S.member (fmap getLHNameSymbol x) (Ms.privateReflects spec)
+      S.member (fmap lhNameToResolvedSymbol x) (Ms.privateReflects spec)
 
 measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
 measureVars spec cbs =
@@ -496,10 +490,8 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
                    ++ (fst <$> Bare.meClassSyms measEnv)
 
 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)
-  $ Ms.qualifiers spec
+makeQualifiers env tycEnv (modn, spec) =
+    Mb.mapMaybe (resolveQParams env tycEnv modn) $ Ms.qualifiers spec
 
 
 -- | @resolveQualParams@ converts the sorts of parameters from, e.g.
@@ -639,22 +631,18 @@ makeSpecRefl src specs env name sig tycEnv = do
   autoInst <- makeAutoInst env mySpec
   rwr      <- makeRewrite env mySpec
   rwrWith  <- makeRewriteWith env mySpec
-  xtes     <- Bare.makeHaskellAxioms src env tycEnv name lmap sig mySpec
+  xtes     <- Bare.makeHaskellAxioms src env tycEnv lmap sig mySpec
   asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv sig mySpec
   let otherAxioms = thd3 <$> asmReflAxioms
   let myAxioms =
-        [ Bare.qualifyTop
-            env
-            name
-            (F.loc lt)
-            e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
-        | (_, lt, e) <- xtes
+        [ e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
+        | (_, _, e) <- xtes
         ] ++ otherAxioms
   let asmReflEls = eqName <$> otherAxioms
   let impAxioms  = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs)
   case anyNonReflFn of
     Just (actSym , preSym) ->
-      let preSym' = show (val preSym) in
+      let preSym' = symbolString $ lhNameToUnqualifiedSymbol (val preSym) in
       let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}"
       in Ex.throw
            (ErrHMeas
@@ -676,7 +664,7 @@ makeSpecRefl src specs env name sig tycEnv = do
     lmap         = Bare.reLMap env
     notInReflOnes (_, a) = not $
       a `S.member` Ms.reflects mySpec ||
-      fmap getLHNameSymbol a `S.member` Ms.privateReflects mySpec
+      fmap lhNameToResolvedSymbol a `S.member` Ms.privateReflects mySpec
     anyNonReflFn = L.find notInReflOnes (Ms.asmReflectSigs mySpec)
 
 ------------------------------------------------------------------------------------------
@@ -713,7 +701,7 @@ addReflSigs env name rtEnv measEnv refl sig =
     -- the functions, we are left with a pair (Var, LocSpecType). The latter /needs/ to be qualified and
     -- expanded again, for example in case it has expression aliases derived from 'inlines'.
     expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
-    expandReflectedSignature = fmap (Bare.qualifyExpand env name rtEnv (F.dummyPos "expand-refSigs") [])
+    expandReflectedSignature = fmap (Bare.expand rtEnv (F.dummyPos "expand-refSigs"))
 
     reflSigs = [ (x, t) | (x, t, _) <- gsHAxioms refl ]
     -- Get the set of all the actual functions (in assume-reflects)
@@ -811,7 +799,7 @@ makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec
            -> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])]
 makeTySigs env sigEnv name spec = do
   bareSigs   <- bareTySigs env                     spec
-  expSigs    <- makeTExpr  env name bareSigs rtEnv spec
+  expSigs    <- makeTExpr  env bareSigs rtEnv spec
   let rawSigs = Bare.resolveLocalBinds env expSigs
   return [ (x, cook x bt, z) | (x, bt, z) <- rawSigs ]
   where
@@ -858,24 +846,22 @@ myAsmSig v sigs = Mb.fromMaybe errImp (mbHome `mplus` mbImp)
     errImp      = impossible Nothing "myAsmSig: cannot happen as sigs is non-null"
     vName       = GM.takeModuleNames (F.symbol v)
 
-makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
+makeTExpr :: Bare.Env -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
           -> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
-makeTExpr env name tySigs rtEnv spec = do
+makeTExpr env tySigs rtEnv spec = do
   vExprs       <- M.fromList <$> makeVarTExprs env spec
   let vSigExprs = Misc.hashMapMapWithKey (\v t -> (t, M.lookup v vExprs)) vSigs
-  return [ (v, t, qual t <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
+  return [ (v, t, qual <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
   where
-    qual t es   = qualifyTermExpr env name rtEnv t <$> es
-    vSigs       = M.fromList tySigs
+    qual es = expandTermExpr rtEnv <$> es
+    vSigs = M.fromList tySigs
 
-qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
-                -> Located F.Expr
-qualifyTermExpr env name rtEnv t le
-        = F.atLoc le (Bare.qualifyExpand env name rtEnv l bs e)
+expandTermExpr :: BareRTEnv -> Located F.Expr -> Located F.Expr
+expandTermExpr rtEnv le
+        = F.atLoc le (Bare.expand rtEnv l e)
   where
     l   = F.loc le
     e   = F.val le
-    bs  = ty_binds . toRTypeRep . val $ t
 
 makeVarTExprs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
 makeVarTExprs env spec =
@@ -1012,7 +998,7 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
                        , let tt  = Bare.plugHoles (typeclass $ getConfig env) sigEnv name (Bare.LqTV x) t
                    ]
   , gsMeas       = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ]
-  , gsMeasures   = Bare.qualifyTopDummy env name <$> (ms1 ++ ms2)
+  , gsMeasures   = ms1 ++ ms2
   , gsOpaqueRefls = fst <$> Bare.meOpaqueRefl measEnv
   , gsInvariants = Misc.nubHashOn (F.loc . snd) invs
   , gsIaliases   = concatMap (makeIAliases env sigEnv) (M.toList specs)
@@ -1026,7 +1012,7 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
     ms2          = Ms.imeas   measuresSp
     mySpec       = M.lookupDefault mempty name specs
     name         = _giTargetMod      src
-    (minvs,usI)  = makeMeasureInvariants env name sig mySpec
+    (minvs,usI)  = makeMeasureInvariants sig mySpec
     invs         = minvs ++ concatMap (makeInvariants env sigEnv) (M.toList specs)
 
 makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
@@ -1058,19 +1044,18 @@ makeSizeInv s lst = lst{val = go (val lst)}
         nat  = MkUReft (Reft (vv_, PAtom Le (ECon $ I 0) (EApp (EVar s) (eVar vv_))))
                        mempty
 
-makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
-                      -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
-makeMeasureInvariants env name sig mySpec
+makeMeasureInvariants :: GhcSpecSig -> Ms.BareSpec -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
+makeMeasureInvariants sig mySpec
   = Mb.catMaybes <$>
-    unzip (measureTypeToInv env name <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs
+    unzip (measureTypeToInv <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs
                                          , x == makeGHCLHNameLocatedFromId y ])
   where
     sigs = gsTySigs sig
     xs   = S.toList (Ms.hmeas  mySpec)
 
-measureTypeToInv :: Bare.Env -> ModName -> (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
-measureTypeToInv env name (x, (v, t))
-  = notracepp "measureTypeToInv" ((Just v, t {val = Bare.qualifyTop env name (F.loc x) mtype}), usorted)
+measureTypeToInv :: (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
+measureTypeToInv (x, (v, t))
+  = notracepp "measureTypeToInv" ((Just v, t {val = mtype}), usorted)
   where
     trep = toRTypeRep (val t)
     rts  = ty_args  trep
@@ -1102,7 +1087,7 @@ mkReft :: Located LHName -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Exp
 mkReft x z _t tr
   | Just q <- stripRTypeBase tr
   = let Reft (v, p) = toReft q
-        su          = mkSubst [(v, mkEApp (fmap getLHNameSymbol x) [EVar v]), (z,EVar v)]
+        su          = mkSubst [(v, mkEApp (fmap lhNameToResolvedSymbol x) [EVar v]), (z,EVar v)]
         -- p'          = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p
     in  Just (v, subst su p)
 mkReft _ _ _ _
@@ -1111,12 +1096,12 @@ mkReft _ _ _ _
 
 -- REBARE: formerly, makeGhcSpec3
 -------------------------------------------------------------------------------------------
-makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
+makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> GhcSpecNames
 -------------------------------------------------------------------------------------------
-makeSpecName env tycEnv measEnv name = SpNames
+makeSpecName env tycEnv measEnv = SpNames
   { gsFreeSyms = Bare.reSyms env
   , gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
-  , gsTconsP   = Bare.qualifyTopDummy env name <$> tycons
+  , gsTconsP   = tycons
   -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
   , gsTcEmbeds = Bare.tcEmbs     tycEnv
   , gsADTs     = Bare.tcAdts     tycEnv
@@ -1154,7 +1139,7 @@ makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.
     (diag0, conTys) = withDiagnostics $ Bare.makeConTypes myName env specs
     specs         = (myName, mySpec) : M.toList iSpecs
     tcs           = Misc.snd3 <$> tcDds
-    tyi           = Bare.qualifyTopDummy env myName (makeTyConInfo embs fiTcs tycons)
+    tyi           = makeTyConInfo embs fiTcs tycons
     -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
     -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
     tycons        = tcs ++ knownWiredTyCons env myName
@@ -1210,14 +1195,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'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t)
+  let ms'      = [ (lhNameToResolvedSymbol (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   = map (first logicNameToSymbol) cms'
+    , meClassSyms   = map (first lhNameToResolvedSymbol) cms'
     , meSyms        = ms'
     , meDataCons    = cs'
     , meClasses     = cls
@@ -1258,7 +1243,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'      = [ (logicNameToSymbol (F.val lx), F.atLoc lx t) | (lx, t) <- ms ]
+  let ms'      = [ (lhNameToResolvedSymbol (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/Axiom.hs

@@ -62,12 +62,12 @@ findDuplicateBetweenLists key l1 l2 =
       [ (x, y) | x <- l2', Just y <- [Map.lookup (key' x) seen]]
 
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec
+makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> LogicMap -> GhcSpecSig -> Ms.BareSpec
                   -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms src env tycEnv name lmap spSig spec = do
+makeHaskellAxioms src env tycEnv lmap spSig spec = do
   let refDefs = getReflectDefs src spSig spec env
-  return (makeAxiom env tycEnv name lmap <$> refDefs)
+  return (makeAxiom env tycEnv lmap <$> refDefs)
 
 -----------------------------------------------------------------------------------------------
 --          Returns a list of elements, one per assume reflect                               --
@@ -84,7 +84,10 @@ makeAssumeReflectAxioms src env tycEnv spSig spec = do
   -- Send an error message if we're redefining a reflection
   case findDuplicatePair val reflActSymbols <|> findDuplicateBetweenLists val refSymbols reflActSymbols of
     Just (x , y) -> Ex.throw $ mkError y $
-                      "Duplicate reflection of " ++ show x ++ " and " ++ show y
+                      "Duplicate reflection of " ++
+                      show (lhNameToUnqualifiedSymbol <$> x) ++
+                      " and " ++
+                      show (lhNameToUnqualifiedSymbol <$> y)
     Nothing -> return $ turnIntoAxiom <$> Ms.asmReflectSigs spec
   where
     turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs (actual, pretended)
@@ -306,15 +309,14 @@ getExprFromUnfolding (Ghc.CoreUnfolding expr _ _ _ _) = Just expr
 getExprFromUnfolding _ = Nothing
 
 --------------------------------------------------------------------------------
-makeAxiom :: Bare.Env -> Bare.TycEnv -> ModName -> LogicMap
+makeAxiom :: Bare.Env -> Bare.TycEnv -> LogicMap
           -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
           -> (Ghc.Var, LocSpecType, F.Equation)
 --------------------------------------------------------------------------------
-makeAxiom env tycEnv name lmap (x, mbT, v, def)
+makeAxiom env tycEnv lmap (x, mbT, v, def)
             = (v, t, e)
   where
-    t       = Bare.qualifyTop env name (F.loc t0) t0
-    (t0, e) = makeAssumeType allowTC embs lmap dm x mbT v def
+    (t, e)  = makeAssumeType allowTC embs lmap dm x mbT v def
     embs    = Bare.tcEmbs       tycEnv
     dm      = Bare.tcDataConMap tycEnv
     allowTC = typeclass (getConfig env)

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

@@ -95,16 +95,16 @@ checkBareSpec sp
     hmeasures = S.map (fmap getLHNameSymbol) (Ms.hmeas sp)
     reflects  = S.map (fmap getLHNameSymbol) (Ms.reflects sp)
     measures  = fmap getLHNameSymbol . msName <$> Ms.measures sp
-    fields    = concatMap dataDeclFields (Ms.dataDecls sp)
+    fields    = map (fmap getLHNameSymbol) $ concatMap dataDeclFields (Ms.dataDecls sp)
 
-dataDeclFields :: DataDecl -> [F.LocSymbol]
-dataDeclFields = filter (not . GM.isTmpSymbol . F.val)
+dataDeclFields :: DataDecl -> [F.Located LHName]
+dataDeclFields = filter (not . GM.isTmpSymbol . getLHNameSymbol . F.val)
                . Misc.hashNubWith val
                . concatMap dataCtorFields
                . fromMaybe []
                . tycDCons
 
-dataCtorFields :: DataCtor -> [F.LocSymbol]
+dataCtorFields :: DataCtor -> [F.Located LHName]
 dataCtorFields c
   | isGadt c  = []
   | otherwise = F.atLoc c <$> [ f | (f,_) <- dcFields c ]

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

@@ -61,7 +61,9 @@ makeMethodTypes allowTC (DEnv hm) cls cbs
       classType Nothing _ = Nothing
       classType (Just (d, ts, _)) x =
         case filter ((==d) . Ghc.dataConWorkId . dcpCon) cls of
-          (di:_) -> (dcpLoc di `F.atLoc`) . subst (zip (dcpFreeTyVars di) ts) <$> L.lookup (mkSymbol x) (dcpTyArgs di)
+          (di:_) ->
+            (dcpLoc di `F.atLoc`) . subst (zip (dcpFreeTyVars di) ts) <$>
+            L.lookup (mkSymbol x) (map (first lhNameToResolvedSymbol) $ dcpTyArgs di)
           _      -> Nothing
 
       methodType d x m = ihastype (M.lookup d m) x
@@ -160,7 +162,7 @@ mkClassE env sigEnv _myName name (RClass cc ss as ms) tc = do
     meths  <- mapM (makeMethod env sigEnv name) ms'
     let vts = [ (m, v, t) | (m, kv, t) <- meths, v <- Mb.maybeToList (plugSrc kv) ]
     let sts = [(val s, unClass $ val t) | (s, _) <- ms | (_, _, t) <- meths]
-    let dcp = DataConP l dc αs [] (val <$> ss') (map (first getLHNameSymbol) (reverse sts)) rt False (F.symbol name) l'
+    let dcp = DataConP l dc αs [] (val <$> ss') (reverse sts) rt False (F.symbol name) l'
     return  $ F.notracepp msg (dcp, vts)
   where
     c      = btc_tc cc