diff --git a/liquid-fixpoint b/liquid-fixpoint index 1876aa6b4c..71ad8e4b78 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 1876aa6b4cce989224994795de23d3bf370ff169 +Subproject commit 71ad8e4b78a2e2bf5c204638be0876f64e95e011 diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index c987cba782..17d8837399 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -90,6 +90,7 @@ library Language.Haskell.Liquid.Bare.Resolve Language.Haskell.Liquid.Bare.ToBare Language.Haskell.Liquid.Bare.Types + Language.Haskell.Liquid.Bare.Elaborate Language.Haskell.Liquid.Constraint.Constraint Language.Haskell.Liquid.Constraint.Env Language.Haskell.Liquid.Constraint.Fresh @@ -123,6 +124,7 @@ library Language.Haskell.Liquid.Transforms.ANF Language.Haskell.Liquid.Transforms.CoreToLogic Language.Haskell.Liquid.Transforms.Rec + Language.Haskell.Liquid.Transforms.InlineAux Language.Haskell.Liquid.Transforms.RefSplit Language.Haskell.Liquid.Transforms.Rewrite Language.Haskell.Liquid.Transforms.Simplify @@ -190,6 +192,8 @@ library , transformers >= 0.3 , unordered-containers >= 0.2 , vector >= 0.10 + , free + , recursion-schemes default-language: Haskell98 default-extensions: PatternGuards ghc-options: -W -fwarn-missing-signatures diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs index c4ac004bc3..b0068f2fb9 100644 --- a/src/Language/Haskell/Liquid/Bare.hs +++ b/src/Language/Haskell/Liquid/Bare.hs @@ -1,9 +1,9 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE OverloadedStrings #-} -- | This module contains the functions that convert /from/ descriptions of @@ -23,6 +23,7 @@ module Language.Haskell.Liquid.Bare ( import Prelude hiding (error) import Control.Monad (unless) +import Control.Monad.Reader import qualified Control.Exception as Ex import qualified Data.Binary as B import qualified Data.Maybe as Mb @@ -42,7 +43,8 @@ import qualified Language.Haskell.Liquid.GHC.API as Ghc import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.WiredIn import qualified Language.Haskell.Liquid.Measure as Ms -import qualified Language.Haskell.Liquid.Bare.Types as Bare +import qualified Language.Haskell.Liquid.Bare.Types as Bare +import Language.Haskell.Liquid.Bare.Elaborate import qualified Language.Haskell.Liquid.Bare.Resolve as Bare import qualified Language.Haskell.Liquid.Bare.DataType as Bare import qualified Language.Haskell.Liquid.Bare.Expand as Bare @@ -53,7 +55,7 @@ import qualified Language.Haskell.Liquid.Bare.ToBare as Bare import qualified Language.Haskell.Liquid.Bare.Class as Bare import qualified Language.Haskell.Liquid.Bare.Check as Bare import qualified Language.Haskell.Liquid.Bare.Laws as Bare -import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic +import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic import Control.Arrow (second) -------------------------------------------------------------------------------- @@ -96,15 +98,15 @@ saveLiftedSpec src sp = do -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then -- validates it using @checkGhcSpec@. ------------------------------------------------------------------------------------- -makeGhcSpec :: Config -> GhcSrc -> LogicMap -> [(ModName, Ms.BareSpec)] -> GhcSpec +makeGhcSpec :: Config -> GhcSrc -> LogicMap -> [(ModName, Ms.BareSpec)] -> Ghc.Ghc GhcSpec ------------------------------------------------------------------------------------- -makeGhcSpec cfg src lmap mspecs0 - = checkThrow (Bare.checkGhcSpec mspecs src renv cbs sp) +makeGhcSpec cfg src lmap mspecs0 = do + sp <- makeGhcSpec0 cfg src lmap mspecs + let renv = ghcSpecEnv sp + pure $ checkThrow (Bare.checkGhcSpec mspecs src renv cbs sp) where mspecs = [ (m, checkThrow $ Bare.checkBareSpec m sp) | (m, sp) <- mspecs0, isTarget m ] ++ [ (m, sp) | (m, sp) <- mspecs0, not (isTarget m)] - sp = makeGhcSpec0 cfg src lmap mspecs - renv = ghcSpecEnv sp cbs = giCbs src checkThrow :: Ex.Exception e => Either e c -> c @@ -125,7 +127,6 @@ ghcSpecEnv sp = fromListSEnv binds vSort = Bare.varSortedReft emb rSort = rTypeSortedReft emb - ------------------------------------------------------------------------------------- -- | @makeGhcSpec0@ slurps up all the relevant information needed to generate -- constraints for a target module and packages them into a @GhcSpec@ @@ -133,41 +134,77 @@ ghcSpecEnv sp = fromListSEnv binds -- essentially, to get to the `BareRTEnv` as soon as possible, as thats what -- lets us use aliases inside data-constructor definitions. ------------------------------------------------------------------------------------- -makeGhcSpec0 :: Config -> GhcSrc -> LogicMap -> [(ModName, Ms.BareSpec)] -> GhcSpec +makeGhcSpec0 :: Config -> GhcSrc -> LogicMap -> [(ModName, Ms.BareSpec)] -> Ghc.Ghc GhcSpec ------------------------------------------------------------------------------------- -makeGhcSpec0 cfg src lmap mspecs = SP - { gsConfig = cfg - , gsImps = makeImports mspecs - , gsSig = addReflSigs refl sig - , gsRefl = refl - , gsLaws = laws - , gsData = sData - , gsQual = qual - , gsName = makeSpecName env tycEnv measEnv name - , gsVars = makeSpecVars cfg src mySpec env measEnv - , gsTerm = makeSpecTerm cfg mySpec env name - , gsLSpec = makeLiftedSpec src env refl sData sig qual myRTE lSpec1 { - impSigs = makeImports mspecs, - expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ], - dataDecls = dataDecls mySpec2 - } - } +makeGhcSpec0 cfg src lmap mspecsNoClass = do + tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier + let tyi = Bare.tcTyConMap tycEnv + sigEnv = makeSigEnv embs tyi (gsExports src) rtEnv + lSpec1 = lSpec0 <> makeLiftedSpec1 cfg src tycEnv lmap mySpec1 + mySpec = mySpec2 <> lSpec1 + specs = M.insert name mySpec iSpecs2 + measEnv = makeMeasEnv env tycEnv sigEnv specs + sig = makeSpecSig cfg name specs env sigEnv tycEnv measEnv (giCbs src) + auxSig <- makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods + elaboratedSig <- elaborateSig sig (F.notracepp "auxSig" auxSig) + let myRTE = myRTEnv src env sigEnv rtEnv + qual = makeSpecQual cfg env tycEnv measEnv rtEnv specs + sData = makeSpecData src env sigEnv measEnv elaboratedSig specs + -- YL: fix + refl = makeSpecRefl cfg src measEnv specs env name elaboratedSig tycEnv + laws = makeSpecLaws env sigEnv (gsTySigs elaboratedSig ++ gsAsmSigs elaboratedSig) measEnv specs + + pure $ SP + { gsConfig = cfg + , gsImps = makeImports mspecs + , gsSig = addReflSigs refl elaboratedSig + , gsRefl = refl + , gsLaws = laws + , gsData = sData + , gsQual = qual + , gsName = makeSpecName env tycEnv measEnv name + , gsVars = makeSpecVars cfg src mySpec env measEnv + , gsTerm = makeSpecTerm cfg mySpec env name + -- YL: shoudl I add the sigs here? + , gsLSpec = makeLiftedSpec src env refl sData elaboratedSig qual myRTE lSpec1 { + impSigs = makeImports mspecs, + expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ], + dataDecls = dataDecls mySpec2 + } + } where - -- build up spec components - myRTE = myRTEnv src env sigEnv rtEnv - qual = makeSpecQual cfg env tycEnv measEnv rtEnv specs - sData = makeSpecData src env sigEnv measEnv sig specs - refl = makeSpecRefl cfg src measEnv specs env name sig tycEnv - laws = makeSpecLaws env sigEnv (gsTySigs sig ++ gsAsmSigs sig) measEnv specs - sig = makeSpecSig cfg name specs env sigEnv tycEnv measEnv (giCbs src) - measEnv = makeMeasEnv env tycEnv sigEnv specs + -- build up spec components + simplifier :: Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr + simplifier = buildSimplifier (giCbs src) + coreToLg e = + case CoreToLogic.runToLogic + embs + lmap + dm + (\x -> todo Nothing ("ctl not working " ++ x)) + (CoreToLogic.coreToLogic e) of + Left _ -> impossible Nothing "can't reach here" + Right e -> e + + elaborateSig si auxsig = do + tySigs <- + forM (gsTySigs si) $ \(x, t) -> + if Ghc.nameModule (Ghc.getName x) == Ghc.gHC_REAL then + pure (x, t) + else do t' <- traverse (elaborateSpecType coreToLg simplifier) t + pure (x, t') + -- things like len breaks the code + -- asmSigs <- forM (gsAsmSigs si) $ \(x, t) -> do + -- t' <- traverse (elaborateSpecType (pure ()) coreToLg) t + -- pure (x, fst <$> t') + pure + si + { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig -- , gsAsmSigs = asmSigs + } + + dm = Bare.tcDataConMap tycEnv0 -- build up environments - specs = M.insert name mySpec iSpecs2 - mySpec = mySpec2 <> lSpec1 - lSpec1 = lSpec0 <> makeLiftedSpec1 cfg src tycEnv lmap mySpec1 - sigEnv = makeSigEnv embs tyi (gsExports src) rtEnv - tyi = Bare.tcTyConMap tycEnv - tycEnv = makeTycEnv cfg name env embs mySpec2 iSpecs2 + (tycEnv0, datacons) = makeTycEnv0 cfg name env embs mySpec2 iSpecs2 mySpec2 = Bare.qualifyExpand env name rtEnv l [] mySpec1 where l = F.dummyPos "expand-mySpec2" iSpecs2 = Bare.qualifyExpand env name rtEnv l [] iSpecs0 where l = F.dummyPos "expand-iSpecs2" rtEnv = Bare.makeRTEnv env name mySpec1 iSpecs0 lmap @@ -175,11 +212,204 @@ makeGhcSpec0 cfg src lmap mspecs = SP lSpec0 = makeLiftedSpec0 cfg src embs lmap mySpec0 embs = makeEmbeds src env ((name, mySpec0) : M.toList iSpecs0) -- extract name and specs - env = Bare.makeEnv cfg src lmap mspecs - (mySpec0, iSpecs0) = splitSpecs name mspecs + env = Bare.makeEnv cfg src lmap mspecsNoClass + mspecs = M.toList $ M.insert name mySpec0 iSpecs0 + (mySpec0, instMethods) = compileClasses src env (name, mySpec0NoClass) (M.toList iSpecs0) + (mySpec0NoClass, iSpecs0) = splitSpecs name mspecsNoClass -- check barespecs name = F.notracepp ("ALL-SPECS" ++ zzz) $ giTargetMod src - zzz = F.showpp (fst <$> mspecs) + zzz = F.showpp (fst <$> mspecsNoClass) + +makeClassAuxTypes :: + (SpecType -> Ghc.Ghc SpecType) + -> [F.Located DataConP] + -> [(Ghc.ClsInst, [Ghc.Var])] + -> Ghc.Ghc [(Ghc.Var, LocSpecType)] +makeClassAuxTypes elab dcps xs = Misc.concatMapM (makeClassAuxTypesOne elab) dcpInstMethods + where + dcpInstMethods = do + dcp <- dcps + (inst, methods) <- xs + let dc = dcpCon . F.val $ dcp + -- YL: only works for non-newtype class + dc' = Ghc.classDataCon $ Ghc.is_cls inst + guard $ dc == dc' + pure (dcp, inst, methods) + + +makeClassAuxTypesOne :: + (SpecType -> Ghc.Ghc SpecType) + -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var]) + -> Ghc.Ghc [(Ghc.Var, LocSpecType)] +makeClassAuxTypesOne elab (ldcp, inst, methods) = + forM methods $ \method -> do + let (headlessSig, preft) = + case L.lookup (mkSymbol method) yts' of + Nothing -> + impossible Nothing ("makeClassAuxTypesOne : unreachable?" ++ F.showpp (mkSymbol method) ++ " " ++ F.showpp yts) + Just sig -> sig + -- dict binder will never be changed because we optimized PAnd[] + -- lq0 lq1 ... + ptys = [(F.vv (Just i), pty, mempty) | (i,pty) <- zip [0,1..] isPredSpecTys] + fullSig = + mkArrow + (zip isRTvs (repeat mempty)) + [] + [] + ptys . + subst (zip clsTvs isSpecTys) $ + headlessSig + elaboratedSig <- flip addCoherenceOblig preft <$> elab fullSig + + let retSig = mapExprReft (\_ -> substAuxMethod dfunSym methodsSet) (F.notracepp ("elaborated" ++ GM.showPpr method) elaboratedSig) + pure (method, F.dummyLoc retSig) + + -- "is" is used as a shorthand for instance, following the convention of the Ghc api + where + -- recsel = F.symbol ("lq$recsel" :: String) + (_,predTys,_,_) = Ghc.instanceSig inst + dfunApped = F.mkEApp dfunSymL [F.eVar $ F.vv (Just i) | (i,_) <- zip [0,1..] predTys] + prefts = L.reverse . take (length yts) $ fmap (F.notracepp "prefts" . Just . (flip MkUReft mempty) . mconcat) preftss ++ repeat Nothing + preftss = F.notracepp "preftss" $ (fmap.fmap) (uncurry (GM.coherenceObligToRefE dfunApped)) (GM.buildCoherenceOblig cls) + yts' = zip (fst <$> yts) (zip (snd <$> yts) prefts) + cls = Mb.fromJust . Ghc.tyConClass_maybe $ Ghc.dataConTyCon (dcpCon dcp) + addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType + addCoherenceOblig t Nothing = t + addCoherenceOblig t (Just r) = F.notracepp "SCSel" . fromRTypeRep $ rrep {ty_res = res `strengthen` r} + where rrep = toRTypeRep t + res = ty_res rrep -- (Monoid.mappend -> $cmappend##Int, ...) + -- core rewriting mark2: do the same thing except they don't have to be symbols + -- YL: poorly written. use a comprehension instead of assuming + methodsSet = F.notracepp "methodSet" $ M.fromList (zip (F.symbol <$> clsMethods) (F.symbol <$> methods)) + -- core rewriting mark1: dfunId + -- () + dfunSymL = GM.namedLocSymbol $ Ghc.instanceDFunId inst + dfunSym = F.val dfunSymL + (isTvs, isPredTys, _, isTys) = Ghc.instanceSig inst + isSpecTys = ofType <$> isTys + isPredSpecTys = ofType <$> isPredTys + isRTvs = makeRTVar . rTyVar <$> isTvs + dcp = F.val ldcp + -- Monoid.mappend, ... + clsMethods = filter (\x -> GM.dropModuleNames (F.symbol x) `elem` fmap mkSymbol methods) $ + Ghc.classAllSelIds (Ghc.is_cls inst) + yts = [(GM.dropModuleNames y, t) | (y, t) <- dcpTyArgs dcp] + mkSymbol x + -- | "$cp" `F.isPrefixOfSym` F.symbol x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x) + | F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $ Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x) + | otherwise = F.dropSym 2 $ GM.simplesymbol x + -- res = dcpTyRes dcp + clsTvs = dcpFreeTyVars dcp + -- copy/pasted from Bare/Class.hs + subst [] t = t + subst ((a, ta):su) t = subsTyVar_meet' (a, ta) (subst su t) + +substAuxMethod :: F.Symbol -> M.HashMap F.Symbol F.Symbol -> F.Expr -> F.Expr +substAuxMethod dfun methods e = F.notracepp "substAuxMethod" $ go e + where go :: F.Expr -> F.Expr + go (F.EApp e0 e1) + | F.EVar x <- F.notracepp "e0" e0 + , (F.EVar dfun_mb, args) <- splitEApp e1 + , dfun_mb == dfun + , Just method <- M.lookup x methods + -- Before: Functor.fmap ($p1Applicative $dFunctor) + -- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative) + = eApps (F.EVar method) args + | otherwise + = F.EApp (go e0) (go e1) + go (F.ENeg e) = F.ENeg (go e) + go (F.EBin bop e0 e1) = F.EBin bop (go e0) (go e1) + go (F.EIte e0 e1 e2) = F.EIte (go e0) (go e1) (go e2) + go (F.ECst e0 s) = F.ECst (go e0) s + go (F.ELam (x, t) body) = F.ELam (x, t) (go body) + go (F.PAnd es) = F.PAnd (go <$> es) + go (F.POr es) = F.POr (go <$> es) + go (F.PNot e) = F.PNot (go e) + go (F.PImp e0 e1) = F.PImp (go e0) (go e1) + go (F.PIff e0 e1) = F.PIff (go e0) (go e1) + go (F.PAtom brel e0 e1) = F.PAtom brel (go e0) (go e1) + go e = F.notracepp "LEAF" e + +compileClasses :: + GhcSrc + -> Bare.Env + -> (ModName, Ms.BareSpec) + -> [(ModName, Ms.BareSpec)] + -> (Ms.BareSpec, [(Ghc.ClsInst, [Ghc.Var])]) +compileClasses src env (name, spec) rest = (spec {sigs = sigs'} <> clsSpec, instmethods) + where + clsSpec = + mempty + { dataDecls = clsDecls + , reflects = + F.notracepp "reflects " $ + S.fromList + (fmap + (fmap GM.dropModuleNames . + GM.namedLocSymbol . Ghc.instanceDFunId . fst) + instClss ++ + methods) + } + clsDecls = Bare.makeClassDataDecl' (M.toList refinedMethods) + -- class methods + (refinedMethods, sigs') = foldr grabClassSig (mempty, mempty) (sigs spec) + grabClassSig :: + (F.LocSymbol, ty) + -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)]) + -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)]) + grabClassSig sig@(lsym, ref) (refs, sigs') = + case clsOp of + Nothing -> (refs, sig : sigs') + Just (cls, sig) -> (M.alter (merge sig) cls refs, sigs') + where + clsOp = do + var <- Bare.maybeResolveSym env name "grabClassSig" lsym + cls <- Ghc.isClassOpId_maybe var + pure (cls, (var, ref)) + merge sig v = + case v of + Nothing -> Just [sig] + Just vs -> Just (sig : vs) + methods = [GM.namedLocSymbol x | (_, xs) <- instmethods, x <- xs] + -- instance methods + + mkSymbol x + | Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x) + | otherwise = F.dropSym 2 $ GM.simplesymbol x + + instmethods :: [(Ghc.ClsInst, [Ghc.Var])] + instmethods = + [ (inst, ms) + | (inst, cls) <- instClss + , let selIds = GM.dropModuleNames . F.symbol <$> Ghc.classAllSelIds cls + , (_, e) <- + Mb.maybeToList + (GM.findVarDefMethod + (GM.dropModuleNames . F.symbol $ Ghc.instanceDFunId inst) + (giCbs src)) + , let ms = filter (\x -> GM.isMethod x && elem (mkSymbol x) selIds) (freeVars mempty e) + ] + instClss :: [(Ghc.ClsInst, Ghc.Class)] + instClss = + [ (inst, cls) + | inst <- mconcat . Mb.maybeToList . gsCls $ src + , Ghc.moduleName (Ghc.nameModule (Ghc.getName inst)) == getModName name + , let cls = Ghc.is_cls inst + , cls `elem` refinedClasses + ] + refinedClasses :: [Ghc.Class] + refinedClasses = + Mb.mapMaybe resolveClassMaybe clsDecls ++ + concatMap (Mb.mapMaybe resolveClassMaybe . dataDecls . snd) rest + resolveClassMaybe :: DataDecl -> Maybe Ghc.Class + resolveClassMaybe d = + Bare.maybeResolveSym + env + name + "resolveClassMaybe" + (dataNameSymbol . tycName $ d) >>= + Ghc.tyConClass_maybe + splitSpecs :: ModName -> [(ModName, Ms.BareSpec)] -> (Ms.BareSpec, Bare.ModSpecs) splitSpecs name specs = (mySpec, iSpecm) @@ -313,7 +543,7 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual } where quals = concatMap (makeQualifiers env tycEnv) (M.toList specs) - -- mSyms = F.tracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv) + -- mSyms = F.notracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv) okQual q = F.notracepp ("okQual: " ++ F.showpp q) $ all (`S.member` mSyms) (F.syms q) mSyms = F.notracepp "MSYMS" . S.fromList @@ -426,10 +656,10 @@ makeSpecRefl :: Config -> GhcSrc -> Bare.MeasEnv -> Bare.ModSpecs -> Bare.Env -> ------------------------------------------------------------------------------------------ makeSpecRefl cfg src menv specs env name sig tycEnv = SpRefl { gsLogicMap = lmap - , gsAutoInst = makeAutoInst env name mySpec + , gsAutoInst = F.notracepp "autoInst" $ makeAutoInst env name mySpec , gsImpAxioms = concatMap (Ms.axeqs . snd) (M.toList specs) , gsMyAxioms = F.notracepp "gsMyAxioms" myAxioms - , gsReflects = F.notracepp "gsReflects" (lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ wReflects) + , gsReflects = lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ wReflects , gsHAxioms = F.notracepp "gsHAxioms" xtes , gsWiredReft = wReflects } @@ -490,7 +720,7 @@ makeSpecSig cfg name specs env sigEnv tycEnv measEnv cbs = SpSig where dicts = Bare.makeSpecDictionaries env sigEnv specs mySpec = M.lookupDefault mempty name specs - asmSigs = Bare.tcSelVars tycEnv + asmSigs = (F.notracepp "tcSelVars" $ Bare.tcSelVars tycEnv ) ++ makeAsmSigs env sigEnv name specs ++ [ (x,t) | (_, x, t) <- concat $ map snd (Bare.meCLaws measEnv)] tySigs = strengthenSigs . concat $ @@ -705,11 +935,12 @@ makeSpecData :: GhcSrc -> Bare.Env -> Bare.SigEnv -> Bare.MeasEnv -> GhcSpecSig -> GhcSpecData ------------------------------------------------------------------------------------------ makeSpecData src env sigEnv measEnv sig specs = SpData - { gsCtors = -- F.notracepp "GS-CTORS" + { gsCtors = F.notracepp "GS-CTORS" [ (x, tt) | (x, t) <- Bare.meDataCons measEnv - , let tt = Bare.plugHoles sigEnv name (Bare.LqTV x) t - ] + , let tt = id t -- Bare.plugHoles sigEnv name (Bare.LqTV x) + ] + , gsMeas = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ] , gsMeasures = Bare.qualifyTopDummy env name <$> (ms1 ++ ms2) , gsInvariants = Misc.nubHashOn (F.loc . snd) invs @@ -813,42 +1044,67 @@ makeSpecName env tycEnv measEnv name = SpNames where datacons, cls :: [DataConP] datacons = Bare.tcDataCons tycEnv - cls = F.tracepp "meClasses" $ Bare.meClasses measEnv + cls = F.notracepp "meClasses" $ Bare.meClasses measEnv tycons = Bare.tcTyCons tycEnv -- REBARE: formerly, makeGhcCHOP1 ------------------------------------------------------------------------------------------- -makeTycEnv :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs - -> Bare.TycEnv +makeTycEnv0 :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs + -> (Bare.TycEnv, [Located DataConP]) ------------------------------------------------------------------------------------------- -makeTycEnv cfg myName env embs mySpec iSpecs = Bare.TycEnv +makeTycEnv0 cfg myName env embs mySpec iSpecs = (Bare.TycEnv { tcTyCons = tycons - , tcDataCons = val <$> datacons - , tcSelMeasures = dcSelectors - , tcSelVars = recSelectors + , tcDataCons = mempty + , tcSelMeasures = dcSelectors + , tcSelVars = mempty + -- , tcSelVars = recSelectors , tcTyConMap = tyi , tcAdts = adts , tcDataConMap = dm , tcEmbs = embs , tcName = myName - } + }, datacons) where (tcDds, dcs) = Misc.concatUnzip $ Bare.makeConTypes env <$> specs specs = (myName, mySpec) : M.toList iSpecs tcs = Misc.snd3 <$> tcDds tyi = Bare.qualifyTopDummy env myName (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 = F.notracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons + -- datacons = Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.notracepp "DATACONS" $ concat dcs) wiredDataCons) tycons = tcs ++ knownWiredTyCons env myName - datacons = Bare.makePluggedDataCon embs tyi <$> (concat dcs ++ knownWiredDataCons env myName) + datacons = F.notracepp "makeTycEnv: datacons" $ Bare.makePluggedDataCon embs tyi <$> (concat dcs ++ knownWiredDataCons env myName) tds = [(name, tcpCon tcp, dd) | (name, tcp, Just dd) <- tcDds] adts = Bare.makeDataDecls cfg embs myName tds datacons dm = Bare.dataConMap adts dcSelectors = concatMap (Bare.makeMeasureSelectors cfg dm) datacons - recSelectors = Bare.makeRecordSelectorSigs env myName datacons + -- recSelectors = Bare.makeRecordSelectorSigs env myName datacons fiTcs = gsFiTcs (Bare.reSrc env) - + + +makeTycEnv1 :: + ModName + -> Bare.Env + -> (Bare.TycEnv, [Located DataConP]) + -> (Ghc.CoreExpr -> F.Expr) + -> (Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr) + -> Ghc.Ghc Bare.TycEnv +makeTycEnv1 myName env (tycEnv, datacons) coreToLg simplifier = do + -- fst for selector generation, snd for dataconsig generation + lclassdcs <- forM classdcs $ traverse (Bare.elaborateClassDcp coreToLg simplifier) + let recSelectors = Bare.makeRecordSelectorSigs env myName (dcs ++ (fmap . fmap) snd lclassdcs) + pure $ + tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )} + where + (classdcs, dcs) = + L.partition + (Ghc.isClassTyCon . Ghc.dataConTyCon . dcpCon . F.val) + datacons + + + + + knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP] knownWiredDataCons env name = filter isKnown wiredDataCons where @@ -864,15 +1120,21 @@ knownWiredTyCons env name = filter isKnown wiredTyCons ------------------------------------------------------------------------------------------- makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs -> Bare.MeasEnv ------------------------------------------------------------------------------------------- -makeMeasEnv env tycEnv sigEnv specs = Bare.MeasEnv - { meMeasureSpec = measures - , meClassSyms = cms' - , meSyms = ms' - , meDataCons = cs' - , meClasses = cls - , meMethods = mts ++ dms - , meCLaws = laws - } +makeMeasEnv env tycEnv sigEnv specs = + -- datacons' <- forM datacons $ \dc -> + -- if Ghc.isClassTyCon . Ghc.dataConTyCon . dcpCon $ dc + -- then Bare.elaborateClassDcp coreToLg dc + -- else pure dc + let cs' = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec embs cs (datacons ++ cls)] in + Bare.MeasEnv + { meMeasureSpec = measures + , meClassSyms = cms' + , meSyms = ms' + , meDataCons = cs' + , meClasses = cls + , meMethods = mts ++ dms + , meCLaws = laws + } where measures = mconcat (Ms.mkMSpec' dcSelectors : (Bare.makeMeasureSpec env sigEnv name <$> M.toList specs)) (cs, ms) = Bare.makeMeasureSpec' measures @@ -880,12 +1142,12 @@ makeMeasEnv env tycEnv sigEnv specs = Bare.MeasEnv cms' = [ (x, Loc l l' $ cSort t) | (Loc l l' x, t) <- cms ] ms' = [ (F.val lx, F.atLoc lx t) | (lx, t) <- ms , Mb.isNothing (lookup (val lx) cms') ] - cs' = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec embs cs (datacons ++ cls)] + txRefs v t = Bare.txRefSort tyi embs (const t <$> GM.locNamedThing v) -- unpacking the environment tyi = Bare.tcTyConMap tycEnv dcSelectors = Bare.tcSelMeasures tycEnv - datacons = Bare.tcDataCons tycEnv + datacons = F.notracepp "tcDataCons" $ Bare.tcDataCons tycEnv embs = Bare.tcEmbs tycEnv name = Bare.tcName tycEnv dms = Bare.makeDefaultMethods env mts diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs index 6f966c509a..b44fea92aa 100644 --- a/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -54,9 +54,9 @@ getReflectDefs src sig spec = findVarDefType cbs sigs <$> xs findVarDefType :: [Ghc.CoreBind] -> [(Ghc.Var, LocSpecType)] -> LocSymbol -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr) -findVarDefType cbs sigs x = case findVarDef (val x) cbs of - Just (v, e) -> if Ghc.isExportedId v - then (x, val <$> lookup v sigs, v, e) +findVarDefType cbs sigs x = case findVarDefMethod (val x) cbs of + Just (v, e) -> if Ghc.isExportedId v || isMethod (F.symbol x) || isDictionary (F.symbol x) + then (F.notracepp "FIND-VAR-DEF-NAME" $ x, F.notracepp "FIND-VAR-DEF" $ val <$> lookup v sigs, v, e) else Ex.throw $ mkError x ("Lifted functions must be exported; please export " ++ show v) Nothing -> Ex.throw $ mkError x "Cannot lift haskell function" @@ -106,7 +106,7 @@ rTypeSortExp tce = typeSort tce . Ghc.expandTypeSynonyms . toType grabBody :: Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr) grabBody (Ghc.ForAllTy _ t) e = grabBody t e -grabBody (Ghc.FunTy tx t) e | Ghc.isClassPred tx +grabBody (Ghc.FunTy tx t) e | isEmbeddedDictType tx = grabBody t e grabBody (Ghc.FunTy _ t) (Ghc.Lam x e) = (x:xs, e') where (xs, e') = grabBody t e @@ -178,7 +178,7 @@ axiomType s t = AT to (reverse xts) res (to, (_,xts, Just res)) = runState (go t) (1,[], Nothing) go (RAllT a t r) = RAllT a <$> go t <*> return r go (RAllP p t) = RAllP p <$> go t - go (RFun x tx t r) | isClassType tx = (\t' -> RFun x tx t' r) <$> go t + go (RFun x tx t r) | isEmbeddedClass tx = (\t' -> RFun x tx t' r) <$> go t go (RFun x tx t r) = do (i,bs,res) <- get let x' = unDummy x i diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs index c69b983495..92951fc553 100644 --- a/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/src/Language/Haskell/Liquid/Bare/Check.hs @@ -309,7 +309,7 @@ checkTerminationExpr emb env (v, Loc l _ t, les) xts = concatMap mkClass $ zip (ty_binds trep) (ty_args trep) trep = toRTypeRep t - mkClass (_, RApp c ts _ _) | isClass c = classBinds emb (rRCls c ts) + mkClass (_, RApp c ts _ _) | isEmbeddedDict c = classBinds emb (rRCls c ts) mkClass (x, t) = [(x, rSort t)] rSort = rTypeSortedReft emb diff --git a/src/Language/Haskell/Liquid/Bare/Class.hs b/src/Language/Haskell/Liquid/Bare/Class.hs index 4138037373..c19f064dc2 100644 --- a/src/Language/Haskell/Liquid/Bare/Class.hs +++ b/src/Language/Haskell/Liquid/Bare/Class.hs @@ -114,7 +114,6 @@ addCC x zz@(Loc l l' st0) addForall _ t = t - splitDictionary :: Ghc.CoreExpr -> Maybe (Ghc.Var, [Ghc.Type], [Ghc.Var]) splitDictionary = go [] [] where @@ -273,4 +272,4 @@ lookupDefaultVar env name v = Mb.maybeToList where dmSym = F.atLoc v (GM.qualifySymbol mSym dnSym) dnSym = F.mappendSym "$dm" nSym - (mSym, nSym) = GM.splitModuleName (F.symbol v) \ No newline at end of file + (mSym, nSym) = GM.splitModuleName (F.symbol v) diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs index 1486248c89..cab9b1b8c9 100644 --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE ScopedTypeVariables #-} module Language.Haskell.Liquid.Bare.DataType ( dataConMap @@ -16,7 +17,13 @@ module Language.Haskell.Liquid.Bare.DataType , makeRecordSelectorSigs , meetDataConSpec -- , makeTyConEmbeds - + + -- * Type Classes + , makeClassDataDecl + , makeClassDataDecl' + , elaborateClassDcp + , stripDataConPPred + ) where import Prelude hiding (error) @@ -30,10 +37,13 @@ import qualified Control.Exception as Ex import qualified Data.List as L import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S -import qualified Data.Maybe as Mb +import qualified Data.Maybe as Mb +import Control.Arrow ((***)) +import Control.Monad -- import qualified Language.Fixpoint.Types.Visitor as V import qualified Language.Fixpoint.Types as F +import Control.Monad.Reader import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Language.Haskell.Liquid.GHC.API as Ghc import Language.Haskell.Liquid.Types.PredType (dataConPSpecType) @@ -47,7 +57,8 @@ import Language.Haskell.Liquid.WiredIn import qualified Language.Haskell.Liquid.Measure as Ms import qualified Language.Haskell.Liquid.Bare.Types as Bare -import qualified Language.Haskell.Liquid.Bare.Resolve as Bare +import qualified Language.Haskell.Liquid.Bare.Resolve as Bare +import Language.Haskell.Liquid.Bare.Elaborate -- import qualified Language.Haskell.Liquid.Bare.Misc as GM -- import Language.Haskell.Liquid.Bare.Env @@ -130,7 +141,7 @@ makeFamInstEmbeds cs0 embs = L.foldl' embed embs famInstSorts {- famInstTyConType :: Ghc.TyCon -> Maybe Ghc.Type famInstTyConType c = case Ghc.tyConFamInst_maybe c of - Just (c', ts) -> F.tracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts)) + Just (c', ts) -> F.notracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts)) $ Just (famInstType (Ghc.tyConArity c) c' ts) Nothing -> Nothing @@ -350,8 +361,8 @@ muSort c n = V.mapSort tx meetDataConSpec :: F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP] -> [(Ghc.Var, SpecType)] -------------------------------------------------------------------------------- -meetDataConSpec emb xts dcs = -- F.notracepp "meetDataConSpec" $ - M.toList $ snd <$> L.foldl' upd dcm0 xts +meetDataConSpec emb xts dcs = F.notracepp "meetDataConSpec" $ + M.toList $ snd <$> L.foldl' upd dcm0 (F.notracepp "meetDataConSpec xts" xts) where dcm0 = M.fromList (dataConSpec' dcs) upd dcm (x, t) = M.insert x (Ghc.getSrcSpan x, tx') dcm @@ -380,6 +391,193 @@ makeConTypes env (name, spec) dcs = Ms.dataDecls spec vdcs = Ms.dvariance spec +makeClassDataDecl :: Bare.Env -> (ModName, Ms.BareSpec) -> [DataDecl] +makeClassDataDecl env (m, spec) = classDeclToDataDecl env m <$> Ms.classes spec + +makeClassDataDecl' :: [(Ghc.Class, [(Ghc.Id, LocBareType)])] -> [DataDecl] +makeClassDataDecl' = fmap (uncurry classDeclToDataDecl') + +classDeclToDataDecl' :: Ghc.Class -> [(Ghc.Id, LocBareType)] -> DataDecl +classDeclToDataDecl' cls refinedIds = F.notracepp "classDeclToDataDecl" $ DataDecl + { tycName = DnName (F.symbol <$> GM.locNamedThing cls) + , tycTyVars = tyVars + , tycPVars = [] + , tycDCons = [dctor] + , tycSrcPos = F.loc . GM.locNamedThing $ cls + , tycSFun = Nothing + , tycPropTy = Nothing + , tycKind = DataUser} + -- YL: assume the class constraint is at the very front.. + where dctor = DataCtor + { dcName = F.dummyLoc $ F.symbol classDc + -- YL: same as class tyvars?? + , dcTyVars = tyVars + -- YL: what is theta? + , dcTheta = [] + , dcFields = fields + , dcResult = Nothing + } + + tyVars = F.symbol <$> Ghc.classTyVars cls + + fields = fmap attachRef classIds + attachRef sid + | Just ref <- L.lookup sid refinedIds + = (F.symbol sid, RT.subts tyVarSubst (F.val ref)) + | otherwise + = (F.symbol sid, RT.bareOfType . dropTheta . Ghc.varType $ sid) + + tyVarSubst = [(GM.dropModuleUnique v, v) | v <- tyVars] + + dropTheta :: Ghc.Type -> Ghc.Type + dropTheta = GM.notracePpr "Dropping pred" . Misc.thd3 . Ghc.tcSplitMethodTy + -- dropTheta (Ghc.ForAllTy _ (Ghc.FunTy _ τ')) = τ' + -- dropTheta (Ghc.ForAllTy _ (Ghc.ForAllTy _ _)) = todo Nothing "multi-parameter type-class not supported" + -- dropTheta _ = impossible Nothing "classDeclToDataDecl': assumption was wrong" + + -- YL: what is the type of superclass-dictionary selectors? + classIds = Ghc.classAllSelIds cls + classDc = Ghc.classDataCon cls + + + +classDeclToDataDecl :: Bare.Env -> ModName -> RClass LocBareType -> DataDecl +classDeclToDataDecl env m rcls = DataDecl + { tycName = DnName (btc_tc . rcName $ rcls) + , tycTyVars = as + , tycPVars = [] + , tycDCons = [dctor] + , tycSrcPos = F.loc . btc_tc . rcName $ rcls + , tycSFun = Nothing + , tycPropTy = Nothing + , tycKind = DataUser} + -- YL : fix it + where Just classTc = (Bare.maybeResolveSym env m "makeClassDataDecl" . btc_tc . rcName $ rcls) >>= Ghc.tyConClass_maybe + classDc = Ghc.classDataCon classTc + as = F.symbol <$> rcTyVars rcls + dctor = DataCtor + { dcName = F.dummyLoc $ F.symbol classDc + , dcTyVars = as + , dcTheta = [] + , dcFields = (F.val *** F.val) <$> rcMethods rcls + , dcResult = Nothing} + +-- makeClassDataConP :: Bare.Env +-- -> (Ghc.Class, [(Ghc.Id, LocBareType)], [Ghc.ClsInst]) +-- -> DataConP +-- makeClassDataConP env (cls, sigs, insts) = _ +-- where +-- -- YL: This function is partial. Fails when the class is a newtype +-- Just name = Ghc.nameModule_maybe (Ghc.getName cls) +-- c' = Ghc.classDataCon cls +-- -- resolved field signatures. need to automatically generate the missing ones +-- ts' = Bare.ofBareType env _modulename _loc_beg Nothing <$> _ts +-- -- result type +-- t0' = RT.ofType $ Ghc.dataConOrigResTy c' +-- _cfg = getConfig env +-- -- don't need this step +-- -- (yts, ot) = qualifyDataCtor (not isGadt) name dLoc (zip ) +-- dLoc = F.Loc _loc_beg _loc_end + + +elaborateClassDcp :: (Ghc.CoreExpr -> F.Expr) -> (Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr) -> DataConP -> Ghc.Ghc (DataConP , DataConP) +elaborateClassDcp coreToLg simplifier dcp = do + t' <- flip (zipWith addCoherenceOblig) prefts <$> forM fts (elaborateSpecType coreToLg simplifier) + let ts' = F.notracepp "elaboratedMethod" $ elaborateMethod (F.symbol dc) (S.fromList xs) <$> t' + pure (F.notracepp "elaborateClassDcp" $ + dcp {dcpTyArgs = zip xs (stripPred <$> ts')}, + dcp {dcpTyArgs = fmap (\(x,t) -> (x, strengthenTy x t)) (zip xs t')}) + where + addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType + addCoherenceOblig t Nothing = t + addCoherenceOblig t (Just r) = F.notracepp "SCSel" . fromRTypeRep $ rrep {ty_res = res `RT.strengthen` r} + where rrep = toRTypeRep t + res = ty_res rrep + prefts = L.reverse . take (length fts) $ fmap (F.notracepp "prefts" . Just . (flip MkUReft mempty) . mconcat) preftss ++ repeat Nothing + preftss = F.notracepp "preftss" $ (fmap.fmap) (uncurry (GM.coherenceObligToRef recsel)) (GM.buildCoherenceOblig cls) + + -- ugly, should have passed cls as an argument + cls = Mb.fromJust $ Ghc.tyConClass_maybe (Ghc.dataConTyCon dc) + recsel = F.symbol ("lq$recsel" :: String) + resTy = dcpTyRes dcp + dc = dcpCon dcp + tvars = + F.notracepp "tvars" $ (\x -> (makeRTVar x, mempty)) <$> dcpFreeTyVars dcp + -- check if the names are qualified + (xs, ts) = F.notracepp "elaborateClassDcpxts" $ unzip (dcpTyArgs dcp) + fts = fullTy <$> ts + -- turns forall a b. (a -> b) -> f a -> f b into + -- forall f. Functor f => forall a b. (a -> b) -> f a -> f b + stripPred :: SpecType -> SpecType + stripPred = Misc.fourth4 . bkUnivClass + fullTy :: SpecType -> SpecType + fullTy t = + F.notracepp "fullTy" $ + mkArrow tvars [] [] [(recsel{- F.symbol dc-}, F.notracepp "resTy" resTy, mempty)] t + strengthenTy :: F.Symbol -> SpecType -> SpecType + strengthenTy x t = mkUnivs tvs pvs (RFun z cls (t' `RT.strengthen` mt) r) + where (tvs, pvs, (RFun z cls t' r)) = bkUniv t + vv = rTypeValueVar t' + mt = F.notracepp ("strengthening:" ++ F.showpp x ++ " " ++ F.showpp z) $ RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar x) (F.EVar z))) + +substClassOpBinding :: + F.Symbol -> F.Symbol -> S.HashSet F.Symbol -> F.Expr -> F.Expr +substClassOpBinding tcbind dc methods e = F.notracepp "substClassOpBinding" $ go e + where + go :: F.Expr -> F.Expr + go (F.EApp e0 e1) + | F.EVar x <- F.notracepp "e0" e0 + , F.EVar y <- F.notracepp "e1" e1 + , F.notracepp "tcbindeq" $ y == tcbind + , S.member x methods + -- Before: Functor.fmap ($p1Applicative $dFunctor) + -- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative) + = F.EVar (x `F.suffixSymbol` dc) + | otherwise + = F.EApp (go e0) (go e1) + go (F.ENeg e) = F.ENeg (go e) + go (F.EBin bop e0 e1) = F.EBin bop (go e0) (go e1) + go (F.EIte e0 e1 e2) = F.EIte (go e0) (go e1) (go e2) + go (F.ECst e0 s) = F.ECst (go e0) s + go (F.ELam (x, t) body) = F.ELam (x, t) (go body) + go (F.PAnd es) = F.PAnd (go <$> es) + go (F.POr es) = F.POr (go <$> es) + go (F.PNot e) = F.PNot (go e) + go (F.PImp e0 e1) = F.PImp (go e0) (go e1) + go (F.PIff e0 e1) = F.PIff (go e0) (go e1) + go (F.PAtom brel e0 e1) = F.PAtom brel (go e0) (go e1) + go e = F.notracepp "LEAF" e + +-- fmap f x == ap ... into +-- fmap ($p1Selector $dMyFunctor) f x == (ap $dMyFunctor) f x +-- fmap $p1Selector##MyFunctor f x = ap##MyFunctor f x +elaborateMethod :: + F.Symbol + -> S.HashSet F.Symbol + -> SpecType + -> SpecType +elaborateMethod dc methods t = + let tcbind = grabtcbind t in + mapExprReft (\_ -> substClassOpBinding (F.notracepp "tcbind" tcbind) dc methods) t + where + grabtcbind :: SpecType -> F.Symbol + grabtcbind t = + F.notracepp "grabtcbind" $ + case Misc.fst3 . Misc.snd3 . bkArrow . Misc.thd3 $ (F.notracepp "univ broken" $ bkUniv t) of + tcbind:_ -> tcbind + [] -> + impossible + Nothing + ("elaborateMethod: inserted dictionary binder disappeared:" ++ F.showpp t) + + +stripDataConPPred :: DataConP -> DataConP +stripDataConPPred dcp = dcp {dcpTyArgs = fmap (\(x,t) -> (x, stripPred t)) yts} + where stripPred :: SpecType -> SpecType + stripPred t = mkUnivs tvs pvs tres + where (tvs, pvs, _, tres) = bkUnivClass t + yts = dcpTyArgs dcp + -- | 'canonizeDecls ds' returns a subset of 'ds' with duplicates, e.g. arising -- due to automatic lifting (via 'makeHaskellDataDecls'). We require that the -- lifted versions appear LATER in the input list, and always use those @@ -473,7 +671,7 @@ ofBDataDecl env name (Just dd@(DataDecl tc as ps cts pos sfun pt _)) maybe_invar | not (checkDataDecl tc' dd) = uError err | otherwise - = ((name, tcp, Just (dd { tycDCons = cts }, pd)), Loc lc lc' <$> cts') + = ((name, tcp, Just (dd { tycDCons = cts }, pd)), F.notracepp "ofBDataDecl" $ Loc lc lc' <$> cts') where πs = Bare.ofBPVar env name pos <$> ps tc' = getDnTyCon env name tc @@ -529,16 +727,16 @@ ofBDataCtor env name l l' tc αs ps πs _ctor@(DataCtor c as _ xts res) = DataCo } where c' = Bare.lookupGhcDataCon env name "ofBDataCtor" c - ts' = Bare.ofBareType env name l (Just ps) <$> ts + ts' = F.notracepp "ofBDataCtorts'" $ Bare.ofBareType env name l (Just ps) <$> ts res' = Bare.ofBareType env name l (Just ps) <$> res - t0' = dataConResultTy c' αs t0 res' - _cfg = getConfig env - (yts, ot) = -- F.tracepp ("dataConTys: " ++ F.showpp (c, αs)) $ - qualifyDataCtor (not isGadt) name dLoc (zip xs ts', t0') - zts = zipWith (normalizeField c') [1..] (reverse yts) + t0' = F.notracepp "ofBDataCtort0'" $ dataConResultTy c' αs t0 res' + _cfg = getConfig env + (yts, ot) = -- F.notracepp ("dataConTys: " ++ F.showpp (c, αs)) $ + F.notracepp "ofBDataCtoryts" $ qualifyDataCtor (not isGadt) name dLoc (zip xs ts', t0') + zts = F.notracepp "zts" $ zipWith (normalizeField c') [1..] (reverse yts) usedTvs = S.fromList (ty_var_value <$> concatMap RT.freeTyVars (t0':ts')) cs = [ p | p <- RT.ofType <$> Ghc.dataConTheta c', keepPredType usedTvs p ] - (xs, ts) = unzip xts + (xs, ts) = F.notracepp "ofBDataCtorxts" $ unzip xts t0 = case RT.famInstTyConType tc of Nothing -> F.notracepp "dataConResult-3: " $ RT.gApp tc αs πs Just ty -> RT.ofType ty @@ -655,20 +853,59 @@ checkRecordSelectorSigs vts = [ (v, take1 v ts) | (v, ts) <- Misc.groupList vts (t:ts) -> Ex.throw (ErrDupSpecs (GM.fSrcSpan t) (pprint v) (GM.fSrcSpan <$> ts) :: Error) _ -> impossible Nothing "checkRecordSelectorSigs" + +-- The type passed in must have full type signature (forall a. Semigroup a => ... ) +strengthenClassSel :: Ghc.Var -> LocSpecType -> LocSpecType +strengthenClassSel v lt = lt {val = t} + where t = runReader (go (F.val lt)) (1,[]) + s = GM.namedLocSymbol v + extend :: F.Symbol -> (Int, [F.Symbol]) -> (Int, [F.Symbol]) + extend x (i, xs) = (i + 1, x:xs) + go :: SpecType -> Reader (Int, [F.Symbol]) SpecType + go (RAllT a t r) = RAllT a <$> go t <*> pure r + go (RAllP p t) = RAllP p <$> go t + go (RFun x tx t r) | isEmbeddedClass tx = + RFun <$> pure x <*> pure tx <*> go t <*> pure r + go (RFun x tx t r) = do + x' <- unDummy x <$> reader fst + r' <- singletonApp s <$> (L.reverse <$> reader snd) + RFun x' tx <$> local (extend x') (go t) <*> pure (F.meet r r') + go t = RT.strengthen t . singletonApp s . L.reverse <$> reader snd + +singletonApp :: F.Symbolic a => F.LocSymbol -> [a] -> UReft F.Reft +singletonApp s ys = MkUReft r mempty + where + r = F.exprReft (F.mkEApp s (F.eVar <$> ys)) + + +-- singletonAppRes :: F.Symbolic a => Ghc.Var -> [a] -> UReft F.Reft + + +-- stolen from Axiom.hs +unDummy :: F.Symbol -> Int -> F.Symbol +unDummy x i + | x /= F.dummySymbol = x + | otherwise = F.symbol ("_cls_lq" ++ show i) + + makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)] makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne where makeOne (Loc l l' dcp) - | null fls -- no field labels + | Just cls <- maybe_cls + = let cfs = Ghc.classAllSelIds cls in + F.notracepp "classSelectors" $ fmap ((,) <$> fst <*> uncurry strengthenClassSel) [(v, Loc l l' t)| (v,t) <- zip cfs (reverse $ fmap snd args)] + | null fls -- no field labels || any (isFunTy . snd) args && not (higherOrderFlag env) -- OR function-valued fields || dcpIsGadt dcp -- OR GADT style datcon = [] | otherwise - = [ (v, t) | (Just v, t) <- zip fs ts ] + = [ (v, F.notracepp "selectorSig" t) | (Just v, t) <- zip fs ts ] where + maybe_cls = Ghc.tyConClass_maybe (Ghc.dataConTyCon dc) dc = dcpCon dcp fls = Ghc.dataConFieldLabels dc - fs = Bare.lookupGhcNamedVar env name . Ghc.flSelector <$> fls + fs = Bare.lookupGhcNamedVar env name <$> fmap Ghc.flSelector fls ts :: [ LocSpecType ] ts = [ Loc l l' (mkArrow (zip (makeRTVar <$> dcpFreeTyVars dcp) (repeat mempty)) [] [] [(z, res, mempty)] diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs new file mode 100644 index 0000000000..692b8ba5ca --- /dev/null +++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs @@ -0,0 +1,725 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE LambdaCase #-} +-- | This module uses GHC API to elaborate the resolves expressions + +module Language.Haskell.Liquid.Bare.Elaborate + ( fixExprToHsExpr + , elaborateSpecType + , buildSimplifier + ) +where + +import qualified Language.Fixpoint.Types as F +import Control.Arrow +import qualified Language.Haskell.Liquid.GHC.Misc + as GM +import Language.Haskell.Liquid.Types.Visitors +import Language.Haskell.Liquid.Types.Types +import Language.Haskell.Liquid.Types.RefType + ( ) +import qualified Data.List as L +import qualified Data.HashMap.Strict as M +import qualified Data.HashSet as S +import Control.Monad.Free +import Data.Functor.Foldable +import Data.Char ( isUpper ) +import GHC +import GhcPlugins ( isDFunId + , gopt_set + ) +import OccName +import FastString +import CoreSyn +import PrelNames +import qualified Outputable as O +import TysWiredIn ( boolTyCon + , true_RDR + ) +import ErrUtils +import RdrName +import BasicTypes +import Data.Default ( def ) +import qualified Data.Maybe as Mb +import CoreSubst hiding ( substExpr ) +import SimplCore +import CoreMonad +import CoreFVs ( exprFreeVarsList ) +import VarEnv ( lookupVarEnv + , lookupInScope + ) +import CoreUtils ( mkTick ) +import qualified Data.HashMap.Strict as M + +lookupIdSubstAll :: O.SDoc -> M.HashMap Id CoreExpr -> Id -> CoreExpr +lookupIdSubstAll doc env v + | Just e <- M.lookup v env = e + | otherwise = Var v + -- Vital! See Note [Extending the Subst] + -- | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v + -- $$ ppr in_scope) + +substExprAll :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr +substExprAll doc subst orig_expr = subst_expr_all doc subst orig_expr + + +subst_expr_all :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr +subst_expr_all doc subst expr = go expr + where + go (Var v) = lookupIdSubstAll (doc O.$$ O.text "subst_expr_all") subst v + go (Type ty ) = Type ty + go (Coercion co ) = Coercion co + go (Lit lit ) = Lit lit + go (App fun arg ) = App (go fun) (go arg) + go (Tick tickish e ) = Tick tickish (go e) + go (Cast e co ) = Cast (go e) co + -- Do not optimise even identity coercions + -- Reason: substitution applies to the LHS of RULES, and + -- if you "optimise" an identity coercion, you may + -- lose a binder. We optimise the LHS of rules at + -- construction time + + go (Lam bndr body) = Lam bndr (subst_expr_all doc subst body) + + go (Let bind body) = Let (mapBnd go bind) (subst_expr_all doc subst body) + + go (Case scrut bndr ty alts) = Case (go scrut) + bndr + ty + (map (go_alt subst) alts) + + go_alt subst (con, bndrs, rhs) = (con, bndrs, subst_expr_all doc subst rhs) + + +mapBnd :: (Expr b -> Expr b) -> Bind b -> Bind b +mapBnd f (NonRec b e) = NonRec b (f e) +mapBnd f (Rec bs ) = Rec (map (second f) bs) + +-- substLet :: CoreExpr -> CoreExpr +-- substLet (Lam b body) = Lam b (substLet body) +-- substLet (Let b body) +-- | NonRec x e <- b = substLet +-- (substExprAll O.empty (extendIdSubst emptySubst x e) body) +-- | otherwise = Let b (substLet body) +-- substLet e = e + + +buildDictSubst :: CoreProgram -> M.HashMap Id CoreExpr +buildDictSubst = cata f + where + f Nil = M.empty + f (Cons b s) + | NonRec x e <- b, isDFunId x -- || isDictonaryId x + = M.insert x e s + | otherwise = s + +buildSimplifier :: CoreProgram -> CoreExpr -> Ghc CoreExpr +buildSimplifier cbs e = pure e-- do + -- df <- getDynFlags + -- liftIO $ simplifyExpr (df `gopt_set` Opt_SuppressUnfoldings) e' + -- where + -- -- fvs = fmap (\x -> (x, getUnique x, isLocalId x)) (freeVars mempty e) + -- dictSubst = buildDictSubst cbs + -- e' = substExprAll O.empty dictSubst e + + +-- | Base functor of RType +data RTypeF c tv r f + = RVarF { + rtf_var :: !tv + , rtf_reft :: !r + } + + | RFunF { + rtf_bind :: !F.Symbol + , rtf_in :: !f + , rtf_out :: !f + , rtf_reft :: !r + } + + | RImpFF { + rtf_bind :: !F.Symbol + , rtf_in :: !f + , rtf_out :: !f + , rtf_reft :: !r + } + + | RAllTF { + rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ())) + , rtf_ty :: !f + , rtf_ref :: !r + } + + -- | "forall x y . TYPE" + -- ^^^^^^^^^^^^^^^^^^^ (rtf_pvbind) + | RAllPF { + rtf_pvbind :: !(PVU c tv) -- ar (RType c tv ())) + , rtf_ty :: !f + } + + -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`) + -- * the `RProp` denoted by `{\h -> v > h}` to + -- * the `RTyCon` denoted by `[]`. + | RAppF { + rtf_tycon :: !c + , rtf_args :: ![f] + , rtf_pargs :: ![RTPropF c tv f] + , rtf_reft :: !r + } + + | RAllEF { + rtf_bind :: !F.Symbol + , rtf_allarg :: !f + , rtf_ty :: !f + } + + | RExF { + rtf_bind :: !F.Symbol + , rtf_exarg :: !f + , rtf_ty :: !f + } + + | RExprArgF (F.Located F.Expr) + + | RAppTyF{ + rtf_arg :: !f + , rtf_res :: !f + , rtf_reft :: !r + } + + | RRTyF { + rtf_env :: ![(F.Symbol, f)] + , rtf_ref :: !r + , rtf_obl :: !Oblig + , rtf_ty :: !f + } + + | RHoleF r + deriving (Functor) + +-- It's probably ok to treat (RType c tv ()) as a leaf.. +type RTPropF c tv f = Ref (RType c tv ()) f + + +-- | SpecType with Holes. +-- It provides us a context to construct the ghc queries. +-- I don't think we can reuse RHole since it is not intended +-- for this use case + +type SpecTypeF = RTypeF RTyCon RTyVar RReft +type PartialSpecType = Free SpecTypeF () + +type instance Base (RType c tv r) = RTypeF c tv r + +instance Recursive (RType c tv r) where + project (RVar var reft ) = RVarF var reft + project (RFun bind tin tout reft) = RFunF bind tin tout reft + project (RImpF bind tin tout reft) = RImpFF bind tin tout reft + project (RAllT tvbind ty ref ) = RAllTF tvbind ty ref + project (RAllP pvbind ty ) = RAllPF pvbind ty + project (RApp c args pargs reft ) = RAppF c args pargs reft + project (RAllE bind allarg ty ) = RAllEF bind allarg ty + project (REx bind exarg ty ) = RExF bind exarg ty + project (RExprArg e ) = RExprArgF e + project (RAppTy arg res reft ) = RAppTyF arg res reft + project (RRTy env ref obl ty ) = RRTyF env ref obl ty + project (RHole r ) = RHoleF r + +instance Corecursive (RType c tv r) where + embed (RVarF var reft ) = RVar var reft + embed (RFunF bind tin tout reft) = RFun bind tin tout reft + embed (RImpFF bind tin tout reft) = RImpF bind tin tout reft + embed (RAllTF tvbind ty ref ) = RAllT tvbind ty ref + embed (RAllPF pvbind ty ) = RAllP pvbind ty + embed (RAppF c args pargs reft ) = RApp c args pargs reft + embed (RAllEF bind allarg ty ) = RAllE bind allarg ty + embed (RExF bind exarg ty ) = REx bind exarg ty + embed (RExprArgF e ) = RExprArg e + embed (RAppTyF arg res reft ) = RAppTy arg res reft + embed (RRTyF env ref obl ty ) = RRTy env ref obl ty + embed (RHoleF r ) = RHole r + + +-- specTypeToLHsType :: SpecType -> LHsType GhcPs +-- specTypeToLHsType = typeToLHsType . toType + +-- -- Given types like x:a -> y:a -> _, this function returns x:a -> y:a -> Bool +-- -- Free monad takes care of substitution + +-- A one-way function. Kind of like injecting something into Maybe +specTypeToPartial :: forall a . SpecType -> SpecTypeF (Free SpecTypeF a) +specTypeToPartial = hylo (fmap wrap) project + +-- probably should return spectype instead.. +plugType :: SpecType -> PartialSpecType -> SpecType +plugType t = refix . f + where + f = hylo Fix $ \case + Pure _ -> specTypeToPartial t + Free res -> res + +-- build the expression we send to ghc for elaboration +-- YL: tweak this function to see if ghc accepts explicit dictionary binders +-- returning both expressions and binders since ghc adds unique id to the expressions + +collectSpecTypeBinders :: SpecType -> [F.Symbol] +collectSpecTypeBinders = para $ \case + RFunF bind (tin, _) (_, bs) _ | isClassType tin -> bs + | otherwise -> bind : bs + RImpFF bind (tin, _) (_, bs) _ | isClassType tin -> bs + | otherwise -> bind : bs + RAllEF b _ (_, res) -> b : res + RAllTF _ (_, res) _ -> res + RExF b _ (_, res) -> b : res + RAppTyF _ (_, res) _ -> res + RRTyF _ _ _ (_, res) -> res + _ -> [] + +-- really should be fused with collectBinders. However, we need the binders +-- to correctly convert fixpoint expressions to ghc expressions because of +-- namespace related issues (whether the symbol denotes a varName or a datacon) +buildHsExpr :: LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs +buildHsExpr res = para $ \case + RFunF bind (tin, _) (_, res) _ + | isClassType tin -> res + | otherwise -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] res + RImpFF bind (tin, _) (_, res) _ + | isClassType tin -> res + | otherwise -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] res + RAllEF _ _ (_, res) -> res + RAllTF _ (_, res) _ -> res + RExF _ _ (_, res) -> res + RAppTyF _ (_, res) _ -> res + RRTyF _ _ _ (_, res) -> res + _ -> res + + + +canonicalizeDictBinder + :: F.Subable a => [F.Symbol] -> (a, [F.Symbol]) -> (a, [F.Symbol]) +canonicalizeDictBinder [] (e', bs') = (e', bs') +canonicalizeDictBinder bs (e', [] ) = (e', bs) +canonicalizeDictBinder bs (e', bs') = (renameDictBinder bs bs' e', bs) + where + renameDictBinder :: (F.Subable a) => [F.Symbol] -> [F.Symbol] -> a -> a + renameDictBinder [] _ = id + renameDictBinder _ [] = id + renameDictBinder canonicalDs ds = F.substa $ \x -> M.lookupDefault x x tbl + where tbl = F.notracepp "TBL" $ M.fromList (zip ds canonicalDs) + +elaborateSpecType + :: (CoreExpr -> F.Expr) + -> (CoreExpr -> Ghc CoreExpr) + -> SpecType + -> Ghc SpecType +elaborateSpecType coreToLogic simplifier t = do + (t', xs) <- elaborateSpecType' (pure ()) coreToLogic simplifier t + case xs of + _ : _ -> panic + Nothing + "elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed" + _ -> pure t' + +elaborateSpecType' + :: PartialSpecType + -> (CoreExpr -> F.Expr) -- core to logic + -> (CoreExpr -> Ghc CoreExpr) + -> SpecType + -> Ghc (SpecType, [F.Symbol]) -- binders for dictionaries + -- should have returned Maybe [F.Symbol] +elaborateSpecType' partialTp coreToLogic simplify t = + case F.notracepp "elaborateSpecType'" t of + RVar (RTV tv) (MkUReft reft@(F.Reft (vv, _oldE)) p) -> do + elaborateReft + (reft, t) + (pure (t, [])) + (\bs' ee -> pure (RVar (RTV tv) (MkUReft (F.Reft (vv, ee)) p), bs')) + -- YL : Fix + RFun bind tin tout ureft@(MkUReft reft@(F.Reft (vv, _oldE)) p) -> do + -- the reft is never actually used by the child + -- maybe i should enforce this information at the type level + let partialFunTp = + Free (RFunF bind (wrap $ specTypeToPartial tin) (pure ()) ureft) :: PartialSpecType + partialTp' = partialTp >> partialFunTp :: PartialSpecType + (eTin , bs ) <- elaborateSpecType' partialTp coreToLogic simplify tin + (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout + let buildRFunContTrivial + | isClassType tin, dictBinder : bs0' <- bs' = do + let (eToutRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eTout, bs0') + pure + ( F.notracepp "RFunTrivial0" + $ RFun dictBinder eTin eToutRenamed ureft + , canonicalBinders + ) + | otherwise = do + let (eToutRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eTout, bs') + pure + ( F.notracepp "RFunTrivial1" $ RFun bind eTin eToutRenamed ureft + , canonicalBinders + ) + buildRFunCont bs'' ee + | isClassType tin, dictBinder : bs0' <- bs' = do + let (eToutRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eTout, bs0') + (eeRenamed, canonicalBinders') = + canonicalizeDictBinder canonicalBinders (ee, bs'') + pure + ( RFun dictBinder + eTin + eToutRenamed + (MkUReft (F.Reft (vv, eeRenamed)) p) + , canonicalBinders' + ) + | otherwise = do + let (eToutRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eTout, bs') + (eeRenamed, canonicalBinders') = + canonicalizeDictBinder canonicalBinders (ee, bs'') + pure + ( RFun bind + eTin + eToutRenamed + (MkUReft (F.Reft (vv, eeRenamed)) p) + , canonicalBinders' + ) + elaborateReft (reft, t) buildRFunContTrivial buildRFunCont + + -- (\bs' ee | isClassType tin -> do + -- let eeRenamed = renameDictBinder canonicalBinders bs' ee + -- pure (RFun bind eTin eToutRenamed (MkUReft (F.Reft (vv, eeRenamed)) p), bs') + -- ) + -- YL: implicit dictionary param doesn't seem possible.. + RImpF bind tin tout ureft@(MkUReft reft@(F.Reft (vv, _oldE)) p) -> do + let partialFunTp = + Free (RImpFF bind (wrap $ specTypeToPartial tin) (pure ()) ureft) :: PartialSpecType + partialTp' = partialTp >> partialFunTp :: PartialSpecType + (eTin , bs ) <- elaborateSpecType' partialTp' coreToLogic simplify tin + (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout + let (eToutRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eTout, bs') + + -- eTin and eTout might have different dictionary names + -- need to do a substitution to make the reference to dictionaries consistent + -- if isClassType eTin + elaborateReft + (reft, t) + (pure (RImpF bind eTin eToutRenamed ureft, canonicalBinders)) + (\bs'' ee -> do + let (eeRenamed, canonicalBinders') = + canonicalizeDictBinder canonicalBinders (ee, bs'') + pure + ( RImpF bind eTin eTout (MkUReft (F.Reft (vv, eeRenamed)) p) + , canonicalBinders' + ) + ) + -- support for RankNTypes/ref + RAllT (RTVar tv ty) tout ureft@(MkUReft ref@(F.Reft (vv, _oldE)) p) -> do + (eTout, bs) <- elaborateSpecType' + (partialTp >> Free (RAllTF (RTVar tv ty) (pure ()) ureft)) + coreToLogic + simplify + tout + elaborateReft + (ref, RVar tv mempty) + (pure (RAllT (RTVar tv ty) eTout ureft, bs)) + (\bs' ee -> + let (eeRenamed, canonicalBinders) = + canonicalizeDictBinder bs (ee, bs') + in pure + ( RAllT (RTVar tv ty) eTout (MkUReft (F.Reft (vv, eeRenamed)) p) + , canonicalBinders + ) + ) + -- pure (RAllT (RTVar tv ty) eTout ref, bts') + -- todo: might as well print an error message? + RAllP pvbind tout -> do + (eTout, bts') <- elaborateSpecType' + (partialTp >> Free (RAllPF pvbind (pure ()))) + coreToLogic + simplify + tout + pure (RAllP pvbind eTout, bts') + -- pargs not handled for now + -- RApp tycon args pargs reft + RApp tycon args pargs ureft@(MkUReft reft@(F.Reft (vv, _)) p) + | isClass tycon -> pure (t, []) + | otherwise -> elaborateReft + (reft, t) + (pure (RApp tycon args pargs ureft, [])) + (\bs' ee -> + pure (RApp tycon args pargs (MkUReft (F.Reft (vv, ee)) p), bs') + ) + RAppTy arg res ureft@(MkUReft reft@(F.Reft (vv, _)) p) -> do + (eArg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify arg + (eRes, bs') <- elaborateSpecType' partialTp coreToLogic simplify res + let (eResRenamed, canonicalBinders) = + canonicalizeDictBinder bs (eRes, bs') + elaborateReft + (reft, t) + (pure (RAppTy eArg eResRenamed ureft, canonicalBinders)) + (\bs'' ee -> + let (eeRenamed, canonicalBinders') = + canonicalizeDictBinder canonicalBinders (ee, bs'') + in pure + ( RAppTy eArg eResRenamed (MkUReft (F.Reft (vv, eeRenamed)) p) + , canonicalBinders' + ) + ) + -- todo: Existential support + RAllE bind allarg ty -> do + (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg + (eTy , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty + let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs') + pure (RAllE bind eAllarg eTyRenamed, canonicalBinders) + REx bind allarg ty -> do + (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg + (eTy , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty + let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs') + pure (REx bind eAllarg eTyRenamed, canonicalBinders) + -- YL: might need to filter RExprArg out and replace RHole with ghc wildcard + -- in the future + RExprArg _ -> impossible Nothing "RExprArg should not appear here" + RHole _ -> impossible Nothing "RHole should not appear here" + RRTy _ _ _ _ -> + todo Nothing ("Not sure how to elaborate RRTy" ++ F.showpp t) + where + boolType = RApp (RTyCon boolTyCon [] def) [] [] mempty :: SpecType + elaborateReft + :: (F.PPrint a) + => (F.Reft, SpecType) + -> Ghc a + -> ([F.Symbol] -> F.Expr -> Ghc a) + -> Ghc a + elaborateReft (reft@(F.Reft (vv, e)), vvTy) trivial nonTrivialCont = + if isTrivial reft + then trivial + else do +-- liftIO $ putStrLn query + let + querySpecType = + plugType (rFun vv vvTy boolType) partialTp :: SpecType + origBinders = collectSpecTypeBinders querySpecType + hsExpr = + buildHsExpr (fixExprToHsExpr (S.fromList origBinders) e) + querySpecType :: LHsExpr GhcPs + exprWithTySigs = + GM.notracePpr "exprWithTySigs" $ noLoc $ ExprWithTySig + (mkLHsSigWcType $ specTypeToLHsType + (F.notracepp "querySpecType" querySpecType) + ) + hsExpr :: LHsExpr GhcPs + (msgs, mbExpr) <- GM.elaborateHsExprInst exprWithTySigs + case mbExpr of + Nothing -> panic + Nothing + ( "Ghc is unable to elaborate the expression: " + ++ GM.showPpr exprWithTySigs + ++ "\n" + ++ -- GM.showPpr + (GM.showSDoc $ O.sep (pprErrMsgBagWithLoc (snd msgs))) + ) + Just eeWithLamsCore -> do + eeWithLamsCore' <- simplify eeWithLamsCore + let + eeWithLams = + coreToLogic (GM.notracePpr "eeWithLamsCore" eeWithLamsCore') + (bs', ee) = F.notracepp "grabLams" $ grabLams ([], eeWithLams) + (dictbs, nondictbs) = + L.partition (F.isPrefixOfSym (F.symbol "$d")) bs' + -- invariant: length nondictbs == length origBinders + subst = if length nondictbs == length origBinders + then F.notracepp "SUBST" $ zip (L.reverse nondictbs) origBinders + else panic + Nothing + "Oops, Ghc gave back more/less binders than I expected" + ret <- nonTrivialCont + dictbs + (F.notracepp "nonTrivialContEE" . eliminateEta $ F.substa + (\x -> Mb.fromMaybe x (L.lookup x subst)) + ee + ) -- (GM.dropModuleUnique <$> bs') + pure (F.notracepp "result" ret) + -- (F.substa ) + isTrivial :: F.Reft -> Bool + isTrivial (F.Reft (_, F.PTrue)) = True + isTrivial _ = False + + grabLams :: ([F.Symbol], F.Expr) -> ([F.Symbol], F.Expr) + grabLams (bs, F.ELam (b, _) e) = grabLams (b : bs, e) + grabLams bse = bse + -- dropBinderUnique :: [F.Symbol] -> F.Expr -> F.Expr + -- dropBinderUnique binders = F.notracepp "ElaboratedExpr" + -- . F.substa (\x -> if L.elem x binders then GM.dropModuleUnique x else x) + + + + +-- | Embed fixpoint expressions into parsed haskell expressions. +-- It allows us to bypass the GHC parser and use arbitrary symbols +-- for identifiers (compared to using the string API) +fixExprToHsExpr :: S.HashSet F.Symbol -> F.Expr -> LHsExpr GhcPs +fixExprToHsExpr env (F.ECon c) = constantToHsExpr c +fixExprToHsExpr env (F.EVar x) = nlHsVar (symbolToRdrName env x) +fixExprToHsExpr env (F.EApp e0 e1) = + mkHsApp (fixExprToHsExpr env e0) (fixExprToHsExpr env e1) +fixExprToHsExpr env (F.ENeg e) = + mkHsApp (nlHsVar (nameRdrName negateName)) (fixExprToHsExpr env e) + +fixExprToHsExpr env (F.EBin bop e0 e1) = mkHsApp + (mkHsApp (bopToHsExpr bop) (fixExprToHsExpr env e0)) + (fixExprToHsExpr env e1) +fixExprToHsExpr env (F.EIte p e0 e1) = nlHsIf (fixExprToHsExpr env p) + (fixExprToHsExpr env e0) + (fixExprToHsExpr env e1) + +-- FIXME: convert sort to HsType +fixExprToHsExpr env (F.ECst e0 _ ) = fixExprToHsExpr env e0 +-- fixExprToHsExpr env (F.PAnd [] ) = nlHsVar true_RDR +fixExprToHsExpr env (F.PAnd [] ) = nlHsVar true_RDR +fixExprToHsExpr env (F.PAnd (e : es)) = L.foldr f (fixExprToHsExpr env e) es + where + f x acc = mkHsApp (mkHsApp (nlHsVar and_RDR) (fixExprToHsExpr env x)) acc + +-- This would work in the latest commit +-- fixExprToHsExpr env (F.PAnd es ) = mkHsApp +-- (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "and"))) +-- (nlList $ fixExprToHsExpr env <$> es) +fixExprToHsExpr env (F.POr es) = mkHsApp + (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "or"))) + (nlList $ fixExprToHsExpr env <$> es) +fixExprToHsExpr env (F.PIff e0 e1) = mkHsApp + (mkHsApp (nlHsVar (mkVarUnqual (mkFastString "<=>"))) (fixExprToHsExpr env e0) + ) + (fixExprToHsExpr env e1) +fixExprToHsExpr env (F.PNot e) = + mkHsApp (nlHsVar not_RDR) (fixExprToHsExpr env e) +fixExprToHsExpr env (F.PAtom brel e0 e1) = mkHsApp + (mkHsApp (brelToHsExpr brel) (fixExprToHsExpr env e0)) + (fixExprToHsExpr env e1) +fixExprToHsExpr env (F.PImp e0 e1) = mkHsApp + (mkHsApp (nlHsVar (mkVarUnqual (mkFastString "==>"))) (fixExprToHsExpr env e0) + ) + (fixExprToHsExpr env e1) + +fixExprToHsExpr env e = + todo Nothing ("toGhcExpr: Don't know how to handle " ++ show e) + +constantToHsExpr :: F.Constant -> LHsExpr GhcPs +-- constantToHsExpr (F.I c) = noLoc (HsLit NoExt (HsInt NoExt (mkIntegralLit c))) +constantToHsExpr (F.I i) = + noLoc (HsOverLit NoExt (mkHsIntegral (mkIntegralLit i))) +constantToHsExpr (F.R d) = + noLoc (HsOverLit NoExt (mkHsFractional (mkFractionalLit d))) +constantToHsExpr _ = + todo Nothing "constantToHsExpr: Not sure how to handle constructor L" + +-- This probably won't work because of the qualifiers +bopToHsExpr :: F.Bop -> LHsExpr GhcPs +bopToHsExpr bop = noLoc (HsVar NoExt (noLoc (f bop))) + where + f F.Plus = plus_RDR + f F.Minus = minus_RDR + f F.Times = times_RDR + f F.Div = mkVarUnqual (fsLit "/") + f F.Mod = varQual_RDR gHC_REAL (fsLit "mod") + f F.RTimes = times_RDR + f F.RDiv = varQual_RDR gHC_REAL (fsLit "/") + +brelToHsExpr :: F.Brel -> LHsExpr GhcPs +brelToHsExpr brel = noLoc (HsVar NoExt (noLoc (f brel))) + where + f F.Eq = mkVarUnqual (mkFastString "==") + f F.Gt = gt_RDR + f F.Lt = lt_RDR + f F.Ge = ge_RDR + f F.Le = le_RDR + f F.Ne = mkVarUnqual (mkFastString "/=") + f _ = impossible Nothing "brelToExpr: Unsupported operation" + +symbolToRdrNameNs :: NameSpace -> F.Symbol -> RdrName +symbolToRdrNameNs ns x + | F.isNonSymbol modName = mkUnqual ns (mkFastString (F.symbolString s)) + | otherwise = mkQual + ns + (mkFastString (F.symbolString modName), mkFastString (F.symbolString s)) + where (modName, s) = GM.splitModuleName x + + +varSymbolToRdrName :: F.Symbol -> RdrName +varSymbolToRdrName = symbolToRdrNameNs varName + + +-- don't use this function... +symbolToRdrName :: S.HashSet F.Symbol -> F.Symbol -> RdrName +symbolToRdrName env x + | F.isNonSymbol modName = mkUnqual ns (mkFastString (F.symbolString s)) + | otherwise = mkQual + ns + (mkFastString (F.symbolString modName), mkFastString (F.symbolString s)) + where + (modName, s) = GM.splitModuleName x + ns | not (S.member x env), Just (c, _) <- F.unconsSym s, isUpper c = dataName + | otherwise = varName + + +specTypeToLHsType :: SpecType -> LHsType GhcPs +-- surprised that the type application is necessary +specTypeToLHsType = + flip (ghylo (distPara @SpecType) distAna) (fmap pure . project) $ \case + RVarF (RTV tv) _ -> nlHsTyVar (symbolToRdrNameNs tvName (F.symbol tv)) -- (getRdrName tv) + RFunF _ (tin, tin') (_, tout) _ + | isClassType tin -> noLoc $ HsQualTy NoExt (noLoc [tin']) tout + | otherwise -> nlHsFunTy tin' tout + RImpFF _ (_, tin) (_, tout) _ -> nlHsFunTy tin tout + RAllTF (ty_var_value -> (RTV tv)) (_, t) _ -> noLoc $ HsForAllTy + NoExt + (userHsTyVarBndrs noSrcSpan + [-- getRdrName tv + (symbolToRdrNameNs tvName (F.symbol tv))] + ) + t + RAllPF _ (_, ty) -> ty + RAppF RTyCon { rtc_tc = tc } ts _ _ -> nlHsTyConApp + (getRdrName tc) + [ hst | (t, hst) <- ts, notExprArg t ] + where + notExprArg (RExprArg _) = False + notExprArg _ = True + RAllEF _ (_, tin) (_, tout) -> nlHsFunTy tin tout + RExF _ (_, tin) (_, tout) -> nlHsFunTy tin tout + -- impossible + RAppTyF _ (RExprArg _, _) _ -> + impossible Nothing "RExprArg should not appear here" + RAppTyF (_, t) (_, t') _ -> nlHsAppTy t t' + -- YL: todo.. + RRTyF _ _ _ (_, t) -> t + RHoleF _ -> noLoc $ HsWildCardTy NoExt + RExprArgF _ -> + todo Nothing "Oops, specTypeToLHsType doesn't know how to handle RExprArg" + +-- the core expression returned by ghc might be eta-expanded +-- we need to do elimination so Pred doesn't contain lambda terms +eliminateEta :: F.Expr -> F.Expr +eliminateEta (F.EApp e0 e1) = F.EApp (eliminateEta e0) (eliminateEta e1) +eliminateEta (F.ENeg e ) = F.ENeg (eliminateEta e) +eliminateEta (F.EBin bop e0 e1) = + F.EBin bop (eliminateEta e0) (eliminateEta e1) +eliminateEta (F.EIte e0 e1 e2) = + F.EIte (eliminateEta e0) (eliminateEta e1) (eliminateEta e2) +eliminateEta (F.ECst e0 s) = F.ECst (eliminateEta e0) s +eliminateEta (F.ELam (x, t) body) + | F.EApp e0 (F.EVar x') <- ebody, x == x' && notElem x (F.syms e0) = e0 + | otherwise = F.ELam (x, t) ebody + where ebody = eliminateEta body +eliminateEta (F.PAnd es ) = F.PAnd (eliminateEta <$> es) +eliminateEta (F.POr es ) = F.POr (eliminateEta <$> es) +eliminateEta (F.PNot e ) = F.PNot (eliminateEta e) +eliminateEta (F.PImp e0 e1) = F.PImp (eliminateEta e0) (eliminateEta e1) +eliminateEta (F.PAtom brel e0 e1) = + F.PAtom brel (eliminateEta e0) (eliminateEta e1) +eliminateEta e = e diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs index a478ba3c4d..b10077b420 100644 --- a/src/Language/Haskell/Liquid/Bare/Measure.hs +++ b/src/Language/Haskell/Liquid/Bare/Measure.hs @@ -79,7 +79,7 @@ makeUnSorted t defs ta = go $ Ghc.expandTypeSynonyms t go (Ghc.ForAllTy _ t) = go t - go (Ghc.FunTy p t) | Ghc.isClassPred p = go t + go (Ghc.FunTy p t) | GM.isEmbeddedDictType p = go t go (Ghc.FunTy t _) = t go t = t -- this should never happen! @@ -151,11 +151,11 @@ makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon] -------------------------------------------------------------------------------- makeHaskellDataDecls cfg name spec tcs | exactDCFlag cfg = Mb.mapMaybe tyConDataDecl - -- . F.tracepp "makeHaskellDataDecls-3" + -- . F.notracepp "makeHaskellDataDecls-3" . zipMap (hasDataDecl name spec . fst) - -- . F.tracepp "makeHaskellDataDecls-2" + -- . F.notracepp "makeHaskellDataDecls-2" . liftableTyCons - -- . F.tracepp "makeHaskellDataDecls-1" + -- . F.notracepp "makeHaskellDataDecls-1" . filter isReflectableTyCon $ tcs | otherwise = [] @@ -172,7 +172,7 @@ liftableTyCons . filter (not . Ghc.isBoxedTupleTyCon) . F.notracepp "LiftableTCs 1" -- . (`sortDiff` wiredInTyCons) - -- . F.tracepp "LiftableTCs 0" + -- . F.notracepp "LiftableTCs 0" zipMap :: (a -> b) -> [a] -> [(a, b)] zipMap f xs = zip xs (map f xs) @@ -284,7 +284,7 @@ dataConSel dc n Check = mkArrow (zip as (repeat mempty)) [] [] [xt] bareBool dataConSel dc n (Proj i) = mkArrow (zip as (repeat mempty)) [] [] [xt] (mempty <$> ti) where ti = Mb.fromMaybe err $ Misc.getNth (i-1) ts - (as, ts, xt) = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon dc n + (as, ts, xt) = {- F.notracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon dc n err = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields" -- bkDataCon :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft)) diff --git a/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs index 6939fd76f9..05f5c8fbf9 100644 --- a/src/Language/Haskell/Liquid/Bare/Misc.hs +++ b/src/Language/Haskell/Liquid/Bare/Misc.hs @@ -96,7 +96,7 @@ mapTyVars :: Type -> SpecType -> StateT MapTyVarST (Either Error) () mapTyVars t (RImpF _ _ t' _) = mapTyVars t t' mapTyVars (FunTy τ τ') t - | isClassPred τ + | isEmbeddedDictType τ = mapTyVars τ' t mapTyVars (FunTy τ τ') (RFun _ t t' _) = mapTyVars τ t >> mapTyVars τ' t' diff --git a/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs index 3980eed77c..d4d2a911c1 100644 --- a/src/Language/Haskell/Liquid/Bare/Plugged.hs +++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs @@ -50,7 +50,7 @@ makePluggedSig :: ModName -> F.TCEmb Ghc.TyCon -> TyConMap -> Ghc.NameSet -> LocSpecType makePluggedSig name embs tyi exports kx t - | Just x <- kxv = mkPlug x + | Just x <- kxv = F.notracepp ("makePluggedSig:" ++ F.showpp t) $ mkPlug x | otherwise = t where kxv = Bare.plugSrc kx @@ -209,7 +209,7 @@ goPlug :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> (Doc -> Doc -> Error) -> (SpecTy -> SpecType goPlug tce tyi err f = go where - go t (RHole r) = (addHoles t') { rt_reft = f t r } + go t (RHole r) = (F.notracepp "goPlug" $ addHoles t') { rt_reft = f t r } where t' = everywhere (mkT $ addRefs tce tyi) t addHoles = everywhere (mkT $ addHole) diff --git a/src/Language/Haskell/Liquid/Bare/Resolve.hs b/src/Language/Haskell/Liquid/Bare/Resolve.hs index a6268439cd..f25992391d 100644 --- a/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -687,7 +687,7 @@ maybeResolveSym env name kind x = case resolveLocSym env name kind x of -- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors ------------------------------------------------------------------------------- ofBareType :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType -ofBareType env name l ps t = either fail id (ofBareTypeE env name l ps t) +ofBareType env name l ps t = F.notracepp ("ofBareType:" ++ F.showpp name) $ either fail id (ofBareTypeE env name l ps t) where fail = Ex.throw -- fail = Misc.errorP "error-ofBareType" . F.showpp @@ -983,4 +983,4 @@ type SymMap = M.HashMap F.Symbol F.Symbol --------------------------------------------------------------------------------- partitionLocalBinds :: [(Ghc.Var, a)] -> ([(Ghc.Var, a)], [(Ghc.Var, a)]) --------------------------------------------------------------------------------- -partitionLocalBinds = L.partition (Mb.isJust . localKey . fst) \ No newline at end of file +partitionLocalBinds = L.partition (Mb.isJust . localKey . fst) diff --git a/src/Language/Haskell/Liquid/Bare/ToBare.hs b/src/Language/Haskell/Liquid/Bare/ToBare.hs index 99a595cf49..5bca2cab3c 100644 --- a/src/Language/Haskell/Liquid/Bare/ToBare.hs +++ b/src/Language/Haskell/Liquid/Bare/ToBare.hs @@ -25,7 +25,7 @@ specToBare :: SpecType -> BareType -------------------------------------------------------------------------------- specToBare = txRType specToBareTC specToBareTV --- specToBare t = F.tracepp ("specToBare t2 = " ++ F.showpp t2) t1 +-- specToBare t = F.notracepp ("specToBare t2 = " ++ F.showpp t2) t1 -- where -- t1 = bareOfType . toType $ t -- t2 = _specToBare t diff --git a/src/Language/Haskell/Liquid/Constraint/Fresh.hs b/src/Language/Haskell/Liquid/Constraint/Fresh.hs index db7ee7360a..f436f98ef8 100644 --- a/src/Language/Haskell/Liquid/Constraint/Fresh.hs +++ b/src/Language/Haskell/Liquid/Constraint/Fresh.hs @@ -80,7 +80,7 @@ freshTy_expr k e _ = freshTy_reftype k $ exprRefType e freshTy_reftype :: KVKind -> SpecType -> CG SpecType freshTy_reftype k _t = (fixTy t >>= refresh) =>> addKVars k where - t = {- F.tracepp ("freshTy_reftype:" ++ show k) -} _t + t = {- F.notracepp ("freshTy_reftype:" ++ show k) -} _t -- | Used to generate "cut" kvars for fixpoint. Typically, KVars for recursive -- definitions, and also to update the KVar profile. @@ -103,7 +103,7 @@ addKuts _x t = modify $ \s -> s { kuts = mappend (F.KS ks) (kuts s) } ks' = S.fromList $ specTypeKVars t ks | S.null ks' = ks' - | otherwise = {- F.tracepp ("addKuts: " ++ showpp _x) -} ks' + | otherwise = {- F.notracepp ("addKuts: " ++ showpp _x) -} ks' specTypeKVars :: SpecType -> [F.KVar] specTypeKVars = foldReft (\ _ r ks -> (kvars $ ur_reft r) ++ ks) [] diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index aeeefbbad2..67f783164f 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -297,7 +297,7 @@ doTermCheck :: Config -> Bind Var -> CG Bool doTermCheck cfg bind = do lazyVs <- specLazy <$> get termVs <- specTmVars <$> get - let skip = any (\x -> S.member x lazyVs || GM.isInternal x) xs + let skip = any (\x -> S.member x lazyVs || GM.isEmbeddedDictVar x) xs let chk = not (structuralTerm cfg) || any (\x -> S.member x termVs) xs return $ chk && not skip where @@ -318,7 +318,7 @@ consCBSizedTys γ xes let rts = (recType autoenv <$>) <$> xeets let xts = zip xs ts γ' <- foldM extender γ xts - let γs = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isPredVar) <$> vs) + let γs = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isEmbeddedDictVar) <$> vs) let xets' = zip3 xs es ts mapM_ (uncurry $ consBind True) (zip γs xets') return γ' @@ -724,7 +724,7 @@ splitConstraints :: TyConable c => RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r) splitConstraints (RRTy cs _ OCons t) = let (css, t') = splitConstraints t in (cs:css, t') -splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isClass c +splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c = let (css, t') = splitConstraints t in (css, RFun x tx t' r) splitConstraints t = ([], t) @@ -1122,7 +1122,7 @@ dropExists γ (REx x tx t) = (, t) <$> γ += ("dropExists", x, tx) dropExists γ t = return (γ, t) dropConstraints :: CGEnv -> SpecType -> CG SpecType -dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isClass c +dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c = (flip (RFun x tx)) r <$> dropConstraints γ t dropConstraints γ (RRTy cts _ OCons t) = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts @@ -1161,7 +1161,7 @@ caseEnv γ x _ (DataAlt c) ys pIs = do tdc <- (γ ??= (dataConWorkId c) >>= refreshVV) let (rtd,yts',_) = unfoldR tdc xt ys yts <- projectTypes pIs yts' - let ys'' = F.symbol <$> filter (not . GM.isPredVar) ys + let ys'' = F.symbol <$> filter (not . GM.isEmbeddedDictVar) ys let r1 = dataConReft c ys'' let r2 = dataConMsReft rtd ys'' let xt = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2)) @@ -1305,7 +1305,7 @@ lamExpr γ (Lit c) = snd $ literalConst (emb γ) c lamExpr γ (Tick _ e) = lamExpr γ e lamExpr γ (App e (Type _)) = lamExpr γ e lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of - (Just p1, Just p2) | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2) + (Just p1, Just p2) | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2) -> Just $ F.EApp p1 p2 (Just p1, Just _ ) -> Just p1 _ -> Nothing @@ -1334,7 +1334,7 @@ varRefType :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType -------------------------------------------------------------------------------- varRefType γ x = do xt <- varRefType' γ x <$> (γ ??= x) - return xt -- F.tracepp (printf "varRefType x = [%s]" (showpp x)) + return xt -- F.notracepp (printf "varRefType x = [%s]" (showpp x)) varRefType' :: CGEnv -> Var -> SpecType -> SpecType varRefType' γ x t' @@ -1357,7 +1357,7 @@ makeSingleton γ e t | higherOrderFlag γ, App f x <- simplify e = case (funExpr γ f, argForAllExpr x) of (Just f', Just x') - | not (GM.isPredExpr x) -- (isClassPred $ exprType x) + | not (GM.isEmbeddedDictExpr x) -- (isClassPred $ exprType x) -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x')) (Just f', Just _) -> strengthenMeet t (uTop $ F.exprReft f') @@ -1382,7 +1382,7 @@ funExpr :: CGEnv -> CoreExpr -> Maybe F.Expr -- reflectefd functions funExpr γ (Var v) | M.member v $ aenv γ - = F.EVar <$> (M.lookup v $ aenv γ) + = F.notracepp "funExpr" $F.EVar <$> (M.lookup v $ aenv γ) -- local function arguments funExpr γ (Var v) | S.member v (fargs γ) || GM.isDataConId v @@ -1390,7 +1390,7 @@ funExpr γ (Var v) | S.member v (fargs γ) || GM.isDataConId v funExpr γ (App e1 e2) = case (funExpr γ e1, argExpr γ e2) of - (Just e1', Just e2') | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2) + (Just e1', Just e2') | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2) -> Just (F.EApp e1' e2') (Just e1', Just _) -> Just e1' @@ -1453,7 +1453,7 @@ isGeneric γ α t = isGenericVar α t && not (isPLETerm γ) -- | @isPLETerm γ@ returns @True@ if the "currrent" top-level binder in γ has PLE enabled. isPLETerm :: CGEnv -> Bool isPLETerm γ - | Just x <- cgVar γ = {- F.tracepp ("isPLEVar:" ++ F.showpp x) $ -} isPLEVar (giSpec . cgInfo $ γ) x + | Just x <- cgVar γ = {- F.notracepp ("isPLEVar:" ++ F.showpp x) $ -} isPLEVar (giSpec . cgInfo $ γ) x | otherwise = False -- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs index ce971bf37d..99fb282ed7 100644 --- a/src/Language/Haskell/Liquid/Constraint/Split.hs +++ b/src/Language/Haskell/Liquid/Constraint/Split.hs @@ -249,7 +249,7 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _)) (Just (x1, _), Just (x2, _)) -> F.mkSubst [(x1, F.EVar x2)] _ -> F.mkSubst [] -splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 +splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isEmbeddedDict c1 && c1 == c2 = return [] splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index af9de86080..9dd3f2b45a 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -85,17 +85,6 @@ makeAxiomEnvironment info xts fcs cfg = getConfig info sp = giSpec info -_isClassOrDict :: Id -> Bool -_isClassOrDict x = F.tracepp ("isClassOrDict: " ++ F.showpp x) - $ (hasClassArg x || GM.isDictionary x || Mb.isJust (Ghc.isClassOpId_maybe x)) - -hasClassArg :: Id -> Bool -hasClassArg x = F.tracepp msg $ (GM.isDataConId x && any Ghc.isClassPred (t:ts)) - where - msg = "hasClassArg: " ++ showpp (x, t:ts) - (ts, t) = Ghc.splitFunTys . snd . Ghc.splitForAllTys . Ghc.varType $ x - - doExpand :: GhcSpec -> Config -> F.SubC Cinfo -> Bool doExpand sp cfg sub = Config.allowGlobalPLE cfg || (Config.allowLocalPLE cfg && maybe False (isPLEVar sp) (subVar sub)) @@ -184,7 +173,7 @@ specTypeToLogic es e t su = F.mkSubst $ zip xs es - (cls, nocls) = L.partition (isClassType.snd) $ zip (ty_binds trep) (ty_args trep) + (cls, nocls) = L.partition (isEmbeddedClass.snd) $ zip (ty_binds trep) (ty_args trep) :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)]) (xs, ts) = unzip nocls :: ([F.Symbol], [SpecType]) diff --git a/src/Language/Haskell/Liquid/GHC/API.hs b/src/Language/Haskell/Liquid/GHC/API.hs index 1dc5068f4f..4700e6ac90 100644 --- a/src/Language/Haskell/Liquid/GHC/API.hs +++ b/src/Language/Haskell/Liquid/GHC/API.hs @@ -3,6 +3,7 @@ module Language.Haskell.Liquid.GHC.API (module Ghc) where import GHC as Ghc +import PrelNames as Ghc (gHC_REAL) import ConLike as Ghc import Var as Ghc import Module as Ghc @@ -19,7 +20,8 @@ import Class as Ghc import Unique as Ghc import RdrName as Ghc import SrcLoc as Ghc -import Name as Ghc hiding (varName) +import Name as Ghc hiding (varName) +import TcType as Ghc (tcSplitMethodTy, tcSplitAppTys) -- import TyCon as Ghc diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs index 32f6f369cf..7a2aed6b7a 100644 --- a/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -217,9 +217,12 @@ configureDynFlags cfg tmp = do , objectDir = Just tmp , hiDir = Just tmp , stubDir = Just tmp + , optLevel = 0 + , ufCreationThreshold = 0 } `gopt_set` Opt_ImplicitImportQualified `gopt_set` Opt_PIC `gopt_set` Opt_DeferTypedHoles + `gopt_set` Opt_SuppressUnfoldings `xopt_set` MagicHash `xopt_set` DeriveGeneric `xopt_set` StandaloneDeriving @@ -431,7 +434,34 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d let modSum = pm_mod_summary (tm_parsed_module typechecked) ghcSrc <- makeGhcSrc cfg file typechecked modSum bareSpecs <- makeBareSpecs cfg depGraph specEnv modSum bareSpec - let ghcSpec = makeGhcSpec cfg ghcSrc logicMap bareSpecs + -- preparing environment for evaluation + setContext [iimport |(modName, _) <- bareSpecs, + let iimport = if isTarget modName + then IIModule (getModName modName) + else IIDecl (simpleImportDecl (getModName modName))] + -- enable partial type inference + dflags <- getSessionDynFlags + setSessionDynFlags (dflags + `xopt_set` + PartialTypeSignatures + `xopt_set` + RankNTypes) + void $ execStmt + "let {infixr 1 ==>; True ==> False = False; _ ==> _ = True}" + execOptions + void $ execStmt + "let {infixr 1 <=>; True <=> False = False; _ <=> _ = True}" + execOptions + void $ execStmt + "let {infix 4 ==; (==) :: a -> a -> Bool; _ == _ = undefined}" + execOptions + void $ execStmt + "let {infix 4 /=; (/=) :: a -> a -> Bool; _ /= _ = undefined}" + execOptions + void $ execStmt + "let {infixl 7 /; (/) :: Num a => a -> a -> a; _ / _ = undefined}" + execOptions + ghcSpec <- makeGhcSpec cfg ghcSrc logicMap bareSpecs _ <- liftIO $ saveLiftedSpec ghcSrc ghcSpec return $ GI ghcSrc ghcSpec @@ -462,7 +492,7 @@ makeGhcSrc cfg file typechecked modSum = do , giTargetMod = ModName Target (moduleName (ms_mod modSum)) , giCbs = coreBinds , giImpVars = impVars - , giDefVars = dataCons ++ (letVars coreBinds) + , giDefVars = dataCons ++ letVars coreBinds , giUseVars = readVars coreBinds , giDerVars = S.fromList (derivedVars cfg modGuts) , gsExports = mgi_exports modGuts @@ -513,7 +543,7 @@ qImports qns = QImports --------------------------------------------------------------------------------------- lookupTyThings :: HscEnv -> TypecheckedModule -> MGIModGuts -> Ghc [(Name, Maybe TyThing)] lookupTyThings hscEnv tcm mg = - forM (mgNames mg) $ \n -> do + forM (mgNames mg ++ instNames mg) $ \n -> do tt1 <- lookupName n tt2 <- liftIO $ Ghc.hscTcRcLookupName hscEnv n tt3 <- modInfoLookupName mi n @@ -553,6 +583,9 @@ _dumpRdrEnv _hscEnv modGuts = do _mgDeps = Ghc.dep_mods . mgi_deps _hscNames = fmap showPpr . Ghc.ic_tythings . Ghc.hsc_IC +instNames :: MGIModGuts -> [Ghc.Name] +instNames = fmap is_dfun_name . join . maybeToList . mgi_cls_inst + mgNames :: MGIModGuts -> [Ghc.Name] mgNames = fmap Ghc.gre_name . Ghc.globalRdrEnvElts . mgi_rdr_env diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs index 7bef43171a..0e8178c873 100644 --- a/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -16,10 +17,23 @@ module Language.Haskell.Liquid.GHC.Misc where -import Class (classKey) +import Class (classKey, classSCSelIds, classBigSig) import Data.String import qualified Data.List as L -import PrelNames (fractionalClassKeys) +import Inst +import GhcMonad +import DsMonad +import Control.Monad.State (evalState, modify, get) +import DsExpr +import RnExpr +import TcRnMonad +import qualified Data.Map.Strict as OM +import TcExpr +import TcSimplify +import GhcPlugins (eqType, nonDetCmpType, getClassPredTys, piResultTys, mkClassPred) +import TcHsSyn +import TcEvidence +import PrelNames (fractionalClassKeys, itName, ordClassKey, numericClassKeys, eqClassKey) import FamInstEnv import Debug.Trace -- import qualified ConLike as Ghc @@ -34,14 +48,14 @@ import qualified CoreSyn as Core import CostCentre import GHC hiding (L) import HscTypes (ModGuts(..), HscEnv(..), FindResult(..), - Dependencies(..)) + Dependencies(..), runInteractiveHsc) import TysWiredIn (anyTy) import NameSet (NameSet) import SrcLoc hiding (L) import Bag import ErrUtils import CoreLint -import CoreMonad +import CoreMonad hiding (getHscEnv) import Text.Parsec.Pos (incSourceColumn, sourceName, sourceLine, sourceColumn, newPos) @@ -56,7 +70,7 @@ import TcRnDriver import RdrName -import Type (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind) +import Type (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind, tyConAppTyCon_maybe, splitForAllTys, coreView) import TyCoRep import Var import IdInfo @@ -219,6 +233,9 @@ unTickExpr x = x isFractionalClass :: Class -> Bool isFractionalClass clas = classKey clas `elem` fractionalClassKeys +isOrdClass :: Class -> Bool +isOrdClass clas = classKey clas == ordClassKey + -------------------------------------------------------------------------------- -- | Pretty Printers ----------------------------------------------------------- -------------------------------------------------------------------------------- @@ -553,7 +570,7 @@ tyConTyVarsDef c | noTyVars c = [] | otherwise = TC.tyConTyVars c --where - -- none = tracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c) + -- none = notracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c) noTyVars :: TyCon -> Bool noTyVars c = (TC.isPrimTyCon c || isFunTyCon c || TC.isPromotedDataCon c) @@ -593,6 +610,9 @@ instance Hashable TyCon where instance Hashable DataCon where hashWithSalt = uniqueHash +instance Hashable Class where + hashWithSalt = uniqueHash + instance Fixpoint Var where toFix = pprDoc @@ -714,6 +734,9 @@ isDictionary = isPrefixOfSym "$f" . dropModuleNames . symbol isMethod :: Symbolic a => a -> Bool isMethod = isPrefixOfSym "$c" . dropModuleNames . symbol +isSCSel :: Symbolic a => a -> Bool +isSCSel = isPrefixOfSym "$p" . dropModuleNames . symbol + isInternal :: Symbolic a => a -> Bool isInternal = isPrefixOfSym "$" . dropModuleNames . symbol @@ -779,6 +802,30 @@ ignoreCoreBinds vs cbs go (Rec xes) = [Rec (filter ((`notElem` vs) . fst) xes)] +findVarDefMethod :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) +findVarDefMethod x cbs = + case rcbs of + (NonRec v def : _ ) -> Just (v, def) + (Rec [(v, def)] : _ ) -> Just (v, def) + _ -> Nothing + where + rcbs | isMethod x = mCbs + | isDictionary (dropModuleNames x) = dCbs + | otherwise = xCbs + xCbs = [ cb | cb <- concatMap unRec cbs, x `elem` coreBindSymbols cb + ] + mCbs = [ cb | cb <- concatMap unRec cbs, x `elem` methodSymbols cb] + dCbs = [ cb | cb <- concatMap unRec cbs, x `elem` dictionarySymbols cb] + unRec (Rec xes) = [NonRec x es | (x,es) <- xes] + unRec nonRec = [nonRec] + +dictionarySymbols :: CoreBind -> [Symbol] +dictionarySymbols = filter isDictionary . map (dropModuleNames . symbol) . binders + + +methodSymbols :: CoreBind -> [Symbol] +methodSymbols = filter isMethod . map (dropModuleNames . symbol) . binders + findVarDef :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) findVarDef x cbs = case xCbs of (NonRec v def : _ ) -> Just (v, def) @@ -802,6 +849,47 @@ binders (Rec xes) = fst <$> xes expandVarType :: Var -> Type expandVarType = expandTypeSynonyms . varType + +-------------------------------------------------------------------------------- +-- | The following functions test if a `CoreExpr` or `CoreVar` can be +-- embedded in logic. With type-class support, we can no longer erase +-- such expressions arbitrarily. +-------------------------------------------------------------------------------- +isEmbeddedDictExpr :: CoreExpr -> Bool +isEmbeddedDictExpr = isEmbeddedDictType . CoreUtils.exprType + +isEmbeddedDictVar :: Var -> Bool +isEmbeddedDictVar v = F.notracepp msg . isEmbeddedDictType . varType $ v + where + msg = "isGoodCaseBind v = " ++ show v + +isEmbeddedDictType :: Type -> Bool +isEmbeddedDictType = anyF [isOrdPred, isNumericPred, isEqPred, isPrelEqPred] + +-- unlike isNumCls, isFracCls, these two don't check if the argument's +-- superclass is Ord or Num. I believe this is the more predictable behavior + +isPrelEqPred :: Type -> Bool +isPrelEqPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> isPrelEqTyCon tyCon + _ -> False + + +isPrelEqTyCon :: TyCon -> Bool +isPrelEqTyCon tc = tc `hasKey` eqClassKey + +isOrdPred :: Type -> Bool +isOrdPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> tyCon `hasKey` ordClassKey + _ -> False + +-- Not just Num, but Fractional, Integral as well +isNumericPred :: Type -> Bool +isNumericPred ty = case tyConAppTyCon_maybe ty of + Just tyCon -> getUnique tyCon `elem` numericClassKeys + _ -> False + + -------------------------------------------------------------------------------- -- | The following functions test if a `CoreExpr` or `CoreVar` are just types -- in disguise, e.g. have `PredType` (in the GHC sense of the word), and so @@ -836,3 +924,111 @@ defaultDataCons (TyConApp tc argτs) ds = do defaultDataCons _ _ = Nothing +-------------------------------------------------------------------------------- +-- | Elaboration +-------------------------------------------------------------------------------- + +-- elaborateExprInst :: GhcMonad m => String -> m (Maybe CoreExpr) +-- elaborateExprInst = elaborateExpr TM_Inst + +-- elaborateExpr :: GhcMonad m => TcRnExprMode -> String -> m (Maybe CoreExpr) +-- elaborateExpr mode expr = +-- withSession $ \hsc_env -> liftIO $ hscElabExpr hsc_env mode expr + +elaborateHsExprInst + :: GhcMonad m => LHsExpr GhcPs -> m (Messages, Maybe CoreExpr) +elaborateHsExprInst expr = elaborateHsExpr TM_Inst expr + + +elaborateHsExpr + :: GhcMonad m => TcRnExprMode -> LHsExpr GhcPs -> m (Messages, Maybe CoreExpr) +elaborateHsExpr mode expr = + withSession $ \hsc_env -> liftIO $ hscElabHsExpr hsc_env mode expr + +hscElabHsExpr :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs -> IO (Messages, Maybe CoreExpr) +hscElabHsExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do + hsc_env <- getHscEnv + liftIO $ elabRnExpr hsc_env mode expr + + + +-- hscElabExpr :: HscEnv -> TcRnExprMode -> String -> IO (Messages, Maybe CoreExpr) +-- hscElabExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do +-- hsc_env <- getHscEnv +-- parsed_expr <- hscParseExpr expr +-- liftIO $ elabRnExpr hsc_env mode parsed_expr + +elabRnExpr + :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs -> IO (Messages, Maybe CoreExpr) +elabRnExpr hsc_env mode rdr_expr = + runTcInteractive hsc_env $ do + (rn_expr, _fvs) <- rnLExpr rdr_expr + failIfErrsM + uniq <- newUnique + let fresh_it = itName uniq (getLoc rdr_expr) + orig = lexprCtOrigin rn_expr + (tclvl, lie, (tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $ do + (_tc_expr, expr_ty) <- tcInferSigma rn_expr + expr_ty' <- if inst + then snd <$> deeplyInstantiate orig expr_ty + else return expr_ty + return (_tc_expr, expr_ty') + (_, _, evbs, residual, _) <- simplifyInfer tclvl + infer_mode + [] {- No sig vars -} + [(fresh_it, res_ty)] + lie + evbs' <- perhaps_disable_default_warnings $ simplifyInteractive residual + full_expr <- zonkTopLExpr (mkHsDictLet (EvBinds evbs') (mkHsDictLet evbs tc_expr)) + initDsTc $ dsLExpr full_expr + where + (inst, infer_mode, perhaps_disable_default_warnings) = case mode of + TM_Inst -> (True, NoRestrictions, id) + TM_NoInst -> (False, NoRestrictions, id) + TM_Default -> (True, EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults) + +newtype HashableType = HashableType {getHType :: Type} + +instance Eq HashableType where + x == y = eqType (getHType x) (getHType y) + +instance Ord HashableType where + compare x y = nonDetCmpType (getHType x) (getHType y) + +instance Outputable HashableType where + ppr = ppr . getHType + + +canonSelectorChains :: PredType -> OM.Map HashableType [Id] +canonSelectorChains t = foldr (OM.unionWith const) mempty (zs : xs) + where + (cls, ts) = getClassPredTys t + scIdTys = classSCSelIds cls + ys = fmap (\d -> (d, piResultTys (idType d) (ts ++ [t]))) scIdTys + zs = OM.fromList $ fmap (\(x, y) -> (HashableType y, [x])) ys + xs = fmap (\(d, t') -> fmap (d :) (canonSelectorChains t')) ys + +buildCoherenceOblig :: Class -> [[([Id], [Id])]] +buildCoherenceOblig cls = evalState (mapM f xs) mempty + where + (ts, _, selIds, _) = classBigSig cls + tts = mkTyVarTy <$> ts + t = mkClassPred cls tts + ys = fmap (\d -> (d, piResultTys (idType d) (tts ++ [t]))) selIds + xs = fmap (\(d, t') -> fmap (d:) (canonSelectorChains t')) ys + f tid = do + ctid' <- get + modify (flip (OM.unionWith const) tid) + pure . OM.elems $ OM.intersectionWith (,) ctid' (fmap tail tid) + + +-- to be zipped onto the super class selectors +coherenceObligToRef :: (F.Symbolic s) => s -> [Id] -> [Id] -> F.Reft +coherenceObligToRef d = coherenceObligToRefE (F.eVar $ F.symbol d) + +coherenceObligToRefE :: F.Expr -> [Id] -> [Id] -> F.Reft +coherenceObligToRefE e rps0 rps1 = F.Reft (F.vv_, F.PAtom F.Eq lhs rhs) + where lhs = L.foldr EApp e ps0 + rhs = L.foldr EApp (F.eVar F.vv_) ps1 + ps0 = F.eVar . F.symbol <$> L.reverse rps0 + ps1 = F.eVar . F.symbol <$> L.reverse rps1 diff --git a/src/Language/Haskell/Liquid/LawInstances.hs b/src/Language/Haskell/Liquid/LawInstances.hs index f01a877bee..071bdc4244 100644 --- a/src/Language/Haskell/Liquid/LawInstances.hs +++ b/src/Language/Haskell/Liquid/LawInstances.hs @@ -90,6 +90,6 @@ splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.S splitTypeConstraints = go [] where go cs (b@(_x, RApp c _ _ _):ts) - | isClass c + | isEmbeddedDict c = go (b:cs) ts go cs r = (reverse cs, map (\(x, t) -> (x, shiftVV t x)) r) diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs index 2e8a67a580..cedf5dace9 100644 --- a/src/Language/Haskell/Liquid/Measure.hs +++ b/src/Language/Haskell/Liquid/Measure.hs @@ -261,7 +261,7 @@ mapArgumens lc t1 t2 = go xts1' xts2' xts1' = dropWhile canDrop xts1 xts2' = dropWhile canDrop xts2 - canDrop (_, t) = isClassType t || isEqType t + canDrop (_, t) = isEmbeddedClass t go xs ys | length xs == length ys && and (zipWith (==) (toRSort . snd <$> xts1') (toRSort . snd <$> xts2')) @@ -300,14 +300,14 @@ stitchArgs sp dc allXs allTs ++ zipWith g xs (ofType <$> ts) | otherwise = panicFieldNumMismatch sp dc nXs nTs where - (pts, ts) = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ isPredTy t) allTs + (pts, ts) = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ isEmbeddedDictType t) allTs (_ , xs) = L.partition (coArg . snd) allXs nXs = length xs nTs = length ts g (x, Just t) _ = (x, t, mempty) g (x, _) t = (x, t, mempty) coArg Nothing = False - coArg (Just t) = isPredTy . toType $ t + coArg (Just t) = isEmbeddedDictType . toType $ t panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3) => SrcSpan -> a3 -> a1 -> a -> a2 diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs index bfbd26ddf0..3a0fb9ed82 100644 --- a/src/Language/Haskell/Liquid/Transforms/ANF.hs +++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs @@ -10,13 +10,13 @@ {-# LANGUAGE OverloadedStrings #-} -module Language.Haskell.Liquid.Transforms.ANF (anormalize) where +module Language.Haskell.Liquid.Transforms.ANF (anormalize, anormalizeExpr) where import Prelude hiding (error) import CoreSyn hiding (mkTyArg) import CoreUtils (exprType) import qualified DsMonad -import DsMonad (initDsWithModGuts) +import DsMonad (initDsWithModGuts, initDsTc) import GHC hiding (exprType) import HscTypes import OccName (OccName, mkVarOccFS) @@ -41,6 +41,7 @@ import Language.Haskell.Liquid.UX.Config as UX import qualified Language.Haskell.Liquid.Misc as Misc import Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.Transforms.Rec +import Language.Haskell.Liquid.Transforms.InlineAux import Language.Haskell.Liquid.Transforms.Rewrite import Language.Haskell.Liquid.Types.Errors @@ -49,7 +50,8 @@ import qualified Language.Haskell.Liquid.GHC.Resugar as Rs import Data.Maybe (fromMaybe) import Data.List (sortBy, (\\)) import Data.Function (on) -import qualified Text.Printf as Printf +import qualified Text.Printf as Printf +import SimplCore -------------------------------------------------------------------------------- -- | A-Normalize a module ------------------------------------------------------ @@ -57,20 +59,31 @@ import qualified Text.Printf as Printf anormalize :: UX.Config -> HscEnv -> ModGuts -> IO [CoreBind] -------------------------------------------------------------------------------- anormalize cfg hscEnv modGuts = do + let df = hsc_dflags hscEnv + aux_cbs = inlineAux (mg_module modGuts) $ mg_binds modGuts + -- rwr_simpl_cbs = rwr_cbs + -- inlineDFun df rwr_cbs + + let orig_cbs = transformRecExpr aux_cbs + rwr_cbs = rewriteBinds cfg orig_cbs + -- rwr_simpl_cbs <- mg_binds <$> core2core hscEnv modGuts {mg_binds = rwr_cbs} + + whenLoud $ do putStrLn "***************************** GHC CoreBinds ***************************" putStrLn $ GM.showCBs untidy (mg_binds modGuts) + putStrLn "***************************** AUX CoreBinds ***************************" + putStrLn $ GM.showCBs untidy aux_cbs putStrLn "***************************** REC CoreBinds ***************************" putStrLn $ GM.showCBs untidy orig_cbs putStrLn "***************************** RWR CoreBinds ***************************" putStrLn $ GM.showCBs untidy rwr_cbs + let act = Misc.concatMapM (normalizeTopBind γ0) rwr_cbs (fromMaybe err . snd) <$> initDsWithModGuts hscEnv modGuts act -- hscEnv m grEnv tEnv emptyFamInstEnv act where err = panic Nothing "Oops, cannot A-Normalize GHC Core!" - act = Misc.concatMapM (normalizeTopBind γ0) rwr_cbs + γ0 = emptyAnfEnv cfg - rwr_cbs = rewriteBinds cfg orig_cbs - orig_cbs = transformRecExpr $ mg_binds modGuts untidy = UX.untidyCore cfg {- @@ -86,10 +99,21 @@ modGutsTypeEnv mg = typeEnvFromEntities ids tcs fis fis = mgi_fam_insts mg -} +anormalizeExpr :: (UX.HasConfig cfg) => cfg -> HscEnv -> CoreExpr -> IO CoreExpr +anormalizeExpr cfg hscEnv e = do + (_, mbE) <- runTcInteractive hscEnv $ initDsTc $ normalizeExpr γ0 e + case mbE of + Nothing -> panic Nothing "Oops, cannot A-Normalize Refinement Expression!" + Just e' -> pure e' + where γ0 = emptyAnfEnv (UX.getConfig cfg) + -------------------------------------------------------------------------------- -- | A-Normalize a @CoreBind@ -------------------------------------------------- -------------------------------------------------------------------------------- +normalizeExpr :: AnfEnv -> CoreExpr -> DsMonad.DsM CoreExpr +normalizeExpr γ e = runDsM $ evalStateT (stitch γ e) (DsST []) + -- Can't make the below default for normalizeBind as it -- fails tests/pos/lets.hs due to GHCs odd let-bindings diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs index aa6d2396d8..36ad09900e 100644 --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -63,7 +63,7 @@ logicType :: (Reftable r) => Type -> RRType r logicType τ = fromRTypeRep $ t { ty_binds = bs, ty_args = as, ty_refts = rs} where t = toRTypeRep $ ofType τ - (bs, as, rs) = unzip3 $ dropWhile (isClassType . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t) + (bs, as, rs) = unzip3 $ dropWhile (isEmbeddedClass . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t) {- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not: CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)} @@ -77,7 +77,7 @@ inlineSpecType v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds = rep = toRTypeRep t res = ty_res rep xs = intSymbol (symbol ("x" :: String)) <$> [1..length $ ty_binds rep] - vxs = dropWhile (isClassType . snd) $ zip xs (ty_args rep) + vxs = dropWhile (isEmbeddedClass . snd) $ zip xs (ty_args rep) f = dummyLoc (symbol v) t = ofType (GM.expandVarType v) :: SpecType mkA = EVar . fst @@ -104,7 +104,7 @@ measureSpecType v = go mkT [] [1..] t go f args i (RAllT a t r) = RAllT a (go f args i t) r go f args i (RAllP p t) = RAllP p $ go f args i t go f args i (RFun x t1 t2 r) - | isClassType t1 = RFun x t1 (go f args i t2) r + | isEmbeddedClass t1 = RFun x t1 (go f args i t2) r go f args i t@(RFun _ t1 t2 r) | hasRApps t = RFun x' t1 (go f (x':args) (tail i) t2) r where x' = intSymbol (symbol ("x" :: String)) (head i) @@ -127,7 +127,7 @@ weakenResult v t = F.notracepp msg t' rep = toRTypeRep t weaken x = pAnd . filter ((Just vE /=) . isSingletonExpr x) . conjuncts vE = mkEApp vF xs - xs = EVar . fst <$> dropWhile (isClassType . snd) xts + xs = EVar . fst <$> dropWhile (isEmbeddedClass . snd) xts xts = zip (ty_binds rep) (ty_args rep) vF = dummyLoc (symbol v) @@ -247,7 +247,7 @@ coreToFun :: LocSymbol -> Var -> C.CoreExpr -> LogicM ([Var], Either Expr Expr) coreToFun _ _v e = go [] $ normalize e where go acc (C.Lam x e) | isTyVar x = go acc e - go acc (C.Lam x e) | isErasable x = go acc e + go acc (C.Lam x e) | GM.isEmbeddedDictVar x = go acc e go acc (C.Lam x e) = go (x:acc) e go acc (C.Tick _ e) = go acc e go acc e = (reverse acc,) . Right <$> coreToLg e @@ -384,6 +384,8 @@ toPredApp p = go . Misc.mapFst opSym . splitArgs $ p = PAnd <$> mapM coreToLg [e1, e2] | f == symbol ("==>" :: String) = PImp <$> coreToLg e1 <*> coreToLg e2 + | f == symbol ("<=>" :: String) + = PIff <$> coreToLg e1 <*> coreToLg e2 go (Just f, [es]) | f == symbol ("or" :: String) = POr . deList <$> coreToLg es @@ -417,10 +419,20 @@ toLogicApp e = do makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr makeApp _ _ f [e] | val f == symbol ("GHC.Num.negate" :: String) = ENeg e + | val f == symbol ("GHC.Num.fromInteger" :: String) + , ECon c <- e + = ECon c + + makeApp _ _ f [e1, e2] | Just op <- M.lookup (val f) bops = EBin op e1 e2 +makeApp _ _ f [e1, e2] | (modName, sym) <- GM.splitModuleName (val f) + , symbol ("Ghci" :: String) `isPrefixOfSym` modName + , Just op <- M.lookup (mappendSym (symbol ("GHC.Num." :: String)) sym) bops + = EBin op e1 e2 + makeApp def lmap f es = eAppWithMap lmap f es def -- where msg = "makeApp f = " ++ show f ++ " es = " ++ show es ++ " def = " ++ show def @@ -478,7 +490,7 @@ splitArgs e = (f, reverse es) (f, es) = go e go (C.App (C.Var i) e) | ignoreVar i = go e - go (C.App f (C.Var v)) | isErasable v = go f + go (C.App f (C.Var v)) | GM.isEmbeddedDictVar v = go f go (C.App f e) = (f', e:es) where (f', es) = go f go f = (f, []) @@ -536,19 +548,19 @@ isBangInteger [(C.DataAlt s, _, _), (C.DataAlt jp,_,_), (C.DataAlt jn,_,_)] && symbol jn == "GHC.Integer.Type.Jn#" isBangInteger _ = False -isErasable :: Id -> Bool -isErasable v = F.notracepp msg $ isGhcSplId v && not (isDCId v) - where - msg = "isErasable: " ++ GM.showPpr (v, Var.idDetails v) +-- isErasable :: Id -> Bool +-- isErasable v = F.tracepp msg $ False -- isGhcSplId v && not (isDCId v) +-- where +-- msg = "isErasable: " ++ GM.showPpr (v, Var.idDetails v) -isGhcSplId :: Id -> Bool -isGhcSplId v = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v) +-- isGhcSplId :: Id -> Bool +-- isGhcSplId v = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v) -isDCId :: Id -> Bool -isDCId v = case Var.idDetails v of - DataConWorkId _ -> True - DataConWrapId _ -> True - _ -> False +-- isDCId :: Id -> Bool +-- isDCId v = case Var.idDetails v of +-- DataConWorkId _ -> True +-- DataConWrapId _ -> True +-- _ -> False isANF :: Id -> Bool isANF v = isPrefixOfSym (symbol ("lq_anf" :: String)) (simpleSymbolVar v) @@ -573,7 +585,7 @@ instance Simplify C.CoreExpr where = e simplify (C.App e (C.Type _)) = simplify e - simplify (C.App e (C.Var dict)) | isErasable dict + simplify (C.App e (C.Var dict)) | GM.isEmbeddedDictVar dict = simplify e simplify (C.App (C.Lam x e) _) | isDead x = simplify e @@ -581,13 +593,13 @@ instance Simplify C.CoreExpr where = C.App (simplify e1) (simplify e2) simplify (C.Lam x e) | isTyVar x = simplify e - simplify (C.Lam x e) | isErasable x + simplify (C.Lam x e) | GM.isEmbeddedDictVar x = simplify e simplify (C.Lam x e) = C.Lam x (simplify e) - simplify (C.Let (C.NonRec x _) e) | isErasable x + simplify (C.Let (C.NonRec x _) e) | GM.isEmbeddedDictVar x = simplify e - simplify (C.Let (C.Rec xes) e) | all (isErasable . fst) xes + simplify (C.Let (C.Rec xes) e) | all (GM.isEmbeddedDictVar . fst) xes = simplify e simplify (C.Let xes e) = C.Let (simplify xes) (simplify e) @@ -639,6 +651,6 @@ instance Simplify C.CoreBind where instance Simplify C.CoreAlt where simplify (c, xs, e) = (c, xs, simplify e) - -- where xs = F.tracepp _msg xs0 + -- where xs = F.notracepp _msg xs0 -- _msg = "isCoVars? " ++ F.showpp [(x, isCoVar x, varType x) | x <- xs0] inline p (c, xs, e) = (c, xs, inline p e) diff --git a/src/Language/Haskell/Liquid/Transforms/InlineAux.hs b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs new file mode 100644 index 0000000000..aae91717be --- /dev/null +++ b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs @@ -0,0 +1,177 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Language.Haskell.Liquid.Transforms.InlineAux + ( inlineAux + , inlineDFun + ) +where + +import CoreSyn +import DynFlags +import qualified Outputable as O +import MkCore +import Control.Arrow ( second ) +import OccurAnal ( occurAnalysePgm ) +import qualified Language.Haskell.Liquid.GHC.Misc + as GM +import Class ( classAllSelIds ) +import Id +import CoreFVs ( exprFreeVarsList ) +import InstEnv +import TcType ( tcSplitDFunTy ) +import GhcPlugins ( isDFunId + , exprType + , OccName + , Module + , occNameString + , getOccName + , mkCoreApps + , isDictId + ) +import qualified Data.HashMap.Strict as M +import CoreSubst +import GHC ( isDictonaryId ) +import SimplMonad +import SimplCore +import Control.Monad.State +import Data.Functor.Foldable + +buildDictSubst :: CoreProgram -> M.HashMap Id CoreExpr +buildDictSubst = cata f + where + f Nil = M.empty + f (Cons b s) | NonRec x e <- b, isDFunId x || isDictonaryId x = M.insert x e s + | otherwise = s + + +inlineAux :: Module -> CoreProgram -> CoreProgram +inlineAux m cbs = -- inlineDFun + -- $ + occurAnalysePgm m (const False) (const False) [] (map f cbs) + where + f :: CoreBind -> CoreBind + f all@(NonRec x e) + | Just (dfunId, methodToAux) <- M.lookup x auxToMethodToAux = NonRec + x + (inlineAuxExpr dfunId methodToAux e) + | otherwise = all + f (Rec bs) = Rec (fmap g bs) + where + g all@(x, e) + | Just (dfunId, methodToAux) <- M.lookup x auxToMethodToAux + = (x, inlineAuxExpr dfunId methodToAux e) + | otherwise + = all + auxToMethodToAux = mconcat $ fmap (uncurry dfunIdSubst) (grepDFunIds cbs) + + +inlineDFun :: DynFlags -> CoreProgram -> IO CoreProgram +inlineDFun df cbs = pure cbs-- mapM go cbs + -- where + -- go orig@(NonRec x e) | isDFunId x = do + -- -- e''' <- simplifyExpr df e'' + -- let newBody = mkCoreApps (GM.tracePpr ("substituted type:" ++ GM.showPpr (exprType (mkCoreApps e' binders))) e') (fmap Var binders) + -- bind = NonRec (mkWildValBinder (exprType newBody)) newBody + -- pure $ NonRec x (mkLet bind e) + -- | otherwise = pure orig + -- where + -- -- wcBinder = mkWildValBinder t + -- (binders, _) = GM.tracePpr "collectBinders"$ collectBinders e + -- e' = substExprAll O.empty subst e + -- go recs = pure recs + -- subst = buildDictSubst cbs + + + +lookupIdSubstAll :: O.SDoc -> M.HashMap Id CoreExpr -> Id -> CoreExpr +lookupIdSubstAll doc env v | Just e <- M.lookup v env = e + | otherwise = Var v + -- Vital! See Note [Extending the Subst] + -- | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v + -- $$ ppr in_scope) + +substExprAll :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr +substExprAll doc subst orig_expr = subst_expr_all doc subst orig_expr + + +subst_expr_all :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr +subst_expr_all doc subst expr = go expr + where + go (Var v) = lookupIdSubstAll (doc O.$$ O.text "subst_expr_all") subst v + go (Type ty ) = Type ty + go (Coercion co ) = Coercion co + go (Lit lit ) = Lit lit + go (App fun arg ) = App (go fun) (go arg) + go (Tick tickish e ) = Tick tickish (go e) + go (Cast e co ) = Cast (go e) co + -- Do not optimise even identity coercions + -- Reason: substitution applies to the LHS of RULES, and + -- if you "optimise" an identity coercion, you may + -- lose a binder. We optimise the LHS of rules at + -- construction time + + go (Lam bndr body) = Lam bndr (subst_expr_all doc subst body) + + go (Let bind body) = Let (mapBnd go bind) (subst_expr_all doc subst body) + + go (Case scrut bndr ty alts) = + Case (go scrut) bndr ty (map (go_alt subst) alts) + + go_alt subst (con, bndrs, rhs) = (con, bndrs, subst_expr_all doc subst rhs) + + + +-- grab the dictionaries +grepDFunIds :: CoreProgram -> [(DFunId, CoreExpr)] +grepDFunIds = filter (isDFunId . fst) . flattenBinds + +isClassOpAuxOccName :: OccName -> Bool +isClassOpAuxOccName occ = case occNameString occ of + '$' : 'c' : _ -> True + _ -> False + +isClassOpAuxOf :: Id -> Id -> Bool +isClassOpAuxOf aux method = case occNameString $ getOccName aux of + '$' : 'c' : rest -> rest == occNameString (getOccName method) + _ -> False + +dfunIdSubst :: DFunId -> CoreExpr -> M.HashMap Id (Id, M.HashMap Id Id) +dfunIdSubst dfunId e = M.fromList $ zip auxIds (repeat (dfunId, methodToAux)) + where + methodToAux = M.fromList + [ (m, aux) | m <- methods, aux <- auxIds, aux `isClassOpAuxOf` m ] + (_, _, cls, _) = tcSplitDFunTy (idType dfunId) + auxIds = filter (isClassOpAuxOccName . getOccName) (exprFreeVarsList e) + methods = classAllSelIds cls + +inlineAuxExpr :: DFunId -> M.HashMap Id Id -> CoreExpr -> CoreExpr +inlineAuxExpr dfunId methodToAux e = go e + where + go :: CoreExpr -> CoreExpr + go (Lam b body) = Lam b (go body) + go (Let b body) + | NonRec x e <- b, isDictId x = go + $ substExpr O.empty (extendIdSubst emptySubst x e) body + | otherwise = Let (mapBnd go b) (go body) + go (Case e x t alts) = Case (go e) x t (fmap (mapAlt go) alts) + go (Cast e c ) = Cast (go e) c + go (Tick t e ) = Tick t (go e) + go e + | (Var m, args) <- collectArgs e + , Just aux <- M.lookup m methodToAux + , arg : argsNoTy <- dropWhile isTypeArg args + , (Var x, argargs) <- collectArgs arg + , x == dfunId + = GM.notracePpr ("inlining in" ++ GM.showPpr e) + $ mkCoreApps (Var aux) (argargs ++ (go <$> argsNoTy)) + go (App e0 e1) = App (go e0) (go e1) + go e = e + + +-- modified from Rec.hs +mapBnd :: (Expr b -> Expr b) -> Bind b -> Bind b +mapBnd f (NonRec b e) = NonRec b (f e) +mapBnd f (Rec bs ) = Rec (map (second f) bs) + +mapAlt :: (Expr b -> Expr b) -> (t, t1, Expr b) -> (t, t1, Expr b) +mapAlt f (d, bs, e) = (d, bs, f e) diff --git a/src/Language/Haskell/Liquid/Transforms/Rewrite.hs b/src/Language/Haskell/Liquid/Transforms/Rewrite.hs index 3fbde1964b..242494b19a 100644 --- a/src/Language/Haskell/Liquid/Transforms/Rewrite.hs +++ b/src/Language/Haskell/Liquid/Transforms/Rewrite.hs @@ -436,7 +436,7 @@ isVarTup xs e isVarTup _ _ = Nothing eqVars :: [Var] -> [Var] -> Bool -eqVars xs ys = {- F.tracepp ("eqVars: " ++ show xs' ++ show ys') -} xs' == ys' +eqVars xs ys = {- F.notracepp ("eqVars: " ++ show xs' ++ show ys') -} xs' == ys' where xs' = {- F.symbol -} show <$> xs ys' = {- F.symbol -} show <$> ys diff --git a/src/Language/Haskell/Liquid/Types/Fresh.hs b/src/Language/Haskell/Liquid/Types/Fresh.hs index a28a2b1dd3..622773282d 100644 --- a/src/Language/Haskell/Liquid/Types/Fresh.hs +++ b/src/Language/Haskell/Liquid/Types/Fresh.hs @@ -91,7 +91,7 @@ trueRefType (RImpF _ t t' _) trueRefType (RFun _ t t' _) = rFun <$> fresh <*> true t <*> true t' -trueRefType (RApp c ts _ _) | isClass c +trueRefType (RApp c ts _ _) | isEmbeddedDict c = rRCls c <$> mapM true ts trueRefType (RApp c ts rs r) @@ -144,7 +144,7 @@ refreshRefType (RFun b t t' _) | b == F.dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t' | otherwise = rFun b <$> refresh t <*> refresh t' -refreshRefType (RApp rc ts _ _) | isClass rc +refreshRefType (RApp rc ts _ _) | isEmbeddedDict rc = return $ rRCls rc ts refreshRefType (RApp rc ts rs r) diff --git a/src/Language/Haskell/Liquid/Types/PredType.hs b/src/Language/Haskell/Liquid/Types/PredType.hs index d90c5a034c..4ae4ae68fb 100644 --- a/src/Language/Haskell/Liquid/Types/PredType.hs +++ b/src/Language/Haskell/Liquid/Types/PredType.hs @@ -40,6 +40,7 @@ import Var import Language.Haskell.Liquid.GHC.TypeRep import Data.Hashable import qualified Data.HashMap.Strict as M +import qualified Data.HashSet as S import qualified Data.Maybe as Mb import qualified Data.List as L -- (foldl', partition) -- import Data.List (nub) @@ -107,9 +108,9 @@ dcWorkSpecType c wrT = fromRTypeRep (meetWorkWrapRep c wkR wrR) dataConWorkRep :: DataCon -> SpecRep dataConWorkRep c = toRTypeRep - -- . F.tracepp ("DCWR-2: " ++ F.showpp c) + -- . F.notracepp ("DCWR-2: " ++ F.showpp c) . ofType - -- . F.tracepp ("DCWR-1: " ++ F.showpp c) + -- . F.notracepp ("DCWR-1: " ++ F.showpp c) . dataConRepType -- . Var.varType -- . dataConWorkId @@ -126,7 +127,7 @@ dataConWorkRep dc = RTypeRep , ty_res = t' } where - (ts', t') = F.tracepp "DCWR-1" (ofType <$> ts, ofType t) + (ts', t') = F.notracepp "DCWR-1" (ofType <$> ts, ofType t) as = makeRTVar . rTyVar <$> αs tArg (αs,_,eqs,th,ts,t) = dataConFullSig dc @@ -158,7 +159,7 @@ meetWorkWrapRep c workR wrapR | otherwise = panic (Just (getSrcSpan c)) errMsg where - pad = {- F.tracepp ("MEETWKRAP: " ++ show (ty_vars workR)) $ -} workN - wrapN + pad = {- F.notracepp ("MEETWKRAP: " ++ show (ty_vars workR)) $ -} workN - wrapN (xs, _) = splitAt pad (ty_binds workR) (ts, ts') = splitAt pad (ty_args workR) workN = length (ty_args workR) @@ -170,15 +171,24 @@ strengthenRType wkT wrT = maybe wkT (strengthen wkT) (stripRTypeBase wrT) dcWrapSpecType :: DataCon -> DataConP -> SpecType dcWrapSpecType dc (DataConP _ _ vs ps cs yts rt _ _ _) - = {- F.tracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ -} + = F.notracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ mkArrow makeVars' ps [] ts' rt' where + isCls = Ghc.isClassTyCon $ Ghc.dataConTyCon dc (xs, ts) = unzip (reverse yts) mkDSym z = (F.symbol z) `F.suffixSymbol` (F.symbol dc) ys = mkDSym <$> xs tx _ [] [] [] = [] - tx su (x:xs) (y:ys) (t:ts) = (y, F.subst (F.mkSubst su) t, mempty) - : tx ((x, F.EVar y):su) xs ys ts + -- NOTE THAT xs and xs' have the same type!!! + -- I renamed them to avoid shadowing but if you modify this + -- code keep that in mind + tx su (x:xs') (y:ys) (t:ts) = ( y + -- special case for class + , if isCls + then t + else F.subst (F.mkSubst su) t + , mempty) + : tx ((x, F.EVar y):su) xs' ys ts tx _ _ _ _ = panic Nothing "PredType.dataConPSpecType.tx called on invalid inputs" yts' = tx [] xs ys ts ts' = map ("" , , mempty) cs ++ yts' diff --git a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs index 714d8ea1af..6c22e2c942 100644 --- a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs +++ b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs @@ -324,19 +324,19 @@ brkFun out = ([], out) ppr_forall :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc ppr_forall bb p t = maybeParen p funPrec $ sep [ ppr_foralls (ppPs bb) (fst <$> ty_vars trep) (ty_preds trep) - , ppr_clss cls + -- , ppr_clss [] , ppr_rtype bb topPrec t' ] where trep = toRTypeRep t - (cls, t') = bkClass $ fromRTypeRep $ trep {ty_vars = [], ty_preds = []} + (_,_, t') = bkUniv $ fromRTypeRep $ trep {ty_vars = [], ty_preds = []} ppr_foralls False _ _ = empty ppr_foralls _ [] [] = empty ppr_foralls True αs πs = text "forall" <+> dαs αs <+> dπs (ppPs bb) πs <-> dot - ppr_clss [] = empty - ppr_clss cs = (parens $ hsep $ punctuate comma (uncurry (ppr_cls bb p) <$> cs)) <+> text "=>" + -- ppr_clss [] = empty + -- ppr_clss cs = (parens $ hsep $ punctuate comma (uncurry (ppr_cls bb p) <$> cs)) <+> text "=>" dαs αs = ppr_rtvar_def αs diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs index 30c979dfc6..a603a612ab 100644 --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -150,7 +150,7 @@ dataConArgs trep = unzip [ (x, t) | (x, t) <- zip xs ts, isValTy t] where xs = ty_binds trep ts = ty_args trep - isValTy = not . GM.isPredType . toType + isValTy = not . GM.isEmbeddedDictType . toType pdVar :: PVar t -> Predicate @@ -890,7 +890,7 @@ famInstArgs c = case Ghc.tyConFamInst_maybe c of cArity = Ghc.tyConArity c -- TODO:faminst-preds: case Ghc.tyConFamInst_maybe c of --- TODO:faminst-preds: Just (c', ts) -> F.tracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts)) +-- TODO:faminst-preds: Just (c', ts) -> F.notracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts)) -- TODO:faminst-preds: $ Just (famInstType (Ghc.tyConArity c) c' ts) -- TODO:faminst-preds: Nothing -> Nothing @@ -1260,7 +1260,7 @@ instance SubsTy Symbol Symbol (BRType r) where subt su (RAppTy t1 t2 r) = RAppTy (subt su t1) (subt su t2) r subt su (RRTy e r o t) = RRTy [(x, subt su p) | (x,p) <- e] r o (subt su t) subt _ (RHole r) = RHole r - + instance SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) where subt su (RProp e t) = RProp [(x, subt su xt) | (x,xt) <- e] (subt su t) @@ -1684,7 +1684,7 @@ grabArgs τs τ = reverse (τ:τs) isNonValueTy :: Type -> Bool -isNonValueTy t = {- Ghc.isPredTy -} isClassPred t || isEqPred t +isNonValueTy t = GM.isEmbeddedDictType t expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs index 32f61ec947..98937327b0 100644 --- a/src/Language/Haskell/Liquid/Types/Types.hs +++ b/src/Language/Haskell/Liquid/Types/Types.hs @@ -52,7 +52,7 @@ module Language.Haskell.Liquid.Types.Types ( , rTyConPVs , rTyConPropVs -- , isClassRTyCon - , isClassType, isEqType, isRVar, isBool + , isClassType, isEqType, isRVar, isBool, isEmbeddedClass -- * Refinement Types , RType (..), Ref(..), RTProp, rPropP @@ -616,6 +616,11 @@ isClassType :: TyConable c => RType c t t1 -> Bool isClassType (RApp c _ _ _) = isClass c isClassType _ = False +isEmbeddedClass :: TyConable c => RType c t t1 -> Bool +isEmbeddedClass (RApp c _ _ _) = isEmbeddedDict c +isEmbeddedClass _ = False + + -- rTyConPVHPs = filter isHPropPV . rtc_pvars -- isHPropPV = not . isPropPV @@ -714,7 +719,7 @@ data RType c tv r | RAllE { rt_bind :: !Symbol , rt_allarg :: !(RType c tv r) - , rt_ty :: !(RType c tv r) + , rt_ty :: !(RType c tv r) -- bind goes here } | REx { @@ -733,9 +738,9 @@ data RType c tv r | RRTy { rt_env :: ![(Symbol, RType c tv r)] - , rt_ref :: !r + , rt_ref :: !r -- depends on env , rt_obl :: !Oblig - , rt_ty :: !(RType c tv r) + , rt_ty :: !(RType c tv r) -- does not depend on env } | RHole r -- ^ let LH match against the Haskell type and add k-vars, e.g. `x:_` @@ -896,15 +901,20 @@ class (Eq c) => TyConable c where isTuple :: c -> Bool ppTycon :: c -> Doc isClass :: c -> Bool + isEmbeddedDict :: c -> Bool isEqual :: c -> Bool isNumCls :: c -> Bool isFracCls :: c -> Bool + isOrdCls :: c -> Bool + isEqCls :: c -> Bool - isClass = const False - isEqual = const False - isNumCls = const False - isFracCls = const False + isClass = const False + isEmbeddedDict c = isNumCls c || isEqual c || isOrdCls c || isEqCls c + isEqual = const False + isNumCls = const False + isFracCls = const False + isOrdCls = const False -- Should just make this a @Pretty@ instance but its too damn tedious @@ -929,10 +939,13 @@ instance TyConable RTyCon where isEqual = isEqual . rtc_tc ppTycon = F.toFix - isNumCls c = maybe False (isClassOrSubClass isNumericClass) + isNumCls c = maybe False isNumericClass + (tyConClass_maybe $ rtc_tc c) + isFracCls c = maybe False isFractionalClass (tyConClass_maybe $ rtc_tc c) - isFracCls c = maybe False (isClassOrSubClass isFractionalClass) + isOrdCls c = maybe False isOrdClass (tyConClass_maybe $ rtc_tc c) + isEqCls c = isEqCls (rtc_tc c) instance TyConable TyCon where @@ -943,10 +956,13 @@ instance TyConable TyCon where isEqual c = c == eqPrimTyCon || c == eqReprPrimTyCon ppTycon = text . showPpr - isNumCls c = maybe False (isClassOrSubClass isNumericClass) - (tyConClass_maybe $ c) - isFracCls c = maybe False (isClassOrSubClass isFractionalClass) - (tyConClass_maybe $ c) + isNumCls c = maybe False isNumericClass + (tyConClass_maybe c) + isFracCls c = maybe False isFractionalClass + (tyConClass_maybe c) + isOrdCls c = maybe False isOrdClass + (tyConClass_maybe c) + isEqCls c = isPrelEqTyCon c isClassOrSubClass :: (Class -> Bool) -> Class -> Bool @@ -1665,7 +1681,7 @@ efoldReft logicBind cb dty g f fp = go go γ z (RAllP p t) = go (fp p γ) z t go γ z (RImpF x t t' r) = go γ z (RFun x t t' r) go γ z me@(RFun _ (RApp c ts _ _) t' r) - | isClass c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') + | isEmbeddedDict c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') go γ z me@(RFun x t t' r) | logicBind x t = f γ (Just me) r (go γ' (go γ z t) t') | otherwise = f γ (Just me) r (go γ (go γ z t) t') diff --git a/src/Language/Haskell/Liquid/UX/CTags.hs b/src/Language/Haskell/Liquid/UX/CTags.hs index e267679fab..40c52c5172 100644 --- a/src/Language/Haskell/Liquid/UX/CTags.hs +++ b/src/Language/Haskell/Liquid/UX/CTags.hs @@ -48,7 +48,7 @@ memTagEnv :: TagKey -> TagEnv -> Bool memTagEnv = M.member makeTagEnv :: [CoreBind] -> TagEnv -makeTagEnv = {- tracepp "TAGENV" . -} M.map (:[]) . callGraphRanks . makeCallGraph +makeTagEnv = {- notracepp "TAGENV" . -} M.map (:[]) . callGraphRanks . makeCallGraph -- makeTagEnv = M.fromList . (`zip` (map (:[]) [1..])). L.sort . map fst . concatMap bindEqns diff --git a/tests/refined-classes/SemigroupOp.hs b/tests/refined-classes/SemigroupOp.hs new file mode 100644 index 0000000000..a47b1302fe --- /dev/null +++ b/tests/refined-classes/SemigroupOp.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE RankNTypes #-} +{-@ LIQUID "--reflection" @-} +{-@ LIQUID "--ple" @-} +module SemigroupOp where +import ProofCombinators + +class MySemigroup a where + ymappend :: a -> a -> a + {-@ lawAssociative :: v:a -> v':a -> v'':a -> {ymappend (ymappend v v') v'' == ymappend v (ymappend v' v'')} @-} + lawAssociative :: a -> a -> a -> () + +class (MySemigroup a) => MyMonoid a where + ymempty :: a + {-@ lawEmpty :: x:a -> {ymappend x ymempty == x && ymappend ymempty x == x} @-} + lawEmpty :: a -> () + + +data PNat = Z | S PNat + +instance MyMonoid PNat where + ymempty = Z + lawEmpty Z = () + lawEmpty (S m) = lawEmpty m + + +k :: a -> b -> b +k _ y = y + + +-- does not typecheck +{-@ assocMonoid :: MyMonoid a => a:a -> b:a -> c:a -> {ymappend a (ymappend b c) == ymappend (ymappend a b) c} @-} +assocMonoid :: MyMonoid a => a -> a -> a -> () +assocMonoid a b c = lawAssociative a b c + +instance MySemigroup PNat where + ymappend Z n = n + ymappend (S m) n = S (ymappend m n) + lawAssociative Z m n = ymappend Z (ymappend m n) `k` + ymappend m n `k` + ymappend (ymappend Z m) n `k` + () + lawAssociative (S p) m n = ymappend (S p) (ymappend m n) `k` + S (ymappend p (ymappend m n)) `k` + lawAssociative p m n `k` + S (ymappend (ymappend p m) n) `k` + ymappend (S (ymappend p m) ) n `k` + ymappend (ymappend (S p) m ) n `k` + () + +data MyList a = + MyNil + | MyCons a (MyList a) + + +instance MySemigroup (MyList a) where + ymappend MyNil t = t + ymappend (MyCons v l) t = MyCons v (ymappend l t) + + -- lawAssociativity x y z = assume (mymappend x (mymappend y z) == mymappend (mymappend x y) z) + lawAssociative MyNil _ _ = () + lawAssociative (MyCons x xs) y z = lawAssociative xs y z + +data Op a = Op a + + +instance (MySemigroup a) => MySemigroup (Op a) where + ymappend (Op x) (Op y) = Op (ymappend y x) + lawAssociative (Op x) (Op y) (Op z) = lawAssociative z y x `cast` () + diff --git a/tests/refined-classes/Subclass.hs b/tests/refined-classes/Subclass.hs new file mode 100644 index 0000000000..3947816af1 --- /dev/null +++ b/tests/refined-classes/Subclass.hs @@ -0,0 +1,60 @@ +{-@ LIQUID "--reflection" @-} +{-@ LIQUID "--ple" @-} +module Subclass where + +class MyFunctor f where + {-@ myfmap :: forall a b. (a -> b) -> f a -> f b @-} + myfmap :: (a -> b) -> f a -> f b + (<$) :: a -> f b -> f a + +{-@ reflect myid @-} +myid :: a -> a +myid x = x + +class MyFunctor f => MyApplicative f where + {-@ mypure :: forall a. a -> f a @-} + mypure :: a -> f a + {-@ myap :: forall a b. f (a -> b) -> f a -> f b @-} + myap :: f (a -> b) -> f a -> f b + {-@ myprop :: forall a b. x:f a -> f:(a -> b) -> {myfmap f x == myap (mypure f) x} @-} + myprop :: f a -> (a -> b) -> () + + +{-@ data MyId a = MyId a @-} +data MyId a = MyId a + +instance MyFunctor MyId where + myfmap f (MyId i) = MyId (f i) + x <$ (MyId _) = MyId x + +instance MyApplicative MyId where + mypure = MyId + myap (MyId f) (MyId a) = MyId (f a) + myprop _ _ = () + +data Optional a = None | Has a + +instance MyFunctor Optional where + myfmap _ None = None + myfmap f (Has x) = Has (f x) + _ <$ None = None + x <$ (Has _) = Has x + +instance MyApplicative Optional where + mypure = Has + myap None _ = None + myap _ None = None + myap (Has f) (Has x) = Has (f x) + myprop _ _ = () + +{-@ impl :: x:Bool -> y:Bool -> {v:Bool | v <=> (x => y)} @-} +impl :: Bool -> Bool -> Bool +impl a b = if a then b else True + +{-@ reflect ffmap @-} +ffmap :: MyFunctor f => (a -> b) -> f a -> f b +ffmap = myfmap + +{-@ trivial :: MyFunctor f => f:(a -> b) -> x:f a -> {myfmap f x == ffmap f x} @-} +trivial :: MyFunctor f => (a -> b) -> f a -> () +trivial _ _ = () diff --git a/tests/refined-classes/SubclassMonoidDs.hs b/tests/refined-classes/SubclassMonoidDs.hs new file mode 100644 index 0000000000..1723cb734d --- /dev/null +++ b/tests/refined-classes/SubclassMonoidDs.hs @@ -0,0 +1,35 @@ +{-@ LIQUID "--reflection" @-} +{-@ LIQUID "--ple" @-} +module SemigroupDs where + +import Prelude hiding (Semigroup, mappend) + + + +{-@ data MySemigroup a = CMySemigroup { + mappend :: a -> a -> a, + lawAssociative :: x:a -> y:a -> z:a -> {mappend x (mappend y z) == mappend (mappend x y) z} } @-} + +data MySemigroup a = CMySemigroup{ + mappend :: a -> a -> a, + lawAssociative :: a -> a -> a -> ()} + +{-@ data MyMonoid a = CMyMonoid { + p1MyMonoid :: MySemigroup a, + mempty :: a, + lawEmpty :: x:a -> {mappend p1MyMonoid x mempty == x && mappend p1MyMonoid mempty x == x}} +@-} + +data MyMonoid a = CMyMonoid { + p1MyMonoid :: MySemigroup a, + mempty :: a, + lawEmpty :: a -> () + } + +{-@ monoidAssoc :: dMyMonoid:MyMonoid a -> a:a -> b:a -> c:a -> + {mappend (p1MyMonoid dMyMonoid) (mappend (p1MyMonoid dMyMonoid) a b) c /= + mappend (p1MyMonoid dMyMonoid) a (mappend (p1MyMonoid dMyMonoid) b c)} @-} +monoidAssoc :: MyMonoid a -> a -> a -> a -> () +monoidAssoc dMyMonoid = + let dMySemigroup = p1MyMonoid dMyMonoid in + \a b c -> lawAssociative dMySemigroup a b c