diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal index 076bcb47e9..be8a88b1d8 100644 --- a/liquidhaskell-boot/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot/liquidhaskell-boot.cabal @@ -126,7 +126,6 @@ library , Diff >= 0.3 && < 0.6 , array , aeson - , base64 , binary , bytestring >= 0.10 , Cabal diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index 98bd328696..4b3de99810 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -645,6 +645,7 @@ import GHC.Types.Name as Ghc import GHC.Types.Name.Env as Ghc ( NameEnv , lookupNameEnv + , mkNameEnv , mkNameEnvWith ) import GHC.Types.Name.Set as Ghc diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 9f45130e28..ba5abb66e7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -34,7 +34,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.LHNameResolution import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Types.DataDecl import Language.Haskell.Liquid.Types.Names @@ -214,7 +214,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods >>= elaborateSig sig else pure sig - let (dg3, refl) = withDiagnostics $ makeSpecRefl cfg src specs env name elaboratedSig tycEnv + let (dg3, refl) = withDiagnostics $ makeSpecRefl src specs env name elaboratedSig tycEnv let eqs = gsHAxioms refl let (dg4, measEnv) = withDiagnostics $ addOpaqueReflMeas cfg tycEnv env mySpec measEnv0 specs eqs let qual = makeSpecQual cfg env tycEnv measEnv rtEnv specs @@ -247,7 +247,10 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen , _gsTerm = spcTerm , _gsLSpec = finalLiftedSpec - { expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ] + { expSigs = + [ (logicNameToSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v) + | v <- gsReflects refl + ] , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec , measures = Ms.measures mySpec -- We want to export measures in a 'LiftedSpec', especially if they are @@ -269,9 +272,11 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen , reflects = Ms.reflects mySpec0 , cmeasures = Ms.cmeasures targetSpec , embeds = Ms.embeds targetSpec + , privateReflects = mconcat $ map (privateReflects . snd) mspecs } }) where + thisModule = Ghc.tcg_mod tcg -- typeclass elaboration coreToLg ce = @@ -609,25 +614,23 @@ getSizeFuns decl ------------------------------------------------------------------------------------------ -makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv +makeSpecRefl :: GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv -> Bare.Lookup GhcSpecRefl ------------------------------------------------------------------------------------------ -makeSpecRefl cfg src specs env name sig tycEnv = do +makeSpecRefl src specs env name sig tycEnv = do autoInst <- makeAutoInst env mySpec rwr <- makeRewrite env mySpec rwrWith <- makeRewriteWith env mySpec - wRefls <- Bare.wiredReflects cfg env name sig - xtes <- Bare.makeHaskellAxioms cfg src env tycEnv name lmap sig mySpec - asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv name sig mySpec + xtes <- Bare.makeHaskellAxioms src env tycEnv name 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 {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))} - | (x, lt, e) <- xtes - , let s = symbol x + e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))} + | (_, lt, e) <- xtes ] ++ otherAxioms let asmReflEls = eqName <$> otherAxioms let impAxioms = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs) @@ -645,9 +648,8 @@ makeSpecRefl cfg src specs env name sig tycEnv = do , gsAutoInst = autoInst , gsImpAxioms = impAxioms , gsMyAxioms = myAxioms - , gsReflects = (fst3 <$> xtes) ++ (fst <$> gsAsmReflects sig) ++ wRefls + , gsReflects = (fst3 <$> xtes) ++ (fst <$> gsAsmReflects sig) , gsHAxioms = F.notracepp "gsHAxioms" $ xtes ++ asmReflAxioms - , gsWiredReft = wRefls , gsRewrites = rwr , gsRewritesWith = rwrWith } @@ -667,7 +669,7 @@ addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> Bare.MeasEnv -> GhcSpecRefl - ------------------------------------------------------------------------------------------ addReflSigs env name rtEnv measEnv refl sig = sig { gsRefSigs = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs - , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) combinedOpaqueAndReflectedAndWiredAsmSigs + , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) combinedOpaqueAndReflectedAsmSigs } where -- We make sure that the reflected functions are excluded from `gsAsmSigs`, except for the signatures of @@ -681,10 +683,9 @@ addReflSigs env name rtEnv measEnv refl sig = -- Based on `M.union`'s handling of duplicates, the leftmost elements in the chain of `M.union` will precede over those -- after, which is why we put the opaque reflection first in the chain. The signatures for opaque reflections are created -- by strengthening the post-conditions, as in (assume-)reflection. - combinedOpaqueAndReflectedAndWiredAsmSigs = M.toList $ + combinedOpaqueAndReflectedAsmSigs = M.toList $ M.fromList (createUpdatedSpecs . fst <$> Bare.meOpaqueRefl measEnv) `M.union` M.fromList (filter notReflected (gsAsmSigs sig)) - `M.union` M.fromList wreflSigs -- Strengthen the post-condition of each of the opaque reflections. createUpdatedSpecs var = (var, Bare.aty <$> Bare.strengthenSpecWithMeasure sig env var (Bare.varLocSym var)) -- See T1738. We need to expand and qualify any reflected signature /here/, after any @@ -696,15 +697,14 @@ addReflSigs env name rtEnv measEnv refl sig = expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType) expandReflectedSignature = fmap (Bare.qualifyExpand env name rtEnv (F.dummyPos "expand-refSigs") []) - (wreflSigs, reflSigs) = L.partition ((`elem` gsWiredReft refl) . fst) - [ (x, t) | (x, t, _) <- gsHAxioms refl ] + reflSigs = [ (x, t) | (x, t, _) <- gsHAxioms refl ] -- Get the set of all the actual functions (in assume-reflects) actualFnsInAssmRefl = S.fromList $ fst <$> gsAsmReflects sig isActualFn x = S.member x actualFnsInAssmRefl -- Get all the variables from the axioms that are not actual functions (in assume-reflects) notReflActualTySigs = L.filter (not . isActualFn . fst) reflSigs -- Get the list of reflected elements. We do not count actual functions in assume reflect as reflected - reflected = S.fromList $ fst <$> (wreflSigs ++ notReflActualTySigs) + reflected = S.fromList $ fst <$> notReflActualTySigs notReflected xt = fst xt `notElem` reflected makeAutoInst :: Bare.Env -> Ms.BareSpec -> @@ -1287,7 +1287,7 @@ makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0 xbs = toBare <$> reflTySigs sigVars = S.difference defVars reflVars defVars = S.fromList (_giDefVars src) - reflTySigs = [(x, t) | (x,t,_) <- gsHAxioms refl, x `notElem` gsWiredReft refl] + reflTySigs = [(x, t) | (x,t,_) <- gsHAxioms refl] reflVars = S.fromList (fst <$> reflTySigs) -- myAliases fld = M.elems . fld $ myRTE srcF = _giTarget src diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs index 458e44a5e9..8f0c8b9f34 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -8,7 +8,7 @@ -- | This module contains the code that DOES reflection; i.e. converts Haskell -- definitions into refinements. -module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, strengthenSpecWithMeasure, makeAssumeReflectAxioms, wiredReflects, AxiomType(..) ) where +module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, strengthenSpecWithMeasure, makeAssumeReflectAxioms, AxiomType(..) ) where import Prelude hiding (error) import Prelude hiding (mapM) @@ -62,13 +62,12 @@ findDuplicateBetweenLists key l1 l2 = [ (x, y) | x <- l2', Just y <- [Map.lookup (key' x) seen]] ----------------------------------------------------------------------------------------------- -makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec +makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)] ----------------------------------------------------------------------------------------------- -makeHaskellAxioms cfg src env tycEnv name lmap spSig spec = do - wiDefs <- wiredDefs cfg env name spSig +makeHaskellAxioms src env tycEnv name lmap spSig spec = do let refDefs = getReflectDefs src spSig spec env - return (makeAxiom env tycEnv name lmap <$> (wiDefs ++ refDefs)) + return (makeAxiom env tycEnv name lmap <$> refDefs) ----------------------------------------------------------------------------------------------- -- Returns a list of elements, one per assume reflect -- @@ -78,17 +77,17 @@ makeHaskellAxioms cfg src env tycEnv name lmap spSig spec = do -- ``VV == pretendedFn arg1 arg2 ...` -- -- * The assume reflect equation, linking the pretended and actual function: -- -- `actualFn arg1 arg 2 ... = pretendedFn arg1 arg2 ...` -- -makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> GhcSpecSig -> Ms.BareSpec +makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> GhcSpecSig -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)] ----------------------------------------------------------------------------------------------- -makeAssumeReflectAxioms src env tycEnv name spSig spec = do +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 Nothing -> return $ turnIntoAxiom <$> Ms.asmReflectSigs spec where - turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs name (actual, pretended) + turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs (actual, pretended) refDefs = getReflectDefs src spSig spec env embs = Bare.tcEmbs tycEnv refSymbols = @@ -99,11 +98,11 @@ makeAssumeReflectAxioms src env tycEnv name spSig spec = do -- Processes one `assume reflect` and returns its axiom element, as detailed in -- -- `makeAssumeReflectAxioms`. Can also be used to compute the updated SpecType of -- -- a type where we add the post-condition that actual and pretended are the same -- -makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon -> ModName +makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon -> (Located LHName, Located LHName) -- actual function and pretended function -> (Ghc.Var, LocSpecType, F.Equation) ----------------------------------------------------------------------------------------------- -makeAssumeReflectAxiom sig env tce name (actual, pretended) = +makeAssumeReflectAxiom sig env tce (actual, pretended) = -- The actual and pretended function must have the same type if pretendedTy == actualTy then (actualV, actual{val = aty at}, actualEq) @@ -122,8 +121,13 @@ makeAssumeReflectAxiom sig env tce name (actual, pretended) = Right x -> x Left _ -> panic (Just $ GM.fSrcSpan pretended) "function to reflect not in scope" -- Get the qualified name symbols for the actual and pretended functions - qActual = Bare.qualifyTop env name (F.loc actual) (getLHNameSymbol $ val actual) - qPretended = Bare.qualifyTop env name (F.loc pretended) (getLHNameSymbol $ val pretended) + lhNameToSymbol lx = + F.symbol $ + Mb.fromMaybe (panic (Just $ GM.fSrcSpan lx) $ "expected a resolved Haskell name: " ++ show lx) $ + getLHGHCName $ + val lx + qActual = lhNameToSymbol actual + qPretended = lhNameToSymbol pretended -- Get the GHC type of the actual and pretended functions actualTy = Ghc.varType actualV pretendedTy = Ghc.varType pretendedV @@ -145,7 +149,7 @@ strengthenSpecWithMeasure :: GhcSpecSig -> Bare.Env -> Located AxiomType ----------------------------------------------------------------------------------------------- strengthenSpecWithMeasure sig env actualV qPretended = - qPretended{ val = addSingletonApp allowTC qPretended rt} + qPretended{ val = addSingletonApp allowTC (val qPretended) rt} where -- Get the GHC type of the actual and pretended functions actualTy = Ghc.varType actualV @@ -324,14 +328,15 @@ makeAssumeType -> Ghc.Var -> Ghc.CoreExpr -> (LocSpecType, F.Equation) makeAssumeType allowTC tce lmap dm sym mbT v def - = (sym {val = aty at `strengthenRes` F.subst su ref}, F.mkEquation (val sym) xts (F.subst su le) out) + = (sym {val = aty at `strengthenRes` F.subst su ref}, F.mkEquation symbolV xts (F.subst su le) out) where + symbolV = F.symbol v rt = fromRTypeRep . (\trep@RTypeRep{..} -> trep{ty_info = fmap (\i -> i{permitTC = Just allowTC}) ty_info}) . toRTypeRep $ Mb.fromMaybe (ofType τ) mbT τ = Ghc.varType v - at = addSingletonApp allowTC sym rt + at = addSingletonApp allowTC symbolV rt out = rTypeSort tce $ ares at xArgs = F.EVar . fst <$> aargs at _msg = unwords [showpp sym, showpp mbT] @@ -427,7 +432,7 @@ data AxiomType = AT { aty :: SpecType, aargs :: [(F.Symbol, SpecType)], ares :: -- @addSingletonApp allowTC f (x:_ -> y: -> {v:_ | p}@ produces a type -- @x:_ -> y:_ -> {v:_ | p && v = f x y}@ -- -addSingletonApp :: Bool -> LocSymbol -> SpecType -> AxiomType +addSingletonApp :: Bool -> F.Symbol -> SpecType -> AxiomType addSingletonApp allowTC s st = AT to (reverse xts) res where (to, (_,xts, Just res)) = runState (go st) (1,[], Nothing) @@ -452,60 +457,7 @@ unDummy x i | x /= F.dummySymbol = x | otherwise = F.symbol ("lq" ++ show i) -singletonApp :: F.Symbolic a => LocSymbol -> [a] -> UReft F.Reft +singletonApp :: F.Symbolic a => F.Symbol -> [a] -> UReft F.Reft singletonApp s ys = MkUReft r mempty where - r = F.exprReft (F.mkEApp s (F.eVar <$> ys)) - - -------------------------------------------------------------------------------- --- | Hardcode imported reflected functions ------------------------------------ -------------------------------------------------------------------------------- - -wiredReflects :: Config -> Bare.Env -> ModName -> GhcSpecSig -> - Bare.Lookup [Ghc.Var] -wiredReflects cfg env name sigs = do - vs <- wiredDefs cfg env name sigs - return [v | (_, _, v, _) <- vs] - -wiredDefs :: Config -> Bare.Env -> ModName -> GhcSpecSig - -> Bare.Lookup [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)] -wiredDefs cfg env name spSig - | reflection cfg = do - let x = F.dummyLoc functionComposisionSymbol - v <- Bare.lookupGhcVar env name "wiredAxioms" x - return [ (x, F.val <$> lookup v (gsTySigs spSig), v, makeCompositionExpression v) ] - | otherwise = - return [] - -------------------------------------------------------------------------------- --- | Expression Definitions of Prelude Functions ------------------------------ --- | NV: Currently Just Hacking Composition ----------------------------- -------------------------------------------------------------------------------- - - -makeCompositionExpression :: Ghc.Id -> Ghc.CoreExpr -makeCompositionExpression gid - = go $ Ghc.varType $ F.notracepp ( -- tracing to find the body of . from the inline spec, - -- replace F.notrace with F.trace to print - "\nv = " ++ GM.showPpr gid ++ - "\n realIdUnfolding = " ++ GM.showPpr (Ghc.realIdUnfolding gid) ++ - "\n maybeUnfoldingTemplate . realIdUnfolding = " ++ GM.showPpr (Ghc.maybeUnfoldingTemplate $ Ghc.realIdUnfolding gid ) ++ - "\n inl_src . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_src $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inl_inline . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_inline $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inl_sat . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_sat $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inl_act . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_act $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inl_rule . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_rule $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inl_rule rule = " ++ GM.showPpr (Ghc.inl_rule $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++ - "\n inline spec = " ++ GM.showPpr (Ghc.inl_inline $ Ghc.inlinePragInfo $ Ghc.idInfo gid) - ) gid - where - go (Ghc.ForAllTy a (Ghc.ForAllTy b (Ghc.ForAllTy c Ghc.FunTy{ Ghc.ft_arg = tf, Ghc.ft_res = Ghc.FunTy { Ghc.ft_arg = tg, Ghc.ft_res = tx}}))) - = let f = stringVar "f" tf - g = stringVar "g" tg - x = stringVar "x" tx - in Ghc.Lam (Ghc.binderVar a) $ - Ghc.Lam (Ghc.binderVar b) $ - Ghc.Lam (Ghc.binderVar c) $ - Ghc.Lam f $ Ghc.Lam g $ Ghc.Lam x $ Ghc.App (Ghc.Var f) (Ghc.App (Ghc.Var g) (Ghc.Var x)) - go _ = error "Axioms.go" + r = F.exprReft (F.eApps (F.EVar s) (F.eVar <$> ys)) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs index 18f76d62d2..b1bc1a9f09 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -16,6 +16,7 @@ module Language.Haskell.Liquid.Bare.Resolve makeEnv , makeLocalVars , makeGHCTyLookupEnv + , GHCTyLookupEnv(..) -- * Resolving symbols , ResolveSym (..) @@ -88,8 +89,7 @@ import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp import qualified Language.Haskell.Liquid.Types.RefType as RT import Language.Haskell.Liquid.Types.Types -import Language.Haskell.Liquid.Measure (BareSpec) -import Language.Haskell.Liquid.Types.Specs hiding (BareSpec) +import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Visitors import Language.Haskell.Liquid.Bare.Types import Language.Haskell.Liquid.UX.Config diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs index 22639e14fa..0043621a9d 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -18,6 +18,7 @@ module Language.Haskell.Liquid.Constraint.Init ( import Prelude hiding (error, undefined) import Control.Monad (foldM, forM) import Control.Monad.State +import Data.Char (isLower) import Data.Maybe (isNothing, fromMaybe, catMaybes, mapMaybe) import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S @@ -188,7 +189,13 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE , syenv = F.fromListSEnv (gsFreeSyms (gsName sp)) , litEnv = F.fromListSEnv lts , constEnv = F.fromListSEnv lt2s - , fenv = initFEnv $ filterHO (tcb' ++ lts ++ (second (rTypeSort tce . val) <$> gsMeas (gsData sp))) + , fenv = + initFEnv $ filterHO $ concat + [ tcb' + , lts + , second (rTypeSort tce . val) <$> gsMeas (gsData sp) + , [(F.eqName e, eqToPolySort e) | e <- gsImpAxioms (gsRefl sp)] + ] , denv = dmapty val $ gsDicts (gsSig sp) , recs = S.empty , invs = mempty @@ -215,6 +222,14 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE lts = lt1s ++ lt2s tcb' = [] +-- | Given an equation whose sorts are @FObj "a"@, @FObj "b"@, etc, +-- replaces those with @FVar@s. +eqToPolySort :: F.EquationV v -> F.Sort +eqToPolySort e = + let s = foldr (F.FFunc . snd) (F.eqSort e) (F.eqArgs e) + ss = filter (all isLower . take 1 . F.symbolString) $ S.toList $ F.sortSymbols s + su = F.mkSortSubst $ zip ss $ map F.FVar [0..] + in F.mkPoly (length ss - 1) $ F.sortSubst su s assm :: TargetInfo -> [(Var, SpecType)] assm = assmGrty (giImpVars . giSrc) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index eecd53c9f7..7ae5441637 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -73,7 +73,7 @@ import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Types.Visitors import Language.Haskell.Liquid.Bare -import Language.Haskell.Liquid.Bare.Resolve (makeLocalVars) +import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve import Language.Haskell.Liquid.UX.CmdLine import Language.Haskell.Liquid.UX.Config @@ -544,7 +544,7 @@ processModule LiquidHaskellContext{..} = do -- call 'evaluate' to force any exception and catch it, if we can. tcg <- getGblEnv - let localVars = makeLocalVars preNormalizedCore + let localVars = Resolve.makeLocalVars preNormalizedCore eBareSpec = resolveLHNames moduleCfg thisModule diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs index 773be58c33..d8df06e96c 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -51,7 +51,7 @@ module Language.Haskell.Liquid.LHNameResolution , exprArg , fromBareSpecLHName , toBareSpecLHName - , LogicNameEnv + , LogicNameEnv(..) ) where import qualified Liquid.GHC.API as GHC hiding (Expr, panic) @@ -72,12 +72,13 @@ import Data.Generics (extT) import qualified Data.HashSet as HS import qualified Data.HashMap.Strict as HM +import Data.List (nub) import Data.Maybe (fromMaybe, listToMaybe, mapMaybe) import qualified Data.Text as Text import qualified GHC.Types.Name.Occurrence import Language.Fixpoint.Types as F hiding (Error, panic) -import Language.Haskell.Liquid.Bare.Resolve (lookupLocalVar) +import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve import Language.Haskell.Liquid.Bare.Types (LocalVars(lvNames), LocalVarDetails(lvdLclEnv)) import Language.Haskell.Liquid.Name.LogicNameEnv import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl @@ -122,23 +123,32 @@ resolveLHNames -> BareSpecParsed -> TargetDependencies -> Either [Error] (BareSpec, LogicNameEnv) -resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = - let (inScopeEnv, logicNameEnv, unhandledNames) = - makeInScopeExprEnv impMods thisModule bareSpec0 dependencies - (bs, (es, ns)) = +resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = do + let ((bs, logicNameEnv), (es, ns)) = flip runState mempty $ do -- 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 - fromBareSpecLHName <$> - resolveLogicNames cfg inScopeEnv globalRdrEnv unhandledNames lmap localVars sp1 - logicNameEnv' = - foldr (uncurry insertSEnv) logicNameEnv [ (logicNameToSymbol n, n) | n <- ns] - in if null es then - Right (bs, logicNameEnv') - else - Left es + 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) + logicNameEnv' = extendLogicNameEnv logicNameEnv ns + if null es then + Right (bs, logicNameEnv') + else + Left es where taliases = collectTypeAliases thisModule bareSpec0 dependencies @@ -158,7 +168,7 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe | isDataCon s -> lookupGRELHName (LHDataConName lcl) lname s listToMaybe | otherwise -> lookupGRELHName ns lname s - (fmap (either id GHC.getName) . lookupLocalVar localVars (atLoc lname s)) + (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s)) LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe n@(LHNResolved (LHRLocal _) _) -> pure n n -> @@ -359,13 +369,13 @@ exprArg l msg = notracepp ("exprArg: " ++ msg) . go -- -- For each symbol we have the aliases with which it is imported and the -- name corresponding to each alias. -type InScopeExprEnv = SEnv [(GHC.ModuleName, LHName)] +type InScopeNonReflectedEnv = SEnv [(GHC.ModuleName, LHName)] -- | Looks the names in scope with the given symbol. -- Returns a list of close but different symbols or a non empty list -- with the matched names. -lookupInScopeExprEnv :: InScopeExprEnv -> Symbol -> Either [Symbol] [LHName] -lookupInScopeExprEnv env s = do +lookupInScopeNonReflectedEnv :: InScopeNonReflectedEnv -> Symbol -> Either [Symbol] [LHName] +lookupInScopeNonReflectedEnv env s = do let n = LH.dropModuleNames s case lookupSEnvWithDistance n env of Alts closeSyms -> Left closeSyms @@ -375,36 +385,37 @@ lookupInScopeExprEnv env s = do [] -> Left $ map ((`LH.qualifySymbol` n) . symbol . GHC.moduleNameString . fst) xs ys -> Right $ map snd ys --- | Builds an 'InScopeExprEnv' from the module aliases for the current module, --- the spec of the current module, and the specs of the dependencies. +-- | Builds an environment of non-reflected names in scope from the module +-- aliases for the current module, the spec of the current module, and the specs +-- of the dependencies. -- -- Also returns a LogicNameEnv constructed from the same names. +-- Also returns the names of reflected private functions. -- Also returns the set of all names that aren't handled yet by name resolution. -makeInScopeExprEnv +makeLogicEnvs :: GHC.ImportedMods -> GHC.Module -> BareSpecParsed -> TargetDependencies - -> ( InScopeExprEnv + -> ( InScopeNonReflectedEnv , LogicNameEnv + , HS.HashSet LocSymbol , HS.HashSet Symbol ) -makeInScopeExprEnv impAvails thisModule spec dependencies = +makeLogicEnvs impAvails thisModule spec dependencies = let unqualify s = if s == LH.qualifySymbol (symbol $ GHC.moduleName thisModule) (LH.dropModuleNames s) then LH.dropModuleNames s else s + + dependencyPairs = HM.toList $ getDependencies dependencies -- Names should be removed from this list as they are supported -- by renaming. unhandledNames = HS.fromList $ map unqualify unhandledNamesList ++ map (LH.qualifySymbol (symbol $ GHC.moduleName thisModule)) unhandledNamesList unhandledNamesList = concat $ - [ map (getLHNameSymbol . val) $ HS.toList $ reflects spec - , map (getLHNameSymbol . val) $ HS.toList $ opaqueReflects spec - , map (getLHNameSymbol . val) $ HS.toList $ hmeas spec - , map (getLHNameSymbol . val) $ HS.toList $ inlines spec - , map (getLHNameSymbol . val . fst) $ asmReflectSigs spec + [ map (getLHNameSymbol . val) $ HS.toList $ hmeas spec , map (val . msName) $ measures spec , map (val . msName) $ cmeasures spec , map (rtName . val) $ ealiases spec @@ -415,15 +426,32 @@ makeInScopeExprEnv impAvails thisModule spec dependencies = mapMaybe DataDecl.tycDCons $ dataDecls spec , map fst wiredSortedSyms - ] ++ map (map getLHNameSymbol . snd) logicNames + ] ++ map (map getLHNameSymbol . snd) unhandledLogicNames + unhandledLogicNames = + [ (GHC.unStableModule sm, collectUnhandledLiftedSpecLogicNames sp) + | (sm, sp) <- dependencyPairs + ] logicNames = - (thisModule, []) : + (thisModule, thisModuleNames) : [ (GHC.unStableModule sm, collectLiftedSpecLogicNames sp) - | (sm, sp) <- HM.toList $ getDependencies dependencies + | (sm, sp) <- dependencyPairs + ] ++ unhandledLogicNames + thisModuleNames = + [ reflectLHName thisModule (val n) + | n <- concat + [ map fst (asmReflectSigs spec) + , HS.toList (reflects spec) + , HS.toList (opaqueReflects spec) + , HS.toList (inlines spec) + ] ] + privateReflectNames = + mconcat $ + privateReflects spec : map (liftedPrivateReflects . snd) dependencyPairs in ( unionAliasEnvs $ map mkAliasEnv logicNames - , mkLogicNameEnv $ concatMap snd logicNames + , mkLogicNameEnv (concatMap snd logicNames) + , privateReflectNames , unhandledNames ) where @@ -431,11 +459,16 @@ makeInScopeExprEnv impAvails thisModule spec dependencies = let aliases = moduleAliases m in fromListSEnv [ (s, map (,lhname) aliases) - | lhname@(LHNResolved (LHRLogic (LogicName s _ _))_) <- lhnames + -- Note that only non-reflected names go to the InScope environement + | lhname@(LHNResolved (LHRLogic (LogicName s _ Nothing))_) <- lhnames ] - unionAliasEnvs :: [InScopeExprEnv] -> InScopeExprEnv - unionAliasEnvs = coerce . foldl' (HM.unionWith (++)) HM.empty . coerce @[InScopeExprEnv] @[HM.HashMap Symbol [(GHC.ModuleName, LHName)]] + unionAliasEnvs :: [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv + unionAliasEnvs = + coerce . + HM.map nub . + foldl' (HM.unionWith (++)) HM.empty . + coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, LHName)]] moduleAliases m = case GHC.lookupModuleEnv impAvails m of @@ -446,32 +479,45 @@ makeInScopeExprEnv impAvails thisModule spec dependencies = | GHC.imv_qualified imv = [GHC.imv_name imv] | otherwise = [GHC.imv_name imv, GHC.mkModuleName ""] - mkLogicNameEnv names = fromListSEnv [ (logicNameToSymbol n, n) | n <- names ] + mkLogicNameEnv names = + LogicNameEnv + { lneLHName = fromListSEnv [ (logicNameToSymbol n, n) | n <- names ] + , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]] + } -collectLiftedSpecLogicNames :: LiftedSpec -> [LHName] -collectLiftedSpecLogicNames sp = +collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName] +collectUnhandledLiftedSpecLogicNames sp = concat - [ map (makeLocalLHName . LH.dropModuleNames . getLHNameSymbol . fst) $ HS.toList $ liftedExpSigs sp - , map (makeLocalLHName . LH.dropModuleNames . val . msName) $ HS.toList $ liftedCmeasures sp + [ map (makeLocalLHName . LH.dropModuleNames . val . msName) $ HS.toList $ liftedCmeasures sp , map (makeLocalLHName . LH.dropModuleNames . val . msName) $ HS.toList $ liftedMeasures sp , map (makeLocalLHName . LH.dropModuleNames . rtName . val) $ HS.toList $ liftedEaliases sp , map (makeLocalLHName . LH.dropModuleNames . fst) $ concatMap DataDecl.dcFields $ concat $ mapMaybe DataDecl.tycDCons $ HS.toList $ liftedDataDecls sp - , map (makeLocalLHName . LH.dropModuleNames . eqName) $ HS.toList $ liftedAxeqs sp ] +collectLiftedSpecLogicNames :: LiftedSpec -> [LHName] +collectLiftedSpecLogicNames sp = + map fst $ HS.toList $ liftedExpSigs sp + +-- | Resolves names in the logic namespace +-- +-- Returns the renamed spec. +-- Adds in the monadic state the errors about ambiguous or missing names, and +-- the names of data constructors that are found during renaming. resolveLogicNames :: Config - -> InScopeExprEnv + -> InScopeNonReflectedEnv -> GHC.GlobalRdrEnv -> HS.HashSet Symbol -> LogicMap -> LocalVars + -> LogicNameEnv + -> HS.HashSet LocSymbol -> BareSpecParsed -> State RenameOutput BareSpecLHName -resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars sp = +resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames sp = emapSpecM (bscope cfg) (map localVarToSymbol . maybe [] lvdLclEnv . (GHC.lookupNameEnv (lvNames localVars) <=< getLHGHCName)) @@ -483,12 +529,13 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars sp = resolveLogicName :: [Symbol] -> LocSymbol -> State RenameOutput LHName resolveLogicName ss ls + -- The name is local | elem s ss = return $ makeLocalLHName s | otherwise = - case lookupInScopeExprEnv env s of + case lookupInScopeNonReflectedEnv env s of Left alts -> -- If names are not in the environment, they must be data constructors, - -- or they must be in the logicmap. + -- or they must be reflected functions, or they must be in the logicmap. case resolveDataConName ls `mplus` resolveVarName lmap0 ls of Just m -> m Nothing -> do @@ -522,9 +569,6 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars sp = return $ makeLocalLHName s | isTupleDC (symbolText s) = Just $ return $ makeLocalLHName s - -- TODO: Remove this case when qualified names are handled - | LH.takeModuleNames s /= "" = Just $ - return $ makeLocalLHName s where s = val ls isTupleDC t = @@ -551,32 +595,50 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars sp = ) return $ makeLocalLHName $ val s - resolveVarName _ s - | val s == "GHC.Internal.Base.." = Just $ do - return $ makeLocalLHName $ val s - resolveVarName lmap s = - case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHVarName LHAnyModuleNameF) (val s)) of - [e] -> do - let n = GHC.greName e - if HM.member (symbol n) (lmSymDefs lmap) then + -- Resolves names of reflected functions or names in the logic map + -- + -- Names of reflected functions are resolved here because, to be in scope, + -- we ask the corresponding Haskell name to be in scope. In contrast, the + -- @InScopeNonReflectedEnv@ indicates where the reflect annotations were + -- imported from, but not where the Haskell names were imported from. + resolveVarName lmap s = do + let gres = + GHC.lookupGRE globalRdrEnv $ + mkLookupGRE (LHVarName LHAnyModuleNameF) (val s) + refls = mapMaybe (findReflection . GHC.greName) gres + case refls of + [lhName] -> Just $ return lhName + _ | HS.member s privateReflectNames + -> Just $ return $ makeLocalLHName (val s) + | otherwise + -> case gres of + [e] -> do + let n = GHC.greName e + if HM.member (symbol n) (lmSymDefs lmap) then + Just $ do + let lhName = makeLogicLHName (symbol n) (GHC.nameModule n) Nothing + addName lhName + -- return lhName + return $ makeLocalLHName $ val s + -- TODO: Remove this case when qualified names are handled + else if LH.takeModuleNames (val s) /= "" then + Just $ return $ makeLocalLHName $ val s + else + Nothing + [] -> + Nothing + es -> Just $ do - let lhName = makeLogicLHName (symbol n) (GHC.nameModule n) (Just n) - addName lhName - -- return lhName + addError + (ErrDupNames + (LH.fSrcSpan s) + (pprint $ val s) + (map (PJ.text . GHC.showPprUnsafe) es) + ) return $ makeLocalLHName $ val s - else - Nothing - [] -> - Nothing - es -> - Just $ do - addError - (ErrDupNames - (LH.fSrcSpan s) - (pprint $ val s) - (map (PJ.text . GHC.showPprUnsafe) es) - ) - return $ makeLocalLHName $ val s + + findReflection :: GHC.Name -> Maybe LHName + findReflection n = GHC.lookupNameEnv (lneReflected lnameEnv) n toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName toBareSpecLHName cfg env sp0 = runIdentity $ go sp0 @@ -598,7 +660,7 @@ toBareSpecLHName cfg env sp0 = runIdentity $ go sp0 symbolToLHName ss s | elem s ss = return $ makeLocalLHName s | otherwise = - case lookupSEnv s env of + case lookupSEnv s (lneLHName env) of Nothing -> do unless (HS.member s unhandledNames) $ panic Nothing $ "toBareSpecLHName: cannot find " ++ show s diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs index 4564bdf9b0..6ec511133a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs @@ -1,7 +1,9 @@ module Language.Haskell.Liquid.Name.LogicNameEnv - ( LogicNameEnv + ( LogicNameEnv(..) + , extendLogicNameEnv ) where +import qualified Liquid.GHC.API as GHC import Language.Fixpoint.Types import Language.Haskell.Liquid.Types.Names @@ -10,4 +12,15 @@ import Language.Haskell.Liquid.Types.Names -- -- Symbols are expected to have been created by 'logicNameToSymbol'. -- -type LogicNameEnv = SEnv LHName +data LogicNameEnv = LogicNameEnv + { lneLHName :: SEnv LHName + -- | Haskell names that have a reflected counterpart + , lneReflected :: GHC.NameEnv LHName + } + +extendLogicNameEnv :: LogicNameEnv -> [LHName] -> LogicNameEnv +extendLogicNameEnv env ns = + env + { lneLHName = + foldr (uncurry insertSEnv) (lneLHName env) [ (logicNameToSymbol n, n) | n <- ns] + } diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 64ecfe85ce..2e61a5afa2 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -100,7 +100,7 @@ initPStateWithList { empList = Just $ \lx -> EVar ("GHC.Types.[]" <$ lx) , singList = Just (\lx e -> EApp (EApp (EVar ("GHC.Types.:" <$ lx)) e) (EVar ("GHC.Types.[]" <$ lx))) } - where composeFun = Just $ EVar . (functionComposisionSymbol <$) + where composeFun = Nothing ------------------------------------------------------------------------------- singleSpecP :: SourcePos -> String -> Either (ParseErrorBundle String Void) BPspec diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs index c163e479d2..b462ccd7bc 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -449,14 +449,13 @@ makeApp _ _ f [e1, e2] , Just op <- M.lookup (mappendSym (symbol ("GHC.Internal.Num." :: String)) sym) bops = EBin op e1 e2 -makeApp def lmap f es - = eAppWithMap lmap f es def +makeApp def lmap f es = + eAppWithMap lmap (val f) es def -- where msg = "makeApp f = " ++ show f ++ " es = " ++ show es ++ " def = " ++ show def eVarWithMap :: Id -> LogicMap -> Expr eVarWithMap x lmap = do - let f' = dummyLoc $ symbol x - in eAppWithMap lmap f' [] (EVar $ symbol x) + eAppWithMap lmap (symbol x) [] (EVar $ symbol x) brels :: M.HashMap Symbol Brel brels = M.fromList [ (symbol ("GHC.Classes.==" :: String), Eq) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs index ecec5de8ed..f28da72137 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs @@ -5,7 +5,6 @@ module Language.Haskell.Liquid.Types.Names ( lenLocSymbol , anyTypeSymbol - , functionComposisionSymbol , selfSymbol , LogicName (..) , LHResolvedName (..) @@ -26,15 +25,14 @@ module Language.Haskell.Liquid.Types.Names , makeUnresolvedLHName , mapLHNames , mapMLocLHNames + , maybeReflectedLHName + , reflectGHCName + , reflectLHName , updateLHNameSymbol ) where import Control.DeepSeq -import qualified Data.Base64.Types as Base64 import qualified Data.Binary as B -import qualified Data.ByteString.Lazy as ByteString -import qualified Data.ByteString.Base64 as Base64 -import qualified Data.ByteString.Builder as Builder import Data.Data (Data, gmapM, gmapT) import Data.Generics (extM, extT) import Data.Hashable @@ -54,12 +52,6 @@ lenLocSymbol = dummyLoc $ symbol ("autolen" :: String) anyTypeSymbol :: Symbol anyTypeSymbol = symbol ("GHC.Prim.Any" :: String) - --- defined in include/GHC/Base.hs -functionComposisionSymbol :: Symbol -functionComposisionSymbol = symbol ("GHC.Internal.Base.." :: String) - - selfSymbol :: Symbol selfSymbol = symbol ("liquid_internal_this" :: String) @@ -68,7 +60,8 @@ selfSymbol = symbol ("liquid_internal_this" :: String) -- For instance, this can be used to represent predicate aliases -- or uninterpreted functions. data LogicName = LogicName - { lnSymbol :: !Symbol + { -- | Unqualified symbol + lnSymbol :: !Symbol -- | Module where the entity was defined , lnModule :: !GHC.Module -- | If the named entity is the reflection of some Haskell name @@ -260,9 +253,20 @@ updateLHNameSymbol :: (Symbol -> Symbol) -> LHName -> LHName updateLHNameSymbol f (LHNResolved n s) = LHNResolved n (f s) updateLHNameSymbol f (LHNUnresolved n s) = LHNUnresolved n (f s) +-- | Converts logic names to symbols. +-- +-- One important postcondition of this function is that the symbol for reflected +-- names must match exactly the symbol for the corresponding Haskell function. +-- Otherwise, LH would fail to link the two at various places where it is needed. logicNameToSymbol :: LHName -> Symbol -logicNameToSymbol (LHNResolved (LHRLogic (LogicName s m _)) _) = - let msymbol = Text.pack $ GHC.moduleNameString $ GHC.moduleName m +logicNameToSymbol (LHNResolved (LHRLogic (LogicName s om mReflectionOf)) _) = + let m = maybe om GHC.nameModule mReflectionOf + msymbol = Text.pack $ GHC.moduleNameString $ GHC.moduleName m + in symbol $ mconcat [msymbol, ".", symbolText s] + {- + TODO: Adding a prefix for the unit would allow LH to deal with + -XPackageImports. This prefix should be added here and in + the Symbolic instance of Name. munique = Text.dropEnd 2 $ -- Remove padding of two characters "==" Base64.extractBase64 $ @@ -275,6 +279,28 @@ logicNameToSymbol (LHNResolved (LHRLogic (LogicName s m _)) _) = GHC.unitIdString $ GHC.moduleUnitId m in symbol $ mconcat ["u", munique, "##", msymbol, ".", symbolText s] + -} logicNameToSymbol (LHNResolved (LHRLocal s) _) = s logicNameToSymbol n = error $ "logicNameToSymbol: unexpected name: " ++ show n +-- | Creates a name in the logic namespace for the given Haskell name. +reflectLHName :: HasCallStack => GHC.Module -> LHName -> LHName +reflectLHName thisModule (LHNResolved (LHRGHC n) _) = reflectGHCName thisModule n +reflectLHName _ n = error $ "not a GHC Name: " ++ show n + +-- | Creates a name in the logic namespace for the given Haskell name. +reflectGHCName :: GHC.Module -> GHC.Name -> LHName +reflectGHCName thisModule n = + LHNResolved + (LHRLogic + (LogicName + (symbol (GHC.occNameString $ GHC.nameOccName n)) + thisModule + (Just n) + ) + ) + (symbol n) + +maybeReflectedLHName :: LHName -> Maybe GHC.Name +maybeReflectedLHName (LHNResolved (LHRLogic (LogicName _ _ m)) _) = m +maybeReflectedLHName _ = Nothing diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 3e4250ef37..75ee6b7808 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -331,7 +331,6 @@ data GhcSpecRefl = SpRefl , gsMyAxioms :: ![F.Equation] -- ^ Axioms from my reflected functions , gsReflects :: ![Var] -- ^ Binders for reflected functions , gsLogicMap :: !LogicMap - , gsWiredReft :: ![Var] , gsRewrites :: S.HashSet (F.Located Var) , gsRewritesWith :: M.HashMap Var [Var] } @@ -345,7 +344,6 @@ instance Semigroup GhcSpecRefl where , gsMyAxioms = gsMyAxioms x <> gsMyAxioms y , gsReflects = gsReflects x <> gsReflects y , gsLogicMap = gsLogicMap x <> gsLogicMap y - , gsWiredReft = gsWiredReft x <> gsWiredReft y , gsRewrites = gsRewrites x <> gsRewrites y , gsRewritesWith = gsRewritesWith x <> gsRewritesWith y } @@ -353,7 +351,7 @@ instance Semigroup GhcSpecRefl where instance Monoid GhcSpecRefl where mempty = SpRefl mempty mempty mempty mempty mempty mempty - mempty mempty mempty + mempty mempty type VarOrLocSymbol = Either Var LocSymbol type BareMeasure = Measure LocBareType F.LocSymbol @@ -702,6 +700,8 @@ data LiftedSpec = LiftedSpec -- ^ User-defined properties for ADTs , liftedExpSigs :: HashSet (LHName, F.Sort) -- ^ Exported logic symbols originated from reflecting functions + , liftedPrivateReflects :: HashSet F.LocSymbol + -- ^ Private functions that have been reflected , liftedAsmSigs :: HashSet (F.Located LHName, LocBareTypeLHName) -- ^ Assumed (unchecked) types; including reflected signatures , liftedSigs :: HashSet (F.Located LHName, LocBareTypeLHName) @@ -771,6 +771,7 @@ emptyLiftedSpec :: LiftedSpec emptyLiftedSpec = LiftedSpec { liftedMeasures = mempty , liftedExpSigs = mempty + , liftedPrivateReflects = mempty , liftedAsmSigs = mempty , liftedSigs = mempty , liftedInvariants = mempty @@ -934,6 +935,7 @@ toLiftedSpec :: BareSpecLHName -> LiftedSpec toLiftedSpec a = LiftedSpec { liftedMeasures = S.fromList . measures $ a , liftedExpSigs = S.fromList . expSigs $ a + , liftedPrivateReflects = privateReflects a , liftedAsmSigs = S.fromList . asmSigs $ a , liftedSigs = S.fromList . sigs $ a , liftedInvariants = S.fromList . invariants $ a @@ -983,7 +985,7 @@ unsafeFromLiftedSpec a = Spec , rewrites = mempty , rewriteWith = mempty , reflects = mempty - , privateReflects = mempty + , privateReflects = liftedPrivateReflects a , opaqueReflects = mempty , autois = liftedAutois a , hmeas = mempty diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs index 8dc01fa225..11e13a9810 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs @@ -275,9 +275,9 @@ toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls} where toLMap (x, ys, e) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e}) -eAppWithMap :: LogicMap -> F.Located Symbol -> [Expr] -> Expr -> Expr +eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr eAppWithMap lmap f es expr - | Just (LMap _ xs e) <- M.lookup (F.val f) (lmSymDefs lmap) + | Just (LMap _ xs e) <- M.lookup f (lmSymDefs lmap) , length xs == length es = F.subst (F.mkSubst $ zip xs es) e | otherwise diff --git a/src/GHC/Base_LHAssumptions.hs b/src/GHC/Base_LHAssumptions.hs index d648e1ca34..6b1f0c53e7 100644 --- a/src/GHC/Base_LHAssumptions.hs +++ b/src/GHC/Base_LHAssumptions.hs @@ -8,6 +8,13 @@ import GHC.Exts_LHAssumptions() import GHC.Types_LHAssumptions() import Data.Tuple_LHAssumptions() +{-@ LIQUID "--higherorder" @-} +{-@ reflect comp @-} +{-@ assume reflect . as comp @-} +comp :: (b -> c) -> (a -> b) -> a -> c +comp f g x = f (g x) + + {-@ assume . :: forall

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. diff --git a/tests/basic/neg/T2349.hs b/tests/basic/neg/T2349.hs index 1781158efc..7a5e7cd315 100644 --- a/tests/basic/neg/T2349.hs +++ b/tests/basic/neg/T2349.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GADTs #-} {-@ LIQUID "--expect-error-containing=is not a subtype of the required type - VV : {VV##1461 : [GHC.Types.Int] | len VV##1461 == ?b + 1}" @-} + VV : {VV##1456 : [GHC.Types.Int] | len VV##1456 == ?b + 1}" @-} {-@ LIQUID "--reflection" @-} -- | Test that the refinement types produced for GADTs are -- compatible with the Haskell types. diff --git a/tests/basic/pos/ReflExt03A.hs b/tests/basic/pos/ReflExt03A.hs index e08f511050..51831b26e8 100644 --- a/tests/basic/pos/ReflExt03A.hs +++ b/tests/basic/pos/ReflExt03A.hs @@ -13,3 +13,6 @@ import ReflExt03B -- 3 * 2 + 2 = 8 {-@ lemma :: {f 3 2 = 8} @-} lemma = () + +{-@ lemma2 :: { ReflExt03B.myAdd 3 2 = 5} @-} +lemma2 = () diff --git a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs index ce881fc3cf..29a0b8c006 100644 --- a/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs +++ b/tests/benchmarks/stitch-lh/src/Language/Stitch/LH/Check.hs @@ -179,7 +179,7 @@ check globals = go Nil where {-@ go :: ts :Language.Stitch.LH.Data.List.List Ty - -> VarsSmallerThan (Language.Stitch.LH.Data.List.length ts) + -> VarsSmallerThan (List.length ts) -> (e1 : WellTypedExp ts -> { t: Ty | exprType e1 = t } -> Either TyError b) -> Either TyError b @-} diff --git a/tests/pos/LNot.hs b/tests/pos/LNot.hs index 729eff0a0f..1cf6fd8b30 100644 --- a/tests/pos/LNot.hs +++ b/tests/pos/LNot.hs @@ -4,7 +4,6 @@ module LNot where import Prelude hiding (any, all, filter, nub, foldr, flip) - {-@ lemma_all_ex_not :: f:(a->Bool) -> ls:[a] -> { (bnot (any f ls)) == all (bnot . f) ls} @-} lemma_all_ex_not :: (a->Bool) -> [a] -> () lemma_all_ex_not f [] = () diff --git a/tests/pos/T1548.hs b/tests/pos/T1548.hs index 91157977df..bf2b249a01 100644 --- a/tests/pos/T1548.hs +++ b/tests/pos/T1548.hs @@ -1,5 +1,5 @@ {-@ LIQUID "--reflection" @-} - +{-@ LIQUID "--ple" @-} module T1548 where