diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal index b784c3e1f7..0378502d82 100644 --- a/liquidhaskell-boot/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot/liquidhaskell-boot.cabal @@ -41,7 +41,6 @@ library Language.Haskell.Liquid.Bare.ToBare Language.Haskell.Liquid.Bare.Types Language.Haskell.Liquid.Bare.Typeclass - Language.Haskell.Liquid.Bare.Elaborate Language.Haskell.Liquid.CSS Language.Haskell.Liquid.Constraint.Constraint Language.Haskell.Liquid.Constraint.Env diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index a0b001487a..2069c376e5 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -56,7 +56,6 @@ 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.DataType as Bare -import Language.Haskell.Liquid.Bare.Elaborate import qualified Language.Haskell.Liquid.Bare.Expand as Bare import qualified Language.Haskell.Liquid.Bare.Measure as Bare import qualified Language.Haskell.Liquid.Bare.Plugged as Bare @@ -262,7 +261,7 @@ makeGhcSpec0 -> Ghc.TcRn (Diagnostics, GhcSpec) makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySpecs = do -- build up environments - tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier + tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) let tyi = Bare.tcTyConMap tycEnv let sigEnv = makeSigEnv embs tyi (_gsExports src) rtEnv let lSpec1 = makeLiftedSpec1 cfg src tycEnv lmap mySpec1 @@ -274,7 +273,7 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp let (dg1, measEnv0) = withDiagnostics $ makeMeasEnv env tycEnv sigEnv specs let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src) elaboratedSig <- - if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods + if allowTC then Bare.makeClassAuxTypes datacons instMethods >>= elaborateSig sig else pure sig let (dg3, refl) = withDiagnostics $ makeSpecRefl cfg src specs env name elaboratedSig tycEnv @@ -333,23 +332,8 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp }) where -- typeclass elaboration - - coreToLg ce = - case CoreToLogic.runToLogic - embs - lmap - dm - (\x -> todo Nothing ("coreToLogic not working " ++ x)) - (CoreToLogic.coreToLogic allowTC ce) of - Left msg -> panic Nothing (F.showpp msg) - Right e -> e elaborateSig si auxsig = do - tySigs <- - forM (gsTySigs si) $ \(x, t) -> - if GM.isFromGHCReal x then - pure (x, t) - else do t' <- traverse (elaborateSpecType coreToLg simplifier) t - pure (x, t') + let tySigs = gsTySigs si -- things like len breaks the code -- asmsigs should be elaborated only if they are from the current module -- asmSigs <- forM (gsAsmSigs si) $ \(x, t) -> do @@ -359,8 +343,6 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp si { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig } - simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr - simplifier = pure -- no simplification allowTC = typeclass cfg mySpec2 = Bare.qualifyExpand env name rtEnv l [] mySpec1 where l = F.dummyPos "expand-mySpec2" iSpecs2 = Bare.qualifyExpand @@ -378,7 +360,6 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp mySpec1 = mySpec0 <> lSpec0 lSpec0 = makeLiftedSpec0 cfg src embs lmap mySpec0 embs = makeEmbeds src env (mySpec0 : map snd dependencySpecs) - dm = Bare.tcDataConMap tycEnv0 (dg0, datacons, tycEnv0) = makeTycEnv0 cfg name env embs mySpec2 iSpecs2 env = Bare.makeEnv cfg session tcg instEnvs localVars src lmap ((name, targetSpec) : dependencySpecs) -- check barespecs @@ -1228,12 +1209,10 @@ makeTycEnv1 :: ModName -> Bare.Env -> (Bare.TycEnv, [Located DataConP]) - -> (Ghc.CoreExpr -> F.Expr) - -> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr) -> Ghc.TcRn Bare.TycEnv -makeTycEnv1 myName env (tycEnv, datacons) coreToLg simplifier = do +makeTycEnv1 myName env (tycEnv, datacons) = do -- fst for selector generation, snd for dataconsig generation - lclassdcs <- forM classdcs $ traverse (Bare.elaborateClassDcp coreToLg simplifier) + lclassdcs <- forM classdcs $ traverse Bare.elaborateClassDcp 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 )} diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs deleted file mode 100644 index 5fdb11e613..0000000000 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs +++ /dev/null @@ -1,710 +0,0 @@ -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE ExplicitForAll #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} - -{-# OPTIONS_GHC -Wno-orphans #-} - --- | This module uses GHC API to elaborate the resolves expressions - --- TODO: Genearlize to BareType and replace the existing resolution mechanisms - -module Language.Haskell.Liquid.Bare.Elaborate - ( fixExprToHsExpr - , elaborateSpecType - -- , buildSimplifier - ) -where - -import qualified Language.Fixpoint.Types as F --- import Control.Arrow -import Liquid.GHC.API hiding (panic, varName) -import qualified Language.Haskell.Liquid.GHC.Misc - as GM -import Language.Haskell.Liquid.Types.Errors -import Language.Haskell.Liquid.Types.RType -import Language.Haskell.Liquid.Types.RTypeOp -import Language.Haskell.Liquid.Types.RefType - ( ofType ) -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.Char ( isUpper ) -import GHC.Types.Name.Occurrence -import qualified Liquid.GHC.API as Ghc - (noExtField) -import qualified Data.Maybe as Mb - --- TODO: make elaboration monadic so typeclass names are unified to something --- that is generated in advance. This can greatly simplify the implementation --- of elaboration - --- the substitution code is meant to inline dictionary functions --- but does not seem to work --- 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 -> TcRn 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_rinfo :: !RFInfo - , _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 () - -project :: SpecType -> SpecTypeF SpecType -project (RVar var reft ) = RVarF var reft -project (RFun bind i tin tout reft) = RFunF bind i 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 - -embed :: SpecTypeF SpecType -> SpecType -embed (RVarF var reft ) = RVar var reft -embed (RFunF bind i tin tout reft) = RFun bind i 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 = cata (fmap wrap) - where - cata g = g . fmap (cata g) . project - -plugType :: SpecType -> PartialSpecType -> SpecType -plugType t = ana $ \case - Pure _ -> specTypeToPartial t - Free res -> res - where - ana g = embed . fmap (ana g) . g - --- 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 - --- | returns (lambda binders, forall binders) -collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol]) -collectSpecTypeBinders = \case - RFun bind _ tin tout _ - | isClassType tin -> collectSpecTypeBinders tout - | otherwise -> let (bs, abs') = collectSpecTypeBinders tout - in (bind : bs, abs') - RAllE b _ t -> - let (bs, abs') = collectSpecTypeBinders t - in (b : bs, abs') - RAllT (RTVar (RTV ab) _) t _ -> - let (bs, abs') = collectSpecTypeBinders t - in (bs, F.symbol ab : abs') - REx b _ t -> - let (bs, abs') = collectSpecTypeBinders t - in (b : bs, abs') - RAppTy _ t _ -> collectSpecTypeBinders t - RRTy _ _ _ t -> collectSpecTypeBinders t - _ -> ([], []) - --- 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 result = go - where - go = \case - RFun bind _ tin tout _ - | isClassType tin -> go tout - | otherwise -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] (go tout) - RAllE _ _ t -> go t - RAllT _ t _ -> go t - REx _ _ t -> go t - RAppTy _ t _ -> go t - RRTy _ _ _ t -> go t - _ -> result - - -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 -> TcRn CoreExpr) - -> SpecType - -> TcRn SpecType -elaborateSpecType coreToLogic simplifier t = GM.withWiredIn $ 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 -> TcRn CoreExpr) - -> SpecType - -> TcRn (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 i 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 i (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 i eTin eToutRenamed ureft - , canonicalBinders - ) - | otherwise = do - let (eToutRenamed, canonicalBinders) = - canonicalizeDictBinder bs (eTout, bs') - pure - ( F.notracepp "RFunTrivial1" $ RFun bind i 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 i - 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 i - 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') - -- ) - - -- 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 -> do - args' <- mapM - (fmap fst . elaborateSpecType' partialTp coreToLogic simplify) - args - 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 [] defaultTyConInfo) [] [] mempty :: SpecType - elaborateReft - :: (F.PPrint a) - => (F.Reft, SpecType) - -> TcRn a - -> ([F.Symbol] -> F.Expr -> TcRn a) - -> TcRn a - elaborateReft (reft@(F.Reft (vv, e)), vvTy) trivial nonTrivialCont = - if isTrivial' reft - then trivial - else do - let - querySpecType = - plugType (rFun' (classRFInfo True) vv vvTy boolType) partialTp :: SpecType - - (origBinders, origTyBinders) = F.notracepp "collectSpecTypeBinders" - $ collectSpecTypeBinders querySpecType - - - - hsExpr = - buildHsExpr (fixExprToHsExpr (S.fromList origBinders) e) - querySpecType :: LHsExpr GhcPs - exprWithTySigs = noLocA $ ExprWithTySig - noAnn - hsExpr - (hsTypeToHsSigWcType (specTypeToLHsType querySpecType)) - eeWithLamsCore <- GM.elabRnExpr exprWithTySigs - eeWithLamsCore' <- simplify eeWithLamsCore - let - (_, tyBinders) = - collectSpecTypeBinders - . ofType - . exprType - $ eeWithLamsCore' - substTy' = zip tyBinders origTyBinders - eeWithLams = - coreToLogic (GM.notracePpr "eeWithLamsCore" eeWithLamsCore') - (bs', ee) = F.notracepp "grabLams" $ grabLams ([], eeWithLams) - (dictbs, nondictbs) = - L.partition (F.isPrefixOfSym "$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 - ( renameBinderCoerc (\x -> Mb.fromMaybe x (L.lookup x substTy')) - . F.substa (\x -> Mb.fromMaybe x (L.lookup x subst)) - $ F.notracepp - ( "elaborated: subst " - ++ F.showpp substTy' - ++ " " - ++ F.showpp - (ofType $ exprType eeWithLamsCore' :: SpecType) - ) - 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) - -renameBinderCoerc :: (F.Symbol -> F.Symbol) -> F.Expr -> F.Expr -renameBinderCoerc f = rename - where - renameSort = renameBinderSort f - rename e'@(F.ESym _ ) = e' - rename e'@(F.ECon _ ) = e' - rename e'@(F.EVar _ ) = e' - rename ( F.EApp e0 e1 ) = F.EApp (rename e0) (rename e1) - rename ( F.ENeg e0 ) = F.ENeg (rename e0) - rename ( F.EBin bop e0 e1 ) = F.EBin bop (rename e0) (rename e1) - rename ( F.EIte e0 e1 e2 ) = F.EIte (rename e0) (rename e1) (rename e2) - rename ( F.ECst e' t ) = F.ECst (rename e') (renameSort t) - -- rename (F.ELam (x, t) e') = F.ELam (x, renameSort t) (rename e') - rename ( F.PAnd es ) = F.PAnd (rename <$> es) - rename ( F.POr es ) = F.POr (rename <$> es) - rename ( F.PNot e' ) = F.PNot (rename e') - rename ( F.PImp e0 e1 ) = F.PImp (rename e0) (rename e1) - rename ( F.PIff e0 e1 ) = F.PIff (rename e0) (rename e1) - rename ( F.PAtom brel e0 e1) = F.PAtom brel (rename e0) (rename e1) - rename (F.ECoerc _ _ e') = rename e' - - rename e = panic - Nothing - ("renameBinderCoerc: Not sure how to handle the expression " ++ F.showpp e) - - - -renameBinderSort :: (F.Symbol -> F.Symbol) -> F.Sort -> F.Sort -renameBinderSort f = rename - where - rename F.FInt = F.FInt - rename F.FReal = F.FReal - rename F.FNum = F.FNum - rename F.FFrac = F.FFrac - rename ( F.FObj s ) = F.FObj (f s) - rename t'@(F.FVar _ ) = t' - rename ( F.FFunc t0 t1) = F.FFunc (rename t0) (rename t1) - rename ( F.FAbs x t') = F.FAbs x (rename t') - rename t'@(F.FTC _ ) = t' - rename ( F.FApp t0 t1 ) = F.FApp (rename t0) (rename t1) - - --- | 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 _ (F.ECon c) = constantToHsExpr c -fixExprToHsExpr env (F.EVar x) - | x == "GHC.Types.[]" = GM.notracePpr "Empty" $ nlHsVar (mkVarUnqual (mkFastString "[]")) - | x == "GHC.Types.:" = GM.notracePpr "Cons" $ nlHsVar (mkVarUnqual (mkFastString ":")) - | otherwise = GM.notracePpr "Var" $ 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 --- This is currently not doable because how do we know if FInt corresponds to --- Int or Integer? -fixExprToHsExpr env (F.ECst e0 _ ) = fixExprToHsExpr env e0 --- fixExprToHsExpr env (F.PAnd [] ) = nlHsVar true_RDR -fixExprToHsExpr _ (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 foldableModule (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 _ 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) = - noLocA $ mkHsOverLit (mkHsIntegral (mkIntegralLit i)) -constantToHsExpr (F.R d) = - noLocA $ mkHsOverLit (mkHsFractional (mkTHFractionalLit (toRational 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 = noLocA (HsVar Ghc.noExtField (noLocA (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 = GM.prependGHCRealQual (fsLit "mod") - f F.RTimes = times_RDR - f F.RDiv = GM.prependGHCRealQual (fsLit "/") - -brelToHsExpr :: F.Brel -> LHsExpr GhcPs -brelToHsExpr brel = noLocA (HsVar Ghc.noExtField (noLocA (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 = \case - RVar (RTV tv) _ -> nlHsTyVar - NotPromoted - -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv) - (symbolToRdrNameNs tvName (F.symbol tv)) - RFun _ _ tin tout _ - | isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (noLocA [specTypeToLHsType tin]) (specTypeToLHsType tout) - | otherwise -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) - RAllT (ty_var_value -> (RTV tv)) t _ -> noLocA $ HsForAllTy - Ghc.noExtField - (mkHsForAllInvisTele noAnn [noLocA $ UserTyVar noAnn SpecifiedSpec (noLocA $ symbolToRdrNameNs tvName (F.symbol tv))]) - (specTypeToLHsType t) - RAllP _ ty -> specTypeToLHsType ty - RApp RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp - (getRdrName tc) - [ specTypeToLHsType t | t <- ts, notExprArg t ] - where - notExprArg (RExprArg _) = False - notExprArg _ = True - RAllE _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) - REx _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) - RAppTy _ (RExprArg _) _ -> - impossible Nothing "RExprArg should not appear here" - RAppTy t t' _ -> nlHsFunTy (specTypeToLHsType t) (specTypeToLHsType t') - RRTy _ _ _ t -> specTypeToLHsType t - RHole _ -> noLocA $ HsWildCardTy Ghc.noExtField - RExprArg _ -> - todo Nothing "Oops, specTypeToLHsType doesn't know how to handle RExprArg" diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs index 586b53cd51..1dba8cebab 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs @@ -21,7 +21,6 @@ import Data.Hashable () import qualified Data.Maybe as Mb import qualified Language.Fixpoint.Types as F import qualified Language.Fixpoint.Misc as Misc -import Language.Haskell.Liquid.Bare.Elaborate import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Liquid.GHC.API @@ -182,14 +181,11 @@ classDeclToDataDecl cls refinedIds = DataDecl -- functions. Each method type contains the full forall quantifiers -- instead of having them chopped off elaborateClassDcp - :: (Ghc.CoreExpr -> F.Expr) - -> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr) - -> DataConP + :: DataConP -> Ghc.TcRn (DataConP, DataConP) -elaborateClassDcp coreToLg simplifier dcp = do - t' <- flip (zipWith addCoherenceOblig) prefts - <$> forM fts (elaborateSpecType coreToLg simplifier) - let ts' = elaborateMethod (F.symbol dc) (S.fromList xs) <$> t' +elaborateClassDcp dcp = do + let t' = zipWith addCoherenceOblig fts prefts + ts' = elaborateMethod (F.symbol dc) (S.fromList xs) <$> t' pure ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') } , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy x t)) (zip xs t') } @@ -316,11 +312,10 @@ renameTvs rename t makeClassAuxTypes :: - (SpecType -> Ghc.TcRn SpecType) - -> [F.Located DataConP] + [F.Located DataConP] -> [(Ghc.ClsInst, [Ghc.Var])] -> Ghc.TcRn [(Ghc.Var, LocSpecType)] -makeClassAuxTypes elab dcps xs = Misc.concatMapM (makeClassAuxTypesOne elab) dcpInstMethods +makeClassAuxTypes dcps xs = Misc.concatMapM makeClassAuxTypesOne dcpInstMethods where dcpInstMethods = do dcp <- dcps @@ -332,10 +327,9 @@ makeClassAuxTypes elab dcps xs = Misc.concatMapM (makeClassAuxTypesOne elab) dcp pure (dcp, inst, methods) makeClassAuxTypesOne :: - (SpecType -> Ghc.TcRn SpecType) - -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var]) + (F.Located DataConP, Ghc.ClsInst, [Ghc.Var]) -> Ghc.TcRn [(Ghc.Var, LocSpecType)] -makeClassAuxTypesOne elab (ldcp, inst, methods) = +makeClassAuxTypesOne (ldcp, inst, methods) = forM methods $ \method -> do let (headlessSig, preft) = case L.lookup (mkSymbol method) yts' of @@ -353,7 +347,7 @@ makeClassAuxTypesOne elab (ldcp, inst, methods) = ptys . subst (zip clsTvs isSpecTys) $ headlessSig - elaboratedSig <- flip addCoherenceOblig preft <$> elab fullSig + elaboratedSig = addCoherenceOblig fullSig preft let retSig = mapExprReft (\_ -> substAuxMethod dfunSym methodsSet) (F.notracepp ("elaborated" ++ GM.showPpr method) elaboratedSig) let tysub = F.notracepp "tysub" $ M.fromList $ zip (F.notracepp "newtype-vars" $ RT.allTyVars' (F.notracepp "new-type" retSig)) (F.notracepp "ghc-type-vars" (RT.allTyVars' ((F.notracepp "ghc-type" $ RT.ofType (Ghc.varType method)) :: SpecType)))