liquidhaskell-boot-0.9.8.2: src/Language/Haskell/Liquid/Bare/Elaborate.hs
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE CPP #-}
{-# 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.Types
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
#if MIN_VERSION_recursion_schemes(5,2,0)
import Data.Fix hiding (hylo)
#endif
import Data.Char ( isUpper )
import Data.Functor.Foldable
import GHC.Types.Name.Occurrence
import qualified Liquid.GHC.API as Ghc
(noExtField)
import Data.Default ( def )
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 <z :: Nat, w :: Int> . 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 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
instance Corecursive (RType c tv r) where
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 = 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
-- | returns (lambda binders, forall binders)
collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol])
collectSpecTypeBinders = para $ \case
RFunF bind _ (tin, _) (_, (bs, abs')) _ | isClassType tin -> (bs, abs')
| otherwise -> (bind : bs, abs')
RAllEF b _ (_, (bs, abs')) -> (b : bs, abs')
RAllTF (RTVar (RTV ab) _) (_, (bs, abs')) _ -> (bs, F.symbol ab : abs')
RExF b _ (_, (bs, abs')) -> (b : bs, abs')
RAppTyF _ (_, (bs, abs')) _ -> (bs, abs')
RRTyF _ _ _ (_, (bs, abs')) -> (bs, abs')
_ -> ([], [])
-- 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 = para $ \case
RFunF 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
_ -> 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 [] def) [] [] 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)
mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp tyconId tyargs = nlHsTyConApp NotPromoted Prefix tyconId (map HsValArg tyargs)
-- | 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 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 _ 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 (HsOverLit noAnn (mkHsIntegral (mkIntegralLit i)))
constantToHsExpr (F.R d) =
noLocA (HsOverLit noAnn (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 =
flip (ghylo (distPara @SpecType) distAna) (fmap pure . project) $ \case
RVarF (RTV tv) _ -> nlHsTyVar
NotPromoted
-- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv)
(symbolToRdrNameNs tvName (F.symbol tv))
RFunF _ _ (tin, tin') (_, tout) _
| isClassType tin -> noLocA $ HsQualTy Ghc.noExtField (noLocA [tin']) tout
| otherwise -> nlHsFunTy tin' tout
RAllTF (ty_var_value -> (RTV tv)) (_, t) _ -> noLocA $ HsForAllTy
Ghc.noExtField
(mkHsForAllInvisTele noAnn [noLocA $ UserTyVar noAnn SpecifiedSpec (noLocA $ symbolToRdrNameNs tvName (F.symbol tv))])
t
RAllPF _ (_, ty) -> ty
RAppF RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp
(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 _ -> noLocA $ HsWildCardTy Ghc.noExtField
RExprArgF _ ->
todo Nothing "Oops, specTypeToLHsType doesn't know how to handle RExprArg"